Difference between revisions of "Publications/blahoudek.14.spin"

From LRDE

(Created page with "{{Publication | published = true | date = 2014-06-16 | authors = František Blahoudek, Alexandre Duret-Lutz, Mojmír Křetínský, Jan Strejček | title = Is There a Best Büc...")
 
 
(8 intermediate revisions by the same user not shown)
Line 5: Line 5:
 
| title = Is There a Best Büchi Automaton for Explicit Model Checking?
  
| title = Is There a Best Büchi Automaton for Explicit Model Checking?
 
| booktitle = Proceedings of the 21th International SPIN Symposium on Model Checking of Software (SPIN'14)
  
| booktitle = Proceedings of the 21th International SPIN Symposium on Model Checking of Software (SPIN'14)
  +
| pages = 68 to 76
 
| publisher = ACM
  
| publisher = ACM
−
| urllrde = 201407-Spin
  
 
| abstract = LTL to Büchi automata (BA) translators are traditionally optimized to produce automata with a small number of states or a small number of non-deterministic states. In this paper, we search for properties of Büchi automata that really influence the performance of explicit model checkers. We do that by manual analysis of several automata and by experiments with common LTL-to-BA translators and realistic verification tasks. As a result of these experiences, we gain a better insight into the characteristics of automata that work well with Spin.
  
| abstract = LTL to Büchi automata (BA) translators are traditionally optimized to produce automata with a small number of states or a small number of non-deterministic states. In this paper, we search for properties of Büchi automata that really influence the performance of explicit model checkers. We do that by manual analysis of several automata and by experiments with common LTL-to-BA translators and realistic verification tasks. As a result of these experiences, we gain a better insight into the characteristics of automata that work well with Spin.
 
| lrdeprojects = Spot
  
| lrdeprojects = Spot
 
| lrdenewsdate = 2014-06-16
  
| lrdenewsdate = 2014-06-16
 
| lrdepaper = http://www.lrde.epita.fr/dload/papers/blahoudek.14.spin.pdf
  
| lrdepaper = http://www.lrde.epita.fr/dload/papers/blahoudek.14.spin.pdf
−
| note = To appear
  
 
| type = inproceedings
  
| type = inproceedings
 
| id = blahoudek.14.spin
  
| id = blahoudek.14.spin
  +
| identifier = doi:10.1145/2632362.2632377
 
| bibtex =
 
| bibtex =
 
@InProceedings<nowiki>{</nowiki> blahoudek.14.spin,
  
@InProceedings<nowiki>{</nowiki> blahoudek.14.spin,
Line 22: Line 22:
 
booktitle = <nowiki>{</nowiki>Proceedings of the 21th International SPIN Symposium on
  
booktitle = <nowiki>{</nowiki>Proceedings of the 21th International SPIN Symposium on
 
Model Checking of Software (SPIN'14)<nowiki>}</nowiki>,
  
Model Checking of Software (SPIN'14)<nowiki>}</nowiki>,
−
year = <nowiki>{</nowiki>2014<nowiki>}</nowiki>,
 +
year = 2014,
  +
month = jan,
  +
pages = <nowiki>{</nowiki>68--76<nowiki>}</nowiki>,
 
publisher = <nowiki>{</nowiki>ACM<nowiki>}</nowiki>,
  
publisher = <nowiki>{</nowiki>ACM<nowiki>}</nowiki>,
 
abstract = <nowiki>{</nowiki> LTL to B\"uchi automata (BA) translators are
  
abstract = <nowiki>{</nowiki> LTL to B\"uchi automata (BA) translators are
Line 34: Line 36:
 
of these experiences, we gain a better insight into the
  
of these experiences, we gain a better insight into the
 
characteristics of automata that work well with Spin. <nowiki>}</nowiki>,
  
characteristics of automata that work well with Spin. <nowiki>}</nowiki>,
−
note = <nowiki>{</nowiki>To appear<nowiki>}</nowiki>
 +
doi = <nowiki>{</nowiki>10.1145/2632362.2632377<nowiki>}</nowiki>
 
<nowiki>}</nowiki>
  
<nowiki>}</nowiki>
   

Latest revision as of 10:21, 3 April 2023

Authors
František Blahoudek, Alexandre Duret-Lutz, Mojmír Křetínský, Jan Strejček
Where
Proceedings of the 21th International SPIN Symposium on Model Checking of Software (SPIN'14)
Type
inproceedings
Publisher
ACM
Projects
Spot
Date
2014-06-16

Abstract

LTL to Büchi automata (BA) translators are traditionally optimized to produce automata with a small number of states or a small number of non-deterministic states. In this paper, we search for properties of Büchi automata that really influence the performance of explicit model checkers. We do that by manual analysis of several automata and by experiments with common LTL-to-BA translators and realistic verification tasks. As a result of these experiences, we gain a better insight into the characteristics of automata that work well with Spin.

Documents

Bibtex (lrde.bib)

@InProceedings{	  blahoudek.14.spin,
  author	= {Franti\v{s}ek Blahoudek and Alexandre Duret-Lutz and
		  Mojm\'{i}r K\v{r}et\'{i}nsk\'{y} and Jan Strej\v{c}ek},
  title		= {Is There a Best {B\"u}chi Automaton for Explicit Model
		  Checking?},
  booktitle	= {Proceedings of the 21th International SPIN Symposium on
		  Model Checking of Software (SPIN'14)},
  year		= 2014,
  month		= jan,
  pages		= {68--76},
  publisher	= {ACM},
  abstract	= { LTL to B\"uchi automata (BA) translators are
		  traditionally optimized to produce automata with a small
		  number of states or a small number of non-deterministic
		  states. In this paper, we search for properties of B\"uchi
		  automata that really influence the performance of explicit
		  model checkers. We do that by manual analysis of several
		  automata and by experiments with common LTL-to-BA
		  translators and realistic verification tasks. As a result
		  of these experiences, we gain a better insight into the
		  characteristics of automata that work well with Spin. },
  doi		= {10.1145/2632362.2632377}
}





Retrieved from "https://www.lrde.epita.fr/index.php?title=Publications/blahoudek.14.spin&oldid=128462"