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

• S.C.C. Blom and J.C. van de Pol, State Space Reduction by Proving Confluence http://www.springerlink.com/content/57bb3gj4auy3kkcq/
• the tools 'confcheck' and 'lpsconfcheck' in the muCRL toolset and its successor mcrl2 http://homepages.cwi.nl/~mcrl/manpages/rn02re03.html http://mcrl2.org/wiki/index.php/User_manual/lpsconfcheck
• slides of MACS 1, lecture 7 8, https://teletopb.utwente.nl/08213531.nsf

Additional Resources

1. The paper