LTL Translation Improvements in Spot

Authors

Alexandre Duret-Lutz

Where

Proceedings of the 5th International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS'11)

Place

Tunis, Tunisia

Type

inproceedings

Publisher

British Computer Society

Projects

Spot

Date

2011-07-25

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

• Paper

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}
}