Hostname: page-component-cd9895bd7-p9bg8 Total loading time: 0 Render date: 2024-12-26T20:02:50.243Z Has data issue: false hasContentIssue false
  • English
  • Français

OBLIGATION BLACKWELL GAMES AND P-AUTOMATA

Published online by Cambridge University Press:  19 June 2017

KRISHNENDU CHATTERJEE  and
NIR PITERMAN
KRISHNENDU CHATTERJEE
Affiliation:
IST AUSTRIA KLOSTERNEUBURGAUSTRIAE-mail: [email protected]
NIR PITERMAN
Affiliation:
DEPARTMENT OF INFORMATICS UNIVERSITY OF LEICESTER LEICESTER, UKE-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We generalize winning conditions in two-player games by adding a structural acceptance condition called obligations. Obligations are orthogonal to the linear winning conditions that define whether a play is winning. Obligations are a declaration that player 0 can achieve a certain value from a configuration. If the obligation is met, the value of that configuration for player 0 is 1.

We define the value in such games and show that obligation games are determined. For Markov chains with Borel objectives and obligations, and finite turn-based stochastic parity games with obligations we give an alternative and simpler characterization of the value function. Based on this simpler definition we show that the decision problem of winning finite turn-based stochastic parity games with obligations is in NP∩co-NP. We also show that obligation games provide a game framework for reasoning about p-automata.

Keywords

03B70automatatwo-player games
Type
Articles
Information
The Journal of Symbolic Logic , Volume 82 , Issue 2 , June 2017 , pp. 420 - 452
Copyright
Copyright © The Association for Symbolic Logic 2017 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

Aziz, A., Singhal, V., Balarin, F., Brayton, R., and Sangiovanni-Vincentelli, A., It usually works: The temporal logic of stochastic systems , Proceedings of the 7th International Conference on Computer Aided Verification (Wolper, P., editor), Lecture Notes in Computer Science, vol. 939, Springer, 1995, pp. 155–165.Google Scholar
Billingsley, P., Probability and Measure, Wiley, USA, 2008.Google Scholar
Castro, P., Kilmurray, C., and Piterman, N., Tractable probabilistic μ-calculus that expresses probabilistic temporal logics , 32nd Symposium on Theoretical Aspects of Computer Science (Mayr, E. W. and Ollinger, N., editors), LIPIcs, Schloss Dagstuhl, 2015, pp. 211–223.Google Scholar
Chatterjee, K., Stochastic ω-regular games, Ph.D. thesis, University of California at Berkeley, 2007.Google Scholar
Chatterjee, K., Jurdziński, M., and Henzinger, T. A., Quantitative stochastic parity games , Symposium on Discrete Algorithms (Ian Munro, J., editor), SIAM, 2004, pp. 114–123.Google Scholar
Ciesinski, F. and Baier, C., Liquor: A tool for qualitative and quantitative linear time analysis of reactive systems , Proceedings of Third International Conference on the Quantitative Evaluation of Systems (D’Argenio, P., Miner, A., and Rubino, G., editors), IEEE Computer Society, 2006, pp. 131–132.Google Scholar
Courcoubetis, C. and Yannakakis, M., The complexity of probabilistic verification . Journal of the ACM, vol. 42 (1995), no. 4, pp. 857–907.Google Scholar
Emerson, E. A. and Lei, C.-L., Modalities for model checking: Branching time logic strikes back , Proceedings of the 12th ACM Symposium on Principles of Programming Languages (Van Deusen, M. S., Galil, Z., and Reid, B. K., editors), ACM press, 1985, pp. 84–96.Google Scholar
Grädel, E., Thomas, W., and Wilke, T., Automata, Logics, and Infinite Games: A Guide to Current Research, Lecture Notes in Computer Science, vol.2500, Springer, 2002.Google Scholar
Hansson, H. and Jonsson, B., A logic for reasoning about time and reliability . Formal Aspects of Computing, vol. 6 (1994), no. 5, pp. 512–535.Google Scholar
Hart, S. and Sharir, M., Probabilistic propositional temporal logics . Information and Control, vol. 70 (1986), no. 2–3, pp. 97–155.Google Scholar
Hart, S., Sharir, M., and Pnueli, A., Termination of probabilistic concurrent programs , Proceedings of the 9th ACM Symposium on Principles of Programming Languages (DeMillo, R. A., editor), ACM press, 1982, pp. 1–6.Google Scholar
Henzinger, T. A., Kupferman, O., and Rajamani, S., Fair simulation . Information and Computation, vol. 173 (2002), no. 1, pp. 64–81.CrossRefGoogle Scholar
Hinton, A., Kwiatkowska, M. Z., Norman, G., and Parker, D., Prism: A tool for automatic verification of probabilistic systems , Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of System (Hermanns, H. and Palsberg, J., editors), Lecture Notes in Computer Science, vol. 3920, Springer, 2006, pp. 441–444.Google Scholar
Huth, M., Piterman, N., and Wagner, D., Weak p-automata: Acceptors of Markov chains , Proceedings of the 7th International Conference on Quantitative Evaluation of Systems (Ciardo, G. and Segala, R., editors), IEEE Computer Society Press, 2010 pp. 161–170.Google Scholar
Jurdziński, M., Deciding the winner in parity games is in UP ∩ co-UP . Information Processing Letters, vol. 68 (1998), no. 3, pp. 119–124.Google Scholar
Kupferman, O., Vardi, M. Y., and Wolper, P., An automata-theoretic approach to branching-time model checking . Journal of the ACM, vol. 47 (2000),no. 2, pp. 312–360.CrossRefGoogle Scholar
Laresn, K. G. and Jonsson, B., Specification and refinement of probabilistic processes , Proceedings of the 6th IEEE Symposium on logic in Computer Science (de Vrijer, R. C. and Klop, J. W., editors), IEEE Computer Society Press, 1991, pp. 266–277.Google Scholar
Larsen, K. G. and Skou, A., Bisimulation through probabilistic testing . Information and Computation, vol. 94 (1991), no. 1, pp. 1–28.CrossRefGoogle Scholar
Martin, D. A., Borel determinacy . Annals of Mathematics, vol. 65 (1975), pp. 363–371.Google Scholar
Martin, D. A., The determinacy of Blackwell games , this Journal, vol. 63 (1998), no. 4, pp. 1565–1581.Google Scholar
Mio, M., Game semantics for probabilistic μ-calculi, Ph.D. thesis, University of Edinburgh, 2012.Google Scholar
Mio, M., Probabilistic modal μ-calculus with independent product . Logical Methods in Computer Science, vol. 8 (2012), no. 4.Google Scholar
Mio, M. and Simpson, A., Łukasiewicz μ-calculus , Proceedings of Fixpoints in Computer Science (Baelde, D. and Carayol, A., editors), EPTCS, 2013, pp. 87–104.Google Scholar
Von Neumann, J., Zur theorie der gesellschaftsspiele . Mathematische Annalen, vol. 100 (1928), no. 1, pp. 295–320.CrossRefGoogle Scholar
Royden, H. L. and Fitzpatrick, P., Real Analysis, Prentice Hall, 2010.Google Scholar
Thomas, W., Languages, automata, and logic , Handbook of Formal Language Theory, vol. III (Rozenberg, G. and Salomaa, A., editors), Springer, 1997, pp. 389–455.CrossRefGoogle Scholar
Vardi, M. Y., Automatic verification of probabilistic concurrent finite-state programs , Proceedings of the 26th IEEE Symposium on Foundations of Computer Science (Blum, M., Hopcroft, J., Lagarias, J., Leighton, T., Rackoff, C., Ruzzo, L.. Stockmeyer, L., Tarjan, B., and Yao, F., editors), IEEE, 1985, pp. 327–338.Google Scholar