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 inherently “interval based” (this is the case, for instance, with telic statements like “the astronaut must walk home in an hour” and temporal aggregations like “the average speed of the rover cannot exceed the established threshold”) and thus cannot be properly modelled by point-based temporal 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 finite sequence of states as an interval and to suitably defining 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., finished-by), starts, and finishes. The proof exploits track bisimilarity and prefix sampling, and it turns out to be much simpler than the previously known one. In addition, it improves some upper bounds.