Automaton-Based Criteria for Membership in CTL

Authors: Udi Boker and Yariv Shaulian

Paper Information

Title:Automaton-Based Criteria for Membership in CTL
Authors:Udi Boker and Yariv Shaulian
Proceedings:LICS PDF files
Editors: Anuj Dawar and Erich Grädel
Keywords:Computation Tree Logic, Tree automata, Linear Temporal Logic, Omega-regular languages

ABSTRACT. Computation Tree Logic (CTL) is widely used in formal verification, however, unlike linear temporal logic (LTL), its connection to automata over words and trees is not yet fully understood. Moreover, the long sought connection between LTL and CTL is still missing; It is not known whether their common fragment is decidable, and there are very limited necessary conditions and sufficient conditions for checking whether an LTL formula is definable in CTL.

We provide sufficient conditions and necessary conditions for LTL formulas and omega-regular languages to be expressible in CTL. The conditions are automaton-based; We first tighten the automaton characterization of CTL to the class of Hesitant Alternating Linear Tree Automata (HALT), and then conduct the conditions by relating between the cycles of a word automaton for a given omega-regular language and the cycles of a potentially equivalent HALT.

The new conditions allow to simplify proofs of known results on languages that are definable, or not, in CTL, as well as to prove new results. Among which, they allow us to refute a conjecture by Clarke and Draghicescu from 1988, regarding a condition for a CTL* formula to be expressible in CTL.

Talk:Jul 09 17:00 (Session 51D)