PRISM Model Checker
Web Page: http://www.prismmodelchecker.org/gsoc/
Mailing List: https://groups.google.com/forum/?fromgroups#!forum/prismmodelchecker-dev
PRISM is a software tool for modelling and studying the behaviour of real-life systems whose behaviour exhibits unpredictability or randomness. It can be used to analyse everything from the reliability of distributed filing systems, to the performance of a Bluetooth-enabled wireless device, to the safety of a car's airbag control system. PRISM has been used by researchers worldwide in fields as diverse as quantum cryptography, systems biology, computer security and robotics. Development of PRISM is split between the University of Birmingham and the University of Oxford, UK. It has been under development for over 10 years and contains about 200K lines of code in total. The software is coded primarily in Java, including a graphical user interface written in Swing, but with various underlying libraries written in C/C++.
Projects
- Markov decision process strategy/policy generation functionality for PRISM PRISM generates an optimal strategy in model checking some properties of MDPs, i.e. the one which corresponds to either the minimum or maximum values of the probabilities or rewards computed during verification. Currently the main version of PRISM just exports optimal strategies (sometimes called adversaries in PRISM) for two classes of properties- maximum or minimum probabilities. They are exported in a simple flat text file, from PRISM's "sparse" engine. It would be good to (in increasing order of complexity) - Optimize the strategies, e.g. by restricting to reachable states -Add alternative file formats, e.g. GraphViz dot files -Add strategy generation for other engines -Expand to other property types, e.g. bounded reachability and LTL formulae
- Model checking for stochastic games This project will focus on implementing model checking techniques for stochastic games. The main goal of the project is to gain support for LTL model checking on the stochastic games engine, and to further improve the games engine itself by solving the equilibriums through strategy iteration techniques. This will improve the analysis of stochastic games both in expressive power and in efficiency.