Reimplementation of testing-automata in Spot

Authors

Martin Huvelle

Type

techreport

Year

2019

Number

1906

Abstract

Spot is a library of model checking algorithms which can manage different kinds of $\omega$-automata. It can also handle testing-automata since Spot 1.0. However, Spot 2.0 introduced a new data structure for automata with generic acceptance conditions that were not available when testing automata where developed. Our goal is to reimplement testing-automata using the more modern data structure. By doing so, we expect to reuse existing algorithms, to reduce the amount code specific to testing automata, and to make testing automata compatible with HOA format. Additionally, our preliminary implementation seems to produce smaller testing-automata than the original one.