[{"related_material":{"record":[{"relation":"later_version","id":"2212","status":"public"}]},"language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-02-23T10:33:08Z","doi":"10.15479/AT:IST-2013-128-v1-1","ddc":["000","005","510"],"publication_identifier":{"issn":["2664-1690"]},"citation":{"short":"K. Chatterjee, L. Doyen, H. Gimbert, Y. Oualhadj, Perfect-Information Stochastic Mean-Payoff Parity Games, IST Austria, 2013.","ama":"Chatterjee K, Doyen L, Gimbert H, Oualhadj Y. <i>Perfect-Information Stochastic Mean-Payoff Parity Games</i>. IST Austria; 2013. doi:<a href=\"https://doi.org/10.15479/AT:IST-2013-128-v1-1\">10.15479/AT:IST-2013-128-v1-1</a>","apa":"Chatterjee, K., Doyen, L., Gimbert, H., &#38; Oualhadj, Y. (2013). <i>Perfect-information stochastic mean-payoff parity games</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2013-128-v1-1\">https://doi.org/10.15479/AT:IST-2013-128-v1-1</a>","chicago":"Chatterjee, Krishnendu, Laurent Doyen, Hugo Gimbert, and Youssouf Oualhadj. <i>Perfect-Information Stochastic Mean-Payoff Parity Games</i>. IST Austria, 2013. <a href=\"https://doi.org/10.15479/AT:IST-2013-128-v1-1\">https://doi.org/10.15479/AT:IST-2013-128-v1-1</a>.","ieee":"K. Chatterjee, L. Doyen, H. Gimbert, and Y. Oualhadj, <i>Perfect-information stochastic mean-payoff parity games</i>. IST Austria, 2013.","ista":"Chatterjee K, Doyen L, Gimbert H, Oualhadj Y. 2013. Perfect-information stochastic mean-payoff parity games, IST Austria, 22p.","mla":"Chatterjee, Krishnendu, et al. <i>Perfect-Information Stochastic Mean-Payoff Parity Games</i>. IST Austria, 2013, doi:<a href=\"https://doi.org/10.15479/AT:IST-2013-128-v1-1\">10.15479/AT:IST-2013-128-v1-1</a>."},"title":"Perfect-information stochastic mean-payoff parity games","day":"08","year":"2013","oa_version":"Published Version","alternative_title":["IST Austria Technical Report"],"has_accepted_license":"1","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"last_name":"Doyen","first_name":"Laurent","full_name":"Doyen, Laurent"},{"last_name":"Gimbert","full_name":"Gimbert, Hugo","first_name":"Hugo"},{"first_name":"Youssouf","full_name":"Oualhadj, Youssouf","last_name":"Oualhadj"}],"type":"technical_report","publisher":"IST Austria","publication_status":"published","oa":1,"department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:46:45Z","pubrep_id":"128","status":"public","page":"22","file":[{"content_type":"application/pdf","relation":"main_file","file_id":"5516","date_created":"2018-12-12T11:53:54Z","file_name":"IST-2013-128-v1+1_full_stoch_mpp.pdf","file_size":387467,"creator":"system","date_updated":"2020-07-14T12:46:45Z","access_level":"open_access","checksum":"ede787a10e74e4f7db302fab8f12f3ca"}],"month":"07","_id":"5405","date_published":"2013-07-08T00:00:00Z","date_created":"2018-12-12T11:39:09Z","abstract":[{"text":"The theory of graph games is the foundation for modeling and synthesizing reactive processes. In the synthesis of stochastic processes, we use 2-1/2-player games where some transitions of the game graph are controlled by two adversarial players, the System and the Environment, and the other transitions are determined probabilistically. We consider 2-1/2-player games where the objective of the System is the conjunction of a qualitative objective (specified as a parity condition) and a quantitative objective (specified as a mean-payoff condition). We establish that the problem of deciding whether the System can ensure that the probability to satisfy the mean-payoff parity objective is at least a given threshold is in NP ∩ coNP, matching the best known bound in the special case of 2-player games (where all transitions are deterministic) with only parity objectives, or with only mean-payoff objectives. We present an algorithm running\r\nin time O(d · n^{2d}·MeanGame) to compute the set of almost-sure winning states from which the objective\r\ncan be ensured with probability 1, where n is the number of states of the game, d the number of priorities\r\nof the parity objective, and MeanGame is the complexity to compute the set of almost-sure winning states\r\nin 2-1/2-player mean-payoff games. Our results are useful in the synthesis of stochastic reactive systems\r\nwith both functional requirement (given as a qualitative objective) and performance requirement (given\r\nas a quantitative objective).","lang":"eng"}]},{"related_material":{"record":[{"status":"public","id":"1376","relation":"later_version"}]},"date_updated":"2023-02-21T17:01:26Z","language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_identifier":{"issn":["2664-1690"]},"doi":"10.15479/AT:IST-2013-130-v1-1","ddc":["005"],"citation":{"short":"K. Chatterjee, T.A. Henzinger, J. Otop, A. Pavlogiannis, Distributed Synthesis for LTL Fragments, IST Austria, 2013.","apa":"Chatterjee, K., Henzinger, T. A., Otop, J., &#38; Pavlogiannis, A. (2013). <i>Distributed synthesis for LTL Fragments</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2013-130-v1-1\">https://doi.org/10.15479/AT:IST-2013-130-v1-1</a>","ama":"Chatterjee K, Henzinger TA, Otop J, Pavlogiannis A. <i>Distributed Synthesis for LTL Fragments</i>. IST Austria; 2013. doi:<a href=\"https://doi.org/10.15479/AT:IST-2013-130-v1-1\">10.15479/AT:IST-2013-130-v1-1</a>","ista":"Chatterjee K, Henzinger TA, Otop J, Pavlogiannis A. 2013. Distributed synthesis for LTL Fragments, IST Austria, 11p.","ieee":"K. Chatterjee, T. A. Henzinger, J. Otop, and A. Pavlogiannis, <i>Distributed synthesis for LTL Fragments</i>. IST Austria, 2013.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Andreas Pavlogiannis. <i>Distributed Synthesis for LTL Fragments</i>. IST Austria, 2013. <a href=\"https://doi.org/10.15479/AT:IST-2013-130-v1-1\">https://doi.org/10.15479/AT:IST-2013-130-v1-1</a>.","mla":"Chatterjee, Krishnendu, et al. <i>Distributed Synthesis for LTL Fragments</i>. IST Austria, 2013, doi:<a href=\"https://doi.org/10.15479/AT:IST-2013-130-v1-1\">10.15479/AT:IST-2013-130-v1-1</a>."},"title":"Distributed synthesis for LTL Fragments","day":"08","type":"technical_report","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"last_name":"Otop","full_name":"Otop, Jan","first_name":"Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722"}],"year":"2013","has_accepted_license":"1","oa_version":"Published Version","alternative_title":["IST Austria Technical Report"],"publication_status":"published","publisher":"IST Austria","oa":1,"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"file_date_updated":"2020-07-14T12:46:45Z","pubrep_id":"130","status":"public","page":"11","month":"07","file":[{"date_created":"2018-12-12T11:54:18Z","content_type":"application/pdf","relation":"main_file","file_id":"5540","checksum":"855513ebaf6f72228800c5fdb522f93c","date_updated":"2020-07-14T12:46:45Z","access_level":"open_access","file_name":"IST-2013-130-v1+1_Distributed_Synthesis.pdf","file_size":467895,"creator":"system"}],"date_created":"2018-12-12T11:39:09Z","_id":"5406","abstract":[{"lang":"eng","text":"We consider the distributed synthesis problem fortemporal logic specifications. Traditionally, the problem has been studied for LTL, and the previous results show that the problem is decidable iff there is no information fork in the architecture. We consider the problem for fragments of LTLand our main results are as follows: (1) We show that the problem is undecidable for architectures with information forks even for the fragment of LTL with temporal operators restricted to next and eventually. (2) For specifications restricted to globally along with non-nested next operators, we establish decidability (in EXPSPACE) for star architectures where the processes receive disjoint inputs, whereas we establish undecidability for architectures containing an information fork-meet structure. (3)Finally, we consider LTL without the next operator, and establish decidability (NEXPTIME-complete) for all architectures for a fragment that consists of a set of safety assumptions, and a set of guarantees where each guarantee is a safety, reachability, or liveness condition."}],"date_published":"2013-07-08T00:00:00Z"},{"page":"17","date_created":"2018-12-12T11:39:10Z","_id":"5408","abstract":[{"text":"We consider two-player partial-observation stochastic games where player 1 has partial observation and player 2 has perfect observation. The winning condition we study are omega-regular conditions specified as parity objectives. The qualitative analysis problem given a partial-observation stochastic game and a parity objective asks whether  there is a strategy to ensure that the objective is satisfied with probability 1 (resp. positive probability). While the qualitative analysis problems are known to be undecidable even for very special cases of parity objectives, they were shown to be decidable in 2EXPTIME under finite-memory  strategies. We improve the complexity and show that the qualitative analysis problems for partial-observation stochastic parity games under finite-memory strategies are \r\nEXPTIME-complete; and also establish optimal (exponential) memory bounds for finite-memory strategies required for qualitative analysis. ","lang":"eng"}],"date_published":"2013-09-12T00:00:00Z","month":"09","file":[{"relation":"main_file","file_id":"5477","content_type":"application/pdf","date_created":"2018-12-12T11:53:16Z","file_size":300481,"creator":"system","file_name":"IST-2013-141-v1+1_main-tech-rpt.pdf","checksum":"226bc791124f8d3138379778ce834e86","access_level":"open_access","date_updated":"2020-07-14T12:46:46Z"}],"oa":1,"publication_status":"published","publisher":"IST Austria","pubrep_id":"141","status":"public","file_date_updated":"2020-07-14T12:46:46Z","department":[{"_id":"KrCh"}],"title":"The complexity of partial-observation stochastic parity games with finite-memory strategies","citation":{"mla":"Chatterjee, Krishnendu, et al. <i>The Complexity of Partial-Observation Stochastic Parity Games with Finite-Memory Strategies</i>. IST Austria, 2013, doi:<a href=\"https://doi.org/10.15479/AT:IST-2013-141-v1-1\">10.15479/AT:IST-2013-141-v1-1</a>.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, Sumit Nain, and Moshe Vardi. <i>The Complexity of Partial-Observation Stochastic Parity Games with Finite-Memory Strategies</i>. IST Austria, 2013. <a href=\"https://doi.org/10.15479/AT:IST-2013-141-v1-1\">https://doi.org/10.15479/AT:IST-2013-141-v1-1</a>.","ista":"Chatterjee K, Doyen L, Nain S, Vardi M. 2013. The complexity of partial-observation stochastic parity games with finite-memory strategies, IST Austria, 17p.","ieee":"K. Chatterjee, L. Doyen, S. Nain, and M. Vardi, <i>The complexity of partial-observation stochastic parity games with finite-memory strategies</i>. IST Austria, 2013.","ama":"Chatterjee K, Doyen L, Nain S, Vardi M. <i>The Complexity of Partial-Observation Stochastic Parity Games with Finite-Memory Strategies</i>. IST Austria; 2013. doi:<a href=\"https://doi.org/10.15479/AT:IST-2013-141-v1-1\">10.15479/AT:IST-2013-141-v1-1</a>","apa":"Chatterjee, K., Doyen, L., Nain, S., &#38; Vardi, M. (2013). <i>The complexity of partial-observation stochastic parity games with finite-memory strategies</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2013-141-v1-1\">https://doi.org/10.15479/AT:IST-2013-141-v1-1</a>","short":"K. Chatterjee, L. Doyen, S. Nain, M. Vardi, The Complexity of Partial-Observation Stochastic Parity Games with Finite-Memory Strategies, IST Austria, 2013."},"author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"full_name":"Doyen, Laurent","first_name":"Laurent","last_name":"Doyen"},{"first_name":"Sumit","full_name":"Nain, Sumit","last_name":"Nain"},{"full_name":"Vardi, Moshe","first_name":"Moshe","last_name":"Vardi"}],"type":"technical_report","has_accepted_license":"1","alternative_title":["IST Austria Technical Report"],"oa_version":"Published Version","year":"2013","day":"12","related_material":{"record":[{"status":"public","id":"2213","relation":"later_version"}]},"publication_identifier":{"issn":["2664-1690"]},"ddc":["000","005"],"doi":"10.15479/AT:IST-2013-141-v1-1","language":[{"iso":"eng"}],"date_updated":"2023-02-23T10:33:11Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"date_published":"2013-10-30T00:00:00Z","_id":"5409","abstract":[{"lang":"eng","text":"The edit distance between two (untimed) traces is the minimum cost of a sequence of edit operations (insertion, deletion, or substitution) needed to transform one trace to the other. Edit distances have been extensively studied in the untimed setting, and form the basis for approximate matching of sequences in different domains such as coding theory, parsing, and speech recognition. \r\nIn this paper, we lift the study of edit distances from untimed languages to the timed setting. We define an edit distance between timed words which incorporates both the edit distance between the untimed words and the absolute difference in timestamps. Our edit distance between two timed words is computable in polynomial time. Further, we show that the edit distance between a timed word and a timed language generated by a timed automaton, defined as the edit distance between the word and the closest word in the language, is PSPACE-complete. While computing the edit distance between two timed automata is undecidable, we show that the approximate version, where we decide if the edit distance between two timed automata is either less than a given parameter or more than delta away from the parameter, for delta>0, can be solved in exponential space and is EXPSPACE-hard. Our definitions and techniques can be generalized to the setting of hybrid systems, and we show analogous decidability results for rectangular automata."}],"date_created":"2018-12-12T11:39:10Z","month":"10","file":[{"content_type":"application/pdf","relation":"main_file","file_id":"5469","date_created":"2018-12-12T11:53:08Z","file_name":"IST-2013-144-v1+1_main.pdf","creator":"system","file_size":336377,"date_updated":"2020-07-14T12:46:46Z","access_level":"open_access","checksum":"0f7633081ba8299c543322f0ad08571f"}],"page":"12","pubrep_id":"144","status":"public","file_date_updated":"2020-07-14T12:46:46Z","department":[{"_id":"KrCh"}],"oa":1,"publisher":"IST Austria","publication_status":"published","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen"},{"last_name":"Majumdar","full_name":"Majumdar, Rupak","first_name":"Rupak"}],"type":"technical_report","has_accepted_license":"1","alternative_title":["IST Austria Technical Report"],"year":"2013","oa_version":"Published Version","day":"30","title":"Edit distance for timed automata","citation":{"short":"K. Chatterjee, R. Ibsen-Jensen, R. Majumdar, Edit Distance for Timed Automata, IST Austria, 2013.","ama":"Chatterjee K, Ibsen-Jensen R, Majumdar R. <i>Edit Distance for Timed Automata</i>. IST Austria; 2013. doi:<a href=\"https://doi.org/10.15479/AT:IST-2013-144-v1-1\">10.15479/AT:IST-2013-144-v1-1</a>","apa":"Chatterjee, K., Ibsen-Jensen, R., &#38; Majumdar, R. (2013). <i>Edit distance for timed automata</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2013-144-v1-1\">https://doi.org/10.15479/AT:IST-2013-144-v1-1</a>","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Rupak Majumdar. <i>Edit Distance for Timed Automata</i>. IST Austria, 2013. <a href=\"https://doi.org/10.15479/AT:IST-2013-144-v1-1\">https://doi.org/10.15479/AT:IST-2013-144-v1-1</a>.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and R. Majumdar, <i>Edit distance for timed automata</i>. IST Austria, 2013.","ista":"Chatterjee K, Ibsen-Jensen R, Majumdar R. 2013. Edit distance for timed automata, IST Austria, 12p.","mla":"Chatterjee, Krishnendu, et al. <i>Edit Distance for Timed Automata</i>. IST Austria, 2013, doi:<a href=\"https://doi.org/10.15479/AT:IST-2013-144-v1-1\">10.15479/AT:IST-2013-144-v1-1</a>."},"publication_identifier":{"issn":["2664-1690"]},"ddc":["000"],"doi":"10.15479/AT:IST-2013-144-v1-1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"date_updated":"2023-02-23T10:33:18Z","related_material":{"record":[{"relation":"later_version","id":"2216","status":"public"}]}},{"page":"13","date_created":"2018-12-12T11:39:10Z","_id":"5410","abstract":[{"text":"Board games, like Tic-Tac-Toe and CONNECT-4, play an important role not only in development of mathematical and logical skills, but also in emotional and social development. In this paper, we address the problem of generating targeted starting positions for such games. This can facilitate new approaches for bringing novice players to mastery, and also leads to discovery of interesting game variants. \r\nOur approach generates starting states of varying hardness levels for player 1 in a two-player board game, given rules of the board game, the desired number of steps required for player 1 to win, and the expertise levels of the two players. Our approach leverages symbolic methods and iterative simulation to efficiently search the extremely large state space. We present experimental results that include discovery of states of varying hardness levels for several simple grid-based board games. Also, the presence of such states for standard game variants like Tic-Tac-Toe on board size 4x4 opens up new games to be played that have not been played for ages since the default start state is heavily biased. ","lang":"eng"}],"date_published":"2013-12-03T00:00:00Z","file":[{"access_level":"open_access","date_updated":"2020-07-14T12:46:46Z","checksum":"409f3aaaf1184e4057b89cbb449dac80","creator":"system","file_size":818189,"file_name":"IST-2013-146-v1+1_main.pdf","date_created":"2018-12-12T11:54:06Z","relation":"main_file","file_id":"5528","content_type":"application/pdf"}],"month":"12","oa":1,"publisher":"IST Austria","publication_status":"published","status":"public","pubrep_id":"146","department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:46:46Z","title":"Automatic generation of alternative starting positions for traditional board games","citation":{"short":"U. Ahmed, K. Chatterjee, S. Gulwani, Automatic Generation of Alternative Starting Positions for Traditional Board Games, IST Austria, 2013.","ama":"Ahmed U, Chatterjee K, Gulwani S. <i>Automatic Generation of Alternative Starting Positions for Traditional Board Games</i>. IST Austria; 2013. doi:<a href=\"https://doi.org/10.15479/AT:IST-2013-146-v1-1\">10.15479/AT:IST-2013-146-v1-1</a>","apa":"Ahmed, U., Chatterjee, K., &#38; Gulwani, S. (2013). <i>Automatic generation of alternative starting positions for traditional board games</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2013-146-v1-1\">https://doi.org/10.15479/AT:IST-2013-146-v1-1</a>","chicago":"Ahmed, Umair, Krishnendu Chatterjee, and Sumit Gulwani. <i>Automatic Generation of Alternative Starting Positions for Traditional Board Games</i>. IST Austria, 2013. <a href=\"https://doi.org/10.15479/AT:IST-2013-146-v1-1\">https://doi.org/10.15479/AT:IST-2013-146-v1-1</a>.","ista":"Ahmed U, Chatterjee K, Gulwani S. 2013. Automatic generation of alternative starting positions for traditional board games, IST Austria, 13p.","ieee":"U. Ahmed, K. Chatterjee, and S. Gulwani, <i>Automatic generation of alternative starting positions for traditional board games</i>. IST Austria, 2013.","mla":"Ahmed, Umair, et al. <i>Automatic Generation of Alternative Starting Positions for Traditional Board Games</i>. IST Austria, 2013, doi:<a href=\"https://doi.org/10.15479/AT:IST-2013-146-v1-1\">10.15479/AT:IST-2013-146-v1-1</a>."},"year":"2013","alternative_title":["IST Austria Technical Report"],"oa_version":"Published Version","has_accepted_license":"1","type":"technical_report","author":[{"full_name":"Ahmed, Umair","first_name":"Umair","last_name":"Ahmed"},{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Gulwani","full_name":"Gulwani, Sumit","first_name":"Sumit"}],"day":"03","related_material":{"record":[{"status":"public","id":"1481","relation":"later_version"}]},"ddc":["000","005"],"doi":"10.15479/AT:IST-2013-146-v1-1","publication_identifier":{"issn":["2664-1690"]},"date_updated":"2023-02-23T10:00:50Z","language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"month":"09","date_created":"2018-12-11T11:51:39Z","series_title":"Leibniz International Proceedings in Informatics","page":"181 - 196","publication":"22nd EACSL Annual Conference on Computer Science Logic","quality_controlled":"1","department":[{"_id":"KrCh"}],"intvolume":"        23","status":"public","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","day":"01","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Fijalkow","full_name":"Fijalkow, Nathanaël","first_name":"Nathanaël"}],"type":"conference","alternative_title":["LIPIcs"],"citation":{"short":"K. Chatterjee, N. Fijalkow, in:, 22nd EACSL Annual Conference on Computer Science Logic, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013, pp. 181–196.","apa":"Chatterjee, K., &#38; Fijalkow, N. (2013). Infinite-state games with finitary conditions. In <i>22nd EACSL Annual Conference on Computer Science Logic</i> (Vol. 23, pp. 181–196). Torino, Italy: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CSL.2013.181\">https://doi.org/10.4230/LIPIcs.CSL.2013.181</a>","ama":"Chatterjee K, Fijalkow N. Infinite-state games with finitary conditions. In: <i>22nd EACSL Annual Conference on Computer Science Logic</i>. Vol 23. Leibniz International Proceedings in Informatics. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2013:181-196. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CSL.2013.181\">10.4230/LIPIcs.CSL.2013.181</a>","ieee":"K. Chatterjee and N. Fijalkow, “Infinite-state games with finitary conditions,” in <i>22nd EACSL Annual Conference on Computer Science Logic</i>, Torino, Italy, 2013, vol. 23, pp. 181–196.","ista":"Chatterjee K, Fijalkow N. 2013. Infinite-state games with finitary conditions. 22nd EACSL Annual Conference on Computer Science Logic. CSL: Computer Science LogicLeibniz International Proceedings in Informatics, LIPIcs, vol. 23, 181–196.","chicago":"Chatterjee, Krishnendu, and Nathanaël Fijalkow. “Infinite-State Games with Finitary Conditions.” In <i>22nd EACSL Annual Conference on Computer Science Logic</i>, 23:181–96. Leibniz International Proceedings in Informatics. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013. <a href=\"https://doi.org/10.4230/LIPIcs.CSL.2013.181\">https://doi.org/10.4230/LIPIcs.CSL.2013.181</a>.","mla":"Chatterjee, Krishnendu, and Nathanaël Fijalkow. “Infinite-State Games with Finitary Conditions.” <i>22nd EACSL Annual Conference on Computer Science Logic</i>, vol. 23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013, pp. 181–96, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CSL.2013.181\">10.4230/LIPIcs.CSL.2013.181</a>."},"ec_funded":1,"title":"Infinite-state games with finitary conditions","conference":{"name":"CSL: Computer Science Logic","end_date":"2013-09-05","start_date":"203-09-02","location":"Torino, Italy"},"language":[{"iso":"eng"}],"ddc":["000"],"doi":"10.4230/LIPIcs.CSL.2013.181","project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"file":[{"file_size":547296,"creator":"system","file_name":"IST-2016-624-v1+1_ChKr_Infinite-state_games_2013_17.pdf","access_level":"open_access","date_updated":"2020-07-14T12:44:47Z","checksum":"b7091a3866db573c0db5ec486952255e","relation":"main_file","file_id":"5023","content_type":"application/pdf","date_created":"2018-12-12T10:13:38Z"}],"abstract":[{"text":"We study two-player zero-sum games over infinite-state graphs equipped with ωB and finitary conditions. Our first contribution is about the strategy complexity, i.e the memory required for winning strategies: we prove that over general infinite-state graphs, memoryless strategies are sufficient for finitary Büchi, and finite-memory suffices for finitary parity games. We then study pushdown games with boundedness conditions, with two contributions. First we prove a collapse result for pushdown games with ωB-conditions, implying the decidability of solving these games. Second we consider pushdown games with finitary parity along with stack boundedness conditions, and show that solving these games is EXPTIME-complete.","lang":"eng"}],"_id":"1374","date_published":"2013-09-01T00:00:00Z","file_date_updated":"2020-07-14T12:44:47Z","pubrep_id":"624","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"volume":23,"publication_status":"published","oa":1,"publist_id":"5837","year":"2013","oa_version":"Published Version","has_accepted_license":"1","scopus_import":1,"date_updated":"2021-01-12T06:50:14Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"publisher":"IEEE","publication_status":"published","quality_controlled":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publication":"13th International Conference on Formal Methods in Computer-Aided Design","status":"public","page":"18 - 25","month":"12","date_created":"2018-12-11T11:51:40Z","_id":"1376","abstract":[{"text":"We consider the distributed synthesis problem for temporal logic specifications. Traditionally, the problem has been studied for LTL, and the previous results show that the problem is decidable iff there is no information fork in the architecture. We consider the problem for fragments of LTL and our main results are as follows: (1) We show that the problem is undecidable for architectures with information forks even for the fragment of LTL with temporal operators restricted to next and eventually. (2) For specifications restricted to globally along with non-nested next operators, we establish decidability (in EXPSPACE) for star architectures where the processes receive disjoint inputs, whereas we establish undecidability for architectures containing an information fork-meet structure. (3) Finally, we consider LTL without the next operator, and establish decidability (NEXPTIME-complete) for all architectures for a fragment that consists of a set of safety assumptions, and a set of guarantees where each guarantee is a safety, reachability, or liveness condition.","lang":"eng"}],"date_published":"2013-12-11T00:00:00Z","related_material":{"record":[{"relation":"earlier_version","id":"5406","status":"public"}]},"project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"date_updated":"2023-02-23T12:24:53Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"doi":"10.1109/FMCAD.2013.6679386","ec_funded":1,"citation":{"short":"K. Chatterjee, T.A. Henzinger, J. Otop, A. Pavlogiannis, in:, 13th International Conference on Formal Methods in Computer-Aided Design, IEEE, 2013, pp. 18–25.","apa":"Chatterjee, K., Henzinger, T. A., Otop, J., &#38; Pavlogiannis, A. (2013). Distributed synthesis for LTL fragments. In <i>13th International Conference on Formal Methods in Computer-Aided Design</i> (pp. 18–25). Portland, OR, United States: IEEE. <a href=\"https://doi.org/10.1109/FMCAD.2013.6679386\">https://doi.org/10.1109/FMCAD.2013.6679386</a>","ama":"Chatterjee K, Henzinger TA, Otop J, Pavlogiannis A. Distributed synthesis for LTL fragments. In: <i>13th International Conference on Formal Methods in Computer-Aided Design</i>. IEEE; 2013:18-25. doi:<a href=\"https://doi.org/10.1109/FMCAD.2013.6679386\">10.1109/FMCAD.2013.6679386</a>","ieee":"K. Chatterjee, T. A. Henzinger, J. Otop, and A. Pavlogiannis, “Distributed synthesis for LTL fragments,” in <i>13th International Conference on Formal Methods in Computer-Aided Design</i>, Portland, OR, United States, 2013, pp. 18–25.","ista":"Chatterjee K, Henzinger TA, Otop J, Pavlogiannis A. 2013. Distributed synthesis for LTL fragments. 13th International Conference on Formal Methods in Computer-Aided Design. FMCAD: Formal Methods in Computer-Aided Design, 18–25.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Andreas Pavlogiannis. “Distributed Synthesis for LTL Fragments.” In <i>13th International Conference on Formal Methods in Computer-Aided Design</i>, 18–25. IEEE, 2013. <a href=\"https://doi.org/10.1109/FMCAD.2013.6679386\">https://doi.org/10.1109/FMCAD.2013.6679386</a>.","mla":"Chatterjee, Krishnendu, et al. “Distributed Synthesis for LTL Fragments.” <i>13th International Conference on Formal Methods in Computer-Aided Design</i>, IEEE, 2013, pp. 18–25, doi:<a href=\"https://doi.org/10.1109/FMCAD.2013.6679386\">10.1109/FMCAD.2013.6679386</a>."},"conference":{"name":"FMCAD: Formal Methods in Computer-Aided Design","start_date":"2013-10-20","end_date":"2013-10-23","location":"Portland, OR, United States"},"title":"Distributed synthesis for LTL fragments","publist_id":"5835","day":"11","oa_version":"None","year":"2013","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","first_name":"Jan","full_name":"Otop, Jan"},{"last_name":"Pavlogiannis","first_name":"Andreas","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87"}],"type":"conference"},{"related_material":{"record":[{"relation":"used_in_publication","id":"2247","status":"public"}]},"date_updated":"2023-02-23T10:34:39Z","user_id":"6785fbc1-c503-11eb-8a32-93094b40e1cf","doi":"10.1371/journal.pone.0080814.s001","citation":{"ama":"Zagorsky B, Reiter J, Chatterjee K, Nowak M. Forgiver triumphs in alternating prisoner’s dilemma . 2013. doi:<a href=\"https://doi.org/10.1371/journal.pone.0080814.s001\">10.1371/journal.pone.0080814.s001</a>","apa":"Zagorsky, B., Reiter, J., Chatterjee, K., &#38; Nowak, M. (2013). Forgiver triumphs in alternating prisoner’s dilemma . Public Library of Science. <a href=\"https://doi.org/10.1371/journal.pone.0080814.s001\">https://doi.org/10.1371/journal.pone.0080814.s001</a>","short":"B. Zagorsky, J. Reiter, K. Chatterjee, M. Nowak, (2013).","mla":"Zagorsky, Benjamin, et al. <i>Forgiver Triumphs in Alternating Prisoner’s Dilemma </i>. Public Library of Science, 2013, doi:<a href=\"https://doi.org/10.1371/journal.pone.0080814.s001\">10.1371/journal.pone.0080814.s001</a>.","chicago":"Zagorsky, Benjamin, Johannes Reiter, Krishnendu Chatterjee, and Martin Nowak. “Forgiver Triumphs in Alternating Prisoner’s Dilemma .” Public Library of Science, 2013. <a href=\"https://doi.org/10.1371/journal.pone.0080814.s001\">https://doi.org/10.1371/journal.pone.0080814.s001</a>.","ista":"Zagorsky B, Reiter J, Chatterjee K, Nowak M. 2013. Forgiver triumphs in alternating prisoner’s dilemma , Public Library of Science, <a href=\"https://doi.org/10.1371/journal.pone.0080814.s001\">10.1371/journal.pone.0080814.s001</a>.","ieee":"B. Zagorsky, J. Reiter, K. Chatterjee, and M. Nowak, “Forgiver triumphs in alternating prisoner’s dilemma .” Public Library of Science, 2013."},"title":"Forgiver triumphs in alternating prisoner's dilemma ","day":"12","year":"2013","oa_version":"Published Version","author":[{"last_name":"Zagorsky","first_name":"Benjamin","full_name":"Zagorsky, Benjamin"},{"full_name":"Reiter, Johannes","first_name":"Johannes","last_name":"Reiter","id":"4A918E98-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0170-7353"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"last_name":"Nowak","full_name":"Nowak, Martin","first_name":"Martin"}],"type":"research_data_reference","publisher":"Public Library of Science","department":[{"_id":"KrCh"}],"status":"public","article_processing_charge":"No","month":"12","_id":"9749","date_published":"2013-12-12T00:00:00Z","date_created":"2021-07-28T15:45:07Z","abstract":[{"text":"Cooperative behavior, where one individual incurs a cost to help another, is a wide spread phenomenon. Here we study direct reciprocity in the context of the alternating Prisoner's Dilemma. We consider all strategies that can be implemented by one and two-state automata. We calculate the payoff matrix of all pairwise encounters in the presence of noise. We explore deterministic selection dynamics with and without mutation. Using different error rates and payoff values, we observe convergence to a small number of distinct equilibria. Two of them are uncooperative strict Nash equilibria representing always-defect (ALLD) and Grim. The third equilibrium is mixed and represents a cooperative alliance of several strategies, dominated by a strategy which we call Forgiver. Forgiver cooperates whenever the opponent has cooperated; it defects once when the opponent has defected, but subsequently Forgiver attempts to re-establish cooperation even if the opponent has defected again. Forgiver is not an evolutionarily stable strategy, but the alliance, which it rules, is asymptotically stable. For a wide range of parameter values the most commonly observed outcome is convergence to the mixed equilibrium, dominated by Forgiver. Our results show that although forgiving might incur a short-term loss it can lead to a long-term gain. Forgiveness facilitates stable cooperation in the presence of exploitation and noise.","lang":"eng"}]},{"page":"461 - 473","date_created":"2018-12-11T11:59:13Z","month":"12","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","status":"public","intvolume":"        18","quality_controlled":"1","department":[{"_id":"KrCh"}],"title":"Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives","conference":{"location":"Hyderabad, India","end_date":"2012-12-17","start_date":"2012-12-15","name":"FSTTCS: Foundations of Software Technology and Theoretical Computer Science"},"citation":{"mla":"Chatterjee, Krishnendu, et al. <i>Average Case Analysis of the Classical Algorithm for Markov Decision Processes with Büchi Objectives</i>. Vol. 18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012, pp. 461–73, doi:<a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2012.461\">10.4230/LIPIcs.FSTTCS.2012.461</a>.","chicago":"Chatterjee, Krishnendu, Manas Joglekar, and Nisarg Shah. “Average Case Analysis of the Classical Algorithm for Markov Decision Processes with Büchi Objectives,” 18:461–73. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. <a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2012.461\">https://doi.org/10.4230/LIPIcs.FSTTCS.2012.461</a>.","ieee":"K. Chatterjee, M. Joglekar, and N. Shah, “Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives,” presented at the FSTTCS: Foundations of Software Technology and Theoretical Computer Science, Hyderabad, India, 2012, vol. 18, pp. 461–473.","ista":"Chatterjee K, Joglekar M, Shah N. 2012. Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives. FSTTCS: Foundations of Software Technology and Theoretical Computer Science, LIPIcs, vol. 18, 461–473.","ama":"Chatterjee K, Joglekar M, Shah N. Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives. In: Vol 18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2012:461-473. doi:<a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2012.461\">10.4230/LIPIcs.FSTTCS.2012.461</a>","apa":"Chatterjee, K., Joglekar, M., &#38; Shah, N. (2012). Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives (Vol. 18, pp. 461–473). Presented at the FSTTCS: Foundations of Software Technology and Theoretical Computer Science, Hyderabad, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.FSTTCS.2012.461\">https://doi.org/10.4230/LIPIcs.FSTTCS.2012.461</a>","short":"K. Chatterjee, M. Joglekar, N. Shah, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012, pp. 461–473."},"ec_funded":1,"type":"conference","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Manas","full_name":"Joglekar, Manas","last_name":"Joglekar"},{"first_name":"Nisarg","full_name":"Shah, Nisarg","last_name":"Shah"}],"alternative_title":["LIPIcs"],"day":"10","related_material":{"record":[{"status":"public","id":"1598","relation":"later_version"}]},"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory","grant_number":"S11407"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"doi":"10.4230/LIPIcs.FSTTCS.2012.461","ddc":["000"],"language":[{"iso":"eng"}],"_id":"2715","date_published":"2012-12-10T00:00:00Z","abstract":[{"text":"We consider Markov decision processes (MDPs) with specifications given as Büchi (liveness) objectives. We consider the problem of computing the set of almost-sure winning vertices from where the objective can be ensured with probability 1. We study for the first time the average case complexity of the classical algorithm for computing the set of almost-sure winning vertices for MDPs with Büchi objectives. Our contributions are as follows: First, we show that for MDPs with constant out-degree the expected number of iterations is at most logarithmic and the average case running time is linear (as compared to the worst case linear number of iterations and quadratic time complexity). Second, for the average case analysis over all MDPs we show that the expected number of iterations is constant and the average case running time is linear (again as compared to the worst case linear number of iterations and quadratic time complexity). Finally we also show that given that all MDPs are equally likely, the probability that the classical algorithm requires more than constant number of iterations is exponentially small.","lang":"eng"}],"file":[{"creator":"system","file_size":519040,"file_name":"IST-2016-525-v1+1_42_1_.pdf","access_level":"open_access","date_updated":"2020-07-14T12:45:45Z","checksum":"d4d644ed1a885dbfc4fa1ef4c5724dab","relation":"main_file","file_id":"5040","content_type":"application/pdf","date_created":"2018-12-12T10:13:53Z"}],"oa":1,"publication_status":"published","tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","image":"/images/cc_by_nc_nd.png","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","short":"CC BY-NC-ND (4.0)"},"pubrep_id":"525","volume":18,"file_date_updated":"2020-07-14T12:45:45Z","oa_version":"Published Version","year":"2012","has_accepted_license":"1","publist_id":"4180","scopus_import":1,"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-02-23T10:06:04Z"},{"publisher":"Elsevier","quality_controlled":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publication":"Journal of Theoretical Biology","intvolume":"       301","status":"public","page":"161 - 173","month":"05","date_created":"2018-12-11T11:59:55Z","project":[{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"pmid":1,"language":[{"iso":"eng"}],"doi":"10.1016/j.jtbi.2012.02.021","ec_funded":1,"citation":{"chicago":"Chatterjee, Krishnendu, Damien Zufferey, and Martin Nowak. “Evolutionary Game Dynamics in Populations with Different Learners.” <i>Journal of Theoretical Biology</i>. Elsevier, 2012. <a href=\"https://doi.org/10.1016/j.jtbi.2012.02.021\">https://doi.org/10.1016/j.jtbi.2012.02.021</a>.","ista":"Chatterjee K, Zufferey D, Nowak M. 2012. Evolutionary game dynamics in populations with different learners. Journal of Theoretical Biology. 301, 161–173.","ieee":"K. Chatterjee, D. Zufferey, and M. Nowak, “Evolutionary game dynamics in populations with different learners,” <i>Journal of Theoretical Biology</i>, vol. 301. Elsevier, pp. 161–173, 2012.","mla":"Chatterjee, Krishnendu, et al. “Evolutionary Game Dynamics in Populations with Different Learners.” <i>Journal of Theoretical Biology</i>, vol. 301, Elsevier, 2012, pp. 161–73, doi:<a href=\"https://doi.org/10.1016/j.jtbi.2012.02.021\">10.1016/j.jtbi.2012.02.021</a>.","short":"K. Chatterjee, D. Zufferey, M. Nowak, Journal of Theoretical Biology 301 (2012) 161–173.","ama":"Chatterjee K, Zufferey D, Nowak M. Evolutionary game dynamics in populations with different learners. <i>Journal of Theoretical Biology</i>. 2012;301:161-173. doi:<a href=\"https://doi.org/10.1016/j.jtbi.2012.02.021\">10.1016/j.jtbi.2012.02.021</a>","apa":"Chatterjee, K., Zufferey, D., &#38; Nowak, M. (2012). Evolutionary game dynamics in populations with different learners. <i>Journal of Theoretical Biology</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.jtbi.2012.02.021\">https://doi.org/10.1016/j.jtbi.2012.02.021</a>"},"title":"Evolutionary game dynamics in populations with different learners","day":"21","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Zufferey","full_name":"Zufferey, Damien","first_name":"Damien","orcid":"0000-0002-3197-8736","id":"4397AC76-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Nowak","first_name":"Martin","full_name":"Nowak, Martin"}],"type":"journal_article","publication_status":"published","main_file_link":[{"open_access":"1","url":"http://www.ncbi.nlm.nih.gov/pmc/articles/PMC3322297/"}],"oa":1,"volume":301,"date_published":"2012-05-21T00:00:00Z","_id":"2848","abstract":[{"text":"We study evolutionary game theory in a setting where individuals learn from each other. We extend the traditional approach by assuming that a population contains individuals with different learning abilities. In particular, we explore the situation where individuals have different search spaces, when attempting to learn the strategies of others. The search space of an individual specifies the set of strategies learnable by that individual. The search space is genetically given and does not change under social evolutionary dynamics. We introduce a general framework and study a specific example in the context of direct reciprocity. For this example, we obtain the counter intuitive result that cooperation can only evolve for intermediate benefit-to-cost ratios, while small and large benefit-to-cost ratios favor defection. Our paper is a step toward making a connection between computational learning theory and evolutionary game dynamics.","lang":"eng"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T07:00:12Z","scopus_import":1,"external_id":{"pmid":["22394652"]},"publist_id":"3946","year":"2012","oa_version":"Submitted Version"},{"project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"related_material":{"record":[{"status":"public","id":"1733","relation":"later_version"}]},"doi":"10.4204/EPTCS.96.3","language":[{"iso":"eng"}],"title":"Interface Simulation Distances","conference":{"location":"Napoli, Italy","name":"GandALF: Games, Automata, Logic, and Formal Verification","start_date":"2012-09-06","end_date":"2012-09-08"},"citation":{"ista":"Cerny P, Chmelik M, Henzinger TA, Radhakrishna A. 2012. Interface Simulation Distances. Electronic Proceedings in Theoretical Computer Science. GandALF: Games, Automata, Logic, and Formal Verification vol. 96, 29–42.","ieee":"P. Cerny, M. Chmelik, T. A. Henzinger, and A. Radhakrishna, “Interface Simulation Distances,” in <i>Electronic Proceedings in Theoretical Computer Science</i>, Napoli, Italy, 2012, vol. 96, pp. 29–42.","chicago":"Cerny, Pavol, Martin Chmelik, Thomas A Henzinger, and Arjun Radhakrishna. “Interface Simulation Distances.” In <i>Electronic Proceedings in Theoretical Computer Science</i>, 96:29–42. EPTCS, 2012. <a href=\"https://doi.org/10.4204/EPTCS.96.3\">https://doi.org/10.4204/EPTCS.96.3</a>.","mla":"Cerny, Pavol, et al. “Interface Simulation Distances.” <i>Electronic Proceedings in Theoretical Computer Science</i>, vol. 96, EPTCS, 2012, pp. 29–42, doi:<a href=\"https://doi.org/10.4204/EPTCS.96.3\">10.4204/EPTCS.96.3</a>.","short":"P. Cerny, M. Chmelik, T.A. Henzinger, A. Radhakrishna, in:, Electronic Proceedings in Theoretical Computer Science, EPTCS, 2012, pp. 29–42.","apa":"Cerny, P., Chmelik, M., Henzinger, T. A., &#38; Radhakrishna, A. (2012). Interface Simulation Distances. In <i>Electronic Proceedings in Theoretical Computer Science</i> (Vol. 96, pp. 29–42). Napoli, Italy: EPTCS. <a href=\"https://doi.org/10.4204/EPTCS.96.3\">https://doi.org/10.4204/EPTCS.96.3</a>","ama":"Cerny P, Chmelik M, Henzinger TA, Radhakrishna A. Interface Simulation Distances. In: <i>Electronic Proceedings in Theoretical Computer Science</i>. Vol 96. EPTCS; 2012:29-42. doi:<a href=\"https://doi.org/10.4204/EPTCS.96.3\">10.4204/EPTCS.96.3</a>"},"ec_funded":1,"author":[{"full_name":"Cerny, Pavol","first_name":"Pavol","last_name":"Cerny","id":"4DCBEFFE-F248-11E8-B48F-1D18A9856A87"},{"id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik","first_name":"Martin","full_name":"Chmelik, Martin"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"last_name":"Radhakrishna","full_name":"Radhakrishna, Arjun","first_name":"Arjun","id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87"}],"type":"conference","day":"07","publisher":"EPTCS","intvolume":"        96","status":"public","publication":"Electronic Proceedings in Theoretical Computer Science","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"quality_controlled":"1","page":"29 - 42","date_created":"2018-12-11T12:00:19Z","month":"10","external_id":{"arxiv":["1210.2450"]},"scopus_import":1,"date_updated":"2023-02-23T10:12:05Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Submitted Version","year":"2012","publist_id":"3827","main_file_link":[{"url":"http://arxiv.org/abs/1210.2450","open_access":"1"}],"oa":1,"publication_status":"published","volume":96,"arxiv":1,"_id":"2916","date_published":"2012-10-07T00:00:00Z","abstract":[{"lang":"eng","text":"The classical (boolean) notion of refinement for behavioral interfaces of system components is the alternating refinement preorder. In this paper, we define a quantitative measure for interfaces, called interface simulation distance. It makes the alternating refinement preorder quantitative by, intu- itively, tolerating errors (while counting them) in the alternating simulation game. We show that the interface simulation distance satisfies the triangle inequality, that the distance between two interfaces does not increase under parallel composition with a third interface, and that the distance between two interfaces can be bounded from above and below by distances between abstractions of the two interfaces. We illustrate the framework, and the properties of the distances under composition of interfaces, with two case studies."}]},{"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1207.7019"}],"oa":1,"publication_status":"published","_id":"2936","date_published":"2012-10-01T00:00:00Z","abstract":[{"text":"The notion of delays arises naturally in many computational models, such as, in the design of circuits, control systems, and dataflow languages. In this work, we introduce automata with delay blocks (ADBs), extending finite state automata with variable time delay blocks, for deferring individual transition output symbols, in a discrete-time setting. We show that the ADB languages strictly subsume the regular languages, and are incomparable in expressive power to the context-free languages. We show that ADBs are closed under union, concatenation and Kleene star, and under intersection with regular languages, but not closed under complementation and intersection with other ADB languages. We show that the emptiness and the membership problems are decidable in polynomial time for ADBs, whereas the universality problem is undecidable. Finally we consider the linear-time model checking problem, i.e., whether the language of an ADB is contained in a regular language, and show that the model checking problem is PSPACE-complete. Copyright 2012 ACM.","lang":"eng"}],"scopus_import":1,"date_updated":"2021-01-12T07:39:53Z","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","year":"2012","oa_version":"Preprint","publist_id":"3799","publisher":"ACM","status":"public","publication":"roceedings of the tenth ACM international conference on Embedded software","quality_controlled":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"page":"43 - 52","date_created":"2018-12-11T12:00:26Z","month":"10","project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"acknowledgement":"This work has been financially supported in part by the European Commission FP7-ICT Cognitive Systems, Interaction, and Robotics under the contract # 270180 (NOPTILUS); by Fundacao para Ciencia e Tecnologia under project PTDC/EEA-CRO/104901/2008 (Modeling and control of Networked vehicle systems in persistent autonomous operations); by Austrian Science Fund (FWF) Grant No P 23499-N23 on Modern Graph Algorithmic Techniques in Formal Verification; FWF NFN Grant No S11407-N23 (RiSE); ERC Start grant (279307: Graph Games); Microsoft faculty fellows award; ERC Advanced grant QUAREM; and FWF Grant No S11403-N23 (RiSE).","doi":"10.1145/2380356.2380370","language":[{"iso":"eng"}],"title":"Finite automata with time delay blocks","conference":{"name":"EMSOFT: Embedded Software ","start_date":"2012-10-07","end_date":"2012-10-12","location":"Tampere, Finland"},"citation":{"ieee":"K. Chatterjee, T. A. Henzinger, and V. Prabhu, “Finite automata with time delay blocks,” in <i>roceedings of the tenth ACM international conference on Embedded software</i>, Tampere, Finland, 2012, pp. 43–52.","ista":"Chatterjee K, Henzinger TA, Prabhu V. 2012. Finite automata with time delay blocks. roceedings of the tenth ACM international conference on Embedded software. EMSOFT: Embedded Software , 43–52.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Vinayak Prabhu. “Finite Automata with Time Delay Blocks.” In <i>Roceedings of the Tenth ACM International Conference on Embedded Software</i>, 43–52. ACM, 2012. <a href=\"https://doi.org/10.1145/2380356.2380370\">https://doi.org/10.1145/2380356.2380370</a>.","mla":"Chatterjee, Krishnendu, et al. “Finite Automata with Time Delay Blocks.” <i>Roceedings of the Tenth ACM International Conference on Embedded Software</i>, ACM, 2012, pp. 43–52, doi:<a href=\"https://doi.org/10.1145/2380356.2380370\">10.1145/2380356.2380370</a>.","short":"K. Chatterjee, T.A. Henzinger, V. Prabhu, in:, Roceedings of the Tenth ACM International Conference on Embedded Software, ACM, 2012, pp. 43–52.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Prabhu, V. (2012). Finite automata with time delay blocks. In <i>roceedings of the tenth ACM international conference on Embedded software</i> (pp. 43–52). Tampere, Finland: ACM. <a href=\"https://doi.org/10.1145/2380356.2380370\">https://doi.org/10.1145/2380356.2380370</a>","ama":"Chatterjee K, Henzinger TA, Prabhu V. Finite automata with time delay blocks. In: <i>Roceedings of the Tenth ACM International Conference on Embedded Software</i>. ACM; 2012:43-52. doi:<a href=\"https://doi.org/10.1145/2380356.2380370\">10.1145/2380356.2380370</a>"},"ec_funded":1,"author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"last_name":"Prabhu","first_name":"Vinayak","full_name":"Prabhu, Vinayak"}],"type":"conference","day":"01"},{"date_published":"2012-06-01T00:00:00Z","_id":"2947","abstract":[{"lang":"eng","text":"We introduce games with probabilistic uncertainty, a model for controller synthesis in which the controller observes the state through imprecise sensors that provide correct information about the current state with a fixed probability. That is, in each step, the sensors return an observed state, and given the observed state, there is a probability distribution (due to the estimation error) over the actual current state. The controller must base its decision on the observed state (rather than the actual current state, which it does not know). On the other hand, we assume that the environment can perfectly observe the current state. We show that controller synthesis for qualitative ω-regular objectives in our model can be reduced in polynomial time to standard partial-observation stochastic games, and vice-versa. As a consequence we establish the precise decidability frontier for the new class of games, and establish optimal complexity results for all the decidable problems."}],"main_file_link":[{"url":"http://arxiv.org/abs/1202.4140","open_access":"1"}],"oa":1,"publication_status":"published","volume":7561,"oa_version":"Preprint","year":"2012","publist_id":"3785","date_updated":"2021-01-12T07:39:58Z","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"page":"385 - 399","date_created":"2018-12-11T12:00:29Z","month":"06","publisher":"Springer","status":"public","intvolume":"      7561","quality_controlled":"1","department":[{"_id":"KrCh"}],"conference":{"location":"Thiruvananthapuram, India","start_date":"2012-10-03","end_date":"2012-10-06","name":" ATVA: Automated Technology for Verification and Analysis"},"title":"Equivalence of games with probabilistic uncertainty and partial observation games","ec_funded":1,"citation":{"chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Ritankar Majumdar. “Equivalence of Games with Probabilistic Uncertainty and Partial Observation Games,” 7561:385–99. Springer, 2012. <a href=\"https://doi.org/10.1007/978-3-642-33386-6_30\">https://doi.org/10.1007/978-3-642-33386-6_30</a>.","ieee":"K. Chatterjee, M. Chmelik, and R. Majumdar, “Equivalence of games with probabilistic uncertainty and partial observation games,” presented at the  ATVA: Automated Technology for Verification and Analysis, Thiruvananthapuram, India, 2012, vol. 7561, pp. 385–399.","ista":"Chatterjee K, Chmelik M, Majumdar R. 2012. Equivalence of games with probabilistic uncertainty and partial observation games.  ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 7561, 385–399.","mla":"Chatterjee, Krishnendu, et al. <i>Equivalence of Games with Probabilistic Uncertainty and Partial Observation Games</i>. Vol. 7561, Springer, 2012, pp. 385–99, doi:<a href=\"https://doi.org/10.1007/978-3-642-33386-6_30\">10.1007/978-3-642-33386-6_30</a>.","short":"K. Chatterjee, M. Chmelik, R. Majumdar, in:, Springer, 2012, pp. 385–399.","ama":"Chatterjee K, Chmelik M, Majumdar R. Equivalence of games with probabilistic uncertainty and partial observation games. In: Vol 7561. Springer; 2012:385-399. doi:<a href=\"https://doi.org/10.1007/978-3-642-33386-6_30\">10.1007/978-3-642-33386-6_30</a>","apa":"Chatterjee, K., Chmelik, M., &#38; Majumdar, R. (2012). Equivalence of games with probabilistic uncertainty and partial observation games (Vol. 7561, pp. 385–399). Presented at the  ATVA: Automated Technology for Verification and Analysis, Thiruvananthapuram, India: Springer. <a href=\"https://doi.org/10.1007/978-3-642-33386-6_30\">https://doi.org/10.1007/978-3-642-33386-6_30</a>"},"alternative_title":["LNCS"],"author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Chmelik, Martin","first_name":"Martin","last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Ritankar","full_name":"Majumdar, Ritankar","last_name":"Majumdar"}],"type":"conference","day":"01","acknowledgement":"The research was supported by Austrian Science Fund (FWF) Grant No P 23499-N23 on Modern Graph Algorithmic Techniques in Formal Verification, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.","project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"doi":"10.1007/978-3-642-33386-6_30","language":[{"iso":"eng"}]},{"publisher":"IEEE","publication":"Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science","quality_controlled":"1","department":[{"_id":"KrCh"}],"status":"public","month":"08","date_created":"2018-12-11T12:00:32Z","related_material":{"record":[{"relation":"later_version","id":"2211","status":"public"},{"relation":"earlier_version","id":"5381","status":"public"}]},"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"acknowledgement":"This work was partially supported by FWF Grant No P 23499-N23, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.","language":[{"iso":"eng"}],"doi":"10.1109/LICS.2012.28","citation":{"chicago":"Chatterjee, Krishnendu, and Laurent Doyen. “Partial-Observation Stochastic Games: How to Win When Belief Fails.” In <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. IEEE, 2012. <a href=\"https://doi.org/10.1109/LICS.2012.28\">https://doi.org/10.1109/LICS.2012.28</a>.","ieee":"K. Chatterjee and L. Doyen, “Partial-observation stochastic games: How to win when belief fails,” in <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Dubrovnik, Croatia, 2012.","ista":"Chatterjee K, Doyen L. 2012. Partial-observation stochastic games: How to win when belief fails. Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 6280436.","mla":"Chatterjee, Krishnendu, and Laurent Doyen. “Partial-Observation Stochastic Games: How to Win When Belief Fails.” <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, 6280436, IEEE, 2012, doi:<a href=\"https://doi.org/10.1109/LICS.2012.28\">10.1109/LICS.2012.28</a>.","short":"K. Chatterjee, L. Doyen, in:, Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2012.","ama":"Chatterjee K, Doyen L. Partial-observation stochastic games: How to win when belief fails. In: <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. IEEE; 2012. doi:<a href=\"https://doi.org/10.1109/LICS.2012.28\">10.1109/LICS.2012.28</a>","apa":"Chatterjee, K., &#38; Doyen, L. (2012). Partial-observation stochastic games: How to win when belief fails. In <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. Dubrovnik, Croatia: IEEE. <a href=\"https://doi.org/10.1109/LICS.2012.28\">https://doi.org/10.1109/LICS.2012.28</a>"},"ec_funded":1,"title":"Partial-observation stochastic games: How to win when belief fails","conference":{"start_date":"2012-06-25","end_date":"2012-06-28","name":"LICS: Logic in Computer Science","location":"Dubrovnik, Croatia"},"day":"23","type":"conference","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Doyen","first_name":"Laurent","full_name":"Doyen, Laurent"}],"publication_status":"published","main_file_link":[{"url":"http://arxiv.org/abs/1107.2141","open_access":"1"}],"oa":1,"arxiv":1,"article_number":"6280436","_id":"2955","abstract":[{"lang":"eng","text":"We consider two-player stochastic games played on finite graphs with reachability objectives where the first player tries to ensure a target state to be visited almost-surely (i.e., with probability 1), or positively (i.e., with positive probability), no matter the strategy of the second player. We classify such games according to the information and the power of randomization available to the players. On the basis of information, the game can be one-sided with either (a) player 1, or (b) player 2 having partial observation (and the other player has perfect observation), or two-sided with (c) both players having partial observation. On the basis of randomization, the players (a) may not be allowed to use randomization (pure strategies), or (b) may choose a probability distribution over actions but the actual random choice is external and not visible to the player (actions invisible), or (c) may use full randomization. Our main results for pure strategies are as follows. (1) For one-sided games with player 1 having partial observation we show that (in contrast to full randomized strategies) belief-based (subset-construction based) strategies are not sufficient, and we present an exponential upper bound on memory both for almostsure and positive winning strategies; we show that the problem of deciding the existence of almost-sure and positive winning strategies for player 1 is EXPTIME-complete. (2) For one-sided games with player 2 having partial observation we show that non-elementary memory is both necessary and sufficient for both almost-sure and positive winning strategies. (3) We show that for the general (two-sided) case finite-memory strategies are sufficient for both positive and almost-sure winning, and at least non-elementary memory is required. We establish the equivalence of the almost-sure winning problems for pure strategies and for randomized strategies with actions invisible. Our equivalence result exhibits serious flaws in previous results of the literature: we show a non-elementary memory lower bound for almost-sure winning whereas an exponential upper bound was previously claimed."}],"date_published":"2012-08-23T00:00:00Z","external_id":{"arxiv":["1107.2141"]},"scopus_import":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-02-23T12:23:43Z","publist_id":"3771","year":"2012","oa_version":"Preprint"},{"year":"2012","oa_version":"None","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"first_name":"Yaron","full_name":"Velner, Yaron","last_name":"Velner"}],"type":"conference","day":"23","publist_id":"3770","conference":{"end_date":"2012-06-28","start_date":"2012-06-25","name":"LICS: Logic in Computer Science","location":"Dubrovnik, Croatia "},"title":"Mean payoff pushdown games","ec_funded":1,"citation":{"short":"K. Chatterjee, Y. Velner, in:, Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2012.","apa":"Chatterjee, K., &#38; Velner, Y. (2012). Mean payoff pushdown games. In <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. Dubrovnik, Croatia : IEEE. <a href=\"https://doi.org/10.1109/LICS.2012.30\">https://doi.org/10.1109/LICS.2012.30</a>","ama":"Chatterjee K, Velner Y. Mean payoff pushdown games. In: <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. IEEE; 2012. doi:<a href=\"https://doi.org/10.1109/LICS.2012.30\">10.1109/LICS.2012.30</a>","ieee":"K. Chatterjee and Y. Velner, “Mean payoff pushdown games,” in <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Dubrovnik, Croatia , 2012.","ista":"Chatterjee K, Velner Y. 2012. Mean payoff pushdown games. Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 6280438.","chicago":"Chatterjee, Krishnendu, and Yaron Velner. “Mean Payoff Pushdown Games.” In <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. IEEE, 2012. <a href=\"https://doi.org/10.1109/LICS.2012.30\">https://doi.org/10.1109/LICS.2012.30</a>.","mla":"Chatterjee, Krishnendu, and Yaron Velner. “Mean Payoff Pushdown Games.” <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, 6280438, IEEE, 2012, doi:<a href=\"https://doi.org/10.1109/LICS.2012.30\">10.1109/LICS.2012.30</a>."},"doi":"10.1109/LICS.2012.30","date_updated":"2023-02-23T12:23:30Z","language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"acknowledgement":"The research was supported by Austrian Science Fund (FWF) Grant No P 23499-N23, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), Microsoft faculty fellows award, the Israeli Centers of Research Excellence (ICORE) program, (Center No. 4/11), the RICH Model Toolkit (ICT COST Action IC0901), and was carried out in partial fulfillment of the requirements for the Ph.D. degree of the second author.\r\nA Technical Report of this paper is available via internal link.","related_material":{"record":[{"relation":"earlier_version","id":"5377","status":"public"}]},"project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"_id":"2956","abstract":[{"text":"Two-player games on graphs are central in many problems in formal verification and program analysis such as synthesis and verification of open systems. In this work we consider solving recursive game graphs (or pushdown game graphs) that can model the control flow of sequential programs with recursion. While pushdown games have been studied before with qualitative objectives, such as reachability and parity objectives, in this work we study for the first time such games with the most well-studied quantitative objective, namely, mean payoff objectives. In pushdown games two types of strategies are relevant: (1) global strategies, that depend on the entire global history; and (2) modular strategies, that have only local memory and thus do not depend on the context of invocation, but only on the history of the current invocation of the module. Our main results are as follows: (1) One-player pushdown games with mean-payoff objectives under global strategies are decidable in polynomial time. (2) Two-player pushdown games with mean-payoff objectives under global strategies are undecidable. (3) One-player pushdown games with mean-payoff objectives under modular strategies are NP-hard. (4) Two-player pushdown games with mean-payoff objectives under modular strategies can be solved in NP (i.e., both one-player and two-player pushdown games with mean-payoff objectives under modular strategies are NP-complete). We also establish the optimal strategy complexity showing that global strategies for mean-payoff objectives require infinite memory even in one-player pushdown games; and memoryless modular strategies are sufficient in two-player pushdown games. Finally we also show that all the problems have the same computational complexity if the stack boundedness condition is added, where along with the mean-payoff objective the player must also ensure that the stack height is bounded.","lang":"eng"}],"date_created":"2018-12-11T12:00:32Z","date_published":"2012-08-23T00:00:00Z","article_number":"6280438","month":"08","status":"public","department":[{"_id":"KrCh"}],"quality_controlled":"1","publication":"Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science","publication_status":"published","publisher":"IEEE"},{"article_number":"6280437","_id":"2957","date_published":"2012-08-23T00:00:00Z","abstract":[{"lang":"eng","text":"We consider probabilistic automata on infinite words with acceptance defined by parity conditions. We consider three qualitative decision problems: (i) the positive decision problem asks whether there is a word that is accepted with positive probability; (ii) the almost decision problem asks whether there is a word that is accepted with probability 1; and (iii) the limit decision problem asks whether words are accepted with probability arbitrarily close to 1. We unify and generalize several decidability results for probabilistic automata over infinite words, and identify a robust (closed under union and intersection) subclass of probabilistic automata for which all the qualitative decision problems are decidable for parity conditions. We also show that if the input words are restricted to lasso shape (regular) words, then the positive and almost problems are decidable for all probabilistic automata with parity conditions. For most decidable problems we show an optimal PSPACE-complete complexity bound."}],"arxiv":1,"publication_status":"published","oa":1,"main_file_link":[{"url":"https://arxiv.org/abs/1107.2091","open_access":"1"}],"publist_id":"3769","year":"2012","oa_version":"Preprint","date_updated":"2023-02-23T12:23:51Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"external_id":{"arxiv":["1107.2091"]},"month":"08","date_created":"2018-12-11T12:00:33Z","department":[{"_id":"KrCh"}],"quality_controlled":"1","publication":"Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science","status":"public","publisher":"IEEE","day":"23","type":"conference","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Tracol, Mathieu","first_name":"Mathieu","last_name":"Tracol","id":"3F54FA38-F248-11E8-B48F-1D18A9856A87"}],"ec_funded":1,"citation":{"ista":"Chatterjee K, Tracol M. 2012. Decidable problems for probabilistic automata on infinite words. Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 6280437.","ieee":"K. Chatterjee and M. Tracol, “Decidable problems for probabilistic automata on infinite words,” in <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Dubrovnik, Croatia , 2012.","chicago":"Chatterjee, Krishnendu, and Mathieu Tracol. “Decidable Problems for Probabilistic Automata on Infinite Words.” In <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. IEEE, 2012. <a href=\"https://doi.org/10.1109/LICS.2012.29\">https://doi.org/10.1109/LICS.2012.29</a>.","mla":"Chatterjee, Krishnendu, and Mathieu Tracol. “Decidable Problems for Probabilistic Automata on Infinite Words.” <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, 6280437, IEEE, 2012, doi:<a href=\"https://doi.org/10.1109/LICS.2012.29\">10.1109/LICS.2012.29</a>.","short":"K. Chatterjee, M. Tracol, in:, Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2012.","apa":"Chatterjee, K., &#38; Tracol, M. (2012). Decidable problems for probabilistic automata on infinite words. In <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. Dubrovnik, Croatia : IEEE. <a href=\"https://doi.org/10.1109/LICS.2012.29\">https://doi.org/10.1109/LICS.2012.29</a>","ama":"Chatterjee K, Tracol M. Decidable problems for probabilistic automata on infinite words. In: <i>Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. IEEE; 2012. doi:<a href=\"https://doi.org/10.1109/LICS.2012.29\">10.1109/LICS.2012.29</a>"},"conference":{"start_date":"2012-06-25","end_date":"2012-06-28","name":"LICS: Logic in Computer Science","location":"Dubrovnik, Croatia "},"title":"Decidable problems for probabilistic automata on infinite words","language":[{"iso":"eng"}],"doi":"10.1109/LICS.2012.29","related_material":{"record":[{"relation":"earlier_version","id":"5384","status":"public"}]},"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}]},{"month":"11","date_created":"2018-12-11T12:00:37Z","page":"49 - 60","department":[{"_id":"KrCh"}],"quality_controlled":"1","publication":"Theoretical Computer Science","intvolume":"       458","status":"public","publisher":"Elsevier","day":"02","type":"journal_article","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Doyen, Laurent","first_name":"Laurent","last_name":"Doyen"}],"ec_funded":1,"citation":{"ista":"Chatterjee K, Doyen L. 2012. Energy parity games. Theoretical Computer Science. 458, 49–60.","ieee":"K. Chatterjee and L. Doyen, “Energy parity games,” <i>Theoretical Computer Science</i>, vol. 458. Elsevier, pp. 49–60, 2012.","chicago":"Chatterjee, Krishnendu, and Laurent Doyen. “Energy Parity Games.” <i>Theoretical Computer Science</i>. Elsevier, 2012. <a href=\"https://doi.org/10.1016/j.tcs.2012.07.038\">https://doi.org/10.1016/j.tcs.2012.07.038</a>.","mla":"Chatterjee, Krishnendu, and Laurent Doyen. “Energy Parity Games.” <i>Theoretical Computer Science</i>, vol. 458, Elsevier, 2012, pp. 49–60, doi:<a href=\"https://doi.org/10.1016/j.tcs.2012.07.038\">10.1016/j.tcs.2012.07.038</a>.","short":"K. Chatterjee, L. Doyen, Theoretical Computer Science 458 (2012) 49–60.","apa":"Chatterjee, K., &#38; Doyen, L. (2012). Energy parity games. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2012.07.038\">https://doi.org/10.1016/j.tcs.2012.07.038</a>","ama":"Chatterjee K, Doyen L. Energy parity games. <i>Theoretical Computer Science</i>. 2012;458:49-60. doi:<a href=\"https://doi.org/10.1016/j.tcs.2012.07.038\">10.1016/j.tcs.2012.07.038</a>"},"title":"Energy parity games","language":[{"iso":"eng"}],"doi":"10.1016/j.tcs.2012.07.038","ddc":["004"],"project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"related_material":{"record":[{"relation":"earlier_version","id":"3851","status":"public"}]},"file":[{"creator":"kschuh","file_size":351271,"file_name":"2012_Elsevier_Chatterjee.pdf","checksum":"719e4a5af5a01ad3f2f7f7f05b3c2b09","access_level":"open_access","date_updated":"2020-07-14T12:45:57Z","relation":"main_file","file_id":"5935","content_type":"application/pdf","date_created":"2019-02-06T11:56:22Z"}],"_id":"2972","date_published":"2012-11-02T00:00:00Z","abstract":[{"lang":"eng","text":"Energy parity games are infinite two-player turn-based games played on weighted graphs. The objective of the game combines a (qualitative) parity condition with the (quantitative) requirement that the sum of the weights (i.e., the level of energy in the game) must remain positive. Beside their own interest in the design and synthesis of resource-constrained omega-regular specifications, energy parity games provide one of the simplest model of games with combined qualitative and quantitative objectives. Our main results are as follows: (a) exponential memory is sufficient and may be necessary for winning strategies in energy parity games; (b) the problem of deciding the winner in energy parity games can be solved in NP ∩ coNP; and (c) we give an algorithm to solve energy parity by reduction to energy games. We also show that the problem of deciding the winner in energy parity games is logspace-equivalent to the problem of deciding the winner in mean-payoff parity games, which can thus be solved in NP ∩ coNP. As a consequence we also obtain a conceptually simple algorithm to solve mean-payoff parity games."}],"arxiv":1,"file_date_updated":"2020-07-14T12:45:57Z","volume":458,"tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","image":"/images/cc_by_nc_nd.png","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","short":"CC BY-NC-ND (4.0)"},"pubrep_id":"935","publication_status":"published","oa":1,"publist_id":"3736","oa_version":"Published Version","has_accepted_license":"1","year":"2012","date_updated":"2023-02-23T11:45:29Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","external_id":{"arxiv":["1001.5183"]},"scopus_import":1},{"pubrep_id":"303","volume":43,"file_date_updated":"2020-07-14T12:46:00Z","oa":1,"publication_status":"published","date_published":"2012-10-01T00:00:00Z","_id":"3128","abstract":[{"text":"We consider two-player zero-sum stochastic games on graphs with ω-regular winning conditions specified as parity objectives. These games have applications in the design and control of reactive systems. We survey the complexity results for the problem of deciding the winner in such games, and in classes of interest obtained as special cases, based on the information and the power of randomization available to the players, on the class of objectives and on the winning mode. On the basis of information, these games can be classified as follows: (a) partial-observation (both players have partial view of the game); (b) one-sided partial-observation (one player has partial-observation and the other player has complete-observation); and (c) complete-observation (both players have complete view of the game). The one-sided partial-observation games have two important subclasses: the one-player games, known as partial-observation Markov decision processes (POMDPs), and the blind one-player games, known as probabilistic automata. On the basis of randomization, (a) the players may not be allowed to use randomization (pure strategies), or (b) they may choose a probability distribution over actions but the actual random choice is external and not visible to the player (actions invisible), or (c) they may use full randomization. Finally, various classes of games are obtained by restricting the parity objective to a reachability, safety, Büchi, or coBüchi condition. We also consider several winning modes, such as sure-winning (i.e., all outcomes of a strategy have to satisfy the winning condition), almost-sure winning (i.e., winning with probability 1), limit-sure winning (i.e., winning with probability arbitrarily close to 1), and value-threshold winning (i.e., winning with probability at least ν, where ν is a given rational). ","lang":"eng"}],"file":[{"date_created":"2018-12-12T10:11:27Z","content_type":"application/pdf","file_id":"4882","relation":"main_file","checksum":"dd3d590f383bb2ac6cfda1489ac1c42a","date_updated":"2020-07-14T12:46:00Z","access_level":"open_access","file_name":"IST-2014-303-v1+1_Survey_Partial-Observation_Stochastic_Parity_Games.pdf","creator":"system","file_size":163983}],"issue":"2","scopus_import":1,"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T07:41:15Z","has_accepted_license":"1","year":"2012","oa_version":"Submitted Version","publist_id":"3570","intvolume":"        43","status":"public","publication":"Formal Methods in System Design","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"quality_controlled":"1","publisher":"Springer","date_created":"2018-12-11T12:01:33Z","month":"10","page":"268 - 284","ddc":["005"],"doi":"10.1007/s10703-012-0164-2","language":[{"iso":"eng"}],"project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"acknowledgement":"The research was supported by Austrian Science Fund (FWF) Grant No. P 23499-N23 on Modern Graph Algorithmic Techniques in Formal Verification, FWF NFN Grant No. S11407-N23(RiSE), ERC Start grant (279307: Graph Games), Microsoft faculty fellows award, ERC Advanced grant QUAREM, and FWF Grant No. S11403-N23 (RiSE).","type":"journal_article","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"full_name":"Doyen, Laurent","first_name":"Laurent","last_name":"Doyen"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"}],"day":"01","title":"A survey of partial-observation stochastic parity games","citation":{"chicago":"Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “A Survey of Partial-Observation Stochastic Parity Games.” <i>Formal Methods in System Design</i>. Springer, 2012. <a href=\"https://doi.org/10.1007/s10703-012-0164-2\">https://doi.org/10.1007/s10703-012-0164-2</a>.","ista":"Chatterjee K, Doyen L, Henzinger TA. 2012. A survey of partial-observation stochastic parity games. Formal Methods in System Design. 43(2), 268–284.","ieee":"K. Chatterjee, L. Doyen, and T. A. Henzinger, “A survey of partial-observation stochastic parity games,” <i>Formal Methods in System Design</i>, vol. 43, no. 2. Springer, pp. 268–284, 2012.","mla":"Chatterjee, Krishnendu, et al. “A Survey of Partial-Observation Stochastic Parity Games.” <i>Formal Methods in System Design</i>, vol. 43, no. 2, Springer, 2012, pp. 268–84, doi:<a href=\"https://doi.org/10.1007/s10703-012-0164-2\">10.1007/s10703-012-0164-2</a>.","short":"K. Chatterjee, L. Doyen, T.A. Henzinger, Formal Methods in System Design 43 (2012) 268–284.","ama":"Chatterjee K, Doyen L, Henzinger TA. A survey of partial-observation stochastic parity games. <i>Formal Methods in System Design</i>. 2012;43(2):268-284. doi:<a href=\"https://doi.org/10.1007/s10703-012-0164-2\">10.1007/s10703-012-0164-2</a>","apa":"Chatterjee, K., Doyen, L., &#38; Henzinger, T. A. (2012). A survey of partial-observation stochastic parity games. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1007/s10703-012-0164-2\">https://doi.org/10.1007/s10703-012-0164-2</a>"},"ec_funded":1},{"publist_id":"3562","year":"2012","oa_version":"Preprint","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T07:41:18Z","scopus_import":1,"abstract":[{"text":"We introduce consumption games, a model for discrete interactive system with multiple resources that are consumed or reloaded independently. More precisely, a consumption game is a finite-state graph where each transition is labeled by a vector of resource updates, where every update is a non-positive number or ω. The ω updates model the reloading of a given resource. Each vertex belongs either to player □ or player ◇, where the aim of player □ is to play so that the resources are never exhausted. We consider several natural algorithmic problems about consumption games, and show that although these problems are computationally hard in general, they are solvable in polynomial time for every fixed number of resource types (i.e., the dimension of the update vectors) and bounded resource updates. ","lang":"eng"}],"_id":"3135","date_published":"2012-07-01T00:00:00Z","publication_status":"published","oa":1,"main_file_link":[{"url":"http://arxiv.org/abs/1202.0796","open_access":"1"}],"volume":7358,"ec_funded":1,"citation":{"apa":"Brázdil, B., Chatterjee, K., Kučera, A., &#38; Novotný, P. (2012). Efficient controller synthesis for consumption games with multiple resource types (Vol. 7358, pp. 23–38). Presented at the CAV: Computer Aided Verification, Berkeley, CA, USA: Springer. <a href=\"https://doi.org/10.1007/978-3-642-31424-7_8\">https://doi.org/10.1007/978-3-642-31424-7_8</a>","ama":"Brázdil B, Chatterjee K, Kučera A, Novotný P. Efficient controller synthesis for consumption games with multiple resource types. In: Vol 7358. Springer; 2012:23-38. doi:<a href=\"https://doi.org/10.1007/978-3-642-31424-7_8\">10.1007/978-3-642-31424-7_8</a>","short":"B. Brázdil, K. Chatterjee, A. Kučera, P. Novotný, in:, Springer, 2012, pp. 23–38.","mla":"Brázdil, Brázdil, et al. <i>Efficient Controller Synthesis for Consumption Games with Multiple Resource Types</i>. Vol. 7358, Springer, 2012, pp. 23–38, doi:<a href=\"https://doi.org/10.1007/978-3-642-31424-7_8\">10.1007/978-3-642-31424-7_8</a>.","ieee":"B. Brázdil, K. Chatterjee, A. Kučera, and P. Novotný, “Efficient controller synthesis for consumption games with multiple resource types,” presented at the CAV: Computer Aided Verification, Berkeley, CA, USA, 2012, vol. 7358, pp. 23–38.","ista":"Brázdil B, Chatterjee K, Kučera A, Novotný P. 2012. Efficient controller synthesis for consumption games with multiple resource types. CAV: Computer Aided Verification, LNCS, vol. 7358, 23–38.","chicago":"Brázdil, Brázdil, Krishnendu Chatterjee, Antonín Kučera, and Petr Novotný. “Efficient Controller Synthesis for Consumption Games with Multiple Resource Types,” 7358:23–38. Springer, 2012. <a href=\"https://doi.org/10.1007/978-3-642-31424-7_8\">https://doi.org/10.1007/978-3-642-31424-7_8</a>."},"conference":{"end_date":"2012-07-13","start_date":"2012-07-07","name":"CAV: Computer Aided Verification","location":"Berkeley, CA, USA"},"title":"Efficient controller synthesis for consumption games with multiple resource types","day":"01","alternative_title":["LNCS"],"author":[{"first_name":"Brázdil","full_name":"Brázdil, Brázdil","last_name":"Brázdil"},{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Kučera, Antonín","first_name":"Antonín","last_name":"Kučera"},{"id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","last_name":"Novotny","first_name":"Petr","full_name":"Novotny, Petr"}],"type":"conference","acknowledgement":"Tomas Brazdil, Antonin Kucera, and Petr Novotny are supported by the Czech Science Foundation, grant No. P202/10/1469. Krishnendu Chatterjee is supported by the FWF (Austrian Science Fund) NFN Grant No S11407-N23 (RiSE) and ERC Start grant (279307: Graph Games).","project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"language":[{"iso":"eng"}],"doi":"10.1007/978-3-642-31424-7_8","page":"23 - 38","month":"07","date_created":"2018-12-11T12:01:35Z","publisher":"Springer","department":[{"_id":"KrCh"}],"quality_controlled":"1","intvolume":"      7358","status":"public"},{"year":"2012","oa_version":"Submitted Version","publist_id":"3537","date_updated":"2023-09-07T11:40:43Z","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"external_id":{"pmid":["22722843"]},"_id":"3157","abstract":[{"lang":"eng","text":"Colorectal tumours that are wild type for KRAS are often sensitive to EGFR blockade, but almost always develop resistance within several months of initiating therapy. The mechanisms underlying this acquired resistance to anti-EGFR antibodies are largely unknown. This situation is in marked contrast to that of small-molecule targeted agents, such as inhibitors of ABL, EGFR, BRAF and MEK, in which mutations in the genes encoding the protein targets render the tumours resistant to the effects of the drugs. The simplest hypothesis to account for the development of resistance to EGFR blockade is that rare cells with KRAS mutations pre-exist at low levels in tumours with ostensibly wild-type KRAS genes. Although this hypothesis would seem readily testable, there is no evidence in pre-clinical models to support it, nor is there data from patients. To test this hypothesis, we determined whether mutant KRAS DNA could be detected in the circulation of 28 patients receiving monotherapy with panitumumab, a therapeutic anti-EGFR antibody. We found that 9 out of 24 (38%) patients whose tumours were initially KRAS wild type developed detectable mutations in KRAS in their sera, three of which developed multiple different KRAS mutations. The appearance of these mutations was very consistent, generally occurring between 5 and 6months following treatment. Mathematical modelling indicated that the mutations were present in expanded subclones before the initiation of panitumumab treatment. These results suggest that the emergence of KRAS mutations is a mediator of acquired resistance to EGFR blockade and that these mutations can be detected in a non-invasive manner. They explain why solid tumours develop resistance to targeted therapies in a highly reproducible fashion."}],"date_published":"2012-06-28T00:00:00Z","issue":"7404","volume":486,"main_file_link":[{"url":"http://www.ncbi.nlm.nih.gov/pmc/articles/PMC3436069/","open_access":"1"}],"oa":1,"publication_status":"published","type":"journal_article","author":[{"full_name":"Diaz Jr, Luis","first_name":"Luis","last_name":"Diaz Jr"},{"full_name":"Williams, Richard","first_name":"Richard","last_name":"Williams"},{"first_name":"Jian","full_name":"Wu, Jian","last_name":"Wu"},{"first_name":"Isaac","full_name":"Kinde, Isaac","last_name":"Kinde"},{"first_name":"Joel","full_name":"Hecht, Joel","last_name":"Hecht"},{"last_name":"Berlin","first_name":"Jordan","full_name":"Berlin, Jordan"},{"full_name":"Allen, Benjamin","first_name":"Benjamin","last_name":"Allen"},{"first_name":"Ivana","full_name":"Božić, Ivana","last_name":"Božić"},{"full_name":"Reiter, Johannes","first_name":"Johannes","last_name":"Reiter","orcid":"0000-0002-0170-7353","id":"4A918E98-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Martin","full_name":"Nowak, Martin","last_name":"Nowak"},{"first_name":"Kenneth","full_name":"Kinzler, Kenneth","last_name":"Kinzler"},{"full_name":"Oliner, Kelly","first_name":"Kelly","last_name":"Oliner"},{"first_name":"Bert","full_name":"Vogelstein, Bert","last_name":"Vogelstein"}],"day":"28","title":"The molecular evolution of acquired resistance to targeted EGFR blockade in colorectal cancers","ec_funded":1,"citation":{"mla":"Diaz Jr, Luis, et al. “The Molecular Evolution of Acquired Resistance to Targeted EGFR Blockade in Colorectal Cancers.” <i>Nature</i>, vol. 486, no. 7404, Nature Publishing Group, 2012, pp. 537–40, doi:<a href=\"https://doi.org/10.1038/nature11219\">10.1038/nature11219</a>.","chicago":"Diaz Jr, Luis, Richard Williams, Jian Wu, Isaac Kinde, Joel Hecht, Jordan Berlin, Benjamin Allen, et al. “The Molecular Evolution of Acquired Resistance to Targeted EGFR Blockade in Colorectal Cancers.” <i>Nature</i>. Nature Publishing Group, 2012. <a href=\"https://doi.org/10.1038/nature11219\">https://doi.org/10.1038/nature11219</a>.","ista":"Diaz Jr L, Williams R, Wu J, Kinde I, Hecht J, Berlin J, Allen B, Božić I, Reiter J, Nowak M, Kinzler K, Oliner K, Vogelstein B. 2012. The molecular evolution of acquired resistance to targeted EGFR blockade in colorectal cancers. Nature. 486(7404), 537–540.","ieee":"L. Diaz Jr <i>et al.</i>, “The molecular evolution of acquired resistance to targeted EGFR blockade in colorectal cancers,” <i>Nature</i>, vol. 486, no. 7404. Nature Publishing Group, pp. 537–540, 2012.","ama":"Diaz Jr L, Williams R, Wu J, et al. The molecular evolution of acquired resistance to targeted EGFR blockade in colorectal cancers. <i>Nature</i>. 2012;486(7404):537-540. doi:<a href=\"https://doi.org/10.1038/nature11219\">10.1038/nature11219</a>","apa":"Diaz Jr, L., Williams, R., Wu, J., Kinde, I., Hecht, J., Berlin, J., … Vogelstein, B. (2012). The molecular evolution of acquired resistance to targeted EGFR blockade in colorectal cancers. <i>Nature</i>. Nature Publishing Group. <a href=\"https://doi.org/10.1038/nature11219\">https://doi.org/10.1038/nature11219</a>","short":"L. Diaz Jr, R. Williams, J. Wu, I. Kinde, J. Hecht, J. Berlin, B. Allen, I. Božić, J. Reiter, M. Nowak, K. Kinzler, K. Oliner, B. Vogelstein, Nature 486 (2012) 537–540."},"doi":"10.1038/nature11219","language":[{"iso":"eng"}],"related_material":{"record":[{"id":"1400","relation":"dissertation_contains","status":"public"}]},"project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"}],"pmid":1,"date_created":"2018-12-11T12:01:43Z","month":"06","page":"537 - 540","status":"public","intvolume":"       486","quality_controlled":"1","department":[{"_id":"KrCh"}],"publication":"Nature","publisher":"Nature Publishing Group"}]