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

From LRDE
Line 12: Line 12:
 
| note = Accepted
  
| note = Accepted
 
| urllrde = 2014-TACAS
  
| 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.
 +
| 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.
 
| 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
Line 37: Line 37:
 
$\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 48:
 
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>
   

Revision as of 09:00, 10 September 2014

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},
  series	= {Lecture Notes in Computer Science},
  volume	= 8413,
  pages		= {440--454},
  address	= {Grenoble, France},
  month		= apr,
  note		= {Accepted},
  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=8604"