[{"date_published":"2024-09-01T00:00:00Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","alternative_title":["LIPIcs"],"abstract":[{"text":"Graph games lie at the algorithmic core of many automated design problems in computer science. These are games usually played between two players on a given graph, where the players keep moving a token along the edges according to pre-determined rules (turn-based, concurrent, etc.), and the winner is decided based on the infinite path (aka play) traversed by the token from a given initial position. In bidding games, the players initially get some monetary budgets which they need to use to bid for the privilege of moving the token at each step. Each round of bidding affects the players' available budgets, which is the only form of update that the budgets experience. We introduce bidding games with charging where the players can additionally improve their budgets during the game by collecting vertex-dependent monetary rewards, aka the \"charges.\" Unlike traditional bidding games (where all charges are zero), bidding games with charging allow non-trivial recurrent behaviors. For example, a reachability objective may require multiple detours to vertices with high charges to earn additional budget. We show that, nonetheless, the central property of traditional bidding games generalizes to bidding games with charging: For each vertex there exists a threshold ratio, which is the necessary and sufficient fraction of the total budget for winning the game from that vertex. While the thresholds of traditional bidding games correspond to unique fixed points of linear systems of equations, in games with charging, these fixed points are no longer unique. This significantly complicates the proof of existence and the algorithmic computation of thresholds for infinite-duration objectives. We also provide the lower complexity bounds for computing thresholds for Rabin and Streett objectives, which are the first known lower bounds in any form of bidding games (with or without charging), and we solve the following repair problem for safety and reachability games that have unsatisfiable objectives: Can we distribute a given amount of charge to the players in a way such that the objective can be satisfied?","lang":"eng"}],"year":"2024","scopus_import":"1","arxiv":1,"date_updated":"2025-12-02T13:46:11Z","month":"09","isi":1,"oa_version":"Published Version","file":[{"file_id":"18083","date_created":"2024-09-17T09:35:03Z","relation":"main_file","access_level":"open_access","creator":"dernst","file_name":"2024_LIPICS_Avni.pdf","checksum":"cb6f2254b84922cd7bf224f550b73f4a","content_type":"application/pdf","date_updated":"2024-09-17T09:35:03Z","success":1,"file_size":854430}],"publication_status":"published","article_processing_charge":"Yes","project":[{"call_identifier":"H2020","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"},{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","call_identifier":"H2020"}],"oa":1,"department":[{"_id":"ToHe"}],"citation":{"apa":"Avni, G., Goharshady, E. K., Henzinger, T. A., &#38; Mallik, K. (2024). Bidding games with charging. In <i>35th International Conference on Concurrency Theory</i> (Vol. 311). Calgary, Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.8\">https://doi.org/10.4230/LIPIcs.CONCUR.2024.8</a>","ista":"Avni G, Goharshady EK, Henzinger TA, Mallik K. 2024. Bidding games with charging. 35th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 311, 8.","mla":"Avni, Guy, et al. “Bidding Games with Charging.” <i>35th International Conference on Concurrency Theory</i>, vol. 311, 8, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.8\">10.4230/LIPIcs.CONCUR.2024.8</a>.","ama":"Avni G, Goharshady EK, Henzinger TA, Mallik K. Bidding games with charging. In: <i>35th International Conference on Concurrency Theory</i>. Vol 311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2024. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.8\">10.4230/LIPIcs.CONCUR.2024.8</a>","short":"G. Avni, E.K. Goharshady, T.A. Henzinger, K. Mallik, in:, 35th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024.","chicago":"Avni, Guy, Ehsan Kafshdar Goharshady, Thomas A Henzinger, and Kaushik Mallik. “Bidding Games with Charging.” In <i>35th International Conference on Concurrency Theory</i>, Vol. 311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.8\">https://doi.org/10.4230/LIPIcs.CONCUR.2024.8</a>.","ieee":"G. Avni, E. K. Goharshady, T. A. Henzinger, and K. Mallik, “Bidding games with charging,” in <i>35th International Conference on Concurrency Theory</i>, Calgary, Canada, 2024, vol. 311."},"type":"conference","doi":"10.4230/LIPIcs.CONCUR.2024.8","acknowledgement":"This work was supported in part by the ERC projects ERC-2020-AdG 101020093 and CoG 863818 (ForM-SMArt) and by ISF grant no. 1679/21.","publication_identifier":{"issn":["1868-8969"],"isbn":["9783959773393"]},"_id":"18066","day":"01","file_date_updated":"2024-09-17T09:35:03Z","publication":"35th International Conference on Concurrency Theory","has_accepted_license":"1","volume":311,"ec_funded":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_number":"8","conference":{"end_date":"2024-09-13","name":"CONCUR: Conference on Concurrency Theory","start_date":"2024-09-09","location":"Calgary, Canada"},"corr_author":"1","date_created":"2024-09-15T22:01:39Z","ddc":["000"],"language":[{"iso":"eng"}],"author":[{"first_name":"Guy","full_name":"Avni, Guy","orcid":"0000-0001-5588-8287","last_name":"Avni","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Ehsan Kafshdar","full_name":"Goharshady, Ehsan Kafshdar","last_name":"Goharshady"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000-0002-2985-7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","last_name":"Mallik","orcid":"0000-0001-9864-7475","full_name":"Mallik, Kaushik","first_name":"Kaushik"}],"external_id":{"arxiv":["2407.06288"],"isi":["001556847400008"]},"intvolume":"       311","status":"public","tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"quality_controlled":"1","title":"Bidding games with charging"},{"publication":"35th International Conference on Concurrency Theory","file_date_updated":"2024-09-17T07:31:18Z","_id":"18067","day":"01","acknowledgement":"Udi Boker: Israel Science Foundation grant 2410/22\r\nThomas A. Henzinger: ERC-2020-AdG 101020093 (VAMOS)\r\nKaroliina Lehtinen: ANR QUASY 23-CE48-0008-01\r\nAditya Prakash: Chancellors’ International Scholarship from the University of Warwick and Centre for Discrete Mathematics and Its Applications (DIMAP)","publication_identifier":{"isbn":["9783959773393"],"issn":["1868-8969"]},"doi":"10.4230/LIPIcs.CONCUR.2024.12","citation":{"chicago":"Boker, Udi, Thomas A Henzinger, Karoliina Lehtinen, and Aditya Prakash. “History-Determinism vs Fair Simulation.” In <i>35th International Conference on Concurrency Theory</i>, Vol. 311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.12\">https://doi.org/10.4230/LIPIcs.CONCUR.2024.12</a>.","ieee":"U. Boker, T. A. Henzinger, K. Lehtinen, and A. Prakash, “History-determinism vs fair simulation,” in <i>35th International Conference on Concurrency Theory</i>, Calgary, Canada, 2024, vol. 311.","ista":"Boker U, Henzinger TA, Lehtinen K, Prakash A. 2024. History-determinism vs fair simulation. 35th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 311, 12.","apa":"Boker, U., Henzinger, T. A., Lehtinen, K., &#38; Prakash, A. (2024). History-determinism vs fair simulation. In <i>35th International Conference on Concurrency Theory</i> (Vol. 311). Calgary, Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.12\">https://doi.org/10.4230/LIPIcs.CONCUR.2024.12</a>","mla":"Boker, Udi, et al. “History-Determinism vs Fair Simulation.” <i>35th International Conference on Concurrency Theory</i>, vol. 311, 12, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.12\">10.4230/LIPIcs.CONCUR.2024.12</a>.","ama":"Boker U, Henzinger TA, Lehtinen K, Prakash A. History-determinism vs fair simulation. In: <i>35th International Conference on Concurrency Theory</i>. Vol 311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2024. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.12\">10.4230/LIPIcs.CONCUR.2024.12</a>","short":"U. Boker, T.A. Henzinger, K. Lehtinen, A. Prakash, in:, 35th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024."},"type":"conference","department":[{"_id":"ToHe"}],"oa":1,"article_processing_charge":"No","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","call_identifier":"H2020"}],"publication_status":"published","oa_version":"Published Version","file":[{"file_id":"18080","access_level":"open_access","creator":"dernst","date_created":"2024-09-17T07:31:18Z","relation":"main_file","content_type":"application/pdf","file_name":"2024_LIPICS_Boker.pdf","checksum":"66db11ef8e600a434079c278050c3f09","file_size":766902,"date_updated":"2024-09-17T07:31:18Z","success":1}],"month":"09","isi":1,"arxiv":1,"date_updated":"2025-12-02T13:44:54Z","year":"2024","abstract":[{"text":"An automaton 𝒜 is history-deterministic if its nondeterminism can be resolved on the fly, only using the prefix of the word read so far. This mild form of nondeterminism has attracted particular attention for its applications in synthesis problems. An automaton 𝒜 is guidable with respect to a class C of automata if it can fairly simulate every automaton in C, whose language is contained in that of 𝒜. In other words, guidable automata are those for which inclusion and simulation coincide, making them particularly interesting for model-checking. We study the connection between these two notions, and specifically the question of when they coincide. For classes of automata on which they do, deciding guidability, an otherwise challenging decision problem, reduces to deciding history-determinism, a problem that is starting to be well-understood for many classes. We provide a selection of sufficient criteria for a class of automata to guarantee the coincidence of the notions, and use them to show that the notions coincide for the most common automata classes, among which are ω-regular automata and many infinite-state automata with safety and reachability acceptance conditions, including vector addition systems with states, one-counter nets, pushdown-, Parikh-, and timed-automata. We also demonstrate that history-determinism and guidability do not always coincide, for example, for the classes of timed automata with a fixed number of clocks.","lang":"eng"}],"scopus_import":"1","alternative_title":["LIPIcs"],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_published":"2024-09-01T00:00:00Z","title":"History-determinism vs fair simulation","quality_controlled":"1","tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"status":"public","intvolume":"       311","author":[{"id":"31E297B6-F248-11E8-B48F-1D18A9856A87","last_name":"Boker","first_name":"Udi","full_name":"Boker, Udi"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger"},{"last_name":"Lehtinen","first_name":"Karoliina","full_name":"Lehtinen, Karoliina"},{"last_name":"Prakash","full_name":"Prakash, Aditya","first_name":"Aditya"}],"external_id":{"arxiv":["2407.08620"],"isi":["001556847400012"]},"language":[{"iso":"eng"}],"ddc":["000"],"date_created":"2024-09-15T22:01:40Z","corr_author":"1","conference":{"location":"Calgary, Canada","start_date":"2024-09-09","name":"CONCUR: Conference on Concurrency Theory","end_date":"2024-09-13"},"article_number":"12","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ec_funded":1,"volume":311,"has_accepted_license":"1"},{"file_date_updated":"2024-09-17T07:48:56Z","publication":"35th International Conference on Concurrency Theory","_id":"18068","day":"01","doi":"10.4230/LIPIcs.CONCUR.2024.29","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093. N. Mazzocchi was affiliated with ISTA when this work was submitted for publication.","publication_identifier":{"issn":["1868-8969"],"isbn":["9783959773393"]},"oa":1,"type":"conference","department":[{"_id":"ToHe"},{"_id":"GradSch"}],"citation":{"apa":"Henzinger, T. A., Mazzocchi, N. A., &#38; Sarac, N. E. (2024). Strategic dominance: A new preorder for nondeterministic processes. In <i>35th International Conference on Concurrency Theory</i> (Vol. 311). Calgary, Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.29\">https://doi.org/10.4230/LIPIcs.CONCUR.2024.29</a>","ista":"Henzinger TA, Mazzocchi NA, Sarac NE. 2024. Strategic dominance: A new preorder for nondeterministic processes. 35th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 311, 29.","short":"T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 35th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024.","ama":"Henzinger TA, Mazzocchi NA, Sarac NE. Strategic dominance: A new preorder for nondeterministic processes. In: <i>35th International Conference on Concurrency Theory</i>. Vol 311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2024. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.29\">10.4230/LIPIcs.CONCUR.2024.29</a>","mla":"Henzinger, Thomas A., et al. “Strategic Dominance: A New Preorder for Nondeterministic Processes.” <i>35th International Conference on Concurrency Theory</i>, vol. 311, 29, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.29\">10.4230/LIPIcs.CONCUR.2024.29</a>.","chicago":"Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Strategic Dominance: A New Preorder for Nondeterministic Processes.” In <i>35th International Conference on Concurrency Theory</i>, Vol. 311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2024.29\">https://doi.org/10.4230/LIPIcs.CONCUR.2024.29</a>.","ieee":"T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Strategic dominance: A new preorder for nondeterministic processes,” in <i>35th International Conference on Concurrency Theory</i>, Calgary, Canada, 2024, vol. 311."},"OA_place":"publisher","publication_status":"published","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","call_identifier":"H2020"}],"article_processing_charge":"Yes","file":[{"file_id":"18081","date_created":"2024-09-17T07:48:56Z","relation":"main_file","access_level":"open_access","creator":"dernst","file_name":"2024_LIPICS_Henzinger.pdf","checksum":"555bd343e1fb38adeab8fc465ff4fad8","content_type":"application/pdf","date_updated":"2024-09-17T07:48:56Z","success":1,"file_size":964124}],"oa_version":"Published Version","alternative_title":["LIPIcs"],"year":"2024","abstract":[{"lang":"eng","text":"We study the following refinement relation between nondeterministic state-transition models: model ℬ strategically dominates model 𝒜 iff every deterministic refinement of 𝒜 is language contained in some deterministic refinement of ℬ. While language containment is trace inclusion, and the (fair) simulation preorder coincides with tree inclusion, strategic dominance falls strictly between the two and can be characterized as \"strategy inclusion\" between 𝒜 and ℬ: every strategy that resolves the nondeterminism of 𝒜 is dominated by a strategy that resolves the nondeterminism of ℬ. Strategic dominance can be checked in 2-ExpTime by a decidable first-order Presburger logic with quantification over words and strategies, called resolver logic. We give several other applications of resolver logic, including checking the co-safety, co-liveness, and history-determinism of boolean and quantitative automata, and checking the inclusion between hyperproperties that are specified by nondeterministic boolean and quantitative automata."}],"scopus_import":"1","arxiv":1,"date_updated":"2025-12-02T13:45:38Z","month":"09","isi":1,"date_published":"2024-09-01T00:00:00Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","quality_controlled":"1","title":"Strategic dominance: A new preorder for nondeterministic processes","tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"intvolume":"       311","status":"public","language":[{"iso":"eng"}],"author":[{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Mazzocchi, Nicolas Adrien","first_name":"Nicolas Adrien","last_name":"Mazzocchi","id":"b26baa86-3308-11ec-87b0-8990f34baa85"},{"id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","last_name":"Sarac","full_name":"Sarac, Naci E","first_name":"Naci E"}],"external_id":{"arxiv":["2407.10473"],"isi":["001556847400029"]},"corr_author":"1","date_created":"2024-09-15T22:01:40Z","ddc":["000"],"article_number":"29","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"end_date":"2024-09-13","name":"CONCUR: Conference on Concurrency Theory","start_date":"2024-09-09","location":"Calgary, Canada"},"volume":311,"ec_funded":1,"has_accepted_license":"1","OA_type":"gold"}]