Jeremy Sproston

Highlights Conference 2013 Conference Abstract

Solving parity games on integer vectors

• Parosh Aziz Abdulla
• Richard Mayr
• Arnaud Sangnier
• Jeremy Sproston

I&C Journal 2007 Journal Article

Symbolic model checking for probabilistic timed automata

• Marta Kwiatkowska
• Gethin Norman
• Jeremy Sproston
• Fuzhi Wang

Probabilistic timed automata are timed automata extended with discrete probability distributions, and can be used to model timed randomised protocols or fault-tolerant systems. We present symbolic model-checking algorithms for probabilistic timed automata to verify both qualitative temporal logic properties, corresponding to satisfaction with probability 0 or 1, and quantitative properties, corresponding to satisfaction with arbitrary probability. The algorithms operate on zones, which represent sets of valuations of the probabilistic timed automaton’s clocks. Our method considers only those system behaviours which guarantee the divergence of time with probability 1. The paper presents a symbolic framework for the verification of probabilistic timed automata against the probabilistic, timed temporal logic PTCTL. We also report on a prototype implementation of the algorithms using Difference Bound Matrices, and present the results of its application to the CSMA/CD and FireWire root contention protocol case studies.

TCS Journal 2002 Journal Article

Automatic verification of real-time systems with discrete probability distributions

• Marta Kwiatkowska
• Gethin Norman
• Roberto Segala
• Jeremy Sproston

We consider the timed automata model of Alur and Dill (Theoret. Comput. Sci. 126 (1994) 183–235), which allows the analysis of real-time systems expressed in terms of quantitative timing constraints. Traditional approaches to real-time system description express the model purely in terms of nondeterminism; however, it is often desirable to express the likelihood of the system making certain transitions. In this paper, we present a model for real-time systems augmented with discrete probability distributions. Furthermore, two approaches to model checking are introduced for this model. The first uses the algorithm of Baier and Kwiatkowska (Distributed Comput. 11 (1998) 125–155) to provide a verification technique against temporal logic formulae which can refer both to timing properties and probabilities. The second, generally more efficient, technique concerns the verification of probabilistic, real-time reachability properties.