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

From LRDE
Line 1: Line 1:
 
{{Publication
  
{{Publication
 
| published = true
  
| published = true
−
| date = 2014-01-01
 +
| date = 2014-04-01
 
| authors = Ala Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon, Yann Thierry-Mieg
  
| authors = Ala Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon, Yann Thierry-Mieg
 
| title = Symbolic Model Checking of Stutter Invariant Properties Using Generalized Testing Automata
  
| title = Symbolic Model Checking of Stutter Invariant Properties Using Generalized Testing Automata
−
| booktitle = 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
 +
| booktitle = Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14)
 
| publisher = Springer
  
| publisher = Springer
 
| series = Lecture Notes in Computer Science
  
| series = Lecture Notes in Computer Science
−
| optvolume = ?
 +
| volume = 8413
−
| pages = to be published
 +
| pages = 440 to 454
 
| address = Grenoble, France
  
| address = Grenoble, France
 
| note = Accepted
  
| note = Accepted
 
| urllrde = 2014-TACAS
  
| urllrde = 2014-TACAS
−
| abstract = In a previous work, we showed that a kind of ω-automata known as Tran­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.
 +
| 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
Line 21: Line 21:
 
author = <nowiki>{</nowiki>Ala Eddine Ben<nowiki>{</nowiki> S<nowiki>}</nowiki>alem and Alexandre Duret-Lutz and
  
author = <nowiki>{</nowiki>Ala Eddine Ben<nowiki>{</nowiki> S<nowiki>}</nowiki>alem and Alexandre Duret-Lutz and
 
Fabrice Kordon and Yann Thierry-Mieg<nowiki>}</nowiki>,
  
Fabrice Kordon and Yann Thierry-Mieg<nowiki>}</nowiki>,
−
title = <nowiki>{</nowiki><nowiki>{</nowiki>Symbolic Model Checking of Stutter Invariant Properties
 +
title = <nowiki>{</nowiki>Symbolic Model Checking of Stutter Invariant Properties
−
Using Generalized Testing Automata<nowiki>}</nowiki><nowiki>}</nowiki>,
 +
Using Generalized Testing Automata<nowiki>}</nowiki>,
−
booktitle = <nowiki>{</nowiki><nowiki>{</nowiki>20th International Conference on Tools and Algorithms for
 +
booktitle = <nowiki>{</nowiki>Proceedings of the 20th International Conference on Tools
−
the Construction and Analysis of Systems (TACAS)<nowiki>}</nowiki><nowiki>}</nowiki>,
 +
and Algorithms for the Construction and Analysis of Systems
  +
(TACAS'14)<nowiki>}</nowiki>,
 
year = 2014,
  
year = 2014,
 
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>,
  
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>,
 
series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>,
  
series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>,
−
optvolume = <nowiki>{</nowiki>?<nowiki>}</nowiki>,
 +
volume = <nowiki>{</nowiki>8413<nowiki>}</nowiki>,
−
pages = <nowiki>{</nowiki>to be published<nowiki>}</nowiki>,
 +
pages = <nowiki>{</nowiki>440--454<nowiki>}</nowiki>,
 
address = <nowiki>{</nowiki>Grenoble, France<nowiki>}</nowiki>,
  
address = <nowiki>{</nowiki>Grenoble, France<nowiki>}</nowiki>,
−
month = <nowiki>{</nowiki>April<nowiki>}</nowiki>,
 +
month = apr,
 
note = <nowiki>{</nowiki>Accepted<nowiki>}</nowiki>,
  
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\"uchi automata traditionally used for \textit<nowiki>{</nowiki>explicit<nowiki>}</nowiki>
 +
Büchi 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 47: 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, 17 June 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 ̈uchi 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üchi 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=8275"