## Fixpoints of Büchi automata

**Mads Dam**
*Abstract:* We give a new and direct proof of the
equivalence between the linear time mu-calculus *v*TL and
Büchi automata. In contrast to previously known constructions
ours is both elementary and compositional. Constructions on
automata are provided which compute their least and greatest fixed
points. Applications include the translation of fragments of the
full branching mu-calculus into the modal mu-calculus, and the
problem of providing reasonable sound and complete axiomaatisations
for *v*TL.

*LFCS report ECS-LFCS-92-224*

This report appeared in the Proceedings of the 12th Conference
on Foundations of Software Technology and Theoretical Computer
Science, Lecture Notes in Computer Science 652 (1992) pp.
39-50.

Previous |

Index |

Next