The Hanoi Omega-Automata Format

We propose a flexible exchange format for ω-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¨uchi, Streett, or Rabin. Such flexibility in the choice of acceptance conditions can be exploited in applications, for example in probabilistic model checking, and furthermore encourages the development of acceptance-agnostic tools for automata manipulations. The format allows acceptance conditions that are either state-based or transition-based, and also supports alternating automata.

• Type: Journal
• Year: 2015
• Where: CAV
• Authors: Tomás Babiak, Frantisek Blahoudek, Alexandre Duret-Lutz, Joachim Klein 0001, Jan Kretínský, David Müller 0001, David Parker 0001, Jan Strejcek
• Keywords: CAV 2015, Hardware