LIPIcs.TIME.2021.17.pdf
- Filesize: 0.83 MB
- 18 pages
Document
1½-Player Stochastic StopWatch Games
Author
Sparsa Roychowdhury 
-
Part of:
Volume:
28th International Symposium on Temporal Representation and Reasoning (TIME 2021)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Symposium on Temporal Representation and Reasoning (TIME) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2021-09-16
File
Document Identifiers
Author Details
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 AsGet 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
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)
0PDF Downloads
References
- 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.
- 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.
- 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.
-
Rajeev Alur and David L Dill. A theory of timed automata. Theoretical computer science, 126(2):183-235, 1994.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
-
Marvin L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, Inc., USA, 1967.
- 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.