[{"publisher":"International Federation for Computational Logic","isi":1,"department":[{"_id":"ToHe"}],"quality_controlled":"1","publication":"Logical Methods in Computer Science","intvolume":"        17","status":"public","page":"10:1-10:23","month":"02","date_created":"2022-01-25T16:32:13Z","acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE), Z211-N23 (Wittgenstein Award), and M 2369-N33 (Meitner fellowship).\r\n","project":[{"name":"Formal Methods meets Algorithmic Game Theory","grant_number":"M02369","call_identifier":"FWF","_id":"264B3912-B435-11E9-9278-68D0E5697425"},{"grant_number":"S11402-N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"}],"language":[{"iso":"eng"}],"keyword":["computer science","computer science and game theory","logic in computer science"],"ddc":["510"],"doi":"10.23638/LMCS-17(1:10)2021","citation":{"short":"M. Aghajohari, G. Avni, T.A. Henzinger, Logical Methods in Computer Science 17 (2021) 10:1-10:23.","ama":"Aghajohari M, Avni G, Henzinger TA. Determinacy in discrete-bidding infinite-duration games. <i>Logical Methods in Computer Science</i>. 2021;17(1):10:1-10:23. doi:<a href=\"https://doi.org/10.23638/LMCS-17(1:10)2021\">10.23638/LMCS-17(1:10)2021</a>","apa":"Aghajohari, M., Avni, G., &#38; Henzinger, T. A. (2021). Determinacy in discrete-bidding infinite-duration games. <i>Logical Methods in Computer Science</i>. International Federation for Computational Logic. <a href=\"https://doi.org/10.23638/LMCS-17(1:10)2021\">https://doi.org/10.23638/LMCS-17(1:10)2021</a>","chicago":"Aghajohari, Milad, Guy Avni, and Thomas A Henzinger. “Determinacy in Discrete-Bidding Infinite-Duration Games.” <i>Logical Methods in Computer Science</i>. International Federation for Computational Logic, 2021. <a href=\"https://doi.org/10.23638/LMCS-17(1:10)2021\">https://doi.org/10.23638/LMCS-17(1:10)2021</a>.","ista":"Aghajohari M, Avni G, Henzinger TA. 2021. Determinacy in discrete-bidding infinite-duration games. Logical Methods in Computer Science. 17(1), 10:1-10:23.","ieee":"M. Aghajohari, G. Avni, and T. A. Henzinger, “Determinacy in discrete-bidding infinite-duration games,” <i>Logical Methods in Computer Science</i>, vol. 17, no. 1. International Federation for Computational Logic, p. 10:1-10:23, 2021.","mla":"Aghajohari, Milad, et al. “Determinacy in Discrete-Bidding Infinite-Duration Games.” <i>Logical Methods in Computer Science</i>, vol. 17, no. 1, International Federation for Computational Logic, 2021, p. 10:1-10:23, doi:<a href=\"https://doi.org/10.23638/LMCS-17(1:10)2021\">10.23638/LMCS-17(1:10)2021</a>."},"title":"Determinacy in discrete-bidding infinite-duration games","day":"03","type":"journal_article","author":[{"last_name":"Aghajohari","full_name":"Aghajohari, Milad","first_name":"Milad"},{"last_name":"Avni","first_name":"Guy","full_name":"Avni, Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"}],"publication_status":"published","oa":1,"file_date_updated":"2022-01-26T08:04:50Z","volume":17,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"arxiv":1,"issue":"1","article_processing_charge":"No","file":[{"content_type":"application/pdf","file_id":"10690","relation":"main_file","date_created":"2022-01-26T08:04:50Z","success":1,"file_name":"2021_LMCS_AGHAJOHAR.pdf","creator":"alisjak","file_size":819878,"checksum":"b35586a50ed1ca8f44767de116d18d81","date_updated":"2022-01-26T08:04:50Z","access_level":"open_access"}],"_id":"10674","abstract":[{"lang":"eng","text":"In two-player games on graphs, the players move a token through a graph to produce an infinite path, which determines the winner of the game. Such games are central in formal methods since they model the interaction between a non-terminating system and its environment. In bidding games the players bid for the right to move the token: in each round, the players simultaneously submit bids, and the higher bidder moves the token and pays the other player. Bidding games are known to have a clean and elegant mathematical structure that relies on the ability of the players to submit arbitrarily small bids. Many applications, however, require a fixed granularity for the bids, which can represent, for example, the monetary value expressed in cents. We study, for the first time, the combination of discrete-bidding and infinite-duration games. Our most important result proves that these games form a large determined subclass of concurrent games, where determinacy is the strong property that there always exists exactly one player who can guarantee winning the game. In particular, we show that, in contrast to non-discrete bidding games, the mechanism with which tied bids are resolved plays an important role in discrete-bidding games. We study several natural tie-breaking mechanisms and show that, while some do not admit determinacy, most natural mechanisms imply determinacy for every pair of initial budgets."}],"date_published":"2021-02-03T00:00:00Z","date_updated":"2023-08-17T06:56:42Z","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","external_id":{"arxiv":["1905.03588"],"isi":["000658724600010"]},"scopus_import":"1","publication_identifier":{"eissn":["1860-5974"]},"article_type":"original","year":"2021","oa_version":"Published Version","has_accepted_license":"1"},{"page":"1-13","date_created":"2021-09-12T22:01:24Z","month":"07","isi":1,"publisher":"Institute of Electrical and Electronics Engineers","status":"public","quality_controlled":"1","department":[{"_id":"KrCh"}],"publication":"Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science","conference":{"location":"Rome, Italy","name":"LICS: Symposium on Logic in Computer Science","end_date":"2021-07-02","start_date":"2021-06-29"},"title":"Symbolic time and space tradeoffs for probabilistic verification","ec_funded":1,"citation":{"apa":"Chatterjee, K., Dvorak, W., Henzinger, M. H., &#38; Svozil, A. (2021). Symbolic time and space tradeoffs for probabilistic verification. In <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i> (pp. 1–13). Rome, Italy: Institute of Electrical and Electronics Engineers. <a href=\"https://doi.org/10.1109/LICS52264.2021.9470739\">https://doi.org/10.1109/LICS52264.2021.9470739</a>","ama":"Chatterjee K, Dvorak W, Henzinger MH, Svozil A. Symbolic time and space tradeoffs for probabilistic verification. In: <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. Institute of Electrical and Electronics Engineers; 2021:1-13. doi:<a href=\"https://doi.org/10.1109/LICS52264.2021.9470739\">10.1109/LICS52264.2021.9470739</a>","short":"K. Chatterjee, W. Dvorak, M.H. Henzinger, A. Svozil, in:, Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, Institute of Electrical and Electronics Engineers, 2021, pp. 1–13.","mla":"Chatterjee, Krishnendu, et al. “Symbolic Time and Space Tradeoffs for Probabilistic Verification.” <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Institute of Electrical and Electronics Engineers, 2021, pp. 1–13, doi:<a href=\"https://doi.org/10.1109/LICS52264.2021.9470739\">10.1109/LICS52264.2021.9470739</a>.","ista":"Chatterjee K, Dvorak W, Henzinger MH, Svozil A. 2021. Symbolic time and space tradeoffs for probabilistic verification. Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Symposium on Logic in Computer Science, 1–13.","ieee":"K. Chatterjee, W. Dvorak, M. H. Henzinger, and A. Svozil, “Symbolic time and space tradeoffs for probabilistic verification,” in <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Rome, Italy, 2021, pp. 1–13.","chicago":"Chatterjee, Krishnendu, Wolfgang Dvorak, Monika H Henzinger, and Alexander Svozil. “Symbolic Time and Space Tradeoffs for Probabilistic Verification.” In <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, 1–13. Institute of Electrical and Electronics Engineers, 2021. <a href=\"https://doi.org/10.1109/LICS52264.2021.9470739\">https://doi.org/10.1109/LICS52264.2021.9470739</a>."},"type":"conference","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"last_name":"Dvorak","full_name":"Dvorak, Wolfgang","first_name":"Wolfgang"},{"first_name":"Monika H","full_name":"Henzinger, Monika H","last_name":"Henzinger","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","orcid":"0000-0002-5008-6530"},{"full_name":"Svozil, Alexander","first_name":"Alexander","last_name":"Svozil"}],"day":"07","acknowledgement":"The authors are grateful to the anonymous referees for their valuable comments. A. S. is fully supported by the Vienna Science and Technology Fund (WWTF) through project ICT15–003. K. C. is supported by the Austrian Science Fund (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE) and by the ERC CoG 863818 (ForM-SMArt). For M. H. the research leading to these results has received funding from the European Research Council under the European Unions Seventh Framework Programme (FP/2007–2013) / ERC Grant Agreement no. 340506.","project":[{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407"},{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"}],"doi":"10.1109/LICS52264.2021.9470739","language":[{"iso":"eng"}],"keyword":["Computer science","Computational modeling","Markov processes","Probabilistic logic","Formal verification","Game Theory"],"article_processing_charge":"No","arxiv":1,"_id":"10002","date_published":"2021-07-07T00:00:00Z","abstract":[{"lang":"eng","text":"We present a faster symbolic algorithm for the following central problem in probabilistic verification: Compute the maximal end-component (MEC) decomposition of Markov decision processes (MDPs). This problem generalizes the SCC decomposition problem of graphs and closed recurrent sets of Markov chains. The model of symbolic algorithms is widely used in formal verification and model-checking, where access to the input model is restricted to only symbolic operations (e.g., basic set operations and computation of one-step neighborhood). For an input MDP with  n  vertices and  m  edges, the classical symbolic algorithm from the 1990s for the MEC decomposition requires  O(n2)  symbolic operations and  O(1)  symbolic space. The only other symbolic algorithm for the MEC decomposition requires  O(nm−−√)  symbolic operations and  O(m−−√)  symbolic space. A main open question is whether the worst-case  O(n2)  bound for symbolic operations can be beaten. We present a symbolic algorithm that requires  O˜(n1.5)  symbolic operations and  O˜(n−−√)  symbolic space. Moreover, the parametrization of our algorithm provides a trade-off between symbolic operations and symbolic space: for all  0<ϵ≤1/2  the symbolic algorithm requires  O˜(n2−ϵ)  symbolic operations and  O˜(nϵ)  symbolic space ( O˜  hides poly-logarithmic factors). Using our techniques we present faster algorithms for computing the almost-sure winning regions of  ω -regular objectives for MDPs. We consider the canonical parity objectives for  ω -regular objectives, and for parity objectives with  d -priorities we present an algorithm that computes the almost-sure winning region with  O˜(n2−ϵ)  symbolic operations and  O˜(nϵ)  symbolic space, for all  0<ϵ≤1/2 ."}],"main_file_link":[{"url":"https://arxiv.org/abs/2104.07466","open_access":"1"}],"oa":1,"publication_status":"published","oa_version":"Preprint","year":"2021","publication_identifier":{"eisbn":["978-1-6654-4895-6"],"isbn":["978-1-6654-4896-3"],"issn":["1043-6871"]},"date_updated":"2025-07-14T09:10:07Z","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","scopus_import":"1","external_id":{"isi":["000947350400089"],"arxiv":["2104.07466"]}},{"title":"Valuation compressions in VCG-based combinatorial auctions","citation":{"ama":"Dütting P, Henzinger MH, Starnberger M. Valuation compressions in VCG-based combinatorial auctions. <i>ACM Transactions on Economics and Computation</i>. 2018;6(2). doi:<a href=\"https://doi.org/10.1145/3232860\">10.1145/3232860</a>","apa":"Dütting, P., Henzinger, M. H., &#38; Starnberger, M. (2018). Valuation compressions in VCG-based combinatorial auctions. <i>ACM Transactions on Economics and Computation</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3232860\">https://doi.org/10.1145/3232860</a>","short":"P. Dütting, M.H. Henzinger, M. Starnberger, ACM Transactions on Economics and Computation 6 (2018).","mla":"Dütting, Paul, et al. “Valuation Compressions in VCG-Based Combinatorial Auctions.” <i>ACM Transactions on Economics and Computation</i>, vol. 6, no. 2, 5, Association for Computing Machinery, 2018, doi:<a href=\"https://doi.org/10.1145/3232860\">10.1145/3232860</a>.","chicago":"Dütting, Paul, Monika H Henzinger, and Martin Starnberger. “Valuation Compressions in VCG-Based Combinatorial Auctions.” <i>ACM Transactions on Economics and Computation</i>. Association for Computing Machinery, 2018. <a href=\"https://doi.org/10.1145/3232860\">https://doi.org/10.1145/3232860</a>.","ieee":"P. Dütting, M. H. Henzinger, and M. Starnberger, “Valuation compressions in VCG-based combinatorial auctions,” <i>ACM Transactions on Economics and Computation</i>, vol. 6, no. 2. Association for Computing Machinery, 2018.","ista":"Dütting P, Henzinger MH, Starnberger M. 2018. Valuation compressions in VCG-based combinatorial auctions. ACM Transactions on Economics and Computation. 6(2), 5."},"type":"journal_article","author":[{"last_name":"Dütting","full_name":"Dütting, Paul","first_name":"Paul"},{"id":"540c9bbd-f2de-11ec-812d-d04a5be85630","orcid":"0000-0002-5008-6530","last_name":"Henzinger","first_name":"Monika H","full_name":"Henzinger, Monika H"},{"first_name":"Martin","full_name":"Starnberger, Martin","last_name":"Starnberger"}],"day":"01","doi":"10.1145/3232860","language":[{"iso":"eng"}],"keyword":["Theory of computation","Algorithmic game theory and mechanism design","Applied computing","Economics","Simplified mechanisms","Combinatorial auctions with item bidding","Price of anarchy"],"date_created":"2022-07-27T11:46:46Z","extern":"1","month":"05","publisher":"Association for Computing Machinery","status":"public","intvolume":"         6","quality_controlled":"1","publication":"ACM Transactions on Economics and Computation","year":"2018","oa_version":"Preprint","article_type":"original","publication_identifier":{"issn":["2167-8375"],"eissn":["2167-8383"]},"date_updated":"2022-09-09T12:04:42Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":"1","external_id":{"arxiv":["1310.3153"]},"issue":"2","article_processing_charge":"No","arxiv":1,"date_published":"2018-05-01T00:00:00Z","_id":"11667","abstract":[{"lang":"eng","text":"The focus of classic mechanism design has been on truthful direct-revelation mechanisms. In the context of combinatorial auctions, the truthful direct-revelation mechanism that maximizes social welfare is the Vickrey-Clarke-Groves mechanism. For many valuation spaces, computing the allocation and payments of the VCG mechanism, however, is a computationally hard problem. We thus study the performance of the VCG mechanism when bidders are forced to choose bids from a subspace of the valuation space for which the VCG outcome can be computed efficiently. We prove improved upper bounds on the welfare loss for restrictions to additive bids and upper and lower bounds for restrictions to non-additive bids. These bounds show that increased expressiveness can give rise to additional equilibria of poorer efficiency."}],"article_number":"5","main_file_link":[{"url":"https://arxiv.org/abs/1310.3153","open_access":"1"}],"oa":1,"publication_status":"published","volume":6},{"date_created":"2022-07-27T12:09:15Z","extern":"1","month":"12","status":"public","intvolume":"         4","quality_controlled":"1","publication":"ACM Transactions on Economics and Computation","publisher":"Association for Computing Machinery","type":"journal_article","author":[{"first_name":"Paul","full_name":"Dütting, Paul","last_name":"Dütting"},{"orcid":"0000-0002-5008-6530","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","first_name":"Monika H","full_name":"Henzinger, Monika H","last_name":"Henzinger"},{"first_name":"Martin","full_name":"Starnberger, Martin","last_name":"Starnberger"}],"day":"05","title":"Auctions for heterogeneous items and budget limits","citation":{"apa":"Dütting, P., Henzinger, M. H., &#38; Starnberger, M. (2015). Auctions for heterogeneous items and budget limits. <i>ACM Transactions on Economics and Computation</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/2818351\">https://doi.org/10.1145/2818351</a>","ama":"Dütting P, Henzinger MH, Starnberger M. Auctions for heterogeneous items and budget limits. <i>ACM Transactions on Economics and Computation</i>. 2015;4(1). doi:<a href=\"https://doi.org/10.1145/2818351\">10.1145/2818351</a>","short":"P. Dütting, M.H. Henzinger, M. Starnberger, ACM Transactions on Economics and Computation 4 (2015).","mla":"Dütting, Paul, et al. “Auctions for Heterogeneous Items and Budget Limits.” <i>ACM Transactions on Economics and Computation</i>, vol. 4, no. 1, 4, Association for Computing Machinery, 2015, doi:<a href=\"https://doi.org/10.1145/2818351\">10.1145/2818351</a>.","ista":"Dütting P, Henzinger MH, Starnberger M. 2015. Auctions for heterogeneous items and budget limits. ACM Transactions on Economics and Computation. 4(1), 4.","ieee":"P. Dütting, M. H. Henzinger, and M. Starnberger, “Auctions for heterogeneous items and budget limits,” <i>ACM Transactions on Economics and Computation</i>, vol. 4, no. 1. Association for Computing Machinery, 2015.","chicago":"Dütting, Paul, Monika H Henzinger, and Martin Starnberger. “Auctions for Heterogeneous Items and Budget Limits.” <i>ACM Transactions on Economics and Computation</i>. Association for Computing Machinery, 2015. <a href=\"https://doi.org/10.1145/2818351\">https://doi.org/10.1145/2818351</a>."},"doi":"10.1145/2818351","language":[{"iso":"eng"}],"keyword":["Algorithmic game theory","auction theory","Clinching auction","Pareto optimality","Budget limits"],"date_published":"2015-12-05T00:00:00Z","_id":"11669","abstract":[{"lang":"eng","text":"We study individual rational, Pareto-optimal, and incentive compatible mechanisms for auctions with heterogeneous items and budget limits. We consider settings with multiunit demand and additive valuations. For single-dimensional valuations we prove a positive result for randomized mechanisms, and a negative result for deterministic mechanisms. While the positive result allows for private budgets, the negative result is for public budgets. For multidimensional valuations and public budgets we prove an impossibility result that applies to deterministic and randomized mechanisms. Taken together this shows the power of randomization in certain settings with heterogeneous items, but it also shows its limitations."}],"article_number":"4","issue":"1","article_processing_charge":"No","arxiv":1,"volume":4,"oa":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1209.6448"}],"publication_status":"published","year":"2015","oa_version":"Preprint","article_type":"original","publication_identifier":{"eissn":["2167-8383"],"issn":["2167-8375"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2022-09-09T12:08:37Z","scopus_import":"1","external_id":{"arxiv":["1209.6448"]}}]