Temporal Logics, Automata and the Modal $\mu$-Calculus
Sander in 't Veld

Abstract:
Computation tree logic (CTL) and its extension CTL offer a rigorous approach to program verification. The highly expressive modal μ-calculus subsumes both CTL and CTL∗ while remaining computationally well-behaved. Translations from CTL and CTL* into the modal μ-calculus are known, but the resulting fragments have not been identified syntactically. Having an exact characterization of a logic as a fragment of the modal μ-calculus gives a better understanding of the expressivity of both logics involved. An automata theoretic approach serves to form a bridge between logics and game semantics are instrumental when comparing formulas with automata.
In this thesis CTL∗ is translated into a class of modal parity automata. An exact characterization of this class of automata as a fragment of the modal μ-calculus is given. Furthermore CTL is fully characterized both as a class of modal automata with singleton clusters and as a one-variable fragment of the modal μ-calculus.