Partial order reduction methods for 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
- 2012
- Number
- 1205
Abstract
Spot is a model checking library implementing an automaton based approach. For the moment to verify a property Spot's algorithm may explore the whole state space of the system without any reduction. They thus suffer from the combinatorial explosion in the model's size. One way to tackle this problem is by using Partial order reduction methods. The idea is to ignore equivalent behaviour of the system with respect to a given property. Hence, reducing the size of the generated state space while preserving the whole behaviour. The goal of this work is to assess how these methods can be implemented in Spot.