2019/10/25 by Jens Oliver Gutsfeld, Gutsfeld, Jens Oliver, Markus Müller-Olm +3
Computer Science · #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Model-Driven Software Engineering Techniques #Natural Language Processing Techniques #cs.FL #cs.LO
paper · pdf · doi:10.48550/arxiv.1910.11594
arxiv created 2019/10/25 · openalex publication_date 2019/10/25 · arxiv updated 2019/10/28 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Computation Tree Logic (CTL) and its extensions CTL* and CTL+ are widely used in automated verification as a basis for common model checking tools. But while they can express many properties of interest like reachability, even simple regular properties like "Every other index is labelled a cannot be expressed in these logics. While many extensions were developed to include regular or even non-regular (e.g. visibly pushdown) languages, the first generic framework, Extended CTL, for CTL with arbitrary language classes was given by Axelsson et. al. and applied to regular, visibly pushdown and (deterministic) context-free languages. We extend this framework to CTL* and CTL+ and analyse it with regard to decidability, complexity, expressivity and satisfiability.