Interval Temporal Logic Model Checking Based on Track Bisimilarity and Prefix Sampling

Since the late 80s, LTL and CTL model checking have been extensively applied in various areas of computer science and AI. Even though they proved themselves to be quite successful in many application domains, there are some relevant temporal conditions which are inher- ently \interval based" (this is the case, for instance, with telic statements like \the astronaut must walk home in an hour" and temporal aggrega- tions like \the average speed of the rover cannot exceed the established threshold") and thus cannot be properly modelled by point-based tem- poral logics. In general, to check interval properties of the behavior of a system, one needs to collect information about states into behavior stretches, which amounts to interpreting each nite sequence of states as an interval and to suitably dening its labelling on the basis of the labelling of the states that compose it. In order to deal with these properties, a model checking framework based on Halpern and Shoham's interval temporal logic (HS for short) and its fragments has been recently proposed and systematically investigated in the literature. In this paper, we give an original proof of EXPSPACE membership of the model checking problem for the HS fragment AABBE (resp., AAEBE) of Allen's interval relations meets, met-by, started-by (resp., nished-by), starts, and nishes. The proof exploits track bisimi- larity and prex sampling, and it turns out to be much simpler than the previously known one. In addition, it improves some upper bounds.