Nested Emptiness Search for Generalized Büchi Automata

Issue title: APPLICATION OF CONCURRENCY TO SYSTEM DESIGN (ACSD'04)

Article type: Research Article

Authors: Tauriainen, Heikki

Affiliations: Helsinki University of Technology, Laboratory for Theoretical Computer Science, P. O. Box 5400, FI-02015 TKK, Finland. E-mail: [email protected]

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. Avoiding a degeneralization step improves the algorithm's worst-case memory requirements and reduces the worst-case number of state visits during the search. We give experimental results and discuss changes needed to make the generalized algorithmcompatible with well-known probabilistic explicit-state model checking techniques.

Keywords: Model checking, uchi automata, nested depth-first search

Journal: Fundamenta Informaticae, vol. 70, no. 1-2, pp. 127-154, 2006