Skip to main content
SpringerLink
Log in

Symbolic Minimum Expected Time Controller Synthesis for Probabilistic Timed Automata

  • Conference paper
  • First Online:
Book cover Formal Modeling and Analysis of Timed Systems (FORMATS 2015)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9268))

Abstract

In this paper we consider the problem of computing the minimum expected time to reach a target and the synthesis of the corresponding optimal controller for a probabilistic timed automaton (PTA). Although this problem admits solutions that employ the digital clocks abstraction or statistical model checking, symbolic methods based on zones and priced zones fail due to the difficulty of incorporating probabilistic branching in the context of dense time. We work in a generalisation of the setting introduced by Asarin and Maler for the corresponding problem for timed automata, where simple and nice functions are introduced to ensure finiteness of the dense-time representation. We find restrictions sufficient for value iteration to converge to the minimum expected time on the uncountable Markov decision process representing the semantics of a PTA. We formulate a Bellman operator on the backwards zone graph of a PTA and prove that value iteration using this operator equals that computed over the PTA’s semantics. This enables us to extract an \(\varepsilon \)-optimal controller from value iteration in the standard way.

This research is supported by ERC AdG VERIWARE.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Dill, D.L.: A theory of timed automata. TCS 126, 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  2. Asarin, E., Maler, O.: As soon as possible: time optimal control for timed automata. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 19–30. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  3. Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Science of Computer Programming 72(1–2), 3–21 (2008)

    Article  MathSciNet  Google Scholar 

  4. Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J.M.T., 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)

    Chapter  Google Scholar 

  5. Bellman, R.: Dynamic Programming. Princeton University Press (1957)

    Google Scholar 

  6. Berendsen, J., Chen, T., Jansen, D.N.: Undecidability of cost-bounded reachability in priced probabilistic timed automata. In: Chen, J., Cooper, S.B. (eds.) TAMC 2009. LNCS, vol. 5532, pp. 128–137. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  7. Berendsen, J., Jansen, D., Katoen, J.-P.: Probably on time and within budget - on reachability in priced probabilistic timed automata. In: Proc. QEST 2006. IEEE Press (2006)

    Google Scholar 

  8. Berendsen, J., Jansen, D., Vaandrager, F.: Fortuna: Model checking priced probabilistic timed automata. In: Proc. QEST 2010. IEEE Press (2010)

    Google Scholar 

  9. Bertsekas, D.: Dynamic Programming and Optimal Control, vol. 1 and 2. Athena Scientific (1995)

    Google Scholar 

  10. Bertsekas, D., Tsitsiklis, J.: An analysis of stochastic shortest path problems. Mathematics of Operations Research 16(3), 580–595 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  11. Bulychev, P., David, A., Larsen, K., Mikučionis, M., Poulsen, D.B., Legay, A., Wang, Z.: UPPAAL-SMC: statistical model checking for priced timed automata. In: Proc. QAPL 2012, vol. 85 of EPTCS. Open Publishing Association (2012)

    Google Scholar 

  12. David, A., Jensen, P.G., Larsen, K.G., Legay, A., Lime, D., Sørensen, M.G., Taankvist, J.H.: On time with minimal expected cost!. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 129–145. Springer, Heidelberg (2014)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  14. James, H., Collins, E.: An analysis of transient Markov decision processes. Journal of Applied Probability 43(3), 603–621 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  15. Jovanović, A., Kwiatkowska, M., Norman, G.: Symbolic minimum expected time controller synthesis for probabilistic timed automata. Technical Report CS-RR-15-04, Oxford University (2015)

    Google Scholar 

  16. Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains. Springer (1976)

    Google Scholar 

  17. Kwiatkowska, M., Norman, G., Parker, D.: Stochastic games for verification of probabilistic timed automata. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol. 5813, pp. 212–227. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  18. Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  19. Kwiatkowska, M., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. FMSD 29, 33–78 (2006)

    MATH  Google Scholar 

  20. Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. TCS 282, 101–150 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  21. Kwiatkowska, M., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. Information and Computation 205(7), 1027–1077 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  22. Larsen, K.G., Behrmann, G., Brinksma, E., Fehnker, A., Hune, T., Pettersson, P., Romijn, J.M.T.: 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)

    Chapter  Google Scholar 

  23. Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a Nutshell. Int. Journal on Software Tools for Technology Transfer 1, 134–152 (1997)

    Article  MATH  Google Scholar 

  24. Tripakis, S.: The analysis of timed systems in practice. PhD thesis, Université Joseph Fourier, Grenoble (1998)

    Google Scholar 

  25. Tripakis, S.: Verifying progress in timed systems. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol. 1601, pp. 299–314. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  26. Tripakis, S., Yovine, S., Bouajjan, A.: Checking timed Büchi automata emptiness efficiently. Formal Methods in System Design 26(3), 267–292 (2005)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Oxford, Oxford, OX1 3QD, UK

    Aleksandra Jovanović & Marta Kwiatkowska

  2. School of Computing Science, University of Glasgow, Glasgow, G12 8RZ, UK

    Gethin Norman

Authors
  1. Aleksandra Jovanović
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marta Kwiatkowska
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Gethin Norman
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Gethin Norman .

Editor information

Editors and Affiliations

  1. University of Colorado, Boulder, Colorado, USA

    Sriram Sankaranarayanan

  2. University of Florence, Florence, Italy

    Enrico Vicario

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Jovanović, A., Kwiatkowska, M., Norman, G. (2015). Symbolic Minimum Expected Time Controller Synthesis for Probabilistic Timed Automata. In: Sankaranarayanan, S., Vicario, E. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2015. Lecture Notes in Computer Science(), vol 9268. Springer, Cham. https://doi.org/10.1007/978-3-319-22975-1_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-22975-1_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-22974-4

  • Online ISBN: 978-3-319-22975-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation