The main achievements of the project, with respect to each of the original project objectives, are as follows.
Objective 1 (costs and rewards)
The PRISM modelling language, property specification language and underlying solution engines have all been enhanced with support for costs and rewards. Two types of "instantaneous" properties (transient and long-run) and two types of "cumulative" properties (time-bound and reachability based) can be analysed against multiple named reward structures. This permits analysis of a very wide range of quantitative measures, such as expected power consumption and expected number of rounds (not just expected-time, as originally proposed). This functionality is now in the public release of PRISM [HKNP06] and has consequently been employed on many new and existing case studies.
Objective 2 (data type reduction)
A novel abstraction technique for the quantitative verification of MDPs has been developed, based on the conversion to a stochastic 2-player game. This abstraction process involves a reduction of the data variables of the model in PRISM language description. Its effectiveness has been demonstrated on a real-world case study: the Zeroconf protocol (also studied without abstraction techniques on this project [KNPS03, KNPS06]). The work was presented at the 3rd International Conference on Quantitative Evaluation of Systems (QEST'06) [KNP06b] and was winner of the conference "best paper" award. This research also represents a crucial component of a new research direction for Kwiatkowska's group (quantitative verification of software with predicate abstraction), now supported by a new 3-year EPSRC grant (EP/D07956X).
Objective 3 (assume-guarantee style reasoning)
This was, as identified in the original proposal, the most ambitious objective, aimed at developing verification methodologies for PRISM in order to scale up the tool's capabilities to larger and/or infinite-state probabilistic systems. We were unable to formulate an assume-guarantee rule for the probabilistic setting, and after further investigation found existing approaches (de Alfaro et al) unsuitable for PRISM. However, promising recent work on algorithms for qualitative and quantitative multi-objective optimisation in MDPs by Kwiatkowska in collaboration with Etessami, Vardi and Yannakakis [EKVY06] is hoped to provide a basis for compositional assume-guarantee style techniques. The project focused on a number of state-of-the-art methodologies to develop a range of techniques that can be used in conjunction with proof-style reasoning and that extend the applicability of PRISM. These include abstraction (see previous paragraph), symmetry reduction, partial order reduction, real-time probabilistic model checking and statistical probabilistic model checking. We now comment briefly on the progress made on each of these topics.
Symmetry reduction
A technique for applying probabilistic model checking to fully symmetric systems was developed and a novel, symbolic (MTBDD-based) implementation devised for all three model types supported by PRISM. The abundance of case studies exhibiting such symmetry, for example distributed randomised algorithms and communication protocols, provides clear motivation for this research. Results were a very significant increase in verification efficiency on many real-life case studies: near-factorial state space reductions and orders-of-magnitude decrease in solution time. The work was presented at CAV'06 [KNP06a] and, in response to significant interest, the implementation has been made publicly available (http://www.prismmodelchecker.org/symm/). The technique has also proved useful in further PRISM case studies developed subsequently, in particular those relating to biological systems [HKN+06, KNP+06].
Partial order reduction
In collaboration with Baier, Ciesinski and Groesser, existing techniques for applying partial order reduction to probabilistic systems (MDPs) were extended to the case where the models are augmented with costs or rewards [BCG+06].
Real-time probabilistic model checking
New techniques for the automatic verification of probabilistic timed automata (PTAs), which model continuous time and are thus inherently infinite state in nature, have also been developed. These include the digital clocks approach [KNPS03, KNPS06], which is based on the reduction of a large class of PTA models to an equivalent integer-valued clocks semantics. Additionally, a symbolic algorithm based on MTBDDs has been implemented [KNSW04, WK05] and, in collaboration with Segala, a probabilistic model with continuous state spaces and branching was proposed and studied [CSKN05].
Statistical probabilistic model checking
An alternative way of handling large probabilistic models is the so-called statistical probabilistic model checking approach, based on hypothesis testing and discrete-event simulation. In collaboration with Younes, a comparative study of this approach with conventional, numerical solution based techniques (as implemented in PRISM) was carried out [YKNP04, YKNP06].
Objective 4 (dynamic environments)
Work has been undertaken to investigate modelling formalisms for dynamic environments, applicable to e.g. mobile wireless networks. A novel probabilistic extension of the mobile ambients formalism, has been proposed, along with a corresponding spatial logic for specification of properties [KNPV06]. This model combines the ability of ambients to represent dynamic, mobile systems, with support for probabilistic behaviour and for nondeterminism, as required to accurately model concurrency. Further investigation into the applicability of such formalisms to probabilistic model checking has been undertaken by exploring the possibility of modelling biological systems with stochastic versions of mobile ambients in collaboration with Heath (Biosciences, Birmingham). Additionally, working with Palamidessi and Wu (LIX), a prototype tool for automatic translation of the probabilistic pi-calculus into PRISM has been developed and is still underway.
Objective 5 (distributed implementation)
Research in this area has focused around iterative solutions for linear equations systems (directly applicable to probabilistic model checking of both DTMCs and CTMCs) for two distinct parallel architectures: small-scale, shared memory based setups (e.g. dual or quad processor machines) and PC clusters. Novel, symbolic techniques for each were developed and presented at MASCOTS'04 [KPZM04] and DSN'05 [ZPK05a], respectively, with impressive speed-ups demonstrated on a range of benchmark models. A journal submission combining and extending the two papers is in progress. More recently, distributed implementations for a larger scale, Grid-based parallel architecture were developed and presented in [ZPK05b]. Finally, the new discrete-event simulation engine (described earlier) was also parallelised [HKNP06].
Objective 6 (case studies)
Throughout the project, we have continued to develop and collaborate on case studies, and also to support work on those being developed externally. This has, as previously, proved useful to test the new techniques developed, identify the need for new functionality, and establish new connections and collaborations.
Key case studies worked on throughout the project include: the wireless communication standard Bluetooth [DKNP04, DKNP06], dynamic power management systems [NPK+05, KNP05c], fault-tolerant systems (NAND multiplexing) [NPKS04, NPKS05] and control systems [KNP04c, KNP06c]. A new application domain, biological systems, has also begun to be studied [HKN+06, KNP+06] and, thanks to newly established collaborations and funding, is expected to become an important source of case studies and research directions for PRISM. Outside the project, case studies have included probabilistic security protocols by Norman (Birmingham) and Shmatikov (now Texas), randomised consensus algorithms by Cheung (now MIT) and PIN cracking schemes by Steel (Edinburgh). Detailed information about these examples, including model source code, is to be found in the online PRISM case study repository.
Finally, invited overview papers describing the application of PRISM to a range of case studies were published in ACM PER [KNP05b] and ENTCS [KNP05d].
Tool enhancements
In addition to the work described above, a wide range of improvements and additions have been made to PRISM, driven by both the needs of the research project and by requests from collaborators and users of the tool. One of the most significant has been an engine for discrete-event simulation [Hin05], which adds both an extremely valuable debugging tool for modellers and approximate Monte-Carlo based probabilistic model checking capabilities to PRISM, feasible on much larger models than for conventional, exact techniques. Other tool enhancements include efficiency improvements to the underlying MTBDD-based model checking algorithms and data structures [KPZM04, KNP04b], extensions to the PRISM model and property specification languages, improvements to the graphical user interface, additional functionality for model import and export, including connections to other tools (e.g. ETMCC/MRMC), and ports of the software to other operating systems (MS Windows, Mac OS X). As always, these enhancements have been distributed in a free and open source fashion, with two major public releases (versions 2.0 and 3.0) of PRISM occurring during this time and corresponding tool papers presented at QEST'04 [KNP04d] and TACAS'06 [HKNP06].