Abstract
Several problems in planning and reactive synthesis can be reduced to the analysis of two-player quantitative graph games. Optimization is one form of analysis. We argue that in many cases it may be better to replace the optimization problem with the satisficing problem, where instead of searching for optimal solutions, the goal is to search for solutions that adhere to a given threshold bound.
This work defines and investigates the satisficing problem on a two-player graph game with the discounted-sum cost model. We show that while the satisficing problem can be solved using numerical methods just like the optimization problem, this approach does not render compelling benefits over optimization. When the discount factor is, however, an integer, we present another approach to satisficing, which is purely based on automata methods. We show that this approach is algorithmically more performant – both theoretically and empirically – and demonstrates the broader applicability of satisficing over optimization.
Chapter PDF
Similar content being viewed by others
References
Satisficing. https://en.wikipedia.org/wiki/Satisficing.
GMP. https://gmplib.org/.
B. Alpern and F. B. Schneider. Recognizing safety and liveness. Distributed computing, 2(3):117–126, 1987.
C. Baier. Probabilistic model checking. In Dependable Software Systems Engineering, pages 1–23. 2016.
S. Bansal, S. Chaudhuri, and M. Y. Vardi. Automata vs linear-programming discounted-sum inclusion. In Proc. of International Conference on Computer-Aided Verification (CAV), 2018.
S. Bansal, S. Chaudhuri, and M. Y. Vardi. Comparator automata in quantitative verification. In Proc. of International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), 2018.
S. Bansal, S. Chaudhuri, and M. Y. Vardi. Comparator automata in quantitative verification (full version). CoRR, abs/1812.06569, 2018.
S. Bansal, Y. Li, L. Tabajara, and M. Y. Vardi. Hybrid compositional reasoning for reactive synthesis from finite-horizon specifications. In Proc. of AAAI, 2020.
S. Bansal and M. Y. Vardi. Safety and co-safety comparator automata for discounted-sum inclusion. In Proc. of International Conference on Computer-Aided Verification (CAV), 2019.
J. Bernet, D. Janin, and I. Walukiewicz. Permissive strategies: from parity games to safety games. RAIRO-Theoretical Informatics and Applications-Informatique Théorique et Applications, 36(3):261–275, 2002.
R. Bloem, K. Chatterjee, T. Henzinger, and B. Jobstmann. Better quality in synthesis through quantitative objectives. In Proc. of CAV, pages 140–156. Springer, 2009.
U. Boker and T. A. Henzinger. Exact and approximate determinization of discounted-sum automata. LMCS, 10(1), 2014.
K. Chatterjee, T. A. Henzinger, J. Otop, and Y. Velner. Quantitative fair simulation games. Information and Computation, 254:143–166, 2017.
D. Clark, S. Hunt, and P. Malacaria. A static analysis for quantifying information flow in a simple imperative language. Journal of Computer Security, 15(3):321–371, 2007.
T. Colcombet and N. Fijalkow. Universal graphs and good for games automata: New tools for infinite duration games. In Proc. of FSTTCS, pages 1–26. Springer, 2019.
B. Finkbeiner, C. Hahn, and H. Torfah. Model checking quantitative hyperproperties. In Proc. of CAV, pages 144–163. Springer, 2018.
T. D. Hansen, P. B. Miltersen, and U. Zwick. Strategy iteration is strongly polynomial for 2-player turn-based stochastic games with a constant discount factor. Journal of the ACM, 60, 2013.
K. He, M. Lahijanian, L. Kavraki, and M. Vardi. Reactive synthesis for finite tasks under resource constraints. In Intelligent Robots and Systems (IROS), 2017 IEEE/RSJ International Conference on, pages 5326–5332. IEEE, 2017
O. Kupferman and M. Y. Vardi. Model checking of safety properties. In Proc. of CAV, pages 172–183. Springer, 1999.
M. Kwiatkowska. Quantitative verification: Models, techniques and tools. In Proc. 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), pages 449–458. ACM Press, September 2007.
M. Kwiatkowska, G. Norman, and D. Parker. Advances and challenges of probabilistic model checking. In 2010 48th Annual Allerton Conference on Communication, Control, and Computing (Allerton), pages 1691–1698. IEEE, 2010.
M. Lahijanian, S. Almagor, D. Fried, L. Kavraki, and M. Vardi. This time the robot settles for a cost: A quantitative approach to temporal logic planning with partial satisfaction. In AAAI, pages 3664–3671, 2015
M. L. Littman. Algorithms for sequential decision making. Brown University Providence, RI, 1996.
M. Osborne and A. Rubinstein. A course in game theory. MIT press, 1994.
M. Puterman. Markov decision processes. Handbooks in operations research and management science, 2:331–434, 1990.
S. A. Seshia, A. Desai, T. Dreossi, D. J. Fremont, S. Ghosh, E. Kim, S. Shivakumar, M. Vazquez-Chanlatte, and X. Yue. Formal specification for deep neural networks. In Proc. of ATVA, pages 20–34. Springer, 2018.
L. S. Shapley. Stochastic games. Proceedings of the National Academy of Sciences of the United States of America, 39(10):1095, 1953.
R. Sutton and A. Barto. Introduction to reinforcement learning, volume 135. MIT press Cambridge, 1998.
L. M. Tabajara and M. Y. Vardi. Partitioning techniques in LTLf synthesis. In IJCAI, pages 5599–5606. AAAI Press, 2019.
W. Thomas, T. Wilke, et al. Automata, logics, and infinite games: A guide to current research, volume 2500. Springer Science & Business Media, 2002.
M. Wen, R. Ehlers, and U. Topcu. Correct-by-synthesis reinforcement learning with temporal logic constraints. In 2015 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pages 4983–4990. IEEE, 2015.
U. Zwick and M. Paterson. The complexity of mean payoff games on graphs. Theoretical Computer Science, 158(1):343–359, 1996.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2021 The Author(s)
About this paper
Cite this paper
Bansal, S., Chatterjee, K., Vardi, M.Y. (2021). On Satisficing in Quantitative Games. In: Groote, J.F., Larsen, K.G. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2021. Lecture Notes in Computer Science(), vol 12651. Springer, Cham. https://doi.org/10.1007/978-3-030-72016-2_2
Download citation
DOI: https://doi.org/10.1007/978-3-030-72016-2_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-72015-5
Online ISBN: 978-3-030-72016-2
eBook Packages: Computer ScienceComputer Science (R0)