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 thoughtheyprovedthemselvestobe quitesuccessfulin manyapplication domains,therearesomerelevanttemporalconditionswhichareinherently “interval based” (this is the case, for instance, with telic statements like “theastronautmustwalkhomeinanhour”andtemporalaggregationslike “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 orderto 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 AAbarBBbarE (resp.,AAbarEBEbar)ofAllen’sintervalrelationsmeets,met-by,started-by (resp., finished-by),starts,andfinishes. The proofexploits 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.