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.


Reachable State Reduction Function Relevant Transition Stateful Model Check Exploration Algorithm 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


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