License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2016.26
URN: urn:nbn:de:0030-drops-68615
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/6861/
Bozzelli, Laura ;
Molinari, Alberto ;
Montanari, Angelo ;
Peron, Adriano ;
Sala, Pietro
Interval vs. Point Temporal Logic Model Checking: an Expressiveness Comparison
Abstract
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*).
BibTeX - Entry
@InProceedings{bozzelli_et_al:LIPIcs:2016:6861,
author = {Laura Bozzelli and Alberto Molinari and Angelo Montanari and Adriano Peron and Pietro Sala},
title = {{Interval vs. Point Temporal Logic Model Checking: an Expressiveness Comparison}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {26:1--26:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Akash Lal and S. Akshay and Saket Saurabh and Sandeep Sen},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2016/6861},
URN = {urn:nbn:de:0030-drops-68615},
doi = {10.4230/LIPIcs.FSTTCS.2016.26},
annote = {Keywords: Interval Temporal Logics, Expressiveness, Model Checking}
}
|
Keywords: |
|
Interval Temporal Logics, Expressiveness, Model Checking |
|
Collection: |
|
36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016) |
|
Issue Date: |
|
2016 |
|
Date of publication: |
|
10.12.2016 |
