zbMATH — the first resource for mathematics

Automata for the modal \(\mu \)-calculus and related results. (English) Zbl 1193.68163
Wiedermann, Jiří (ed.) et al., Mathematical foundations of computer science 1995. 20th international symposium, MFCS ’95, Prague, Czech Republic, August 28-September 1, 1995. Proceedings. Berlin: Springer-Verlag (ISBN 3-540-60246-1). Lect. Notes Comput. Sci. 969, 552-562 (1995).
Summary: The propositional \(\mu\)-calculus as introduced by Kozen 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.
For the entire collection see [Zbl 0847.00052].

68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science
68Q45 Formal languages and automata
Full Text: DOI