## Composing a Büchi machine for LTL

Classical Büchi automata and state-labeled Büchi automata are
generalized here to Büchi machines without change of expressibility.
LTL stands for linear temporal logic with the temporal operators for
until, next, and release. A construction of a Büchi machine for a
given LTL formula is proposed that uses induction on the structure of
the LTL formula. The constituents of this machine are constructors
for the temporal opators in the formula. Various constructors are
proposed. One set of constructors aims at few states. Another set
yields a state-labeled Büchi machine. In the latter case, there are
short-cuts for composed operators.

Almost all results have been verified with the proof assistant
PVS. see the
PVS dumpfile.

Comments and questions are welcome.

Back to my home page.

Wim H. Hesselink

Last modified: Thu Apr 22 15:31:21 CEST 2021