Alternating automata support

Authors

Amaury Fauchille

Type

techreport

Year

2016

Number

1612

Abstract

Alternating automata add a universal branching to the existential branching from non-deterministic automata. Büchi alternating automata are exponentially more concise than non-deterministic Büchi automata. Additionally, they are well suited to translate linear temporal logic as their size is proportional to the translated formula. This work aims to add alternating automata support to Spot. This will make Spot compatible with other tools producing or using aternating automata, and allow future algorithms working on alternating automata to be implemented.