On Translating Linear Temporal Logic into Alternating and Nondeterministic Automata


Heikki Tauriainen. On translating linear temporal logic into alternating and nondeterministic automata. Research Report A83, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, December 2003.


Automata theory provides valuable tools for designing and implementing decision procedures for temporal logics and their applications to automatic verification of systems against their logical specifications. Implementing these decision procedures by analyzing automata built from the systems and their specifications with translation procedures is nevertheless very challenging in practice due to the tendency of the automata to grow easily unmanageably large as the size of the systems or (especially) the logical specifications increases.

This thesis develops the theory of translating future-time propositional linear temporal logic (LTL) into nondeterministic automata via linear alternating automata. Unlike nondeterministic automata, linear alternating automata are expressively equivalent to LTL and allow a conceptually simple translation of LTL specifications into automata using a set of rules for building automata incrementally from smaller components. The proposed unified generalized definition for both alternating and nondeterministic automata facilitates combining the rules with new minimization heuristics for alternating automata, based on the general theory of using language containment tests and structural analysis of automata for removing transitions. The generalized definition supports translation of linear alternating automata into nondeterministic automata within the best known limit for the worst case increase in the number of states of the resulting automata. The translation construction also reveals a simple syntactic subclass of LTL for which the exponential increase in the number of states can always be avoided. Additionally, the emptiness of generalized nondeterministic automata is shown to be decidable without degeneralization by using a new variant of the well-known nested depth-first search algorithm.


linear temporal logic, alternating automata, automata minimization, nested depth-first search

Suggested BibTeX entry:

    address = {Espoo, Finland},
    author = {Heikki Tauriainen},
    institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science},
    month = {December},
    number = {A83},
    pages = {132},
    title = {On Translating Linear Temporal Logic into Alternating and Nondeterministic Automata},
    type = {Research Report},
    year = {2003},

NOTE: Reprint of Licentiate's thesis.
PostScript (2 MB)
GZipped PostScript (717 kB)
PDF (1 MB)