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

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