Quantitative solution of omega-regular games380872

ABSTRACT

We consider two-player games played for an infinite number of rounds, with &ohgr;-regular winning conditions. The games may be concurrent, in that the players choose their moves simultaneously and independently, and probabilistic, in that the moves determine a probability distribution for the successor state. We introduce quantitative game &mgr;-calculus, and we show that the maximal probability of winning such games can be expressed as the fixpoint formulas in this calculus. We develop the arguments both for deterministic and for probabilistic concurrent games; as a special case, we solve probabilistic turn-based games with &ohgr;-regular winning conditions, which was also open. We also characterize the optimality, and the memory requirements, of the winning strategies. In particular, we show that while memoryless strategies suffice for winning games with safety and reachability conditions, Büchi conditions require the use of strategies with infinite memory. The existence of optimal strategies, as opposed to &egr;-optimal, is only guaranteed in games with safety winning conditions.

REFERENCES

• 1: Dimitri P. Bertsekas, Dynamic Programming and Optimal Control, Athena Scientific, 1995
• 2: [2] J. Büchi and L. Landweber. Solving sequential conditions by finite-state strategies. Trans. Amer. Math. Soc., 138:295-311, 1969.
• 3: J. R. Burch , E. M. Clarke , K. L. McMillan , David L. Dill, Sequential circuit verification using symbolic model checking, Proceedings of the 27th ACM/IEEE conference on Design automation, p.46-51, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.123223]
• 4: [4] E. Clarke, M. Fujita, and X. Zhao. Multi-Terminal Binary Decision Diagrams and Hybrid Decision Diagrams, Representations of Discrete Functions, pages 93-108. Kluwer Academic Publishers, 1996.
• 5: Costas Courcoubetis , Mihalis Yannakakis, Markov decision processes and regular events, Proceedings of the seventeenth international colloquium on Automata, languages and programming, p.336-349, July 1990, Warwick University, England
• 6: 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
• 7: Luca de Alfaro , Marta Z. Kwiatkowska , Gethin Norman , David Parker , Roberto Segala, Symbolic Model Checking of Probabilistic Processes Using MTBDDs and the Kronecker Representation, Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems: Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, p.395-410, March 25-April 02, 2000
• 8: E. A. Emerson , C. S. Jutla, Tree automata, Mu-Calculus and determinacy, Proceedings of the 32nd annual symposium on Foundations of computer science, p.368-377, September 1991, San Juan, Puerto Rico [doi>10.1109/SFCS.1991.185392]
• 9: [9] H. Everett. Recursive games. In Contributions to the Theory of Games III, volume 39 of Annals of Mathematical Studies, pages 47-78, 1957.
• 10: Jerzy Filar , Koos Vrieze, Competitive Markov decision processes, Springer-Verlag New York, Inc., New York, NY, 1996
• 11: Yuri Gurevich , Leo Harrington, Trees, automata, and games, Proceedings of the fourteenth annual ACM symposium on Theory of computing, p.60-65, May 05-07, 1982, San Francisco, California, United States [doi>10.1145/800070.802177]
• 12: Michael Huth , Marta Kwiatkowska, Quantitative Analysis and Model Checking, Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, p.111, June 29-July 02, 1997
• 13: Dexter Kozen, A probabilistic PDL, Proceedings of the fifteenth annual ACM symposium on Theory of computing, p.291-297, December 1983 [doi>10.1145/800061.808758]
• 14: [14] D. Kozen. Results on the propositional µ-calculus. Theoretical Computer Science, 27(3):333-354, 1983.
• 15: [15] P. Kumar and T. 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.
• 16: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 17: [17] D. Martin. The determinacy of Blackwell games. The Journal of Symbolic Logic, 63(4):1565-1581, 1998.
• 18: [18] A. McIver. Reasoning about efficiency within a probabilitic µ-calculus. In Proc. of PROBMIV, pages 45-58, 1998. Technical Report CSR-98-4, University of Birmingham, School of Computer Science.
• 19: [19] R. McNaughton. Infinite games played on finite graphs. Ann. Pure Appl. Logic, 65:149-184, 1993.
• 20: Carroll Morgan , Annabelle McIver , Karen Seidel, Probabilistic predicate transformers, ACM Transactions on Programming Languages and Systems (TOPLAS), v.18 n.3, p.325-353, May 1996 [doi>10.1145/229542.229547]
• 21: [21] A. Mostowski. Regular expressions for infinite trees and a standard form of automata. In Computation Theory, volume 208 of Lect. Notes in Comp. Sci., pages 157-168. Springer-Verlag, 1984.
• 22: [22] D. Ornstein. On the existence of stationary optimal strategies. Proc. Am. Math. Soc., 20:563-569, 1969.
• 23: [23] G. Owen. Game Theory. Academic Press, 1995.
• 24: [24] T. Raghavan and J. Filar. Algorithms for stochastic games -- a survey. ZOR -- Methods and Models of Op. Res., 35:437-472, 1991.
• 25: [25] L. Shapley. Stochastic games. Proc. Nat. Acad. Sci. USA, 39:1095-1100, 1953.
• 26: [26] W. Thomas. On the synthesis of strategies in infinite games. In Proc. of 12th Annual Symp. on Theor. Asp. of Comp. Sci., volume 900 of Lect. Notes in Comp. Sci., pages 1-13. Springer-Verlag, 1995.
• 27: [27] F. Thuijsman and O. Vrieze. The bad match, a total reward stochastic game. Operations Research Spektrum, 9:93-99, 1987.
• 28: [28] M. Vardi. Automatic verification of probabilistic concurrent finite-state systems. In Proc. 26th IEEE Symp. Found. of Comp. Sci., pages 327-338. IEEE Computer Society Press, 1985.
• 29: [29] J. von Neumann and O. Morgenstern. Theory of games and economic behavior. Princeton University Press, 1947.
• 30: [30] D. Williams. Probability With Martingales. Cambridge University Press, 1991.

INDEX TERMS

Primary Classification:
  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS

Additional Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Computations on discrete structures

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.1 Applications and Expert Systems
          Subjects: Games

General Terms:
Performance, Reliability, Theory, Verification