Performance Analysis of Probabilistic Timed Automata Using Digital Clocks

  • Marta Kwiatkowska
  • Gethin Norman
  • David Parker
  • Jeremy Sproston
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2791)


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.


Discrete Probability Distribution Message Loss Address Resolution Protocol Digital Clock Reachability Property 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Alur, R., Torre, S., Pappas, G.: Optimal paths in weighted timed automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 49–62. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  3. 3.
    Behrmann, G., David, A., Larsen, K., Möller, O., Pettersson, P., Yi, W.: UPPAAL - present and future. In: Proc. CDC 2001, IEEE Computer Society Press, Los Alamitos (2001)Google Scholar
  4. 4.
    Behrmann, G., Fehnker, A., Hune, T., Larsen, K., Pettersson, P., Romijn, J.: Efficient guiding towards cost-optimality in UPPAAL. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 174–188. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  5. 5.
    Behrmann, G., Fehnker, A., Hune, T., Larsen, K., Pettersson, P., Romijn, J., Vaandrager, F.: Minimum-cost reachability for priced timed automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 147–161. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  6. 6.
    Bertsekas, D., Tsitsiklis, J.: An analysis of stochastic shortest path problems. Mathematics of Operations Research 16(3), 580–595 (1991)zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499–513. Springer, Heidelberg (1995)Google Scholar
  8. 8.
    Bohnenkamp, H., Stok, P.v.d., Hermanns, H., Vaandrager, F.: Costoptimisation of the IPv4 zeroconf protocol. In: Proc. IPDS 2003, IEEE CS Press, Los Alamitos (2003)Google Scholar
  9. 9.
    Bosnacki, D.: Digitization of timed automata. In: Proc. FMICS 1999, pp. 283–302 (1999)Google Scholar
  10. 10.
    Cheshire, S., Adoba, B., Guttman, E.: Dynamic configuration of IPv4 link-local addresses. Draft (August 2002), Available from
  11. 11.
    Daws, C., Kwiatkowska, M., Norman, G.: Automatic verification of the IEEE 1394 root contention protocol with Kronos and Prism. In: Proc. FMICS 2002. ENTCS, vol. 66(2), Elsevier Science, Amsterdam (2002)Google Scholar
  12. 12.
    de Alfaro, L.: Formal Verification of Probabilistic Systems. PhD thesis, Stanford University (1997)Google Scholar
  13. 13.
    de Alfaro, L.: Computing minimum and maximum reachability times in probabilistic systems. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 66–81. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  14. 14.
    Derman, C.: Finite-State Markovian Decision Processes. Academic Press, London (1970)zbMATHGoogle Scholar
  15. 15.
    Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 545–558. Springer, Heidelberg (1992)Google Scholar
  16. 16.
    Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains, 2nd edn. Graduate Texts in Mathematics. Springer, Heidelberg (1976)zbMATHGoogle Scholar
  17. 17.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 200–204. Springer, Heidelberg (2002)Google Scholar
  18. 18.
    Kwiatkowska, M., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. Technical Report CSR-03-6, School of Computer Science, University of Birmingham (2003)Google Scholar
  19. 19.
    Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science 282, 101–150 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  20. 20.
    Kwiatkowska, M., Norman, G., Sproston, J.: Symbolic computation of maximal probabilistic reachability. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 169–183. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  21. 21.
    Kwiatkowska, M., Norman, G., Sproston, J.: Probabilistic model checking of the IEEE 802.11 wireless local area network protocol. In: Hermanns, H., Segala, R. (eds.) PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol. 2399, pp. 169–187. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  22. 22.
    Kwiatkowska, M., Norman, G., Sproston, J.: Probabilistic model checking of deadline properties in the IEEE 1394 FireWire root contention protocol. Formal Aspects of Computing 14(3), 295–318 (2003)CrossRefGoogle Scholar
  23. 23.
    Larsen, K., Behrmann, G., Brinksma, E., Fehnker, A., Hune, T., Pettersson, P., Romijn, J.: As cheap as possible: Efficient cost-optimal reachability for priced timed automata. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 493–505. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  24. 24.
    Ouaknine, J., Worrell, J.: Universality and language inclusion for open and closed timed automata. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 375–388. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  25. 25.
  26. 26.
    Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Massachusetts Institute of Technology (1995)Google Scholar
  27. 27.
    Tripakis, S.: The formal analysis of timed systems in practice. PhD thesis, Université Joseph Fourier (1998)Google Scholar
  28. 28.
    Vardi, M.: Automatic verification of probabilistic concurrent finite state programs. In: Proc. FOCS 1985, pp. 327–338. IEEE Computer Society Press, Los Alamitos (1985)Google Scholar
  29. 29.
    Zhang, M., Vaandrager, F.: Analysis of a protocol for dynamic configuration of IPv4 link local addresses using Uppaal. Technical Report, NIII, University of Nijmegen (2003)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Marta Kwiatkowska
    • 1
  • Gethin Norman
    • 1
  • David Parker
    • 1
  • Jeremy Sproston
    • 2
  1. 1.School of Computer ScienceUniversity of BirminghamBirminghamUK
  2. 2.Dipartimento di InformaticaUniversità di TorinoTorinoItaly

Personalised recommendations