[{"month":"09","oa":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"project":[{"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"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","doi":"10.1371/journal.pcbi.1003818","language":[{"iso":"eng"}],"article_number":"7p","publist_id":"5012","ec_funded":1,"file_date_updated":"2020-07-14T12:45:26Z","license":"https://creativecommons.org/licenses/by/4.0/","year":"2014","department":[{"_id":"KrCh"}],"publisher":"Public Library of Science","publication_status":"published","related_material":{"record":[{"id":"9739","relation":"research_data","status":"public"}]},"author":[{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","first_name":"Andreas","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas"},{"full_name":"Adlam, Ben","first_name":"Ben","last_name":"Adlam"},{"first_name":"Martin","last_name":"Nowak","full_name":"Nowak, Martin"}],"volume":10,"date_created":"2018-12-11T11:55:22Z","date_updated":"2023-02-23T14:06:36Z","scopus_import":1,"has_accepted_license":"1","day":"11","citation":{"short":"K. Chatterjee, A. Pavlogiannis, B. Adlam, M. Nowak, PLoS Computational Biology 10 (2014).","mla":"Chatterjee, Krishnendu, et al. “The Time Scale of Evolutionary Innovation.” PLoS Computational Biology, vol. 10, no. 9, 7p, Public Library of Science, 2014, doi:10.1371/journal.pcbi.1003818.","chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, Ben Adlam, and Martin Nowak. “The Time Scale of Evolutionary Innovation.” PLoS Computational Biology. Public Library of Science, 2014. https://doi.org/10.1371/journal.pcbi.1003818.","ama":"Chatterjee K, Pavlogiannis A, Adlam B, Nowak M. The time scale of evolutionary innovation. PLoS Computational Biology. 2014;10(9). doi:10.1371/journal.pcbi.1003818","ieee":"K. Chatterjee, A. Pavlogiannis, B. Adlam, and M. Nowak, “The time scale of evolutionary innovation,” PLoS Computational Biology, vol. 10, no. 9. Public Library of Science, 2014.","apa":"Chatterjee, K., Pavlogiannis, A., Adlam, B., & Nowak, M. (2014). The time scale of evolutionary innovation. PLoS Computational Biology. Public Library of Science. https://doi.org/10.1371/journal.pcbi.1003818","ista":"Chatterjee K, Pavlogiannis A, Adlam B, Nowak M. 2014. The time scale of evolutionary innovation. PLoS Computational Biology. 10(9), 7p."},"publication":"PLoS Computational Biology","date_published":"2014-09-11T00:00:00Z","type":"journal_article","issue":"9","abstract":[{"text":"A fundamental question in biology is the following: what is the time scale that is needed for evolutionary innovations? There are many results that characterize single steps in terms of the fixation time of new mutants arising in populations of certain size and structure. But here we ask a different question, which is concerned with the much longer time scale of evolutionary trajectories: how long does it take for a population exploring a fitness landscape to find target sequences that encode new biological functions? Our key variable is the length, (Formula presented.) of the genetic sequence that undergoes adaptation. In computer science there is a crucial distinction between problems that require algorithms which take polynomial or exponential time. The latter are considered to be intractable. Here we develop a theoretical approach that allows us to estimate the time of evolution as function of (Formula presented.) We show that adaptation on many fitness landscapes takes time that is exponential in (Formula presented.) even if there are broad selection gradients and many targets uniformly distributed in sequence space. These negative results lead us to search for specific mechanisms that allow evolution to work on polynomial time scales. We study a regeneration process and show that it enables evolution to work in polynomial time.","lang":"eng"}],"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","_id":"2039","intvolume":" 10","status":"public","title":"The time scale of evolutionary innovation","ddc":["510"],"pubrep_id":"440","file":[{"access_level":"open_access","file_name":"IST-2016-440-v1+1_journal.pcbi.1003818.pdf","content_type":"application/pdf","file_size":1399093,"creator":"system","relation":"main_file","file_id":"4890","checksum":"712d4c5787ddf97809cfc962507f0738","date_updated":"2020-07-14T12:45:26Z","date_created":"2018-12-12T10:11:35Z"}],"oa_version":"Published Version"},{"citation":{"mla":"Chatterjee, Krishnendu, et al. Detailed Proofs for “The Time Scale of Evolutionary Innovation.” Public Library of Science, 2014, doi:10.1371/journal.pcbi.1003818.s001.","short":"K. Chatterjee, A. Pavlogiannis, B. Adlam, M. Novak, (2014).","chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, Ben Adlam, and Martin Novak. “Detailed Proofs for ‘The Time Scale of Evolutionary Innovation.’” Public Library of Science, 2014. https://doi.org/10.1371/journal.pcbi.1003818.s001.","ama":"Chatterjee K, Pavlogiannis A, Adlam B, Novak M. Detailed proofs for “The time scale of evolutionary innovation.” 2014. doi:10.1371/journal.pcbi.1003818.s001","ista":"Chatterjee K, Pavlogiannis A, Adlam B, Novak M. 2014. Detailed proofs for “The time scale of evolutionary innovation”, Public Library of Science, 10.1371/journal.pcbi.1003818.s001.","apa":"Chatterjee, K., Pavlogiannis, A., Adlam, B., & Novak, M. (2014). Detailed proofs for “The time scale of evolutionary innovation.” Public Library of Science. https://doi.org/10.1371/journal.pcbi.1003818.s001","ieee":"K. Chatterjee, A. Pavlogiannis, B. Adlam, and M. Novak, “Detailed proofs for ‘The time scale of evolutionary innovation.’” Public Library of Science, 2014."},"doi":"10.1371/journal.pcbi.1003818.s001","date_published":"2014-09-11T00:00:00Z","article_processing_charge":"No","month":"09","day":"11","year":"2014","_id":"9739","user_id":"6785fbc1-c503-11eb-8a32-93094b40e1cf","publisher":"Public Library of Science","department":[{"_id":"KrCh"}],"title":"Detailed proofs for “The time scale of evolutionary innovation”","status":"public","related_material":{"record":[{"status":"public","relation":"used_in_publication","id":"2039"}]},"author":[{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"first_name":"Andreas","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas"},{"first_name":"Ben","last_name":"Adlam","full_name":"Adlam, Ben"},{"first_name":"Martin","last_name":"Novak","full_name":"Novak, Martin"}],"oa_version":"Published Version","date_updated":"2023-02-23T10:25:37Z","date_created":"2021-07-28T08:13:57Z","type":"research_data_reference"},{"type":"journal_article","issue":"3","abstract":[{"text":"Energy games belong to a class of turn-based two-player infinite-duration games played on a weighted directed graph. It is one of the rare and intriguing combinatorial problems that lie in NP∩co-NP, but are not known to be in P. The existence of polynomial-time algorithms has been a major open problem for decades and apart from pseudopolynomial algorithms there is no algorithm that solves any non-trivial subclass in polynomial time. In this paper, we give several results based on the weight structures of the graph. First, we identify a notion of penalty and present a polynomial-time algorithm when the penalty is large. Our algorithm is the first polynomial-time algorithm on a large class of weighted graphs. It includes several worst-case instances on which previous algorithms, such as value iteration and random facet algorithms, require at least sub-exponential time. Our main technique is developing the first non-trivial approximation algorithm and showing how to convert it to an exact algorithm. Moreover, we show that in a practical case in verification where weights are clustered around a constant number of values, the energy game problem can be solved in polynomial time. We also show that the problem is still as hard as in general when the clique-width is bounded or the graph is strongly ergodic, suggesting that restricting the graph structure does not necessarily help.","lang":"eng"}],"intvolume":" 70","title":"Polynomial-time algorithms for energy games with special weight structures","status":"public","user_id":"72615eeb-f1f3-11ec-aa25-d4573ddc34fd","_id":"535","oa_version":"Preprint","scopus_import":"1","article_processing_charge":"No","day":"01","page":"457 - 492","article_type":"original","citation":{"short":"K. Chatterjee, M.H. Henzinger, S. Krinninger, D. Nanongkai, Algorithmica 70 (2014) 457–492.","mla":"Chatterjee, Krishnendu, et al. “Polynomial-Time Algorithms for Energy Games with Special Weight Structures.” Algorithmica, vol. 70, no. 3, Springer, 2014, pp. 457–92, doi:10.1007/s00453-013-9843-7.","chicago":"Chatterjee, Krishnendu, Monika H Henzinger, Sebastian Krinninger, and Danupon Nanongkai. “Polynomial-Time Algorithms for Energy Games with Special Weight Structures.” Algorithmica. Springer, 2014. https://doi.org/10.1007/s00453-013-9843-7.","ama":"Chatterjee K, Henzinger MH, Krinninger S, Nanongkai D. Polynomial-time algorithms for energy games with special weight structures. Algorithmica. 2014;70(3):457-492. doi:10.1007/s00453-013-9843-7","apa":"Chatterjee, K., Henzinger, M. H., Krinninger, S., & Nanongkai, D. (2014). Polynomial-time algorithms for energy games with special weight structures. Algorithmica. Springer. https://doi.org/10.1007/s00453-013-9843-7","ieee":"K. Chatterjee, M. H. Henzinger, S. Krinninger, and D. Nanongkai, “Polynomial-time algorithms for energy games with special weight structures,” Algorithmica, vol. 70, no. 3. Springer, pp. 457–492, 2014.","ista":"Chatterjee K, Henzinger MH, Krinninger S, Nanongkai D. 2014. Polynomial-time algorithms for energy games with special weight structures. Algorithmica. 70(3), 457–492."},"publication":"Algorithmica","date_published":"2014-11-01T00:00:00Z","ec_funded":1,"publist_id":"7282","department":[{"_id":"KrCh"}],"publisher":"Springer","publication_status":"published","year":"2014","volume":70,"date_created":"2018-12-11T11:47:01Z","date_updated":"2023-09-05T14:09:29Z","related_material":{"record":[{"id":"10905","relation":"earlier_version","status":"public"}]},"author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Henzinger, Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","orcid":"0000-0002-5008-6530","first_name":"Monika H","last_name":"Henzinger"},{"full_name":"Krinninger, Sebastian","first_name":"Sebastian","last_name":"Krinninger"},{"first_name":"Danupon","last_name":"Nanongkai","full_name":"Nanongkai, Danupon"}],"month":"11","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","main_file_link":[{"url":"https://arxiv.org/abs/1604.08234","open_access":"1"}],"oa":1,"external_id":{"arxiv":["1604.08234"]},"language":[{"iso":"eng"}],"doi":"10.1007/s00453-013-9843-7"},{"oa_version":"None","volume":8559,"date_updated":"2023-09-07T11:58:33Z","date_created":"2018-12-11T11:55:30Z","related_material":{"record":[{"id":"5412","status":"public","relation":"earlier_version"},{"id":"5413","status":"public","relation":"earlier_version"},{"id":"5414","relation":"earlier_version","status":"public"},{"id":"1155","relation":"dissertation_contains","status":"public"}]},"author":[{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"last_name":"Chmelik","first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","full_name":"Chmelik, Martin"},{"last_name":"Daca","first_name":"Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87","full_name":"Daca, Przemyslaw"}],"publisher":"Springer","intvolume":" 8559","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publication_status":"published","status":"public","title":"CEGAR for qualitative analysis of probabilistic systems","_id":"2063","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2014","publist_id":"4978","ec_funded":1,"abstract":[{"text":"We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems.We focus on qualitative properties forMDPs that can express that desired behaviors of the system arise almost-surely (with probability 1) or with positive probability. We introduce a new simulation relation to capture the refinement relation ofMDPs with respect to qualitative properties, and present discrete graph theoretic algorithms with quadratic complexity to compute the simulation relation.We present an automated technique for assume-guarantee style reasoning for compositional analysis ofMDPs with qualitative properties by giving a counterexample guided abstraction-refinement approach to compute our new simulation relation. We have implemented our algorithms and show that the compositional analysis leads to significant improvements.","lang":"eng"}],"alternative_title":["LNCS"],"type":"conference","language":[{"iso":"eng"}],"doi":"10.1007/978-3-319-08867-9_31","date_published":"2014-07-01T00:00:00Z","conference":{"location":"Vienna, Austria","start_date":"2014-07-18","end_date":"2014-07-22","name":"CAV: Computer Aided Verification"},"project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","call_identifier":"FWF","name":"Game Theory"},{"call_identifier":"FWF","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"}],"page":"473 - 490","quality_controlled":"1","citation":{"ieee":"K. Chatterjee, M. Chmelik, and P. Daca, “CEGAR for qualitative analysis of probabilistic systems,” presented at the CAV: Computer Aided Verification, Vienna, Austria, 2014, vol. 8559, pp. 473–490.","apa":"Chatterjee, K., Chmelik, M., & Daca, P. (2014). CEGAR for qualitative analysis of probabilistic systems (Vol. 8559, pp. 473–490). Presented at the CAV: Computer Aided Verification, Vienna, Austria: Springer. https://doi.org/10.1007/978-3-319-08867-9_31","ista":"Chatterjee K, Chmelik M, Daca P. 2014. CEGAR for qualitative analysis of probabilistic systems. CAV: Computer Aided Verification, LNCS, vol. 8559, 473–490.","ama":"Chatterjee K, Chmelik M, Daca P. CEGAR for qualitative analysis of probabilistic systems. In: Vol 8559. Springer; 2014:473-490. doi:10.1007/978-3-319-08867-9_31","chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Przemyslaw Daca. “CEGAR for Qualitative Analysis of Probabilistic Systems,” 8559:473–90. Springer, 2014. https://doi.org/10.1007/978-3-319-08867-9_31.","short":"K. Chatterjee, M. Chmelik, P. Daca, in:, Springer, 2014, pp. 473–490.","mla":"Chatterjee, Krishnendu, et al. CEGAR for Qualitative Analysis of Probabilistic Systems. Vol. 8559, Springer, 2014, pp. 473–90, doi:10.1007/978-3-319-08867-9_31."},"month":"07","day":"01"},{"language":[{"iso":"eng"}],"date_published":"2014-12-05T00:00:00Z","doi":"10.15479/AT:IST-2014-315-v1-1","page":"26","oa":1,"citation":{"short":"K. Chatterjee, T.A. Henzinger, J. Otop, Y. Velner, Quantitative Fair Simulation Games, IST Austria, 2014.","mla":"Chatterjee, Krishnendu, et al. Quantitative Fair Simulation Games. IST Austria, 2014, doi:10.15479/AT:IST-2014-315-v1-1.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Yaron Velner. Quantitative Fair Simulation Games. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-315-v1-1.","ama":"Chatterjee K, Henzinger TA, Otop J, Velner Y. Quantitative Fair Simulation Games. IST Austria; 2014. doi:10.15479/AT:IST-2014-315-v1-1","ieee":"K. Chatterjee, T. A. Henzinger, J. Otop, and Y. Velner, Quantitative fair simulation games. IST Austria, 2014.","apa":"Chatterjee, K., Henzinger, T. A., Otop, J., & Velner, Y. (2014). Quantitative fair simulation games. IST Austria. https://doi.org/10.15479/AT:IST-2014-315-v1-1","ista":"Chatterjee K, Henzinger TA, Otop J, Velner Y. 2014. Quantitative fair simulation games, IST Austria, 26p."},"month":"12","day":"05","publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1","date_created":"2018-12-12T11:39:16Z","date_updated":"2023-09-20T12:07:48Z","file":[{"relation":"main_file","file_id":"5521","date_created":"2018-12-12T11:53:59Z","date_updated":"2020-07-14T12:46:52Z","checksum":"b1d573bc04365625ff9974880c0aa807","file_name":"IST-2014-315-v1+1_report.pdf","access_level":"open_access","content_type":"application/pdf","file_size":531046,"creator":"system"}],"oa_version":"Published Version","author":[{"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","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"},{"first_name":"Jan","last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan"},{"full_name":"Velner, Yaron","first_name":"Yaron","last_name":"Velner"}],"pubrep_id":"315","related_material":{"record":[{"relation":"later_version","status":"public","id":"1066"}]},"ddc":["004"],"publication_status":"published","status":"public","title":"Quantitative fair simulation games","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publisher":"IST Austria","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"5428","year":"2014","abstract":[{"text":"Simulation is an attractive alternative for language inclusion for automata as it is an under-approximation of language inclusion, but usually has much lower complexity. For non-deterministic automata, while language inclusion is PSPACE-complete, simulation can be computed in polynomial time. Simulation has also been extended in two orthogonal directions, namely, (1) fair simulation, for simulation over specified set of infinite runs; and (2) quantitative simulation, for simulation between weighted automata. Again, while fair trace inclusion is PSPACE-complete, fair simulation can be computed in polynomial time. For weighted automata, the (quantitative) language inclusion problem is undecidable for mean-payoff automata and the decidability is open for discounted-sum automata, whereas the (quantitative) simulation reduce to mean-payoff games and discounted-sum games, which admit pseudo-polynomial time algorithms.\r\n\r\nIn this work, we study (quantitative) simulation for weighted automata with Büchi acceptance conditions, i.e., we generalize fair simulation from non-weighted automata to weighted automata. We show that imposing Büchi acceptance conditions on weighted automata changes many fundamental properties of the simulation games. For example, whereas for mean-payoff and discounted-sum games, the players do not need memory to play optimally; we show in contrast that for simulation games with Büchi acceptance conditions, (i) for mean-payoff objectives, optimal strategies for both players require infinite memory in general, and (ii) for discounted-sum objectives, optimal strategies need not exist for both players. While the simulation games with Büchi acceptance conditions are more complicated (e.g., due to infinite-memory requirements for mean-payoff objectives) as compared to their counterpart without Büchi acceptance conditions, we still present pseudo-polynomial time algorithms to solve simulation games with Büchi acceptance conditions for both weighted mean-payoff and weighted discounted-sum automata.","lang":"eng"}],"file_date_updated":"2020-07-14T12:46:52Z","alternative_title":["IST Austria Technical Report"],"type":"technical_report"},{"page":"181 - 196","citation":{"apa":"Chatterjee, K., & Fijalkow, N. (2013). Infinite-state games with finitary conditions. In 22nd EACSL Annual Conference on Computer Science Logic (Vol. 23, pp. 181–196). Torino, Italy: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CSL.2013.181","ieee":"K. Chatterjee and N. Fijalkow, “Infinite-state games with finitary conditions,” in 22nd EACSL Annual Conference on Computer Science Logic, Torino, Italy, 2013, vol. 23, pp. 181–196.","ista":"Chatterjee K, Fijalkow N. 2013. Infinite-state games with finitary conditions. 22nd EACSL Annual Conference on Computer Science Logic. CSL: Computer Science LogicLeibniz International Proceedings in Informatics, LIPIcs, vol. 23, 181–196.","ama":"Chatterjee K, Fijalkow N. Infinite-state games with finitary conditions. In: 22nd EACSL Annual Conference on Computer Science Logic. Vol 23. Leibniz International Proceedings in Informatics. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2013:181-196. doi:10.4230/LIPIcs.CSL.2013.181","chicago":"Chatterjee, Krishnendu, and Nathanaël Fijalkow. “Infinite-State Games with Finitary Conditions.” In 22nd EACSL Annual Conference on Computer Science Logic, 23:181–96. Leibniz International Proceedings in Informatics. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013. https://doi.org/10.4230/LIPIcs.CSL.2013.181.","short":"K. Chatterjee, N. Fijalkow, in:, 22nd EACSL Annual Conference on Computer Science Logic, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013, pp. 181–196.","mla":"Chatterjee, Krishnendu, and Nathanaël Fijalkow. “Infinite-State Games with Finitary Conditions.” 22nd EACSL Annual Conference on Computer Science Logic, vol. 23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013, pp. 181–96, doi:10.4230/LIPIcs.CSL.2013.181."},"publication":"22nd EACSL Annual Conference on Computer Science Logic","date_published":"2013-09-01T00:00:00Z","series_title":"Leibniz International Proceedings in Informatics","scopus_import":1,"has_accepted_license":"1","day":"01","intvolume":" 23","title":"Infinite-state games with finitary conditions","status":"public","ddc":["000"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"1374","oa_version":"Published Version","file":[{"file_size":547296,"content_type":"application/pdf","creator":"system","file_name":"IST-2016-624-v1+1_ChKr_Infinite-state_games_2013_17.pdf","access_level":"open_access","date_updated":"2020-07-14T12:44:47Z","date_created":"2018-12-12T10:13:38Z","checksum":"b7091a3866db573c0db5ec486952255e","relation":"main_file","file_id":"5023"}],"pubrep_id":"624","alternative_title":["LIPIcs"],"type":"conference","abstract":[{"lang":"eng","text":"We study two-player zero-sum games over infinite-state graphs equipped with ωB and finitary conditions. Our first contribution is about the strategy complexity, i.e the memory required for winning strategies: we prove that over general infinite-state graphs, memoryless strategies are sufficient for finitary Büchi, and finite-memory suffices for finitary parity games. We then study pushdown games with boundedness conditions, with two contributions. First we prove a collapse result for pushdown games with ωB-conditions, implying the decidability of solving these games. Second we consider pushdown games with finitary parity along with stack boundedness conditions, and show that solving these games is EXPTIME-complete."}],"project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","call_identifier":"FWF","name":"Game Theory"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"quality_controlled":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"oa":1,"language":[{"iso":"eng"}],"doi":"10.4230/LIPIcs.CSL.2013.181","conference":{"start_date":"203-09-02","location":"Torino, Italy","end_date":"2013-09-05","name":"CSL: Computer Science Logic"},"month":"09","department":[{"_id":"KrCh"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","publication_status":"published","year":"2013","volume":23,"date_updated":"2021-01-12T06:50:14Z","date_created":"2018-12-11T11:51:39Z","author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Fijalkow, Nathanaël","last_name":"Fijalkow","first_name":"Nathanaël"}],"ec_funded":1,"publist_id":"5837","file_date_updated":"2020-07-14T12:44:47Z"},{"status":"public","title":"Multi-objective discounted reward verification in graphs and MDPs","intvolume":" 8312","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"2238","oa_version":"None","alternative_title":["LNCS"],"type":"conference","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"}],"page":"228 - 242","citation":{"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.","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.","short":"K. Chatterjee, V. Forejt, D. Wojtczak, 8312 (2013) 228–242.","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","ieee":"K. Chatterjee, V. Forejt, and D. Wojtczak, “Multi-objective discounted reward verification in graphs and MDPs,” vol. 8312. Springer, pp. 228–242, 2013.","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"},"date_published":"2013-12-01T00:00:00Z","series_title":"Lecture Notes in Computer Science","scopus_import":1,"day":"01","publication_status":"published","publisher":"Springer","department":[{"_id":"KrCh"}],"year":"2013","date_created":"2018-12-11T11:56:30Z","date_updated":"2020-08-11T10:09:42Z","volume":8312,"author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Forejt, Vojtěch","first_name":"Vojtěch","last_name":"Forejt"},{"last_name":"Wojtczak","first_name":"Dominik","full_name":"Wojtczak, Dominik"}],"ec_funded":1,"publist_id":"4723","quality_controlled":"1","project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"}],"language":[{"iso":"eng"}],"conference":{"name":"LPAR: Logic for Programming, Artificial Intelligence, and Reasoning","end_date":"2013-12-19","location":"Stellenbosch, South Africa","start_date":"2013-12-14"},"doi":"10.1007/978-3-642-45221-5_17","month":"12"},{"page":"VI - 854","quality_controlled":"1","citation":{"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.","short":"K. Chatterjee, J. Sgall, eds., Mathematical Foundations of Computer Science 2013, Springer, 2013.","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.","ieee":"K. Chatterjee and J. Sgall, Eds., Mathematical Foundations of Computer Science 2013, vol. 8087. Springer, 2013, p. VI-854.","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","ista":"Chatterjee K, Sgall J eds. 2013. Mathematical Foundations of Computer Science 2013, Springer,p.","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"},"language":[{"iso":"eng"}],"doi":"10.1007/978-3-642-40313-2","date_published":"2013-08-08T00:00:00Z","conference":{"name":"MFCS: Mathematical Foundations of Computer Science","start_date":"2013-08-26","location":"Klosterneuburg, Austria","end_date":"2013-08-30"},"series_title":"Lecture Notes in Computer Science","scopus_import":1,"publication_identifier":{"isbn":["978-3-642-40312-5"]},"month":"08","day":"08","department":[{"_id":"KrCh"}],"intvolume":" 8087","editor":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Jiri","last_name":"Sgall","full_name":"Sgall, Jiri"}],"publisher":"Springer","status":"public","publication_status":"published","title":"Mathematical Foundations of Computer Science 2013","_id":"2292","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2013","oa_version":"None","volume":8087,"date_created":"2018-12-11T11:56:48Z","date_updated":"2020-08-11T10:09:45Z","alternative_title":["LNCS"],"type":"conference_editor","publist_id":"4636","abstract":[{"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.","lang":"eng"}]},{"date_created":"2018-12-11T11:56:51Z","date_updated":"2021-01-12T06:56:37Z","volume":15,"author":[{"id":"5B547124-EB61-11E9-8887-89D9C04DBDF5","last_name":"Godhal","first_name":"Yashdeep","full_name":"Godhal, Yashdeep"},{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"}],"publication_status":"published","publisher":"Springer","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"year":"2013","file_date_updated":"2020-07-14T12:45:37Z","publist_id":"4629","language":[{"iso":"eng"}],"doi":"10.1007/s10009-011-0207-9","quality_controlled":"1","project":[{"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"}],"oa":1,"month":"10","file":[{"access_level":"open_access","file_name":"IST-2012-87-v1+1_Synthesis_of_AMBA_AHB_from_formal_specifications-_A_case_study.pdf","content_type":"application/pdf","file_size":277372,"creator":"system","relation":"main_file","file_id":"4910","checksum":"57b06a732dd8d6349190dba6b5b0d33b","date_created":"2018-12-12T10:11:53Z","date_updated":"2020-07-14T12:45:37Z"}],"oa_version":"Submitted Version","pubrep_id":"87","ddc":["000"],"title":"Synthesis of AMBA AHB from formal specification: A case study","status":"public","intvolume":" 15","_id":"2299","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"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.","lang":"eng"}],"issue":"5-6","type":"journal_article","date_published":"2013-10-01T00:00:00Z","page":"585 - 601","publication":"International Journal on Software Tools for Technology Transfer","citation":{"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","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.","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.","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","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.","short":"Y. Godhal, K. Chatterjee, T.A. Henzinger, International Journal on Software Tools for Technology Transfer 15 (2013) 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."},"day":"01","has_accepted_license":"1","scopus_import":1},{"date_updated":"2020-08-11T10:09:47Z","date_created":"2018-12-11T11:57:42Z","volume":8044,"author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"last_name":"Gaiser","first_name":"Andreas","full_name":"Gaiser, Andreas"},{"first_name":"Jan","last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan"}],"publication_status":"published","publisher":"Springer","department":[{"_id":"KrCh"}],"year":"2013","ec_funded":1,"publist_id":"4457","language":[{"iso":"eng"}],"conference":{"name":"CAV: Computer Aided Verification","start_date":"2013-07-13","location":"St. Petersburg, Russia","end_date":"2013-07-19"},"doi":"10.1007/978-3-642-39799-8_37","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"},{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory"},{"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"}],"oa":1,"main_file_link":[{"url":"http://arxiv.org/abs/1304.5281","open_access":"1"}],"external_id":{"arxiv":["1304.5281"]},"month":"07","oa_version":"Preprint","title":"Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis","status":"public","intvolume":" 8044","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"2446","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"}],"alternative_title":["LNCS"],"type":"conference","date_published":"2013-07-01T00:00:00Z","page":"559 - 575","citation":{"ista":"Chatterjee K, Gaiser A, Kretinsky J. 2013. Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. 8044, 559–575.","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.","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","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","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.","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.","short":"K. Chatterjee, A. Gaiser, J. Kretinsky, 8044 (2013) 559–575."},"day":"01","series_title":"Lecture Notes in Computer Science","scopus_import":1}]