SPOT: an extensible model checking library using transition-based generalized Büchi automata

Author

Duret-Lutz, Alexandre ; Poitrenaud, Denis

Author_Institution

Lab. d´´Informatique de Paris 6, Univ. Pierre et Marie Curie, Paris, France

fYear

2004

Firstpage

76

Lastpage

83

Abstract

SPOT (SPOT produces our traces), is a C++ library offering model checking bricks that can be combined and interfaced with third party tools to build a model checker. It relies on transition-based generalized Büchi automata (TGBA) and does not need to degeneralize these automata to check their emptiness. We motivate the choice of TGBA by illustrating a very simple (yet efficient) translation of LTL (linear temporal logic) into TGBA. We then show how it supports on-the-fly computations, and how it can be extended or integrated in other tools.

Keywords

C language; automata theory; object-oriented methods; software libraries; temporal logic; C++ library; extensible model checking library; linear temporal logic; model checker; object-oriented library; transition-based generalized Buchi automata; Automata; Computational modeling; Computer interfaces; Impedance; Libraries; Logic; Object oriented modeling; Pipelines; State-space methods; Telecommunication computing;

fLanguage

English

Publisher

ieee

Conference_Titel

Modeling, Analysis, and Simulation of Computer and Telecommunications Systems, 2004. (MASCOTS 2004). Proceedings. The IEEE Computer Society's 12th Annual International Symposium on

ISSN

1526-7539

Print_ISBN

0-7695-2251-3

Type

conf

DOI

10.1109/MASCOT.2004.1348184

Filename

1348184