|Djurre van der Wal
|Improving Symbolic Confluence Detection
|Case studies and Applications
|Jaco van de Pol
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.
- Develop and implement a framework in order to dispatch the confluence formulas to a parallel cluster of theorem provers.
- 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.
- [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?
- 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