Computation tree logic for synchronization properties
Download
Conference Paper
| Published
| English
Scopus indexed
Author
Chatterjee, KrishnenduISTA
;
Doyen, Laurent

Department
Grant
Series Title
LIPIcs
Abstract
We present a logic that extends CTL (Computation Tree Logic) with operators that express synchronization properties. A property is synchronized in a system if it holds in all paths of a certain length. The new logic is obtained by using the same path quantifiers and temporal operators as in CTL, but allowing a different order of the quantifiers. This small syntactic variation induces a logic that can express non-regular properties for which known extensions of MSO with equality of path length are undecidable. We show that our variant of CTL is decidable and that the model-checking problem is in Delta_3^P = P^{NP^NP}, and is DP-hard. We analogously consider quantifier exchange in extensions of CTL, and we present operators defined using basic operators of CTL* that express the occurrence of infinitely many synchronization points. We show that the model-checking problem remains in Delta_3^P. The distinguishing power of CTL and of our new logic coincide if the Next operator is allowed in the logics, thus the classical bisimulation quotient can be used for state-space reduction before model checking.
Publishing Year
Date Published
2016-01-01
Publisher
Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Acknowledgement
This research was partially supported by Austrian Science Fund (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant (279307: Graph Games), Vienna Science and Technology Fund (WWTF) through project ICT15-003, and European project Cassting (FP7-601148).
We thank Stefan Göller and anonymous reviewers for their insightful
comments and suggestions.
Volume
55
Article Number
98
Conference
ICALP: Automata, Languages and Programming
Conference Location
Rome, Italy
Conference Date
2016-07-12 – 2016-07-15
IST-REx-ID
All files available under the following license(s):
Creative Commons Attribution 4.0 International Public License (CC-BY 4.0):
Main File(s)
File Name
Access Level

Date Uploaded
2018-12-12