[{"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"isi":1,"ddc":["510"],"year":"2021","doi":"10.23638/LMCS-17(1:10)2021","external_id":{"isi":["000658724600010"],"arxiv":["1905.03588"]},"title":"Determinacy in discrete-bidding infinite-duration games","arxiv":1,"article_processing_charge":"No","oa":1,"date_updated":"2023-08-17T06:56:42Z","volume":17,"publication_identifier":{"eissn":["1860-5974"]},"_id":"10674","oa_version":"Published Version","project":[{"grant_number":"M02369","_id":"264B3912-B435-11E9-9278-68D0E5697425","name":"Formal Methods meets Algorithmic Game Theory","call_identifier":"FWF"},{"grant_number":"S11402-N23","name":"Rigorous Systems Engineering","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"Z211","call_identifier":"FWF","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","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","citation":{"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>","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>.","short":"M. Aghajohari, G. Avni, T.A. Henzinger, Logical Methods in Computer Science 17 (2021) 10:1-10:23.","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.","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>","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.","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>."},"publication_status":"published","abstract":[{"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.","lang":"eng"}],"author":[{"last_name":"Aghajohari","full_name":"Aghajohari, Milad","first_name":"Milad"},{"id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5588-8287","last_name":"Avni","full_name":"Avni, Guy","first_name":"Guy"},{"first_name":"Thomas A","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"keyword":["computer science","computer science and game theory","logic in computer science"],"has_accepted_license":"1","department":[{"_id":"ToHe"}],"file":[{"date_updated":"2022-01-26T08:04:50Z","access_level":"open_access","date_created":"2022-01-26T08:04:50Z","checksum":"b35586a50ed1ca8f44767de116d18d81","file_name":"2021_LMCS_AGHAJOHAR.pdf","file_size":819878,"file_id":"10690","creator":"alisjak","content_type":"application/pdf","relation":"main_file","success":1}],"date_created":"2022-01-25T16:32:13Z","month":"02","article_type":"original","date_published":"2021-02-03T00:00:00Z","scopus_import":"1","publisher":"International Federation for Computational Logic","language":[{"iso":"eng"}],"publication":"Logical Methods in Computer Science","issue":"1","file_date_updated":"2022-01-26T08:04:50Z","page":"10:1-10:23","day":"03","type":"journal_article","intvolume":"        17","status":"public"},{"author":[{"first_name":"Martin","full_name":"Zeiner, Martin","last_name":"Zeiner"},{"first_name":"Ulrich","full_name":"Schmid, Ulrich","last_name":"Schmid"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"}],"abstract":[{"text":"We study optimal election sequences for repeatedly selecting a (very) small group of leaders among a set of participants (players) with publicly known unique ids. In every time slot, every player has to select exactly one player that it considers to be the current leader, oblivious to the selection of the other players, but with the overarching goal of maximizing a given parameterized global (“social”) payoff function in the limit. We consider a quite generic model, where the local payoff achieved by a given player depends, weighted by some arbitrary but fixed real parameter, on the number of different leaders chosen in a round, the number of players that choose the given player as the leader, and whether the chosen leader has changed w.r.t. the previous round or not. The social payoff can be the maximum, average or minimum local payoff of the players. Possible applications include quite diverse examples such as rotating coordinator-based distributed algorithms and long-haul formation flying of social birds. Depending on the weights and the particular social payoff, optimal sequences can be very different, from simple round-robin where all players chose the same leader alternatingly every time slot to very exotic patterns, where a small group of leaders (at most 2) is elected in every time slot. Moreover, we study the question if and when a single player would not benefit w.r.t. its local payoff when deviating from the given optimal sequence, i.e., when our optimal sequences are Nash equilibria in the restricted strategy space of oblivious strategies. As this is the case for many parameterizations of our model, our results reveal that no punishment is needed to make it rational for the players to optimize the social payoff.","lang":"eng"}],"publication_status":"published","citation":{"ista":"Zeiner M, Schmid U, Chatterjee K. 2021. Optimal strategies for selecting coordinators. Discrete Applied Mathematics. 289(1), 392–415.","short":"M. Zeiner, U. Schmid, K. Chatterjee, Discrete Applied Mathematics 289 (2021) 392–415.","mla":"Zeiner, Martin, et al. “Optimal Strategies for Selecting Coordinators.” <i>Discrete Applied Mathematics</i>, vol. 289, no. 1, Elsevier, 2021, pp. 392–415, doi:<a href=\"https://doi.org/10.1016/j.dam.2020.10.022\">10.1016/j.dam.2020.10.022</a>.","ama":"Zeiner M, Schmid U, Chatterjee K. Optimal strategies for selecting coordinators. <i>Discrete Applied Mathematics</i>. 2021;289(1):392-415. doi:<a href=\"https://doi.org/10.1016/j.dam.2020.10.022\">10.1016/j.dam.2020.10.022</a>","chicago":"Zeiner, Martin, Ulrich Schmid, and Krishnendu Chatterjee. “Optimal Strategies for Selecting Coordinators.” <i>Discrete Applied Mathematics</i>. Elsevier, 2021. <a href=\"https://doi.org/10.1016/j.dam.2020.10.022\">https://doi.org/10.1016/j.dam.2020.10.022</a>.","apa":"Zeiner, M., Schmid, U., &#38; Chatterjee, K. (2021). Optimal strategies for selecting coordinators. <i>Discrete Applied Mathematics</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.dam.2020.10.022\">https://doi.org/10.1016/j.dam.2020.10.022</a>","ieee":"M. Zeiner, U. Schmid, and K. Chatterjee, “Optimal strategies for selecting coordinators,” <i>Discrete Applied Mathematics</i>, vol. 289, no. 1. Elsevier, pp. 392–415, 2021."},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","acknowledgement":"We are grateful to Matthias Függer and Thomas Nowak for having raised our interest in the problem studied in this paper.\r\nThis work has been supported the Austrian Science Fund (FWF) projects S11405, S11407 (RiSE), and P28182 (ADynNet).","oa_version":"Published Version","quality_controlled":"1","project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"},{"name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11407"}],"_id":"8793","publication_identifier":{"issn":["0166218X"]},"oa":1,"date_updated":"2023-08-04T11:12:41Z","volume":289,"article_processing_charge":"No","external_id":{"isi":["000596823800035"]},"title":"Optimal strategies for selecting coordinators","doi":"10.1016/j.dam.2020.10.022","year":"2021","ddc":["510"],"isi":1,"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"status":"public","intvolume":"       289","type":"journal_article","day":"31","file_date_updated":"2021-02-04T11:28:42Z","page":"392-415","issue":"1","publication":"Discrete Applied Mathematics","language":[{"iso":"eng"}],"publisher":"Elsevier","scopus_import":"1","date_published":"2021-01-31T00:00:00Z","article_type":"original","month":"01","file":[{"creator":"dernst","file_id":"9089","content_type":"application/pdf","relation":"main_file","success":1,"date_updated":"2021-02-04T11:28:42Z","access_level":"open_access","date_created":"2021-02-04T11:28:42Z","checksum":"f1039ff5a2d6ca116720efdb84ee9d5e","file_name":"2021_DiscreteApplMath_Zeiner.pdf","file_size":652739}],"date_created":"2020-11-22T23:01:26Z","department":[{"_id":"KrCh"}],"has_accepted_license":"1"},{"file_date_updated":"2021-11-09T09:00:50Z","page":"166","supervisor":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"}],"status":"public","day":"31","type":"dissertation","file":[{"access_level":"open_access","date_updated":"2021-11-08T14:12:22Z","checksum":"4f412a1ee60952221b499a4b1268df35","date_created":"2021-11-08T14:12:22Z","file_size":2915234,"file_name":"toman_th_final.pdf","file_id":"10225","creator":"vtoman","relation":"main_file","content_type":"application/pdf"},{"date_updated":"2021-11-09T09:00:50Z","access_level":"closed","date_created":"2021-11-08T14:12:46Z","checksum":"9584943f99127be2dd2963f6784c37d4","file_name":"toman_thesis.zip","file_size":8616056,"creator":"vtoman","file_id":"10226","content_type":"application/zip","relation":"source_file"}],"date_created":"2021-10-29T20:09:01Z","degree_awarded":"PhD","has_accepted_license":"1","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"publisher":"Institute of Science and Technology Austria","language":[{"iso":"eng"}],"month":"10","date_published":"2021-10-31T00:00:00Z","publication_identifier":{"issn":["2663-337X"]},"_id":"10199","project":[{"call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","name":"International IST Doctoral Program","grant_number":"665385"},{"grant_number":"S11402-N23","name":"Rigorous Systems Engineering","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020"}],"oa_version":"Published Version","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","article_processing_charge":"No","date_updated":"2025-07-14T09:10:16Z","oa":1,"abstract":[{"text":"The design and verification of concurrent systems remains an open challenge due to the non-determinism that arises from the inter-process communication. In particular, concurrent programs are notoriously difficult both to be written correctly and to be analyzed formally, as complex thread interaction has to be accounted for. The difficulties are further exacerbated when concurrent programs get executed on modern-day hardware, which contains various buffering and caching mechanisms for efficiency reasons. This causes further subtle non-determinism, which can often produce very unintuitive behavior of the concurrent programs. Model checking is at the forefront of tackling the verification problem, where the task is to decide, given as input a concurrent system and a desired property, whether the system satisfies the property. The inherent state-space explosion problem in model checking of concurrent systems causes naïve explicit methods not to scale, thus more inventive methods are required. One such method is stateless model checking (SMC), which explores in memory-efficient manner the program executions rather than the states of the program. State-of-the-art SMC is typically coupled with partial order reduction (POR) techniques, which argue that certain executions provably produce identical system behavior, thus limiting the amount of executions one needs to explore in order to cover all possible behaviors. Another method to tackle the state-space explosion is symbolic model checking, where the considered techniques operate on a succinct implicit representation of the input system rather than explicitly accessing the system. In this thesis we present new techniques for verification of concurrent systems. We present several novel POR methods for SMC of concurrent programs under various models of semantics, some of which account for write-buffering mechanisms. Additionally, we present novel algorithms for symbolic model checking of finite-state concurrent systems, where the desired property of the systems is to ensure a formally defined notion of fairness.","lang":"eng"}],"keyword":["concurrency","verification","model checking"],"author":[{"first_name":"Viktor","orcid":"0000-0001-9036-063X","last_name":"Toman","full_name":"Toman, Viktor","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87"}],"citation":{"chicago":"Toman, Viktor. “Improved Verification Techniques for Concurrent Systems.” Institute of Science and Technology Austria, 2021. <a href=\"https://doi.org/10.15479/at:ista:10199\">https://doi.org/10.15479/at:ista:10199</a>.","apa":"Toman, V. (2021). <i>Improved verification techniques for concurrent systems</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/at:ista:10199\">https://doi.org/10.15479/at:ista:10199</a>","ieee":"V. Toman, “Improved verification techniques for concurrent systems,” Institute of Science and Technology Austria, 2021.","short":"V. Toman, Improved Verification Techniques for Concurrent Systems, Institute of Science and Technology Austria, 2021.","ista":"Toman V. 2021. Improved verification techniques for concurrent systems. Institute of Science and Technology Austria.","mla":"Toman, Viktor. <i>Improved Verification Techniques for Concurrent Systems</i>. Institute of Science and Technology Austria, 2021, doi:<a href=\"https://doi.org/10.15479/at:ista:10199\">10.15479/at:ista:10199</a>.","ama":"Toman V. Improved verification techniques for concurrent systems. 2021. doi:<a href=\"https://doi.org/10.15479/at:ista:10199\">10.15479/at:ista:10199</a>"},"publication_status":"published","related_material":{"record":[{"status":"public","relation":"part_of_dissertation","id":"10190"},{"status":"public","relation":"part_of_dissertation","id":"9987"},{"status":"public","relation":"part_of_dissertation","id":"141"},{"status":"public","relation":"part_of_dissertation","id":"10191"}]},"ddc":["000"],"alternative_title":["ISTA Thesis"],"title":"Improved verification techniques for concurrent systems","doi":"10.15479/at:ista:10199","year":"2021","acknowledged_ssus":[{"_id":"SSU"}],"ec_funded":1},{"language":[{"iso":"eng"}],"scopus_import":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_published":"2020-08-06T00:00:00Z","month":"08","file":[{"access_level":"open_access","date_updated":"2020-10-05T14:04:25Z","checksum":"5039752f644c4b72b9361d21a5e31baf","date_created":"2020-10-05T14:04:25Z","file_size":601231,"file_name":"2020_LIPIcsCONCUR_Chatterjee.pdf","file_id":"8610","creator":"dernst","relation":"main_file","content_type":"application/pdf","success":1}],"date_created":"2020-10-04T22:01:36Z","conference":{"end_date":"2020-09-04","location":"Virtual","name":"CONCUR: Conference on Concurrency Theory","start_date":"2020-09-01"},"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"has_accepted_license":"1","license":"https://creativecommons.org/licenses/by/3.0/","status":"public","intvolume":"       171","type":"conference","day":"06","file_date_updated":"2020-10-05T14:04:25Z","publication":"31st International Conference on Concurrency Theory","external_id":{"arxiv":["2007.08917"]},"title":"Multi-dimensional long-run average problems for vector addition systems with states","year":"2020","doi":"10.4230/LIPIcs.CONCUR.2020.23","ddc":["000"],"article_number":"23","tmp":{"name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)","short":"CC BY (3.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode"},"alternative_title":["LIPIcs"],"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu"},{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Jan","full_name":"Otop, Jan","last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"abstract":[{"text":"A vector addition system with states (VASS) consists of a finite set of states and counters. A transition changes the current state to the next state, and every counter is either incremented, or decremented, or left unchanged. A state and value for each counter is a configuration; and a computation is an infinite sequence of configurations with transitions between successive configurations. A probabilistic VASS consists of a VASS along with a probability distribution over the transitions for each state. Qualitative properties such as state and configuration reachability have been widely studied for VASS. In this work we consider multi-dimensional long-run average objectives for VASS and probabilistic VASS. For a counter, the cost of a configuration is the value of the counter; and the long-run average value of a computation for the counter is the long-run average of the costs of the configurations in the computation. The multi-dimensional long-run average problem given a VASS and a threshold value for each counter, asks whether there is a computation such that for each counter the long-run average value for the counter does not exceed the respective threshold. For probabilistic VASS, instead of the existence of a computation, we consider whether the expected long-run average value for each counter does not exceed the respective threshold. Our main results are as follows: we show that the multi-dimensional long-run average problem (a) is NP-complete for integer-valued VASS; (b) is undecidable for natural-valued VASS (i.e., nonnegative counters); and (c) can be solved in polynomial time for probabilistic integer-valued VASS, and probabilistic natural-valued VASS when all computations are non-terminating.","lang":"eng"}],"citation":{"apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2020). Multi-dimensional long-run average problems for vector addition systems with states. In <i>31st International Conference on Concurrency Theory</i> (Vol. 171). Virtual: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2020.23\">https://doi.org/10.4230/LIPIcs.CONCUR.2020.23</a>","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Multi-dimensional long-run average problems for vector addition systems with states,” in <i>31st International Conference on Concurrency Theory</i>, Virtual, 2020, vol. 171.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Multi-Dimensional Long-Run Average Problems for Vector Addition Systems with States.” In <i>31st International Conference on Concurrency Theory</i>, Vol. 171. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2020.23\">https://doi.org/10.4230/LIPIcs.CONCUR.2020.23</a>.","mla":"Chatterjee, Krishnendu, et al. “Multi-Dimensional Long-Run Average Problems for Vector Addition Systems with States.” <i>31st International Conference on Concurrency Theory</i>, vol. 171, 23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2020.23\">10.4230/LIPIcs.CONCUR.2020.23</a>.","ama":"Chatterjee K, Henzinger TA, Otop J. Multi-dimensional long-run average problems for vector addition systems with states. In: <i>31st International Conference on Concurrency Theory</i>. Vol 171. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2020. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2020.23\">10.4230/LIPIcs.CONCUR.2020.23</a>","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, 31st International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.","ista":"Chatterjee K, Henzinger TA, Otop J. 2020. Multi-dimensional long-run average problems for vector addition systems with states. 31st International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 171, 23."},"publication_status":"published","project":[{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23"},{"name":"Rigorous Systems Engineering","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11402-N23"},{"grant_number":"Z211","call_identifier":"FWF","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"oa_version":"Published Version","quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_identifier":{"issn":["18688969"],"isbn":["9783959771603"]},"_id":"8600","article_processing_charge":"No","oa":1,"volume":171,"date_updated":"2021-01-12T08:20:15Z","arxiv":1},{"language":[{"iso":"eng"}],"publisher":"Elsevier","scopus_import":"1","article_type":"original","date_published":"2020-02-06T00:00:00Z","month":"02","date_created":"2019-08-04T21:59:20Z","file":[{"checksum":"e86635417f45eb2cd75778f91382f737","date_created":"2020-10-09T06:31:22Z","file_size":1413001,"file_name":"2020_TheoreticalCS_Avni.pdf","access_level":"open_access","date_updated":"2020-10-09T06:31:22Z","success":1,"file_id":"8639","creator":"dernst","relation":"main_file","content_type":"application/pdf"}],"department":[{"_id":"ToHe"}],"has_accepted_license":"1","status":"public","intvolume":"       807","type":"journal_article","day":"06","file_date_updated":"2020-10-09T06:31:22Z","page":"42-55","publication":"Theoretical Computer Science","title":"Dynamic resource allocation games","external_id":{"isi":["000512219400004"]},"doi":"10.1016/j.tcs.2019.06.031","year":"2020","ddc":["000"],"related_material":{"record":[{"status":"public","id":"1341","relation":"earlier_version"}]},"isi":1,"author":[{"id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","first_name":"Guy","full_name":"Avni, Guy","last_name":"Avni","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"},{"last_name":"Kupferman","full_name":"Kupferman, Orna","first_name":"Orna"}],"abstract":[{"lang":"eng","text":"In resource allocation games, selfish players share resources that are needed in order to fulfill their objectives. The cost of using a resource depends on the load on it. In the traditional setting, the players make their choices concurrently and in one-shot. That is, a strategy for a player is a subset of the resources. We introduce and study dynamic resource allocation games. In this setting, the game proceeds in phases. In each phase each player chooses one resource. A scheduler dictates the order in which the players proceed in a phase, possibly scheduling several players to proceed concurrently. The game ends when each player has collected a set of resources that fulfills his objective. The cost for each player then depends on this set as well as on the load on the resources in it – we consider both congestion and cost-sharing games. We argue that the dynamic setting is the suitable setting for many applications in practice. We study the stability of dynamic resource allocation games, where the appropriate notion of stability is that of subgame perfect equilibrium, study the inefficiency incurred due to selfish behavior, and also study problems that are particular to the dynamic setting, like constraints on the order in which resources can be chosen or the problem of finding a scheduler that achieves stability."}],"publication_status":"published","citation":{"ista":"Avni G, Henzinger TA, Kupferman O. 2020. Dynamic resource allocation games. Theoretical Computer Science. 807, 42–55.","short":"G. Avni, T.A. Henzinger, O. Kupferman, Theoretical Computer Science 807 (2020) 42–55.","mla":"Avni, Guy, et al. “Dynamic Resource Allocation Games.” <i>Theoretical Computer Science</i>, vol. 807, Elsevier, 2020, pp. 42–55, doi:<a href=\"https://doi.org/10.1016/j.tcs.2019.06.031\">10.1016/j.tcs.2019.06.031</a>.","ama":"Avni G, Henzinger TA, Kupferman O. Dynamic resource allocation games. <i>Theoretical Computer Science</i>. 2020;807:42-55. doi:<a href=\"https://doi.org/10.1016/j.tcs.2019.06.031\">10.1016/j.tcs.2019.06.031</a>","chicago":"Avni, Guy, Thomas A Henzinger, and Orna Kupferman. “Dynamic Resource Allocation Games.” <i>Theoretical Computer Science</i>. Elsevier, 2020. <a href=\"https://doi.org/10.1016/j.tcs.2019.06.031\">https://doi.org/10.1016/j.tcs.2019.06.031</a>.","apa":"Avni, G., Henzinger, T. A., &#38; Kupferman, O. (2020). Dynamic resource allocation games. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2019.06.031\">https://doi.org/10.1016/j.tcs.2019.06.031</a>","ieee":"G. Avni, T. A. Henzinger, and O. Kupferman, “Dynamic resource allocation games,” <i>Theoretical Computer Science</i>, vol. 807. Elsevier, pp. 42–55, 2020."},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","quality_controlled":"1","project":[{"grant_number":"S11402-N23","call_identifier":"FWF","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"},{"name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211"},{"grant_number":"M02369","name":"Formal Methods meets Algorithmic Game Theory","_id":"264B3912-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"oa_version":"Submitted Version","_id":"6761","publication_identifier":{"issn":["03043975"]},"oa":1,"volume":807,"date_updated":"2023-08-17T13:52:49Z","article_processing_charge":"No"},{"file_date_updated":"2020-07-14T12:47:56Z","publication":"28th EACSL Annual Conference on Computer Science Logic","type":"conference","day":"15","status":"public","intvolume":"       152","department":[{"_id":"ToHe"}],"has_accepted_license":"1","date_created":"2020-01-21T11:22:21Z","file":[{"relation":"main_file","content_type":"application/pdf","creator":"bkragl","file_id":"7349","file_size":617206,"file_name":"main.pdf","checksum":"b9a691d658d075c6369d3304d17fb818","date_created":"2020-01-21T11:21:04Z","access_level":"open_access","date_updated":"2020-07-14T12:47:56Z"}],"conference":{"name":"CSL: Computer Science Logic","end_date":"2020-01-16","location":"Barcelona, Spain","start_date":"2020-01-13"},"date_published":"2020-01-15T00:00:00Z","month":"01","language":[{"iso":"eng"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","scopus_import":1,"volume":152,"oa":1,"date_updated":"2021-01-12T08:13:12Z","article_processing_charge":"No","arxiv":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","project":[{"grant_number":"S11402-N23","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"}],"oa_version":"Published Version","_id":"7348","publication_identifier":{"issn":["1868-8969"],"isbn":["9783959771320"]},"publication_status":"published","citation":{"chicago":"Ferrere, Thomas, Thomas A Henzinger, and Bernhard Kragl. “Monitoring Event Frequencies.” In <i>28th EACSL Annual Conference on Computer Science Logic</i>, Vol. 152. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. <a href=\"https://doi.org/10.4230/LIPIcs.CSL.2020.20\">https://doi.org/10.4230/LIPIcs.CSL.2020.20</a>.","ieee":"T. Ferrere, T. A. Henzinger, and B. Kragl, “Monitoring event frequencies,” in <i>28th EACSL Annual Conference on Computer Science Logic</i>, Barcelona, Spain, 2020, vol. 152.","apa":"Ferrere, T., Henzinger, T. A., &#38; Kragl, B. (2020). Monitoring event frequencies. In <i>28th EACSL Annual Conference on Computer Science Logic</i> (Vol. 152). Barcelona, Spain: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CSL.2020.20\">https://doi.org/10.4230/LIPIcs.CSL.2020.20</a>","short":"T. Ferrere, T.A. Henzinger, B. Kragl, in:, 28th EACSL Annual Conference on Computer Science Logic, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.","ista":"Ferrere T, Henzinger TA, Kragl B. 2020. Monitoring event frequencies. 28th EACSL Annual Conference on Computer Science Logic. CSL: Computer Science Logic, LIPIcs, vol. 152, 20.","ama":"Ferrere T, Henzinger TA, Kragl B. Monitoring event frequencies. In: <i>28th EACSL Annual Conference on Computer Science Logic</i>. Vol 152. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2020. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CSL.2020.20\">10.4230/LIPIcs.CSL.2020.20</a>","mla":"Ferrere, Thomas, et al. “Monitoring Event Frequencies.” <i>28th EACSL Annual Conference on Computer Science Logic</i>, vol. 152, 20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CSL.2020.20\">10.4230/LIPIcs.CSL.2020.20</a>."},"author":[{"id":"40960E6E-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas","orcid":"0000-0001-5199-3143","last_name":"Ferrere","full_name":"Ferrere, Thomas"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"320FC952-F248-11E8-B48F-1D18A9856A87","full_name":"Kragl, Bernhard","last_name":"Kragl","orcid":"0000-0001-7745-9117","first_name":"Bernhard"}],"abstract":[{"text":"The monitoring of event frequencies can be used to recognize behavioral anomalies, to identify trends, and to deduce or discard hypotheses about the underlying system. For example, the performance of a web server may be monitored based on the ratio of the total count of requests from the least and most active clients. Exact frequency monitoring, however, can be prohibitively expensive; in the above example it would require as many counters as there are clients. In this paper, we propose the efficient probabilistic monitoring of common frequency properties, including the mode (i.e., the most common event) and the median of an event sequence. We define a logic to express composite frequency properties as a combination of atomic frequency properties. Our main contribution is an algorithm that, under suitable probabilistic assumptions, can be used to monitor these important frequency properties with four counters, independent of the number of different events. Our algorithm samples longer and longer subwords of an infinite event sequence. We prove the almost-sure convergence of our algorithm by generalizing ergodic theory from increasing-length prefixes to increasing-length subwords of an infinite sequence. A similar algorithm could be used to learn a connected Markov chain of a given structure from observing its outputs, to arbitrary precision, for a given confidence. ","lang":"eng"}],"article_number":"20","alternative_title":["LIPIcs"],"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"ddc":["000"],"year":"2020","doi":"10.4230/LIPIcs.CSL.2020.20","title":"Monitoring event frequencies","external_id":{"arxiv":["1910.06097"]}},{"page":"1798-1805","issue":"02","publication":"Proceedings of the AAAI Conference on Artificial Intelligence","type":"journal_article","day":"03","status":"public","intvolume":"        34","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"date_created":"2021-02-25T09:05:18Z","conference":{"location":"New York, NY, United States","end_date":"2020-02-12","name":"AAAI: Conference on Artificial Intelligence","start_date":"2020-02-07"},"date_published":"2020-04-03T00:00:00Z","article_type":"original","month":"04","language":[{"iso":"eng"}],"publisher":"Association for the Advancement of Artificial Intelligence","scopus_import":"1","date_updated":"2023-09-05T12:40:00Z","volume":34,"article_processing_charge":"No","arxiv":1,"acknowledgement":"This research was supported by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE), Z211-N23 (Wittgenstein Award), and M 2369-N33 (Meitner fellowship).","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","project":[{"grant_number":"S11402-N23","call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"},{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Formal Methods meets Algorithmic Game Theory","_id":"264B3912-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"M02369"}],"oa_version":"Preprint","quality_controlled":"1","_id":"9197","publication_identifier":{"isbn":["9781577358350"],"issn":["2159-5399"],"eissn":["2374-3468"]},"publication_status":"published","citation":{"ieee":"G. Avni, R. Ibsen-Jensen, and J. Tkadlec, “All-pay bidding games on graphs,” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, vol. 34, no. 02. Association for the Advancement of Artificial Intelligence, pp. 1798–1805, 2020.","apa":"Avni, G., Ibsen-Jensen, R., &#38; Tkadlec, J. (2020). All-pay bidding games on graphs. <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. New York, NY, United States: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v34i02.5546\">https://doi.org/10.1609/aaai.v34i02.5546</a>","chicago":"Avni, Guy, Rasmus Ibsen-Jensen, and Josef Tkadlec. “All-Pay Bidding Games on Graphs.” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. Association for the Advancement of Artificial Intelligence, 2020. <a href=\"https://doi.org/10.1609/aaai.v34i02.5546\">https://doi.org/10.1609/aaai.v34i02.5546</a>.","mla":"Avni, Guy, et al. “All-Pay Bidding Games on Graphs.” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, vol. 34, no. 02, Association for the Advancement of Artificial Intelligence, 2020, pp. 1798–805, doi:<a href=\"https://doi.org/10.1609/aaai.v34i02.5546\">10.1609/aaai.v34i02.5546</a>.","ama":"Avni G, Ibsen-Jensen R, Tkadlec J. All-pay bidding games on graphs. <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. 2020;34(02):1798-1805. doi:<a href=\"https://doi.org/10.1609/aaai.v34i02.5546\">10.1609/aaai.v34i02.5546</a>","short":"G. Avni, R. Ibsen-Jensen, J. Tkadlec, Proceedings of the AAAI Conference on Artificial Intelligence 34 (2020) 1798–1805.","ista":"Avni G, Ibsen-Jensen R, Tkadlec J. 2020. All-pay bidding games on graphs. Proceedings of the AAAI Conference on Artificial Intelligence. 34(02), 1798–1805."},"author":[{"first_name":"Guy","last_name":"Avni","full_name":"Avni, Guy","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus","last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389"},{"first_name":"Josef","orcid":"0000-0002-1097-9684","full_name":"Tkadlec, Josef","last_name":"Tkadlec","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87"}],"abstract":[{"lang":"eng","text":"In this paper we introduce and study all-pay bidding games, a class of two player, zero-sum games on graphs. The game proceeds as follows. We place a token on some vertex in the graph and assign budgets to the two players. Each turn, each player submits a sealed legal bid (non-negative and below their remaining budget), which is deducted from their budget and the highest bidder moves the token onto an adjacent vertex. The game ends once a sink is reached, and Player 1 pays Player 2 the outcome that is associated with the sink. The players attempt to maximize their expected outcome. Our games model settings where effort (of no inherent value) needs to be invested in an ongoing and stateful manner. On the negative side, we show that even in simple games on DAGs, optimal strategies may require a distribution over bids with infinite support. A central quantity in bidding games is the ratio of the players budgets. On the positive side, we show a simple FPTAS for DAGs, that, for each budget ratio, outputs an approximation for the optimal strategy for that ratio. We also implement it, show that it performs well, and suggests interesting properties of these games. Then, given an outcome c, we show an algorithm for finding the necessary and sufficient initial ratio for guaranteeing outcome c with probability 1 and a strategy ensuring such. Finally, while the general case has not previously been studied, solving the specific game in which Player 1 wins iff he wins the first two auctions, has been long stated as an open question, which we solve."}],"year":"2020","doi":"10.1609/aaai.v34i02.5546","external_id":{"arxiv":["1911.08360"]},"title":"All-pay bidding games on graphs"},{"status":"public","intvolume":"        66","type":"journal_article","day":"16","publication":"Journal of the ACM","issue":"4","language":[{"iso":"eng"}],"scopus_import":"1","publisher":"ACM","date_published":"2019-07-16T00:00:00Z","month":"07","date_created":"2019-08-04T21:59:16Z","department":[{"_id":"ToHe"}],"author":[{"id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","first_name":"Guy","orcid":"0000-0001-5588-8287","last_name":"Avni","full_name":"Avni, Guy"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"id":"36CBE2E6-F248-11E8-B48F-1D18A9856A87","first_name":"Ventsislav K","full_name":"Chonev, Ventsislav K","last_name":"Chonev"}],"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."}],"citation":{"ista":"Avni G, Henzinger TA, Chonev VK. 2019. Infinite-duration bidding games. Journal of the ACM. 66(4), 31.","short":"G. Avni, T.A. Henzinger, V.K. Chonev, Journal of the ACM 66 (2019).","ama":"Avni G, Henzinger TA, Chonev VK. Infinite-duration bidding games. <i>Journal of the ACM</i>. 2019;66(4). doi:<a href=\"https://doi.org/10.1145/3340295\">10.1145/3340295</a>","mla":"Avni, Guy, et al. “Infinite-Duration Bidding Games.” <i>Journal of the ACM</i>, vol. 66, no. 4, 31, ACM, 2019, doi:<a href=\"https://doi.org/10.1145/3340295\">10.1145/3340295</a>.","chicago":"Avni, Guy, Thomas A Henzinger, and Ventsislav K Chonev. “Infinite-Duration Bidding Games.” <i>Journal of the ACM</i>. ACM, 2019. <a href=\"https://doi.org/10.1145/3340295\">https://doi.org/10.1145/3340295</a>.","ieee":"G. Avni, T. A. Henzinger, and V. K. Chonev, “Infinite-duration bidding games,” <i>Journal of the ACM</i>, vol. 66, no. 4. ACM, 2019.","apa":"Avni, G., Henzinger, T. A., &#38; Chonev, V. K. (2019). Infinite-duration bidding games. <i>Journal of the ACM</i>. ACM. <a href=\"https://doi.org/10.1145/3340295\">https://doi.org/10.1145/3340295</a>"},"publication_status":"published","quality_controlled":"1","oa_version":"Preprint","project":[{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","call_identifier":"FWF"},{"_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S11402-N23"},{"call_identifier":"FWF","_id":"264B3912-B435-11E9-9278-68D0E5697425","name":"Formal Methods meets Algorithmic Game Theory","grant_number":"M02369"}],"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","publication_identifier":{"eissn":["1557735X"],"issn":["00045411"]},"_id":"6752","article_processing_charge":"No","volume":66,"date_updated":"2023-08-29T07:02:13Z","oa":1,"arxiv":1,"external_id":{"isi":["000487714900008"],"arxiv":["1705.01433"]},"title":"Infinite-duration bidding games","doi":"10.1145/3340295","year":"2019","related_material":{"record":[{"status":"public","id":"950","relation":"earlier_version"}]},"main_file_link":[{"url":"https://arxiv.org/abs/1705.01433","open_access":"1"}],"article_number":"31","isi":1},{"status":"public","intvolume":"     11674","type":"conference","day":"06","file_date_updated":"2020-07-14T12:47:41Z","page":"1-12","publication":" Proceedings of the 13th International Conference of Reachability Problems","language":[{"iso":"eng"}],"scopus_import":1,"publisher":"Springer","date_published":"2019-09-06T00:00:00Z","month":"09","file":[{"file_id":"6823","creator":"gavni","content_type":"application/pdf","relation":"main_file","date_updated":"2020-07-14T12:47:41Z","access_level":"open_access","date_created":"2019-08-19T07:56:40Z","checksum":"45ebbc709af2b247d28c7c293c01504b","file_name":"prob.pdf","file_size":436635}],"date_created":"2019-08-19T07:58:10Z","conference":{"end_date":"2019-09-13","location":"Brussels, Belgium","name":"RP: Reachability Problems","start_date":"2019-09-11"},"department":[{"_id":"ToHe"}],"has_accepted_license":"1","author":[{"last_name":"Avni","full_name":"Avni, Guy","orcid":"0000-0001-5588-8287","first_name":"Guy","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Thomas A","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389","first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Novotny, Petr","last_name":"Novotny","first_name":"Petr"}],"abstract":[{"text":"In two-player games on graphs, the players move a token through a graph to produce an infinite path, which determines the qualitative winner or quantitative payoff of the game. In bidding games, in each turn, we hold an auction between the two players to determine which player moves the token. Bidding games have largely been studied with concrete bidding mechanisms that are variants of a first-price auction: in each turn both players simultaneously submit bids, the higher\r\nbidder moves the token, and pays his bid to the lower bidder in Richman bidding, to the bank in poorman bidding, and in taxman bidding, the bid is split between the other player and the bank according to a predefined constant factor. Bidding games are deterministic games. They have an intriguing connection with a fragment of stochastic games called \r\n randomturn games. We study, for the first time, a combination of bidding games with probabilistic behavior; namely, we study bidding games that are played on Markov decision processes, where the players bid for the right to choose the next action, which determines the probability distribution according to which the next vertex is chosen. We study parity and meanpayoff bidding games on MDPs and extend results from the deterministic bidding setting to the probabilistic one.","lang":"eng"}],"citation":{"apa":"Avni, G., Henzinger, T. A., Ibsen-Jensen, R., &#38; Novotny, P. (2019). Bidding games on Markov decision processes. In <i> Proceedings of the 13th International Conference of Reachability Problems</i> (Vol. 11674, pp. 1–12). Brussels, Belgium: Springer. <a href=\"https://doi.org/10.1007/978-3-030-30806-3_1\">https://doi.org/10.1007/978-3-030-30806-3_1</a>","ieee":"G. Avni, T. A. Henzinger, R. Ibsen-Jensen, and P. Novotny, “Bidding games on Markov decision processes,” in <i> Proceedings of the 13th International Conference of Reachability Problems</i>, Brussels, Belgium, 2019, vol. 11674, pp. 1–12.","chicago":"Avni, Guy, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Petr Novotny. “Bidding Games on Markov Decision Processes.” In <i> Proceedings of the 13th International Conference of Reachability Problems</i>, 11674:1–12. Springer, 2019. <a href=\"https://doi.org/10.1007/978-3-030-30806-3_1\">https://doi.org/10.1007/978-3-030-30806-3_1</a>.","ama":"Avni G, Henzinger TA, Ibsen-Jensen R, Novotny P. Bidding games on Markov decision processes. In: <i> Proceedings of the 13th International Conference of Reachability Problems</i>. Vol 11674. Springer; 2019:1-12. doi:<a href=\"https://doi.org/10.1007/978-3-030-30806-3_1\">10.1007/978-3-030-30806-3_1</a>","mla":"Avni, Guy, et al. “Bidding Games on Markov Decision Processes.” <i> Proceedings of the 13th International Conference of Reachability Problems</i>, vol. 11674, Springer, 2019, pp. 1–12, doi:<a href=\"https://doi.org/10.1007/978-3-030-30806-3_1\">10.1007/978-3-030-30806-3_1</a>.","ista":"Avni G, Henzinger TA, Ibsen-Jensen R, Novotny P. 2019. Bidding games on Markov decision processes.  Proceedings of the 13th International Conference of Reachability Problems. RP: Reachability Problems, LNCS, vol. 11674, 1–12.","short":"G. Avni, T.A. Henzinger, R. Ibsen-Jensen, P. Novotny, in:,  Proceedings of the 13th International Conference of Reachability Problems, Springer, 2019, pp. 1–12."},"publication_status":"published","quality_controlled":"1","project":[{"call_identifier":"FWF","_id":"264B3912-B435-11E9-9278-68D0E5697425","name":"Formal Methods meets Algorithmic Game Theory","grant_number":"M02369"},{"_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S11402-N23"},{"name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211"}],"oa_version":"Submitted Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_identifier":{"issn":["0302-9743"],"isbn":["978-303030805-6"]},"_id":"6822","oa":1,"volume":11674,"date_updated":"2021-01-12T08:09:12Z","title":"Bidding games on Markov decision processes","doi":"10.1007/978-3-030-30806-3_1","year":"2019","ddc":["000"],"alternative_title":["LNCS"]},{"citation":{"mla":"Avni, Guy, et al. <i>Bidding Mechanisms in Graph Games</i>. Vol. 138, 11, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019, doi:<a href=\"https://doi.org/10.4230/LIPICS.MFCS.2019.11\">10.4230/LIPICS.MFCS.2019.11</a>.","ama":"Avni G, Henzinger TA, Zikelic D. Bidding mechanisms in graph games. In: Vol 138. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2019. doi:<a href=\"https://doi.org/10.4230/LIPICS.MFCS.2019.11\">10.4230/LIPICS.MFCS.2019.11</a>","ista":"Avni G, Henzinger TA, Zikelic D. 2019. Bidding mechanisms in graph games. MFCS: nternational Symposium on Mathematical Foundations of Computer Science, LIPIcs, vol. 138, 11.","short":"G. Avni, T.A. Henzinger, D. Zikelic, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.","apa":"Avni, G., Henzinger, T. A., &#38; Zikelic, D. (2019). Bidding mechanisms in graph games (Vol. 138). Presented at the MFCS: nternational Symposium on Mathematical Foundations of Computer Science, Aachen, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPICS.MFCS.2019.11\">https://doi.org/10.4230/LIPICS.MFCS.2019.11</a>","ieee":"G. Avni, T. A. Henzinger, and D. Zikelic, “Bidding mechanisms in graph games,” presented at the MFCS: nternational Symposium on Mathematical Foundations of Computer Science, Aachen, Germany, 2019, vol. 138.","chicago":"Avni, Guy, Thomas A Henzinger, and Dorde Zikelic. “Bidding Mechanisms in Graph Games,” Vol. 138. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. <a href=\"https://doi.org/10.4230/LIPICS.MFCS.2019.11\">https://doi.org/10.4230/LIPICS.MFCS.2019.11</a>."},"publication_status":"published","author":[{"id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","first_name":"Guy","orcid":"0000-0001-5588-8287","full_name":"Avni, Guy","last_name":"Avni"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","first_name":"Thomas A"},{"full_name":"Zikelic, Dorde","last_name":"Zikelic","first_name":"Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"}],"abstract":[{"text":"In two-player games on graphs, the players move a token through a graph to produce a finite or infinite path, which determines the qualitative winner or quantitative payoff of the game. We study bidding games in which the players bid for the right to move the token. Several bidding rules were studied previously. In Richman bidding, in each round, the players simultaneously submit bids, and the higher bidder moves the token and pays the other player. Poorman bidding is similar except that the winner of the bidding pays the \"bank\" rather than the other player. Taxman bidding spans the spectrum between Richman and poorman bidding. They are parameterized by a constant tau in [0,1]: portion tau of the winning bid is paid to the other player, and portion 1-tau to the bank. While finite-duration (reachability) taxman games have been studied before, we present, for the first time, results on infinite-duration taxman games. It was previously shown that both Richman and poorman infinite-duration games with qualitative objectives reduce to reachability games, and we show a similar result here. Our most interesting results concern quantitative taxman games, namely mean-payoff games, where poorman and Richman bidding differ significantly. A central quantity in these games is the ratio between the two players' initial budgets. While in poorman mean-payoff games, the optimal payoff of a player depends on the initial ratio, in Richman bidding, the payoff depends only on the structure of the game. In both games the optimal payoffs can be found using (different) probabilistic connections with random-turn games in which in each turn, instead of bidding, a coin is tossed to determine which player moves. While the value with Richman bidding equals the value of a random-turn game with an un-biased coin, with poorman bidding, the bias in the coin is the initial ratio of the budgets. We give a complete classification of mean-payoff taxman games that is based on a probabilistic connection: the value of a taxman bidding game with parameter tau and initial ratio r, equals the value of a random-turn game that uses a coin with bias F(tau, r) = (r+tau * (1-r))/(1+tau). Thus, we show that Richman bidding is the exception; namely, for every tau <1, the value of the game depends on the initial ratio. Our proof technique simplifies and unifies the previous proof techniques for both Richman and poorman bidding. ","lang":"eng"}],"date_updated":"2023-08-07T14:08:34Z","volume":138,"oa":1,"arxiv":1,"oa_version":"Published Version","quality_controlled":"1","project":[{"name":"International IST Doctoral Program","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","grant_number":"665385"},{"grant_number":"M02369","call_identifier":"FWF","name":"Formal Methods meets Algorithmic Game Theory","_id":"264B3912-B435-11E9-9278-68D0E5697425"},{"name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211"},{"grant_number":"S11402-N23","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"6884","ec_funded":1,"doi":"10.4230/LIPICS.MFCS.2019.11","year":"2019","title":"Bidding mechanisms in graph games","external_id":{"arxiv":["1905.03835"]},"article_number":"11","tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"alternative_title":["LIPIcs"],"ddc":["004"],"related_material":{"record":[{"id":"9239","relation":"later_version","status":"public"}]},"type":"conference","day":"01","status":"public","intvolume":"       138","file_date_updated":"2020-07-14T12:47:42Z","date_published":"2019-08-01T00:00:00Z","month":"08","language":[{"iso":"eng"}],"scopus_import":1,"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"has_accepted_license":"1","date_created":"2019-09-18T08:04:26Z","file":[{"date_updated":"2020-07-14T12:47:42Z","access_level":"open_access","file_name":"2019_LIPIcs_Avni.pdf","file_size":554457,"date_created":"2019-09-27T11:45:15Z","checksum":"6346e116a4f4ed1414174d96d2c4fbd7","content_type":"application/pdf","relation":"main_file","creator":"kschuh","file_id":"6913"}],"conference":{"location":"Aachen, Germany","end_date":"2019-08-30","name":"MFCS: nternational Symposium on Mathematical Foundations of Computer Science","start_date":"2019-08-26"}},{"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"alternative_title":["LIPIcs"],"article_number":"27","ddc":["000"],"year":"2019","doi":"10.4230/LIPICS.CONCUR.2019.27","title":"Long-run average behavior of vector addition systems with states","volume":140,"oa":1,"date_updated":"2021-01-12T08:09:27Z","_id":"6885","quality_controlled":"1","oa_version":"Published Version","project":[{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","call_identifier":"FWF"},{"grant_number":"S11402-N23","call_identifier":"FWF","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Chatterjee, Krishnendu, et al. <i>Long-Run Average Behavior of Vector Addition Systems with States</i>. Vol. 140, 27, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019, doi:<a href=\"https://doi.org/10.4230/LIPICS.CONCUR.2019.27\">10.4230/LIPICS.CONCUR.2019.27</a>.","ama":"Chatterjee K, Henzinger TA, Otop J. Long-run average behavior of vector addition systems with states. In: Vol 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2019. doi:<a href=\"https://doi.org/10.4230/LIPICS.CONCUR.2019.27\">10.4230/LIPICS.CONCUR.2019.27</a>","ista":"Chatterjee K, Henzinger TA, Otop J. 2019. Long-run average behavior of vector addition systems with states. CONCUR: International Conference on Concurrency Theory, LIPIcs, vol. 140, 27.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2019). Long-run average behavior of vector addition systems with states (Vol. 140). Presented at the CONCUR: International Conference on Concurrency Theory, Amsterdam, Netherlands: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPICS.CONCUR.2019.27\">https://doi.org/10.4230/LIPICS.CONCUR.2019.27</a>","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Long-run average behavior of vector addition systems with states,” presented at the CONCUR: International Conference on Concurrency Theory, Amsterdam, Netherlands, 2019, vol. 140.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Long-Run Average Behavior of Vector Addition Systems with States,” Vol. 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. <a href=\"https://doi.org/10.4230/LIPICS.CONCUR.2019.27\">https://doi.org/10.4230/LIPICS.CONCUR.2019.27</a>."},"publication_status":"published","abstract":[{"lang":"eng","text":"A vector addition system with states (VASS) consists of a finite set of states and counters. A configuration is a state and a value for each counter; a transition changes the state and each counter is incremented, decremented, or left unchanged. While qualitative properties such as state and configuration reachability have been studied for VASS, we consider the long-run average cost of infinite computations of VASS. The cost of a configuration is for each state, a linear combination of the counter values. In the special case of uniform cost functions, the linear combination is the same for all states. The (regular) long-run emptiness problem is, given a VASS, a cost function, and a threshold value, if there is a (lasso-shaped) computation such that the long-run average value of the cost function does not exceed the threshold. For uniform cost functions, we show that the regular long-run emptiness problem is (a) decidable in polynomial time for integer-valued VASS, and (b) decidable but nonelementarily hard for natural-valued VASS (i.e., nonnegative counters). For general cost functions, we show that the problem is (c) NP-complete for integer-valued VASS, and (d) undecidable for natural-valued VASS. Our most interesting result is for (c) integer-valued VASS with general cost functions, where we establish a connection between the regular long-run emptiness problem and quadratic Diophantine inequalities. The general (nonregular) long-run emptiness problem is equally hard as the regular problem in all cases except (c), where it remains open. "}],"author":[{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000−0002−2985−7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Jan","last_name":"Otop","full_name":"Otop, Jan"}],"has_accepted_license":"1","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"conference":{"start_date":"2019-08-27","end_date":"2019-08-30","location":"Amsterdam, Netherlands","name":"CONCUR: International Conference on Concurrency Theory"},"date_created":"2019-09-18T08:06:14Z","file":[{"date_updated":"2020-07-14T12:47:43Z","access_level":"open_access","file_name":"2019_LIPIcs_Chatterjee.pdf","file_size":538120,"date_created":"2019-09-27T12:09:35Z","checksum":"4985e26e1572d1575d64d38acabd71d6","content_type":"application/pdf","relation":"main_file","creator":"kschuh","file_id":"6914"}],"month":"08","date_published":"2019-08-01T00:00:00Z","scopus_import":1,"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","language":[{"iso":"eng"}],"file_date_updated":"2020-07-14T12:47:43Z","day":"01","type":"conference","intvolume":"       140","status":"public"},{"ddc":["000"],"tmp":{"name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)","short":"CC BY (3.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode"},"alternative_title":["LIPIcs"],"article_number":"20","title":"Determinacy in discrete-bidding infinite-duration games","external_id":{"arxiv":["1905.03588"]},"year":"2019","doi":"10.4230/LIPICS.CONCUR.2019.20","_id":"6886","oa_version":"Published Version","quality_controlled":"1","project":[{"grant_number":"S11402-N23","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"grant_number":"M02369","call_identifier":"FWF","_id":"264B3912-B435-11E9-9278-68D0E5697425","name":"Formal Methods meets Algorithmic Game Theory"}],"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","arxiv":1,"article_processing_charge":"No","volume":140,"date_updated":"2022-01-26T08:27:10Z","oa":1,"abstract":[{"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. ","lang":"eng"}],"author":[{"full_name":"Aghajohari, Milad","last_name":"Aghajohari","first_name":"Milad"},{"first_name":"Guy","orcid":"0000-0001-5588-8287","full_name":"Avni, Guy","last_name":"Avni","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"citation":{"mla":"Aghajohari, Milad, et al. <i>Determinacy in Discrete-Bidding Infinite-Duration Games</i>. Vol. 140, 20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019, doi:<a href=\"https://doi.org/10.4230/LIPICS.CONCUR.2019.20\">10.4230/LIPICS.CONCUR.2019.20</a>.","ama":"Aghajohari M, Avni G, Henzinger TA. Determinacy in discrete-bidding infinite-duration games. In: Vol 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2019. doi:<a href=\"https://doi.org/10.4230/LIPICS.CONCUR.2019.20\">10.4230/LIPICS.CONCUR.2019.20</a>","ista":"Aghajohari M, Avni G, Henzinger TA. 2019. Determinacy in discrete-bidding infinite-duration games. CONCUR: International Conference on Concurrency Theory, LIPIcs, vol. 140, 20.","short":"M. Aghajohari, G. Avni, T.A. Henzinger, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.","apa":"Aghajohari, M., Avni, G., &#38; Henzinger, T. A. (2019). Determinacy in discrete-bidding infinite-duration games (Vol. 140). Presented at the CONCUR: International Conference on Concurrency Theory, Amsterdam, Netherlands: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPICS.CONCUR.2019.20\">https://doi.org/10.4230/LIPICS.CONCUR.2019.20</a>","ieee":"M. Aghajohari, G. Avni, and T. A. Henzinger, “Determinacy in discrete-bidding infinite-duration games,” presented at the CONCUR: International Conference on Concurrency Theory, Amsterdam, Netherlands, 2019, vol. 140.","chicago":"Aghajohari, Milad, Guy Avni, and Thomas A Henzinger. “Determinacy in Discrete-Bidding Infinite-Duration Games,” Vol. 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. <a href=\"https://doi.org/10.4230/LIPICS.CONCUR.2019.20\">https://doi.org/10.4230/LIPICS.CONCUR.2019.20</a>."},"publication_status":"published","conference":{"start_date":"2019-08-27","location":"Amsterdam, Netherlands","end_date":"2019-08-30","name":"CONCUR: International Conference on Concurrency Theory"},"file":[{"file_id":"6915","creator":"kschuh","content_type":"application/pdf","relation":"main_file","date_created":"2019-09-27T12:21:38Z","checksum":"4df6d3575c506edb17215adada03cc8e","file_name":"2019_LIPIcs_Aghajohari.pdf","file_size":741425,"date_updated":"2020-07-14T12:47:43Z","access_level":"open_access"}],"date_created":"2019-09-18T08:06:58Z","has_accepted_license":"1","department":[{"_id":"ToHe"}],"scopus_import":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","language":[{"iso":"eng"}],"month":"08","date_published":"2019-08-01T00:00:00Z","file_date_updated":"2020-07-14T12:47:43Z","intvolume":"       140","status":"public","day":"01","type":"conference"},{"title":"Strategy representation by decision trees with linear classifiers","external_id":{"isi":["000679281300007"],"arxiv":["1906.08178"]},"year":"2019","doi":"10.1007/978-3-030-30281-8_7","isi":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1906.08178"}],"alternative_title":["LNCS"],"author":[{"first_name":"Pranav","last_name":"Ashok","full_name":"Ashok, Pranav"},{"full_name":"Brázdil, Tomáš","last_name":"Brázdil","first_name":"Tomáš"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"last_name":"Křetínský","full_name":"Křetínský, Jan","first_name":"Jan"},{"id":"40C20FD2-F248-11E8-B48F-1D18A9856A87","first_name":"Christoph","orcid":"0000-0001-8622-7887","full_name":"Lampert, Christoph","last_name":"Lampert"},{"id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","full_name":"Toman, Viktor","last_name":"Toman","orcid":"0000-0001-9036-063X","first_name":"Viktor"}],"abstract":[{"text":"Graph games and Markov decision processes (MDPs) are standard models in reactive synthesis and verification of probabilistic systems with nondeterminism. The class of   𝜔 -regular winning conditions; e.g., safety, reachability, liveness, parity conditions; provides a robust and expressive specification formalism for properties that arise in analysis of reactive systems. The resolutions of nondeterminism in games and MDPs are represented as strategies, and we consider succinct representation of such strategies. The decision-tree data structure from machine learning retains the flavor of decisions of strategies and allows entropy-based minimization to obtain succinct trees. However, in contrast to traditional machine-learning problems where small errors are allowed, for winning strategies in graph games and MDPs no error is allowed, and the decision tree must represent the entire strategy. In this work we propose decision trees with linear classifiers for representation of strategies in graph games and MDPs. We have implemented strategy representation using this data structure and we present experimental results for problems on graph games and MDPs, which show that this new data structure presents a much more efficient strategy representation as compared to standard decision trees.","lang":"eng"}],"publication_status":"published","citation":{"apa":"Ashok, P., Brázdil, T., Chatterjee, K., Křetínský, J., Lampert, C., &#38; Toman, V. (2019). Strategy representation by decision trees with linear classifiers. In <i>16th International Conference on Quantitative Evaluation of Systems</i> (Vol. 11785, pp. 109–128). Glasgow, United Kingdom: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-30281-8_7\">https://doi.org/10.1007/978-3-030-30281-8_7</a>","ieee":"P. Ashok, T. Brázdil, K. Chatterjee, J. Křetínský, C. Lampert, and V. Toman, “Strategy representation by decision trees with linear classifiers,” in <i>16th International Conference on Quantitative Evaluation of Systems</i>, Glasgow, United Kingdom, 2019, vol. 11785, pp. 109–128.","chicago":"Ashok, Pranav, Tomáš Brázdil, Krishnendu Chatterjee, Jan Křetínský, Christoph Lampert, and Viktor Toman. “Strategy Representation by Decision Trees with Linear Classifiers.” In <i>16th International Conference on Quantitative Evaluation of Systems</i>, 11785:109–28. Springer Nature, 2019. <a href=\"https://doi.org/10.1007/978-3-030-30281-8_7\">https://doi.org/10.1007/978-3-030-30281-8_7</a>.","mla":"Ashok, Pranav, et al. “Strategy Representation by Decision Trees with Linear Classifiers.” <i>16th International Conference on Quantitative Evaluation of Systems</i>, vol. 11785, Springer Nature, 2019, pp. 109–28, doi:<a href=\"https://doi.org/10.1007/978-3-030-30281-8_7\">10.1007/978-3-030-30281-8_7</a>.","ama":"Ashok P, Brázdil T, Chatterjee K, Křetínský J, Lampert C, Toman V. Strategy representation by decision trees with linear classifiers. In: <i>16th International Conference on Quantitative Evaluation of Systems</i>. Vol 11785. Springer Nature; 2019:109-128. doi:<a href=\"https://doi.org/10.1007/978-3-030-30281-8_7\">10.1007/978-3-030-30281-8_7</a>","ista":"Ashok P, Brázdil T, Chatterjee K, Křetínský J, Lampert C, Toman V. 2019. Strategy representation by decision trees with linear classifiers. 16th International Conference on Quantitative Evaluation of Systems. QEST: Quantitative Evaluation of Systems, LNCS, vol. 11785, 109–128.","short":"P. Ashok, T. Brázdil, K. Chatterjee, J. Křetínský, C. Lampert, V. Toman, in:, 16th International Conference on Quantitative Evaluation of Systems, Springer Nature, 2019, pp. 109–128."},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","oa_version":"Preprint","project":[{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","call_identifier":"FWF"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"},{"name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003"}],"quality_controlled":"1","_id":"6942","publication_identifier":{"eisbn":["9783030302818"],"isbn":["9783030302801"],"issn":["0302-9743"]},"volume":11785,"oa":1,"date_updated":"2025-06-02T08:53:47Z","article_processing_charge":"No","arxiv":1,"language":[{"iso":"eng"}],"publisher":"Springer Nature","scopus_import":"1","date_published":"2019-09-04T00:00:00Z","month":"09","date_created":"2019-10-14T06:57:49Z","conference":{"start_date":"2019-09-10","end_date":"2019-09-12","name":"QEST: Quantitative Evaluation of Systems","location":"Glasgow, United Kingdom"},"department":[{"_id":"KrCh"},{"_id":"ChLa"}],"status":"public","intvolume":"     11785","type":"conference","day":"04","page":"109-128","publication":"16th International Conference on Quantitative Evaluation of Systems"},{"publication":"19th International Conference on Runtime Verification","page":"292-309","intvolume":"     11757","status":"public","day":"01","type":"conference","conference":{"location":"Porto, Portugal","name":"RV: Runtime Verification","end_date":"2019-10-11","start_date":"2019-10-08"},"date_created":"2019-12-09T08:47:55Z","department":[{"_id":"ToHe"}],"scopus_import":"1","publisher":"Springer Nature","language":[{"iso":"eng"}],"month":"10","date_published":"2019-10-01T00:00:00Z","publication_identifier":{"isbn":["9783030320782","9783030320799"],"issn":["0302-9743"]},"_id":"7159","quality_controlled":"1","oa_version":"None","project":[{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","call_identifier":"FWF"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","article_processing_charge":"No","date_updated":"2023-09-06T11:24:10Z","volume":11757,"abstract":[{"lang":"eng","text":"Cyber-physical systems (CPS) and the Internet-of-Things (IoT) result in a tremendous amount of generated, measured and recorded time-series data. Extracting temporal segments that encode patterns with useful information out of these huge amounts of data is an extremely difficult problem. We propose shape expressions as a declarative formalism for specifying, querying and extracting sophisticated temporal patterns from possibly noisy data. Shape expressions are regular expressions with arbitrary (linear, exponential, sinusoidal, etc.) shapes with parameters as atomic predicates and additional constraints on these parameters. We equip shape expressions with a novel noisy semantics that combines regular expression matching semantics with statistical regression. We characterize essential properties of the formalism and propose an efficient approximate shape expression matching procedure. We demonstrate the wide applicability of this technique on two case studies. "}],"author":[{"full_name":"Ničković, Dejan","last_name":"Ničković","first_name":"Dejan"},{"last_name":"Qin","full_name":"Qin, Xin","first_name":"Xin"},{"id":"40960E6E-F248-11E8-B48F-1D18A9856A87","last_name":"Ferrere","full_name":"Ferrere, Thomas","orcid":"0000-0001-5199-3143","first_name":"Thomas"},{"full_name":"Mateis, Cristinel","last_name":"Mateis","first_name":"Cristinel"},{"first_name":"Jyotirmoy","full_name":"Deshmukh, Jyotirmoy","last_name":"Deshmukh"}],"citation":{"apa":"Ničković, D., Qin, X., Ferrere, T., Mateis, C., &#38; Deshmukh, J. (2019). Shape expressions for specifying and extracting signal features. In <i>19th International Conference on Runtime Verification</i> (Vol. 11757, pp. 292–309). Porto, Portugal: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-32079-9_17\">https://doi.org/10.1007/978-3-030-32079-9_17</a>","ieee":"D. Ničković, X. Qin, T. Ferrere, C. Mateis, and J. Deshmukh, “Shape expressions for specifying and extracting signal features,” in <i>19th International Conference on Runtime Verification</i>, Porto, Portugal, 2019, vol. 11757, pp. 292–309.","chicago":"Ničković, Dejan, Xin Qin, Thomas Ferrere, Cristinel Mateis, and Jyotirmoy Deshmukh. “Shape Expressions for Specifying and Extracting Signal Features.” In <i>19th International Conference on Runtime Verification</i>, 11757:292–309. Springer Nature, 2019. <a href=\"https://doi.org/10.1007/978-3-030-32079-9_17\">https://doi.org/10.1007/978-3-030-32079-9_17</a>.","ama":"Ničković D, Qin X, Ferrere T, Mateis C, Deshmukh J. Shape expressions for specifying and extracting signal features. In: <i>19th International Conference on Runtime Verification</i>. Vol 11757. Springer Nature; 2019:292-309. doi:<a href=\"https://doi.org/10.1007/978-3-030-32079-9_17\">10.1007/978-3-030-32079-9_17</a>","mla":"Ničković, Dejan, et al. “Shape Expressions for Specifying and Extracting Signal Features.” <i>19th International Conference on Runtime Verification</i>, vol. 11757, Springer Nature, 2019, pp. 292–309, doi:<a href=\"https://doi.org/10.1007/978-3-030-32079-9_17\">10.1007/978-3-030-32079-9_17</a>.","ista":"Ničković D, Qin X, Ferrere T, Mateis C, Deshmukh J. 2019. Shape expressions for specifying and extracting signal features. 19th International Conference on Runtime Verification. RV: Runtime Verification, LNCS, vol. 11757, 292–309.","short":"D. Ničković, X. Qin, T. Ferrere, C. Mateis, J. Deshmukh, in:, 19th International Conference on Runtime Verification, Springer Nature, 2019, pp. 292–309."},"publication_status":"published","alternative_title":["LNCS"],"isi":1,"external_id":{"isi":["000570006300017"]},"title":"Shape expressions for specifying and extracting signal features","year":"2019","doi":"10.1007/978-3-030-32079-9_17"},{"publication_status":"published","citation":{"mla":"Alur, Rajeev, et al. “Continuous-Time Models for System Design and Analysis.” <i>Computing and Software Science</i>, edited by Bernhard Steffen and Gerhard Woeginger, vol. 10000, Springer Nature, 2019, pp. 452–77, doi:<a href=\"https://doi.org/10.1007/978-3-319-91908-9_22\">10.1007/978-3-319-91908-9_22</a>.","ama":"Alur R, Giacobbe M, Henzinger TA, Larsen KG, Mikučionis M. Continuous-time models for system design and analysis. In: Steffen B, Woeginger G, eds. <i>Computing and Software Science</i>. Vol 10000. LNCS. Springer Nature; 2019:452-477. doi:<a href=\"https://doi.org/10.1007/978-3-319-91908-9_22\">10.1007/978-3-319-91908-9_22</a>","ista":"Alur R, Giacobbe M, Henzinger TA, Larsen KG, Mikučionis M. 2019.Continuous-time models for system design and analysis. In: Computing and Software Science. Lecture Notes in Computer Science, vol. 10000, 452–477.","short":"R. Alur, M. Giacobbe, T.A. Henzinger, K.G. Larsen, M. Mikučionis, in:, B. Steffen, G. Woeginger (Eds.), Computing and Software Science, Springer Nature, 2019, pp. 452–477.","ieee":"R. Alur, M. Giacobbe, T. A. Henzinger, K. G. Larsen, and M. Mikučionis, “Continuous-time models for system design and analysis,” in <i>Computing and Software Science</i>, vol. 10000, B. Steffen and G. Woeginger, Eds. Springer Nature, 2019, pp. 452–477.","apa":"Alur, R., Giacobbe, M., Henzinger, T. A., Larsen, K. G., &#38; Mikučionis, M. (2019). Continuous-time models for system design and analysis. In B. Steffen &#38; G. Woeginger (Eds.), <i>Computing and Software Science</i> (Vol. 10000, pp. 452–477). Springer Nature. <a href=\"https://doi.org/10.1007/978-3-319-91908-9_22\">https://doi.org/10.1007/978-3-319-91908-9_22</a>","chicago":"Alur, Rajeev, Mirco Giacobbe, Thomas A Henzinger, Kim G. Larsen, and Marius Mikučionis. “Continuous-Time Models for System Design and Analysis.” In <i>Computing and Software Science</i>, edited by Bernhard Steffen and Gerhard Woeginger, 10000:452–77. LNCS. Springer Nature, 2019. <a href=\"https://doi.org/10.1007/978-3-319-91908-9_22\">https://doi.org/10.1007/978-3-319-91908-9_22</a>."},"abstract":[{"lang":"eng","text":"We illustrate the ingredients of the state-of-the-art of model-based approach for the formal design and verification of cyber-physical systems. To capture the interaction between a discrete controller and its continuously evolving environment, we use the formal models of timed and hybrid automata. We explain the steps of modeling and verification in the tools Uppaal and SpaceEx using a case study based on a dual-chamber implantable pacemaker monitoring a human heart. We show how to design a model as a composition of components, how to construct models at varying levels of detail, how to establish that one model is an abstraction of another, how to specify correctness requirements using temporal logic, and how to verify that a model satisfies a logical requirement."}],"author":[{"full_name":"Alur, Rajeev","last_name":"Alur","first_name":"Rajeev"},{"first_name":"Mirco","orcid":"0000-0001-8180-0904","last_name":"Giacobbe","full_name":"Giacobbe, Mirco","id":"3444EA5E-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A"},{"full_name":"Larsen, Kim G.","last_name":"Larsen","first_name":"Kim G."},{"last_name":"Mikučionis","full_name":"Mikučionis, Marius","first_name":"Marius"}],"editor":[{"first_name":"Bernhard","last_name":"Steffen","full_name":"Steffen, Bernhard"},{"full_name":"Woeginger, Gerhard","last_name":"Woeginger","first_name":"Gerhard"}],"date_updated":"2022-09-06T08:25:52Z","oa":1,"volume":10000,"article_processing_charge":"No","_id":"7453","publication_identifier":{"eisbn":["9783319919089"],"issn":["1611-3349"],"isbn":["9783319919072"],"eissn":["0302-9743"]},"acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23(RiSE/SHiNE) and Z211-N23 (Wittgenstein Award). This research has received funding from the Sino-Danish Basic Research Centre, IDEA4CPS, funded by the Danish National Research Foundation and the National Science Foundation, China, the Innovation Fund Denmark centre DiCyPS, as well as the ERC Advanced Grant LASSO.","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Published Version","quality_controlled":"1","project":[{"name":"Rigorous Systems Engineering","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11402-N23"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"}],"year":"2019","doi":"10.1007/978-3-319-91908-9_22","title":"Continuous-time models for system design and analysis","alternative_title":["Lecture Notes in Computer Science"],"main_file_link":[{"url":"https://doi.org/10.1007/978-3-319-91908-9_22","open_access":"1"}],"day":"05","type":"book_chapter","series_title":"LNCS","intvolume":"     10000","status":"public","publication":"Computing and Software Science","page":"452-477","month":"10","date_published":"2019-10-05T00:00:00Z","publisher":"Springer Nature","scopus_import":"1","language":[{"iso":"eng"}],"department":[{"_id":"ToHe"}],"date_created":"2020-02-05T10:51:44Z"},{"file":[{"file_size":745438,"file_name":"IST-2018-853-v2+2_concur2018.pdf","checksum":"c90895f4c5fafc18ddc54d1c8848077e","date_created":"2018-12-12T10:18:46Z","access_level":"open_access","date_updated":"2020-07-14T12:44:44Z","relation":"main_file","content_type":"application/pdf","creator":"system","file_id":"5368"}],"date_created":"2018-12-11T11:44:48Z","conference":{"start_date":"2018-09-04","name":"CONCUR: International Conference on Concurrency Theory","end_date":"2018-09-07","location":"Beijing, China"},"department":[{"_id":"ToHe"}],"has_accepted_license":"1","language":[{"iso":"eng"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","scopus_import":1,"date_published":"2018-08-13T00:00:00Z","month":"08","file_date_updated":"2020-07-14T12:44:44Z","status":"public","intvolume":"       118","type":"conference","day":"13","ddc":["000"],"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"6426"},{"id":"8332","relation":"dissertation_contains","status":"public"}]},"article_number":"21","alternative_title":["LIPIcs"],"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"pubrep_id":"1039","title":"Synchronizing the asynchronous","year":"2018","doi":"10.4230/LIPIcs.CONCUR.2018.21","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","oa_version":"Published Version","project":[{"grant_number":"S11402-N23","call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"},{"grant_number":"S11402-N23","call_identifier":"FWF","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"}],"_id":"133","publication_identifier":{"issn":["18688969"]},"date_updated":"2023-09-07T13:18:00Z","oa":1,"publist_id":"7790","volume":118,"author":[{"full_name":"Kragl, Bernhard","last_name":"Kragl","orcid":"0000-0001-7745-9117","first_name":"Bernhard","id":"320FC952-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Qadeer","full_name":"Qadeer, Shaz","first_name":"Shaz"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"abstract":[{"text":"Synchronous programs are easy to specify because the side effects of an operation are finished by the time the invocation of the operation returns to the caller. Asynchronous programs, on the other hand, are difficult to specify because there are side effects due to pending computation scheduled as a result of the invocation of an operation. They are also difficult to verify because of the large number of possible interleavings of concurrent computation threads. We present synchronization, a new proof rule that simplifies the verification of asynchronous programs by introducing the fiction, for proof purposes, that asynchronous operations complete synchronously. Synchronization summarizes an asynchronous computation as immediate atomic effect. Modular verification is enabled via pending asynchronous calls in atomic summaries, and a complementary proof rule that eliminates pending asynchronous calls when components and their specifications are composed. We evaluate synchronization in the context of a multi-layer refinement verification methodology on a collection of benchmark programs.","lang":"eng"}],"publication_status":"published","citation":{"ista":"Kragl B, Qadeer S, Henzinger TA. 2018. Synchronizing the asynchronous. CONCUR: International Conference on Concurrency Theory, LIPIcs, vol. 118, 21.","short":"B. Kragl, S. Qadeer, T.A. Henzinger, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.","mla":"Kragl, Bernhard, et al. <i>Synchronizing the Asynchronous</i>. Vol. 118, 21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2018.21\">10.4230/LIPIcs.CONCUR.2018.21</a>.","ama":"Kragl B, Qadeer S, Henzinger TA. Synchronizing the asynchronous. In: Vol 118. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2018. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2018.21\">10.4230/LIPIcs.CONCUR.2018.21</a>","chicago":"Kragl, Bernhard, Shaz Qadeer, and Thomas A Henzinger. “Synchronizing the Asynchronous,” Vol. 118. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2018.21\">https://doi.org/10.4230/LIPIcs.CONCUR.2018.21</a>.","apa":"Kragl, B., Qadeer, S., &#38; Henzinger, T. A. (2018). Synchronizing the asynchronous (Vol. 118). Presented at the CONCUR: International Conference on Concurrency Theory, Beijing, China: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2018.21\">https://doi.org/10.4230/LIPIcs.CONCUR.2018.21</a>","ieee":"B. Kragl, S. Qadeer, and T. A. Henzinger, “Synchronizing the asynchronous,” presented at the CONCUR: International Conference on Concurrency Theory, Beijing, China, 2018, vol. 118."}},{"title":"Specification-centered robustness","year":"2011","doi":"10.1109/SIES.2011.5953660","ec_funded":1,"main_file_link":[{"open_access":"1","url":"https://openlib.tugraz.at/download.php?id=5cb57c8a49344&location=browse"}],"abstract":[{"text":"In addition to being correct, a system should be robust, that is, it should behave reasonably even after receiving unexpected inputs. In this paper, we summarize two formal notions of robustness that we have introduced previously for reactive systems. One of the notions is based on assigning costs for failures on a user-provided notion of incorrect transitions in a specification. Here, we define a system to be robust if a finite number of incorrect inputs does not lead to an infinite number of incorrect outputs. We also give a more refined notion of robustness that aims to minimize the ratio of output failures to input failures. The second notion is aimed at liveness. In contrast to the previous notion, it has no concept of recovery from an error. Instead, it compares the ratio of the number of liveness constraints that the system violates to the number of liveness constraints that the environment violates.","lang":"eng"}],"author":[{"last_name":"Bloem","full_name":"Bloem, Roderick","first_name":"Roderick"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"first_name":"Karin","last_name":"Greimel","full_name":"Greimel, Karin"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A"},{"full_name":"Jobstmann, Barbara","last_name":"Jobstmann","first_name":"Barbara"}],"citation":{"chicago":"Bloem, Roderick, Krishnendu Chatterjee, Karin Greimel, Thomas A Henzinger, and Barbara Jobstmann. “Specification-Centered Robustness.” In <i>6th IEEE International Symposium on Industrial and Embedded Systems</i>, 176–85. IEEE, 2011. <a href=\"https://doi.org/10.1109/SIES.2011.5953660\">https://doi.org/10.1109/SIES.2011.5953660</a>.","ieee":"R. Bloem, K. Chatterjee, K. Greimel, T. A. Henzinger, and B. Jobstmann, “Specification-centered robustness,” in <i>6th IEEE International Symposium on Industrial and Embedded Systems</i>, Vasteras, Sweden, 2011, pp. 176–185.","apa":"Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T. A., &#38; Jobstmann, B. (2011). Specification-centered robustness. In <i>6th IEEE International Symposium on Industrial and Embedded Systems</i> (pp. 176–185). Vasteras, Sweden: IEEE. <a href=\"https://doi.org/10.1109/SIES.2011.5953660\">https://doi.org/10.1109/SIES.2011.5953660</a>","ista":"Bloem R, Chatterjee K, Greimel K, Henzinger TA, Jobstmann B. 2011. Specification-centered robustness. 6th IEEE International Symposium on Industrial and Embedded Systems.  SIES: International Symposium on Industrial Embedded Systems, 176–185.","short":"R. Bloem, K. Chatterjee, K. Greimel, T.A. Henzinger, B. Jobstmann, in:, 6th IEEE International Symposium on Industrial and Embedded Systems, IEEE, 2011, pp. 176–185.","mla":"Bloem, Roderick, et al. “Specification-Centered Robustness.” <i>6th IEEE International Symposium on Industrial and Embedded Systems</i>, IEEE, 2011, pp. 176–85, doi:<a href=\"https://doi.org/10.1109/SIES.2011.5953660\">10.1109/SIES.2011.5953660</a>.","ama":"Bloem R, Chatterjee K, Greimel K, Henzinger TA, Jobstmann B. Specification-centered robustness. In: <i>6th IEEE International Symposium on Industrial and Embedded Systems</i>. IEEE; 2011:176-185. doi:<a href=\"https://doi.org/10.1109/SIES.2011.5953660\">10.1109/SIES.2011.5953660</a>"},"publication_status":"published","_id":"3316","oa_version":"Published Version","quality_controlled":"1","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7","grant_number":"267989"},{"call_identifier":"FWF","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S11402-N23"},{"grant_number":"214373","call_identifier":"FP7","_id":"25F1337C-B435-11E9-9278-68D0E5697425","name":"Design for Embedded Systems"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","oa":1,"date_updated":"2021-01-12T07:42:36Z","publist_id":"3323","scopus_import":1,"publisher":"IEEE","language":[{"iso":"eng"}],"month":"07","date_published":"2011-07-14T00:00:00Z","conference":{"name":" SIES: International Symposium on Industrial Embedded Systems","location":"Vasteras, Sweden","end_date":"2011-06-17","start_date":"2011-06-15"},"date_created":"2018-12-11T12:02:38Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"status":"public","day":"14","type":"conference","publication":"6th IEEE International Symposium on Industrial and Embedded Systems","page":"176 - 185"}]