Practical Stutter-Invariance Checks for ω-Regular Languages

Authors

Thibaud Michaud, Alexandre Duret-Lutz

Where

Proceedings of the 22th International SPIN Symposium on Model Checking of Software (SPIN'15)

Type

inproceedings

Publisher

Springer

Projects

Spot

Date

2015-06-15

Abstract

We propose several automata-based constructions that check whether a specification is stutter-invariant. These constructions assume that a specification and its negation can be translated into Büchi automata, but aside from that, they are independent of the specification formalism. These transformations were inspired by a construction due to Holzmann and Kupferman, but that we broke down into two operations that can have different realizations, and that can be combined in different ways. As it turns outimplementing only one of these operations is needed to obtain a functional stutter-invariant check. Finally we have implemented these techniques in a tool so that users can easily check whether an LTL or PSL formula is stutter-invariant.

Documents

• Paper

Bibtex (lrde.bib)

@InProceedings{	  michaud.15.spin,
  author	= {Thibaud Michaud and Alexandre Duret-Lutz},
  title		= {Practical Stutter-Invariance Checks for {$\omega$}-Regular
		  Languages},
  booktitle	= {Proceedings of the 22th International SPIN Symposium on
		  Model Checking of Software (SPIN'15)},
  year		= 2015,
  month		= aug,
  pages		= {84--101},
  volume	= 9232,
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer},
  abstract	= {We propose several automata-based constructions that check
		  whether a specification is stutter-invariant. These
		  constructions assume that a specification and its negation
		  can be translated into B{\"u}chi automata, but aside from
		  that, they are independent of the specification formalism.
		  These transformations were inspired by a construction due
		  to Holzmann and Kupferman, but that we broke down into two
		  operations that can have different realizations, and that
		  can be combined in different ways. As it turns out,
		  implementing only one of these operations is needed to
		  obtain a functional stutter-invariant check. Finally we
		  have implemented these techniques in a tool so that users
		  can easily check whether an LTL or PSL formula is
		  stutter-invariant.},
  doi		= {10.1007/978-3-319-23404-5_7}
}