Language Containment Checking with Nondeterministic BDDs

Abstract. Checking for language containment between nondeterministic ω-automata is a central task in automata-based hierarchical verification. We present a symbolic procedure for language containment checking between two B¨uchi automata. Our algorithm avoids determinization by intersecting the implementation automaton with the complement of the specification automaton as an alternating automaton. We present a fixpoint algorithm for the emptiness check of alternating automata. The main data structure is a nondeterministic extension of binary decision diagrams that canonically represents sets of Boolean functions. This is a slightly revised version (April 2001) of the following article: c 2001 Springer-Verlag. Bernd Finkbeiner. Language Containment Checking with Nondetermistic BDDs. In Tiziana

• Type: Conference
• Year: 2001
• Where: TACAS
• Authors: Bernd Finkbeiner
• Keywords: Algorithms, Automata-based Hierarchical Verification, Checking, Language Containment, TACAS 2001