On Refinement of Büchi Automata for Explicit Model Checking

From LRDE

Revision as of 17:55, 4 January 2018 by Bot (talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

Abstract

In explicit model checking, systems are typically described in an implicit and compact way. Some valid information about the system can be easily derived directly from this description, for example that some atomic propositions cannot be valid at the same time. The paper shows several ways to apply this information to improve the Büchi automaton built from an LTL specification. As a result, we get smaller automata with shorter edge labels that are easier to understand and, more importantly, for which the explicit model checking process performs better.

Documents

Bibtex (lrde.bib)

@InProceedings{	  blahoudek.15.spin,
  author	= {Franti\v{s}ek Blahoudek and Alexandre Duret-Lutz and
		  Vojt\v{c}ech Rujbr and Jan Strej\v{c}ek},
  title		= {On Refinement of {B\"u}chi Automata for Explicit Model
		  Checking},
  booktitle	= {Proceedings of the 22th International SPIN Symposium on
		  Model Checking of Software (SPIN'15)},
  year		= 2015,
  month		= aug,
  pages		= {66--83},
  publisher	= {Springer},
  volume	= 9232,
  series	= {Lecture Notes in Computer Science},
  abstract	= {In explicit model checking, systems are typically
		  described in an implicit and compact way. Some valid
		  information about the system can be easily derived directly
		  from this description, for example that some atomic
		  propositions cannot be valid at the same time. The paper
		  shows several ways to apply this information to improve the
		  B{\"u}chi automaton built from an LTL specification. As a
		  result, we get smaller automata with shorter edge labels
		  that are easier to understand and, more importantly, for
		  which the explicit model checking process performs better.},
  doi		= {10.1007/978-3-319-23404-5_6}
}