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