2026-07-24T00:57:09Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:6861 2024-03-06T10:39:03Z ddc:004 open_access

Interval vs. Point Temporal Logic Model Checking: an Expressiveness Comparison Bozzelli, Laura Molinari, Alberto Montanari, Angelo Peron, Adriano Sala, Pietro Interval Temporal Logics Expressiveness Model Checking Model checking is a powerful method widely explored in formal verification to check the (state-transition) model of a system against desired properties of its behaviour. Classically, properties are expressed by formulas of a temporal logic, such as LTL, CTL, and CTL*. These logics are "point-wise" interpreted, as they describe how the system evolves state-by-state. On the contrary, Halpern and Shoham's interval temporal logic (HS) is "interval-wise" interpreted, thus allowing one to naturally express properties of computation stretches, spanning a sequence of states, or properties involving temporal aggregations, which are inherently "interval-based". In this paper, we study the expressiveness of HS in model checking, in comparison with that of the standard logics LTL, CTL, and CTL*. To this end, we consider HS endowed with three semantic variants: the state-based semantics, introduced by Montanari et al., which allows branching in the past and in the future, the linear-past semantics, allowing branching only in the future, and the linear semantics, disallowing branching. These variants are compared, as for their expressiveness, among themselves and to standard temporal logics, getting a complete picture. In particular, HS with linear (resp., linear-past) semantics is proved to be equivalent to LTL (resp., finitary CTL*). Schloss Dagstuhl – Leibniz-Zentrum für Informatik Laura Bozzelli and Alberto Molinari and Angelo Montanari and Adriano Peron and Pietro Sala 2016 Is Part Of LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2016.26 urn:nbn:de:0030-drops-68615 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.26 eng https://creativecommons.org/licenses/by/3.0/legalcode