{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:06:12Z","timestamp":1742911572767,"version":"3.40.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030720155"},{"type":"electronic","value":"9783030720162"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,20]],"date-time":"2021-03-20T00:00:00Z","timestamp":1616198400000},"content-version":"vor","delay-in-days":78,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Several problems in planning and reactive synthesis can be reduced to the analysis of two-player quantitative graph games.<jats:italic>Optimization<\/jats:italic>is one form of analysis. We argue that in many cases it may be better to replace the optimization problem with the<jats:italic>satisficing problem<\/jats:italic>, where instead of searching for optimal solutions, the goal is to search for solutions that adhere to a given threshold bound.<\/jats:p><jats:p>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 \u2013 both theoretically and empirically \u2013 and demonstrates the broader applicability of satisficing over optimization.<\/jats:p>","DOI":"10.1007\/978-3-030-72016-2_2","type":"book-chapter","created":{"date-parts":[[2021,3,19]],"date-time":"2021-03-19T22:03:37Z","timestamp":1616191417000},"page":"20-37","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["On Satisficing in Quantitative Games"],"prefix":"10.1007","author":[{"given":"Suguman","family":"Bansal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Krishnendu","family":"Chatterjee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,3,20]]},"reference":[{"key":"2_CR1","unstructured":"Satisficing. https:\/\/en.wikipedia.org\/wiki\/Satisficing."},{"key":"2_CR2","unstructured":"GMP. https:\/\/gmplib.org\/."},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"B.\u00a0Alpern and F.\u00a0B. Schneider. Recognizing safety and liveness. Distributed computing, 2(3):117\u2013126, 1987.","DOI":"10.1007\/BF01782772"},{"key":"2_CR4","unstructured":"C.\u00a0Baier. Probabilistic model checking. In Dependable Software Systems Engineering, pages 1\u201323. 2016."},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"S.\u00a0Bansal, S.\u00a0Chaudhuri, and M.\u00a0Y. Vardi. Automata vs linear-programming discounted-sum inclusion. In Proc. of International Conference on Computer-Aided Verification (CAV), 2018.","DOI":"10.1007\/978-3-319-96142-2_9"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"S.\u00a0Bansal, S.\u00a0Chaudhuri, and M.\u00a0Y. Vardi. Comparator automata in quantitative verification. In Proc. of International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), 2018.","DOI":"10.1007\/978-3-319-89366-2_23"},{"key":"2_CR7","unstructured":"S.\u00a0Bansal, S.\u00a0Chaudhuri, and M.\u00a0Y. Vardi. Comparator automata in quantitative verification (full version). CoRR, abs\/1812.06569, 2018."},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"S.\u00a0Bansal, Y.\u00a0Li, L.\u00a0Tabajara, and M.\u00a0Y. Vardi. Hybrid compositional reasoning for reactive synthesis from finite-horizon specifications. In Proc. of AAAI, 2020.","DOI":"10.1609\/aaai.v34i06.6528"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"S.\u00a0Bansal and M.\u00a0Y. Vardi. Safety and co-safety comparator automata for discounted-sum inclusion. In Proc. of International Conference on Computer-Aided Verification (CAV), 2019.","DOI":"10.1007\/978-3-030-25540-4_4"},{"key":"2_CR10","unstructured":"J.\u00a0Bernet, D.\u00a0Janin, and I.\u00a0Walukiewicz. Permissive strategies: from parity games to safety games. RAIRO-Theoretical Informatics and Applications-Informatique Th\u00e9orique et Applications, 36(3):261\u2013275, 2002."},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"R.\u00a0Bloem, K.\u00a0Chatterjee, T.\u00a0Henzinger, and B.\u00a0Jobstmann. Better quality in synthesis through quantitative objectives. In Proc. of CAV, pages 140\u2013156. Springer, 2009.","DOI":"10.1007\/978-3-642-02658-4_14"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"U.\u00a0Boker and T.\u00a0A. Henzinger. Exact and approximate determinization of discounted-sum automata. LMCS, 10(1), 2014.","DOI":"10.2168\/LMCS-10(1:10)2014"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"K.\u00a0Chatterjee, T.\u00a0A. Henzinger, J.\u00a0Otop, and Y.\u00a0Velner. Quantitative fair simulation games. Information and Computation, 254:143\u2013166, 2017.","DOI":"10.1016\/j.ic.2016.10.006"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"D.\u00a0Clark, S.\u00a0Hunt, and P.\u00a0Malacaria. A static analysis for quantifying information flow in a simple imperative language. Journal of Computer Security, 15(3):321\u2013371, 2007.","DOI":"10.3233\/JCS-2007-15302"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"T.\u00a0Colcombet and N.\u00a0Fijalkow. Universal graphs and good for games automata: New tools for infinite duration games. In Proc. of FSTTCS, pages 1\u201326. Springer, 2019.","DOI":"10.1007\/978-3-030-17127-8_1"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"B.\u00a0Finkbeiner, C.\u00a0Hahn, and H.\u00a0Torfah. Model checking quantitative hyperproperties. In Proc. of CAV, pages 144\u2013163. Springer, 2018.","DOI":"10.1007\/978-3-319-96145-3_8"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"T.\u00a0D. Hansen, P.\u00a0B. Miltersen, and U.\u00a0Zwick. Strategy iteration is strongly polynomial for 2-player turn-based stochastic games with a constant discount factor. Journal of the ACM, 60, 2013.","DOI":"10.1145\/2432622.2432623"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"K.\u00a0He, M.\u00a0Lahijanian, L.\u00a0Kavraki, and M.\u00a0Vardi. Reactive synthesis for finite tasks under resource constraints. In Intelligent Robots and Systems (IROS), 2017 IEEE\/RSJ International Conference on, pages 5326\u20135332. IEEE, 2017","DOI":"10.1109\/IROS.2017.8206426"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"O.\u00a0Kupferman and M.\u00a0Y. Vardi. Model checking of safety properties. In Proc. of CAV, pages 172\u2013183. Springer, 1999.","DOI":"10.1007\/3-540-48683-6_17"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"M.\u00a0Kwiatkowska. 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\u2013458. ACM Press, September 2007.","DOI":"10.1145\/1295014.1295018"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"M.\u00a0Kwiatkowska, G.\u00a0Norman, and D.\u00a0Parker. Advances and challenges of probabilistic model checking. In 2010 48th Annual Allerton Conference on Communication, Control, and Computing (Allerton), pages 1691\u20131698. IEEE, 2010.","DOI":"10.1109\/ALLERTON.2010.5707120"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"M.\u00a0Lahijanian, S.\u00a0Almagor, D.\u00a0Fried, L.\u00a0Kavraki, and M.\u00a0Vardi. This time the robot settles for a cost: A quantitative approach to temporal logic planning with partial satisfaction. In AAAI, pages 3664\u20133671, 2015","DOI":"10.1609\/aaai.v29i1.9670"},{"key":"2_CR23","unstructured":"M.\u00a0L. Littman. Algorithms for sequential decision making. Brown University Providence, RI, 1996."},{"key":"2_CR24","unstructured":"M.\u00a0Osborne and A.\u00a0Rubinstein. A course in game theory. MIT press, 1994."},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"M.\u00a0Puterman. Markov decision processes. Handbooks in operations research and management science, 2:331\u2013434, 1990.","DOI":"10.1016\/S0927-0507(05)80172-0"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"S.\u00a0A. Seshia, A.\u00a0Desai, T.\u00a0Dreossi, D.\u00a0J. Fremont, S.\u00a0Ghosh, E.\u00a0Kim, S.\u00a0Shivakumar, M.\u00a0Vazquez-Chanlatte, and X.\u00a0Yue. Formal specification for deep neural networks. In Proc. of ATVA, pages 20\u201334. Springer, 2018.","DOI":"10.1007\/978-3-030-01090-4_2"},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"L.\u00a0S. Shapley. Stochastic games. Proceedings of the National Academy of Sciences of the United States of America, 39(10):1095, 1953.","DOI":"10.1073\/pnas.39.10.1953"},{"key":"2_CR28","unstructured":"R.\u00a0Sutton and A.\u00a0Barto. Introduction to reinforcement learning, volume 135. MIT press Cambridge, 1998."},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"L.\u00a0M. Tabajara and M.\u00a0Y. Vardi. Partitioning techniques in LTLf synthesis. In IJCAI, pages 5599\u20135606. AAAI Press, 2019.","DOI":"10.24963\/ijcai.2019\/777"},{"key":"2_CR30","unstructured":"W.\u00a0Thomas, T.\u00a0Wilke, et\u00a0al. Automata, logics, and infinite games: A guide to current research, volume 2500. Springer Science & Business Media, 2002."},{"key":"2_CR31","doi-asserted-by":"crossref","unstructured":"M.\u00a0Wen, R.\u00a0Ehlers, and U.\u00a0Topcu. Correct-by-synthesis reinforcement learning with temporal logic constraints. In 2015 IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS), pages 4983\u20134990. IEEE, 2015.","DOI":"10.1109\/IROS.2015.7354078"},{"key":"2_CR32","doi-asserted-by":"crossref","unstructured":"U.\u00a0Zwick and M.\u00a0Paterson. The complexity of mean payoff games on graphs. Theoretical Computer Science, 158(1):343\u2013359, 1996.","DOI":"10.1016\/0304-3975(95)00188-3"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72016-2_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,26]],"date-time":"2024-08-26T11:48:37Z","timestamp":1724672917000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-72016-2_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720155","9783030720162"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72016-2_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"20 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"141","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"41","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"21","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference changed to an online format due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}