author: Djurre van der Wal
title: Improving Symbolic Confluence Detection
keywords:
topics: Case studies and Applications
committee: Jaco van de Pol
end: January 2015

Description

Model checking often leads to very large state spaces. In order to do something about that, we apply confluence reduction, a variant of partial order reduction which is useful for process algebras. For confluence reduction, one must first check for all pairs of transitions if they are independent or not: independent transitions can be commuted. Basically, for each pair a formula is generated, and a call to an automated theorem prover is issued.

If a system has 1000 transitions, this means 1.000.000 theorems to (dis)prove! The reward of this work is a potential exponential gain in the size of the state space.

A confluence checker and corresponding theorem prover is implemented in the mCRL toolset.

Tasks

  1. Develop and implement a framework in order to dispatch the confluence formulas to a parallel cluster of theorem provers.
  2. Investigate if a prior static analysis can bring down the number of pairs to check, for instance due to symmetries, or because transitions can never be enabled at the same time.
  3. [optional] Understand the trade-off between 1 and 2. In particular, (1) favours no communication overhead between the N^2 tasks, while (2) may require information sharing between the N^2 tasks. Where is the golden middle?

Literature

Additional Resources

  1. The paper