Spot 2.0 --- a framework for LTL and ω-automata manipulation

From LRDE

Revision as of 23:01, 17 June 2016 by Bot (talk | contribs) (Created page with "{{Publication | published = true | date = 2016-10-01 | authors = Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Renault, Laurent Xu | ti...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

Abstract

We present Spot 2.0, a C++ library with Python bindings and an assortment of command-line tools designed to manipulate LTL and ω-automata in batch. New automata-manipulation tools were introduced in Spot 2.0; they support arbitrary acceptance conditions, as expressible in the Hanoi Omega Automaton format. Besides being useful to researchers who have automata to process, its Python bindings can also be used in interactive environments to teach ω-automata and model checking.

Documents

Bibtex (lrde.bib)

@InProceedings{	  duret.16.atva2,
  author	= {Alexandre Duret-Lutz and Alexandre Lewkowicz and Amaury
		  Fauchille and Thibaud Michaud and Etienne Renault and
		  Laurent Xu},
  title		= {Spot 2.0 --- a framework for {LTL} and $\omega$-automata
		  manipulation},
  booktitle	= {Proceedings of the 14th International Symposium on
		  Automated Technology for Verification and Analysis
		  (ATVA'16)},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer},
  volume	= {????},
  pages		= {??--??},
  year		= {2016},
  month		= oct,
  pdf		= {adl/duret.16.atva2.pdf},
  abstract	= {We present Spot 2.0, a C++ library with Python bindings
		  and an assortment of command-line tools designed to
		  manipulate LTL and $\omega$-automata in batch. New
		  automata-manipulation tools were introduced in Spot 2.0;
		  they support arbitrary acceptance conditions, as
		  expressible in the Hanoi Omega Automaton format. Besides
		  being useful to researchers who have automata to process,
		  its Python bindings can also be used in interactive
		  environments to teach $\omega$-automata and model checking.},
  note		= {To appear.}
}