Abstract
We give a new and direct proof of the equivalence between the finear time µ-calculus νTL and Büchi automata. Constructions on automata are given which compute their least and greatest fixed points. Together with other well-known constructions corresponding to the remaining νTL connectives the result is a representation of νTL as Büchi automata which in contrast to previously known constructions is both elementary and compositional. Applications to the problem of completely axiomatising νTL are discussed.
Cite
CITATION STYLE
Dam, M. (1992). Fixed points of büchi automata. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 652 LNCS, pp. 39–50). Springer Verlag. https://doi.org/10.1007/3-540-56287-7_93
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
