Advanced Symmetry Reduction Tools for explicit state model checking

Model checking is an established technique for checking the reliability of software-controlled systems and constitutes one of hte leading applications of logic to computer science. This automatic technique involves the construction of a model of a system over which properties are checked. One of the major problems with model checking is the (so-called) state-space explosion problem - where models become too large to feasibly check. A popular technique for combatting state-space explosion is symmetry reduction. Though efficient, most symmetry reduction tools are highly restrictive. They often rely on the existence of full symmetry between components of a system, and can be used to check only a limited class of system property. In addition, full access to the source-code of the original model checking software is essential for successful development of a symmetry reduction tool. Explicit state probabilistic model checking is still in its infancy and as such has yet to have had symmetry reduction methods applied to it. In our previous research developing the TopSPIN symmetry reduction package for SPIN, we have cultivated a unique framework of techniques and tools for symmetry reduced explicit state model checking. We propose to extend TopSPIN and construct a new, purpose-built explicit state model checker as a test-bed for explicit state symmetry reduction techniques for probabilistic systems. The major deliverables of this proposal are the development of advanced theories for, and implementation of:- an extension of TopSPIN for a wider class of properties, increased usability and faster execution and- a new explicit state probabilistic model checker, with built-in symmetry reduction capability.The proposed research builds on our existing work (the techniques use for the initial development of TopSPIN). As such we are in a unique position to undertake this research. The principal investigator (PI) will devote 3 hours a week to this project. In addition we request a 2 year postdoctoral reasearch assistant (PDRA) and a 3 year postgraduate research student (PGRS). The PDRA will work on the TopSPIN extension and train the PGRS. The PGRS will develop the model checker, under the guidance of the PI and the PDRA.