Document Open Access Logo

1½-Player Stochastic StopWatch Games

Author Sparsa Roychowdhury

PDF
Thumbnail PDF

File

LIPIcs.TIME.2021.17.pdf
  • Filesize: 0.83 MB
  • 18 pages

Document Identifiers

Author Details

Sparsa Roychowdhury
  • Indian Institute of Technology Bombay, Mumbai, India

Acknowledgements

The author thanks Prof. Krishna S. of IIT Bombay, India for insightful discussions, suggestions and encouragement towards this work. The open access publication of this article was supported by the Alpen-Adria-Universität Klagenfurt, Austria.

Cite As Get BibTex

Sparsa Roychowdhury. 1½-Player Stochastic StopWatch Games. In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 17:1-17:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.TIME.2021.17

Abstract

Stochastic timed games (STGs), introduced by Bouyer and Forejt, generalize continuous-time Markov chains and timed automata. Depending on the number of players - 2, 1, or 0 - subclasses of stochastic timed games are classified as 2½-player, 1½-player, and ½-player games where the ½ symbolizes the presence of the stochastic player. The qualitative and quantitative reachability problem for STGs was studied in [Patricia Bouyer and Vojtech Forejt, 2009] and [S. Akshay et al., 2016]. In this paper, we introduce stochastic stopwatch games (SSG), an extension of (STG) from clocks to stopwatches. We focus on 1½-player SSGs and prove that with two variables which can be either a clock or a stopwatch, qualitative reachability is decidable, whereas, if we increase the number of variables to three, with at least one stopwatch, the problem becomes undecidable.

Subject Classification

ACM Subject Classification
  • Theory of computation → Timed and hybrid models
Keywords
  • Timed Automata
  • Stopwatches
  • Stochastic Timed Games

Metrics

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

References

  1. S. Akshay, Patricia Bouyer, Shankara Narayanan Krishna, Lakshmi Manasa, and Ashutosh Trivedi. Stochastic Timed Games Revisited. In Piotr Faliszewski, Anca Muscholl, and Rolf Niedermeier, editors, 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016), volume 58 of Leibniz International Proceedings in Informatics (LIPIcs), pages 8:1-8:14, Dagstuhl, Germany, 2016. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.MFCS.2016.8.
  2. R. Alur, C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138(1):3-34, February 1995. URL: https://doi.org/10.1016/0304-3975(94)00202-t.
  3. Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger, and Pei Hsin Ho. Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In Hybrid Systems, pages 209-229. Springer Berlin Heidelberg, 1993. URL: https://doi.org/10.1007/3-540-57318-6_30.
  4. Rajeev Alur and David L Dill. A theory of timed automata. Theoretical computer science, 126(2):183-235, 1994. Google Scholar
  5. Eugene Asarin, Oded Maler, Amir Pnueli, and Joseph Sifakis. Controller synthesis for timed automata. IFAC Proceedings Volumes, 31(18):447-452, 1998. URL: https://doi.org/10.1016/S1474-6670(17)42032-5.
  6. C. Baier, B. Haverkort, H. Hermanns, and J.-P. Katoen. Model-checking algorithms for continuous-time markov chains. IEEE Transactions on Software Engineering, 29(6):524-541, June 2003. URL: https://doi.org/10.1109/tse.2003.1205180.
  7. Christel Baier, Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, and Marcus Größer. Probabilistic and topological semantics for timed automata. In FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science, pages 179-191. Springer Berlin Heidelberg, 2007. URL: https://doi.org/10.1007/978-3-540-77050-3_15.
  8. Christel Baier, Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, and Marcus Grosser. Almost-sure model checking of infinite paths in one-clock timed automata. In 2008 23rd Annual IEEE Symposium on Logic in Computer Science. IEEE, June 2008. URL: https://doi.org/10.1109/lics.2008.25.
  9. Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, Quentin Menet, Christel Baier, Marcus Groesser, and Marcin Jurdzinski. Stochastic timed automata. Logical Methods in Computer Science, 10(4), December 2014. URL: https://doi.org/10.2168/lmcs-10(4:6)2014.
  10. Patricia Bouyer and Vojtech Forejt. Reachability in stochastic timed games. In ICALP, pages 103-114. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02930-1_9.
  11. Thomas Brihaye, Véronique Bruyère, and Jean-François Raskin. On model-checking timed automata with stopwatch observers. Information and Computation, 204(3):408-433, 2006. URL: https://doi.org/10.1016/j.ic.2005.12.001.
  12. Thomas Brihaye, Laurent Doyen, Gilles Geeraerts, Joel Ouaknine, Jean-Francois Raskin, and James Worrell. Time-bounded reachability for monotonic hybrid automata: Complexity and fixed points. In Automated Technology for Verification and Analysis, pages 55-70. Springer International Publishing, 2013. URL: https://doi.org/10.1007/978-3-319-02444-8_6.
  13. Franck Cassez and Kim Larsen. The impressive power of stopwatches. In CONCUR 2000 - Concurrency Theory, pages 138-152. Springer Berlin Heidelberg, 2000. URL: https://doi.org/10.1007/3-540-44618-4_12.
  14. Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, and Pravin Varaiya. Whatquotesingles decidable about hybrid automata? Journal of Computer and System Sciences, 57(1):94-124, August 1998. URL: https://doi.org/10.1006/jcss.1998.1581.
  15. Marcin Jurdzinski, Jeremy Sproston, and Francois Laroussinie. Model checking probabilistic timed automata with one or two clocks. Logical Methods in Computer Science, 4(3), September 2008. URL: https://doi.org/10.2168/lmcs-4(3:12)2008.
  16. Shankara Narayanan Krishna, Umang Mathur, and Ashutosh Trivedi. Weak singular hybrid automata. In Lecture Notes in Computer Science, pages 161-175. Springer International Publishing, 2014. URL: https://doi.org/10.1007/978-3-319-10512-3_12.
  17. Marta Kwiatkowska, Gethin Norman, Roberto Segala, and Jeremy Sproston. Verifying quantitative properties of continuous probabilistic timed automata. In CONCUR 2000 - Concurrency Theory, pages 123-137. Springer Berlin Heidelberg, 2000. URL: https://doi.org/10.1007/3-540-44618-4_11.
  18. Marta Kwiatkowska, Gethin Norman, Roberto Segala, and Jeremy Sproston. Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science, 282(1):101-150, June 2002. URL: https://doi.org/10.1016/s0304-3975(01)00046-9.
  19. Marvin L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, Inc., USA, 1967. Google Scholar
  20. Nima Roohi and Mahesh Viswanathan. Time-bounded reachability for initialized hybrid automata with linear differential inclusions and rectangular constraints. In Lecture Notes in Computer Science, pages 191-205. Springer International Publishing, 2014. URL: https://doi.org/10.1007/978-3-319-10512-3_14.
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 About DROPS Imprint Privacy Contact