Interval vs. Point Temporal Logic Model Checking: an Expressiveness Comparison
From MaRDI portal
(Redirected from Publication:4636573)
Abstract: In the last 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 paper, 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., 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*).
Recommendations
- Interval vs. point temporal logic model checking. An expressiveness comparison
- Model checking interval temporal logics with regular expressions
- scientific article; zbMATH DE number 2196601
- An in-depth investigation of interval temporal logic model checking with regular expressions
- Complexity analysis of a unifying algorithm for model checking interval temporal logic
- Complexity analysis of a unifying algorithm for model checking interval temporal logic
- scientific article; zbMATH DE number 6767596
- Model-checking timed temporal logics
- Evaluation of temporal datasets via interval temporal logic model checking
- Constraining cycle alternations in model checking for interval temporal logic
Cited in
(14)- Model checking for fragments of Halpern and Shoham's interval temporal logic based on track representatives
- Which fragments of the interval temporal logic HS are tractable in model checking?
- Decidability and complexity of the fragments of the modal logic of Allen's relations over the rationals
- Model checking for fragments of the interval temporal logic HS at the low levels of the polynomial time hierarchy
- Model checking interval temporal logics with regular expressions
- Interval temporal logic model checking: the border between good and bad HS fragments
- Checking interval properties of computations
- On the complexity of model checking for syntactically maximal fragments of the interval temporal logic HS with regular expressions
- Interval vs. point temporal logic model checking. An expressiveness comparison
- A separation theorem for discrete-time interval temporal logic
- An in-depth investigation of interval temporal logic model checking with regular expressions
- scientific article; zbMATH DE number 6767596 (Why is no real title available?)
- An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning
- An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning
This page was built for publication: Interval vs. Point Temporal Logic Model Checking: an Expressiveness Comparison
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4636573)
