Static Partial Order Reduction in Stateful Model Checking

Part of the BestMasters book series (BEST)


POR is a particularly effective technique to alleviate the state explosion problem by limiting the exploration of redundant transition interleavings. POR works by selecting only a subset of enabled transitions in each step, which are sufficient to prove the desired properties. The other transitions are temporarily ignored, since they are non-interfering with those that are selected. A stateful search on the other hand avoids re-exploration of already visited states. A naive combination of both techniques can lead to the point, where a relevant transition is permanently ignored due to a cycle in the reduced state space.


Val89 Alse 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer Fachmedien Wiesbaden 2016

Authors and Affiliations

  1. 1.BremenGermany

Personalised recommendations