Efficient Symbolic Model Checking for Process Algebras

Different approaches have been developed to mitigate the state space explosion of model checking techniques. Among them, symbolic verification techniques use efficient representations such as BDDs to reason over sets of states rather than over individual states. Unfortunately, past experience has shown that these techniques do not work well for loosely-synchronized models. This paper presents a new algorithm and a new tool that combines BDD-based model checking with partial order reduction (POR) to allow the verification of models featuring asynchronous processes, with significant performance improvements over currently available tools. We start from the ImProviso algorithm (Lerda et al.) for computing reachable states, which combines POR and symbolic verification. We merge it with the FwdUntil method (Iwashita et al.) that supports verification of a subset of CTL. Our algorithm has been implemented in a prototype that is applicable to action-based models and logics such as process alg...

• Type: Conference
• Year: 2008
• Where: FMICS
• Authors: José Vander Meulen, Charles Pecheur
• Keywords: FMICS 2008, Formal Methods, Model Checking, Symbolic Verification, Symbolic Verification Techniques