Abstract: We give a new and direct proof of the equivalence between the linear time mu-calculus vTL 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 vTL.
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 An error occured whilst processing this directive