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 PS PACE decision procedure for the meaningful fragments AABB and AAEE.
Checking interval properties of computations / Angelo, Monatnari; Murano, Aniello; Giuseppe, Perelli; Peron, Adriano. - (2014), pp. 59-68. (Intervento presentato al convegno TIME 2014, 21st International Symposium on Temporal Representation and Reasoning tenutosi a Verona nel Settembre 2014) [10.1109/TIME.2014.24].
Checking interval properties of computations
MURANO, ANIELLO;PERON, ADRIANO
2014
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 PS PACE decision procedure for the meaningful fragments AABB and AAEE.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.