Improving degeneralization in Spot
From LRDE
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.
- Authors
- Pierre Parutto
- Type
- techreport
- Year
- 2011
- Number
- 1111
- Projects
- Spot
- Keywords
- model checking, automaton, degeneralization, Spot, tgbatba, counter automaton
Abstract
Spot is a model checking library developed at the LRDE. Its strengh is to be based on Transition Based generalized Büchi Automaton (TGBA), instead of Transition Based Büchi Automaton (TBA) widely used in other model checkers. TGBAs allows us to create a very small automaton representing a given formula hence making the whole model checking process faster. Spot emphasizes on the usability and customization of its tools, a great concern is to be able to interface Spot with other programs. Degeneralization the process of transforming a TGBA into a TBA, is central in this view. We present in this report an analysis of the tools already present in Spot for degeneralization and we proposes some way to improve them.