[{"author":[{"first_name":"Brázdil","full_name":"Brázdil, Brázdil","last_name":"Brázdil"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"first_name":"Antonín","full_name":"Kučera, Antonín","last_name":"Kučera"},{"last_name":"Novotny","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","first_name":"Petr","full_name":"Novotny, Petr"}],"day":"01","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1202.0796"}],"oa_version":"Preprint","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","conference":{"end_date":"2012-07-13","location":"Berkeley, CA, USA","start_date":"2012-07-07","name":"CAV: Computer Aided Verification"},"month":"07","alternative_title":["LNCS"],"type":"conference","status":"public","title":"Efficient controller synthesis for consumption games with multiple resource types","oa":1,"date_updated":"2021-01-12T07:41:18Z","intvolume":"      7358","scopus_import":1,"language":[{"iso":"eng"}],"publication_status":"published","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"}],"project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"}],"department":[{"_id":"KrCh"}],"page":"23 - 38","quality_controlled":"1","volume":7358,"publisher":"Springer","date_published":"2012-07-01T00:00:00Z","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>","short":"B. Brázdil, K. Chatterjee, A. Kučera, P. Novotný, in:, Springer, 2012, pp. 23–38.","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.","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>","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>.","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>."},"date_created":"2018-12-11T12:01:35Z","publist_id":"3562","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).","year":"2012","ec_funded":1,"_id":"3135","doi":"10.1007/978-3-642-31424-7_8"},{"language":[{"iso":"eng"}],"publication":"Nature","issue":"7404","oa":1,"date_updated":"2023-09-07T11:40:43Z","title":"The molecular evolution of acquired resistance to targeted EGFR blockade in colorectal cancers","scopus_import":1,"intvolume":"       486","status":"public","type":"journal_article","pmid":1,"author":[{"last_name":"Diaz Jr","full_name":"Diaz Jr, Luis","first_name":"Luis"},{"last_name":"Williams","first_name":"Richard","full_name":"Williams, Richard"},{"full_name":"Wu, Jian","first_name":"Jian","last_name":"Wu"},{"full_name":"Kinde, Isaac","first_name":"Isaac","last_name":"Kinde"},{"full_name":"Hecht, Joel","first_name":"Joel","last_name":"Hecht"},{"last_name":"Berlin","first_name":"Jordan","full_name":"Berlin, Jordan"},{"last_name":"Allen","first_name":"Benjamin","full_name":"Allen, Benjamin"},{"full_name":"Božić, Ivana","first_name":"Ivana","last_name":"Božić"},{"id":"4A918E98-F248-11E8-B48F-1D18A9856A87","last_name":"Reiter","orcid":"0000-0002-0170-7353","full_name":"Reiter, Johannes","first_name":"Johannes"},{"full_name":"Nowak, Martin","first_name":"Martin","last_name":"Nowak"},{"full_name":"Kinzler, Kenneth","first_name":"Kenneth","last_name":"Kinzler"},{"last_name":"Oliner","first_name":"Kelly","full_name":"Oliner, Kelly"},{"full_name":"Vogelstein, Bert","first_name":"Bert","last_name":"Vogelstein"}],"month":"06","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","day":"28","main_file_link":[{"open_access":"1","url":"http://www.ncbi.nlm.nih.gov/pmc/articles/PMC3436069/"}],"oa_version":"Submitted Version","_id":"3157","doi":"10.1038/nature11219","year":"2012","date_created":"2018-12-11T12:01:43Z","publist_id":"3537","citation":{"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>","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.","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.","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>.","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>.","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.","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>"},"related_material":{"record":[{"status":"public","id":"1400","relation":"dissertation_contains"}]},"ec_funded":1,"project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"date_published":"2012-06-28T00:00:00Z","publisher":"Nature Publishing Group","volume":486,"quality_controlled":"1","department":[{"_id":"KrCh"}],"page":"537 - 540","publication_status":"published","abstract":[{"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.","lang":"eng"}],"external_id":{"pmid":["22722843"]}},{"external_id":{"arxiv":["1109.5018"]},"abstract":[{"lang":"eng","text":"Computing the winning set for Büchi objectives in alternating games on graphs is a central problem in computer aided verification with a large number of applications. The long standing best known upper bound for solving the problem is Õ(n·m), where n is the number of vertices and m is the number of edges in the graph. We are the first to break the Õ(n·m) boundary by presenting a new technique that reduces the running time to O(n 2). This bound also leads to O(n 2) time algorithms for computing the set of almost-sure winning vertices for Büchi objectives (1) in alternating games with probabilistic transitions (improving an earlier bound of Õ(n·m)), (2) in concurrent graph games with constant actions (improving an earlier bound of O(n 3)), and (3) in Markov decision processes (improving for m &gt; n 4/3 an earlier bound of O(min(m 1.5, m·n 2/3)). We also show that the same technique can be used to compute the maximal end-component decomposition of a graph in time O(n 2), which is an improvement over earlier bounds for m &gt; n 4/3. Finally, we show how to maintain the winning set for Büchi objectives in alternating games under a sequence of edge insertions or a sequence of edge deletions in O(n) amortized time per operation. This is the first dynamic algorithm for this problem."}],"publication_status":"published","publisher":"SIAM","date_published":"2012-01-01T00:00:00Z","department":[{"_id":"KrCh"}],"page":"1386 - 1399","quality_controlled":"1","project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_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","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"ec_funded":1,"related_material":{"record":[{"relation":"earlier_version","id":"5379","status":"public"},{"status":"public","id":"2141","relation":"later_version"}]},"acknowledgement":"The research was supported by Austrian Science Fund (FWF) Grant No P 23499-N23 on Modern Graph Algorithmic Techniques in Formal Verification, Vienna Science and Technology Fund (WWTF) Grant ICT10-002, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.","year":"2012","citation":{"apa":"Chatterjee, K., &#38; Henzinger, M. H. (2012). An O(n2) time algorithm for alternating Büchi games. In <i>Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms</i> (pp. 1386–1399). Kyoto, Japan: SIAM. <a href=\"https://doi.org/10.1137/1.9781611973099.109\">https://doi.org/10.1137/1.9781611973099.109</a>","ista":"Chatterjee K, Henzinger MH. 2012. An O(n2) time algorithm for alternating Büchi games. Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms. SODA: Symposium on Discrete Algorithms, 1386–1399.","chicago":"Chatterjee, Krishnendu, and Monika H Henzinger. “An O(N2) Time Algorithm for Alternating Büchi Games.” In <i>Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms</i>, 1386–99. SIAM, 2012. <a href=\"https://doi.org/10.1137/1.9781611973099.109\">https://doi.org/10.1137/1.9781611973099.109</a>.","mla":"Chatterjee, Krishnendu, and Monika H. Henzinger. “An O(N2) Time Algorithm for Alternating Büchi Games.” <i>Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms</i>, SIAM, 2012, pp. 1386–99, doi:<a href=\"https://doi.org/10.1137/1.9781611973099.109\">10.1137/1.9781611973099.109</a>.","short":"K. Chatterjee, M.H. Henzinger, in:, Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms, SIAM, 2012, pp. 1386–1399.","ieee":"K. Chatterjee and M. H. Henzinger, “An O(n2) time algorithm for alternating Büchi games,” in <i>Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms</i>, Kyoto, Japan, 2012, pp. 1386–1399.","ama":"Chatterjee K, Henzinger MH. An O(n2) time algorithm for alternating Büchi games. In: <i>Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms</i>. SIAM; 2012:1386-1399. doi:<a href=\"https://doi.org/10.1137/1.9781611973099.109\">10.1137/1.9781611973099.109</a>"},"publist_id":"3519","date_created":"2018-12-11T12:01:46Z","doi":"10.1137/1.9781611973099.109","_id":"3165","conference":{"location":"Kyoto, Japan","end_date":"2012-01-19","name":"SODA: Symposium on Discrete Algorithms","start_date":"2012-01-17"},"month":"01","main_file_link":[{"url":"https://arxiv.org/abs/1109.5018","open_access":"1"}],"day":"01","oa_version":"None","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Henzinger","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","orcid":"0000-0002-5008-6530","first_name":"Monika H","full_name":"Henzinger, Monika H"}],"arxiv":1,"status":"public","type":"conference","date_updated":"2025-06-02T08:53:48Z","pubrep_id":"15","oa":1,"article_processing_charge":"No","title":"An O(n2) time algorithm for alternating Büchi games","publication":"Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms","language":[{"iso":"eng"}]},{"language":[{"iso":"eng"}],"scopus_import":1,"intvolume":"      7148","title":"Synthesizing protocols for digital contract signing","date_updated":"2021-01-12T07:42:08Z","oa":1,"alternative_title":["LNCS"],"status":"public","type":"conference","oa_version":"Preprint","main_file_link":[{"url":"https://arxiv.org/abs/1004.2697","open_access":"1"}],"day":"20","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","conference":{"start_date":"2012-01-22","name":"VMCAI: Verification, Model Checking and Abstract Interpretation","end_date":"2012-01-24","location":"Philadelphia, PA, USA"},"month":"01","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"last_name":"Raman","full_name":"Raman, Vishwanath","first_name":"Vishwanath"}],"doi":"10.1007/978-3-642-27940-9_11","_id":"3252","ec_funded":1,"citation":{"ista":"Chatterjee K, Raman V. 2012. Synthesizing protocols for digital contract signing. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 7148, 152–168.","chicago":"Chatterjee, Krishnendu, and Vishwanath Raman. “Synthesizing Protocols for Digital Contract Signing,” 7148:152–68. Springer, 2012. <a href=\"https://doi.org/10.1007/978-3-642-27940-9_11\">https://doi.org/10.1007/978-3-642-27940-9_11</a>.","mla":"Chatterjee, Krishnendu, and Vishwanath Raman. <i>Synthesizing Protocols for Digital Contract Signing</i>. Vol. 7148, Springer, 2012, pp. 152–68, doi:<a href=\"https://doi.org/10.1007/978-3-642-27940-9_11\">10.1007/978-3-642-27940-9_11</a>.","ama":"Chatterjee K, Raman V. Synthesizing protocols for digital contract signing. In: Vol 7148. Springer; 2012:152-168. doi:<a href=\"https://doi.org/10.1007/978-3-642-27940-9_11\">10.1007/978-3-642-27940-9_11</a>","ieee":"K. Chatterjee and V. Raman, “Synthesizing protocols for digital contract signing,” presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Philadelphia, PA, USA, 2012, vol. 7148, pp. 152–168.","short":"K. Chatterjee, V. Raman, in:, Springer, 2012, pp. 152–168.","apa":"Chatterjee, K., &#38; Raman, V. (2012). Synthesizing protocols for digital contract signing (Vol. 7148, pp. 152–168). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Philadelphia, PA, USA: Springer. <a href=\"https://doi.org/10.1007/978-3-642-27940-9_11\">https://doi.org/10.1007/978-3-642-27940-9_11</a>"},"date_created":"2018-12-11T12:02:16Z","publist_id":"3405","acknowledgement":"The research was supported by Austrian Science Fund (FWF) Grant No P 23499-N23 (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.\r\nThe authors would like to thank Avik Chaudhuri for his invaluable help and feedback.","year":"2012","page":"152 - 168","department":[{"_id":"KrCh"}],"volume":7148,"quality_controlled":"1","publisher":"Springer","date_published":"2012-01-20T00:00:00Z","project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"abstract":[{"text":"We study the automatic synthesis of fair non-repudiation protocols, a class of fair exchange protocols, used for digital contract signing. First, we show how to specify the objectives of the participating agents, the trusted third party (TTP) and the protocols as path formulas in Linear Temporal Logic (LTL) and prove that the satisfaction of the objectives of the agents and the TTP imply satisfaction of the protocol objectives. We then show that weak (co-operative) co-synthesis and classical (strictly competitive) co-synthesis fail in synthesizing these protocols, whereas assume-guarantee synthesis (AGS) succeeds. We demonstrate the success of assume-guarantee synthesis as follows: (a) any solution of assume-guarantee synthesis is attack-free; no subset of participants can violate the objectives of the other participants without violating their own objectives; (b) the Asokan-Shoup-Waidner (ASW) certified mail protocol that has known vulnerabilities is not a solution of AGS; and (c) the Kremer-Markowitch (KM) non-repudiation protocol is a solution of AGS. To our knowledge this is the first application of synthesis to fair non-repudiation protocols, and our results show how synthesis can generate correct protocols and automatically discover vulnerabilities. The solution to assume-guarantee synthesis can be computed efficiently as the secure equilibrium solution of three-player graph games. © 2012 Springer-Verlag.","lang":"eng"}],"publication_status":"published"},{"status":"public","type":"journal_article","author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"}],"month":"02","oa_version":"None","main_file_link":[{"url":"http://arise.or.at/pubpdf/The_complexity_of_stochastic_M___u_ller_games.pdf"}],"day":"01","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"publication":"Information and Computation","date_updated":"2021-01-12T07:42:09Z","title":"The complexity of stochastic Müller games","intvolume":"       211","scopus_import":1,"project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"publisher":"Elsevier","date_published":"2012-02-01T00:00:00Z","page":"29 - 48","department":[{"_id":"KrCh"}],"volume":211,"quality_controlled":"1","publication_status":"published","abstract":[{"lang":"eng","text":"The theory of graph games with ω-regular winning conditions is the foundation for modeling and synthesizing reactive processes. In the case of stochastic reactive processes, the corresponding stochastic graph games have three players, two of them (System and Environment) behaving adversarially, and the third (Uncertainty) behaving probabilistically. We consider two problems for stochastic graph games: the qualitative problem asks for the set of states from which a player can win with probability 1 (almost-sure winning); and the quantitative problem asks for the maximal probability of winning (optimal winning) from each state. We consider ω-regular winning conditions formalized as Müller winning conditions. We present optimal memory bounds for pure (deterministic) almost-sure winning and optimal winning strategies in stochastic graph games with Müller winning conditions. We also study the complexity of stochastic Müller games and show that both the qualitative and quantitative analysis problems are PSPACE-complete. Our results are relevant in synthesis of stochastic reactive processes."}],"_id":"3254","doi":"10.1016/j.ic.2011.11.004","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.","year":"2012","citation":{"ama":"Chatterjee K. The complexity of stochastic Müller games. <i>Information and Computation</i>. 2012;211:29-48. doi:<a href=\"https://doi.org/10.1016/j.ic.2011.11.004\">10.1016/j.ic.2011.11.004</a>","ieee":"K. Chatterjee, “The complexity of stochastic Müller games,” <i>Information and Computation</i>, vol. 211. Elsevier, pp. 29–48, 2012.","short":"K. Chatterjee, Information and Computation 211 (2012) 29–48.","chicago":"Chatterjee, Krishnendu. “The Complexity of Stochastic Müller Games.” <i>Information and Computation</i>. Elsevier, 2012. <a href=\"https://doi.org/10.1016/j.ic.2011.11.004\">https://doi.org/10.1016/j.ic.2011.11.004</a>.","mla":"Chatterjee, Krishnendu. “The Complexity of Stochastic Müller Games.” <i>Information and Computation</i>, vol. 211, Elsevier, 2012, pp. 29–48, doi:<a href=\"https://doi.org/10.1016/j.ic.2011.11.004\">10.1016/j.ic.2011.11.004</a>.","ista":"Chatterjee K. 2012. The complexity of stochastic Müller games. Information and Computation. 211, 29–48.","apa":"Chatterjee, K. (2012). The complexity of stochastic Müller games. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2011.11.004\">https://doi.org/10.1016/j.ic.2011.11.004</a>"},"date_created":"2018-12-11T12:02:17Z","publist_id":"3403","ec_funded":1},{"language":[{"iso":"eng"}],"title":"Games and Markov decision processes with mean payoff parity and energy parity objectives","oa":1,"date_updated":"2021-01-12T07:42:10Z","article_processing_charge":"No","has_accepted_license":"1","scopus_import":1,"intvolume":"      7119","alternative_title":["LNCS"],"type":"conference","status":"public","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Doyen","first_name":"Laurent","full_name":"Doyen, Laurent"}],"day":"01","oa_version":"Submitted Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"date_created":"2020-05-15T12:53:12Z","date_updated":"2020-07-14T12:46:05Z","file_id":"7863","file_name":"2012_MEMICS_Chatterjee.pdf","checksum":"eed2cc1e76b160418c977e76e8899a60","file_size":114060,"relation":"main_file","content_type":"application/pdf","access_level":"open_access","creator":"dernst"}],"conference":{"end_date":"2011-10-16","location":"Lednice, Czech Republic","start_date":"2011-10-14","name":"MEMICS: Mathematical and Engineering Methods in Computer Science"},"month":"01","file_date_updated":"2020-07-14T12:46:05Z","_id":"3255","doi":"10.1007/978-3-642-25929-6_3","citation":{"apa":"Chatterjee, K., &#38; Doyen, L. (2012). Games and Markov decision processes with mean payoff parity and energy parity objectives (Vol. 7119, pp. 37–46). Presented at the MEMICS: Mathematical and Engineering Methods in Computer Science, Lednice, Czech Republic: Springer. <a href=\"https://doi.org/10.1007/978-3-642-25929-6_3\">https://doi.org/10.1007/978-3-642-25929-6_3</a>","chicago":"Chatterjee, Krishnendu, and Laurent Doyen. “Games and Markov Decision Processes with Mean Payoff Parity and Energy Parity Objectives,” 7119:37–46. Springer, 2012. <a href=\"https://doi.org/10.1007/978-3-642-25929-6_3\">https://doi.org/10.1007/978-3-642-25929-6_3</a>.","mla":"Chatterjee, Krishnendu, and Laurent Doyen. <i>Games and Markov Decision Processes with Mean Payoff Parity and Energy Parity Objectives</i>. Vol. 7119, Springer, 2012, pp. 37–46, doi:<a href=\"https://doi.org/10.1007/978-3-642-25929-6_3\">10.1007/978-3-642-25929-6_3</a>.","ista":"Chatterjee K, Doyen L. 2012. Games and Markov decision processes with mean payoff parity and energy parity objectives. MEMICS: Mathematical and Engineering Methods in Computer Science, LNCS, vol. 7119, 37–46.","short":"K. Chatterjee, L. Doyen, in:, Springer, 2012, pp. 37–46.","ieee":"K. Chatterjee and L. Doyen, “Games and Markov decision processes with mean payoff parity and energy parity objectives,” presented at the MEMICS: Mathematical and Engineering Methods in Computer Science, Lednice, Czech Republic, 2012, vol. 7119, pp. 37–46.","ama":"Chatterjee K, Doyen L. Games and Markov decision processes with mean payoff parity and energy parity objectives. In: Vol 7119. Springer; 2012:37-46. doi:<a href=\"https://doi.org/10.1007/978-3-642-25929-6_3\">10.1007/978-3-642-25929-6_3</a>"},"publist_id":"3400","date_created":"2018-12-11T12:02:17Z","acknowledgement":"This work was partially supported by FWF NFN Grant S11407-N23 (RiSE) and a Microsoft faculty fellowship.","year":"2012","project":[{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"}],"department":[{"_id":"KrCh"}],"page":"37 - 46","quality_controlled":"1","volume":7119,"publisher":"Springer","date_published":"2012-01-01T00:00:00Z","publication_status":"published","abstract":[{"text":"In this paper we survey results of two-player games on graphs and Markov decision processes with parity, mean-payoff and energy objectives, and the combination of mean-payoff and energy objectives with parity objectives. These problems have applications in verification and synthesis of reactive systems in resource-constrained environments.","lang":"eng"}],"ddc":["000"]},{"scopus_import":1,"intvolume":"        81","issue":"1","oa":1,"date_updated":"2023-09-07T11:40:43Z","title":"Evolutionary dynamics of biological auctions","publication":"Theoretical Population Biology","language":[{"iso":"eng"}],"month":"02","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"01","main_file_link":[{"url":"http://www.ncbi.nlm.nih.gov/pmc/articles/PMC3279759/ ","open_access":"1"}],"oa_version":"Submitted Version","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"first_name":"Johannes","full_name":"Reiter, Johannes","id":"4A918E98-F248-11E8-B48F-1D18A9856A87","last_name":"Reiter","orcid":"0000-0002-0170-7353"},{"last_name":"Nowak","first_name":"Martin","full_name":"Nowak, Martin"}],"type":"journal_article","status":"public","pmid":1,"related_material":{"record":[{"id":"1400","relation":"dissertation_contains","status":"public"}]},"ec_funded":1,"year":"2012","publist_id":"3388","date_created":"2018-12-11T12:02:19Z","citation":{"ama":"Chatterjee K, Reiter J, Nowak M. Evolutionary dynamics of biological auctions. <i>Theoretical Population Biology</i>. 2012;81(1):69-80. doi:<a href=\"https://doi.org/10.1016/j.tpb.2011.11.003\">10.1016/j.tpb.2011.11.003</a>","ieee":"K. Chatterjee, J. Reiter, and M. Nowak, “Evolutionary dynamics of biological auctions,” <i>Theoretical Population Biology</i>, vol. 81, no. 1. Academic Press, pp. 69–80, 2012.","short":"K. Chatterjee, J. Reiter, M. Nowak, Theoretical Population Biology 81 (2012) 69–80.","chicago":"Chatterjee, Krishnendu, Johannes Reiter, and Martin Nowak. “Evolutionary Dynamics of Biological Auctions.” <i>Theoretical Population Biology</i>. Academic Press, 2012. <a href=\"https://doi.org/10.1016/j.tpb.2011.11.003\">https://doi.org/10.1016/j.tpb.2011.11.003</a>.","mla":"Chatterjee, Krishnendu, et al. “Evolutionary Dynamics of Biological Auctions.” <i>Theoretical Population Biology</i>, vol. 81, no. 1, Academic Press, 2012, pp. 69–80, doi:<a href=\"https://doi.org/10.1016/j.tpb.2011.11.003\">10.1016/j.tpb.2011.11.003</a>.","ista":"Chatterjee K, Reiter J, Nowak M. 2012. Evolutionary dynamics of biological auctions. Theoretical Population Biology. 81(1), 69–80.","apa":"Chatterjee, K., Reiter, J., &#38; Nowak, M. (2012). Evolutionary dynamics of biological auctions. <i>Theoretical Population Biology</i>. Academic Press. <a href=\"https://doi.org/10.1016/j.tpb.2011.11.003\">https://doi.org/10.1016/j.tpb.2011.11.003</a>"},"doi":"10.1016/j.tpb.2011.11.003","_id":"3260","abstract":[{"lang":"eng","text":"Many scenarios in the living world, where individual organisms compete for winning positions (or resources), have properties of auctions. Here we study the evolution of bids in biological auctions. For each auction, n individuals are drawn at random from a population of size N. Each individual makes a bid which entails a cost. The winner obtains a benefit of a certain value. Costs and benefits are translated into reproductive success (fitness). Therefore, successful bidding strategies spread in the population. We compare two types of auctions. In “biological all-pay auctions”, the costs are the bid for every participating individual. In “biological second price all-pay auctions”, the cost for everyone other than the winner is the bid, but the cost for the winner is the second highest bid. Second price all-pay auctions are generalizations of the “war of attrition” introduced by Maynard Smith. We study evolutionary dynamics in both types of auctions. We calculate pairwise invasion plots and evolutionarily stable distributions over the continuous strategy space. We find that the average bid in second price all-pay auctions is higher than in all-pay auctions, but the average cost for the winner is similar in both auctions. In both cases, the average bid is a declining function of the number of participants, n. The more individuals participate in an auction the smaller is the chance of winning, and thus expensive bids must be avoided.\r\n"}],"external_id":{"pmid":["22120126"]},"publication_status":"published","date_published":"2012-02-01T00:00:00Z","publisher":"Academic Press","quality_controlled":"1","volume":81,"department":[{"_id":"KrCh"}],"page":"69 - 80","project":[{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}]},{"project":[{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"date_published":"2012-04-01T00:00:00Z","status":"public","type":"journal_article","publisher":"World Scientific Publishing","volume":23,"quality_controlled":"1","department":[{"_id":"KrCh"}],"page":"609 - 625","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Ritankar","full_name":"Majumdar, Ritankar","last_name":"Majumdar"}],"publication_status":"published","month":"04","abstract":[{"lang":"eng","text":"We introduce two-level discounted and mean-payoff games played by two players on a perfect-information stochastic game graph. The upper level game is a discounted or mean-payoff game and the lower level game is a (undiscounted) reachability game. Two-level games model hierarchical and sequential decision making under uncertainty across different time scales. For both discounted and mean-payoff two-level games, we show the existence of pure memoryless optimal strategies for both players and an ordered field property. We show that if there is only one player (Markov decision processes), then the values can be computed in polynomial time. It follows that whether the value of a player is equal to a given rational constant in two-level discounted or mean-payoff games can be decided in NP ∩ coNP. We also give an alternate strategy improvement algorithm to compute the value. © 2012 World Scientific Publishing Company."}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","oa_version":"None","day":"01","language":[{"iso":"eng"}],"_id":"3314","publication":"International Journal of Foundations of Computer Science","doi":"10.1142/S0129054112400308","year":"2012","issue":"3","date_updated":"2021-01-12T07:42:35Z","date_created":"2018-12-11T12:02:37Z","citation":{"chicago":"Chatterjee, Krishnendu, and Ritankar Majumdar. “Discounting and Averaging in Games across Time Scales.” <i>International Journal of Foundations of Computer Science</i>. World Scientific Publishing, 2012. <a href=\"https://doi.org/10.1142/S0129054112400308\">https://doi.org/10.1142/S0129054112400308</a>.","ista":"Chatterjee K, Majumdar R. 2012. Discounting and averaging in games across time scales. International Journal of Foundations of Computer Science. 23(3), 609–625.","mla":"Chatterjee, Krishnendu, and Ritankar Majumdar. “Discounting and Averaging in Games across Time Scales.” <i>International Journal of Foundations of Computer Science</i>, vol. 23, no. 3, World Scientific Publishing, 2012, pp. 609–25, doi:<a href=\"https://doi.org/10.1142/S0129054112400308\">10.1142/S0129054112400308</a>.","ama":"Chatterjee K, Majumdar R. Discounting and averaging in games across time scales. <i>International Journal of Foundations of Computer Science</i>. 2012;23(3):609-625. doi:<a href=\"https://doi.org/10.1142/S0129054112400308\">10.1142/S0129054112400308</a>","ieee":"K. Chatterjee and R. Majumdar, “Discounting and averaging in games across time scales,” <i>International Journal of Foundations of Computer Science</i>, vol. 23, no. 3. World Scientific Publishing, pp. 609–625, 2012.","short":"K. Chatterjee, R. Majumdar, International Journal of Foundations of Computer Science 23 (2012) 609–625.","apa":"Chatterjee, K., &#38; Majumdar, R. (2012). Discounting and averaging in games across time scales. <i>International Journal of Foundations of Computer Science</i>. World Scientific Publishing. <a href=\"https://doi.org/10.1142/S0129054112400308\">https://doi.org/10.1142/S0129054112400308</a>"},"title":"Discounting and averaging in games across time scales","publist_id":"3326","scopus_import":1,"intvolume":"        23"},{"title":"Robustness of structurally equivalent concurrent parity games","date_updated":"2023-02-23T12:23:46Z","oa":1,"scopus_import":1,"intvolume":"      7213","language":[{"iso":"eng"}],"arxiv":1,"author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","main_file_link":[{"url":"http://arxiv.org/abs/1107.2009","open_access":"1"}],"day":"22","oa_version":"Preprint","month":"03","conference":{"start_date":"2012-03-24","name":"FoSSaCS: Foundations of Software Science and Computation Structures","end_date":"2012-04-01","location":"Tallinn, Estonia"},"status":"public","type":"conference","alternative_title":["LNCS"],"citation":{"ama":"Chatterjee K. Robustness of structurally equivalent concurrent parity games. In: Vol 7213. Springer; 2012:270-285. doi:<a href=\"https://doi.org/10.1007/978-3-642-28729-9_18\">10.1007/978-3-642-28729-9_18</a>","ieee":"K. Chatterjee, “Robustness of structurally equivalent concurrent parity games,” presented at the FoSSaCS: Foundations of Software Science and Computation Structures, Tallinn, Estonia, 2012, vol. 7213, pp. 270–285.","short":"K. Chatterjee, in:, Springer, 2012, pp. 270–285.","chicago":"Chatterjee, Krishnendu. “Robustness of Structurally Equivalent Concurrent Parity Games,” 7213:270–85. Springer, 2012. <a href=\"https://doi.org/10.1007/978-3-642-28729-9_18\">https://doi.org/10.1007/978-3-642-28729-9_18</a>.","mla":"Chatterjee, Krishnendu. <i>Robustness of Structurally Equivalent Concurrent Parity Games</i>. Vol. 7213, Springer, 2012, pp. 270–85, doi:<a href=\"https://doi.org/10.1007/978-3-642-28729-9_18\">10.1007/978-3-642-28729-9_18</a>.","ista":"Chatterjee K. 2012. Robustness of structurally equivalent concurrent parity games. FoSSaCS: Foundations of Software Science and Computation Structures, LNCS, vol. 7213, 270–285.","apa":"Chatterjee, K. (2012). Robustness of structurally equivalent concurrent parity games (Vol. 7213, pp. 270–285). Presented at the FoSSaCS: Foundations of Software Science and Computation Structures, Tallinn, Estonia: Springer. <a href=\"https://doi.org/10.1007/978-3-642-28729-9_18\">https://doi.org/10.1007/978-3-642-28729-9_18</a>"},"date_created":"2018-12-11T12:02:46Z","publist_id":"3284","year":"2012","related_material":{"record":[{"relation":"earlier_version","id":"5382","status":"public"}]},"ec_funded":1,"_id":"3341","doi":"10.1007/978-3-642-28729-9_18","publication_status":"published","abstract":[{"text":"We consider two-player stochastic games played on a finite state space for an infinite number of rounds. The games are concurrent: in each round, the two players (player 1 and player 2) choose their moves independently and simultaneously; the current state and the two moves determine a probability distribution over the successor states. We also consider the important special case of turn-based stochastic games where players make moves in turns, rather than concurrently. We study concurrent games with \\omega-regular winning conditions specified as parity objectives. The value for player 1 for a parity objective is the maximal probability with which the player can guarantee the satisfaction of the objective against all strategies of the opponent. We study the problem of continuity and robustness of the value function in concurrent and turn-based stochastic parity gameswith respect to imprecision in the transition probabilities. We present quantitative bounds on the difference of the value function (in terms of the imprecision of the transition probabilities) and show the value continuity for structurally equivalent concurrent games (two games are structurally equivalent if the support of the transition function is same and the probabilities differ). We also show robustness of optimal strategies for structurally equivalent turn-based stochastic parity games. Finally we show that the value continuity property breaks without the structurally equivalent assumption (even for Markov chains) and show that our quantitative bound is asymptotically optimal. Hence our results are tight (the assumption is both necessary and sufficient) and optimal (our quantitative bound is asymptotically optimal).","lang":"eng"}],"external_id":{"arxiv":["1107.2009"]},"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"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"}],"quality_controlled":"1","volume":7213,"page":"270 - 285","department":[{"_id":"KrCh"}],"date_published":"2012-03-22T00:00:00Z","publisher":"Springer"},{"type":"journal_article","status":"public","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A"}],"month":"03","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"relation":"main_file","access_level":"open_access","file_size":336450,"content_type":"application/pdf","creator":"kschuh","date_updated":"2020-07-14T12:46:17Z","date_created":"2019-01-29T10:54:28Z","file_name":"a_survey_of_stochastic_omega-regular_games.pdf","file_id":"5897","checksum":"241b939deb4517cdd4426d49c67e3fa2"}],"main_file_link":[{"open_access":"1","url":"https://doi.org/10.1016/j.jcss.2011.05.002"}],"day":"02","oa_version":"Submitted Version","language":[{"iso":"eng"}],"publication":"Journal of Computer and System Sciences","issue":"2","article_processing_charge":"No","oa":1,"date_updated":"2022-05-24T08:00:54Z","title":"A survey of stochastic ω regular games","intvolume":"        78","scopus_import":"1","has_accepted_license":"1","date_published":"2012-03-02T00:00:00Z","publisher":"Elsevier","quality_controlled":"1","volume":78,"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"page":"394 - 413","publication_status":"published","ddc":["000"],"abstract":[{"lang":"eng","text":"We summarize classical and recent results about two-player games played on graphs with ω-regular objectives. These games have applications in the verification and synthesis of reactive systems. Important distinctions are whether a graph game is turn-based or concurrent; deterministic or stochastic; zero-sum or not. We cluster known results and open problems according to these classifications."}],"article_type":"original","_id":"3846","file_date_updated":"2020-07-14T12:46:17Z","doi":"10.1016/j.jcss.2011.05.002","year":"2012","acknowledgement":"This research was supported in part by the ONR grant N00014-02-1-0671, by the AFOSR MURI grant F49620-00-1-0327, and by the NSF grants CCR-9988172, CCR-0085949, and CCR-0225610.","citation":{"ieee":"K. Chatterjee and T. A. Henzinger, “A survey of stochastic ω regular games,” <i>Journal of Computer and System Sciences</i>, vol. 78, no. 2. Elsevier, pp. 394–413, 2012.","ama":"Chatterjee K, Henzinger TA. A survey of stochastic ω regular games. <i>Journal of Computer and System Sciences</i>. 2012;78(2):394-413. doi:<a href=\"https://doi.org/10.1016/j.jcss.2011.05.002\">10.1016/j.jcss.2011.05.002</a>","short":"K. Chatterjee, T.A. Henzinger, Journal of Computer and System Sciences 78 (2012) 394–413.","mla":"Chatterjee, Krishnendu, and Thomas A. Henzinger. “A Survey of Stochastic ω Regular Games.” <i>Journal of Computer and System Sciences</i>, vol. 78, no. 2, Elsevier, 2012, pp. 394–413, doi:<a href=\"https://doi.org/10.1016/j.jcss.2011.05.002\">10.1016/j.jcss.2011.05.002</a>.","chicago":"Chatterjee, Krishnendu, and Thomas A Henzinger. “A Survey of Stochastic ω Regular Games.” <i>Journal of Computer and System Sciences</i>. Elsevier, 2012. <a href=\"https://doi.org/10.1016/j.jcss.2011.05.002\">https://doi.org/10.1016/j.jcss.2011.05.002</a>.","ista":"Chatterjee K, Henzinger TA. 2012. A survey of stochastic ω regular games. Journal of Computer and System Sciences. 78(2), 394–413.","apa":"Chatterjee, K., &#38; Henzinger, T. A. (2012). A survey of stochastic ω regular games. <i>Journal of Computer and System Sciences</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.jcss.2011.05.002\">https://doi.org/10.1016/j.jcss.2011.05.002</a>"},"publist_id":"2341","date_created":"2018-12-11T12:05:29Z"},{"ec_funded":1,"year":"2012","publist_id":"7325","citation":{"apa":"Kruckman, A., Rubin, S., Sheridan, J., &#38; Zax, B. (2012). A Myhill Nerode theorem for automata with advice. In <i>Proceedings GandALF 2012</i> (Vol. 96, pp. 238–246). Napoli, Italy: Open Publishing Association. <a href=\"https://doi.org/10.4204/EPTCS.96.18\">https://doi.org/10.4204/EPTCS.96.18</a>","short":"A. Kruckman, S. Rubin, J. Sheridan, B. Zax, in:, Proceedings GandALF 2012, Open Publishing Association, 2012, pp. 238–246.","ieee":"A. Kruckman, S. Rubin, J. Sheridan, and B. Zax, “A Myhill Nerode theorem for automata with advice,” in <i>Proceedings GandALF 2012</i>, Napoli, Italy, 2012, vol. 96, pp. 238–246.","ama":"Kruckman A, Rubin S, Sheridan J, Zax B. A Myhill Nerode theorem for automata with advice. In: <i>Proceedings GandALF 2012</i>. Vol 96. Open Publishing Association; 2012:238-246. doi:<a href=\"https://doi.org/10.4204/EPTCS.96.18\">10.4204/EPTCS.96.18</a>","mla":"Kruckman, Alex, et al. “A Myhill Nerode Theorem for Automata with Advice.” <i>Proceedings GandALF 2012</i>, vol. 96, Open Publishing Association, 2012, pp. 238–46, doi:<a href=\"https://doi.org/10.4204/EPTCS.96.18\">10.4204/EPTCS.96.18</a>.","chicago":"Kruckman, Alex, Sasha Rubin, John Sheridan, and Ben Zax. “A Myhill Nerode Theorem for Automata with Advice.” In <i>Proceedings GandALF 2012</i>, 96:238–46. Open Publishing Association, 2012. <a href=\"https://doi.org/10.4204/EPTCS.96.18\">https://doi.org/10.4204/EPTCS.96.18</a>.","ista":"Kruckman A, Rubin S, Sheridan J, Zax B. 2012. A Myhill Nerode theorem for automata with advice. Proceedings GandALF 2012. GandALF: Games, Automata, Logics and Formal Verification, EPTCS, vol. 96, 238–246."},"date_created":"2018-12-11T11:46:47Z","doi":"10.4204/EPTCS.96.18","file_date_updated":"2020-07-14T12:46:35Z","_id":"495","ddc":["004"],"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":[{"lang":"eng","text":"An automaton with advice is a finite state automaton which has access to an additional fixed infinite string called an advice tape. We refine the Myhill-Nerode theorem to characterize the languages of finite strings that are accepted by automata with advice. We do the same for tree automata with advice."}],"publication_status":"published","publisher":"Open Publishing Association","date_published":"2012-10-07T00:00:00Z","department":[{"_id":"KrCh"}],"page":"238 - 246","quality_controlled":"1","volume":96,"project":[{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"}],"scopus_import":1,"has_accepted_license":"1","intvolume":"        96","oa":1,"pubrep_id":"944","date_updated":"2021-01-12T08:01:04Z","title":"A Myhill Nerode theorem for automata with advice","publication":"Proceedings GandALF 2012","language":[{"iso":"eng"}],"conference":{"end_date":"2012-09-08","location":"Napoli, Italy","start_date":"2012-09-06","name":"GandALF: Games, Automata, Logics and Formal Verification"},"month":"10","day":"07","oa_version":"Published Version","file":[{"content_type":"application/pdf","access_level":"open_access","relation":"main_file","file_size":97736,"creator":"system","date_updated":"2020-07-14T12:46:35Z","date_created":"2018-12-12T10:15:31Z","file_name":"IST-2018-944-v1+1_2012_Rubin_A_Myhill.pdf","checksum":"56277f95edc9d531fa3bdc5f9579fda8","file_id":"5152"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","author":[{"last_name":"Kruckman","full_name":"Kruckman, Alex","first_name":"Alex"},{"first_name":"Sasha","full_name":"Rubin, Sasha","last_name":"Rubin","id":"2EC51194-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Sheridan","first_name":"John","full_name":"Sheridan, John"},{"full_name":"Zax, Ben","first_name":"Ben","last_name":"Zax"}],"alternative_title":["EPTCS"],"status":"public","type":"conference"},{"date_updated":"2021-01-12T08:01:05Z","oa":1,"year":"2012","date_created":"2018-12-11T11:46:47Z","citation":{"apa":"Rabinovich, A., &#38; Rubin, S. (2012). Interpretations in trees with countably many branches. Presented at the LICS: Symposium on Logic in Computer Science, Dubrovnik, Croatia: IEEE. <a href=\"https://doi.org/10.1109/LICS.2012.65\">https://doi.org/10.1109/LICS.2012.65</a>","short":"A. Rabinovich, S. Rubin, in:, IEEE, 2012.","ama":"Rabinovich A, Rubin S. Interpretations in trees with countably many branches. In: IEEE; 2012. doi:<a href=\"https://doi.org/10.1109/LICS.2012.65\">10.1109/LICS.2012.65</a>","ieee":"A. Rabinovich and S. Rubin, “Interpretations in trees with countably many branches,” presented at the LICS: Symposium on Logic in Computer Science, Dubrovnik, Croatia, 2012.","ista":"Rabinovich A, Rubin S. 2012. Interpretations in trees with countably many branches. LICS: Symposium on Logic in Computer Science, LICS, , 6280474.","mla":"Rabinovich, Alexander, and Sasha Rubin. <i>Interpretations in Trees with Countably Many Branches</i>. 6280474, IEEE, 2012, doi:<a href=\"https://doi.org/10.1109/LICS.2012.65\">10.1109/LICS.2012.65</a>.","chicago":"Rabinovich, Alexander, and Sasha Rubin. “Interpretations in Trees with Countably Many Branches.” IEEE, 2012. <a href=\"https://doi.org/10.1109/LICS.2012.65\">https://doi.org/10.1109/LICS.2012.65</a>."},"title":"Interpretations in trees with countably many branches","publist_id":"7324","ec_funded":1,"scopus_import":1,"article_number":"6280474","_id":"496","language":[{"iso":"eng"}],"doi":"10.1109/LICS.2012.65","publication_status":"published","author":[{"full_name":"Rabinovich, Alexander","first_name":"Alexander","last_name":"Rabinovich"},{"full_name":"Rubin, Sasha","first_name":"Sasha","id":"2EC51194-F248-11E8-B48F-1D18A9856A87","last_name":"Rubin"}],"conference":{"end_date":"2012-06-28","location":"Dubrovnik, Croatia","start_date":"2012-06-25","name":"LICS: Symposium on Logic in Computer Science"},"month":"01","oa_version":"Preprint","main_file_link":[{"open_access":"1","url":"https://arise.or.at/pubpdf/Interpretations_in_Trees_with_Countably_Many_Branches.pdf"}],"day":"01","abstract":[{"text":"We study the expressive power of logical interpretations on the class of scattered trees, namely those with countably many infinite branches. Scattered trees can be thought of as the tree analogue of scattered linear orders. Every scattered tree has an ordinal rank that reflects the structure of its infinite branches. We prove, roughly, that trees and orders of large rank cannot be interpreted in scattered trees of small rank. We consider a quite general notion of interpretation: each element of the interpreted structure is represented by a set of tuples of subsets of the interpreting tree. Our trees are countable, not necessarily finitely branching, and may have finitely many unary predicates as labellings. We also show how to replace injective set-interpretations in (not necessarily scattered) trees by 'finitary' set-interpretations.","lang":"eng"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","project":[{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"}],"alternative_title":["LICS"],"publisher":"IEEE","type":"conference","status":"public","date_published":"2012-01-01T00:00:00Z","department":[{"_id":"KrCh"}],"quality_controlled":"1"},{"has_accepted_license":"1","scopus_import":1,"intvolume":"        16","pubrep_id":"943","date_updated":"2023-02-23T12:23:32Z","oa":1,"title":"Faster algorithms for alternating refinement relations","language":[{"iso":"eng"}],"conference":{"name":"EACSL: European Association for Computer Science Logic","start_date":"2012-09-03","location":"Fontainebleau, France","end_date":"2012-09-06"},"month":"09","oa_version":"Published Version","day":"01","file":[{"checksum":"f1b0dd99240800db2d7dbf9b5131fe5e","file_name":"IST-2018-943-v1+1_2012_Chatterjee_Faster_Algorithms.pdf","file_id":"4712","date_created":"2018-12-12T10:08:50Z","date_updated":"2020-07-14T12:46:35Z","creator":"system","content_type":"application/pdf","access_level":"open_access","file_size":471236,"relation":"main_file"}],"user_id":"3E5EF7F0-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"},{"last_name":"Chaubal","full_name":"Chaubal, Siddhesh","first_name":"Siddhesh"},{"last_name":"Kamath","first_name":"Pritish","full_name":"Kamath, Pritish"}],"alternative_title":["LIPIcs"],"type":"conference","status":"public","ec_funded":1,"related_material":{"record":[{"relation":"earlier_version","id":"5378","status":"public"}]},"year":"2012","publist_id":"7323","date_created":"2018-12-11T11:46:48Z","citation":{"ista":"Chatterjee K, Chaubal S, Kamath P. 2012. Faster algorithms for alternating refinement relations. EACSL: European Association for Computer Science Logic, LIPIcs, vol. 16, 167–182.","mla":"Chatterjee, Krishnendu, et al. <i>Faster Algorithms for Alternating Refinement Relations</i>. Vol. 16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012, pp. 167–82, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CSL.2012.167\">10.4230/LIPIcs.CSL.2012.167</a>.","chicago":"Chatterjee, Krishnendu, Siddhesh Chaubal, and Pritish Kamath. “Faster Algorithms for Alternating Refinement Relations,” 16:167–82. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. <a href=\"https://doi.org/10.4230/LIPIcs.CSL.2012.167\">https://doi.org/10.4230/LIPIcs.CSL.2012.167</a>.","short":"K. Chatterjee, S. Chaubal, P. Kamath, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012, pp. 167–182.","ieee":"K. Chatterjee, S. Chaubal, and P. Kamath, “Faster algorithms for alternating refinement relations,” presented at the EACSL: European Association for Computer Science Logic, Fontainebleau, France, 2012, vol. 16, pp. 167–182.","ama":"Chatterjee K, Chaubal S, Kamath P. Faster algorithms for alternating refinement relations. In: Vol 16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2012:167-182. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CSL.2012.167\">10.4230/LIPIcs.CSL.2012.167</a>","apa":"Chatterjee, K., Chaubal, S., &#38; Kamath, P. (2012). Faster algorithms for alternating refinement relations (Vol. 16, pp. 167–182). Presented at the EACSL: European Association for Computer Science Logic, Fontainebleau, France: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CSL.2012.167\">https://doi.org/10.4230/LIPIcs.CSL.2012.167</a>"},"doi":"10.4230/LIPIcs.CSL.2012.167","file_date_updated":"2020-07-14T12:46:35Z","_id":"497","ddc":["004"],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","image":"/images/cc_by_nc_nd.png","short":"CC BY-NC-ND (4.0)","name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)"},"abstract":[{"lang":"eng","text":"One central issue in the formal design and analysis of reactive systems is the notion of refinement that asks whether all behaviors of the implementation is allowed by the specification. The local interpretation of behavior leads to the notion of simulation. Alternating transition systems (ATSs) provide a general model for composite reactive systems, and the simulation relation for ATSs is known as alternating simulation. The simulation relation for fair transition systems is called fair simulation. In this work our main contributions are as follows: (1) We present an improved algorithm for fair simulation with Büchi fairness constraints; our algorithm requires O(n 3·m) time as compared to the previous known O(n 6)-time algorithm, where n is the number of states and m is the number of transitions. (2) We present a game based algorithm for alternating simulation that requires O(m2)-time as compared to the previous known O((n·m)2)-time algorithm, where n is the number of states and m is the size of transition relation. (3) We present an iterative algorithm for alternating simulation that matches the time complexity of the game based algorithm, but is more space efficient than the game based algorithm. © Krishnendu Chatterjee, Siddhesh Chaubal, and Pritish Kamath."}],"publication_status":"published","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_published":"2012-09-01T00:00:00Z","department":[{"_id":"KrCh"}],"page":"167 - 182","volume":16,"quality_controlled":"1","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"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"}]},{"file_date_updated":"2020-07-14T12:46:38Z","_id":"5377","language":[{"iso":"eng"}],"doi":"10.15479/AT:IST-2012-0002","citation":{"apa":"Chatterjee, K., &#38; Velner, Y. (2012). <i>Mean-payoff pushdown games</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2012-0002\">https://doi.org/10.15479/AT:IST-2012-0002</a>","chicago":"Chatterjee, Krishnendu, and Yaron Velner. <i>Mean-Payoff Pushdown Games</i>. IST Austria, 2012. <a href=\"https://doi.org/10.15479/AT:IST-2012-0002\">https://doi.org/10.15479/AT:IST-2012-0002</a>.","ista":"Chatterjee K, Velner Y. 2012. Mean-payoff pushdown games, IST Austria, 33p.","mla":"Chatterjee, Krishnendu, and Yaron Velner. <i>Mean-Payoff Pushdown Games</i>. IST Austria, 2012, doi:<a href=\"https://doi.org/10.15479/AT:IST-2012-0002\">10.15479/AT:IST-2012-0002</a>.","short":"K. Chatterjee, Y. Velner, Mean-Payoff Pushdown Games, IST Austria, 2012.","ama":"Chatterjee K, Velner Y. <i>Mean-Payoff Pushdown Games</i>. IST Austria; 2012. doi:<a href=\"https://doi.org/10.15479/AT:IST-2012-0002\">10.15479/AT:IST-2012-0002</a>","ieee":"K. Chatterjee and Y. Velner, <i>Mean-payoff pushdown games</i>. IST Austria, 2012."},"date_created":"2018-12-12T11:38:59Z","title":"Mean-payoff pushdown games","pubrep_id":"10","date_updated":"2023-02-23T11:05:50Z","oa":1,"year":"2012","has_accepted_license":"1","related_material":{"record":[{"id":"2956","relation":"later_version","status":"public"}]},"department":[{"_id":"KrCh"}],"page":"33","alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","status":"public","date_published":"2012-07-02T00:00:00Z","type":"technical_report","publication_status":"published","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Velner","first_name":"Yaron","full_name":"Velner, Yaron"}],"oa_version":"Published Version","day":"02","file":[{"creator":"system","access_level":"open_access","content_type":"application/pdf","relation":"main_file","file_size":592098,"file_name":"IST-2012-002_IST-2012-0002.pdf","checksum":"a03c08c1589dbb0c96183a8bcf3ab240","file_id":"5522","date_created":"2018-12-12T11:54:00Z","date_updated":"2020-07-14T12:46:38Z"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","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 ω-regular 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 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"}],"ddc":["000","005"],"publication_identifier":{"issn":["2664-1690"]},"month":"07"},{"department":[{"_id":"KrCh"}],"page":"21","alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","date_published":"2012-07-04T00:00:00Z","status":"public","type":"technical_report","oa_version":"Published Version","day":"04","abstract":[{"text":"One central issue in the formal design and analysis of reactive systems is the notion of refinement that asks whether all behaviors of the implementation is allowed by the specification. The local interpretation of behavior leads to the notion of simulation. Alternating transition systems (ATSs) provide a general model for composite reactive systems, and the simulation relation for ATSs is known as alternating simulation. The simulation relation for fair transition systems is called fair simulation. In this work our main contributions are as follows: (1) We present an improved algorithm for fair simulation with Büchi fairness constraints; our algorithm requires O(n3 · m) time as compared to the previous known O(n6)-time algorithm, where n is the number of states and m is the number of transitions. (2) We present a game based algorithm for alternating simulation that requires O(m2)-time as compared to the previous known O((n · m)2)-time algorithm, where n is the number of states and m is the size of transition relation. (3) We present an iterative algorithm for alternating simulation that matches the time complexity of the game based algorithm, but is more space efficient than the game based algorithm.","lang":"eng"}],"file":[{"creator":"system","access_level":"open_access","content_type":"application/pdf","file_size":394256,"relation":"main_file","checksum":"ec8d1857cc7095d3de5107a0162ced37","file_name":"IST-2012-0001_IST-2012-0001.pdf","file_id":"5489","date_created":"2018-12-12T11:53:28Z","date_updated":"2020-07-14T12:46:39Z"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000","005"],"publication_identifier":{"issn":["2664-1690"]},"month":"07","publication_status":"published","author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"full_name":"Chaubal, Siddhesh","first_name":"Siddhesh","last_name":"Chaubal"},{"full_name":"Kamath, Pritish","first_name":"Pritish","last_name":"Kamath"}],"doi":"10.15479/AT:IST-2012-0001","file_date_updated":"2020-07-14T12:46:39Z","_id":"5378","language":[{"iso":"eng"}],"related_material":{"record":[{"status":"public","id":"497","relation":"later_version"}]},"has_accepted_license":"1","date_created":"2018-12-12T11:38:59Z","title":"Faster algorithms for alternating refinement relations","citation":{"apa":"Chatterjee, K., Chaubal, S., &#38; Kamath, P. (2012). <i>Faster algorithms for alternating refinement relations</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2012-0001\">https://doi.org/10.15479/AT:IST-2012-0001</a>","mla":"Chatterjee, Krishnendu, et al. <i>Faster Algorithms for Alternating Refinement Relations</i>. IST Austria, 2012, doi:<a href=\"https://doi.org/10.15479/AT:IST-2012-0001\">10.15479/AT:IST-2012-0001</a>.","ista":"Chatterjee K, Chaubal S, Kamath P. 2012. Faster algorithms for alternating refinement relations, IST Austria, 21p.","chicago":"Chatterjee, Krishnendu, Siddhesh Chaubal, and Pritish Kamath. <i>Faster Algorithms for Alternating Refinement Relations</i>. IST Austria, 2012. <a href=\"https://doi.org/10.15479/AT:IST-2012-0001\">https://doi.org/10.15479/AT:IST-2012-0001</a>.","short":"K. Chatterjee, S. Chaubal, P. Kamath, Faster Algorithms for Alternating Refinement Relations, IST Austria, 2012.","ieee":"K. Chatterjee, S. Chaubal, and P. Kamath, <i>Faster algorithms for alternating refinement relations</i>. IST Austria, 2012.","ama":"Chatterjee K, Chaubal S, Kamath P. <i>Faster Algorithms for Alternating Refinement Relations</i>. IST Austria; 2012. doi:<a href=\"https://doi.org/10.15479/AT:IST-2012-0001\">10.15479/AT:IST-2012-0001</a>"},"pubrep_id":"14","oa":1,"date_updated":"2023-02-23T12:21:38Z","year":"2012"},{"pubrep_id":"23","oa":1,"date_updated":"2023-02-23T11:23:11Z","year":"2011","citation":{"apa":"Chatterjee, K., &#38; Doyen, L. (2011). <i>Energy and mean-payoff parity Markov decision processes</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2011-0001\">https://doi.org/10.15479/AT:IST-2011-0001</a>","chicago":"Chatterjee, Krishnendu, and Laurent Doyen. <i>Energy and Mean-Payoff Parity Markov Decision Processes</i>. IST Austria, 2011. <a href=\"https://doi.org/10.15479/AT:IST-2011-0001\">https://doi.org/10.15479/AT:IST-2011-0001</a>.","mla":"Chatterjee, Krishnendu, and Laurent Doyen. <i>Energy and Mean-Payoff Parity Markov Decision Processes</i>. IST Austria, 2011, doi:<a href=\"https://doi.org/10.15479/AT:IST-2011-0001\">10.15479/AT:IST-2011-0001</a>.","ista":"Chatterjee K, Doyen L. 2011. Energy and mean-payoff parity Markov decision processes, IST Austria, 20p.","ieee":"K. Chatterjee and L. Doyen, <i>Energy and mean-payoff parity Markov decision processes</i>. IST Austria, 2011.","ama":"Chatterjee K, Doyen L. <i>Energy and Mean-Payoff Parity Markov Decision Processes</i>. IST Austria; 2011. doi:<a href=\"https://doi.org/10.15479/AT:IST-2011-0001\">10.15479/AT:IST-2011-0001</a>","short":"K. Chatterjee, L. Doyen, Energy and Mean-Payoff Parity Markov Decision Processes, IST Austria, 2011."},"date_created":"2018-12-12T11:39:02Z","title":"Energy and mean-payoff parity Markov decision processes","has_accepted_license":"1","related_material":{"record":[{"status":"public","relation":"later_version","id":"3345"}]},"file_date_updated":"2020-07-14T12:46:41Z","_id":"5387","language":[{"iso":"eng"}],"doi":"10.15479/AT:IST-2011-0001","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"}],"publication_status":"published","ddc":["000","005"],"publication_identifier":{"issn":["2664-1690"]},"month":"02","oa_version":"Published Version","day":"16","file":[{"date_updated":"2020-07-14T12:46:41Z","date_created":"2018-12-12T11:52:57Z","checksum":"824d6c70e6d3feb3e836b009e0b3cf73","file_id":"5458","file_name":"IST-2011-0001_IST-2011-0001.pdf","file_size":329976,"relation":"main_file","access_level":"open_access","content_type":"application/pdf","creator":"system"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"lang":"eng","text":"We consider Markov Decision Processes (MDPs) with mean-payoff parity and energy parity objectives. In system design, the parity objective is used to encode ω-regular specifications, and the mean-payoff and energy objectives can be used to model quantitative resource constraints. The energy condition re- quires that the resource level never drops below 0, and the mean-payoff condi- tion requires that the limit-average value of the resource consumption is within a threshold. While these two (energy and mean-payoff) classical conditions are equivalent for two-player games, we show that they differ for MDPs. We show that the problem of deciding whether a state is almost-sure winning (i.e., winning with probability 1) in energy parity MDPs is in NP ∩ coNP, while for mean- payoff parity MDPs, the problem is solvable in polynomial time, improving a recent PSPACE bound."}],"alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","status":"public","date_published":"2011-02-16T00:00:00Z","type":"technical_report","page":"20","department":[{"_id":"KrCh"}]},{"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"quality_controlled":"1","volume":7,"publisher":"International Federation of Computational Logic","license":"https://creativecommons.org/licenses/by-nd/4.0/","date_published":"2011-12-14T00:00:00Z","project":[{"call_identifier":"FP7","name":"COMponent-Based Embedded Systems design Techniques","grant_number":"215543","_id":"25EFB36C-B435-11E9-9278-68D0E5697425"}],"abstract":[{"text":"We consider two-player games played in real time on game structures with clocks where the objectives of players are described using parity conditions. The games are concurrent in that at each turn, both players independently propose a time delay and an action, and the action with the shorter delay is chosen. To prevent a player from winning by blocking time, we restrict each player to play strategies that ensure that the player cannot be responsible for causing a zeno run. First, we present an efficient reduction of these games to turn-based (i.e., not concurrent) finite-state (i.e., untimed) parity games. Our reduction improves the best known complexity for solving timed parity games. Moreover, the rich class of algorithms for classical parity games can now be applied to timed parity games. The states of the resulting game are based on clock regions of the original game, and the state space of the finite game is linear in the size of the region graph. Second, we consider two restricted classes of strategies for the player that represents the controller in a real-time synthesis problem, namely, limit-robust and bounded-robust winning strategies. Using a limit-robust winning strategy, the controller cannot choose an exact real-valued time delay but must allow for some nonzero jitter in each of its actions. If there is a given lower bound on the jitter, then the strategy is bounded-robust winning. We show that exact strategies are more powerful than limit-robust strategies, which are more powerful than bounded-robust winning strategies for any bound. For both kinds of robust strategies, we present efficient reductions to standard timed automaton games. These reductions provide algorithms for the synthesis of robust real-time controllers.","lang":"eng"}],"ddc":["000","005"],"tmp":{"image":"/image/cc_by_nd.png","legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","short":"CC BY-ND (4.0)"},"publication_status":"published","doi":"10.2168/LMCS-7(4:8)2011","file_date_updated":"2020-07-14T12:46:07Z","_id":"3315","ec_funded":1,"related_material":{"record":[{"relation":"earlier_version","id":"3876","status":"public"}]},"publist_id":"3324","citation":{"apa":"Chatterjee, K., Henzinger, T. A., &#38; Prabhu, V. (2011). Timed parity games: Complexity and robustness. <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic. <a href=\"https://doi.org/10.2168/LMCS-7(4:8)2011\">https://doi.org/10.2168/LMCS-7(4:8)2011</a>","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Vinayak Prabhu. “Timed Parity Games: Complexity and Robustness.” <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic, 2011. <a href=\"https://doi.org/10.2168/LMCS-7(4:8)2011\">https://doi.org/10.2168/LMCS-7(4:8)2011</a>.","ista":"Chatterjee K, Henzinger TA, Prabhu V. 2011. Timed parity games: Complexity and robustness. Logical Methods in Computer Science. 7(4).","mla":"Chatterjee, Krishnendu, et al. “Timed Parity Games: Complexity and Robustness.” <i>Logical Methods in Computer Science</i>, vol. 7, no. 4, International Federation of Computational Logic, 2011, doi:<a href=\"https://doi.org/10.2168/LMCS-7(4:8)2011\">10.2168/LMCS-7(4:8)2011</a>.","short":"K. Chatterjee, T.A. Henzinger, V. Prabhu, Logical Methods in Computer Science 7 (2011).","ama":"Chatterjee K, Henzinger TA, Prabhu V. Timed parity games: Complexity and robustness. <i>Logical Methods in Computer Science</i>. 2011;7(4). doi:<a href=\"https://doi.org/10.2168/LMCS-7(4:8)2011\">10.2168/LMCS-7(4:8)2011</a>","ieee":"K. Chatterjee, T. A. Henzinger, and V. Prabhu, “Timed parity games: Complexity and robustness,” <i>Logical Methods in Computer Science</i>, vol. 7, no. 4. International Federation of Computational Logic, 2011."},"date_created":"2018-12-11T12:02:37Z","year":"2011","status":"public","type":"journal_article","oa_version":"Published Version","day":"14","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","file":[{"access_level":"open_access","relation":"main_file","content_type":"application/pdf","file_size":588863,"creator":"system","date_created":"2018-12-12T10:16:42Z","date_updated":"2020-07-14T12:46:07Z","checksum":"3480e1594bbef25ff7462fa93a8a814e","file_name":"IST-2016-86-v2+1_1011.0688_3_.pdf","file_id":"5231"}],"month":"12","author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Prabhu","full_name":"Prabhu, Vinayak","first_name":"Vinayak"}],"publication":"Logical Methods in Computer Science","language":[{"iso":"eng"}],"has_accepted_license":"1","intvolume":"         7","scopus_import":1,"title":"Timed parity games: Complexity and robustness","date_updated":"2023-02-23T11:46:35Z","pubrep_id":"506","oa":1,"issue":"4"},{"date_published":"2011-07-14T00:00:00Z","publisher":"IEEE","quality_controlled":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"page":"176 - 185","project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S11402-N23","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"},{"name":"Design for Embedded Systems","call_identifier":"FP7","_id":"25F1337C-B435-11E9-9278-68D0E5697425","grant_number":"214373"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"abstract":[{"lang":"eng","text":"In addition to being correct, a system should be robust, that is, it should behave reasonably even after receiving unexpected inputs. In this paper, we summarize two formal notions of robustness that we have introduced previously for reactive systems. One of the notions is based on assigning costs for failures on a user-provided notion of incorrect transitions in a specification. Here, we define a system to be robust if a finite number of incorrect inputs does not lead to an infinite number of incorrect outputs. We also give a more refined notion of robustness that aims to minimize the ratio of output failures to input failures. The second notion is aimed at liveness. In contrast to the previous notion, it has no concept of recovery from an error. Instead, it compares the ratio of the number of liveness constraints that the system violates to the number of liveness constraints that the environment violates."}],"publication_status":"published","doi":"10.1109/SIES.2011.5953660","_id":"3316","ec_funded":1,"year":"2011","publist_id":"3323","date_created":"2018-12-11T12:02:38Z","citation":{"chicago":"Bloem, Roderick, Krishnendu Chatterjee, Karin Greimel, Thomas A Henzinger, and Barbara Jobstmann. “Specification-Centered Robustness.” In <i>6th IEEE International Symposium on Industrial and Embedded Systems</i>, 176–85. IEEE, 2011. <a href=\"https://doi.org/10.1109/SIES.2011.5953660\">https://doi.org/10.1109/SIES.2011.5953660</a>.","mla":"Bloem, Roderick, et al. “Specification-Centered Robustness.” <i>6th IEEE International Symposium on Industrial and Embedded Systems</i>, IEEE, 2011, pp. 176–85, doi:<a href=\"https://doi.org/10.1109/SIES.2011.5953660\">10.1109/SIES.2011.5953660</a>.","ista":"Bloem R, Chatterjee K, Greimel K, Henzinger TA, Jobstmann B. 2011. Specification-centered robustness. 6th IEEE International Symposium on Industrial and Embedded Systems.  SIES: International Symposium on Industrial Embedded Systems, 176–185.","ieee":"R. Bloem, K. Chatterjee, K. Greimel, T. A. Henzinger, and B. Jobstmann, “Specification-centered robustness,” in <i>6th IEEE International Symposium on Industrial and Embedded Systems</i>, Vasteras, Sweden, 2011, pp. 176–185.","ama":"Bloem R, Chatterjee K, Greimel K, Henzinger TA, Jobstmann B. Specification-centered robustness. In: <i>6th IEEE International Symposium on Industrial and Embedded Systems</i>. IEEE; 2011:176-185. doi:<a href=\"https://doi.org/10.1109/SIES.2011.5953660\">10.1109/SIES.2011.5953660</a>","short":"R. Bloem, K. Chatterjee, K. Greimel, T.A. Henzinger, B. Jobstmann, in:, 6th IEEE International Symposium on Industrial and Embedded Systems, IEEE, 2011, pp. 176–185.","apa":"Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T. A., &#38; Jobstmann, B. (2011). Specification-centered robustness. In <i>6th IEEE International Symposium on Industrial and Embedded Systems</i> (pp. 176–185). Vasteras, Sweden: IEEE. <a href=\"https://doi.org/10.1109/SIES.2011.5953660\">https://doi.org/10.1109/SIES.2011.5953660</a>"},"status":"public","type":"conference","month":"07","conference":{"location":"Vasteras, Sweden","end_date":"2011-06-17","name":" SIES: International Symposium on Industrial Embedded Systems","start_date":"2011-06-15"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"14","main_file_link":[{"open_access":"1","url":"https://openlib.tugraz.at/download.php?id=5cb57c8a49344&location=browse"}],"oa_version":"Published Version","author":[{"full_name":"Bloem, Roderick","first_name":"Roderick","last_name":"Bloem"},{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"last_name":"Greimel","first_name":"Karin","full_name":"Greimel, Karin"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Jobstmann","first_name":"Barbara","full_name":"Jobstmann, Barbara"}],"publication":"6th IEEE International Symposium on Industrial and Embedded Systems","language":[{"iso":"eng"}],"scopus_import":1,"article_processing_charge":"No","oa":1,"date_updated":"2021-01-12T07:42:36Z","title":"Specification-centered robustness"},{"publication":"arXiv","language":[{"iso":"eng"}],"_id":"3338","related_material":{"record":[{"relation":"earlier_version","id":"5380","status":"public"}]},"title":"Bounded rationality in concurrent parity games","publist_id":"3287","date_created":"2018-12-11T12:02:45Z","citation":{"chicago":"Chatterjee, Krishnendu. “Bounded Rationality in Concurrent Parity Games.” <i>ArXiv</i>. ArXiv, 2011.","mla":"Chatterjee, Krishnendu. “Bounded Rationality in Concurrent Parity Games.” <i>ArXiv</i>, ArXiv, 2011, pp. 1–51.","ista":"Chatterjee K. 2011. Bounded rationality in concurrent parity games. arXiv, 1–51, .","short":"K. Chatterjee, ArXiv (2011) 1–51.","ama":"Chatterjee K. Bounded rationality in concurrent parity games. <i>arXiv</i>. 2011:1-51.","ieee":"K. Chatterjee, “Bounded rationality in concurrent parity games,” <i>arXiv</i>. ArXiv, pp. 1–51, 2011.","apa":"Chatterjee, K. (2011). Bounded rationality in concurrent parity games. <i>arXiv</i>. ArXiv."},"oa":1,"date_updated":"2023-02-23T12:23:40Z","year":"2011","page":"1 - 51","department":[{"_id":"KrCh"}],"publisher":"ArXiv","status":"public","date_published":"2011-07-11T00:00:00Z","type":"preprint","main_file_link":[{"url":"http://arxiv.org/abs/1107.2146","open_access":"1"}],"oa_version":"Preprint","external_id":{"arxiv":["1107.2146"]},"day":"11","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"lang":"eng","text":"We consider 2-player games played on a finite state space for an infinite number of rounds. The games are concurrent: in each round, the two players (player 1 and player 2) choose their moves inde- pendently and simultaneously; the current state and the two moves determine the successor state. We study concurrent games with ω-regular winning conditions specified as parity objectives. We consider the qualitative analysis problems: the computation of the almost-sure and limit-sure winning set of states, where player 1 can ensure to win with probability 1 and with probability arbitrarily close to 1, respec- tively. In general the almost-sure and limit-sure winning strategies require both infinite-memory as well as infinite-precision (to describe probabilities). We study the bounded-rationality problem for qualitative analysis of concurrent parity games, where the strategy set for player 1 is restricted to bounded-resource strategies. In terms of precision, strategies can be deterministic, uniform, finite-precision or infinite- precision; and in terms of memory, strategies can be memoryless, finite-memory or infinite-memory. We present a precise and complete characterization of the qualitative winning sets for all combinations of classes of strategies. In particular, we show that uniform memoryless strategies are as powerful as finite-precision infinite-memory strategies, and infinite-precision memoryless strategies are as power- ful as infinite-precision finite-memory strategies. We show that the winning sets can be computed in O(n2d+3) time, where n is the size of the game structure and 2d is the number of priorities (or colors), and our algorithms are symbolic. The membership problem of whether a state belongs to a winning set can be decided in NP ∩ coNP. While this complexity is the same as for the simpler class of turn-based parity games, where in each state only one of the two players has a choice of moves, our algorithms, that are obtained by characterization of the winning sets as μ-calculus formulas, are considerably more involved than those for turn-based games."}],"month":"07","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"}],"publication_status":"published","arxiv":1},{"_id":"3339","language":[{"iso":"eng"}],"publication":"arXiv","date_updated":"2021-01-12T07:42:46Z","oa":1,"year":"2011","date_created":"2018-12-11T12:02:46Z","citation":{"chicago":"Chatterjee, Krishnendu, Luca De Alfaro, and Roy Pritam. “Magnifying Lens Abstraction for Stochastic Games with Discounted and Long-Run Average Objectives.” <i>ArXiv</i>. ArXiv, 2011.","ista":"Chatterjee K, De Alfaro L, Pritam R. 2011. Magnifying lens abstraction for stochastic games with discounted and long-run average objectives. arXiv, .","mla":"Chatterjee, Krishnendu, et al. “Magnifying Lens Abstraction for Stochastic Games with Discounted and Long-Run Average Objectives.” <i>ArXiv</i>, ArXiv, 2011.","ieee":"K. Chatterjee, L. De Alfaro, and R. Pritam, “Magnifying lens abstraction for stochastic games with discounted and long-run average objectives,” <i>arXiv</i>. ArXiv, 2011.","ama":"Chatterjee K, De Alfaro L, Pritam R. Magnifying lens abstraction for stochastic games with discounted and long-run average objectives. <i>arXiv</i>. 2011.","short":"K. Chatterjee, L. De Alfaro, R. Pritam, ArXiv (2011).","apa":"Chatterjee, K., De Alfaro, L., &#38; Pritam, R. (2011). Magnifying lens abstraction for stochastic games with discounted and long-run average objectives. <i>arXiv</i>. ArXiv."},"title":"Magnifying lens abstraction for stochastic games with discounted and long-run average objectives","publist_id":"3286","publisher":"ArXiv","type":"preprint","status":"public","date_published":"2011-07-11T00:00:00Z","page":"17","department":[{"_id":"KrCh"}],"publication_status":"published","author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"last_name":"De Alfaro","first_name":"Luca","full_name":"De Alfaro, Luca"},{"first_name":"Roy","full_name":"Pritam, Roy","last_name":"Pritam"}],"arxiv":1,"month":"07","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1107.2132"}],"day":"11","oa_version":"Preprint","external_id":{"arxiv":["1107.2132"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"lang":"eng","text":"Turn-based stochastic games and its important subclass Markov decision processes (MDPs) provide models for systems with both probabilistic and nondeterministic behaviors. We consider turn-based stochastic games with two classical quantitative objectives: discounted-sum and long-run average objectives. The game models and the quantitative objectives are widely used in probabilistic verification, planning, optimal inventory control, network protocol and performance analysis. Games and MDPs that model realistic systems often have very large state spaces, and probabilistic abstraction techniques are necessary to handle the state-space explosion. The commonly used full-abstraction techniques do not yield space-savings for systems that have many states with similar value, but does not necessarily have similar transition structure. A semi-abstraction technique, namely Magnifying-lens abstractions (MLA), that clusters states based on value only, disregarding differences in their transition relation was proposed for qualitative objectives (reachability and safety objectives). In this paper we extend the MLA technique to solve stochastic games with discounted-sum and long-run average objectives. We present the MLA technique based abstraction-refinement algorithm for stochastic games and MDPs with discounted-sum objectives. For long-run average objectives, our solution works for all MDPs and a sub-class of stochastic games where every state has the same value. "}]}]