Complementing Büchi Automata

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.