Model checking is the process of establishing whether a certain formula is satisfied by a given structure, and it is usually associated with point-based temporal logics. Recently, the question of how to correctly define and study the model checking problem for interval-based temporal logics has been raised. In this paper, we focus on a very natural finite version of the model checking problem for Halpern and Shoham's modal logic of time intervals, a.k.a. HS, for which an algorithm that behaves in a very effcient way (under certain conditions) can be designed. We present an implementation of such an algorithm and analyse its performance through a systematic series of tests.

A Model Checker for Interval Temporal Logics over Finite Structures

SCIAVICCO, Guido
2017

Abstract

Model checking is the process of establishing whether a certain formula is satisfied by a given structure, and it is usually associated with point-based temporal logics. Recently, the question of how to correctly define and study the model checking problem for interval-based temporal logics has been raised. In this paper, we focus on a very natural finite version of the model checking problem for Halpern and Shoham's modal logic of time intervals, a.k.a. HS, for which an algorithm that behaves in a very effcient way (under certain conditions) can be designed. We present an implementation of such an algorithm and analyse its performance through a systematic series of tests.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in SFERA 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/11392/2376364
 Attenzione

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

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