Nested Emptiness Search for Generalized Büchi Automata

Reference:

Heikki Tauriainen. Nested emptiness search for generalized Büchi automata. Research Report A79, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, July 2003.

Abstract:

We generalize the classic explicit state emptiness checking algorithm for Büchi word automata (the ``nested depth-first search'') into Büchi automata with multiple acceptance conditions. Bypassing an explicit acceptance condition reduction improves the algorithm's worst case memory requirements. The generalized algorithm handles multiple unconditional and weak fairness constraints directly and is compatible with well-known probabilistic explicit state model checking techniques.

Keywords:

Model checking, Büchi automata emptiness checking, nested depth-first search

Suggested BibTeX entry:

@techreport{HUT-TCS-A79,
    address = {Espoo, Finland},
    author = {Heikki Tauriainen},
    institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science},
    month = {July},
    number = {A79},
    pages = {16},
    title = {Nested Emptiness Search for Generalized {B}\"uchi Automata},
    type = {Research Report},
    year = {2003},
}