Difference between revisions of "Publications/duret.11.atva"

From LRDE

(Created page with "{{Publication | date = 2011-10-01 | authors = Alexandre Duret-Lutz, Kais Klai, Denis Poitrenaud, Yann Thierry-Mieg | title = Self-Loop Aggregation Product --- A New Hybrid App...")
 
 
(15 intermediate revisions by the same user not shown)
Line 1: Line 1:
 
{{Publication
  
{{Publication
−
| date = 2011-10-01
 +
| published = true
  +
| date = 2011-06-23
 
| authors = Alexandre Duret-Lutz, Kais Klai, Denis Poitrenaud, Yann Thierry-Mieg
  
| authors = Alexandre Duret-Lutz, Kais Klai, Denis Poitrenaud, Yann Thierry-Mieg
−
| title = Self-Loop Aggregation Product --- A New Hybrid Approach to On-the-Fly LTL Model Checking
 +
| title = Self-Loop Aggregation Product — A New Hybrid Approach to On-the-Fly LTL Model Checking
 
| booktitle = Proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis (ATVA'11)
  
| booktitle = Proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis (ATVA'11)
 
| series = Lecture Notes in Computer Science
  
| series = Lecture Notes in Computer Science
Line 9: Line 10:
 
| address = Taipei, Taiwan
  
| address = Taipei, Taiwan
 
| publisher = Springer
  
| publisher = Springer
−
| urllrde = 201110-ATVA
  
 
| abstract = We present the Self-Loop Aggregation Product (SLAP), a new hybrid technique that replaces the synchronized product used in the automata-theoretic approach for LTL model checking. The proposed product is an explicit graph of aggregates (symbolic sets of states) that can be interpreted as a Büchi automata. The criterion used by SLAP to aggregate states from the Kripke structure is based on the analysis of self-loops that occur in the Büchi automaton expressing the property to verify. Our hybrid approach allows on the one hand to use classical emptiness-check algorithms and build the graph on-the-flyand on the other hand, to have a compact encoding of the state space thanks to the symbolic representation of the aggregates. Our experiments show that this technique often outperforms other existing (hybrid or fully symbolic) approaches.
  
| abstract = We present the Self-Loop Aggregation Product (SLAP), a new hybrid technique that replaces the synchronized product used in the automata-theoretic approach for LTL model checking. The proposed product is an explicit graph of aggregates (symbolic sets of states) that can be interpreted as a Büchi automata. The criterion used by SLAP to aggregate states from the Kripke structure is based on the analysis of self-loops that occur in the Büchi automaton expressing the property to verify. Our hybrid approach allows on the one hand to use classical emptiness-check algorithms and build the graph on-the-flyand on the other hand, to have a compact encoding of the state space thanks to the symbolic representation of the aggregates. Our experiments show that this technique often outperforms other existing (hybrid or fully symbolic) approaches.
  +
| lrdeslides = http://www.lrde.epita.fr/dload/papers/duret.11.atva.slides.pdf
  +
| lrdepaper = http://www.lrde.epita.fr/dload/papers/duret.11.atva.pdf
  +
| lrdeprojects = Spot
  +
| lrdenewsdate = 2011-06-23
 
| type = inproceedings
  
| type = inproceedings
 
| id = duret.11.atva
  
| id = duret.11.atva
  +
| identifier = doi:10.1007/978-3-642-24372-1_24
 
| bibtex =
 
| bibtex =
 
@InProceedings<nowiki>{</nowiki> duret.11.atva,
  
@InProceedings<nowiki>{</nowiki> duret.11.atva,
Line 24: Line 29:
 
year = 2011,
  
year = 2011,
 
series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>,
  
series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>,
−
volume = <nowiki>{</nowiki>6996<nowiki>}</nowiki>,
 +
volume = 6996,
 
pages = <nowiki>{</nowiki>336--350<nowiki>}</nowiki>,
  
pages = <nowiki>{</nowiki>336--350<nowiki>}</nowiki>,
 
address = <nowiki>{</nowiki>Taipei, Taiwan<nowiki>}</nowiki>,
  
address = <nowiki>{</nowiki>Taipei, Taiwan<nowiki>}</nowiki>,
Line 44: Line 49:
 
aggregates. Our experiments show that this technique often
  
aggregates. Our experiments show that this technique often
 
outperforms other existing (hybrid or fully symbolic)
  
outperforms other existing (hybrid or fully symbolic)
−
approaches.<nowiki>}</nowiki>
 +
approaches.<nowiki>}</nowiki>,
  +
doi = <nowiki>{</nowiki>10.1007/978-3-642-24372-1_24<nowiki>}</nowiki>
 
<nowiki>}</nowiki>
  
<nowiki>}</nowiki>
   

Latest revision as of 11:30, 1 April 2019

Authors
Alexandre Duret-Lutz, Kais Klai, Denis Poitrenaud, Yann Thierry-Mieg
Where
Proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis (ATVA'11)
Place
Taipei, Taiwan
Type
inproceedings
Publisher
Springer
Projects
Spot
Date
2011-06-23

Abstract

We present the Self-Loop Aggregation Product (SLAP), a new hybrid technique that replaces the synchronized product used in the automata-theoretic approach for LTL model checking. The proposed product is an explicit graph of aggregates (symbolic sets of states) that can be interpreted as a Büchi automata. The criterion used by SLAP to aggregate states from the Kripke structure is based on the analysis of self-loops that occur in the Büchi automaton expressing the property to verify. Our hybrid approach allows on the one hand to use classical emptiness-check algorithms and build the graph on-the-flyand on the other hand, to have a compact encoding of the state space thanks to the symbolic representation of the aggregates. Our experiments show that this technique often outperforms other existing (hybrid or fully symbolic) approaches.

Documents

Bibtex (lrde.bib)

@InProceedings{	  duret.11.atva,
  author	= {Alexandre Duret-Lutz and Kais Klai and Denis Poitrenaud
		  and Yann Thierry-Mieg},
  title		= {Self-Loop Aggregation Product --- A New Hybrid Approach to
		  On-the-Fly {LTL} Model Checking},
  booktitle	= {Proceedings of the 9th International Symposium on
		  Automated Technology for Verification and Analysis
		  (ATVA'11)},
  year		= 2011,
  series	= {Lecture Notes in Computer Science},
  volume	= 6996,
  pages		= {336--350},
  address	= {Taipei, Taiwan},
  month		= oct,
  publisher	= {Springer},
  abstract	= {We present the \emph{Self-Loop Aggregation Product}
		  (SLAP), a new hybrid technique that replaces the
		  synchronized product used in the automata-theoretic
		  approach for LTL model checking. The proposed product is an
		  explicit graph of aggregates (symbolic sets of states) that
		  can be interpreted as a B\"uchi automata. The criterion
		  used by SLAP to aggregate states from the Kripke structure
		  is based on the analysis of self-loops that occur in the
		  B\"uchi automaton expressing the property to verify. Our
		  hybrid approach allows on the one hand to use classical
		  emptiness-check algorithms and build the graph on-the-fly,
		  and on the other hand, to have a compact encoding of the
		  state space thanks to the symbolic representation of the
		  aggregates. Our experiments show that this technique often
		  outperforms other existing (hybrid or fully symbolic)
		  approaches.},
  doi		= {10.1007/978-3-642-24372-1_24}
}





Retrieved from "https://www.lrde.epita.fr/index.php?title=Publications/duret.11.atva&oldid=123234"