Checking Interval Properties of Computations

Abstract

Model checking is a powerful method widely explored in formal verification. Given a model of a system, e.g., a Kripke structure, and a formula specifying its expected behaviour, one can verify whether the system meets the behaviour by checking the formula against the model. Classically, system behaviour is expressed by a formula of a temporal logic, such as LTL and the like. These logics are "point-wise" interpreted, as they describe how the system evolves state-by-state. However, there are relevant properties, such as those constraining the temporal relations between pairs of temporally extended events or involving temporal aggregations, which are inherently "interval-based", and thus asking for an interval temporal logic. In this paper, we give a formalization of the model checking problem in an interval logic setting. First, we provide an interpretation of formulas of Halpern and Shoham's interval temporal logic HS over finite Kripke structures, which allows one to check interval properties of computations. Then, we prove that the model checking problem for HS against finite Kripke structures is decidable by a suitable small model theorem, and we provide a lower bound to its computational complexity.

In Journal: Acta Informatica, Springer Berlin Heidelber, 2015

Cited by in corpus (11)

• On the Complexity of Model Checking for Syntactically Maximal Fragments of the Interval Temporal Logic HS with Regular Expressions
• Complexity of ITL model checking: some well-behaved fragments of the interval logic HS
• Interval vs. Point Temporal Logic Model Checking: an Expressiveness Comparison
• Model Checking for Fragments of Halpern and Shoham's Interval Temporal Logic Based on Track Representatives
• Satisfiability and Model Checking for the Logic of Sub-Intervals under the Homogeneity Assumption
• Adding the Relation Meets to the Temporal Logic of Prefixes and Infixes makes it EXPSPACE-Complete
• Model Checking the Logic of Allen's Relations Meets and Started-by is $P^{N}P$-Complete
• Model checking: the interval way
• Model Checking Epistemic Halpern-Shoham Logic Extended with Regular Expressions
• The addition of temporal neighborhood makes the logic of prefixes and sub-intervals EXPSPACE-complete
• Parametric Interval Temporal Logic over Infinite Words