Termination criteria for solving concurrent safety and reachability games

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Termination criteria for solving concurrent safety and reachability games

Full text

Pdf (452 KB)

Source

Symposium on Discrete Algorithms archive
Proceedings of the Nineteenth Annual ACM -SIAM Symposium on Discrete Algorithms table of contents

New York, New York

Pages 197-206

Year of Publication: 2009

Authors

Krishnendu Chatterjee	CE, UC Santa Cruz
Luca de Alfaro	CE, UC Santa Cruz
Thomas A. Henzinger	UC Berkeley, and EPFL, Switzerland

Publisher

Society for Industrial and Applied Mathematics Philadelphia, PA, USA

Bibliometrics

Downloads (6 Weeks): n/a, Downloads (12 Months): n/a, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

ABSTRACT

We consider concurrent games played on graphs. At every round of a game, each player simultaneously and independently selects a move; the moves jointly determine the transition to a successor state. Two basic objectives are the safety objective to stay forever in a given set of states, and its dual, the reachability objective to reach a given set of states. We present in this paper a strategy improvement algorithm for computing the value of a concurrent safety game, that is, the maximal probability with which player 1 can enforce the safety objective. The algorithm yields a sequence of player-1 strategies which ensure probabilities of winning that converge monotonically to the value of the safety game.

Our result is significant because the strategy improvement algorithm provides, for the first time, a way to approximate the value of a concurrent safety game from below. Since a value iteration algorithm, or a strategy improvement algorithm for reachability games, can be used to approximate the same value from above, the combination of both algorithms yields a method for computing a converging sequence of upper and lower bounds for the values of concurrent reachability and safety games. Previous methods could approximate the values of these games only from one direction, and as no rates of convergence are known, they did not provide a practical way to solve these games.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Dimitri P. Bertsekas, Dynamic Programming and Optimal Control, Athena Scientific, 1995
	2	Krishnendu Chatterjee , Luca de Alfaro , Thomas A. Henzinger, Strategy Improvement for Concurrent Reachability Games, Proceedings of the 3rd international conference on the Quantitative Evaluation of Systems, p.291-300, September 11-14, 2006 [doi>10.1109/QEST.2006.48]
	3	K. Chatterjee, L. de Alfaro, and T. A. Henzinger. Termination criteria for solving concurrent safety and reachability games. CoRR, abs/0809.4017, 2008.
	4	K. Chatterjee, M. Jurdziński, and T. A. Henzinger. Simple stochastic parity games. In CSL'03: Computer Science Logic, volume 2803 of LNCS, pages 100--113. Springer, 2003.
	5	Anne Condon, The complexity of stochastic games, Information and Computation, v.96 n.2, p.203-224, Feb. 1992 [doi>10.1016/0890-5401(92)90048-K]
	6	A. Condon. On algorithms for simple stochastic games. In Advances in Computational Complexity Theory, volume 13 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 51--73. American Mathematical Society, 1993.
	7	Luca de Alfaro , Thomas A. Henzinger, Concurrent Omega-Regular Games, Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, p.141, June 26-29, 2000
	8	Luca de Alfaro , Thomas A. Henzinger , Orna Kupferman, Concurrent reachability games, Theoretical Computer Science, v.386 n.3, p.188-217, October 2007 [doi>10.1016/j.tcs.2007.07.008]
	9	Luca de Alfaro , Rupak Majumdar, Quantitative solution of omega-regular games, Journal of Computer and System Sciences, v.68 n.2, p.374-397, March 2004 [doi>10.1016/j.jcss.2003.07.009]
	10	Cyrus Derman, Finite State Markovian Decision Processes, Academic Press, Inc., Orlando, FL, 1970
	11	K. Etessami and M. Yannakakis. Recursive concurrent stochastic games. In ICALP 06: Automata, Languages, and Programming, volume 4052 of LNCS, pages 324--335. Springer, 2006.
	12	Jerzy Filar , Koos Vrieze, Competitive Markov decision processes, Springer-Verlag New York, Inc., New York, NY, 1996
	13	H. Gimbert and F. Horn. Simple stochastic games with few random vertices are easy to solve. In FoSSaCS'08: Foundations of Software Science and Computational Structures, volume 4962 of LNCS, pages 5--19, 2008.
	14	P. R. Kumar and T. H. Shiau. Existence of value and randomized strategies in zero-sum discrete-time stochastic dynamic games. SIAM J. Control and Optimization, 19(5):617--634, 1981.
	15	D. A. Martin. The determinacy of Blackwell games. The Journal of Symbolic Logic, 63(4):1565--1581, 1998.
	16	Uri Zwick , Mike Paterson, The complexity of mean payoff games on graphs, Theoretical Computer Science, v.158 n.1-2, p.343-359, May 20, 1996 [doi>10.1016/0304-3975(95)00188-3]