The Hanoi omega-automata format Conference Paper


Author(s): Babiak, Tomáš; Blahoudek, František; Duret-Lutz, Alexandre; Klein, Joachim C; Křetínský, Jan; Mueller, Daniel; Parker, David; Strejček, Jan
Title: The Hanoi omega-automata format
Title Series: LNCS
Affiliation IST Austria
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.
Conference Title: CAV: Computer Aided Verification
Volume: 9206
Conference Dates: July 18-24, 2015
Conference Location: San Francisco, CA, USA
Publisher: Springer  
Date Published: 2015-07-16
Start Page: 479
End Page: 486
DOI: 10.1007/978-3-319-21690-4_31
Notes: T. Babiak, F. Blahoudek, and J. Strejček have been supported by The Czech Science Foundation, grant GBP202/12/G061. J. Klein and D. Müller have been supported by the DFG through the collaborative research centre HAEC (SFB 912), the Excellence Initiative by the German Federal and State Governments (cluster of excellence cfAED and Institutional Strategy), the Graduiertenkolleg QuantLA (1763), and the DFG/NWO-project ROCKS, and the EU-FP-7 grant MEALS (295261). J. Křetínský has been supported in part by the European Research Council (ERC) under grant 267989 (QUAREM), by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), and by the People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007–2013) under REA grant agreement No 291734.
Open access: no
IST Austria Authors
Related IST Austria Work