Combining Partial Order Reduction with Symbolic Model Checking

JosÚ Vander Meulen
, , , , ,
Combining Partial Order Reduction with Symbolic Model Checking
JosÚ Vander Meulen
 dissertation.pdf Δ   1,048Kb   15 Jun 2012
Doctoral thesis, UniversitÚ catholique de Louvain


Model checking is an efficient technique for verifying properties on asynchronous systems. Unfortunately, it suffers from the so-called combinatorial state-space explosion problem. Two common approaches are used to fight this problem, with different perspectives. On the one hand, partial-order reduction (POR) methods explore a reduced state space in a property-preserving way. On the other hand, symbolic techniques use efficient structures such as binary decision diagrams (BDD's) to concisely encode and compute large state spaces. This thesis presents algorithms which, one way or another, combine symbolic model checking and partial-order reduction, allowing efficient verification of CTLX and LTLX properties on models featuring asynchronous processes.

At the root of our work was the ImProviso algorithm for computing reachable states, which combines POR and symbolic verification, and the FwdUntil method that supports verification of a subset of CTL. We present the PartialExploration algorithm which adapts and extends ImProviso to support the verification of a fragment of CTLX. Then, the evalCTLX algorithm merges the PartialExploration algorithm with the classical backward algorithm to support the totality of CTL.

The evalLTLX algorithm checks LTLX properties. We start from the tableau-based reduction of LTL verification of Clarke et al. which translates an LTL problem into a fair path detection problem. While classical BDD-based model-checking would perform this search with a backward traversal, we use the forward-traversal approach of Iwashita et al. Part of the resulting computation amounts to computing the reachable state space; to that end we use our PartialExploration algorithm.

The BPE algorithm adapts our PartialExploration algorithm and bounded model checking techniques in an original way. The encoding to a SAT problem strongly reduces the complexity and non-determinism of each transition step, allowing efficient analysis even with longer execution traces.

The algorithms developed in this thesis were implemented in a new model checker which is called Milestones. It allows us to check the absence of deadlock, LTL properties, and CTL properties. In order to compare our approach to others, Milestones can translate a model into an equivalent Spin model or NuSMV model.

Tags Tags: , , , , ,

BibTeX Record
    TITLE = {Combining Partial Order Reduction with Symbolic Model Checking},
    AUTHOR = {JosÚ {Vander Meulen}},
    YEAR = {2012},
    VOLUME = {370},
    PUBLISHER = {Doctoral thesis, UniversitÚ catholique de Louvain},
    URL = {},