Document Open Access Logo

Stochastic Timed Games Revisited

Authors S. Akshay, Patricia Bouyer, Shankara Narayanan Krishna, Lakshmi Manasa, Ashutosh Trivedi

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2016.8.pdf
  • Filesize: 0.6 MB
  • 14 pages

Document Identifiers

Subject Classification

Keywords
  • timed automata
  • stochastic games
  • two-counter machines

Metrics

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

Abstract

Stochastic timed games (STGs), introduced by Bouyer and Forejt, naturally generalize both continuous-time Markov chains and timed automata by providing a partition of the locations between those controlled by two players (Player Box and Player Diamond) with competing objectives and those governed by stochastic laws. Depending on the number of players - 2, 1, or 0 - subclasses of stochastic timed games are often classified as 2 1/2-player, 1 1/2-player, and 1/2-player games where the 1/2 symbolizes the presence of the stochastic "nature" player. For STGs with reachability objectives it is known that 1 1/2-player one-clock STGs are decidable for qualitative objectives, and that 2 1/2-player three-clock STGs are undecidable for quantitative reachability objectives. This paper further refines the gap in this decidability spectrum. We show that quantitative reachability objectives are already undecidable for 1 1/2 player four-clock STGs, and even under the time-bounded restriction for  2 1/2-player five-clock STGs. We also obtain a class of 1 1/2, 2 1/2 player STGs for which the quantitative reachability problem is decidable.

Cite As Get BibTex

S. Akshay, Patricia Bouyer, Shankara Narayanan Krishna, Lakshmi Manasa, and Ashutosh Trivedi. Stochastic Timed Games Revisited. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 8:1-8:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.MFCS.2016.8

Author Details

S. Akshay
Patricia Bouyer
Shankara Narayanan Krishna
Lakshmi Manasa
Ashutosh Trivedi

References

  1. S. Akshay, P. Bouyer, S. N. Krishna, L. Manasa, and A. Trivedi. Stochastic timed games revisited. http://www.cse.iitb.ac.in/~krishnas/TR16.pdf.
  2. R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994. Google Scholar
  3. E. Asarin, O. Maler, A. Pnueli, and J. Sifakis. Controller synthesis for timed automata. In Proc. of IFAC Symposium on System Structure and Control, pages 469-474. Elsevier, 1998. Google Scholar
  4. C. Baier, P. Bouyer, T. Brihaye, and M. Größer. Almost-sure model checking of infinite paths in one-clock timed automata. In Proc. 23rd Annual Symposium on Logic in Computer Science (LICS'08), pages 217-226. IEEE Computer Society Press, 2008. Google Scholar
  5. C. Baier, B. Haverkort, H. Hermanns, and J.-P. Katoen. Model-checking algorithms for continuous-time Markov chains. IEEE Transactions on Software Engineering, 29(7):524-541, 2003. Google Scholar
  6. C Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, 2008. Google Scholar
  7. N. Bertrand, P. Bouyer, T. Brihaye, and P. Carlier. Analysing decisive stochastic processes. In Proc. 43rd International Colloquium on Automata, Languages and Programming (ICALP'16) - Part II, Leibniz International Proceedings in Informatics. Leibniz-Zentrum für Informatik, July 2016. To appear. Google Scholar
  8. N. Bertrand, P. Bouyer, T. Brihaye, and N. Markey. Quantitative model-checking of one-clock timed automata under probabilistic semantics. In Proc. 5th International Conference on Quantitative Evaluation of Systems (QEST'08). IEEE Computer Society Press, 2008. Google Scholar
  9. N. Bertrand, P. Bouyer, T. Brihaye, Q. Menet, M. Größer, and M. Jurdziński. Stochastic timed automata. Logical Methods in Computer Science, 10(4):1-73, 2014. Google Scholar
  10. N. Bertrand, T. Brihaye, and B. Genest. Deciding the value 1 problem for reachability in 1-clock decision stochastic timed automata. In Proc. 11th International Conference on Quantitative Evaluation of Systems (QEST'14), pages 313-328. IEEE Computer Society Press, 2014. Google Scholar
  11. H.C. Bohnenkamp, P.R. D'Argenio, H. Hermanns, and J.-P. Katoen. MODEST: A compositional modeling formalism for hard and softly timed systems. IEEE Transactions on Software Engineering, 32(10):812-830, 2006. Google Scholar
  12. P. Bouyer and V. Forejt. Reachability in stochastic timed games. In Proc. 36th International Colloquium on Automata, Languages and Programming (ICALP'09), volume 5556 of LNCS, pages 103-114. Springer, 2009. Google Scholar
  13. Tomáš Brázdil, Jan Krčál, Jan Křetínský, and Vojtěch Řehák. Fixed-delay events in generalized semi-Markov processes revisited. In Proc. 22nd International Conference on Concurrency Theory (CONCUR'11), volume 6901 of LNCS, pages 140-155. Springer, 2011. Google Scholar
  14. T. Brihaye, G. Geeraerts, S. N. Krishna, L. Manasa, B. Monmege, and A. Trivedi. Adding negative prices to priced timed games. In Proc. 25th International Conference on Concurrency Theory (CONCUR'14), LIPIcs, pages 560-575. Leibniz-Zentrum für Informatik, 2014. Google Scholar
  15. J. Filar and K. Vrieze. Competitive Markov Decision Processes. Springer, 1997. Google Scholar
  16. V. Forejt, M. Kwiatkowska, G. Norman, and A. Trivedi. Expected reachability-time games. In Proc. 8th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'10), volume 6246 of LNCS, pages 122-136. Springer, 2010. Google Scholar
  17. M. Kwiatkowska, G. Norman, R. Segala, and J. Sproston. Verifying quantitative properties of continuous probabilistic timed automata. In Proc. of 11th International Conference on Concurrency Theorey, (CONCUR'00), volume 1877 of LNCS, pages 123-137. Springer, 2000. Google Scholar
  18. M. Kwiatkowska, G. Norman, R. Segala, and J. Sproston. Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science, 282(1):101-150, June 2002. Google Scholar
  19. F. Laroussinie, N. Markey, and P. Schnoebelen. Model checking timed automata with one or two clocks. In Proc. 15th International Conference on Concurrency Theory (CONCUR'04), volume 3170 of LNCS, pages 387-401. Springer, 2004. Google Scholar
  20. J. Ouaknine, A. Rabinovich, and J. Worrell. Time-bounded verification. In Proc. 20th International Conference on Concurrency Theory (CONCUR'09), volume 5710 of LNCS, pages 496-510. Springer, 2009. Google Scholar
  21. J. Ouaknine and J. Worrell. Towards a theory of time-bounded verification. In Proc. 37th International Colloquium on Automata, Languages and Programming (ICALP'10), volume 6199 of LNCS, pages 22-37. Springer, 2010. Google Scholar
  22. M. L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, 1994. Google Scholar
  23. Uppaal case-studies. http://www.it.uu.se/research/group/darts/uppaal/examples.shtml.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact