Difference between revisions of "Publications/bensalem.14.tacas"

From LRDE
 
(13 intermediate revisions by the same user not shown)
Line 10: Line 10:
 
| pages = 440 to 454
  
| pages = 440 to 454
 
| address = Grenoble, France
  
| address = Grenoble, France
  ⚫
| abstract = In a previous work, we showed that a kind of <math>\omega</math>-automata known as emphTran­sition-based Generalized Testing Automata (TGTA) can outperform the Büchi automata traditionally used for explicit model checking when verifying stutter-invariant properties. In this work, we investigate the use of these generalized testing automata to improve symbolic model checking of stutter-invariant LTL properties. We propose an efficient symbolic encoding of stuttering transitions in the product between a model and a TGTA. Saturation techniques available for decision diagrams then benefit from the presence of stuttering self-loops on all states of TGTA. Experimentation of this approach confirms that it outperforms the symbolic approach based on (transition-based) Generalized Büchi Automata.
−
| note = Accepted
  
−
| urllrde = 2014-TACAS
  
⚫
| abstract = In a previous work, we showed that a kind of ω-automata known as emphTran­sition-based Generalized Testing Automata (TGTA) can outperform the Büchi automata traditionally used for explicit model checking when verifying stutter-invariant properties. In this work, we investigate the use of these generalized testing automata to improve symbolic model checking of stutter-invariant LTL properties. We propose an efficient symbolic encoding of stuttering transitions in the product between a model and a TGTA. Saturation techniques available for decision diagrams then benefit from the presence of stuttering self-loops on all states of TGTA. Experimentation of this approach confirms that it outperforms the symbolic approach based on (transition-based) Generalized B ̈uchi Automata.
  
 
| lrdepaper = http://www.lrde.epita.fr/dload/papers/bensalem.14.tacas.pdf
  
| lrdepaper = http://www.lrde.epita.fr/dload/papers/bensalem.14.tacas.pdf
 
| lrdeprojects = Spot
  
| lrdeprojects = Spot
 
| type = inproceedings
  
| type = inproceedings
 
| id = bensalem.14.tacas
  
| id = bensalem.14.tacas
  +
| identifier = doi:10.1007/978-3-642-54862-8_38
 
| bibtex =
 
| bibtex =
 
@InProceedings<nowiki>{</nowiki> bensalem.14.tacas,
  
@InProceedings<nowiki>{</nowiki> bensalem.14.tacas,
Line 28: Line 27:
 
year = 2014,
  
year = 2014,
 
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>,
  
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>,
  ⚫
doi = <nowiki>{</nowiki>10.1007/978-3-642-54862-8_38<nowiki>}</nowiki>,
 
series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>,
  
series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>,
−
volume = <nowiki>{</nowiki>8413<nowiki>}</nowiki>,
 +
volume = 8413,
 
pages = <nowiki>{</nowiki>440--454<nowiki>}</nowiki>,
  
pages = <nowiki>{</nowiki>440--454<nowiki>}</nowiki>,
 
address = <nowiki>{</nowiki>Grenoble, France<nowiki>}</nowiki>,
  
address = <nowiki>{</nowiki>Grenoble, France<nowiki>}</nowiki>,
 
month = apr,
  
month = apr,
⚫
note = <nowiki>{</nowiki>Accepted<nowiki>}</nowiki>,
  
 
abstract = <nowiki>{</nowiki>In a previous work, we showed that a kind of
  
abstract = <nowiki>{</nowiki>In a previous work, we showed that a kind of
 
$\omega$-automata known as \emph<nowiki>{</nowiki>Tran\-sition-based
  
$\omega$-automata known as \emph<nowiki>{</nowiki>Tran\-sition-based
 
Generalized Testing Automata<nowiki>}</nowiki> (TGTA) can outperform the
  
Generalized Testing Automata<nowiki>}</nowiki> (TGTA) can outperform the
−
Büchi automata traditionally used for \textit<nowiki>{</nowiki>explicit<nowiki>}</nowiki>
 +
B\"uchi automata traditionally used for \textit<nowiki>{</nowiki>explicit<nowiki>}</nowiki>
 
model checking when verifying stutter-invariant properties.
  
model checking when verifying stutter-invariant properties.
 
In this work, we investigate the use of these generalized
  
In this work, we investigate the use of these generalized
Line 48: Line 47:
 
TGTA. Experimentation of this approach confirms that it
  
TGTA. Experimentation of this approach confirms that it
 
outperforms the symbolic approach based on
  
outperforms the symbolic approach based on
−
(transition-based) Generalized B\ ̈uchi Automata.<nowiki>}</nowiki>
 +
(transition-based) Generalized B\"uchi Automata.<nowiki>}</nowiki>
 
<nowiki>}</nowiki>
  
<nowiki>}</nowiki>
   

Latest revision as of 11:29, 1 April 2019

Authors
Ala Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon, Yann Thierry-Mieg
Where
Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14)
Place
Grenoble, France
Type
inproceedings
Publisher
Springer
Projects
Spot
Date
2014-04-01

Abstract

In a previous work, we showed that a kind of -automata known as emphTran­sition-based Generalized Testing Automata (TGTA) can outperform the Büchi automata traditionally used for explicit model checking when verifying stutter-invariant properties. In this work, we investigate the use of these generalized testing automata to improve symbolic model checking of stutter-invariant LTL properties. We propose an efficient symbolic encoding of stuttering transitions in the product between a model and a TGTA. Saturation techniques available for decision diagrams then benefit from the presence of stuttering self-loops on all states of TGTA. Experimentation of this approach confirms that it outperforms the symbolic approach based on (transition-based) Generalized Büchi Automata.

Documents

Bibtex (lrde.bib)

@InProceedings{	  bensalem.14.tacas,
  author	= {Ala Eddine Ben{ S}alem and Alexandre Duret-Lutz and
		  Fabrice Kordon and Yann Thierry-Mieg},
  title		= {Symbolic Model Checking of Stutter Invariant Properties
		  Using Generalized Testing Automata},
  booktitle	= {Proceedings of the 20th International Conference on Tools
		  and Algorithms for the Construction and Analysis of Systems
		  (TACAS'14)},
  year		= 2014,
  publisher	= {Springer},
  doi		= {10.1007/978-3-642-54862-8_38},
  series	= {Lecture Notes in Computer Science},
  volume	= 8413,
  pages		= {440--454},
  address	= {Grenoble, France},
  month		= apr,
  abstract	= {In a previous work, we showed that a kind of
		  $\omega$-automata known as \emph{Tran\-sition-based
		  Generalized Testing Automata} (TGTA) can outperform the
		  B\"uchi automata traditionally used for \textit{explicit}
		  model checking when verifying stutter-invariant properties.
		  In this work, we investigate the use of these generalized
		  testing automata to improve \textit{symbolic} model
		  checking of stutter-invariant LTL properties. We propose an
		  efficient symbolic encoding of stuttering transitions in
		  the product between a model and a TGTA. Saturation
		  techniques available for decision diagrams then benefit
		  from the presence of stuttering self-loops on all states of
		  TGTA. Experimentation of this approach confirms that it
		  outperforms the symbolic approach based on
		  (transition-based) Generalized B\"uchi Automata.}
}





Retrieved from "https://www.lrde.epita.fr/index.php?title=Publications/bensalem.14.tacas&oldid=123226"