[{"publication_status":"published","author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"first_name":"Jan","full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop"},{"first_name":"Andreas","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis"}],"day":"08","oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"creator":"system","relation":"main_file","file_size":467895,"access_level":"open_access","content_type":"application/pdf","file_id":"5540","checksum":"855513ebaf6f72228800c5fdb522f93c","file_name":"IST-2013-130-v1+1_Distributed_Synthesis.pdf","date_updated":"2020-07-14T12:46:45Z","date_created":"2018-12-12T11:54:18Z"}],"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."}],"ddc":["005"],"month":"07","publication_identifier":{"issn":["2664-1690"]},"page":"11","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","status":"public","date_published":"2013-07-08T00:00:00Z","type":"technical_report","date_created":"2018-12-12T11:39:09Z","citation":{"apa":"Chatterjee, K., Henzinger, T. A., Otop, J., & Pavlogiannis, A. (2013). Distributed synthesis for LTL Fragments. IST Austria. https://doi.org/10.15479/AT:IST-2013-130-v1-1","short":"K. Chatterjee, T.A. Henzinger, J. Otop, A. Pavlogiannis, Distributed Synthesis for LTL Fragments, IST Austria, 2013.","ieee":"K. Chatterjee, T. A. Henzinger, J. Otop, and A. Pavlogiannis, Distributed synthesis for LTL Fragments. IST Austria, 2013.","ama":"Chatterjee K, Henzinger TA, Otop J, Pavlogiannis A. Distributed Synthesis for LTL Fragments. IST Austria; 2013. doi:10.15479/AT:IST-2013-130-v1-1","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Andreas Pavlogiannis. Distributed Synthesis for LTL Fragments. IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-130-v1-1.","ista":"Chatterjee K, Henzinger TA, Otop J, Pavlogiannis A. 2013. Distributed synthesis for LTL Fragments, IST Austria, 11p.","mla":"Chatterjee, Krishnendu, et al. Distributed Synthesis for LTL Fragments. IST Austria, 2013, doi:10.15479/AT:IST-2013-130-v1-1."},"title":"Distributed synthesis for LTL Fragments","date_updated":"2023-02-21T17:01:26Z","oa":1,"pubrep_id":"130","year":"2013","has_accepted_license":"1","related_material":{"record":[{"id":"1376","relation":"later_version","status":"public"}]},"file_date_updated":"2020-07-14T12:46:45Z","_id":"5406","language":[{"iso":"eng"}],"doi":"10.15479/AT:IST-2013-130-v1-1"},{"doi":"10.15479/AT:IST-2013-141-v1-1","file_date_updated":"2020-07-14T12:46:46Z","language":[{"iso":"eng"}],"_id":"5408","has_accepted_license":"1","related_material":{"record":[{"relation":"later_version","id":"2213","status":"public"}]},"date_updated":"2023-02-23T10:33:11Z","oa":1,"pubrep_id":"141","year":"2013","title":"The complexity of partial-observation stochastic parity games with finite-memory strategies","date_created":"2018-12-12T11:39:10Z","citation":{"apa":"Chatterjee, K., Doyen, L., Nain, S., & Vardi, M. (2013). The complexity of partial-observation stochastic parity games with finite-memory strategies. IST Austria. https://doi.org/10.15479/AT:IST-2013-141-v1-1","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.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, Sumit Nain, and Moshe Vardi. The Complexity of Partial-Observation Stochastic Parity Games with Finite-Memory Strategies. IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-141-v1-1.","mla":"Chatterjee, Krishnendu, et al. The Complexity of Partial-Observation Stochastic Parity Games with Finite-Memory Strategies. IST Austria, 2013, doi:10.15479/AT:IST-2013-141-v1-1.","ama":"Chatterjee K, Doyen L, Nain S, Vardi M. The Complexity of Partial-Observation Stochastic Parity Games with Finite-Memory Strategies. IST Austria; 2013. doi:10.15479/AT:IST-2013-141-v1-1","ieee":"K. Chatterjee, L. Doyen, S. Nain, and M. Vardi, The complexity of partial-observation stochastic parity games with finite-memory strategies. IST Austria, 2013.","short":"K. Chatterjee, L. Doyen, S. Nain, M. Vardi, The Complexity of Partial-Observation Stochastic Parity Games with Finite-Memory Strategies, IST Austria, 2013."},"alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","status":"public","date_published":"2013-09-12T00:00:00Z","type":"technical_report","department":[{"_id":"KrCh"}],"page":"17","ddc":["000","005"],"publication_identifier":{"issn":["2664-1690"]},"month":"09","oa_version":"Published Version","day":"12","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","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"}],"file":[{"creator":"system","relation":"main_file","content_type":"application/pdf","access_level":"open_access","file_size":300481,"file_id":"5477","checksum":"226bc791124f8d3138379778ce834e86","file_name":"IST-2013-141-v1+1_main-tech-rpt.pdf","date_updated":"2020-07-14T12:46:46Z","date_created":"2018-12-12T11:53:16Z"}],"author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"last_name":"Doyen","full_name":"Doyen, Laurent","first_name":"Laurent"},{"first_name":"Sumit","full_name":"Nain, Sumit","last_name":"Nain"},{"last_name":"Vardi","first_name":"Moshe","full_name":"Vardi, Moshe"}],"publication_status":"published"},{"ddc":["000"],"publication_identifier":{"issn":["2664-1690"]},"month":"10","oa_version":"Published Version","day":"30","file":[{"checksum":"0f7633081ba8299c543322f0ad08571f","file_id":"5469","file_name":"IST-2013-144-v1+1_main.pdf","date_updated":"2020-07-14T12:46:46Z","date_created":"2018-12-12T11:53:08Z","creator":"system","content_type":"application/pdf","access_level":"open_access","relation":"main_file","file_size":336377}],"abstract":[{"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.","lang":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"published","author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus"},{"last_name":"Majumdar","full_name":"Majumdar, Rupak","first_name":"Rupak"}],"alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","date_published":"2013-10-30T00:00:00Z","type":"technical_report","status":"public","page":"12","department":[{"_id":"KrCh"}],"has_accepted_license":"1","related_material":{"record":[{"status":"public","id":"2216","relation":"later_version"}]},"oa":1,"pubrep_id":"144","date_updated":"2023-02-23T10:33:18Z","year":"2013","title":"Edit distance for timed automata","citation":{"ista":"Chatterjee K, Ibsen-Jensen R, Majumdar R. 2013. Edit distance for timed automata, IST Austria, 12p.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Rupak Majumdar. Edit Distance for Timed Automata. IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-144-v1-1.","mla":"Chatterjee, Krishnendu, et al. Edit Distance for Timed Automata. IST Austria, 2013, doi:10.15479/AT:IST-2013-144-v1-1.","ama":"Chatterjee K, Ibsen-Jensen R, Majumdar R. Edit Distance for Timed Automata. IST Austria; 2013. doi:10.15479/AT:IST-2013-144-v1-1","ieee":"K. Chatterjee, R. Ibsen-Jensen, and R. Majumdar, Edit distance for timed automata. IST Austria, 2013.","short":"K. Chatterjee, R. Ibsen-Jensen, R. Majumdar, Edit Distance for Timed Automata, IST Austria, 2013.","apa":"Chatterjee, K., Ibsen-Jensen, R., & Majumdar, R. (2013). Edit distance for timed automata. IST Austria. https://doi.org/10.15479/AT:IST-2013-144-v1-1"},"date_created":"2018-12-12T11:39:10Z","doi":"10.15479/AT:IST-2013-144-v1-1","file_date_updated":"2020-07-14T12:46:46Z","_id":"5409","language":[{"iso":"eng"}]},{"has_accepted_license":"1","related_material":{"record":[{"relation":"later_version","id":"1481","status":"public"}]},"year":"2013","pubrep_id":"146","date_updated":"2023-02-23T10:00:50Z","oa":1,"date_created":"2018-12-12T11:39:10Z","title":"Automatic generation of alternative starting positions for traditional board games","citation":{"apa":"Ahmed, U., Chatterjee, K., & Gulwani, S. (2013). Automatic generation of alternative starting positions for traditional board games. IST Austria. https://doi.org/10.15479/AT:IST-2013-146-v1-1","ieee":"U. Ahmed, K. Chatterjee, and S. Gulwani, Automatic generation of alternative starting positions for traditional board games. IST Austria, 2013.","ama":"Ahmed U, Chatterjee K, Gulwani S. Automatic Generation of Alternative Starting Positions for Traditional Board Games. IST Austria; 2013. doi:10.15479/AT:IST-2013-146-v1-1","short":"U. Ahmed, K. Chatterjee, S. Gulwani, Automatic Generation of Alternative Starting Positions for Traditional Board Games, IST Austria, 2013.","ista":"Ahmed U, Chatterjee K, Gulwani S. 2013. Automatic generation of alternative starting positions for traditional board games, IST Austria, 13p.","chicago":"Ahmed, Umair, Krishnendu Chatterjee, and Sumit Gulwani. Automatic Generation of Alternative Starting Positions for Traditional Board Games. IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-146-v1-1.","mla":"Ahmed, Umair, et al. Automatic Generation of Alternative Starting Positions for Traditional Board Games. IST Austria, 2013, doi:10.15479/AT:IST-2013-146-v1-1."},"doi":"10.15479/AT:IST-2013-146-v1-1","_id":"5410","language":[{"iso":"eng"}],"file_date_updated":"2020-07-14T12:46:46Z","month":"12","publication_identifier":{"issn":["2664-1690"]},"ddc":["000","005"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","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"}],"file":[{"content_type":"application/pdf","file_size":818189,"access_level":"open_access","relation":"main_file","creator":"system","date_updated":"2020-07-14T12:46:46Z","date_created":"2018-12-12T11:54:06Z","file_id":"5528","file_name":"IST-2013-146-v1+1_main.pdf","checksum":"409f3aaaf1184e4057b89cbb449dac80"}],"oa_version":"Published Version","day":"03","author":[{"last_name":"Ahmed","full_name":"Ahmed, Umair","first_name":"Umair"},{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Gulwani","full_name":"Gulwani, Sumit","first_name":"Sumit"}],"publication_status":"published","date_published":"2013-12-03T00:00:00Z","type":"technical_report","status":"public","alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","department":[{"_id":"KrCh"}],"page":"13"},{"user_id":"6785fbc1-c503-11eb-8a32-93094b40e1cf","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"}],"oa_version":"Published Version","day":"12","month":"12","author":[{"last_name":"Zagorsky","full_name":"Zagorsky, Benjamin","first_name":"Benjamin"},{"first_name":"Johannes","full_name":"Reiter, Johannes","orcid":"0000-0002-0170-7353","last_name":"Reiter","id":"4A918E98-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"first_name":"Martin","full_name":"Nowak, Martin","last_name":"Nowak"}],"department":[{"_id":"KrCh"}],"type":"research_data_reference","status":"public","date_published":"2013-12-12T00:00:00Z","publisher":"Public Library of Science","related_material":{"record":[{"id":"2247","relation":"used_in_publication","status":"public"}]},"date_created":"2021-07-28T15:45:07Z","title":"Forgiver triumphs in alternating prisoner's dilemma ","citation":{"apa":"Zagorsky, B., Reiter, J., Chatterjee, K., & Nowak, M. (2013). Forgiver triumphs in alternating prisoner’s dilemma . Public Library of Science. https://doi.org/10.1371/journal.pone.0080814.s001","ama":"Zagorsky B, Reiter J, Chatterjee K, Nowak M. Forgiver triumphs in alternating prisoner’s dilemma . 2013. doi:10.1371/journal.pone.0080814.s001","ieee":"B. Zagorsky, J. Reiter, K. Chatterjee, and M. Nowak, “Forgiver triumphs in alternating prisoner’s dilemma .” Public Library of Science, 2013.","short":"B. Zagorsky, J. Reiter, K. Chatterjee, M. Nowak, (2013).","mla":"Zagorsky, Benjamin, et al. Forgiver Triumphs in Alternating Prisoner’s Dilemma . Public Library of Science, 2013, doi:10.1371/journal.pone.0080814.s001.","ista":"Zagorsky B, Reiter J, Chatterjee K, Nowak M. 2013. Forgiver triumphs in alternating prisoner’s dilemma , Public Library of Science, 10.1371/journal.pone.0080814.s001.","chicago":"Zagorsky, Benjamin, Johannes Reiter, Krishnendu Chatterjee, and Martin Nowak. “Forgiver Triumphs in Alternating Prisoner’s Dilemma .” Public Library of Science, 2013. https://doi.org/10.1371/journal.pone.0080814.s001."},"article_processing_charge":"No","year":"2013","date_updated":"2023-02-23T10:34:39Z","doi":"10.1371/journal.pone.0080814.s001","_id":"9749"},{"publication_status":"published","series_title":"Lecture Notes in Computer Science","ddc":["000"],"abstract":[{"lang":"eng","text":"We consider two core algorithmic problems for probabilistic verification: the maximal end-component decomposition and the almost-sure reachability set computation for Markov decision processes (MDPs). For MDPs with treewidth k, we present two improved static algorithms for both the problems that run in time O(n·k 2.38·2k ) and O(m·logn· k), respectively, where n is the number of states and m is the number of edges, significantly improving the previous known O(n·k·√n· k) bound for low treewidth. We also present decremental algorithms for both problems for MDPs with constant treewidth that run in amortized logarithmic time, which is a huge improvement over the previously known algorithms that require amortized linear time."}],"external_id":{"arxiv":["1304.0084"]},"project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"call_identifier":"FWF","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"date_published":"2013-07-01T00:00:00Z","publisher":"Springer","das_tickbox":"1","quality_controlled":"1","volume":8044,"page":"543 - 558","department":[{"_id":"KrCh"}],"year":"2013","publist_id":"4459","date_created":"2018-12-11T11:57:42Z","citation":{"chicago":"Chatterjee, Krishnendu, and Jakub Ła̧Cki. “Faster Algorithms for Markov Decision Processes with Low Treewidth.” Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-39799-8_36.","mla":"Chatterjee, Krishnendu, and Jakub Ła̧Cki. Faster Algorithms for Markov Decision Processes with Low Treewidth. Vol. 8044, Springer, 2013, pp. 543–58, doi:10.1007/978-3-642-39799-8_36.","ista":"Chatterjee K, Ła̧Cki J. 2013. Faster algorithms for Markov decision processes with low treewidth. 8044, 543–558.","ama":"Chatterjee K, Ła̧Cki J. Faster algorithms for Markov decision processes with low treewidth. 2013;8044:543-558. doi:10.1007/978-3-642-39799-8_36","ieee":"K. Chatterjee and J. Ła̧Cki, “Faster algorithms for Markov decision processes with low treewidth,” vol. 8044. Springer, pp. 543–558, 2013.","short":"K. Chatterjee, J. Ła̧Cki, 8044 (2013) 543–558.","apa":"Chatterjee, K., & Ła̧Cki, J. (2013). Faster algorithms for Markov decision processes with low treewidth. Presented at the CAV: Computer Aided Verification, St. Petersburg, Russia: Springer. https://doi.org/10.1007/978-3-642-39799-8_36"},"ec_funded":1,"_id":"2444","doi":"10.1007/978-3-642-39799-8_36","arxiv":1,"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"full_name":"Ła̧Cki, Jakub","first_name":"Jakub","last_name":"Ła̧Cki"}],"month":"07","conference":{"start_date":"2013-07-13","name":"CAV: Computer Aided Verification","end_date":"2013-07-19","location":"St. Petersburg, Russia"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","main_file_link":[{"url":"http://arxiv.org/abs/1304.0084","open_access":"1"}],"day":"01","oa_version":"Preprint","type":"conference","status":"public","alternative_title":["LNCS"],"article_processing_charge":"No","oa":1,"date_updated":"2026-06-18T07:50:03Z","title":"Faster algorithms for Markov decision processes with low treewidth","intvolume":" 8044","scopus_import":"1","language":[{"iso":"eng"}]},{"intvolume":" 7810","scopus_import":"1","title":"How to travel between languages","date_updated":"2023-09-05T15:10:38Z","article_processing_charge":"No","publication":"7th International Conference on Language and Automata Theory and Applications","language":[{"iso":"eng"}],"day":"15","oa_version":"None","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","conference":{"end_date":"2013-04-05","location":"Bilbao, Spain","start_date":"2013-04-02","name":"LATA: Conference on Language and Automata Theory and Applications"},"publication_identifier":{"eissn":["1611-3349"],"eisbn":["9783642370649"],"isbn":["9783642370632"],"issn":["0302-9743"]},"month":"04","author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"last_name":"Chaubal","full_name":"Chaubal, Siddhesh","first_name":"Siddhesh"},{"last_name":"Rubin","id":"2EC51194-F248-11E8-B48F-1D18A9856A87","first_name":"Sasha","full_name":"Rubin, Sasha"}],"alternative_title":["LNCS"],"type":"conference","status":"public","ec_funded":1,"citation":{"apa":"Chatterjee, K., Chaubal, S., & Rubin, S. (2013). How to travel between languages. In 7th International Conference on Language and Automata Theory and Applications (Vol. 7810, pp. 214–225). Berlin, Heidelberg: Springer Nature. https://doi.org/10.1007/978-3-642-37064-9_20","chicago":"Chatterjee, Krishnendu, Siddhesh Chaubal, and Sasha Rubin. “How to Travel between Languages.” In 7th International Conference on Language and Automata Theory and Applications, 7810:214–25. LNCS. Berlin, Heidelberg: Springer Nature, 2013. https://doi.org/10.1007/978-3-642-37064-9_20.","ista":"Chatterjee K, Chaubal S, Rubin S. 2013. How to travel between languages. 7th International Conference on Language and Automata Theory and Applications. LATA: Conference on Language and Automata Theory and ApplicationsLNCS, LNCS, vol. 7810, 214–225.","mla":"Chatterjee, Krishnendu, et al. “How to Travel between Languages.” 7th International Conference on Language and Automata Theory and Applications, vol. 7810, Springer Nature, 2013, pp. 214–25, doi:10.1007/978-3-642-37064-9_20.","short":"K. Chatterjee, S. Chaubal, S. Rubin, in:, 7th International Conference on Language and Automata Theory and Applications, Springer Nature, Berlin, Heidelberg, 2013, pp. 214–225.","ieee":"K. Chatterjee, S. Chaubal, and S. Rubin, “How to travel between languages,” in 7th International Conference on Language and Automata Theory and Applications, Bilbao, Spain, 2013, vol. 7810, pp. 214–225.","ama":"Chatterjee K, Chaubal S, Rubin S. How to travel between languages. In: 7th International Conference on Language and Automata Theory and Applications. Vol 7810. LNCS. Berlin, Heidelberg: Springer Nature; 2013:214-225. doi:10.1007/978-3-642-37064-9_20"},"date_created":"2022-03-21T07:56:21Z","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), and Microsoft faculty fellows award. Thanks to Gabriele Puppis for suggesting the problem of identifying a deterministic transducer to compute the optimal cost, and to Martin Chmelik for his comments on the introduction.","year":"2013","doi":"10.1007/978-3-642-37064-9_20","_id":"10902","abstract":[{"lang":"eng","text":"We consider how to edit strings from a source language so that the edited strings belong to a target language, where the languages are given as deterministic finite automata. Non-streaming (or offline) transducers perform edits given the whole source string. We show that the class of deterministic one-pass transducers with registers along with increment and min operation suffices for computing optimal edit distance, whereas the same class of transducers without the min operation is not sufficient. Streaming (or online) transducers perform edits as the letters of the source string are received. We present a polynomial time algorithm for the partial-repair problem that given a bound α asks for the construction of a deterministic streaming transducer (if one exists) that ensures that the ‘maximum fraction’ η of the strings of the source language are edited, within cost α, to the target language."}],"series_title":"LNCS","publication_status":"published","place":"Berlin, Heidelberg","department":[{"_id":"KrCh"}],"page":"214-225","volume":7810,"quality_controlled":"1","publisher":"Springer Nature","date_published":"2013-04-15T00:00:00Z","project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"call_identifier":"FWF","name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}]},{"abstract":[{"text":"We study the problem of achieving a given value in Markov decision processes (MDPs) with several independent discounted reward objectives. We consider a generalised version of discounted reward objectives, in which the amount of discounting depends on the states visited and on the objective. This definition extends the usual definition of discounted reward, and allows to capture the systems in which the value of different commodities diminish at different and variable rates.\r\n\r\nWe establish results for two prominent subclasses of the problem, namely state-discount models where the discount factors are only dependent on the state of the MDP (and independent of the objective), and reward-discount models where they are only dependent on the objective (but not on the state of the MDP). For the state-discount models we use a straightforward reduction to expected total reward and show that the problem whether a value is achievable can be solved in polynomial time. For the reward-discount model we show that memory and randomisation of the strategies are required, but nevertheless that the problem is decidable and it is sufficient to consider strategies which after a certain number of steps behave in a memoryless way.\r\n\r\nFor the general case, we show that when restricted to graphs (i.e. MDPs with no randomisation), pure strategies and discount factors of the form 1/n where n is an integer, the problem is in PSPACE and finite memory suffices for achieving a given value. We also show that when the discount factors are not of the form 1/n, the memory required by a strategy can be infinite.\r\n","lang":"eng"}],"series_title":"Lecture Notes in Computer Science","publication_status":"published","quality_controlled":"1","volume":8312,"page":"228 - 242","department":[{"_id":"KrCh"}],"date_published":"2013-12-01T00:00:00Z","publisher":"Springer","project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"}],"ec_funded":1,"citation":{"ama":"Chatterjee K, Forejt V, Wojtczak D. Multi-objective discounted reward verification in graphs and MDPs. 2013;8312:228-242. doi:10.1007/978-3-642-45221-5_17","ieee":"K. Chatterjee, V. Forejt, and D. Wojtczak, “Multi-objective discounted reward verification in graphs and MDPs,” vol. 8312. Springer, pp. 228–242, 2013.","short":"K. Chatterjee, V. Forejt, D. Wojtczak, 8312 (2013) 228–242.","mla":"Chatterjee, Krishnendu, et al. Multi-Objective Discounted Reward Verification in Graphs and MDPs. Vol. 8312, Springer, 2013, pp. 228–42, doi:10.1007/978-3-642-45221-5_17.","chicago":"Chatterjee, Krishnendu, Vojtěch Forejt, and Dominik Wojtczak. “Multi-Objective Discounted Reward Verification in Graphs and MDPs.” Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-45221-5_17.","ista":"Chatterjee K, Forejt V, Wojtczak D. 2013. Multi-objective discounted reward verification in graphs and MDPs. 8312, 228–242.","apa":"Chatterjee, K., Forejt, V., & Wojtczak, D. (2013). Multi-objective discounted reward verification in graphs and MDPs. Presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Stellenbosch, South Africa: Springer. https://doi.org/10.1007/978-3-642-45221-5_17"},"publist_id":"4723","date_created":"2018-12-11T11:56:30Z","year":"2013","doi":"10.1007/978-3-642-45221-5_17","_id":"2238","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"01","oa_version":"None","month":"12","conference":{"location":"Stellenbosch, South Africa","end_date":"2013-12-19","name":"LPAR: Logic for Programming, Artificial Intelligence, and Reasoning","start_date":"2013-12-14"},"author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Forejt","first_name":"Vojtěch","full_name":"Forejt, Vojtěch"},{"full_name":"Wojtczak, Dominik","first_name":"Dominik","last_name":"Wojtczak"}],"status":"public","type":"conference","alternative_title":["LNCS"],"scopus_import":1,"intvolume":" 8312","title":"Multi-objective discounted reward verification in graphs and MDPs","date_updated":"2020-08-11T10:09:42Z","language":[{"iso":"eng"}]},{"project":[{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"publisher":"Public Library of Science","date_published":"2013-12-12T00:00:00Z","department":[{"_id":"KrCh"}],"volume":8,"quality_controlled":"1","publication_status":"published","ddc":["000"],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"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"}],"file_date_updated":"2020-07-14T12:45:34Z","_id":"2247","doi":"10.1371/journal.pone.0080814","year":"2013","citation":{"apa":"Zagorsky, B., Reiter, J., Chatterjee, K., & Nowak, M. (2013). Forgiver triumphs in alternating prisoner’s dilemma . PLoS One. Public Library of Science. https://doi.org/10.1371/journal.pone.0080814","mla":"Zagorsky, Benjamin, et al. “Forgiver Triumphs in Alternating Prisoner’s Dilemma .” PLoS One, vol. 8, no. 12, e80814, Public Library of Science, 2013, doi:10.1371/journal.pone.0080814.","ista":"Zagorsky B, Reiter J, Chatterjee K, Nowak M. 2013. Forgiver triumphs in alternating prisoner’s dilemma . PLoS One. 8(12), e80814.","chicago":"Zagorsky, Benjamin, Johannes Reiter, Krishnendu Chatterjee, and Martin Nowak. “Forgiver Triumphs in Alternating Prisoner’s Dilemma .” PLoS One. Public Library of Science, 2013. https://doi.org/10.1371/journal.pone.0080814.","short":"B. Zagorsky, J. Reiter, K. Chatterjee, M. Nowak, PLoS One 8 (2013).","ama":"Zagorsky B, Reiter J, Chatterjee K, Nowak M. Forgiver triumphs in alternating prisoner’s dilemma . PLoS One. 2013;8(12). doi:10.1371/journal.pone.0080814","ieee":"B. Zagorsky, J. Reiter, K. Chatterjee, and M. Nowak, “Forgiver triumphs in alternating prisoner’s dilemma ,” PLoS One, vol. 8, no. 12. Public Library of Science, 2013."},"publist_id":"4702","date_created":"2018-12-11T11:56:33Z","ec_funded":1,"article_number":"e80814","related_material":{"record":[{"id":"9749","relation":"research_data","status":"public"},{"relation":"dissertation_contains","id":"1400","status":"public"}]},"status":"public","type":"journal_article","author":[{"full_name":"Zagorsky, Benjamin","first_name":"Benjamin","last_name":"Zagorsky"},{"id":"4A918E98-F248-11E8-B48F-1D18A9856A87","last_name":"Reiter","orcid":"0000-0002-0170-7353","first_name":"Johannes","full_name":"Reiter, Johannes"},{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"first_name":"Martin","full_name":"Nowak, Martin","last_name":"Nowak"}],"month":"12","day":"12","oa_version":"Published Version","file":[{"checksum":"808e8b9e6e89658bee4ffbbfac1bd19d","file_name":"IST-2016-409-v1+1_journal.pone.0080814.pdf","file_id":"4868","date_updated":"2020-07-14T12:45:34Z","date_created":"2018-12-12T10:11:15Z","creator":"system","relation":"main_file","file_size":1050042,"content_type":"application/pdf","access_level":"open_access"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"publication":"PLoS One","date_updated":"2023-09-07T11:40:43Z","oa":1,"pubrep_id":"409","issue":"12","title":"Forgiver triumphs in alternating prisoner's dilemma ","scopus_import":1,"has_accepted_license":"1","intvolume":" 8"},{"oa":1,"date_updated":"2023-02-23T12:22:51Z","title":"Looking at mean-payoff and total-payoff through windows","intvolume":" 8172","scopus_import":1,"language":[{"iso":"eng"}],"author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"full_name":"Doyen, Laurent","first_name":"Laurent","last_name":"Doyen"},{"first_name":"Mickael","full_name":"Randour, Mickael","last_name":"Randour"},{"last_name":"Raskin","full_name":"Raskin, Jean","first_name":"Jean"}],"month":"01","conference":{"location":"Hanoi, Vietnam","end_date":"2013-10-18","name":"ATVA: Automated Technology for Verification and Analysis","start_date":"2013-10-15"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Preprint","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1302.4248"}],"day":"01","status":"public","type":"conference","alternative_title":["LNCS"],"year":"2013","acknowledgement":"279307; ERC; Fonds National de la Reserche Luxembourg; 279499; ERC; Fonds National de la Reserche Luxembourg","publist_id":"4656","date_created":"2018-12-11T11:56:44Z","citation":{"ama":"Chatterjee K, Doyen L, Randour M, Raskin J. Looking at mean-payoff and total-payoff through windows. 2013;8172:118-132. doi:10.1007/978-3-319-02444-8_10","ieee":"K. Chatterjee, L. Doyen, M. Randour, and J. Raskin, “Looking at mean-payoff and total-payoff through windows,” vol. 8172. Springer, pp. 118–132, 2013.","short":"K. Chatterjee, L. Doyen, M. Randour, J. Raskin, 8172 (2013) 118–132.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, Mickael Randour, and Jean Raskin. “Looking at Mean-Payoff and Total-Payoff through Windows.” Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-319-02444-8_10.","ista":"Chatterjee K, Doyen L, Randour M, Raskin J. 2013. Looking at mean-payoff and total-payoff through windows. 8172, 118–132.","mla":"Chatterjee, Krishnendu, et al. Looking at Mean-Payoff and Total-Payoff through Windows. Vol. 8172, Springer, 2013, pp. 118–32, doi:10.1007/978-3-319-02444-8_10.","apa":"Chatterjee, K., Doyen, L., Randour, M., & Raskin, J. (2013). Looking at mean-payoff and total-payoff through windows. Presented at the ATVA: Automated Technology for Verification and Analysis, Hanoi, Vietnam: Springer. https://doi.org/10.1007/978-3-319-02444-8_10"},"related_material":{"record":[{"id":"523","relation":"later_version","status":"public"}]},"ec_funded":1,"_id":"2279","doi":"10.1007/978-3-319-02444-8_10","publication_status":"published","series_title":"Lecture Notes in Computer Science","abstract":[{"lang":"eng","text":"We consider two-player games played on weighted directed graphs with mean-payoff and total-payoff objectives, two classical quantitative objectives. While for single-dimensional games the complexity and memory bounds for both objectives coincide, we show that in contrast to multi-dimensional mean-payoff games that are known to be coNP-complete, multi-dimensional total-payoff games are undecidable. We introduce conservative approximations of these objectives, where the payoff is considered over a local finite window sliding along a play, instead of the whole play. For single dimension, we show that (i) if the window size is polynomial, deciding the winner takes polynomial time, and (ii) the existence of a bounded window can be decided in NP ∩ coNP, and is at least as hard as solving mean-payoff games. For multiple dimensions, we show that (i) the problem with fixed window size is EXPTIME-complete, and (ii) there is no primitive-recursive algorithm to decide the existence of a bounded window."}],"project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"}],"date_published":"2013-01-01T00:00:00Z","publisher":"Springer","volume":8172,"quality_controlled":"1","page":"118 - 132","department":[{"_id":"KrCh"}]},{"publication_status":"published","publication_identifier":{"isbn":["978-3-642-40312-5"]},"month":"08","series_title":"Lecture Notes in Computer Science","conference":{"name":"MFCS: Mathematical Foundations of Computer Science","start_date":"2013-08-26","location":"Klosterneuburg, Austria","end_date":"2013-08-30"},"abstract":[{"lang":"eng","text":"This book constitutes the thoroughly refereed conference proceedings of the 38th International Symposium on Mathematical Foundations of Computer Science, MFCS 2013, held in Klosterneuburg, Austria, in August 2013. The 67 revised full papers presented together with six invited talks were carefully selected from 191 submissions. Topics covered include algorithmic game theory, algorithmic learning theory, algorithms and data structures, automata, formal languages, bioinformatics, complexity, computational geometry, computer-assisted reasoning, concurrency theory, databases and knowledge-based systems, foundations of computing, logic in computer science, models of computation, semantics and verification of programs, and theoretical issues in artificial intelligence."}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"None","day":"08","date_published":"2013-08-08T00:00:00Z","type":"conference_editor","status":"public","alternative_title":["LNCS"],"publisher":"Springer","volume":8087,"quality_controlled":"1","page":"VI - 854","department":[{"_id":"KrCh"}],"year":"2013","date_updated":"2020-08-11T10:09:45Z","citation":{"ama":"Chatterjee K, Sgall J, eds. Mathematical Foundations of Computer Science 2013. Vol 8087. Springer; 2013:VI-854. doi:10.1007/978-3-642-40313-2","ieee":"K. Chatterjee and J. Sgall, Eds., Mathematical Foundations of Computer Science 2013, vol. 8087. Springer, 2013, p. VI-854.","short":"K. Chatterjee, J. Sgall, eds., Mathematical Foundations of Computer Science 2013, Springer, 2013.","chicago":"Chatterjee, Krishnendu, and Jiri Sgall, eds. Mathematical Foundations of Computer Science 2013. Vol. 8087. Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-40313-2.","mla":"Chatterjee, Krishnendu, and Jiri Sgall, editors. Mathematical Foundations of Computer Science 2013. Vol. 8087, Springer, 2013, p. VI-854, doi:10.1007/978-3-642-40313-2.","ista":"Chatterjee K, Sgall J eds. 2013. Mathematical Foundations of Computer Science 2013, Springer,p.","apa":"Chatterjee, K., & Sgall, J. (Eds.). (2013). Mathematical Foundations of Computer Science 2013 (Vol. 8087, p. VI-854). Presented at the MFCS: Mathematical Foundations of Computer Science, Klosterneuburg, Austria: Springer. https://doi.org/10.1007/978-3-642-40313-2"},"date_created":"2018-12-11T11:56:48Z","publist_id":"4636","title":"Mathematical Foundations of Computer Science 2013","editor":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"last_name":"Sgall","full_name":"Sgall, Jiri","first_name":"Jiri"}],"scopus_import":1,"intvolume":" 8087","_id":"2292","language":[{"iso":"eng"}],"doi":"10.1007/978-3-642-40313-2"},{"month":"08","conference":{"location":"Torino, Italy","end_date":"2013-09-05","name":"CSL: Computer Science Logic","start_date":"2013-09-02"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"creator":"system","access_level":"open_access","relation":"main_file","file_size":345171,"content_type":"application/pdf","file_id":"4766","checksum":"ba2828322955574d9283bea0e17a37a6","file_name":"IST-2017-756-v1+1_2.pdf","date_updated":"2020-07-14T12:45:37Z","date_created":"2018-12-12T10:09:42Z"}],"oa_version":"Published Version","day":"27","author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik","full_name":"Chmelik, Martin","first_name":"Martin"},{"first_name":"Mathieu","full_name":"Tracol, Mathieu","last_name":"Tracol","id":"3F54FA38-F248-11E8-B48F-1D18A9856A87"}],"type":"conference","status":"public","alternative_title":["LIPIcs"],"scopus_import":1,"has_accepted_license":"1","intvolume":" 23","pubrep_id":"756","oa":1,"date_updated":"2023-02-23T12:24:38Z","title":"What is decidable about partially observable Markov decision processes with omega-regular objectives","language":[{"iso":"eng"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"ddc":["000"],"series_title":"Leibniz International Proceedings in Informatics","abstract":[{"text":"We consider partially observable Markov decision processes (POMDPs) with ω-regular conditions specified as parity objectives. The qualitative analysis problem given a POMDP 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, we establish decidability (with optimal EXPTIME-complete complexity) of the qualitative analysis problems for POMDPs with all parity objectives under finite-memory strategies. We also establish asymptotically optimal (exponential) memory bounds.","lang":"eng"}],"publication_status":"published","date_published":"2013-08-27T00:00:00Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","quality_controlled":"1","volume":23,"department":[{"_id":"KrCh"}],"page":"165 - 180","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"call_identifier":"FWF","name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"related_material":{"record":[{"status":"public","relation":"later_version","id":"1477"},{"id":"5400","relation":"earlier_version","status":"public"}]},"ec_funded":1,"year":"2013","publist_id":"4633","date_created":"2018-12-11T11:56:50Z","citation":{"short":"K. Chatterjee, M. Chmelik, M. Tracol, 23 (2013) 165–180.","ama":"Chatterjee K, Chmelik M, Tracol M. What is decidable about partially observable Markov decision processes with omega-regular objectives. 2013;23:165-180. doi:10.4230/LIPIcs.CSL.2013.165","ieee":"K. Chatterjee, M. Chmelik, and M. Tracol, “What is decidable about partially observable Markov decision processes with omega-regular objectives,” vol. 23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 165–180, 2013.","mla":"Chatterjee, Krishnendu, et al. What Is Decidable about Partially Observable Markov Decision Processes with Omega-Regular Objectives. Vol. 23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013, pp. 165–80, doi:10.4230/LIPIcs.CSL.2013.165.","ista":"Chatterjee K, Chmelik M, Tracol M. 2013. What is decidable about partially observable Markov decision processes with omega-regular objectives. 23, 165–180.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Mathieu Tracol. “What Is Decidable about Partially Observable Markov Decision Processes with Omega-Regular Objectives.” Leibniz International Proceedings in Informatics. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013. https://doi.org/10.4230/LIPIcs.CSL.2013.165.","apa":"Chatterjee, K., Chmelik, M., & Tracol, M. (2013). What is decidable about partially observable Markov decision processes with omega-regular objectives. Presented at the CSL: Computer Science Logic, Torino, Italy: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CSL.2013.165"},"doi":"10.4230/LIPIcs.CSL.2013.165","_id":"2295","file_date_updated":"2020-07-14T12:45:37Z"},{"publication_status":"published","ddc":["000"],"abstract":[{"lang":"eng","text":"The standard hardware design flow involves: (a) design of an integrated circuit using a hardware description language, (b) extensive functional and formal verification, and (c) logical synthesis. However, the above-mentioned processes consume significant effort and time. An alternative approach is to use a formal specification language as a high-level hardware description language and synthesize hardware from formal specifications. Our work is a case study of the synthesis of the widely and industrially used AMBA AHB protocol from formal specifications. Bloem et al. presented the first formal specifications for the AMBA AHB Arbiter and synthesized the AHB Arbiter circuit. However, in the first formal specification some important assumptions were missing. Our contributions are as follows: (a) We present detailed formal specifications for the AHB Arbiter incorporating the missing details, and obtain significant improvements in the synthesis results (both with respect to the number of gates in the synthesized circuit and with respect to the time taken to synthesize the circuit), and (b) we present formal specifications to generate compact circuits for the remaining two main components of AMBA AHB, namely, AHB Master and AHB Slave. Thus with systematic description we are able to automatically and completely synthesize an important and widely used industrial protocol."}],"project":[{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"date_published":"2013-10-01T00:00:00Z","publisher":"Springer","volume":15,"quality_controlled":"1","page":"585 - 601","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"year":"2013","citation":{"apa":"Godhal, Y., Chatterjee, K., & Henzinger, T. A. (2013). Synthesis of AMBA AHB from formal specification: A case study. International Journal on Software Tools for Technology Transfer. Springer. https://doi.org/10.1007/s10009-011-0207-9","ista":"Godhal Y, Chatterjee K, Henzinger TA. 2013. Synthesis of AMBA AHB from formal specification: A case study. International Journal on Software Tools for Technology Transfer. 15(5–6), 585–601.","chicago":"Godhal, Yashdeep, Krishnendu Chatterjee, and Thomas A Henzinger. “Synthesis of AMBA AHB from Formal Specification: A Case Study.” International Journal on Software Tools for Technology Transfer. Springer, 2013. https://doi.org/10.1007/s10009-011-0207-9.","mla":"Godhal, Yashdeep, et al. “Synthesis of AMBA AHB from Formal Specification: A Case Study.” International Journal on Software Tools for Technology Transfer, vol. 15, no. 5–6, Springer, 2013, pp. 585–601, doi:10.1007/s10009-011-0207-9.","ama":"Godhal Y, Chatterjee K, Henzinger TA. Synthesis of AMBA AHB from formal specification: A case study. International Journal on Software Tools for Technology Transfer. 2013;15(5-6):585-601. doi:10.1007/s10009-011-0207-9","ieee":"Y. Godhal, K. Chatterjee, and T. A. Henzinger, “Synthesis of AMBA AHB from formal specification: A case study,” International Journal on Software Tools for Technology Transfer, vol. 15, no. 5–6. Springer, pp. 585–601, 2013.","short":"Y. Godhal, K. Chatterjee, T.A. Henzinger, International Journal on Software Tools for Technology Transfer 15 (2013) 585–601."},"date_created":"2018-12-11T11:56:51Z","publist_id":"4629","_id":"2299","file_date_updated":"2020-07-14T12:45:37Z","doi":"10.1007/s10009-011-0207-9","author":[{"id":"5B547124-EB61-11E9-8887-89D9C04DBDF5","last_name":"Godhal","first_name":"Yashdeep","full_name":"Godhal, Yashdeep"},{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"month":"10","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"creator":"system","access_level":"open_access","content_type":"application/pdf","relation":"main_file","file_size":277372,"file_id":"4910","file_name":"IST-2012-87-v1+1_Synthesis_of_AMBA_AHB_from_formal_specifications-_A_case_study.pdf","checksum":"57b06a732dd8d6349190dba6b5b0d33b","date_created":"2018-12-12T10:11:53Z","date_updated":"2020-07-14T12:45:37Z"}],"day":"01","oa_version":"Submitted Version","type":"journal_article","status":"public","issue":"5-6","date_updated":"2021-01-12T06:56:37Z","pubrep_id":"87","oa":1,"title":"Synthesis of AMBA AHB from formal specification: A case study","has_accepted_license":"1","scopus_import":1,"intvolume":" 15","language":[{"iso":"eng"}],"publication":"International Journal on Software Tools for Technology Transfer"},{"doi":"10.1109/LICS.2013.39","_id":"2305","related_material":{"record":[{"relation":"later_version","id":"1294","status":"public"}]},"ec_funded":1,"year":"2013","date_created":"2018-12-11T11:56:53Z","publist_id":"4622","citation":{"apa":"Brázdil, T., Chatterjee, K., Forejt, V., & Kučera, A. (2013). Trading performance for stability in Markov decision processes. In 28th Annual ACM/IEEE Symposium (pp. 331–340). New Orleans, LA, United States: IEEE. https://doi.org/10.1109/LICS.2013.39","ieee":"T. Brázdil, K. Chatterjee, V. Forejt, and A. Kučera, “Trading performance for stability in Markov decision processes,” in 28th Annual ACM/IEEE Symposium, New Orleans, LA, United States, 2013, pp. 331–340.","ama":"Brázdil T, Chatterjee K, Forejt V, Kučera A. Trading performance for stability in Markov decision processes. In: 28th Annual ACM/IEEE Symposium. IEEE; 2013:331-340. doi:10.1109/LICS.2013.39","short":"T. Brázdil, K. Chatterjee, V. Forejt, A. Kučera, in:, 28th Annual ACM/IEEE Symposium, IEEE, 2013, pp. 331–340.","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Vojtěch Forejt, and Antonín Kučera. “Trading Performance for Stability in Markov Decision Processes.” In 28th Annual ACM/IEEE Symposium, 331–40. IEEE, 2013. https://doi.org/10.1109/LICS.2013.39.","mla":"Brázdil, Tomáš, et al. “Trading Performance for Stability in Markov Decision Processes.” 28th Annual ACM/IEEE Symposium, IEEE, 2013, pp. 331–40, doi:10.1109/LICS.2013.39.","ista":"Brázdil T, Chatterjee K, Forejt V, Kučera A. 2013. Trading performance for stability in Markov decision processes. 28th Annual ACM/IEEE Symposium. LICS: Logic in Computer Science, 331–340."},"date_published":"2013-08-01T00:00:00Z","publisher":"IEEE","quality_controlled":"1","page":"331 - 340","department":[{"_id":"KrCh"}],"project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"abstract":[{"text":"We study the complexity of central controller synthesis problems for finite-state Markov decision processes, where the objective is to optimize both the expected mean-payoff performance of the system and its stability. e argue that the basic theoretical notion of expressing the stability in terms of the variance of the mean-payoff (called global variance in our paper) is not always sufficient, since it ignores possible instabilities on respective runs. For this reason we propose alernative definitions of stability, which we call local and hybrid variance, and which express how rewards on each run deviate from the run's own mean-payoff and from the expected mean-payoff, respectively. We show that a strategy ensuring both the expected mean-payoff and the variance below given bounds requires randomization and memory, under all the above semantics of variance. We then look at the problem of determining whether there is a such a strategy. For the global variance, we show that the problem is in PSPACE, and that the answer can be approximated in pseudo-polynomial time. For the hybrid variance, the analogous decision problem is in NP, and a polynomial-time approximating algorithm also exists. For local variance, we show that the decision problem is in NP. Since the overall performance can be traded for stability (and vice versa), we also present algorithms for approximating the associated Pareto curve in all the three cases. Finally, we study a special case of the decision problems, where we require a given expected mean-payoff together with zero variance. Here we show that the problems can be all solved in polynomial time.","lang":"eng"}],"external_id":{"arxiv":["1305.4103"]},"publication_status":"published","publication":"28th Annual ACM/IEEE Symposium","language":[{"iso":"eng"}],"scopus_import":1,"oa":1,"date_updated":"2023-09-20T11:15:30Z","title":"Trading performance for stability in Markov decision processes","type":"conference","status":"public","month":"08","conference":{"start_date":"2013-06-25","name":"LICS: Logic in Computer Science","end_date":"2013-06-28","location":"New Orleans, LA, United States"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"01","main_file_link":[{"url":"http://arxiv.org/abs/1305.4103","open_access":"1"}],"oa_version":"Preprint","arxiv":1,"author":[{"first_name":"Tomáš","full_name":"Brázdil, Tomáš","last_name":"Brázdil"},{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"full_name":"Forejt, Vojtěch","first_name":"Vojtěch","last_name":"Forejt"},{"last_name":"Kučera","first_name":"Antonín","full_name":"Kučera, Antonín"}]},{"main_file_link":[{"url":"http://arxiv.org/abs/1210.3141","open_access":"1"}],"day":"01","oa_version":"Preprint","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"start_date":"2013-08-27","name":"CONCUR: Concurrency Theory","end_date":"2013-08-30","location":"Buenos Aires, Argentinia"},"month":"08","author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"full_name":"Velner, Yaron","first_name":"Yaron","last_name":"Velner"}],"arxiv":1,"alternative_title":["LNCS"],"type":"conference","status":"public","scopus_import":1,"intvolume":" 8052","title":"Hyperplane separation technique for multidimensional mean-payoff games","oa":1,"date_updated":"2023-02-23T13:00:42Z","language":[{"iso":"eng"}],"external_id":{"arxiv":["1210.3141"]},"abstract":[{"lang":"eng","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 both finite-state game graphs, and recursive game graphs (or pushdown game graphs) that model the control flow of sequential programs with recursion. The objectives we study are multidimensional mean-payoff objectives, where the goal of player 1 is to ensure that the mean-payoff is non-negative in all dimensions. 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. Our main contributions are as follows: (1) We show that finite-state multidimensional mean-payoff games can be solved in polynomial time if the number of dimensions and the maximal absolute value of the weights are fixed; whereas if the number of dimensions is arbitrary, then the problem is known to be coNP-complete. (2) We show that pushdown graphs with multidimensional mean-payoff objectives can be solved in polynomial time. For both (1) and (2) our algorithms are based on hyperplane separation technique. (3) For pushdown games under global strategies both one and multidimensional mean-payoff objectives problems are known to be undecidable, and we show that under modular strategies the multidimensional problem is also undecidable; under modular strategies the one-dimensional problem is NP-complete. We show that if the number of modules, the number of exits, and the maximal absolute value of the weights are fixed, then pushdown games under modular strategies with one-dimensional mean-payoff objectives can be solved in polynomial time, and if either the number of exits or the number of modules is unbounded, then the problem is NP-hard. (4) Finally we show that a fixed parameter tractable algorithm for finite-state multidimensional mean-payoff games or pushdown games under modular strategies with one-dimensional mean-payoff objectives would imply the fixed parameter tractability of parity games."}],"series_title":"Lecture Notes in Computer Science","publication_status":"published","page":"500 - 515","department":[{"_id":"KrCh"}],"quality_controlled":"1","volume":8052,"publisher":"Springer","date_published":"2013-08-01T00:00:00Z","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory","call_identifier":"FWF"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"ec_funded":1,"related_material":{"record":[{"status":"public","relation":"later_version","id":"717"}]},"citation":{"apa":"Chatterjee, K., & Velner, Y. (2013). Hyperplane separation technique for multidimensional mean-payoff games. Presented at the CONCUR: Concurrency Theory, Buenos Aires, Argentinia: Springer. https://doi.org/10.1007/978-3-642-40184-8_35","ieee":"K. Chatterjee and Y. Velner, “Hyperplane separation technique for multidimensional mean-payoff games,” vol. 8052. Springer, pp. 500–515, 2013.","ama":"Chatterjee K, Velner Y. Hyperplane separation technique for multidimensional mean-payoff games. 2013;8052:500-515. doi:10.1007/978-3-642-40184-8_35","short":"K. Chatterjee, Y. Velner, 8052 (2013) 500–515.","chicago":"Chatterjee, Krishnendu, and Yaron Velner. “Hyperplane Separation Technique for Multidimensional Mean-Payoff Games.” Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-40184-8_35.","mla":"Chatterjee, Krishnendu, and Yaron Velner. Hyperplane Separation Technique for Multidimensional Mean-Payoff Games. Vol. 8052, Springer, 2013, pp. 500–15, doi:10.1007/978-3-642-40184-8_35.","ista":"Chatterjee K, Velner Y. 2013. Hyperplane separation technique for multidimensional mean-payoff games. 8052, 500–515."},"publist_id":"4597","date_created":"2018-12-11T11:57:01Z","year":"2013","doi":"10.1007/978-3-642-40184-8_35","_id":"2329"},{"doi":"10.1007/978-3-642-39799-8_37","_id":"2446","ec_funded":1,"date_created":"2018-12-11T11:57:42Z","citation":{"short":"K. Chatterjee, A. Gaiser, J. Kretinsky, 8044 (2013) 559–575.","ama":"Chatterjee K, Gaiser A, Kretinsky J. Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. 2013;8044:559-575. doi:10.1007/978-3-642-39799-8_37","ieee":"K. Chatterjee, A. Gaiser, and J. Kretinsky, “Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis,” vol. 8044. Springer, pp. 559–575, 2013.","ista":"Chatterjee K, Gaiser A, Kretinsky J. 2013. Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. 8044, 559–575.","mla":"Chatterjee, Krishnendu, et al. Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis. Vol. 8044, Springer, 2013, pp. 559–75, doi:10.1007/978-3-642-39799-8_37.","chicago":"Chatterjee, Krishnendu, Andreas Gaiser, and Jan Kretinsky. “Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis.” Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-39799-8_37.","apa":"Chatterjee, K., Gaiser, A., & Kretinsky, J. (2013). Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. Presented at the CAV: Computer Aided Verification, St. Petersburg, Russia: Springer. https://doi.org/10.1007/978-3-642-39799-8_37"},"publist_id":"4457","year":"2013","page":"559 - 575","department":[{"_id":"KrCh"}],"quality_controlled":"1","volume":8044,"publisher":"Springer","date_published":"2013-07-01T00:00:00Z","project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"external_id":{"arxiv":["1304.5281"]},"abstract":[{"text":"The model-checking problem for probabilistic systems crucially relies on the translation of LTL to deterministic Rabin automata (DRW). Our recent Safraless translation [KE12, GKE12] for the LTL(F,G) fragment produces smaller automata as compared to the traditional approach. In this work, instead of DRW we consider deterministic automata with acceptance condition given as disjunction of generalized Rabin pairs (DGRW). The Safraless translation of LTL(F,G) formulas to DGRW results in smaller automata as compared to DRW. We present algorithms for probabilistic model-checking as well as game solving for DGRW conditions. Our new algorithms lead to improvement both in terms of theoretical bounds as well as practical evaluation. We compare PRISM with and without our new translation, and show that the new translation leads to significant improvements.","lang":"eng"}],"series_title":"Lecture Notes in Computer Science","publication_status":"published","language":[{"iso":"eng"}],"scopus_import":1,"intvolume":" 8044","title":"Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis","date_updated":"2020-08-11T10:09:47Z","oa":1,"alternative_title":["LNCS"],"status":"public","type":"conference","day":"01","oa_version":"Preprint","main_file_link":[{"url":"http://arxiv.org/abs/1304.5281","open_access":"1"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"name":"CAV: Computer Aided Verification","start_date":"2013-07-13","location":"St. Petersburg, Russia","end_date":"2013-07-19"},"month":"07","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"first_name":"Andreas","full_name":"Gaiser, Andreas","last_name":"Gaiser"},{"full_name":"Kretinsky, Jan","first_name":"Jan","last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881"}],"arxiv":1},{"month":"02","main_file_link":[{"url":"https://arxiv.org/abs/0804.4525","open_access":"1"}],"day":"01","oa_version":"Preprint","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Alfaro, Luca","first_name":"Luca","last_name":"Alfaro"},{"last_name":"Majumdar","full_name":"Majumdar, Ritankar","first_name":"Ritankar"}],"arxiv":1,"status":"public","type":"journal_article","intvolume":" 24","scopus_import":1,"date_updated":"2021-01-12T06:59:54Z","oa":1,"issue":"2","title":"The complexity of coverage","publication":"International Journal of Foundations of Computer Science","language":[{"iso":"eng"}],"external_id":{"arxiv":["0804.4525"]},"abstract":[{"text":"We study the problem of generating a test sequence that achieves maximal coverage for a reactive system under test. We formulate the problem as a repeated game between the tester and the system, where the system state space is partitioned according to some coverage criterion and the objective of the tester is to maximize the set of partitions (or coverage goals) visited during the game. We show the complexity of the maximal coverage problem for non-deterministic systems is PSPACE-complete, but is NP-complete for deterministic systems. For the special case of non-deterministic systems with a re-initializing "reset" action, which represent running a new test input on a re-initialized system, we show that the complexity is coNP-complete. Our proof technique for reset games uses randomized testing strategies that circumvent the exponentially large memory requirement of deterministic testing strategies. We also discuss the memory requirement for deterministic strategies and extensions of our results to other models, such as pushdown systems and timed systems.","lang":"eng"}],"publication_status":"published","publisher":"World Scientific Publishing","date_published":"2013-02-01T00:00:00Z","department":[{"_id":"KrCh"}],"page":"165 - 185","quality_controlled":"1","volume":24,"project":[{"call_identifier":"FWF","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"ec_funded":1,"year":"2013","citation":{"short":"K. Chatterjee, L. Alfaro, R. Majumdar, International Journal of Foundations of Computer Science 24 (2013) 165–185.","ama":"Chatterjee K, Alfaro L, Majumdar R. The complexity of coverage. International Journal of Foundations of Computer Science. 2013;24(2):165-185. doi:10.1142/S0129054113400066","ieee":"K. Chatterjee, L. Alfaro, and R. Majumdar, “The complexity of coverage,” International Journal of Foundations of Computer Science, vol. 24, no. 2. World Scientific Publishing, pp. 165–185, 2013.","chicago":"Chatterjee, Krishnendu, Luca Alfaro, and Ritankar Majumdar. “The Complexity of Coverage.” International Journal of Foundations of Computer Science. World Scientific Publishing, 2013. https://doi.org/10.1142/S0129054113400066.","mla":"Chatterjee, Krishnendu, et al. “The Complexity of Coverage.” International Journal of Foundations of Computer Science, vol. 24, no. 2, World Scientific Publishing, 2013, pp. 165–85, doi:10.1142/S0129054113400066.","ista":"Chatterjee K, Alfaro L, Majumdar R. 2013. The complexity of coverage. International Journal of Foundations of Computer Science. 24(2), 165–185.","apa":"Chatterjee, K., Alfaro, L., & Majumdar, R. (2013). The complexity of coverage. International Journal of Foundations of Computer Science. World Scientific Publishing. https://doi.org/10.1142/S0129054113400066"},"date_created":"2018-12-11T11:59:44Z","publist_id":"4070","doi":"10.1142/S0129054113400066","_id":"2814"},{"ddc":["570","610"],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"abstract":[{"text":"In solid tumors, targeted treatments can lead to dramatic regressions, but responses are often short-lived because resistant cancer cells arise. The major strategy proposed for overcoming resistance is combination therapy. We present a mathematical model describing the evolutionary dynamics of lesions in response to treatment. We first studied 20 melanoma patients receiving vemurafenib. We then applied our model to an independent set of pancreatic, colorectal, and melanoma cancer patients with metastatic disease. We find that dual therapy results in long-term disease control for most patients, if there are no single mutations that cause cross-resistance to both drugs; in patients with large disease burden, triple therapy is needed. We also find that simultaneous therapy with two drugs is much more effective than sequential therapy. Our results provide realistic expectations for the efficacy of new drug combinations and inform the design of trials for new cancer therapeutics.","lang":"eng"}],"publication_status":"published","publisher":"eLife Sciences Publications","date_published":"2013-06-25T00:00:00Z","department":[{"_id":"KrCh"}],"quality_controlled":"1","volume":2,"article_number":"e00747","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"1400"}]},"year":"2013","publist_id":"3985","citation":{"apa":"Božić, I., Reiter, J., Allen, B., Antal, T., Chatterjee, K., Shah, P., … Nowak, M. (2013). Evolutionary dynamics of cancer in response to targeted combination therapy. ELife. eLife Sciences Publications. https://doi.org/10.7554/eLife.00747","short":"I. Božić, J. Reiter, B. Allen, T. Antal, K. Chatterjee, P. Shah, Y. Moon, A. Yaqubie, N. Kelly, D. Le, E. Lipson, P. Chapman, L. Diaz, B. Vogelstein, M. Nowak, ELife 2 (2013).","ieee":"I. Božić et al., “Evolutionary dynamics of cancer in response to targeted combination therapy,” eLife, vol. 2. eLife Sciences Publications, 2013.","ama":"Božić I, Reiter J, Allen B, et al. Evolutionary dynamics of cancer in response to targeted combination therapy. eLife. 2013;2. doi:10.7554/eLife.00747","mla":"Božić, Ivana, et al. “Evolutionary Dynamics of Cancer in Response to Targeted Combination Therapy.” ELife, vol. 2, e00747, eLife Sciences Publications, 2013, doi:10.7554/eLife.00747.","chicago":"Božić, Ivana, Johannes Reiter, Benjamin Allen, Tibor Antal, Krishnendu Chatterjee, Preya Shah, Yo Moon, et al. “Evolutionary Dynamics of Cancer in Response to Targeted Combination Therapy.” ELife. eLife Sciences Publications, 2013. https://doi.org/10.7554/eLife.00747.","ista":"Božić I, Reiter J, Allen B, Antal T, Chatterjee K, Shah P, Moon Y, Yaqubie A, Kelly N, Le D, Lipson E, Chapman P, Diaz L, Vogelstein B, Nowak M. 2013. Evolutionary dynamics of cancer in response to targeted combination therapy. eLife. 2, e00747."},"date_created":"2018-12-11T11:59:45Z","doi":"10.7554/eLife.00747","file_date_updated":"2020-07-14T12:45:49Z","_id":"2816","month":"06","oa_version":"Published Version","day":"25","file":[{"creator":"system","relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_size":3358321,"file_name":"IST-2013-134-v1+1_e00747.full.pdf","checksum":"2c38c47815eacd8fa66cb8b404cf7c61","file_id":"4967","date_updated":"2020-07-14T12:45:49Z","date_created":"2018-12-12T10:12:48Z"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"last_name":"Božić","first_name":"Ivana","full_name":"Božić, Ivana"},{"id":"4A918E98-F248-11E8-B48F-1D18A9856A87","last_name":"Reiter","orcid":"0000-0002-0170-7353","full_name":"Reiter, Johannes","first_name":"Johannes"},{"first_name":"Benjamin","full_name":"Allen, Benjamin","last_name":"Allen"},{"first_name":"Tibor","full_name":"Antal, Tibor","last_name":"Antal"},{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"last_name":"Shah","full_name":"Shah, Preya","first_name":"Preya"},{"first_name":"Yo","full_name":"Moon, Yo","last_name":"Moon"},{"full_name":"Yaqubie, Amin","first_name":"Amin","last_name":"Yaqubie"},{"last_name":"Kelly","first_name":"Nicole","full_name":"Kelly, Nicole"},{"last_name":"Le","full_name":"Le, Dung","first_name":"Dung"},{"first_name":"Evan","full_name":"Lipson, Evan","last_name":"Lipson"},{"last_name":"Chapman","first_name":"Paul","full_name":"Chapman, Paul"},{"full_name":"Diaz, Luis","first_name":"Luis","last_name":"Diaz"},{"last_name":"Vogelstein","full_name":"Vogelstein, Bert","first_name":"Bert"},{"last_name":"Nowak","first_name":"Martin","full_name":"Nowak, Martin"}],"status":"public","type":"journal_article","has_accepted_license":"1","scopus_import":1,"intvolume":" 2","date_updated":"2023-09-07T11:40:43Z","oa":1,"pubrep_id":"134","title":"Evolutionary dynamics of cancer in response to targeted combination therapy","publication":"eLife","language":[{"iso":"eng"}]},{"publication_status":"published","abstract":[{"text":"The basic idea of evolutionary game theory is that payoff determines reproductive rate. Successful individuals have a higher payoff and produce more offspring. But in evolutionary and ecological situations there is not only reproductive rate but also carrying capacity. Individuals may differ in their exposure to density limiting effects. Here we explore an alternative approach to evolutionary game theory by assuming that the payoff from the game determines the carrying capacity of individual phenotypes. Successful strategies are less affected by density limitation (crowding) and reach higher equilibrium abundance. We demonstrate similarities and differences between our framework and the standard replicator equation. Our equation is defined on the positive orthant, instead of the simplex, but has the same equilibrium points as the replicator equation. Linear stability analysis produces the classical conditions for asymptotic stability of pure strategies, but the stability properties of internal equilibria can differ in the two frameworks. For example, in a two-strategy game with an internal equilibrium that is always stable under the replicator equation, the corresponding equilibrium can be unstable in the new framework resulting in a limit cycle.","lang":"eng"}],"ddc":["000"],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"project":[{"_id":"25B07788-B435-11E9-9278-68D0E5697425","grant_number":"250152","name":"Limits to selection in biology and in evolutionary computation","call_identifier":"FP7"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"page":"26 - 34","department":[{"_id":"NiBa"},{"_id":"KrCh"}],"quality_controlled":"1","volume":334,"publisher":"Elsevier","date_published":"2013-10-07T00:00:00Z","citation":{"apa":"Novak, S., Chatterjee, K., & Nowak, M. (2013). Density games. Journal of Theoretical Biology. Elsevier. https://doi.org/10.1016/j.jtbi.2013.05.029","chicago":"Novak, Sebastian, Krishnendu Chatterjee, and Martin Nowak. “Density Games.” Journal of Theoretical Biology. Elsevier, 2013. https://doi.org/10.1016/j.jtbi.2013.05.029.","ista":"Novak S, Chatterjee K, Nowak M. 2013. Density games. Journal of Theoretical Biology. 334, 26–34.","mla":"Novak, Sebastian, et al. “Density Games.” Journal of Theoretical Biology, vol. 334, Elsevier, 2013, pp. 26–34, doi:10.1016/j.jtbi.2013.05.029.","short":"S. Novak, K. Chatterjee, M. Nowak, Journal of Theoretical Biology 334 (2013) 26–34.","ieee":"S. Novak, K. Chatterjee, and M. Nowak, “Density games,” Journal of Theoretical Biology, vol. 334. Elsevier, pp. 26–34, 2013.","ama":"Novak S, Chatterjee K, Nowak M. Density games. Journal of Theoretical Biology. 2013;334:26-34. doi:10.1016/j.jtbi.2013.05.029"},"publist_id":"3984","date_created":"2018-12-11T11:59:45Z","year":"2013","ec_funded":1,"file_date_updated":"2020-07-14T12:45:49Z","_id":"2817","doi":"10.1016/j.jtbi.2013.05.029","author":[{"first_name":"Sebastian","full_name":"Novak, Sebastian","last_name":"Novak","id":"461468AE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2519-824X"},{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"last_name":"Nowak","first_name":"Martin","full_name":"Nowak, Martin"}],"oa_version":"Published Version","day":"07","file":[{"creator":"system","content_type":"application/pdf","file_size":834604,"relation":"main_file","access_level":"open_access","file_id":"5110","file_name":"IST-2016-400-v1+1_1-s2.0-S0022519313002609-main.pdf","checksum":"3c29059ab03a4b8f97a07646b817ddbb","date_created":"2018-12-12T10:14:54Z","date_updated":"2020-07-14T12:45:49Z"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"10","status":"public","type":"journal_article","title":"Density games","oa":1,"pubrep_id":"400","date_updated":"2025-05-28T11:42:43Z","scopus_import":1,"intvolume":" 334","has_accepted_license":"1","language":[{"iso":"eng"}],"publication":"Journal of Theoretical Biology"},{"date_updated":"2021-01-12T06:59:56Z","oa":1,"title":"Quantitative timed simulation functions and refinement metrics for real-time systems","intvolume":" 1","scopus_import":1,"language":[{"iso":"eng"}],"publication":"Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"first_name":"Vinayak","full_name":"Prabhu, Vinayak","last_name":"Prabhu"}],"month":"04","conference":{"start_date":"2013-04-08","name":"HSCC: Hybrid Systems - Computation and Control","end_date":"2013-04-11","location":"Philadelphia, PA USA"},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","day":"01","oa_version":"Preprint","main_file_link":[{"url":"http://arxiv.org/abs/1212.6556","open_access":"1"}],"type":"conference","status":"public","year":"2013","acknowledgement":"This work has been financially supported in part by the European Commission FP7-ICT Cognitive Systems, Interaction, and Robotics under the contract # 270180 (NOP-TILUS); 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); and the Microsoft faculty fellows award","date_created":"2018-12-11T11:59:46Z","citation":{"ieee":"K. Chatterjee and V. Prabhu, “Quantitative timed simulation functions and refinement metrics for real-time systems,” in Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, Philadelphia, PA USA, 2013, vol. 1, pp. 273–282.","ama":"Chatterjee K, Prabhu V. Quantitative timed simulation functions and refinement metrics for real-time systems. In: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control. Vol 1. Springer; 2013:273-282. doi:10.1145/2461328.2461370","short":"K. Chatterjee, V. Prabhu, in:, Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, Springer, 2013, pp. 273–282.","ista":"Chatterjee K, Prabhu V. 2013. Quantitative timed simulation functions and refinement metrics for real-time systems. Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems - Computation and Control vol. 1, 273–282.","chicago":"Chatterjee, Krishnendu, and Vinayak Prabhu. “Quantitative Timed Simulation Functions and Refinement Metrics for Real-Time Systems.” In Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, 1:273–82. Springer, 2013. https://doi.org/10.1145/2461328.2461370.","mla":"Chatterjee, Krishnendu, and Vinayak Prabhu. “Quantitative Timed Simulation Functions and Refinement Metrics for Real-Time Systems.” Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, vol. 1, Springer, 2013, pp. 273–82, doi:10.1145/2461328.2461370.","apa":"Chatterjee, K., & Prabhu, V. (2013). Quantitative timed simulation functions and refinement metrics for real-time systems. In Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control (Vol. 1, pp. 273–282). Philadelphia, PA USA: Springer. https://doi.org/10.1145/2461328.2461370"},"publist_id":"3982","ec_funded":1,"_id":"2819","doi":"10.1145/2461328.2461370","publication_status":"published","abstract":[{"lang":"eng","text":"We introduce quantatitive timed refinement metrics and quantitative timed simulation functions, incorporating zenoness checks, for timed systems. These functions assign positive real numbers between zero and infinity which quantify the timing mismatches between two timed systems, amongst non-zeno runs. We quantify timing mismatches in three ways: (1) the maximum timing mismatch that can arise, (2) the "steady-state" maximum timing mismatches, where initial transient timing mismatches are ignored; and (3) the (long-run) average timing mismatches amongst two systems. These three kinds of mismatches constitute three important types of timing differences. Our event times are the global times, measured from the start of the system execution, not just the time durations of individual steps. We present algorithms over timed automata for computing the three quantitative simulation functions to within any desired degree of accuracy. In order to compute the values of the quantitative simulation functions, we use a game theoretic formulation. We introduce two new kinds of objectives for two player games on finite state game graphs: (1) eventual debit-sum level objectives, and (2) average debit-sum level objectives. We present algorithms for computing the optimal values for these objectives for player 1, and then use these algorithms to compute the values of the quantitative timed simulation functions. "}],"project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"date_published":"2013-04-01T00:00:00Z","publisher":"Springer","volume":1,"quality_controlled":"1","department":[{"_id":"KrCh"}],"page":"273 - 282"}]