Title :
Checking Interval Properties of Computations
Author :
Montanari, Alessandro ; Murano, Aniello ; Perelli, Giuseppe ; Peron, Adriano
Author_Institution :
Univ. degli Studi di Udine, Udine, Italy
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 and AAbarEEbar.
Keywords :
formal verification; temporal logic; Halpern interval temporal logic; Kripke structures; PSpace decision procedure; Shoham interval temporal logic HS; formal verification; interval logic setting; interval property checking; model checking problem; point-wise logic; system model; Abstracts; Artificial intelligence; Bismuth; Computational modeling; Labeling; Model checking; Semantics;
Conference_Titel :
Temporal Representation and Reasoning (TIME), 2014 21st International Symposium on
Conference_Location :
Verona
Print_ISBN :
978-1-4799-4228-2
DOI :
10.1109/TIME.2014.24