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