The transitive µ-calculus is Büchi definable
Giacomo Lenzi · Annual Conference on Computers · 2006
The Modal µ-Calculus is an extension of Modal Logic with two operators for least (µ) and greatest (ν) fixpoints of monotone functions. This logic is widely used as a tool for specification and verification of computer systems. We show that, on transitive structures, every formula of the µ-Calculus is equivalent to a Buchi automaton.