Abstract
Gist is a tool that (a) solves the qualitative analysis problem of turn-based probabilistic games with ω-regular objectives; and (b) synthesizes reasonable environment assumptions for synthesis of unrealizable specifications. Our tool provides the first and efficient implementations of several reduction-based techniques to solve turn-based probabilistic games, and uses the analysis of turn-based probabilistic games for synthesizing environment assumptions for unrealizable specifications.
This research was supported by the European Union project COMBEST and the European Network of Excellence ArtistDesign.
Chapter PDF
Similar content being viewed by others
Keywords
- Game Graph
- Parity Objective
- Fairness Assumption
- Probabilistic Transition Function
- Environment Assumption
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Chatterjee, K.: Stochastic ω-Regular Games. PhD thesis, UC Berkeley (2007)
Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Environment assumptions for synthesis. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 147–161. Springer, Heidelberg (2008)
Chatterjee, K., Henzinger, T.A., Jobstmann, B., Radhakrishna, A.: Gist: A solver for probabilistic games. CoRR, abs/1004.2367 (2010)
Chatterjee, K., Jurdziński, M., Henzinger, T.A.: Quantitative stochastic parity games. In: Ian Munro, J. (ed.) Proceedings of the Fifteenth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2004, New Orleans, Louisiana, USA, January 11-14. SIAM, Philadelphia (2004)
Gurevich, Y., Harrington, L.: Trees, automata, and games. In: STOC ’82: Proceedings of the fourteenth annual ACM symposium on Theory of computing, San Francisco, California, United States, pp. 60–65. ACM Press, New York (1982) ISBN: 0-89791-070-2, http://doi.acm.org/10.1145/800070.802177
Lange, M., Friedmann, O.: The pgsolver collection of parity game solvers. Technical report, Institut für Informatik, Ludwig-Maximilians-Universität (2009)
Tsay, Y., Chen, Y., Tsai, M., Chan, W., Luo, C.: Goal extended: Towards a research tool for omega automata and temporal logic. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 346–350. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chatterjee, K., Henzinger, T.A., Jobstmann, B., Radhakrishna, A. (2010). Gist: A Solver for Probabilistic Games. In: Touili, T., Cook, B., Jackson, P. (eds) Computer Aided Verification. CAV 2010. Lecture Notes in Computer Science, vol 6174. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14295-6_57
Download citation
DOI: https://doi.org/10.1007/978-3-642-14295-6_57
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14294-9
Online ISBN: 978-3-642-14295-6
eBook Packages: Computer ScienceComputer Science (R0)