MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper) | SpringerLink
Skip to main content
Springer Nature Link
Log in

MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper)

  • Conference paper
  • First Online:
Interactive Theorem Proving (ITP 2018)

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

Included in the following conference series:

  • 932 Accesses

Abstract

We present a formalization of probabilistic timed automata (PTA) in which we try to follow the formula “MDP + TA = PTA” as far as possible: our work starts from existing formalizations of Markov decision processes (MDP) and timed automata (TA) and combines them modularly. We prove the fundamental result for probabilistic timed automata: the region construction that is known from timed automata carries over to the probabilistic setting. In particular, this allows us to prove that minimum and maximum reachability probabilities can be computed via a reduction to MDP model checking, including the case where one wants to disregard unrealizable behavior.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 10295
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 12869
Price includes VAT (Japan)
  • 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

Similar content being viewed by others

Notes

  1. 1.

    We use the same notions as in [8]. Soundness: for every abstract run, there is a concrete instantiation. Completeness: every concrete run can be abstracted.

References

  1. Alur, R., Dill, D.L.: A theory of timed automata. Th. Comp. Sci. 126(2), 183–235 (1994). https://doi.org/10.1016/0304-3975(94)90010-8

    Article  MathSciNet  MATH  Google Scholar 

  2. Hölzl, J.: Markov chains and Markov decision processes in Isabelle/HOL. J. Autom. Reasoning 59(3), 345–387 (2017). https://doi.org/10.1007/s10817-016-9401-5

    Article  MathSciNet  MATH  Google Scholar 

  3. 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). https://doi.org/10.1007/978-3-642-22110-1_47

    Chapter  Google Scholar 

  4. Kwiatkowska, M., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. Inf. Comput. 205(7), 1027–1077 (2007)

    Article  MathSciNet  Google Scholar 

  5. Kwiatkowska, M.Z., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Th. Comp. Sci. 282(1)

    Google Scholar 

  6. Norman, G., Parker, D., Sproston, J.: Model checking for probabilistic timed automata. Formal Methods Syst. Des. 43(2), 164–190 (2013)

    Article  Google Scholar 

  7. Paulin-Mohring, C.: Modelisation of timed automata in Coq. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, pp. 298–315. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45500-0_15

    Chapter  MATH  Google Scholar 

  8. Wimmer, S.: Formalized timed automata. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 425–440. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-43144-4_26

    Chapter  Google Scholar 

  9. Wimmer, S., Hölzl, J.: Probabilistic timed automata. Archive of Formal Proofs (2018). Formal proof development. http://isa-afp.org/entries/Probabilistic_Timed_Automata.html

  10. Wimmer, S., Lammich, P.: Verified model checking of timed automata. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 61–78. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89960-2_4

    Chapter  Google Scholar 

  11. Xu, Q., Miao, H.: Formal verification framework for safety of real-time system based on timed automata model in PVS. In: Proceedings of IASTED 2006, pp. 107–112 (2006)

    Google Scholar 

Download references

Acknowledgments

We want to thank David Parker and Gethin Norman for clarifying our understanding of PTA model checking w.r.t. divergence. This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation program (grant agreement No 713999 - Matryoshka).

Author information

Authors and Affiliations

  1. TU München, Munich, Germany

    Simon Wimmer

  2. VU Amsterdam, Amsterdam, Netherlands

    Johannes Hölzl

Authors
  1. Simon Wimmer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Johannes Hölzl
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Simon Wimmer .

Editor information

Editors and Affiliations

  1. Carnegie Mellon University, Pittsburgh, PA, USA

    Jeremy Avigad

  2. Inria, Nantes, France

    Assia Mahboubi

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Wimmer, S., Hölzl, J. (2018). MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper). In: Avigad, J., Mahboubi, A. (eds) Interactive Theorem Proving. ITP 2018. Lecture Notes in Computer Science(), vol 10895. Springer, Cham. https://doi.org/10.1007/978-3-319-94821-8_35

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-94821-8_35

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-94820-1

  • Online ISBN: 978-3-319-94821-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation