Difference between revisions of "Publications/babiak.15.cav"
From LRDE
| (One intermediate revision by the same user not shown) | |||
| Line 9: | Line 9: | ||
| pages = 479 to 486 |
| pages = 479 to 486 |
||
| publisher = Springer |
| publisher = Springer |
||
| − | | abstract = We propose a flexible exchange format for |
+ | | abstract = We propose a flexible exchange format for <math>\omega</math>-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. |
| lrdeprojects = Spot |
| lrdeprojects = Spot |
||
| lrdenewsdate = 2015-04-27 |
| lrdenewsdate = 2015-04-27 |
||
| Line 21: | Line 21: | ||
author = <nowiki>{</nowiki>Tom<nowiki>{</nowiki>\'<nowiki>{</nowiki>a<nowiki>}</nowiki>\v<nowiki>{</nowiki>s<nowiki>}</nowiki><nowiki>}</nowiki> Babiak and Franti<nowiki>{</nowiki>\v<nowiki>{</nowiki>s<nowiki>}</nowiki><nowiki>}</nowiki>ek Blahoudek and |
author = <nowiki>{</nowiki>Tom<nowiki>{</nowiki>\'<nowiki>{</nowiki>a<nowiki>}</nowiki>\v<nowiki>{</nowiki>s<nowiki>}</nowiki><nowiki>}</nowiki> Babiak and Franti<nowiki>{</nowiki>\v<nowiki>{</nowiki>s<nowiki>}</nowiki><nowiki>}</nowiki>ek Blahoudek and |
||
Alexandre Duret-Lutz and Joachim Klein and Jan K<nowiki>{</nowiki>\v |
Alexandre Duret-Lutz and Joachim Klein and Jan K<nowiki>{</nowiki>\v |
||
| − | r<nowiki>}</nowiki>et<nowiki>{</nowiki>\' |
+ | r<nowiki>}</nowiki>et<nowiki>{</nowiki>\'i<nowiki>}</nowiki>nsk<nowiki>{</nowiki>\'<nowiki>{</nowiki>y<nowiki>}</nowiki><nowiki>}</nowiki> and David M<nowiki>{</nowiki>\"u<nowiki>}</nowiki>ller and David Parker |
| − | + | and Jan Strej<nowiki>{</nowiki>\v<nowiki>{</nowiki>c<nowiki>}</nowiki><nowiki>}</nowiki>ek<nowiki>}</nowiki>, |
|
title = <nowiki>{</nowiki>The <nowiki>{</nowiki>H<nowiki>}</nowiki>anoi <nowiki>{</nowiki>O<nowiki>}</nowiki>mega-<nowiki>{</nowiki>A<nowiki>}</nowiki>utomata Format<nowiki>}</nowiki>, |
title = <nowiki>{</nowiki>The <nowiki>{</nowiki>H<nowiki>}</nowiki>anoi <nowiki>{</nowiki>O<nowiki>}</nowiki>mega-<nowiki>{</nowiki>A<nowiki>}</nowiki>utomata Format<nowiki>}</nowiki>, |
||
booktitle = <nowiki>{</nowiki>Proceedings of the 27th International Conference on |
booktitle = <nowiki>{</nowiki>Proceedings of the 27th International Conference on |
||
Latest revision as of 23:01, 5 February 2018
- Authors
- Tomáš Babiak, František Blahoudek, Alexandre Duret-Lutz, Joachim Klein, Jan Kv retínský, David Müller, David Parker, Jan Strejček
- Where
- Proceedings of the 27th International Conference on Computer Aided Verification (CAV'15)
- Type
- inproceedings
- Publisher
- Springer
- Projects
- Spot
- Date
- 2015-04-27
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.
Documents
Bibtex (lrde.bib)
@InProceedings{ babiak.15.cav,
author = {Tom{\'{a}\v{s}} Babiak and Franti{\v{s}}ek Blahoudek and
Alexandre Duret-Lutz and Joachim Klein and Jan K{\v
r}et{\'i}nsk{\'{y}} and David M{\"u}ller and David Parker
and Jan Strej{\v{c}}ek},
title = {The {H}anoi {O}mega-{A}utomata Format},
booktitle = {Proceedings of the 27th International Conference on
Computer Aided Verification (CAV'15)},
year = 2015,
volume = {9206},
series = {Lecture Notes in Computer Science},
pages = {479--486},
month = jul,
publisher = {Springer},
abstract = { We propose a flexible 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\"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.},
doi = {10.1007/978-3-319-21690-4_31}
}