Alternating automata support


Revision as of 17:04, 9 January 2018 by Bot (talk | contribs) (Created page with "{{CSIReport | authors = Amaury Fauchille | title = Alternating automata support | year = 2016 | number = 1612 | abstract = Alternating automata add a universal branching to th...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)


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.