Translating Path-based Logics to Modal mu-Calculus

Abstract

The modal μ-calculus Lμ is an expressive temporal logic defined on full transition systems. Lμ merely has immediate neighbour modalities and no direct way to specify properties on a path-by-path basis, so it is remarkable that Lμ can simulate logics such as linear temporal logic (LTL) whose semantics are based on linear paths, where an LTL formula ϕ is said to hold at a state s if ϕ holds on every path starting from s. However, expressing such path-based properties in Lμ is generally nontrivial. As a baseline, one may find a translation by constructing an automaton as an intermediate step. However, a naive implementation of such a method may cause a non-elementary blowup in the size of the translation. A translation obtained this way also tends to reflect the structure of the automaton rather than that of the original input formula. In this thesis, we investigate a more syntactic approach to translate path-based logics into Lμ. In particular, we analyse the method given by [Dam94] to translate LTL into Lμ in depth, and reformulate it in several aspects. Furthermore, we generalise the method to the fragment of the linear-time μ-calculus LTμ where fixpoint variables in a formula occur exactly once and are not nested. These translations achieve a worst-case doubly exponential blowup in formula size. For simpler inputs, directly inspecting the translations may yield insights as to how Lμ accommodates path-based properties.