The Hanoi Omega-Automata Format

We propose a succinct, human-readable, flexible, and extensible exchange format for omega-automata, as typically used in formal verification, and implement support for it in a range of established tools. Our aim is to simplify the interaction of tools, helping the research community to build upon other people's work. A key feature of the format is the use of very generic acceptance conditions, specified by Boolean combinations of acceptance primitives, rather than being limited to common cases such as Büchi, Streett, or Rabin. 09: 54 10: 20 Coffee Break

Authors

• Jan Strejcek

Keywords

No keywords are indexed for this paper.