Branching-time logics and fairness, revisited
Markus Latte · Mathematical Structures in Computer Science · 2021
Abstract Emerson and Halpern (1986,Journal of the Association for Computing Machinery33, 151–178) prove that the Computation Tree Logic (CTL) cannot express the existence of a path on which a proposition holds infinitely often (fairness for short). The scope is widened fromCTLto a general branching-time logic. A path quantifier is followed by a language with temporal descriptions. In this extended setting, the said inexpressiveness is strengthened in two aspects. First, universal path quantifiers are unrestricted. In this way, they are relieved of any temporal quantifiers such as of those in $\mathtt{AU}$ and $\mathtt{AR}$ fromCTL. Second, existential path quantifiers are allowed with any countable language. Instances are the temporal quantifiers in $\mathtt{EU}$ and $\mathtt{ER}$ fromCTL. By contrast, the fairness statement is an existential path quantifier with an uncountable language. Both aspects indicate that this inexpressiveness is optimal with respect to the polarity of path quantifiers and to the cardinality of their languages.