2026-07-22T05:54:32Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:6233 2024-03-06T10:37:50Z ddc:004 open_access

Computation Tree Logic for Synchronization Properties Chatterjee, Krishnendu Doyen, Laurent Computation Tree Logic Synchronization model-checking complexity 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 hard for the class of problems solvable in polynomial time using a parallel access to an NP oracle. 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Krishnendu Chatterjee and Laurent Doyen 2016 Is Part Of LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2016.98 urn:nbn:de:0030-drops-62334 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.98 eng https://creativecommons.org/licenses/by/3.0/legalcode