We believe that this project fully satisfied the objectives as stated in the original proposal. The research was directly aimed at the software tool PRISM, a Probabilistic Symbolic Model Checker [KNP02a] implemented at the University of Birmingham with the help of EPSRC funding (EPSRC MathFIT studentship for Dave Parker and GR/M04617 completed in 2001 and rated Outstanding). PRISM is at the core of the research programme being carried out by the probabilistic model checking goup. Since PRISM was released for use in September 2001 (available freely for academic use from here), it has has been downloaded by 600 users, and is now the leading tool in the area.
PRISM provides direct support for three types of models, discrete time Markov chains, Markov decision processes and continuous time Markov chains, and indirectly supports probabilistic timed automata via a connection to KRONOS [DKN04,DKN02] and digital clocks [KNS02a,KNPS03]. This project contributed mostly to the probabilistic timed automata model and, to some extent, Markov chains. In the lifetime of this project we were able to substantially advance the software technology that underpins probabilistic model checking with PRISM.
The project additionally benefitted from EPSRC project Automatic Verification of Randomized Distributed Algorithms (GR/M04617), a MathFIT studentship for Dave Parker, British-German collaboration project on Stochastic Modelling and Verification and additional financial support from QinetiQ. Rashid Mehmood, PhD student, and visitors and collaborators (Conrado Daws, Stephen Gilmore, Rajesh Gupta, Holger Hermanns, Annabelle McIver, Carroll Morgan, Sylvain Peyronnet, Antonio Pacheco, Roberto Segala, Vitaly Shmatikov, Sandeep Shukla, Markus Siegle and Hakan Younes) also contributed.
Below we summarise the main achievements in relation to the objectives.
We have continued the development of the probabilistic timed automata model [KNSS02] formulating model checking algorithms based on digital clocks [KNPS03,KNS02a], the region graph [KNSS02], and forwards [KNSS02] and backwards [KNS00,KNS03c,KNS01b] traversal of the zone graph. The recent generalisation of the symbolic model checking method to full PTCTL [KNS03d] completes the framework. An algorithm for the verification of probabilistic timed automata extended with continuous time probability distributions is presented in [KNSS00a], solving an open problem. Probabilistic hybrid automata were introduced by Sproston in [Spr00] where decidability of certain problems was demonstrated.
For Quality of Service properties, we have considered both probabilistic reachability problems [KNS00] and their extension to costs/rewards [KNPS03], as well as the logic PTCTL [KNS03b,KNS03d]. We have also advanced the logic CSL for continuous time Markov chain models, by formulating extensions with random time bounds, for until formulas [KNP02c] and expected time [KNP02d].
A broad range of industrially relevant case studies were developed, see here. The Byzantine agreement of Kursawe et al was verified using PRISM and Cadence SMV [KN02]. This example was contributed by collaborators at QinetiQ. Shmatikov used PRISM to analyse the Crowds anonymity protocol [Shm02, Shm04] and, with Norman, contract signing [NS02]. The IEEE 1394 FireWire Root Contention was analysed using digital clocks [KNS03b] and forwards reachability for probabilistic timed automata introduced in [KNSS02], with the help of the connection to the KRONOS real-time model checker [DKN04,DKN02]. The IEEE 802.11 WLAN MAC protocol was analysed in [KNS02a] and the IPv4 ZeroConf dynamic configuration protocol in [KNPS03]. With Shukla and Gupta, PRISM was used for dynamic power management [NPK+03,NPK+02]. Reliability of defect-tolerant architectures for nanotechnology was considered in [NPKS04]. There was an exchange of case studies with Dr Katoen, Visiting Fellow and contributor to the tool ETMCC.
This line of research is being pursued by Stefano Cattani, PhD student currently in the 3rd year. His research focuses on CSP, for which he has proposed an extension with clocks in the style of timed automata. The chief motivation is to obtain a decidable refinement procedure for this CSP extension that allows to establish a chain of refinements. This is nontrivial in view of existing undecidability results for timed automata language inclusion, and also for Timed CSP. A preliminary paper was presented at AVoCS'03 [CK03], and a journal version is currently under preparation. A continuous probabilistic trace semantics, and the corresponding extension of CSP, is making progress utilising aspects of [CS02] introduced in Cattani's MSc thesis.
We substantially advanced data structures and algorithms for symbolic model checking of probabilistic processes, and specifically for continuous time Markov chains, where collaboration with the Visiting Fellow, Dr. Katoen, resulted in impressive O(N) improvement to the methodology [KKNP01]. We investigated in detail the performance of MTBDD data structures when representing and verifying probabilistic systems [HKN+03], formulated a compact data structure for representing Markov models (offset-labelled MTBDDs) which performs nearly as fast as sparse matrices [KNP02b], and developed a range of out-of-core approaches for the analysis of large models [KM02,KMNP02]. Work on combining compact, BDD-based, data structures for probability (MTBDDs) and time (CDDs) is being continued by PhD student Fuzhi Wang. This will be incorporated within the PRISM tool as soon as practical.
This project has led to engagement in a collaborative project (FORWARD, funded by DTI/QinetiQ as part of the Next Wave Initiative) involving QinetiQ, Oxford, Birmingham and Formal Systems that aims, amongst other things, to connect the CSP FDR model checker as a front-end to PRISM. A PEPA reflector for PRISM was earlier implemented with the help of Stephen Gilmore, University of Edinburgh. We are shortly to make available an approximation method for discrete time Markov chains achieved in collaboration with Sylvain Peyronnet, Paris Orsay, and for CSL with Hakan Younes, CMU. A new GUI, including support for graphical input and function graph plots, has been implemented by student Andrew Hinton. More information about existing collaborations can be found here.