Difference between revisions of "Publications/babiak.15.cav"

From LRDE

(Created page with "{{Publication | published = true | date = 2015-04-27 | authors = Tomáš Babiak, František Blahoudek, Alexandre Duret-Lutz, Joachim Klein, Jan Kv retínský, David Müller, D...")
 
 
(11 intermediate revisions by the same user not shown)
Line 5: Line 5:
 
| title = The Hanoi Omega-Automata Format
  
| title = The Hanoi Omega-Automata Format
 
| booktitle = Proceedings of the 27th International Conference on Computer Aided Verification (CAV'15)
  
| booktitle = Proceedings of the 27th International Conference on Computer Aided Verification (CAV'15)
−
| volume = ???
 +
| volume = 9206
 
| series = Lecture Notes in Computer Science
  
| series = Lecture Notes in Computer Science
−
| pages = ??? to ???
 +
| pages = 479 to 486
 
| publisher = Springer
  
| publisher = Springer
  ⚫
| 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.
−
| urllrde = 201507-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.
  
 
| lrdeprojects = Spot
  
| lrdeprojects = Spot
 
| lrdenewsdate = 2015-04-27
  
| lrdenewsdate = 2015-04-27
  +
| lrdepaper = http://www.lrde.epita.fr/dload/papers/babiak.15.cav.pdf
−
| note = To appear.
  
  +
| lrdeposter = http://www.lrde.epita.fr/dload/papers/babiak.15.cav.poster.pdf
 
| type = inproceedings
  
| type = inproceedings
 
| id = babiak.15.cav
  
| id = babiak.15.cav
  +
| identifier = doi:10.1007/978-3-319-21690-4_31
 
| bibtex =
 
| bibtex =
 
@InProceedings<nowiki>{</nowiki> babiak.15.cav,
  
@InProceedings<nowiki>{</nowiki> babiak.15.cav,
 
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>\'<nowiki>{</nowiki>\i<nowiki>}</nowiki><nowiki>}</nowiki>nsk<nowiki>{</nowiki>\'<nowiki>{</nowiki>y<nowiki>}</nowiki><nowiki>}</nowiki> and David M<nowiki>{</nowiki>\"u<nowiki>}</nowiki>ller and David
 +
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
−
Parker and Jan Strej<nowiki>{</nowiki>\v<nowiki>{</nowiki>c<nowiki>}</nowiki><nowiki>}</nowiki>ek<nowiki>}</nowiki>,
 +
and Jan Strej<nowiki>{</nowiki>\v<nowiki>{</nowiki>c<nowiki>}</nowiki><nowiki>}</nowiki>ek<nowiki>}</nowiki>,
−
title = <nowiki>{</nowiki>The Hanoi Omega-Automata 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
 
Computer Aided Verification (CAV'15)<nowiki>}</nowiki>,
  
Computer Aided Verification (CAV'15)<nowiki>}</nowiki>,
 
year = 2015,
  
year = 2015,
−
volume = <nowiki>{</nowiki>???<nowiki>}</nowiki>,
 +
volume = <nowiki>{</nowiki>9206<nowiki>}</nowiki>,
 
series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>,
  
series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>,
−
pages = <nowiki>{</nowiki>???--???<nowiki>}</nowiki>,
 +
pages = <nowiki>{</nowiki>479--486<nowiki>}</nowiki>,
 
month = jul,
  
month = jul,
 
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>,
  
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>,
Line 47: Line 48:
 
state-based or transition-based, and also supports
  
state-based or transition-based, and also supports
 
alternating automata.<nowiki>}</nowiki>,
  
alternating automata.<nowiki>}</nowiki>,
−
note = <nowiki>{</nowiki>To appear.<nowiki>}</nowiki>
 +
doi = <nowiki>{</nowiki>10.1007/978-3-319-21690-4_31<nowiki>}</nowiki>
 
<nowiki>}</nowiki>
  
<nowiki>}</nowiki>
   

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}
}





Retrieved from "https://www.lrde.epita.fr/index.php?title=Publications/babiak.15.cav&oldid=121216"