In recent years, model checking with interval temporal logics is emerging as a viable alternative to model checking with standard point-based temporal logics, such as LTL, CTL, CTL∗, and the like. The behavior of the system is modeled by means of (finite) Kripke structures, as usual. However, while temporal logics which are interpreted “point-wise” describe how the system evolves state-by-state, and predicate properties of system states, those which are interpreted “interval-wise” express properties of computation stretches, spanning a sequence of states. A proposition letter is assumed to hold over a computation stretch (interval) if and only if it holds over each component state (homogeneity assumption). A natural question arises: is there any advantage in replacing points by intervals as the primary temporal entities, or is it just a matter of taste? In this article, we study the expressiveness of Halpern and Shoham's interval temporal logic (HS) in model checking, in comparison with those of LTL, CTL, and CTL∗. To this end, we consider three semantic variants of HS: the state-based one, introduced by Montanari et al. in [30, 34], that allows time to branch both in the past and in the future, the computation-tree-based one, that allows time to branch in the future only, and the trace-based variant, that disallows time to branch. These variants are compared among themselves and to the aforementioned standard logics, getting a complete picture. In particular, we show that HS with trace-based semantics is equivalent to LTL (but at least exponentially more succinct), HS with computation-tree-based semantics is equivalent to finitary CTL∗, and HS with state-based semantics is incomparable with all of them (LTL, CTL, and CTL∗). © 2018 Association for Computing Machinery.

Interval vs. point temporal logic model checking: An expressiveness comparison / Bozzelli, Laura; Molinari, Alberto; Montanari, Angelo; Peron, Adriano; Sala, Pietro. - In: ACM TRANSACTIONS ON COMPUTATIONAL LOGIC. - ISSN 1529-3785. - 20:1(2019), pp. 1-31. [10.1145/3281028]

Interval vs. point temporal logic model checking: An expressiveness comparison

Bozzelli, Laura
;
Montanari, Angelo
;
Peron, Adriano
;
2019

Abstract

In recent years, model checking with interval temporal logics is emerging as a viable alternative to model checking with standard point-based temporal logics, such as LTL, CTL, CTL∗, and the like. The behavior of the system is modeled by means of (finite) Kripke structures, as usual. However, while temporal logics which are interpreted “point-wise” describe how the system evolves state-by-state, and predicate properties of system states, those which are interpreted “interval-wise” express properties of computation stretches, spanning a sequence of states. A proposition letter is assumed to hold over a computation stretch (interval) if and only if it holds over each component state (homogeneity assumption). A natural question arises: is there any advantage in replacing points by intervals as the primary temporal entities, or is it just a matter of taste? In this article, we study the expressiveness of Halpern and Shoham's interval temporal logic (HS) in model checking, in comparison with those of LTL, CTL, and CTL∗. To this end, we consider three semantic variants of HS: the state-based one, introduced by Montanari et al. in [30, 34], that allows time to branch both in the past and in the future, the computation-tree-based one, that allows time to branch in the future only, and the trace-based variant, that disallows time to branch. These variants are compared among themselves and to the aforementioned standard logics, getting a complete picture. In particular, we show that HS with trace-based semantics is equivalent to LTL (but at least exponentially more succinct), HS with computation-tree-based semantics is equivalent to finitary CTL∗, and HS with state-based semantics is incomparable with all of them (LTL, CTL, and CTL∗). © 2018 Association for Computing Machinery.
2019
Interval vs. point temporal logic model checking: An expressiveness comparison / Bozzelli, Laura; Molinari, Alberto; Montanari, Angelo; Peron, Adriano; Sala, Pietro. - In: ACM TRANSACTIONS ON COMPUTATIONAL LOGIC. - ISSN 1529-3785. - 20:1(2019), pp. 1-31. [10.1145/3281028]
File in questo prodotto:
File Dimensione Formato  
tocl.pdf

non disponibili

Descrizione: Articolo principale
Tipologia: Documento in Post-print
Licenza: Accesso privato/ristretto
Dimensione 928.99 kB
Formato Adobe PDF
928.99 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/11588/727990
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 17
  • ???jsp.display-item.citation.isi??? 10
social impact