www.prismmodelchecker.org
[KNPS03] Marta Kwiatkowska, Gethin Norman, David Parker and Jeremy Sproston. Performance Analysis of Probabilistic Timed Automata using Digital Clocks. In Proc. Formal Modeling and Analysis of Timed Systems (FORMATS'03), volume 2791 of LNCS, pages 105-120, Springer. September 2003. [ps.gz] [pdf] [bib]
Downloads:  ps.gz ps.gz (104 KB)  pdf pdf (293 KB)  bib bib
Notes: This paper is now superceded by the journal version [KNPS06].

An extended version of this paper is available in the technical report CSR-03-06.

Further information and verification results are available from the PRISM web page. The original publication is available at www.springerlink.com.
Abstract. Probabilistic timed automata, a variant of timed automata extended with discrete probability distributions, is a specification formalism suitable for describing both nondeterministic and probabilistic aspects of real-time systems, and is amenable to model checking against probabilistic timed temporal logic properties. In the case of classical (non-probabilistic) timed automata, it has been shown that for a large class of real-time verification problems correctness can be established using an integer-time model, inducing a notion of digital clocks, as opposed to the standard dense model of time. Based on these results, we address the question of under what conditions digital clocks are sufficient for the performance analysis of probabilistic timed automata. We extend previous results concerning the integer-time semantics of an important subclass of probabilistic timed automata to consider the computation of expected costs or rewards. We illustrate this approach through the analysis of the dynamic configuration protocol for IPv4 link-local addresses.

Publications