Improving degeneralization in Spot

From LRDE

Revision as of 17:06, 9 January 2018 by Bot (talk | contribs) (Created page with "{{CSIReport | authors = Pierre Parutto | title = Improving degeneralization in Spot | year = 2011 | abstract = Spot is a model checking library developed at the LRDE. Its stre...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

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.