Partial order reduction in SPOT



Nowadays, model-checking tools suffer from a scalling problem, due to their memory consuption. Partial order reduction is one way allowing to notably reduce it, by computing only needed data on-the-fly. There are many state-of-the-art algorithms, and this method is used in many softwares (such as SPIN or LTSmin). We are going to talk about the implementation of it in the Spot libraryand then the optimisation. The results show a great decrease of the memory consuption, which implies some gain in all subsequent steps.