Checking Interval Properties of Computations

Citations Over TimeTop 10% of 2014 papers

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 behavior, one can verify whether the system meets the behavior by checking the formula against the model. Classically, system behavior is given as 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 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 Kripke structures, which allows one to check interval properties of computations. Then, we prove that the model checking problem for HS against Kripke structures is decidable by a suitable small model theorem, and we outline a PSPACE decision procedure for the meaningful fragments AAbarBBbar e and AAbarEEbar.

Related Papers

• → Checking Interval Properties of Computations(2014)15 cited
• → A Probabilistic Temporal Logic with Frequency Operators and Its Model Checking(2011)8 cited
• A Linear Temporal Logic with Clocks for Verification of Real-Time Systems(2002)
• → Characterizing Kripke structures in temporal logic. Interim report(1987)1 cited
• Formal modelling and verification of multi-robot systems specified with temporal logic(2010)