Open AccessAutomata for the mu-calculus and Related Results
Author(s) -
David Janin,
Igor Walukiewicz
Publication year - 1995
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v2i27.19929
Subject(s) - mathematics , satisfiability , expressive power , discrete mathematics , propositional calculus , automaton , calculus (dental) , combinatorics , algebra over a field , pure mathematics , computer science , programming language , theoretical computer science , medicine , dentistry
The propositional mu-calculus as introduced by Kozen in [4] 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.