[Lrde Annonce] New publication: The Hanoi Omega-Automata Format (CAV'15)

I am happy to announce that the following paper has been accepted at the 27th International Conference on Computer Aided Verification (CAV'15), to be held on July 18–24, at San Francisco. The Hanoi Omega-Automata Format Tomáš Babiak¹, František Blahoudek¹, Alexandre Duret-Lutz², Joachim Klein³, Jan Křetínský⁵, David Müller³, David Parker⁴, and Jan Strejček¹ ¹Faculty of Informatics, Masaryk University, Brno, Czech Republic ²LRDE, EPITA, Le Kremlin-Bicêtre, France ³Technische Universität Dresden, Germany ⁴University of Birmingham, UK ⁵IST Austria https://www.lrde.epita.fr/wiki/Publications/babiak.15.cav Abstract: 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üchi, 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. -- Alexandre Duret-Lutz