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.

Checking interval properties of computations / Molinari, Alberto; Montanari, Angelo; Murano, Aniello; Perelli, Giuseppe; Peron, Adriano. - In: ACTA INFORMATICA. - ISSN 1432-0525. - 53:6-8(2016), pp. 587-619. [10.1007/s00236-015-0250-1]

Checking interval properties of computations

Giuseppe Perelli;
2016

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.
2016
interval temporal logics; model checking; Kripke structures; complexity
01 Pubblicazione su rivista::01a Articolo in rivista
Checking interval properties of computations / Molinari, Alberto; Montanari, Angelo; Murano, Aniello; Perelli, Giuseppe; Peron, Adriano. - In: ACTA INFORMATICA. - ISSN 1432-0525. - 53:6-8(2016), pp. 587-619. [10.1007/s00236-015-0250-1]
File allegati a questo prodotto
File Dimensione Formato  
Molinari_Checking_2016.pdf

solo gestori archivio

Tipologia: Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 1.01 MB
Formato Adobe PDF
1.01 MB Adobe PDF   Contatta l'autore

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11573/1403529
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 43
  • ???jsp.display-item.citation.isi??? 20
social impact