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 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 ̈uchi Automata.
 +
| 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.
 
| 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 36: Line 36:
 
$\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 47: 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>
   

Revision as of 18:36, 26 May 2014

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

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.

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	= {{20th International Conference on Tools and Algorithms for
		  the Construction and Analysis of Systems (TACAS)}},
  year		= 2014,
  publisher	= {Springer},
  series	= {Lecture Notes in Computer Science},
  optvolume	= {?},
  pages		= {to be published},
  address	= {Grenoble, France},
  month		= {April},
  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=8117"