Complementing Büchi Automata With Alternating Automata

Authors

Guillaume Sadegh

Type

techreport

Year

2010

Number

0915

Projects

Spot

Abstract

Model checking is a field of formal verification which aims to automatically test the behavior of a system with the help of temporal 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. An operation for automata was recently added in Spot : the complementation. Research of algorithms for this operation is still relevant today, since there is still no algorithm reaching the theoretical optimal bound. We will present two recent complementation algorithms implemented in Spot.