Difference between revisions of "Publications/baier.19.atva"

From LRDE

 
Line 5: Line 5:
 
| title = Generic Emptiness Check for Fun and Profit
 
| title = Generic Emptiness Check for Fun and Profit
 
| booktitle = Proceedings of the 17th International Symposium on Automated Technology for Verification and Analysis (ATVA'19)
 
| booktitle = Proceedings of the 17th International Symposium on Automated Technology for Verification and Analysis (ATVA'19)
| volume = ?????
+
| volume = 11781
 
| series = Lecture Notes in Computer Science
 
| series = Lecture Notes in Computer Science
| pages = ??? to ???
+
| pages = 445 to 461
 
| publisher = Springer
 
| publisher = Springer
| note = To appear
 
 
| abstract = We present a new algorithm for checking the emptiness of <math>\omega</math>-automata with an Emerson-Lei acceptance condition (i.e., a positive Boolean formula over sets of states or transitions that must be visited infinitely or finitely often). The algorithm can also solve the model checking problem of probabilistic positiveness of MDP under a property given as a deterministic Emerson-Lei automaton. Although both these problems are known to be NP-complete and our algorithm is exponential in general, it runs in polynomial time for simpler acceptance conditions like generalized Rabin, Streett, or parity. In fact, the algorithm provides a unifying view on emptiness checks for these simpler automata classes. We have implemented the algorithm in Spot and PRISM and our experiments show improved performance over previous solutions.
 
| abstract = We present a new algorithm for checking the emptiness of <math>\omega</math>-automata with an Emerson-Lei acceptance condition (i.e., a positive Boolean formula over sets of states or transitions that must be visited infinitely or finitely often). The algorithm can also solve the model checking problem of probabilistic positiveness of MDP under a property given as a deterministic Emerson-Lei automaton. Although both these problems are known to be NP-complete and our algorithm is exponential in general, it runs in polynomial time for simpler acceptance conditions like generalized Rabin, Streett, or parity. In fact, the algorithm provides a unifying view on emptiness checks for these simpler automata classes. We have implemented the algorithm in Spot and PRISM and our experiments show improved performance over previous solutions.
 
| lrdekeywords = Spot
 
| lrdekeywords = Spot
Line 17: Line 16:
 
| type = inproceedings
 
| type = inproceedings
 
| id = baier.19.atva
 
| id = baier.19.atva
  +
| identifier = doi:10.1007/978-3-030-31784-3_26
 
| bibtex =
 
| bibtex =
 
@InProceedings<nowiki>{</nowiki> baier.19.atva,
 
@InProceedings<nowiki>{</nowiki> baier.19.atva,
Line 27: Line 27:
 
(ATVA'19)<nowiki>}</nowiki>,
 
(ATVA'19)<nowiki>}</nowiki>,
 
year = <nowiki>{</nowiki>2019<nowiki>}</nowiki>,
 
year = <nowiki>{</nowiki>2019<nowiki>}</nowiki>,
volume = <nowiki>{</nowiki>?????<nowiki>}</nowiki>,
+
volume = <nowiki>{</nowiki>11781<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>445--461<nowiki>}</nowiki>,
 
month = oct,
 
month = oct,
 
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>,
 
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>,
note = <nowiki>{</nowiki>To appear<nowiki>}</nowiki>,
 
 
abstract = <nowiki>{</nowiki>We present a new algorithm for checking the emptiness of
 
abstract = <nowiki>{</nowiki>We present a new algorithm for checking the emptiness of
 
$\omega$-automata with an Emerson-Lei acceptance condition
 
$\omega$-automata with an Emerson-Lei acceptance condition
Line 47: Line 46:
 
these simpler automata classes. We have implemented the
 
these simpler automata classes. We have implemented the
 
algorithm in Spot and PRISM and our experiments show
 
algorithm in Spot and PRISM and our experiments show
improved performance over previous solutions.<nowiki>}</nowiki>
+
improved performance over previous solutions.<nowiki>}</nowiki>,
  +
doi = <nowiki>{</nowiki>10.1007/978-3-030-31784-3_26<nowiki>}</nowiki>
 
<nowiki>}</nowiki>
 
<nowiki>}</nowiki>
   

Latest revision as of 13:05, 8 November 2019

Abstract

We present a new algorithm for checking the emptiness of -automata with an Emerson-Lei acceptance condition (i.e., a positive Boolean formula over sets of states or transitions that must be visited infinitely or finitely often). The algorithm can also solve the model checking problem of probabilistic positiveness of MDP under a property given as a deterministic Emerson-Lei automaton. Although both these problems are known to be NP-complete and our algorithm is exponential in general, it runs in polynomial time for simpler acceptance conditions like generalized Rabin, Streett, or parity. In fact, the algorithm provides a unifying view on emptiness checks for these simpler automata classes. We have implemented the algorithm in Spot and PRISM and our experiments show improved performance over previous solutions.

Documents

Bibtex (lrde.bib)

@InProceedings{	  baier.19.atva,
  author	= {Christel Baier and Franti\v{s}ek Blahoudek and Alexandre
		  Duret-Lutz and Joachim Klein and David M\"uller and Jan
		  Strej\v{c}ek},
  title		= {Generic Emptiness Check for Fun and Profit},
  booktitle	= {Proceedings of the 17th International Symposium on
		  Automated Technology for Verification and Analysis
		  (ATVA'19)},
  year		= {2019},
  volume	= {11781},
  series	= {Lecture Notes in Computer Science},
  pages		= {445--461},
  month		= oct,
  publisher	= {Springer},
  abstract	= {We present a new algorithm for checking the emptiness of
		  $\omega$-automata with an Emerson-Lei acceptance condition
		  (i.e., a positive Boolean formula over sets of states or
		  transitions that must be visited infinitely or finitely
		  often). The algorithm can also solve the model checking
		  problem of probabilistic positiveness of MDP under a
		  property given as a deterministic Emerson-Lei automaton.
		  Although both these problems are known to be NP-complete
		  and our algorithm is exponential in general, it runs in
		  polynomial time for simpler acceptance conditions like
		  generalized Rabin, Streett, or parity. In fact, the
		  algorithm provides a unifying view on emptiness checks for
		  these simpler automata classes. We have implemented the
		  algorithm in Spot and PRISM and our experiments show
		  improved performance over previous solutions.},
  doi		= {10.1007/978-3-030-31784-3_26}
}