Automata for the mu-calculus and Related Results
AbstractThe propositional mu-calculus as introduced by Kozen in  is
considered. The notion of disjunctive formula is defined and it is shown
that every formula is semantically equivalent to a disjunctive formula.
For these formulas many difficulties encountered in the general case may
be avoided. For instance, satisfiability checking is linear for disjunctive
formulas. This kind of formula gives rise to a new notion of finite automaton
which characterizes the expressive power of the mu-calculus over
all transition systems.
How to Cite
Janin, D., & Walukiewicz, I. (1995). Automata for the mu-calculus and Related Results. BRICS Report Series, 2(27). https://doi.org/10.7146/brics.v2i27.19929
Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.