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.I documenti in SFERA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
