Details of Grant 

EPSRC Reference:	EP/E032354/1
Title:	Advanced Symmetry Reduction Tools for explicit state model checking
Principal Investigator:	Miller, Professor AA
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Department:	School of Computing Science
Organisation:	University of Glasgow
Scheme:	First Grant Scheme
Starts:	01 June 2007	Ends:	30 September 2010	Value (£):	209,508
EPSRC Research Topic Classifications:	Fundamentals of Computing
EPSRC Industrial Sector Classifications:	No relevance to Underpinning Sectors
Related Grants:
Panel History:
Summary on Grant Application Form
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.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk Summary Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:
Further Information:
Organisation Website:	http://www.gla.ac.uk