Undecidability of Cost-Bounded Reachability in Priced Probabilistic Timed Automata

  • Jasper Berendsen
  • Taolue Chen
  • David N. Jansen
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5532)


Priced Probabilistic Timed Automata (PPTA) extend timed automata with cost-rates in locations and discrete probabilistic branching. The model is a natural combination of Priced Timed Automata and Probabilistic Timed Automata. In this paper we focus on cost-bounded probabilistic reachability for PPTA, which determines if the maximal probability to reach a goal location within a given cost bound (and time bound) exceeds a threshold p ∈ (0,1]. We prove undecidability of the problem for simple PPTA in 3 variants: with 3 clocks and stopwatch cost-rates or strictly positive cost-rates. Because we encode a 2-counter machine in a new way, we can also show undecidability for cost-rates in ℤ and only 2 clocks.


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.L., Pappas, G.J.: 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., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J., Vaandrager, F.W.: 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
  4. 4.
    Berendsen, J., Jansen, D.N., Katoen, J.P.: Probably on time and within budget: On reachability in priced probabilistic timed automata. In: QEST, pp. 311–322. IEEE Computer Society Press, Los Alamitos (2006)Google Scholar
  5. 5.
    Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science 282(1), 101–150 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Bouyer, P., Brihaye, T., Markey, N.: Improved undecidability results on weighted timed automata. Inf. Process. Lett. 98(5), 188–194 (2006)CrossRefMathSciNetGoogle Scholar
  7. 7.
    Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Srba, J.: Infinite runs in weighted timed automata with energy constraints. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 33–47. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  8. 8.
    Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains, 2nd edn. Springer, New York (1976)zbMATHGoogle Scholar
  9. 9.
    Minsky, M.L.: Computation: finite and infinite machines. Prentice-Hall, Inc., Upper Saddle River (1967)zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Jasper Berendsen
    • 1
  • Taolue Chen
    • 2
  • David N. Jansen
    • 1
  1. 1.Institute for Computing and Information SciencesRadboud University NijmegenNijmegenThe Netherlands
  2. 2.Department of Software EngineeringCWIAmsterdamThe Netherlands

Personalised recommendations