Partial order reduction methods for Spot

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.