Back to Search Start Over

Model checking for fragments of Halpern and Shoham's interval temporal logic based on track representatives.

Authors :
Molinari, Alberto
Montanari, Angelo
Peron, Adriano
Source :
Information & Computation. Apr2018 Part 3, Vol. 259, p412-443. 32p.
Publication Year :
2018

Abstract

Model checking allows one to automatically verify a specification of the expected properties of a system against a formal model of its behavior (generally, a Kripke structure). Point-based temporal logics, such as LTL, CTL, and CTL ⁎ , that describe how the system evolves state-by-state, are commonly used as specification languages. They proved themselves quite successful in a variety of application domains. However, properties constraining the temporal ordering of temporally extended events as well as properties involving temporal aggregations, which are inherently interval-based, can not be properly dealt with by them. Interval temporal logics (ITLs), that take intervals as their primitive temporal entities, turn out to be well-suited for the specification and verification of interval properties of computations (we interpret all the tracks of a Kripke structure as computation intervals). In this paper, we study the model checking problem for some fragments of Halpern and Shoham's modal logic of time intervals (HS). HS features one modality for each possible ordering relation between pairs of intervals (the so-called Allen's relations). First, we describe an EXPSPACE model checking algorithm for the HS fragment of Allen's relations meets , met-by , starts , started-by , and finishes , which exploits the possibility of finding, for each track (of unbounded length), an equivalent bounded-length track representative. While checking a property, it only needs to consider tracks whose length does not exceed the given bound. Then, we prove the model checking problem for such a fragment to be PSPACE-hard. Finally, we identify other well-behaved HS fragments which are expressive enough to capture meaningful interval properties of systems, such as mutual exclusion, state reachability, and non-starvation, and whose computational complexity is less than or equal to that of LTL. [ABSTRACT FROM AUTHOR]

Details

Language :
English
ISSN :
08905401
Volume :
259
Database :
Academic Search Index
Journal :
Information & Computation
Publication Type :
Academic Journal
Accession number :
128475262
Full Text :
https://doi.org/10.1016/j.ic.2017.08.011