We list below some key papers related to the development of Spot.
(When adding new entries to this page, please complete the HlinsDatabase with the author homepages and other things that must be turned into hyperlinks.)

1. About Spot

[duret.04.mascots]: Alexandre Duret-Lutz and Denis Poitrenaud. Spot: an extensible model checking library using transition-based generalized Büchi automata. In Proceedings of the 12th IEEE/ACM International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS'04), pages 76-83, Volendam, The Netherlands, October 2004. IEEE Computer Society Press. [ .pdf ]

2. About Algorithms

This list could use an update. In the meantime you may want to check LtlTranslationAlgorithms and EmptinessCheckAlgorithms if you are looking for bibliographical references.

[baarir.07.acsd]: Souheib Baarir and Alexandre Duret-Lutz. Emptiness check of powerset Büchi automata. In Proceedings of the 7th International Conference on Application of Concurrency to System Design (ACSD'07), pages 41-50. IEEE Computer Society, July 2007. [ .pdf ]
A special emptiness check for powerset Büchi automata, implemented in Spot.
[couvreur.05.spin]: Jean-Michel Couvreur, Alexandre Duret-Lutz, and Denis Poitrenaud. On-the-fly emptiness checks for generalized Büchi automata. In Patrice Godefroid, editor, Proceedings of the 12th International SPIN Workshop on Model Checking of Software, volume 3639 of Lecture Notes in Computer Science, pages 143-158. ©Springer-Verlag, August 2005. [ .pdf ]
Comparison of various emptiness check algorithms, all implemented in Spot.
[couvreur.00.lacim]: Jean-Michel Couvreur. Un point de vue symbolique sur la logique temporelle linéaire. In Pierre Leroux, editor, Actes du Colloque LaCIM 2000, volume 27 of Publications du LaCIM, pages 131-140. Université du Québec à Montréal, August 2000. [ .pdf ]
This paper describes a LTL-to-Büchi translation algorithm available in Spot as ltl_to_tgba_lacim(). The automata produced are not really small. However they are really fast to build, and can be represented compactly using BDDs.
[couvreur.99.fm]: Jean-Michel Couvreur. On-the-fly verification of temporal logic. In Jeannette M. Wing, Jim Woodcock, and Jim Davies, editors, Proceedings of the World Congress on Formal Methods in the Development of Computing Systems (FM'99), volume 1708 of Lecture Notes in Computer Science, pages 253-271, Toulouse, France, September 1999. ©Springer-Verlag. [ .pdf ]
Work started on Spot to implement the algorithms introduced in this paper. The LTL-to-Büchi translation algorithm is available in Spot as ltl_to_tgba_fm(). The emptiness-check with generalized acceptance conditions is implemented by the emptiness_check class.
[minato.92.sasimi]: Shin-ichi Minato. Fast generation of irredundant sum-of-products forms from binary decision diagrams. In Proceedings of the third Synthesis and Simulation Meeting and International Interchange workshop (SASIMI'92), pages 64-73, Kobe, Japan, April 1992. [ .pdf ]
The LTL translator algorithm from [couvreur.99.fm] requires some prime impliquant computation. We use the Minato-Morreale algorithm.
[godefroid.93.pstv]: Patrice Godefroid and Gerard J. Holzmann. On the verification of temporal properties. In André A. S. Danthine, Guy Leduc, and Pierre Wolper, editors, Proceedings of the 13th IFIP TC6/WG6.1 International Symposium on Protocol Specification, Testing, and Verification (PSTV'93), volume C-16 of IFIP Transactions, pages 109-124, Liege, Belgium, May 1993. North-Holland. [ .pdf ]
The magic search is available in Spot as a magic_search class.
[giannakopoulou.02.forte]: Dimitra Giannakopoulou and Flavio Lerda. From states to transitions: Improving translation of LTL formulae to Büchi automata. In Doron A. Peled and Moshe Y. Vardi, editors, Proceedings of the 22nd IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'02), volume 2529 of Lecture Notes in Computer Science, pages 308-326, Houston, Texas, November 2002. ©Springer-Verlag. [ .pdf ]
This papers introduces Transitions-based Generalized Büchi automata (TGBA) and explains how they are smaller than the usual state-based Büchi automata. TGBAs were already used earlier in [couvreur.99.fm] and [couvreur.00.lacim] but this paper coined the acronym "TGBA" which we are using in Spot. Spot's tgba is an abstract class with many possible implementations. Its interface really is the heart of the library.
[sebastiani.03.charme]: Roberto Sebastiani and Stefano Tonetta. "more deterministic" vs. "smaller" büchi automata for efficient ltl model checking. In G. Goos, J. Hartmanis, and J. van Leeuwen, editors, Proceedings for the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME'03), volume 2860 of Lecture Notes in Computer Science, pages 126-140. ©Springer-Verlag, October 2003. [ .ps ]
This paper introduces two optimizations which we have implemented into Couvreur's [couvreur.99.fm] algorithm to obtain more deterministic automata. These are the "semantic branching" (which is called "exprop" inside Spot and "optimize determinism" on the on-line LTL-to-TGBA translator) and the "branching postponement".