LTL Translation Improvements in Spot

From LRDE

Revision as of 11:14, 26 April 2016 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

Spot is a library of model-checking algorithms. This paper focuses on the module translating LTL formulæ into automata. We discuss improvements that have been implemented in the last four years, we show how Spot's translation competes on various benchmarks, and we give some insight into its implementation.

Documents

Bibtex (lrde.bib)

@InProceedings{	  duret.11.vecos,
  author	= {Alexandre Duret-Lutz},
  title		= {{LTL} Translation Improvements in {Spot}},
  booktitle	= {Proceedings of the 5th International Workshop on
		  Verification and Evaluation of Computer and Communication
		  Systems (VECoS'11)},
  year		= 2011,
  series	= {Electronic Workshops in Computing},
  address	= {Tunis, Tunisia},
  month		= sep,
  publisher	= {British Computer Society},
  abstract	= {Spot is a library of model-checking algorithms. This paper
		  focuses on the module translating LTL formul{\ae} into
		  automata. We discuss improvements that have been
		  implemented in the last four years, we show how Spot's
		  translation competes on various benchmarks, and we give
		  some insight into its implementation.},
  url		= {http://ewic.bcs.org/category/15853}
}