[{"external_id":{"isi":["000487714900008"],"arxiv":["1705.01433"]},"article_processing_charge":"No","author":[{"full_name":"Avni, Guy","orcid":"0000-0001-5588-8287","last_name":"Avni","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","first_name":"Guy"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger"},{"last_name":"Chonev","full_name":"Chonev, Ventsislav K","first_name":"Ventsislav K","id":"36CBE2E6-F248-11E8-B48F-1D18A9856A87"}],"title":"Infinite-duration bidding games","citation":{"chicago":"Avni, Guy, Thomas A Henzinger, and Ventsislav K Chonev. “Infinite-Duration Bidding Games.” Journal of the ACM. ACM, 2019. https://doi.org/10.1145/3340295.","ista":"Avni G, Henzinger TA, Chonev VK. 2019. Infinite-duration bidding games. Journal of the ACM. 66(4), 31.","mla":"Avni, Guy, et al. “Infinite-Duration Bidding Games.” Journal of the ACM, vol. 66, no. 4, 31, ACM, 2019, doi:10.1145/3340295.","apa":"Avni, G., Henzinger, T. A., & Chonev, V. K. (2019). Infinite-duration bidding games. Journal of the ACM. ACM. https://doi.org/10.1145/3340295","ama":"Avni G, Henzinger TA, Chonev VK. Infinite-duration bidding games. Journal of the ACM. 2019;66(4). doi:10.1145/3340295","short":"G. Avni, T.A. Henzinger, V.K. Chonev, Journal of the ACM 66 (2019).","ieee":"G. Avni, T. A. Henzinger, and V. K. Chonev, “Infinite-duration bidding games,” Journal of the ACM, vol. 66, no. 4. ACM, 2019."},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","project":[{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"S11402-N23","name":"Rigorous Systems Engineering","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"264B3912-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"M02369","name":"Formal Methods meets Algorithmic Game Theory"}],"article_number":"31","date_created":"2019-08-04T21:59:16Z","date_published":"2019-07-16T00:00:00Z","doi":"10.1145/3340295","year":"2019","isi":1,"publication":"Journal of the ACM","day":"16","oa":1,"quality_controlled":"1","publisher":"ACM","department":[{"_id":"ToHe"}],"date_updated":"2023-08-29T07:02:13Z","type":"journal_article","status":"public","_id":"6752","issue":"4","volume":66,"related_material":{"record":[{"status":"public","id":"950","relation":"earlier_version"}]},"publication_status":"published","publication_identifier":{"issn":["00045411"],"eissn":["1557735X"]},"language":[{"iso":"eng"}],"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1705.01433"}],"scopus_import":"1","intvolume":" 66","month":"07","abstract":[{"lang":"eng","text":"Two-player games on graphs are widely studied in formal methods, as they model the interaction between a system and its environment. The game is played by moving a token throughout a graph to produce an infinite path. There are several common modes to determine how the players move the token through the graph; e.g., in turn-based games the players alternate turns in moving the token. We study the bidding mode of moving the token, which, to the best of our knowledge, has never been studied in infinite-duration games. The following bidding rule was previously defined and called Richman bidding. Both players have separate budgets, which sum up to 1. In each turn, a bidding takes place: Both players submit bids simultaneously, where a bid is legal if it does not exceed the available budget, and the higher bidder pays his bid to the other player and moves the token. The central question studied in bidding games is a necessary and sufficient initial budget for winning the game: a threshold budget in a vertex is a value t ∈ [0, 1] such that if Player 1’s budget exceeds t, he can win the game; and if Player 2’s budget exceeds 1 − t, he can win the game. Threshold budgets were previously shown to exist in every vertex of a reachability game, which have an interesting connection with random-turn games—a sub-class of simple stochastic games in which the player who moves is chosen randomly. We show the existence of threshold budgets for a qualitative class of infinite-duration games, namely parity games, and a quantitative class, namely mean-payoff games. The key component of the proof is a quantitative solution to strongly connected mean-payoff bidding games in which we extend the connection with random-turn games to these games, and construct explicit optimal strategies for both players."}],"oa_version":"Preprint"},{"title":"Infinite-duration bidding games","external_id":{"arxiv":["1705.01433"]},"author":[{"orcid":"0000-0001-5588-8287","full_name":"Avni, Guy","last_name":"Avni","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","first_name":"Guy"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"full_name":"Chonev, Ventsislav K","last_name":"Chonev","id":"36CBE2E6-F248-11E8-B48F-1D18A9856A87","first_name":"Ventsislav K"}],"publist_id":"6466","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"chicago":"Avni, Guy, Thomas A Henzinger, and Ventsislav K Chonev. “Infinite-Duration Bidding Games,” Vol. 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. https://doi.org/10.4230/LIPIcs.CONCUR.2017.21.","ista":"Avni G, Henzinger TA, Chonev VK. 2017. Infinite-duration bidding games. CONCUR: Concurrency Theory, LIPIcs, vol. 85, 17.","mla":"Avni, Guy, et al. Infinite-Duration Bidding Games. Vol. 85, 17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:10.4230/LIPIcs.CONCUR.2017.21.","ieee":"G. Avni, T. A. Henzinger, and V. K. Chonev, “Infinite-duration bidding games,” presented at the CONCUR: Concurrency Theory, Berlin, Germany, 2017, vol. 85.","short":"G. Avni, T.A. Henzinger, V.K. Chonev, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.","ama":"Avni G, Henzinger TA, Chonev VK. Infinite-duration bidding games. In: Vol 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:10.4230/LIPIcs.CONCUR.2017.21","apa":"Avni, G., Henzinger, T. A., & Chonev, V. K. (2017). Infinite-duration bidding games (Vol. 85). Presented at the CONCUR: Concurrency Theory, Berlin, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2017.21"},"project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211"}],"article_number":"17","date_created":"2018-12-11T11:49:22Z","date_published":"2017-09-01T00:00:00Z","doi":"10.4230/LIPIcs.CONCUR.2017.21","day":"01","year":"2017","has_accepted_license":"1","oa":1,"quality_controlled":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","file_date_updated":"2020-07-14T12:48:16Z","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"ddc":["000"],"date_updated":"2023-08-29T07:02:13Z","pubrep_id":"844","status":"public","conference":{"start_date":"2017-09-05","end_date":"2017-09-07","location":"Berlin, Germany","name":"CONCUR: Concurrency Theory"},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"type":"conference","_id":"950","license":"https://creativecommons.org/licenses/by/4.0/","related_material":{"record":[{"id":"6752","status":"public","relation":"later_version"}]},"volume":85,"language":[{"iso":"eng"}],"file":[{"file_name":"IST-2017-844-v1+1_concur-cr.pdf","date_created":"2018-12-12T10:18:00Z","creator":"system","file_size":335170,"date_updated":"2020-07-14T12:48:16Z","checksum":"6d5cccf755207b91ccbef95d8275b013","file_id":"5318","relation":"main_file","access_level":"open_access","content_type":"application/pdf"}],"publication_status":"published","publication_identifier":{"issn":["1868-8969"]},"intvolume":" 85","month":"09","alternative_title":["LIPIcs"],"scopus_import":1,"oa_version":"Published Version","abstract":[{"text":"Two-player games on graphs are widely studied in formal methods as they model the interaction between a system and its environment. The game is played by moving a token throughout a graph to produce an infinite path. There are several common modes to determine how the players move the token through the graph; e.g., in turn-based games the players alternate turns in moving the token. We study the bidding mode of moving the token, which, to the best of our knowledge, has never been studied in infinite-duration games. Both players have separate budgets, which sum up to $1$. In each turn, a bidding takes place. Both players submit bids simultaneously, and a bid is legal if it does not exceed the available budget. The winner of the bidding pays his bid to the other player and moves the token. For reachability objectives, repeated bidding games have been studied and are called Richman games. There, a central question is the existence and computation of threshold budgets; namely, a value t\\in [0,1] such that if\\PO's budget exceeds $t$, he can win the game, and if\\PT's budget exceeds 1-t, he can win the game. We focus on parity games and mean-payoff games. We show the existence of threshold budgets in these games, and reduce the problem of finding them to Richman games. We also determine the strategy-complexity of an optimal strategy. Our most interesting result shows that memoryless strategies suffice for mean-payoff bidding games. \r\n","lang":"eng"}]},{"ec_funded":1,"volume":55,"publication_status":"published","language":[{"iso":"eng"}],"file":[{"access_level":"open_access","relation":"main_file","content_type":"application/pdf","file_id":"5213","creator":"system","date_updated":"2018-12-12T10:16:26Z","file_size":521415,"date_created":"2018-12-12T10:16:26Z","file_name":"IST-2017-778-v1+1_LIPIcs-ICALP-2016-100.pdf"}],"scopus_import":1,"alternative_title":["LIPIcs"],"intvolume":" 55","month":"08","abstract":[{"lang":"eng","text":"The Continuous Skolem Problem asks whether a real-valued function satisfying a linear differen-\r\ntial equation has a zero in a given interval of real numbers. This is a fundamental reachability\r\nproblem for continuous linear dynamical systems, such as linear hybrid automata and continuous-\r\ntime Markov chains. Decidability of the problem is currently open – indeed decidability is open\r\neven for the sub-problem in which a zero is sought in a bounded interval. In this paper we show\r\ndecidability of the bounded problem subject to Schanuel’s Conjecture, a unifying conjecture in\r\ntranscendental number theory. We furthermore analyse the unbounded problem in terms of the\r\nfrequencies of the differential equation, that is, the imaginary parts of the characteristic roots.\r\nWe show that the unbounded problem can be reduced to the bounded problem if there is at most\r\none rationally linearly independent frequency, or if there are two rationally linearly independent\r\nfrequencies and all characteristic roots are simple. We complete the picture by showing that de-\r\ncidability of the unbounded problem in the case of two (or more) rationally linearly independent\r\nfrequencies would entail a major new effectiveness result in Diophantine approximation, namely\r\ncomputability of the Diophantine-approximation types of all real algebraic numbers."}],"oa_version":"Published Version","file_date_updated":"2018-12-12T10:16:26Z","department":[{"_id":"KrCh"}],"date_updated":"2021-01-12T06:48:03Z","ddc":["004","006"],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"end_date":"2016-07-15","location":"Rome, Italy","start_date":"2016-07-12","name":"ICALP: Automata, Languages and Programming"},"type":"conference","pubrep_id":"778","status":"public","_id":"1069","date_created":"2018-12-11T11:49:59Z","date_published":"2016-08-01T00:00:00Z","doi":"10.4230/LIPIcs.ICALP.2016.100","year":"2016","has_accepted_license":"1","day":"01","oa":1,"publisher":"Schloss Dagstuhl- Leibniz-Zentrum fur Informatik","quality_controlled":"1","acknowledgement":"Ventsislav Chonev is supported by Austrian Science Fund (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant (279307: Graph Games), and ERC Advanced Grant (267989: QUAREM).","author":[{"first_name":"Ventsislav K","id":"36CBE2E6-F248-11E8-B48F-1D18A9856A87","full_name":"Chonev, Ventsislav K","last_name":"Chonev"},{"first_name":"Joël","full_name":"Ouaknine, Joël","last_name":"Ouaknine"},{"first_name":"James","last_name":"Worrell","full_name":"Worrell, James"}],"publist_id":"6314","title":"On the skolem problem for continuous linear dynamical systems","citation":{"short":"V.K. Chonev, J. Ouaknine, J. Worrell, in:, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik, 2016.","ieee":"V. K. Chonev, J. Ouaknine, and J. Worrell, “On the skolem problem for continuous linear dynamical systems,” presented at the ICALP: Automata, Languages and Programming, Rome, Italy, 2016, vol. 55.","ama":"Chonev VK, Ouaknine J, Worrell J. On the skolem problem for continuous linear dynamical systems. In: Vol 55. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik; 2016. doi:10.4230/LIPIcs.ICALP.2016.100","apa":"Chonev, V. K., Ouaknine, J., & Worrell, J. (2016). On the skolem problem for continuous linear dynamical systems (Vol. 55). Presented at the ICALP: Automata, Languages and Programming, Rome, Italy: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik. https://doi.org/10.4230/LIPIcs.ICALP.2016.100","mla":"Chonev, Ventsislav K., et al. On the Skolem Problem for Continuous Linear Dynamical Systems. Vol. 55, 100, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik, 2016, doi:10.4230/LIPIcs.ICALP.2016.100.","ista":"Chonev VK, Ouaknine J, Worrell J. 2016. On the skolem problem for continuous linear dynamical systems. ICALP: Automata, Languages and Programming, LIPIcs, vol. 55, 100.","chicago":"Chonev, Ventsislav K, Joël Ouaknine, and James Worrell. “On the Skolem Problem for Continuous Linear Dynamical Systems,” Vol. 55. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik, 2016. https://doi.org/10.4230/LIPIcs.ICALP.2016.100."},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"}],"article_number":"100"},{"volume":63,"date_published":"2016-06-01T00:00:00Z","doi":"10.1145/2857050","issue":"3","date_created":"2018-12-11T11:51:41Z","day":"01","publication":"Journal of the ACM","language":[{"iso":"eng"}],"year":"2016","publication_status":"published","month":"06","intvolume":" 63","publisher":"ACM","scopus_import":1,"quality_controlled":"1","oa":1,"main_file_link":[{"url":"http://arxiv.org/abs/1303.2981","open_access":"1"}],"oa_version":"Preprint","abstract":[{"lang":"eng","text":"We consider higher-dimensional versions of Kannan and Lipton's Orbit Problem - determining whether a target vector space V may be reached from a starting point x under repeated applications of a linear transformation A. Answering two questions posed by Kannan and Lipton in the 1980s, we show that when V has dimension one, this problem is solvable in polynomial time, and when V has dimension two or three, the problem is in NPRP."}],"department":[{"_id":"KrCh"}],"title":"On the complexity of the orbit problem","publist_id":"5831","author":[{"full_name":"Chonev, Ventsislav K","last_name":"Chonev","first_name":"Ventsislav K","id":"36CBE2E6-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Ouaknine, Joël","last_name":"Ouaknine","first_name":"Joël"},{"first_name":"James","last_name":"Worrell","full_name":"Worrell, James"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T06:50:17Z","citation":{"ama":"Chonev VK, Ouaknine J, Worrell J. On the complexity of the orbit problem. Journal of the ACM. 2016;63(3). doi:10.1145/2857050","apa":"Chonev, V. K., Ouaknine, J., & Worrell, J. (2016). On the complexity of the orbit problem. Journal of the ACM. ACM. https://doi.org/10.1145/2857050","short":"V.K. Chonev, J. Ouaknine, J. Worrell, Journal of the ACM 63 (2016).","ieee":"V. K. Chonev, J. Ouaknine, and J. Worrell, “On the complexity of the orbit problem,” Journal of the ACM, vol. 63, no. 3. ACM, 2016.","mla":"Chonev, Ventsislav K., et al. “On the Complexity of the Orbit Problem.” Journal of the ACM, vol. 63, no. 3, 23, ACM, 2016, doi:10.1145/2857050.","ista":"Chonev VK, Ouaknine J, Worrell J. 2016. On the complexity of the orbit problem. Journal of the ACM. 63(3), 23.","chicago":"Chonev, Ventsislav K, Joël Ouaknine, and James Worrell. “On the Complexity of the Orbit Problem.” Journal of the ACM. ACM, 2016. https://doi.org/10.1145/2857050."},"status":"public","type":"journal_article","article_number":"23","_id":"1380"},{"_id":"1389","conference":{"start_date":"2018-07-05","location":"New York, NY, USA","end_date":"2018-07-08","name":"LICS: Logic in Computer Science"},"type":"conference","project":[{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989"}],"status":"public","date_updated":"2021-01-12T06:50:20Z","citation":{"ama":"Chonev VK, Ouaknine J, Worrell J. On recurrent reachability for continuous linear dynamical systems. In: LICS ’16. IEEE; 2016:515-524. doi:10.1145/2933575.2934548","apa":"Chonev, V. K., Ouaknine, J., & Worrell, J. (2016). On recurrent reachability for continuous linear dynamical systems. In LICS ’16 (pp. 515–524). New York, NY, USA: IEEE. https://doi.org/10.1145/2933575.2934548","ieee":"V. K. Chonev, J. Ouaknine, and J. Worrell, “On recurrent reachability for continuous linear dynamical systems,” in LICS ’16, New York, NY, USA, 2016, pp. 515–524.","short":"V.K. Chonev, J. Ouaknine, J. Worrell, in:, LICS ’16, IEEE, 2016, pp. 515–524.","mla":"Chonev, Ventsislav K., et al. “On Recurrent Reachability for Continuous Linear Dynamical Systems.” LICS ’16, IEEE, 2016, pp. 515–24, doi:10.1145/2933575.2934548.","ista":"Chonev VK, Ouaknine J, Worrell J. 2016. On recurrent reachability for continuous linear dynamical systems. LICS ’16. LICS: Logic in Computer Science, 515–524.","chicago":"Chonev, Ventsislav K, Joël Ouaknine, and James Worrell. “On Recurrent Reachability for Continuous Linear Dynamical Systems.” In LICS ’16, 515–24. IEEE, 2016. https://doi.org/10.1145/2933575.2934548."},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","author":[{"first_name":"Ventsislav K","id":"36CBE2E6-F248-11E8-B48F-1D18A9856A87","full_name":"Chonev, Ventsislav K","last_name":"Chonev"},{"first_name":"Joël","full_name":"Ouaknine, Joël","last_name":"Ouaknine"},{"first_name":"James","full_name":"Worrell, James","last_name":"Worrell"}],"publist_id":"5820","department":[{"_id":"KrCh"}],"title":"On recurrent reachability for continuous linear dynamical systems","abstract":[{"text":"The continuous evolution of a wide variety of systems, including continous-time Markov chains and linear hybrid automata, can be\r\ndescribed in terms of linear differential equations. In this paper we study the decision problem of whether the solution x(t) of a system of linear differential equations dx/dt = Ax reaches a target halfspace infinitely often. This recurrent reachability problem can\r\nequivalently be formulated as the following Infinite Zeros Problem: does a real-valued function f:R≥0 --> R satisfying a given linear\r\ndifferential equation have infinitely many zeros? Our main decidability result is that if the differential equation has order at most 7, then the Infinite Zeros Problem is decidable. On the other hand, we show that a decision procedure for the Infinite Zeros Problem at order 9 (and above) would entail a major breakthrough in Diophantine Approximation, specifically an algorithm for computing the Lagrange constants of arbitrary real algebraic numbers to arbitrary precision.","lang":"eng"}],"oa_version":"Preprint","oa":1,"main_file_link":[{"url":"https://arxiv.org/abs/1507.03632","open_access":"1"}],"publisher":"IEEE","scopus_import":1,"quality_controlled":"1","month":"07","year":"2016","publication_status":"published","language":[{"iso":"eng"}],"publication":"LICS '16","day":"05","page":"515 - 524","date_created":"2018-12-11T11:51:44Z","ec_funded":1,"date_published":"2016-07-05T00:00:00Z","doi":"10.1145/2933575.2934548"}]