Automata and Linear Temporal Logic: Translations with Transition-Based Acceptance

Reference:

Heikki Tauriainen. Automata and linear temporal logic: Translations with transition-based acceptance. Research Report A104, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, September 2006. Doctoral dissertation.

Abstract:

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

This thesis develops the theory of translating propositional linear time temporal logic (LTL) into nondeterministic automata via self-loop alternating automata. Unlike nondeterministic automata, self-loop 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 use of generalized transition-based acceptance for automata throughout all constructions gives rise to new optimized translation rules and facilitates designing heuristics for the minimization of automata by making use of language containment tests combined with structural analysis of automata. The generalized definition also supports the translation of self-loop alternating automata into nondeterministic automata by essentially applying the standard subset construction; this construction can be further simplified and optimized when working with automata built from LTL formulas. The translation rules can also be used to identify a syntactic subclass of LTL for which the exponential increase caused by the subset construction in the number of states of the automaton can always be avoided; consequently, the satisfiability problem for this subclass, which is shown to extend related subclasses known from the literature, is NP-complete. Additionally, the emptiness of generalized nondeterministic automata is shown to be testable without giving up generalized transition-based acceptance by using a new variant of the well-known nested depth-first search algorithm with improved worst-case resource requirements.

Keywords:

linear time temporal logic, alternating automata, nondeterministic automata, transition-based acceptance, minimization, nondeterminization, emptiness checking, nested depth-first search

Suggested BibTeX entry:

@techreport{HUT-TCS-A104,
    address = {Espoo, Finland},
    author = {Heikki Tauriainen},
    institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science},
    month = {September},
    note = {Doctoral dissertation},
    number = {A104},
    pages = {xii+229},
    title = {Automata and Linear Temporal Logic: Translations with Transition-Based Acceptance},
    type = {Research Report},
    year = {2006},
}