www.prismmodelchecker.org
[KNSW04] M. Kwiatkowska, G. Norman, J. Sproston and F. Wang. Symbolic Model Checking for Probabilistic Timed Automata. In Y. Lakhnech and S. Yovine (editors), Proc. FORMATS/FTRTFT'04, volume 3253 of Lecture Notes in Computer Science, pages 293-308, Springer. September 2004. [ps.gz] [pdf] [bib]
Downloads:  ps.gz ps.gz (108 KB)  pdf pdf (298 KB)  bib bib
Notes: Proofs of the key results are available in the technical report version [KNS03d].

Initial experimential results concerning a prototype implemation of the algorithms presented in this paper are available from the PRISM web page. The original publication is available at www.springerlink.com.
Abstract. Probabilistic timed automata are an extension of timed automata with discrete probability distributions, and can be used to model timed randomized protocols or fault-tolerant systems. We present symbolic model checking algorithms for verifying probabilistic timed automata against properties of PTCTL (Probabilistic Timed Computation Tree Logic). The algorithms operate on zones, which are sets of valuations of the probabilistic timed automaton's clocks, and therefore avoid an explicit construction of the state space. Furthermore, the algorithms are restricted to system behaviours which guarantee the divergence of time with probability 1. We 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.

Publications