Computation Tree Logic for Synchronization Properties

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. The talk is based on a joint work with Krishnendu Chatterjee (accepted at ICALP 2016)

Authors

• Krishnendu Chatterjee Institute of Science and Technology Austria
• Laurent Doyen

Keywords

No keywords are indexed for this paper.