Computation tree logic for synchronization properties

Chatterjee, Krishnendu and Doyen, Laurent (2016) Computation tree logic for synchronization properties. In: ICALP: International Colloquium on Automata, Languages and Programming , July 12-15, 2016, Rome, IT.

[img] PDF
Download (533Kb)
Official URL:


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.

Item Type: Conference or Workshop Item (Paper)
Uncontrolled Keywords: complexity, computation tree logic, synchronization, model-checking
Subjects: 000 Computer science, knowledge & general works > 000 Computer science, knowledge & systems > 005 Computer programming, programs & data
Research Group: Chatterjee Group
SWORD Depositor: Sword Import User
Depositing User: Sword Import User
Date Deposited: 21 Apr 2017 05:47
Last Modified: 21 Apr 2017 05:47

Actions (login required)

View Item View Item