Document Open Access Logo

On Decidability of Time-Bounded Reachability in CTMDPs

Authors Rupak Majumdar , Mahmoud Salamati , Sadegh Soudjani

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2020.133.pdf
  • Filesize: 0.62 MB
  • 19 pages

Document Identifiers

Author Details

Rupak Majumdar
  • Max-Planck Institute for Software Systems, Kaiserslautern, Germany
Mahmoud Salamati
  • Max-Planck Institute for Software Systems, Kaiserslautern, Germany
Sadegh Soudjani
  • Newcastle University, Newcastle upon Tyne, UK

Funding

This research was funded in part by the Deutsche Forschungsgemeinschaft project 389792660-TRR 248 and by the European Research Council under the Grant Agreement 610150 (ERC Synergy Grant ImPACT).

Acknowledgements

We thank Joël Ouaknine, James Worrell, and Joost-Pieter Katoen for discussions and pointers.

Cite AsGet BibTex

Rupak Majumdar, Mahmoud Salamati, and Sadegh Soudjani. On Decidability of Time-Bounded Reachability in CTMDPs. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 133:1-133:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.ICALP.2020.133

Abstract

We consider the time-bounded reachability problem for continuous-time Markov decision processes. We show that the problem is decidable subject to Schanuel’s conjecture. Our decision procedure relies on the structure of optimal policies and the conditional decidability (under Schanuel’s conjecture) of the theory of reals extended with exponential and trigonometric functions over bounded domains. We further show that any unconditional decidability result would imply unconditional decidability of the bounded continuous Skolem problem, or equivalently, the problem of checking if an exponential polynomial has a non-tangential zero in a bounded interval. We note that the latter problems are also decidable subject to Schanuel’s conjecture but finding unconditional decision procedures remain longstanding open problems.

Subject Classification

ACM Subject Classification
  • Theory of computation → Numeric approximation algorithms
  • Mathematics of computing → Markov processes
  • Theory of computation → Verification by model checking
Keywords
  • CTMDP
  • Time bounded reachability
  • Continuous Skolem Problem
  • Schanuel’s Conjecture

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Mark J. Ablowitz and Athanassios S. Fokas. Complex Variables: Introduction and Applications. Cambridge Texts in Applied Mathematics. Cambridge University Press, 2003. URL: https://doi.org/10.1017/CBO9780511791246.
  2. S. Akshay, Timos Antonopoulos, Joël Ouaknine, and James Worrell. Reachability problems for Markov chains. Inf. Process. Lett., 115(2):155-158, 2015. URL: https://doi.org/10.1016/j.ipl.2014.08.013.
  3. Ana Medina Ayala, Sean B. Andersson, and Calin Belta. Formal synthesis of control policies for continuous time Markov processes from time-bounded temporal logic specifications. IEEE Trans. Automat. Contr., 59(9):2568-2573, 2014. URL: https://doi.org/10.1109/TAC.2014.2309033.
  4. Adnan Aziz, Kumud Sanwal, Vigyan Singhal, and Robert K. Brayton. Model-checking continous-time Markov chains. ACM Trans. Comput. Log., 1(1):162-170, 2000. URL: https://doi.org/10.1145/343369.343402.
  5. Christel Baier, Holger Hermanns, Joost-Pieter Katoen, and Boudewijn R. Haverkort. Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. Theor. Comput. Sci., 345(1):2-26, 2005. URL: https://doi.org/10.1016/j.tcs.2005.07.022.
  6. Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008. Google Scholar
  7. Paul C. Bell, Jean-Charles Delvenne, Raphaël M. Jungers, and Vincent D. Blondel. The continuous Skolem-Pisot problem. Theor. Comput. Sci., 411(40-42):3625-3634, 2010. URL: https://doi.org/10.1016/j.tcs.2010.06.005.
  8. Tomás Brázdil, Vojtech Forejt, Jan Krcál, Jan Kretínský, and Antonín Kucera. Continuous-time stochastic games with time-bounded reachability. Inf. Comput., 224:46-70, 2013. URL: https://doi.org/10.1016/j.ic.2013.01.001.
  9. Peter Buchholz, Ernst Moritz Hahn, Holger Hermanns, and Lijun Zhang. Model checking algorithms for CTMDPs. In Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 225-242. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22110-1_19.
  10. Peter Buchholz and Ingo Schulz. Numerical analysis of continuous time Markov decision processes over finite horizons. Comput. Oper. Res., 38(3):651-659, 2011. URL: https://doi.org/10.1016/j.cor.2010.08.011.
  11. Ventsislav Chonev, Joël Ouaknine, and James Worrell. On the Skolem problem for continuous linear dynamical systems. In 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, volume 55 of LIPIcs, pages 100:1-100:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.ICALP.2016.100.
  12. Laure Daviaud, Marcin Jurdzinski, Ranko Lazic, Filip Mazowiecki, Guillermo A. Pérez, and James Worrell. When is containment decidable for probabilistic automata? In 45th International Colloquium on Automata, Languages, and Programming, ICALP 2018, July 9-13, 2018, Prague, Czech Republic, volume 107 of LIPIcs, pages 121:1-121:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.ICALP.2018.121.
  13. John Fearnley, Markus N. Rabe, Sven Schewe, and Lijun Zhang. Efficient approximation of optimal control for continuous-time Markov games. Inf. Comput., 247:106-129, 2016. URL: https://doi.org/10.1016/j.ic.2015.12.002.
  14. Serge Lang. Introduction to transcendental numbers. Addison-Wesley series in mathematics. Addison-Wesley Pub. Co., 1966. Google Scholar
  15. Serge Lang. Transcendental numbers and Diophantine approximations. Bull. Amer. Math. Soc., 77(5):635-677, September 1971. Google Scholar
  16. Angus Macintyre. Model theory of exponentials on Lie algebras. Math. Struct. Comput. Sci., 18(1):189-204, 2008. URL: https://doi.org/10.1017/S0960129508006622.
  17. Angus Macintyre. Turing meets Schanuel. Ann. Pure Appl. Log., 167(10):901-938, 2016. URL: https://doi.org/10.1016/j.apal.2015.10.003.
  18. Angus Macintyre and Alex J. Wilkie. On the decidability of the real exponential field. In Kreiseliana. About and Around Georg Kreisel, pages 441-467. A K Peters, 1996. Google Scholar
  19. Bruce L. Miller. Finite state continuous time Markov decision processes with a finite planning horizon. SIAM Journal on Control, 6(2):266-280, 1968. Google Scholar
  20. Martin R. Neuhäußer, Mariëlle Stoelinga, and Joost-Pieter Katoen. Delayed nondeterminism in continuous-time Markov decision processes. In Foundations of Software Science and Computational Structures, 12th International Conference, FOSSACS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, volume 5504 of Lecture Notes in Computer Science, pages 364-379. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-00596-1_26.
  21. Martin R. Neuhäußer and Lijun Zhang. Time-bounded reachability probabilities in continuous-time Markov decision processes. In QEST 2010, Seventh International Conference on the Quantitative Evaluation of Systems, Williamsburg, Virginia, USA, 15-18 September 2010, pages 209-218. IEEE Computer Society, 2010. URL: https://doi.org/10.1109/QEST.2010.47.
  22. Martin R. Neuhäußer. Model checking nondeterministic and randomly timed systems. PhD thesis, Univ. Twente, Enschede, 2010. Google Scholar
  23. Jakob Piribauer and Christel Baier. On Skolem-hardness and saturation points in Markov decision processes. In ICALP, 2020. Google Scholar
  24. Markus N. Rabe and Sven Schewe. Finite optimal control for time-bounded reachability in CTMDPs and continuous-time Markov games. Acta Inf., 48(5-6):291-315, 2011. URL: https://doi.org/10.1007/s00236-011-0140-0.
  25. Markus N. Rabe and Sven Schewe. Optimal time-abstract schedulers for CTMDPs and continuous-time Markov games. Theor. Comput. Sci., 467:53-67, 2013. URL: https://doi.org/10.1016/j.tcs.2012.10.001.
  26. Mahmoud Salamati, Sadegh Soudjani, and Rupak Majumdar. A Lyapunov approach for time-bounded reachability of CTMCs and CTMDPs. ACM Transactions on Modeling and Performance Evaluation of Computing Systems (TOMPECS), 5(1):1-29, 2020. Google Scholar
  27. A. J. Wilkie. Schanuel’s conjecture and the decidability of the real exponential field. In Algebraic Model Theory, pages 223-230. Springer Netherlands, Dordrecht, 1997. Google Scholar
  28. Nicolás Wolovick and Sven Johr. A characterization of meaningful schedulers for continuous-time Markov decision processes. In Formal Modeling and Analysis of Timed Systems, 4th International Conference, FORMATS 2006, Paris, France, September 25-27, 2006, Proceedings, volume 4202 of Lecture Notes in Computer Science, pages 352-367. Springer, 2006. URL: https://doi.org/10.1007/11867340_25.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact