Reimplementation of testing-automata in Spot

From LRDE

Revision as of 12:29, 27 June 2019 by Bot (talk | contribs) (Created page with "{{CSIReport | authors = Martin Huvelle | title = Reimplementation of testing-automata in Spot | year = 2019 | number = 1906 | abstract = Spot is a library of model checking al...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

Abstract

Spot is a library of model checking algorithms which can manage different kinds of Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \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.