Benchmarking of Partial Order Reduction in Spot

Authors

Vincent Tourneur

Type

techreport

Year

2019

Number

1901

Abstract

This report summarizes three methods implemented in the model checking tool Spot. The first method aims at improving the conversion of a program model to a Kripke structure with partial order reduction, a technique where the order of some actions of the program is not considered relevant. This may reduce the size of the Kripke structure. The second method is a modification of the first, which makes it possible to use for LTL properties checking, with any LTL formula. The third method goal is to verify that no livelock may occur in a model, without the need of LTL property. We give benchmarks of all these methods, focusing on testing their common goal: reducing the amount of memory needed, which is an important bottleneck in the model checking field.