Complementing Büchi Automata
From LRDE
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.
- Authors
- Guillaume Sadegh
- Type
- techreport
- Year
- 2009
- Number
- 0903
- Projects
- Spot
- Keywords
- complementation, determinization, Büchi automata, Rabin automata, Safra construction
Abstract
Model checking is a field of formal verification which aims to automatically test the behavior of a system with the help of logic formulae. Spot is a model checking library which relies on one technique: the automata-theoretic approach. In this approach, both system and formula are expressed with Büchi automata, which are automata on infinite words. Spot provides several algorithms to deal with these automata, with model checking as objective. However, an algorithm is missing: the complementation of Büchi automata. Because of its high complexity this algorithm is rarely used in practical, but it does not lack theoretical interests. We will present an implementation of this algorithm in Spot.