Temporal Logics with Language Parameters

TL;DR

This paper extends the framework of CTL with language parameters to CTL* and CTL+, analyzing their decidability, complexity, and expressivity for various language classes, enhancing model checking capabilities.

Contribution

It generalizes the Extended CTL framework to CTL* and CTL+, providing a comprehensive analysis of their properties across different language classes.

Findings

Decidability results for extended CTL* and CTL+

Complexity classifications for model checking with language parameters

Enhanced expressivity for regular, visibly pushdown, and context-free languages

Abstract

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.