spotlogo64
(Spot Produces Our Traces)

1. Introduction

Spot is an object-oriented model checking library written in C++. It offers a set of bricks to experiment with and develop your own model checker. It is co-developed by people at LRDE and at LIP6.

Presently Spot is centered around the AutomataTheoreticApproachToModelChecking for LtlFormulae. In this approach, the verification is split as follows:

  1. computation of the state space,
  2. translation of the negated formula into an omega-automaton,
  3. synchronized product of these two objects,

  4. EmptinessCheck of the resulting product.

Spot offers different algorithms to perform the last three steps (and more); but they may as well be combined differently. The first step is expected to be carried out by third party tools. This way we do not impose any high-level formalism. So, for instance, if you have devised your own modeling formalism and have a program which is able to compute the state space of a model, then you can link your program with Spot (InterfacingSpot) in order to check LtlFormulae on your model. Our interface supports on-the-fly computations.

The library uses a special kind of automata called Transition-based Generalized Büchi Automata (TGBA). These are OmegaAutomata with labels on transitions, and multiple acceptance sets of transitions. Compared to more traditional Büchi Automata with acceptance sets of states, TGBA allow LtlFormulae to be represented more concisely.

Interesting starting points:

2. Spot Wiki

This is a Wiki for Spot. It uses the MoinMoin engine. If you are unfamiliar with Wikis, please read the HelpForBeginners.

Please create yourself an account and use it to edit these pages. Click on UserPreferences to do that; there is always a link for this on the top when you are not logged. Anonymous edits are only allowed from the intranet. If you need to delete or rename pages, ask someone in the AdminGroup.

Note from 2007-10-13: because I just got fed up with the spam I had to remove every day, I have disabled write access to all but of few selected IP domains (notably LIP6 and LRDE). I you want a new IP address added to the list, drop me a mail.

3. News

2010-02-01

Spot 0.5 is out. GetSpot. This release contains more than two years worth of work. It includes new LTL translations algoithms, complementations algorithms, and several bug fixes.

2007-07-17

Spot 0.4 is out. GetSpot. These are mainly bug fixes, more LTL simplifications, and the emptiness check for our ACSD'07 paper.

2006-01-25

Spot 0.3 is out. GetSpot. These are mainly bug fixes, and Spot's on-line LTL-to-TGBA translator now offer options to compute accepting runs.

2005-04-08

Spot 0.2 is out. GetSpot. The main change is a new interface to pass EmptinessCheckOptions to the algorithms from the command line. (This is especially helpful with the emptiness-check benchmarks in directory bench/emptchk/.)

2005-01-31

Spot 0.1 is out. GetSpot, it includes implementations for several EmptinessCheckAlgorithms. CheckPn (0.0b) has been updated too.

4. How-Tos and other documents

SpotWiki (last edited 2010-02-01 10:13:44 by AlexandreDuretLutz)

All text is available under the terms of the GNU Free Documentation License, see SpotWikiLicense for details.