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.

Checking Interval Properties of Computations

MONTANARI, Angelo;
2014-01-01

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.
File in questo prodotto:
File Dimensione Formato  
Article.pdf

non disponibili

Tipologia: Documento in Pre-print
Licenza: Non pubblico
Dimensione 336.32 kB
Formato Adobe PDF
336.32 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

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/11390/1037148
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 16
  • ???jsp.display-item.citation.isi??? 9
social impact