[{"external_id":{"arxiv":["1201.2829"]},"date_updated":"2021-01-12T08:12:08Z","citation":{"short":"K. Chatterjee, Y. Velner, Journal of the ACM 64 (2017) 34.","mla":"Chatterjee, Krishnendu, and Yaron Velner. “The Complexity of Mean-Payoff Pushdown Games.” <i>Journal of the ACM</i>, vol. 64, no. 5, ACM, 2017, p. 34, doi:<a href=\"https://doi.org/10.1145/3121408\">10.1145/3121408</a>.","ista":"Chatterjee K, Velner Y. 2017. The complexity of mean-payoff pushdown games. Journal of the ACM. 64(5), 34.","apa":"Chatterjee, K., &#38; Velner, Y. (2017). The complexity of mean-payoff pushdown games. <i>Journal of the ACM</i>. ACM. <a href=\"https://doi.org/10.1145/3121408\">https://doi.org/10.1145/3121408</a>","ama":"Chatterjee K, Velner Y. The complexity of mean-payoff pushdown games. <i>Journal of the ACM</i>. 2017;64(5):34. doi:<a href=\"https://doi.org/10.1145/3121408\">10.1145/3121408</a>","ieee":"K. Chatterjee and Y. Velner, “The complexity of mean-payoff pushdown games,” <i>Journal of the ACM</i>, vol. 64, no. 5. ACM, p. 34, 2017.","chicago":"Chatterjee, Krishnendu, and Yaron Velner. “The Complexity of Mean-Payoff Pushdown Games.” <i>Journal of the ACM</i>. ACM, 2017. <a href=\"https://doi.org/10.1145/3121408\">https://doi.org/10.1145/3121408</a>."},"year":"2017","abstract":[{"lang":"eng","text":"Two-player games on graphs are central in many problems in formal verification and program analysis, such as synthesis and verification of open systems. In this work, we consider solving recursive game graphs (or pushdown game graphs) that 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, the mean-payoff objective. In pushdown games, two types of strategies are relevant: (1) global strategies, which depend on the entire global history; and (2) modular strategies, which have only local memory and thus do not depend on the context of invocation but rather 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 by 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."}],"doi":"10.1145/3121408","arxiv":1,"day":"01","volume":64,"author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Velner","first_name":"Yaron","full_name":"Velner, Yaron"}],"issue":"5","_id":"716","scopus_import":1,"title":"The complexity of mean-payoff pushdown games","intvolume":"        64","publication_status":"published","date_created":"2018-12-11T11:48:06Z","department":[{"_id":"KrCh"}],"page":"34","ec_funded":1,"quality_controlled":"1","article_type":"original","publisher":"ACM","date_published":"2017-09-01T00:00:00Z","type":"journal_article","oa":1,"publist_id":"6964","publication_identifier":{"issn":["00045411"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1201.2829"}],"publication":"Journal of the ACM","month":"09","oa_version":"Preprint","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"grant_number":"S11407","name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"language":[{"iso":"eng"}]},{"page":"236 - 259","ec_funded":1,"quality_controlled":"1","publisher":"Academic Press","_id":"717","scopus_import":1,"author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Velner","first_name":"Yaron","full_name":"Velner, Yaron"}],"publication_status":"published","date_created":"2018-12-11T11:48:07Z","department":[{"_id":"KrCh"}],"title":"Hyperplane separation technique for multidimensional mean-payoff games","intvolume":"        88","acknowledgement":"The research was supported by Austrian Science Fund (FWF) Grant No. P 23499-N23, FWF NFN Grant No. S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), Microsoft faculty fellows award, the RICH Model Toolkit (ICT COST Action IC0901), and was carried out in partial fulfillment of the requirements for the Ph.D. degree of the second author.","volume":88,"date_updated":"2023-02-23T10:38:15Z","year":"2017","citation":{"ieee":"K. Chatterjee and Y. Velner, “Hyperplane separation technique for multidimensional mean-payoff games,” <i>Journal of Computer and System Sciences</i>, vol. 88. Academic Press, pp. 236–259, 2017.","chicago":"Chatterjee, Krishnendu, and Yaron Velner. “Hyperplane Separation Technique for Multidimensional Mean-Payoff Games.” <i>Journal of Computer and System Sciences</i>. Academic Press, 2017. <a href=\"https://doi.org/10.1016/j.jcss.2017.04.005\">https://doi.org/10.1016/j.jcss.2017.04.005</a>.","apa":"Chatterjee, K., &#38; Velner, Y. (2017). Hyperplane separation technique for multidimensional mean-payoff games. <i>Journal of Computer and System Sciences</i>. Academic Press. <a href=\"https://doi.org/10.1016/j.jcss.2017.04.005\">https://doi.org/10.1016/j.jcss.2017.04.005</a>","ama":"Chatterjee K, Velner Y. Hyperplane separation technique for multidimensional mean-payoff games. <i>Journal of Computer and System Sciences</i>. 2017;88:236-259. doi:<a href=\"https://doi.org/10.1016/j.jcss.2017.04.005\">10.1016/j.jcss.2017.04.005</a>","ista":"Chatterjee K, Velner Y. 2017. Hyperplane separation technique for multidimensional mean-payoff games. Journal of Computer and System Sciences. 88, 236–259.","short":"K. Chatterjee, Y. Velner, Journal of Computer and System Sciences 88 (2017) 236–259.","mla":"Chatterjee, Krishnendu, and Yaron Velner. “Hyperplane Separation Technique for Multidimensional Mean-Payoff Games.” <i>Journal of Computer and System Sciences</i>, vol. 88, Academic Press, 2017, pp. 236–59, doi:<a href=\"https://doi.org/10.1016/j.jcss.2017.04.005\">10.1016/j.jcss.2017.04.005</a>."},"doi":"10.1016/j.jcss.2017.04.005","day":"01","abstract":[{"text":"We consider finite-state and recursive game graphs with multidimensional mean-payoff objectives. In recursive games two types of strategies are relevant: global strategies and modular strategies. Our contributions are: (1) We show that finite-state multidimensional mean-payoff games can be solved in polynomial time if the number of dimensions and the maximal absolute value of weights are fixed; whereas for arbitrary dimensions the problem is coNP-complete. (2) We show that one-player recursive games with multidimensional mean-payoff objectives can be solved in polynomial time. Both above algorithms are based on hyperplane separation technique. (3) For recursive games we show that under modular strategies the multidimensional problem is undecidable. We show that if the number of modules, exits, and the maximal absolute value of the weights are fixed, then one-dimensional recursive mean-payoff games under modular strategies can be solved in polynomial time, whereas for unbounded number of exits or modules the problem is NP-hard.","lang":"eng"}],"language":[{"iso":"eng"}],"publication":"Journal of Computer and System Sciences","oa_version":"Preprint","project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory","grant_number":"S11407"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"month":"09","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1210.3141"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"id":"2329","relation":"earlier_version","status":"public"}]},"status":"public","date_published":"2017-09-01T00:00:00Z","type":"journal_article","oa":1,"publist_id":"6963"},{"department":[{"_id":"KrCh"}],"date_created":"2018-12-11T11:48:07Z","publication_status":"published","oa_version":"None","intvolume":"        54","title":"Special issue: Synthesis and SYNT 2014","month":"09","scopus_import":1,"_id":"719","publication":"Acta Informatica","issue":"6","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"},{"full_name":"Ehlers, Rüdiger","first_name":"Rüdiger","last_name":"Ehlers"}],"publisher":"Springer","quality_controlled":"1","page":"543 - 544","language":[{"iso":"eng"}],"day":"01","publication_identifier":{"issn":["00015903"]},"doi":"10.1007/s00236-017-0299-0","publist_id":"6961","abstract":[{"lang":"eng","text":"The ubiquity of computation in modern machines and devices imposes a need to assert the correctness of their behavior. Especially in the case of safety-critical systems, their designers need to take measures that enforce their safe operation. Formal methods has emerged as a research field that addresses this challenge: by rigorously proving that all system executions adhere to their specifications, the correctness of an implementation under concern can be assured. To achieve this goal, a plethora of techniques are nowadays available, all of which are optimized for different system types and application domains."}],"year":"2017","citation":{"ista":"Chatterjee K, Ehlers R. 2017. Special issue: Synthesis and SYNT 2014. Acta Informatica. 54(6), 543–544.","short":"K. Chatterjee, R. Ehlers, Acta Informatica 54 (2017) 543–544.","mla":"Chatterjee, Krishnendu, and Rüdiger Ehlers. “Special Issue: Synthesis and SYNT 2014.” <i>Acta Informatica</i>, vol. 54, no. 6, Springer, 2017, pp. 543–44, doi:<a href=\"https://doi.org/10.1007/s00236-017-0299-0\">10.1007/s00236-017-0299-0</a>.","chicago":"Chatterjee, Krishnendu, and Rüdiger Ehlers. “Special Issue: Synthesis and SYNT 2014.” <i>Acta Informatica</i>. Springer, 2017. <a href=\"https://doi.org/10.1007/s00236-017-0299-0\">https://doi.org/10.1007/s00236-017-0299-0</a>.","ieee":"K. Chatterjee and R. Ehlers, “Special issue: Synthesis and SYNT 2014,” <i>Acta Informatica</i>, vol. 54, no. 6. Springer, pp. 543–544, 2017.","ama":"Chatterjee K, Ehlers R. Special issue: Synthesis and SYNT 2014. <i>Acta Informatica</i>. 2017;54(6):543-544. doi:<a href=\"https://doi.org/10.1007/s00236-017-0299-0\">10.1007/s00236-017-0299-0</a>","apa":"Chatterjee, K., &#38; Ehlers, R. (2017). Special issue: Synthesis and SYNT 2014. <i>Acta Informatica</i>. Springer. <a href=\"https://doi.org/10.1007/s00236-017-0299-0\">https://doi.org/10.1007/s00236-017-0299-0</a>"},"date_updated":"2021-01-12T08:12:18Z","type":"journal_article","date_published":"2017-09-01T00:00:00Z","volume":54,"status":"public","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87"},{"has_accepted_license":"1","publication":" Journal of Theoretical Biology","project":[{"name":"International IST Postdoc Fellowship Programme","grant_number":"291734","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"}],"oa_version":"Submitted Version","month":"11","language":[{"iso":"eng"}],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","short":"CC BY-NC-ND (4.0)","name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","image":"/images/cc_by_nc_nd.png"},"type":"journal_article","date_published":"2017-11-21T00:00:00Z","publication_identifier":{"issn":["00225193"]},"publist_id":"6923","oa":1,"file":[{"checksum":"4b43af1615ebf1a861840cb03d8a320c","file_size":537323,"date_created":"2019-11-19T07:57:39Z","content_type":"application/pdf","file_name":"2017_JournTheoretBio_Priklopil.pdf","date_updated":"2020-07-14T12:47:58Z","relation":"main_file","access_level":"open_access","creator":"dernst","file_id":"7047"}],"status":"public","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","scopus_import":"1","license":"https://creativecommons.org/licenses/by-nc-nd/4.0/","_id":"744","pmid":1,"author":[{"id":"3C869AA0-F248-11E8-B48F-1D18A9856A87","last_name":"Priklopil","first_name":"Tadeas","full_name":"Priklopil, Tadeas"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Nowak, Martin","last_name":"Nowak","first_name":"Martin"}],"article_processing_charge":"No","date_created":"2018-12-11T11:48:16Z","department":[{"_id":"KrCh"}],"publication_status":"published","intvolume":"       433","title":"Optional interactions and suspicious behaviour facilitates trustful cooperation in prisoners dilemma","ec_funded":1,"quality_controlled":"1","page":"64 - 72","file_date_updated":"2020-07-14T12:47:58Z","publisher":"Elsevier","article_type":"original","year":"2017","citation":{"apa":"Priklopil, T., Chatterjee, K., &#38; Nowak, M. (2017). Optional interactions and suspicious behaviour facilitates trustful cooperation in prisoners dilemma. <i> Journal of Theoretical Biology</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.jtbi.2017.08.025\">https://doi.org/10.1016/j.jtbi.2017.08.025</a>","ama":"Priklopil T, Chatterjee K, Nowak M. Optional interactions and suspicious behaviour facilitates trustful cooperation in prisoners dilemma. <i> Journal of Theoretical Biology</i>. 2017;433:64-72. doi:<a href=\"https://doi.org/10.1016/j.jtbi.2017.08.025\">10.1016/j.jtbi.2017.08.025</a>","ieee":"T. Priklopil, K. Chatterjee, and M. Nowak, “Optional interactions and suspicious behaviour facilitates trustful cooperation in prisoners dilemma,” <i> Journal of Theoretical Biology</i>, vol. 433. Elsevier, pp. 64–72, 2017.","chicago":"Priklopil, Tadeas, Krishnendu Chatterjee, and Martin Nowak. “Optional Interactions and Suspicious Behaviour Facilitates Trustful Cooperation in Prisoners Dilemma.” <i> Journal of Theoretical Biology</i>. Elsevier, 2017. <a href=\"https://doi.org/10.1016/j.jtbi.2017.08.025\">https://doi.org/10.1016/j.jtbi.2017.08.025</a>.","short":"T. Priklopil, K. Chatterjee, M. Nowak,  Journal of Theoretical Biology 433 (2017) 64–72.","mla":"Priklopil, Tadeas, et al. “Optional Interactions and Suspicious Behaviour Facilitates Trustful Cooperation in Prisoners Dilemma.” <i> Journal of Theoretical Biology</i>, vol. 433, Elsevier, 2017, pp. 64–72, doi:<a href=\"https://doi.org/10.1016/j.jtbi.2017.08.025\">10.1016/j.jtbi.2017.08.025</a>.","ista":"Priklopil T, Chatterjee K, Nowak M. 2017. Optional interactions and suspicious behaviour facilitates trustful cooperation in prisoners dilemma.  Journal of Theoretical Biology. 433, 64–72."},"date_updated":"2023-09-27T12:29:02Z","external_id":{"pmid":["28867224"],"isi":["000412039800007"]},"isi":1,"day":"21","doi":"10.1016/j.jtbi.2017.08.025","abstract":[{"text":"In evolutionary game theory interactions between individuals are often assumed obligatory. However, in many real-life situations, individuals can decide to opt out of an interaction depending on the information they have about the opponent. We consider a simple evolutionary game theoretic model to study such a scenario, where at each encounter between two individuals the type of the opponent (cooperator/defector) is known with some probability, and where each individual either accepts or opts out of the interaction. If the type of the opponent is unknown, a trustful individual accepts the interaction, whereas a suspicious individual opts out of the interaction. If either of the two individuals opt out both individuals remain without an interaction. We show that in the prisoners dilemma optional interactions along with suspicious behaviour facilitates the emergence of trustful cooperation.","lang":"eng"}],"volume":433,"ddc":["000","570"]},{"intvolume":"        13","title":"Improved algorithms for parity and Streett objectives","pubrep_id":"956","department":[{"_id":"KrCh"}],"article_processing_charge":"No","date_created":"2018-12-11T11:46:37Z","publication_status":"published","issue":"3","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"id":"540c9bbd-f2de-11ec-812d-d04a5be85630","first_name":"Monika H","last_name":"Henzinger","orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H"},{"full_name":"Loitzenbauer, Veronika","last_name":"Loitzenbauer","first_name":"Veronika"}],"license":"https://creativecommons.org/licenses/by-nd/4.0/","scopus_import":"1","_id":"464","publisher":"International Federation of Computational Logic","file_date_updated":"2020-07-14T12:46:32Z","ec_funded":1,"quality_controlled":"1","abstract":[{"lang":"eng","text":"The computation of the winning set for parity objectives and for Streett objectives in graphs as well as in game graphs are central problems in computer-aided verification, with application to the verification of closed systems with strong fairness conditions, the verification of open systems, checking interface compatibility, well-formedness of specifications, and the synthesis of reactive systems. We show how to compute the winning set on n vertices for (1) parity-3 (aka one-pair Streett) objectives in game graphs in time O(n5/2) and for (2) k-pair Streett objectives in graphs in time O(n2+nklogn). For both problems this gives faster algorithms for dense graphs and represents the first improvement in asymptotic running time in 15 years."}],"day":"26","arxiv":1,"doi":"10.23638/LMCS-13(3:26)2017","external_id":{"arxiv":["1410.0833"]},"citation":{"ama":"Chatterjee K, Henzinger MH, Loitzenbauer V. Improved algorithms for parity and Streett objectives. <i>Logical Methods in Computer Science</i>. 2017;13(3). doi:<a href=\"https://doi.org/10.23638/LMCS-13(3:26)2017\">10.23638/LMCS-13(3:26)2017</a>","apa":"Chatterjee, K., Henzinger, M. H., &#38; Loitzenbauer, V. (2017). Improved algorithms for parity and Streett objectives. <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic. <a href=\"https://doi.org/10.23638/LMCS-13(3:26)2017\">https://doi.org/10.23638/LMCS-13(3:26)2017</a>","ieee":"K. Chatterjee, M. H. Henzinger, and V. Loitzenbauer, “Improved algorithms for parity and Streett objectives,” <i>Logical Methods in Computer Science</i>, vol. 13, no. 3. International Federation of Computational Logic, 2017.","chicago":"Chatterjee, Krishnendu, Monika H Henzinger, and Veronika Loitzenbauer. “Improved Algorithms for Parity and Streett Objectives.” <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic, 2017. <a href=\"https://doi.org/10.23638/LMCS-13(3:26)2017\">https://doi.org/10.23638/LMCS-13(3:26)2017</a>.","mla":"Chatterjee, Krishnendu, et al. “Improved Algorithms for Parity and Streett Objectives.” <i>Logical Methods in Computer Science</i>, vol. 13, no. 3, 26, International Federation of Computational Logic, 2017, doi:<a href=\"https://doi.org/10.23638/LMCS-13(3:26)2017\">10.23638/LMCS-13(3:26)2017</a>.","short":"K. Chatterjee, M.H. Henzinger, V. Loitzenbauer, Logical Methods in Computer Science 13 (2017).","ista":"Chatterjee K, Henzinger MH, Loitzenbauer V. 2017. Improved algorithms for parity and Streett objectives. Logical Methods in Computer Science. 13(3), 26."},"year":"2017","date_updated":"2025-06-02T08:53:41Z","ddc":["004"],"volume":13,"article_number":"26","month":"09","project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Game Theory","grant_number":"S11407","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"}],"oa_version":"Published Version","has_accepted_license":"1","publication":"Logical Methods in Computer Science","language":[{"iso":"eng"}],"oa":1,"publist_id":"7357","publication_identifier":{"issn":["1860-5974"]},"type":"journal_article","date_published":"2017-09-26T00:00:00Z","tmp":{"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)","image":"/image/cc_by_nd.png","short":"CC BY-ND (4.0)"},"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"relation":"earlier_version","id":"1661","status":"public"}]},"file":[{"date_updated":"2020-07-14T12:46:32Z","content_type":"application/pdf","file_name":"IST-2018-956-v1+1_2017_Chatterjee_Improved_algorithms.pdf","date_created":"2018-12-12T10:13:27Z","checksum":"12d469ae69b80361333d7dead965cf5d","file_size":582940,"file_id":"5010","creator":"system","relation":"main_file","access_level":"open_access"}]},{"ddc":["004"],"volume":13,"abstract":[{"lang":"eng","text":"The edit distance between two words w 1 , w 2 is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform w 1 to w 2 . The edit distance generalizes to languages L 1 , L 2 , where the edit distance from L 1 to L 2 is the minimal number k such that for every word from L 1 there exists a word in L 2 with edit distance at most k . We study the edit distance computation problem between pushdown automata and their subclasses. The problem of computing edit distance to a pushdown automaton is undecidable, and in practice, the interesting question is to compute the edit distance from a pushdown automaton (the implementation, a standard model for programs with recursion) to a regular language (the specification). In this work, we present a complete picture of decidability and complexity for the following problems: (1) deciding whether, for a given threshold k , the edit distance from a pushdown automaton to a finite automaton is at most k , and (2) deciding whether the edit distance from a pushdown automaton to a finite automaton is finite. "}],"day":"13","doi":"10.23638/LMCS-13(3:23)2017","citation":{"ista":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2017. Edit distance for pushdown automata. Logical Methods in Computer Science. 13(3).","mla":"Chatterjee, Krishnendu, et al. “Edit Distance for Pushdown Automata.” <i>Logical Methods in Computer Science</i>, vol. 13, no. 3, International Federation of Computational Logic, 2017, doi:<a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">10.23638/LMCS-13(3:23)2017</a>.","short":"K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, Logical Methods in Computer Science 13 (2017).","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan Otop. “Edit Distance for Pushdown Automata.” <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic, 2017. <a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">https://doi.org/10.23638/LMCS-13(3:23)2017</a>.","ieee":"K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, “Edit distance for pushdown automata,” <i>Logical Methods in Computer Science</i>, vol. 13, no. 3. International Federation of Computational Logic, 2017.","apa":"Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., &#38; Otop, J. (2017). Edit distance for pushdown automata. <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic. <a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">https://doi.org/10.23638/LMCS-13(3:23)2017</a>","ama":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. Edit distance for pushdown automata. <i>Logical Methods in Computer Science</i>. 2017;13(3). doi:<a href=\"https://doi.org/10.23638/LMCS-13(3:23)2017\">10.23638/LMCS-13(3:23)2017</a>"},"year":"2017","date_updated":"2023-02-23T12:26:25Z","publisher":"International Federation of Computational Logic","file_date_updated":"2020-07-14T12:46:33Z","ec_funded":1,"quality_controlled":"1","intvolume":"        13","title":"Edit distance for pushdown automata","pubrep_id":"955","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"date_created":"2018-12-11T11:46:37Z","publication_status":"published","issue":"3","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","last_name":"Ibsen-Jensen"},{"full_name":"Otop, Jan","last_name":"Otop","first_name":"Jan"}],"scopus_import":1,"_id":"465","status":"public","related_material":{"record":[{"status":"public","id":"1610","relation":"earlier_version"},{"status":"public","relation":"earlier_version","id":"5438"}]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"checksum":"08041379ba408d40664f449eb5907a8f","file_size":279071,"date_created":"2018-12-12T10:14:37Z","content_type":"application/pdf","file_name":"IST-2015-321-v1+1_main.pdf","date_updated":"2020-07-14T12:46:33Z","relation":"main_file","access_level":"open_access","creator":"system","file_id":"5090"},{"relation":"main_file","access_level":"open_access","creator":"system","file_id":"5091","file_size":279071,"checksum":"08041379ba408d40664f449eb5907a8f","date_created":"2018-12-12T10:14:38Z","file_name":"IST-2018-955-v1+1_2017_Chatterjee_Edit_distance.pdf","content_type":"application/pdf","date_updated":"2020-07-14T12:46:33Z"}],"publist_id":"7356","oa":1,"publication_identifier":{"issn":["18605974"]},"type":"journal_article","date_published":"2017-09-13T00:00:00Z","tmp":{"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)","image":"/image/cc_by_nd.png","short":"CC BY-ND (4.0)"},"language":[{"iso":"eng"}],"month":"09","project":[{"call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23"},{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory"}],"oa_version":"Published Version","has_accepted_license":"1","publication":"Logical Methods in Computer Science"},{"abstract":[{"lang":"eng","text":"We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. There exist two different views: (i) the expectation semantics, where the goal is to optimize the expected mean-payoff objective, and (ii) the satisfaction semantics, where the goal is to maximize the probability of runs such that the mean-payoff value stays above a given vector. We consider optimization with respect to both objectives at once, thus unifying the existing semantics. Precisely, the goal is to optimize the expectation while ensuring the satisfaction constraint. Our problem captures the notion of optimization with respect to strategies that are risk-averse (i.e., ensure certain probabilistic guarantee). Our main results are as follows: First, we present algorithms for the decision problems which are always polynomial in the size of the MDP. We also show that an approximation of the Pareto-curve can be computed in time polynomial in the size of the MDP, and the approximation factor, but exponential in the number of dimensions. Second, we present a complete characterization of the strategy complexity (in terms of memory bounds and randomization) required to solve our problem. "}],"doi":"10.23638/LMCS-13(2:15)2017","day":"03","date_updated":"2023-02-23T12:26:16Z","year":"2017","citation":{"apa":"Chatterjee, K., Křetínská, Z., &#38; Kretinsky, J. (2017). Unifying two views on multiple mean-payoff objectives in Markov decision processes. <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic. <a href=\"https://doi.org/10.23638/LMCS-13(2:15)2017\">https://doi.org/10.23638/LMCS-13(2:15)2017</a>","ama":"Chatterjee K, Křetínská Z, Kretinsky J. Unifying two views on multiple mean-payoff objectives in Markov decision processes. <i>Logical Methods in Computer Science</i>. 2017;13(2). doi:<a href=\"https://doi.org/10.23638/LMCS-13(2:15)2017\">10.23638/LMCS-13(2:15)2017</a>","chicago":"Chatterjee, Krishnendu, Zuzana Křetínská, and Jan Kretinsky. “Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.” <i>Logical Methods in Computer Science</i>. International Federation of Computational Logic, 2017. <a href=\"https://doi.org/10.23638/LMCS-13(2:15)2017\">https://doi.org/10.23638/LMCS-13(2:15)2017</a>.","ieee":"K. Chatterjee, Z. Křetínská, and J. Kretinsky, “Unifying two views on multiple mean-payoff objectives in Markov decision processes,” <i>Logical Methods in Computer Science</i>, vol. 13, no. 2. International Federation of Computational Logic, 2017.","mla":"Chatterjee, Krishnendu, et al. “Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.” <i>Logical Methods in Computer Science</i>, vol. 13, no. 2, 15, International Federation of Computational Logic, 2017, doi:<a href=\"https://doi.org/10.23638/LMCS-13(2:15)2017\">10.23638/LMCS-13(2:15)2017</a>.","short":"K. Chatterjee, Z. Křetínská, J. Kretinsky, Logical Methods in Computer Science 13 (2017).","ista":"Chatterjee K, Křetínská Z, Kretinsky J. 2017. Unifying two views on multiple mean-payoff objectives in Markov decision processes. Logical Methods in Computer Science. 13(2), 15."},"ddc":["004"],"volume":13,"pubrep_id":"957","title":"Unifying two views on multiple mean-payoff objectives in Markov decision processes","intvolume":"        13","publication_status":"published","date_created":"2018-12-11T11:46:38Z","department":[{"_id":"KrCh"}],"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"first_name":"Zuzana","last_name":"Křetínská","full_name":"Křetínská, Zuzana"},{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","last_name":"Kretinsky","first_name":"Jan"}],"issue":"2","_id":"466","scopus_import":1,"publisher":"International Federation of Computational Logic","file_date_updated":"2020-07-14T12:46:33Z","ec_funded":1,"quality_controlled":"1","oa":1,"publist_id":"7355","publication_identifier":{"issn":["18605974"]},"date_published":"2017-07-03T00:00:00Z","type":"journal_article","tmp":{"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)","image":"/image/cc_by_nd.png","short":"CC BY-ND (4.0)"},"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"relation":"earlier_version","id":"1657","status":"public"},{"id":"5429","relation":"earlier_version","status":"public"},{"id":"5435","relation":"earlier_version","status":"public"}]},"file":[{"file_id":"5354","creator":"system","access_level":"open_access","relation":"main_file","date_updated":"2020-07-14T12:46:33Z","file_name":"IST-2018-957-v1+1_2017_Chatterjee_Unifying_two.pdf","content_type":"application/pdf","date_created":"2018-12-12T10:18:32Z","file_size":511832,"checksum":"bfa405385ec6229ad5ead89ab5751639"}],"month":"07","article_number":"15","oa_version":"Published Version","project":[{"name":"International IST Postdoc Fellowship Programme","grant_number":"291734","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425"},{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"_id":"2590DB08-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","name":"Atomic-Resolution Structures of Mitochondrial Respiratory Chain Supercomplexes (H2020)","grant_number":"701309"}],"publication":"Logical Methods in Computer Science","has_accepted_license":"1","language":[{"iso":"eng"}]},{"language":[{"iso":"eng"}],"oa_version":"Preprint","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"month":"12","article_number":"31","publication":"ACM Transactions on Computational Logic (TOCL)","main_file_link":[{"url":"https://arxiv.org/abs/1606.03598","open_access":"1"}],"related_material":{"record":[{"id":"1656","relation":"earlier_version","status":"public"},{"status":"public","relation":"earlier_version","id":"5415"},{"relation":"earlier_version","id":"5436","status":"public"}]},"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_identifier":{"issn":["15293785"]},"oa":1,"publist_id":"7354","date_published":"2017-12-01T00:00:00Z","type":"journal_article","publisher":"ACM","ec_funded":1,"quality_controlled":"1","publication_status":"published","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"date_created":"2018-12-11T11:46:38Z","title":"Nested weighted automata","intvolume":"        18","_id":"467","scopus_import":1,"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","full_name":"Otop, Jan","last_name":"Otop","first_name":"Jan"}],"issue":"4","volume":18,"doi":"10.1145/3152769","arxiv":1,"day":"01","abstract":[{"text":"Recently there has been a significant effort to handle quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, perhaps surprisingly, some basic system properties such as average response time cannot be expressed using weighted automata or in any other known decidable formalism. In this work, we introduce nested weighted automata as a natural extension of weighted automata, which makes it possible to express important quantitative properties such as average response time. In nested weighted automata, a master automaton spins off and collects results from weighted slave automata, each of which computes a quantity along a finite portion of an infinite word. Nested weighted automata can be viewed as the quantitative analogue of monitor automata, which are used in runtime verification. We establish an almost-complete decidability picture for the basic decision problems about nested weighted automata and illustrate their applicability in several domains. In particular, nested weighted automata can be used to decide average response time properties.","lang":"eng"}],"date_updated":"2023-02-23T12:26:19Z","citation":{"chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted Automata.” <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM, 2017. <a href=\"https://doi.org/10.1145/3152769\">https://doi.org/10.1145/3152769</a>.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted automata,” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 18, no. 4. ACM, 2017.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2017). Nested weighted automata. <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM. <a href=\"https://doi.org/10.1145/3152769\">https://doi.org/10.1145/3152769</a>","ama":"Chatterjee K, Henzinger TA, Otop J. Nested weighted automata. <i>ACM Transactions on Computational Logic (TOCL)</i>. 2017;18(4). doi:<a href=\"https://doi.org/10.1145/3152769\">10.1145/3152769</a>","ista":"Chatterjee K, Henzinger TA, Otop J. 2017. Nested weighted automata. ACM Transactions on Computational Logic (TOCL). 18(4), 31.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, ACM Transactions on Computational Logic (TOCL) 18 (2017).","mla":"Chatterjee, Krishnendu, et al. “Nested Weighted Automata.” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 18, no. 4, 31, ACM, 2017, doi:<a href=\"https://doi.org/10.1145/3152769\">10.1145/3152769</a>."},"year":"2017","external_id":{"arxiv":["1606.03598"]}},{"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"5449"}]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","file":[{"content_type":"application/pdf","file_name":"IST-2018-938-v1+1_2017_Pavlogiannis_Amplification_on.pdf","date_updated":"2020-07-14T12:46:36Z","checksum":"7d05cbdd914e194a019c0f91fb64e9a8","file_size":1536783,"date_created":"2018-12-12T10:18:35Z","creator":"system","file_id":"5357","access_level":"open_access","relation":"main_file"}],"date_published":"2017-03-06T00:00:00Z","type":"journal_article","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"oa":1,"publist_id":"7307","publication_identifier":{"issn":["20452322"]},"language":[{"iso":"eng"}],"publication":"Scientific Reports","has_accepted_license":"1","month":"03","article_number":"82","oa_version":"Published Version","project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"ddc":["004"],"volume":7,"date_updated":"2023-02-23T12:26:57Z","year":"2017","citation":{"ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, “Amplification on undirected population structures: Comets beat stars,” <i>Scientific Reports</i>, vol. 7, no. 1. Nature Publishing Group, 2017.","chicago":"Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak. “Amplification on Undirected Population Structures: Comets Beat Stars.” <i>Scientific Reports</i>. Nature Publishing Group, 2017. <a href=\"https://doi.org/10.1038/s41598-017-00107-w\">https://doi.org/10.1038/s41598-017-00107-w</a>.","ama":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. Amplification on undirected population structures: Comets beat stars. <i>Scientific Reports</i>. 2017;7(1). doi:<a href=\"https://doi.org/10.1038/s41598-017-00107-w\">10.1038/s41598-017-00107-w</a>","apa":"Pavlogiannis, A., Tkadlec, J., Chatterjee, K., &#38; Nowak, M. (2017). Amplification on undirected population structures: Comets beat stars. <i>Scientific Reports</i>. Nature Publishing Group. <a href=\"https://doi.org/10.1038/s41598-017-00107-w\">https://doi.org/10.1038/s41598-017-00107-w</a>","ista":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2017. Amplification on undirected population structures: Comets beat stars. Scientific Reports. 7(1), 82.","short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Scientific Reports 7 (2017).","mla":"Pavlogiannis, Andreas, et al. “Amplification on Undirected Population Structures: Comets Beat Stars.” <i>Scientific Reports</i>, vol. 7, no. 1, 82, Nature Publishing Group, 2017, doi:<a href=\"https://doi.org/10.1038/s41598-017-00107-w\">10.1038/s41598-017-00107-w</a>."},"abstract":[{"lang":"eng","text":"The fixation probability is the probability that a new mutant introduced in a homogeneous population eventually takes over the entire population. The fixation probability is a fundamental quantity of natural selection, and known to depend on the population structure. Amplifiers of natural selection are population structures which increase the fixation probability of advantageous mutants, as compared to the baseline case of well-mixed populations. In this work we focus on symmetric population structures represented as undirected graphs. In the regime of undirected graphs, the strongest amplifier known has been the Star graph, and the existence of undirected graphs with stronger amplification properties has remained open for over a decade. In this work we present the Comet and Comet-swarm families of undirected graphs. We show that for a range of fitness values of the mutants, the Comet and Cometswarm graphs have fixation probability strictly larger than the fixation probability of the Star graph, for fixed population size and at the limit of large populations, respectively. "}],"doi":"10.1038/s41598-017-00107-w","day":"06","file_date_updated":"2020-07-14T12:46:36Z","ec_funded":1,"quality_controlled":"1","publisher":"Nature Publishing Group","author":[{"full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-1097-9684","full_name":"Tkadlec, Josef","first_name":"Josef","last_name":"Tkadlec"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"full_name":"Nowak, Martin","last_name":"Nowak","first_name":"Martin"}],"issue":"1","_id":"512","scopus_import":1,"title":"Amplification on undirected population structures: Comets beat stars","pubrep_id":"938","intvolume":"         7","publication_status":"published","date_created":"2018-12-11T11:46:53Z","department":[{"_id":"KrCh"}],"article_processing_charge":"No"},{"author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Choudhary, Bhavya","last_name":"Choudhary","first_name":"Bhavya"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","first_name":"Andreas","last_name":"Pavlogiannis"}],"_id":"5455","title":"Optimal Dyck reachability for data-dependence and alias analysis","pubrep_id":"870","alternative_title":["IST Austria Technical Report"],"department":[{"_id":"KrCh"}],"article_processing_charge":"No","date_created":"2018-12-12T11:39:26Z","publication_status":"published","file_date_updated":"2020-07-14T12:46:59Z","page":"37","publisher":"IST Austria","citation":{"ista":"Chatterjee K, Choudhary B, Pavlogiannis A. 2017. Optimal Dyck reachability for data-dependence and alias analysis, IST Austria, 37p.","short":"K. Chatterjee, B. Choudhary, A. Pavlogiannis, Optimal Dyck Reachability for Data-Dependence and Alias Analysis, IST Austria, 2017.","mla":"Chatterjee, Krishnendu, et al. <i>Optimal Dyck Reachability for Data-Dependence and Alias Analysis</i>. IST Austria, 2017, doi:<a href=\"https://doi.org/10.15479/AT:IST-2017-870-v1-1\">10.15479/AT:IST-2017-870-v1-1</a>.","chicago":"Chatterjee, Krishnendu, Bhavya Choudhary, and Andreas Pavlogiannis. <i>Optimal Dyck Reachability for Data-Dependence and Alias Analysis</i>. IST Austria, 2017. <a href=\"https://doi.org/10.15479/AT:IST-2017-870-v1-1\">https://doi.org/10.15479/AT:IST-2017-870-v1-1</a>.","ieee":"K. Chatterjee, B. Choudhary, and A. Pavlogiannis, <i>Optimal Dyck reachability for data-dependence and alias analysis</i>. IST Austria, 2017.","ama":"Chatterjee K, Choudhary B, Pavlogiannis A. <i>Optimal Dyck Reachability for Data-Dependence and Alias Analysis</i>. IST Austria; 2017. doi:<a href=\"https://doi.org/10.15479/AT:IST-2017-870-v1-1\">10.15479/AT:IST-2017-870-v1-1</a>","apa":"Chatterjee, K., Choudhary, B., &#38; Pavlogiannis, A. (2017). <i>Optimal Dyck reachability for data-dependence and alias analysis</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2017-870-v1-1\">https://doi.org/10.15479/AT:IST-2017-870-v1-1</a>"},"year":"2017","date_updated":"2023-02-21T15:54:10Z","abstract":[{"lang":"eng","text":"A fundamental algorithmic problem at the heart of static analysis is Dyck reachability. The input is a graphwhere the edges are labeled with different types of opening and closing parentheses, and the reachabilityinformation is computed via paths whose parentheses are properly matched. We present new results for Dyckreachability problems with applications to alias analysis and data-dependence analysis. Our main contributions,that include improved upper bounds as well as lower bounds that establish optimality guarantees, are asfollows:First, we consider Dyck reachability on bidirected graphs, which is the standard way of performing field-sensitive points-to analysis. Given a bidirected graph withnnodes andmedges, we present: (i) an algorithmwith worst-case running timeO(m+n·α(n)), whereα(n)is the inverse Ackermann function, improving thepreviously knownO(n2)time bound; (ii) a matching lower bound that shows that our algorithm is optimalwrt to worst-case complexity; and (iii) an optimal average-case upper bound ofO(m)time, improving thepreviously knownO(m·logn)bound.Second, we consider the problem of context-sensitive data-dependence analysis, where the task is to obtainanalysis summaries of library code in the presence of callbacks. Our algorithm preprocesses libraries in almostlinear time, after which the contribution of the library in the complexity of the client analysis is only linear,and only wrt the number of call sites.Third, we prove that combinatorial algorithms for Dyck reachability on general graphs with truly sub-cubic bounds cannot be obtained without obtaining sub-cubic combinatorial algorithms for Boolean MatrixMultiplication, which is a long-standing open problem. Thus we establish that the existing combinatorialalgorithms for Dyck reachability are (conditionally) optimal for general graphs. We also show that the samehardness holds for graphs of constant treewidth.Finally, we provide a prototype implementation of our algorithms for both alias analysis and data-dependenceanalysis. Our experimental evaluation demonstrates that the new algorithms significantly outperform allexisting methods on the two problems, over real-world benchmarks."}],"day":"23","doi":"10.15479/AT:IST-2017-870-v1-1","ddc":["000"],"has_accepted_license":"1","month":"10","oa_version":"Published Version","language":[{"iso":"eng"}],"type":"technical_report","date_published":"2017-10-23T00:00:00Z","oa":1,"publication_identifier":{"issn":["2664-1690"]},"related_material":{"record":[{"status":"public","relation":"later_version","id":"10416"}]},"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","status":"public","file":[{"access_level":"open_access","relation":"main_file","file_id":"5524","creator":"system","date_created":"2018-12-12T11:54:02Z","file_size":960491,"checksum":"177a84a46e3ac17e87b31534ad16a4c9","date_updated":"2020-07-14T12:46:59Z","content_type":"application/pdf","file_name":"IST-2017-870-v1+1_main.pdf"}]},{"file":[{"checksum":"d2635c4cf013000f0a1b09e80f9e4ab7","file_size":910347,"date_created":"2018-12-12T11:53:26Z","file_name":"IST-2017-872-v1+1_main.pdf","content_type":"application/pdf","date_updated":"2020-07-14T12:46:59Z","relation":"main_file","access_level":"open_access","creator":"system","file_id":"5487"}],"ddc":["000"],"related_material":{"record":[{"id":"10417","relation":"later_version","status":"public"},{"id":"5448","relation":"earlier_version","status":"public"}]},"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-02-23T12:26:54Z","citation":{"mla":"Chalupa, Marek, et al. <i>Data-Centric Dynamic Partial Order Reduction</i>. IST Austria, 2017, doi:<a href=\"https://doi.org/10.15479/AT:IST-2017-872-v1-1\">10.15479/AT:IST-2017-872-v1-1</a>.","short":"M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, K. Vaidya, Data-Centric Dynamic Partial Order Reduction, IST Austria, 2017.","ista":"Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. 2017. Data-centric dynamic partial order reduction, IST Austria, 36p.","ama":"Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. <i>Data-Centric Dynamic Partial Order Reduction</i>. IST Austria; 2017. doi:<a href=\"https://doi.org/10.15479/AT:IST-2017-872-v1-1\">10.15479/AT:IST-2017-872-v1-1</a>","apa":"Chalupa, M., Chatterjee, K., Pavlogiannis, A., Sinha, N., &#38; Vaidya, K. (2017). <i>Data-centric dynamic partial order reduction</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2017-872-v1-1\">https://doi.org/10.15479/AT:IST-2017-872-v1-1</a>","ieee":"M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya, <i>Data-centric dynamic partial order reduction</i>. IST Austria, 2017.","chicago":"Chalupa, Marek, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya. <i>Data-Centric Dynamic Partial Order Reduction</i>. IST Austria, 2017. <a href=\"https://doi.org/10.15479/AT:IST-2017-872-v1-1\">https://doi.org/10.15479/AT:IST-2017-872-v1-1</a>."},"year":"2017","date_published":"2017-10-23T00:00:00Z","type":"technical_report","doi":"10.15479/AT:IST-2017-872-v1-1","publication_identifier":{"issn":["2664-1690"]},"day":"23","abstract":[{"text":"We present a new dynamic partial-order reduction method for stateless model checking of concurrent programs. A common approach for exploring program behaviors relies on enumerating the traces of the program, without storing the visited states (aka stateless exploration). As the number of distinct traces grows exponentially, dynamic partial-order reduction (DPOR) techniques have been successfully used to partition the space of traces into equivalence classes (Mazurkiewicz partitioning), with the goal of exploring only few representative traces from each class.\r\nWe introduce a new equivalence on traces under sequential consistency semantics, which we call the observation equivalence. Two traces are observationally equivalent if every read event observes the same write event in both traces. While the traditional Mazurkiewicz equivalence is control-centric, our new definition is data-centric. We show that our observation equivalence is coarser than the Mazurkiewicz equivalence, and in many cases even exponentially coarser. We devise a DPOR exploration of the trace space, called data-centric DPOR, based on the observation equivalence.\r\n1. For acyclic architectures, our algorithm is guaranteed to explore exactly one representative trace from each observation class, while spending polynomial time per class. Hence, our algorithm is optimal wrt the observation equivalence, and in several cases explores exponentially fewer traces than any enumerative method based on the Mazurkiewicz equivalence.\r\n2. For cyclic architectures, we consider an equivalence between traces which is finer than the observation equivalence; but coarser than the Mazurkiewicz equivalence, and in some cases is exponentially coarser. Our data-centric DPOR algorithm remains optimal under this trace equivalence. \r\nFinally, we perform a basic experimental comparison between the existing Mazurkiewicz-based DPOR and our data-centric DPOR on a set of academic benchmarks. Our results show a significant reduction in both running time and the number of explored equivalence classes.","lang":"eng"}],"oa":1,"page":"36","language":[{"iso":"eng"}],"file_date_updated":"2020-07-14T12:46:59Z","publisher":"IST Austria","_id":"5456","has_accepted_license":"1","author":[{"full_name":"Chalupa, Marek","last_name":"Chalupa","first_name":"Marek"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Sinha, Nishant","last_name":"Sinha","first_name":"Nishant"},{"first_name":"Kapil","last_name":"Vaidya","full_name":"Vaidya, Kapil"}],"oa_version":"Published Version","publication_status":"published","date_created":"2018-12-12T11:39:26Z","department":[{"_id":"KrCh"}],"alternative_title":["IST Austria Technical Report"],"month":"10","pubrep_id":"872","title":"Data-centric dynamic partial order reduction"},{"publication":"Leibniz International Proceedings in Informatics","has_accepted_license":"1","oa_version":"Published Version","month":"11","article_number":"61","language":[{"iso":"eng"}],"conference":{"location":"Aalborg, Denmark","end_date":"2017-08-25","start_date":"2017-08-21","name":"MFCS: Mathematical Foundations of Computer Science (SG)"},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"date_published":"2017-11-01T00:00:00Z","type":"conference","publication_identifier":{"isbn":["978-395977046-0"]},"oa":1,"publist_id":"7263","file":[{"creator":"system","file_id":"5322","access_level":"open_access","relation":"main_file","file_name":"IST-2018-924-v1+1_LIPIcs-MFCS-2017-61.pdf","content_type":"application/pdf","date_updated":"2020-07-14T12:47:00Z","file_size":535077,"checksum":"2eed5224c0e4e259484a1d71acb8ba6a","date_created":"2018-12-12T10:18:04Z"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","status":"public","_id":"551","scopus_import":1,"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","last_name":"Ibsen-Jensen"},{"first_name":"Martin","last_name":"Nowak","full_name":"Nowak, Martin"}],"publication_status":"published","department":[{"_id":"KrCh"}],"date_created":"2018-12-11T11:47:08Z","alternative_title":["LIPIcs"],"pubrep_id":"924","title":"Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs","intvolume":"        83","quality_controlled":"1","file_date_updated":"2020-07-14T12:47:00Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_updated":"2021-01-12T08:02:34Z","year":"2017","citation":{"chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Martin Nowak. “Faster Monte Carlo Algorithms for Fixation Probability of the Moran Process on Undirected Graphs.” In <i>Leibniz International Proceedings in Informatics</i>, Vol. 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.61\">https://doi.org/10.4230/LIPIcs.MFCS.2017.61</a>.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and M. Nowak, “Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs,” in <i>Leibniz International Proceedings in Informatics</i>, Aalborg, Denmark, 2017, vol. 83.","ama":"Chatterjee K, Ibsen-Jensen R, Nowak M. Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs. In: <i>Leibniz International Proceedings in Informatics</i>. Vol 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.61\">10.4230/LIPIcs.MFCS.2017.61</a>","apa":"Chatterjee, K., Ibsen-Jensen, R., &#38; Nowak, M. (2017). Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs. In <i>Leibniz International Proceedings in Informatics</i> (Vol. 83). Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.61\">https://doi.org/10.4230/LIPIcs.MFCS.2017.61</a>","ista":"Chatterjee K, Ibsen-Jensen R, Nowak M. 2017. Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs. Leibniz International Proceedings in Informatics. MFCS: Mathematical Foundations of Computer Science (SG), LIPIcs, vol. 83, 61.","short":"K. Chatterjee, R. Ibsen-Jensen, M. Nowak, in:, Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.","mla":"Chatterjee, Krishnendu, et al. “Faster Monte Carlo Algorithms for Fixation Probability of the Moran Process on Undirected Graphs.” <i>Leibniz International Proceedings in Informatics</i>, vol. 83, 61, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.61\">10.4230/LIPIcs.MFCS.2017.61</a>."},"doi":"10.4230/LIPIcs.MFCS.2017.61","day":"01","abstract":[{"lang":"eng","text":"Evolutionary graph theory studies the evolutionary dynamics in a population structure given as a connected graph. Each node of the graph represents an individual of the population, and edges determine how offspring are placed. We consider the classical birth-death Moran process where there are two types of individuals, namely, the residents with fitness 1 and mutants with fitness r. The fitness indicates the reproductive strength. The evolutionary dynamics happens as follows: in the initial step, in a population of all resident individuals a mutant is introduced, and then at each step, an individual is chosen proportional to the fitness of its type to reproduce, and the offspring replaces a neighbor uniformly at random. The process stops when all individuals are either residents or mutants. The probability that all individuals in the end are mutants is called the fixation probability, which is a key factor in the rate of evolution. We consider the problem of approximating the fixation probability. The class of algorithms that is extremely relevant for approximation of the fixation probabilities is the Monte-Carlo simulation of the process. Previous results present a polynomial-time Monte-Carlo algorithm for undirected graphs when r is given in unary. First, we present a simple modification: instead of simulating each step, we discard ineffective steps, where no node changes type (i.e., either residents replace residents, or mutants replace mutants). Using the above simple modification and our result that the number of effective steps is concentrated around the expected number of effective steps, we present faster polynomial-time Monte-Carlo algorithms for undirected graphs. Our algorithms are always at least a factor O(n2/ log n) faster as compared to the previous algorithms, where n is the number of nodes, and is polynomial even if r is given in binary. We also present lower bounds showing that the upper bound on the expected number of effective steps we present is asymptotically tight for undirected graphs. "}],"volume":83,"ddc":["004"]},{"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"date_created":"2018-12-12T10:16:57Z","file_size":610339,"checksum":"c67f4866ddbfd555afef1f63ae9a8fc7","date_updated":"2020-07-14T12:47:00Z","file_name":"IST-2018-923-v1+1_LIPIcs-MFCS-2017-39.pdf","content_type":"application/pdf","relation":"main_file","access_level":"open_access","file_id":"5248","creator":"system"}],"type":"conference","date_published":"2017-11-01T00:00:00Z","tmp":{"name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)","image":"/images/cc_by.png","short":"CC BY (3.0)","legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode"},"oa":1,"publist_id":"7262","publication_identifier":{"isbn":["978-395977046-0"]},"language":[{"iso":"eng"}],"conference":{"end_date":"2017-08-25","location":"Aalborg, Denmark","start_date":"2017-08-21","name":"MFCS: Mathematical Foundations of Computer Science (SG)"},"has_accepted_license":"1","publication":"Leibniz International Proceedings in Informatics","article_number":"39","month":"11","project":[{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory","grant_number":"S11407"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"oa_version":"Published Version","ddc":["004"],"volume":83,"year":"2017","citation":{"ieee":"K. Chatterjee, M. H. Henzinger, and A. Svozil, “Faster algorithms for mean-payoff parity games,” in <i>Leibniz International Proceedings in Informatics</i>, Aalborg, Denmark, 2017, vol. 83.","chicago":"Chatterjee, Krishnendu, Monika H Henzinger, and Alexander Svozil. “Faster Algorithms for Mean-Payoff Parity Games.” In <i>Leibniz International Proceedings in Informatics</i>, Vol. 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.39\">https://doi.org/10.4230/LIPIcs.MFCS.2017.39</a>.","apa":"Chatterjee, K., Henzinger, M. H., &#38; Svozil, A. (2017). Faster algorithms for mean-payoff parity games. In <i>Leibniz International Proceedings in Informatics</i> (Vol. 83). Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.39\">https://doi.org/10.4230/LIPIcs.MFCS.2017.39</a>","ama":"Chatterjee K, Henzinger MH, Svozil A. Faster algorithms for mean-payoff parity games. In: <i>Leibniz International Proceedings in Informatics</i>. Vol 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.39\">10.4230/LIPIcs.MFCS.2017.39</a>","ista":"Chatterjee K, Henzinger MH, Svozil A. 2017. Faster algorithms for mean-payoff parity games. Leibniz International Proceedings in Informatics. MFCS: Mathematical Foundations of Computer Science (SG), LIPIcs, vol. 83, 39.","short":"K. Chatterjee, M.H. Henzinger, A. Svozil, in:, Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.","mla":"Chatterjee, Krishnendu, et al. “Faster Algorithms for Mean-Payoff Parity Games.” <i>Leibniz International Proceedings in Informatics</i>, vol. 83, 39, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.39\">10.4230/LIPIcs.MFCS.2017.39</a>."},"date_updated":"2023-02-14T10:06:46Z","abstract":[{"lang":"eng","text":"Graph games provide the foundation for modeling and synthesis of reactive processes. Such games are played over graphs where the vertices are controlled by two adversarial players. We consider graph games where the objective of the first player is the conjunction of a qualitative objective (specified as a parity condition) and a quantitative objective (specified as a meanpayoff condition). There are two variants of the problem, namely, the threshold problem where the quantitative goal is to ensure that the mean-payoff value is above a threshold, and the value problem where the quantitative goal is to ensure the optimal mean-payoff value; in both cases ensuring the qualitative parity objective. The previous best-known algorithms for game graphs with n vertices, m edges, parity objectives with d priorities, and maximal absolute reward value W for mean-payoff objectives, are as follows: O(nd+1 . m . w) for the threshold problem, and O(nd+2 · m · W) for the value problem. Our main contributions are faster algorithms, and the running times of our algorithms are as follows: O(nd-1 · m ·W) for the threshold problem, and O(nd · m · W · log(n · W)) for the value problem. For mean-payoff parity objectives with two priorities, our algorithms match the best-known bounds of the algorithms for mean-payoff games (without conjunction with parity objectives). Our results are relevant in synthesis of reactive systems with both functional requirement (given as a qualitative objective) and performance requirement (given as a quantitative objective)."}],"day":"01","doi":"10.4230/LIPIcs.MFCS.2017.39","file_date_updated":"2020-07-14T12:47:00Z","ec_funded":1,"quality_controlled":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Monika H","last_name":"Henzinger","orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630"},{"last_name":"Svozil","first_name":"Alexander","full_name":"Svozil, Alexander"}],"license":"https://creativecommons.org/licenses/by/3.0/","scopus_import":"1","_id":"552","intvolume":"        83","title":"Faster algorithms for mean-payoff parity games","pubrep_id":"923","alternative_title":["LIPIcs"],"department":[{"_id":"KrCh"}],"date_created":"2018-12-11T11:47:08Z","article_processing_charge":"No","publication_status":"published"},{"day":"01","doi":"10.4230/LIPIcs.MFCS.2017.55","abstract":[{"text":"We consider two player, zero-sum, finite-state concurrent reachability games, played for an infinite number of rounds, where in every round, each player simultaneously and independently of the other players chooses an action, whereafter the successor state is determined by a probability distribution given by the current state and the chosen actions. Player 1 wins iff a designated goal state is eventually visited. We are interested in the complexity of stationary strategies measured by their patience, which is defined as the inverse of the smallest non-zero probability employed. Our main results are as follows: We show that: (i) the optimal bound on the patience of optimal and -optimal strategies, for both players is doubly exponential; and (ii) even in games with a single non-absorbing state exponential (in the number of actions) patience is necessary. ","lang":"eng"}],"year":"2017","citation":{"ieee":"K. Chatterjee, K. Hansen, and R. Ibsen-Jensen, “Strategy complexity of concurrent safety games,” in <i>Leibniz International Proceedings in Informatics</i>, Aalborg, Denmark, 2017, vol. 83.","chicago":"Chatterjee, Krishnendu, Kristofer Hansen, and Rasmus Ibsen-Jensen. “Strategy Complexity of Concurrent Safety Games.” In <i>Leibniz International Proceedings in Informatics</i>, Vol. 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.55\">https://doi.org/10.4230/LIPIcs.MFCS.2017.55</a>.","apa":"Chatterjee, K., Hansen, K., &#38; Ibsen-Jensen, R. (2017). Strategy complexity of concurrent safety games. In <i>Leibniz International Proceedings in Informatics</i> (Vol. 83). Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.55\">https://doi.org/10.4230/LIPIcs.MFCS.2017.55</a>","ama":"Chatterjee K, Hansen K, Ibsen-Jensen R. Strategy complexity of concurrent safety games. In: <i>Leibniz International Proceedings in Informatics</i>. Vol 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.55\">10.4230/LIPIcs.MFCS.2017.55</a>","ista":"Chatterjee K, Hansen K, Ibsen-Jensen R. 2017. Strategy complexity of concurrent safety games. Leibniz International Proceedings in Informatics. MFCS: Mathematical Foundations of Computer Science (SG), LIPIcs, vol. 83, 55.","mla":"Chatterjee, Krishnendu, et al. “Strategy Complexity of Concurrent Safety Games.” <i>Leibniz International Proceedings in Informatics</i>, vol. 83, 55, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.55\">10.4230/LIPIcs.MFCS.2017.55</a>.","short":"K. Chatterjee, K. Hansen, R. Ibsen-Jensen, in:, Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017."},"date_updated":"2021-01-12T08:02:35Z","volume":83,"ddc":["004"],"department":[{"_id":"KrCh"}],"date_created":"2018-12-11T11:47:08Z","publication_status":"published","intvolume":"        83","alternative_title":["LIPIcs"],"pubrep_id":"922","title":"Strategy complexity of concurrent safety games","scopus_import":1,"_id":"553","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Hansen, Kristofer","first_name":"Kristofer","last_name":"Hansen"},{"last_name":"Ibsen-Jensen","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","quality_controlled":"1","file_date_updated":"2020-07-14T12:47:00Z","publication_identifier":{"isbn":["978-395977046-0"]},"publist_id":"7261","oa":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"type":"conference","date_published":"2017-11-01T00:00:00Z","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1506.02434"}],"file":[{"creator":"system","file_id":"4753","access_level":"open_access","relation":"main_file","content_type":"application/pdf","file_name":"IST-2018-922-v1+1_LIPIcs-MFCS-2017-55.pdf","date_updated":"2020-07-14T12:47:00Z","checksum":"7101facb56ade363205c695d72dbd173","file_size":549967,"date_created":"2018-12-12T10:09:29Z"}],"status":"public","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","oa_version":"Published Version","article_number":"55","month":"11","has_accepted_license":"1","publication":"Leibniz International Proceedings in Informatics","conference":{"location":"Aalborg, Denmark","end_date":"2017-08-25","name":"MFCS: Mathematical Foundations of Computer Science (SG)","start_date":"2017-08-21"},"language":[{"iso":"eng"}]},{"type":"research_data","date_published":"2017-01-02T00:00:00Z","citation":{"ama":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak  M. Strong amplifiers of natural selection. 2017. doi:<a href=\"https://doi.org/10.15479/AT:ISTA:51\">10.15479/AT:ISTA:51</a>","apa":"Pavlogiannis, A., Tkadlec, J., Chatterjee, K., &#38; Nowak , M. (2017). Strong amplifiers of natural selection. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT:ISTA:51\">https://doi.org/10.15479/AT:ISTA:51</a>","chicago":"Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak . “Strong Amplifiers of Natural Selection.” Institute of Science and Technology Austria, 2017. <a href=\"https://doi.org/10.15479/AT:ISTA:51\">https://doi.org/10.15479/AT:ISTA:51</a>.","ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak , “Strong amplifiers of natural selection.” Institute of Science and Technology Austria, 2017.","short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak , (2017).","mla":"Pavlogiannis, Andreas, et al. <i>Strong Amplifiers of Natural Selection</i>. Institute of Science and Technology Austria, 2017, doi:<a href=\"https://doi.org/10.15479/AT:ISTA:51\">10.15479/AT:ISTA:51</a>.","ista":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak  M. 2017. Strong amplifiers of natural selection, Institute of Science and Technology Austria, <a href=\"https://doi.org/10.15479/AT:ISTA:51\">10.15479/AT:ISTA:51</a>."},"year":"2017","date_updated":"2024-02-21T13:48:42Z","oa":1,"abstract":[{"lang":"eng","text":"Strong amplifiers of natural selection"}],"day":"02","doi":"10.15479/AT:ISTA:51","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"id":"5452","relation":"research_paper","status":"public"},{"status":"public","id":"5751","relation":"research_paper"}]},"status":"public","ddc":["519"],"file":[{"creator":"system","file_id":"5644","relation":"main_file","access_level":"open_access","content_type":"video/mp4","file_name":"IST-2017-51-v1+2_illustration.mp4","date_updated":"2020-07-14T12:47:02Z","file_size":32987015,"checksum":"b427dd46a30096a1911b245640c47af8","date_created":"2018-12-12T13:05:18Z"}],"datarep_id":"51","author":[{"last_name":"Pavlogiannis","first_name":"Andreas","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Tkadlec, Josef","orcid":"0000-0002-1097-9684","last_name":"Tkadlec","first_name":"Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"last_name":"Nowak ","first_name":"Martin","full_name":"Nowak , Martin"}],"has_accepted_license":"1","_id":"5559","title":"Strong amplifiers of natural selection","month":"01","department":[{"_id":"KrCh"}],"article_processing_charge":"No","project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"}],"date_created":"2018-12-12T12:31:32Z","oa_version":"Published Version","keyword":["natural selection"],"file_date_updated":"2020-07-14T12:47:02Z","ec_funded":1,"publisher":"Institute of Science and Technology Austria"},{"publication":"Models, Algorithms, Logics and Tools","has_accepted_license":"1","oa_version":"Submitted Version","project":[{"grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","call_identifier":"FWF","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407"},{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"}],"month":"07","language":[{"iso":"eng"}],"date_published":"2017-07-25T00:00:00Z","type":"book_chapter","publication_identifier":{"isbn":["978-3-319-63120-2"],"issn":["0302-9743"]},"oa":1,"publist_id":"7170","file":[{"access_level":"open_access","relation":"main_file","creator":"dernst","file_id":"7048","checksum":"b2402766ec02c79801aac634bd8f9f6c","file_size":192826,"date_created":"2019-11-19T08:06:50Z","file_name":"2017_ModelsAlgorithms_Chatterjee.pdf","content_type":"application/pdf","date_updated":"2020-07-14T12:47:25Z"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","_id":"625","scopus_import":"1","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"first_name":"Laurent","last_name":"Doyen","full_name":"Doyen, Laurent"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A"}],"publication_status":"published","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"article_processing_charge":"No","date_created":"2018-12-11T11:47:34Z","title":"The cost of exactness in quantitative reachability","alternative_title":["LNCS"],"intvolume":"     10460","page":"367 - 381","ec_funded":1,"series_title":"Theoretical Computer Science and General Issues","quality_controlled":"1","file_date_updated":"2020-07-14T12:47:25Z","publisher":"Springer","editor":[{"full_name":"Aceto, Luca","first_name":"Luca","last_name":"Aceto"},{"last_name":"Bacci","first_name":"Giorgio","full_name":"Bacci, Giorgio"},{"first_name":"Anna","last_name":"Ingólfsdóttir","full_name":"Ingólfsdóttir, Anna"},{"full_name":"Legay, Axel","last_name":"Legay","first_name":"Axel"},{"full_name":"Mardare, Radu","last_name":"Mardare","first_name":"Radu"}],"date_updated":"2025-06-02T08:53:45Z","citation":{"mla":"Chatterjee, Krishnendu, et al. “The Cost of Exactness in Quantitative Reachability.” <i>Models, Algorithms, Logics and Tools</i>, edited by Luca Aceto et al., vol. 10460, Springer, 2017, pp. 367–81, doi:<a href=\"https://doi.org/10.1007/978-3-319-63121-9_18\">10.1007/978-3-319-63121-9_18</a>.","short":"K. Chatterjee, L. Doyen, T.A. Henzinger, in:, L. Aceto, G. Bacci, A. Ingólfsdóttir, A. Legay, R. Mardare (Eds.), Models, Algorithms, Logics and Tools, Springer, 2017, pp. 367–381.","ista":"Chatterjee K, Doyen L, Henzinger TA. 2017.The cost of exactness in quantitative reachability. In: Models, Algorithms, Logics and Tools. LNCS, vol. 10460, 367–381.","ama":"Chatterjee K, Doyen L, Henzinger TA. The cost of exactness in quantitative reachability. In: Aceto L, Bacci G, Ingólfsdóttir A, Legay A, Mardare R, eds. <i>Models, Algorithms, Logics and Tools</i>. Vol 10460. Theoretical Computer Science and General Issues. Springer; 2017:367-381. doi:<a href=\"https://doi.org/10.1007/978-3-319-63121-9_18\">10.1007/978-3-319-63121-9_18</a>","apa":"Chatterjee, K., Doyen, L., &#38; Henzinger, T. A. (2017). The cost of exactness in quantitative reachability. In L. Aceto, G. Bacci, A. Ingólfsdóttir, A. Legay, &#38; R. Mardare (Eds.), <i>Models, Algorithms, Logics and Tools</i> (Vol. 10460, pp. 367–381). Springer. <a href=\"https://doi.org/10.1007/978-3-319-63121-9_18\">https://doi.org/10.1007/978-3-319-63121-9_18</a>","ieee":"K. Chatterjee, L. Doyen, and T. A. Henzinger, “The cost of exactness in quantitative reachability,” in <i>Models, Algorithms, Logics and Tools</i>, vol. 10460, L. Aceto, G. Bacci, A. Ingólfsdóttir, A. Legay, and R. Mardare, Eds. Springer, 2017, pp. 367–381.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “The Cost of Exactness in Quantitative Reachability.” In <i>Models, Algorithms, Logics and Tools</i>, edited by Luca Aceto, Giorgio Bacci, Anna Ingólfsdóttir, Axel Legay, and Radu Mardare, 10460:367–81. Theoretical Computer Science and General Issues. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-319-63121-9_18\">https://doi.org/10.1007/978-3-319-63121-9_18</a>."},"year":"2017","doi":"10.1007/978-3-319-63121-9_18","day":"25","abstract":[{"text":"In the analysis of reactive systems a quantitative objective assigns a real value to every trace of the system. The value decision problem for a quantitative objective requires a trace whose value is at least a given threshold, and the exact value decision problem requires a trace whose value is exactly the threshold. We compare the computational complexity of the value and exact value decision problems for classical quantitative objectives, such as sum, discounted sum, energy, and mean-payoff for two standard models of reactive systems, namely, graphs and graph games.","lang":"eng"}],"acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23 and S11407-N23 (RiSE/SHiNE), and Z211-N23 (Wittgenstein Award), ERC Start grant (279307: Graph Games), Vienna Science and Technology Fund (WWTF) through project ICT15-003.","volume":10460,"ddc":["000"]},{"publication_identifier":{"isbn":["978-331963386-2"]},"oa":1,"publist_id":"7166","date_published":"2017-01-01T00:00:00Z","type":"conference","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1705.00314"}],"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","status":"public","oa_version":"Submitted Version","project":[{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"}],"month":"01","conference":{"name":"CAV: Computer Aided Verification","start_date":"2017-07-24","location":"Heidelberg, Germany","end_date":"2017-07-28"},"language":[{"iso":"eng"}],"doi":"10.1007/978-3-319-63387-9_6","day":"01","abstract":[{"text":"We consider the problem of developing automated techniques for solving recurrence relations to aid the expected-runtime analysis of programs. The motivation is that several classical textbook algorithms have quite efficient expected-runtime complexity, whereas the corresponding worst-case bounds are either inefficient (e.g., Quick-Sort), or completely ineffective (e.g., Coupon-Collector). Since the main focus of expected-runtime analysis is to obtain efficient bounds, we consider bounds that are either logarithmic, linear or almost-linear (O(log n), O(n), O(n · log n), respectively, where n represents the input size). Our main contribution is an efficient (simple linear-time algorithm) sound approach for deriving such expected-runtime bounds for the analysis of recurrence relations induced by randomized algorithms. The experimental results show that our approach can efficiently derive asymptotically optimal expected-runtime bounds for recurrences of classical randomized algorithms, including Randomized-Search, Quick-Sort, Quick-Select, Coupon-Collector, where the worst-case bounds are either inefficient (such as linear as compared to logarithmic expected-runtime complexity, or quadratic as compared to linear or almost-linear expected-runtime complexity), or ineffective.","lang":"eng"}],"date_updated":"2021-01-12T08:06:55Z","year":"2017","citation":{"ista":"Chatterjee K, Fu H, Murhekar A. 2017. Automated recurrence analysis for almost linear expected runtime bounds. CAV: Computer Aided Verification, LNCS, vol. 10426, 118–139.","short":"K. Chatterjee, H. Fu, A. Murhekar, in:, R. Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 118–139.","mla":"Chatterjee, Krishnendu, et al. <i>Automated Recurrence Analysis for Almost Linear Expected Runtime Bounds</i>. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10426, Springer, 2017, pp. 118–39, doi:<a href=\"https://doi.org/10.1007/978-3-319-63387-9_6\">10.1007/978-3-319-63387-9_6</a>.","ieee":"K. Chatterjee, H. Fu, and A. Murhekar, “Automated recurrence analysis for almost linear expected runtime bounds,” presented at the CAV: Computer Aided Verification, Heidelberg, Germany, 2017, vol. 10426, pp. 118–139.","chicago":"Chatterjee, Krishnendu, Hongfei Fu, and Aniket Murhekar. “Automated Recurrence Analysis for Almost Linear Expected Runtime Bounds.” edited by Rupak Majumdar and Viktor Kunčak, 10426:118–39. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-319-63387-9_6\">https://doi.org/10.1007/978-3-319-63387-9_6</a>.","ama":"Chatterjee K, Fu H, Murhekar A. Automated recurrence analysis for almost linear expected runtime bounds. In: Majumdar R, Kunčak V, eds. Vol 10426. Springer; 2017:118-139. doi:<a href=\"https://doi.org/10.1007/978-3-319-63387-9_6\">10.1007/978-3-319-63387-9_6</a>","apa":"Chatterjee, K., Fu, H., &#38; Murhekar, A. (2017). Automated recurrence analysis for almost linear expected runtime bounds. In R. Majumdar &#38; V. Kunčak (Eds.) (Vol. 10426, pp. 118–139). Presented at the CAV: Computer Aided Verification, Heidelberg, Germany: Springer. <a href=\"https://doi.org/10.1007/978-3-319-63387-9_6\">https://doi.org/10.1007/978-3-319-63387-9_6</a>"},"volume":10426,"publication_status":"published","department":[{"_id":"KrCh"}],"date_created":"2018-12-11T11:47:35Z","alternative_title":["LNCS"],"title":"Automated recurrence analysis for almost linear expected runtime bounds","intvolume":"     10426","_id":"628","scopus_import":1,"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"last_name":"Fu","first_name":"Hongfei","full_name":"Fu, Hongfei"},{"full_name":"Murhekar, Aniket","last_name":"Murhekar","first_name":"Aniket"}],"publisher":"Springer","editor":[{"full_name":"Majumdar, Rupak","first_name":"Rupak","last_name":"Majumdar"},{"last_name":"Kunčak","first_name":"Viktor","full_name":"Kunčak, Viktor"}],"page":"118 - 139","ec_funded":1,"quality_controlled":"1"},{"project":[{"grant_number":"S11407","name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"}],"oa_version":"Submitted Version","month":"01","language":[{"iso":"eng"}],"conference":{"start_date":"2017-07-24","name":"CAV: Computer Aided Verification","location":"Heidelberg, Germany","end_date":"2017-07-28"},"type":"conference","date_published":"2017-01-01T00:00:00Z","publication_identifier":{"isbn":["978-331963389-3"]},"oa":1,"publist_id":"7149","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1705.00317"}],"related_material":{"record":[{"id":"8934","relation":"dissertation_contains","status":"public"},{"id":"7014","relation":"later_version","status":"public"}]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","scopus_import":1,"_id":"639","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Hongfei","last_name":"Fu","full_name":"Fu, Hongfei"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir","first_name":"Amir","last_name":"Goharshady"}],"date_created":"2018-12-11T11:47:39Z","article_processing_charge":"No","department":[{"_id":"KrCh"}],"publication_status":"published","intvolume":"     10427","alternative_title":["LNCS"],"title":"Non-polynomial worst case analysis of recursive programs","ec_funded":1,"quality_controlled":"1","page":"41 - 63","editor":[{"full_name":"Majumdar, Rupak","last_name":"Majumdar","first_name":"Rupak"},{"last_name":"Kunčak","first_name":"Viktor","full_name":"Kunčak, Viktor"}],"publisher":"Springer","year":"2017","citation":{"ista":"Chatterjee K, Fu H, Goharshady AK. 2017. Non-polynomial worst case analysis of recursive programs. CAV: Computer Aided Verification, LNCS, vol. 10427, 41–63.","short":"K. Chatterjee, H. Fu, A.K. Goharshady, in:, R. Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 41–63.","mla":"Chatterjee, Krishnendu, et al. <i>Non-Polynomial Worst Case Analysis of Recursive Programs</i>. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10427, Springer, 2017, pp. 41–63, doi:<a href=\"https://doi.org/10.1007/978-3-319-63390-9_3\">10.1007/978-3-319-63390-9_3</a>.","chicago":"Chatterjee, Krishnendu, Hongfei Fu, and Amir Kafshdar Goharshady. “Non-Polynomial Worst Case Analysis of Recursive Programs.” edited by Rupak Majumdar and Viktor Kunčak, 10427:41–63. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-319-63390-9_3\">https://doi.org/10.1007/978-3-319-63390-9_3</a>.","ieee":"K. Chatterjee, H. Fu, and A. K. Goharshady, “Non-polynomial worst case analysis of recursive programs,” presented at the CAV: Computer Aided Verification, Heidelberg, Germany, 2017, vol. 10427, pp. 41–63.","ama":"Chatterjee K, Fu H, Goharshady AK. Non-polynomial worst case analysis of recursive programs. In: Majumdar R, Kunčak V, eds. Vol 10427. Springer; 2017:41-63. doi:<a href=\"https://doi.org/10.1007/978-3-319-63390-9_3\">10.1007/978-3-319-63390-9_3</a>","apa":"Chatterjee, K., Fu, H., &#38; Goharshady, A. K. (2017). Non-polynomial worst case analysis of recursive programs. In R. Majumdar &#38; V. Kunčak (Eds.) (Vol. 10427, pp. 41–63). Presented at the CAV: Computer Aided Verification, Heidelberg, Germany: Springer. <a href=\"https://doi.org/10.1007/978-3-319-63390-9_3\">https://doi.org/10.1007/978-3-319-63390-9_3</a>"},"date_updated":"2025-06-02T08:53:47Z","external_id":{"arxiv":["1705.00317"]},"day":"01","arxiv":1,"doi":"10.1007/978-3-319-63390-9_3","abstract":[{"text":"We study the problem of developing efficient approaches for proving worst-case bounds of non-deterministic recursive programs. Ranking functions are sound and complete for proving termination and worst-case bounds of non-recursive programs. First, we apply ranking functions to recursion, resulting in measure functions, and show that they provide a sound and complete approach to prove worst-case bounds of non-deterministic recursive programs. Our second contribution is the synthesis of measure functions in non-polynomial forms. We show that non-polynomial measure functions with logarithm and exponentiation can be synthesized through abstraction of logarithmic or exponentiation terms, Farkas’ Lemma, and Handelman’s Theorem using linear programming. While previous methods obtain worst-case polynomial bounds, our approach can synthesize bounds of the form O(n log n) as well as O(nr) where r is not an integer. We present experimental results to demonstrate that our approach can efficiently obtain worst-case bounds of classical recursive algorithms such as Merge-Sort, Closest-Pair, Karatsuba’s algorithm and Strassen’s algorithm.","lang":"eng"}],"volume":10427},{"publication_identifier":{"isbn":["978-331963386-2"]},"publist_id":"7135","oa":1,"type":"conference","date_published":"2017-07-13T00:00:00Z","main_file_link":[{"url":"https://arxiv.org/abs/1705.02326","open_access":"1"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","status":"public","project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11407","name":"Game Theory"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"}],"oa_version":"Submitted Version","month":"07","conference":{"name":"CAV: Computer Aided Verification","start_date":"2017-07-24","end_date":"2017-07-28","location":"Heidelberg, Germany"},"language":[{"iso":"eng"}],"day":"13","doi":"10.1007/978-3-319-63387-9_10","abstract":[{"lang":"eng","text":"Markov decision processes (MDPs) are standard models for probabilistic systems with non-deterministic behaviours. Long-run average rewards provide a mathematically elegant formalism for expressing long term performance. Value iteration (VI) is one of the simplest and most efficient algorithmic approaches to MDPs with other properties, such as reachability objectives. Unfortunately, a naive extension of VI does not work for MDPs with long-run average rewards, as there is no known stopping criterion. In this work our contributions are threefold. (1) We refute a conjecture related to stopping criteria for MDPs with long-run average rewards. (2) We present two practical algorithms for MDPs with long-run average rewards based on VI. First, we show that a combination of applying VI locally for each maximal end-component (MEC) and VI for reachability objectives can provide approximation guarantees. Second, extending the above approach with a simulation-guided on-demand variant of VI, we present an anytime algorithm that is able to deal with very large models. (3) Finally, we present experimental results showing that our methods significantly outperform the standard approaches on several benchmarks."}],"year":"2017","citation":{"short":"P. Ashok, K. Chatterjee, P. Daca, J. Kretinsky, T. Meggendorfer, in:, R. Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 201–221.","mla":"Ashok, Pranav, et al. <i>Value Iteration for Long Run Average Reward in Markov Decision Processes</i>. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10426, Springer, 2017, pp. 201–21, doi:<a href=\"https://doi.org/10.1007/978-3-319-63387-9_10\">10.1007/978-3-319-63387-9_10</a>.","ista":"Ashok P, Chatterjee K, Daca P, Kretinsky J, Meggendorfer T. 2017. Value iteration for long run average reward in markov decision processes. CAV: Computer Aided Verification, LNCS, vol. 10426, 201–221.","apa":"Ashok, P., Chatterjee, K., Daca, P., Kretinsky, J., &#38; Meggendorfer, T. (2017). Value iteration for long run average reward in markov decision processes. In R. Majumdar &#38; V. Kunčak (Eds.) (Vol. 10426, pp. 201–221). Presented at the CAV: Computer Aided Verification, Heidelberg, Germany: Springer. <a href=\"https://doi.org/10.1007/978-3-319-63387-9_10\">https://doi.org/10.1007/978-3-319-63387-9_10</a>","ama":"Ashok P, Chatterjee K, Daca P, Kretinsky J, Meggendorfer T. Value iteration for long run average reward in markov decision processes. In: Majumdar R, Kunčak V, eds. Vol 10426. Springer; 2017:201-221. doi:<a href=\"https://doi.org/10.1007/978-3-319-63387-9_10\">10.1007/978-3-319-63387-9_10</a>","chicago":"Ashok, Pranav, Krishnendu Chatterjee, Przemyslaw Daca, Jan Kretinsky, and Tobias Meggendorfer. “Value Iteration for Long Run Average Reward in Markov Decision Processes.” edited by Rupak Majumdar and Viktor Kunčak, 10426:201–21. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-319-63387-9_10\">https://doi.org/10.1007/978-3-319-63387-9_10</a>.","ieee":"P. Ashok, K. Chatterjee, P. Daca, J. Kretinsky, and T. Meggendorfer, “Value iteration for long run average reward in markov decision processes,” presented at the CAV: Computer Aided Verification, Heidelberg, Germany, 2017, vol. 10426, pp. 201–221."},"date_updated":"2021-01-12T08:07:32Z","volume":10426,"department":[{"_id":"KrCh"}],"date_created":"2018-12-11T11:47:41Z","publication_status":"published","intvolume":"     10426","alternative_title":["LNCS"],"title":"Value iteration for long run average reward in markov decision processes","scopus_import":1,"_id":"645","author":[{"first_name":"Pranav","last_name":"Ashok","full_name":"Ashok, Pranav"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Daca, Przemyslaw","last_name":"Daca","first_name":"Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Kretinsky","first_name":"Jan","full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Meggendorfer, Tobias","first_name":"Tobias","last_name":"Meggendorfer"}],"editor":[{"last_name":"Majumdar","first_name":"Rupak","full_name":"Majumdar, Rupak"},{"full_name":"Kunčak, Viktor","first_name":"Viktor","last_name":"Kunčak"}],"publisher":"Springer","ec_funded":1,"quality_controlled":"1","page":"201 - 221"},{"oa":1,"tmp":{"name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)","image":"/images/cc_by.png","short":"CC BY (3.0)","legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode"},"date_published":"2017-08-01T00:00:00Z","type":"conference","file":[{"date_created":"2019-06-04T12:56:52Z","file_size":710185,"checksum":"7c2c9d09970af79026d7e37d9b632ef8","date_updated":"2020-07-14T12:47:33Z","content_type":"application/pdf","file_name":"2017_LIPIcs-Chatterjee.pdf","relation":"main_file","access_level":"open_access","file_id":"6520","creator":"kschuh"}],"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Published Version","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"month":"08","article_number":"18","has_accepted_license":"1","conference":{"name":"CSL: Conference on Computer Science Logic","start_date":"2017-08-20","end_date":"2017-08-24","location":"Stockholm, Sweden"},"language":[{"iso":"eng"}],"doi":"10.4230/LIPICS.CSL.2017.18","day":"01","abstract":[{"text":"Graph games with omega-regular winning conditions provide a mathematical framework to analyze a wide range of problems in the analysis of reactive systems and programs (such as the synthesis of reactive systems, program repair, and the verification of branching time properties). Parity conditions are canonical forms to specify omega-regular winning conditions. Graph games with parity conditions are equivalent to mu-calculus model checking, and thus a very important algorithmic problem. Symbolic algorithms are of great significance because they provide scalable algorithms for the analysis of large finite-state systems, as well as algorithms for the analysis of infinite-state systems with finite quotient. A set-based symbolic algorithm uses the basic set operations and the one-step predecessor operators. We consider graph games with n vertices and parity conditions with c priorities (equivalently, a mu-calculus formula with c alternations of least and greatest fixed points). While many explicit algorithms exist for graph games with parity conditions, for set-based symbolic algorithms there are only two algorithms (notice that we use space to refer to the number of sets stored by a symbolic algorithm): (a) the basic algorithm that requires O(n^c) symbolic operations and linear space; and (b) an improved algorithm that requires O(n^{c/2+1}) symbolic operations but also O(n^{c/2+1}) space (i.e., exponential space). In this work we present two set-based symbolic algorithms for parity games: (a) our first algorithm requires O(n^{c/2+1}) symbolic operations and only requires linear space; and (b) developing on our first algorithm, we present an algorithm that requires O(n^{c/3+1}) symbolic operations and only linear space. We also present the first linear space set-based symbolic algorithm for parity games that requires at most a sub-exponential number of symbolic operations. ","lang":"eng"}],"date_updated":"2025-06-02T08:53:46Z","citation":{"apa":"Chatterjee, K., Dvorák, W., Henzinger, M. H., &#38; Loitzenbauer, V. (2017). Improved set-based symbolic algorithms for parity games (Vol. 82). Presented at the CSL: Conference on Computer Science Logic, Stockholm, Sweden: Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik. <a href=\"https://doi.org/10.4230/LIPICS.CSL.2017.18\">https://doi.org/10.4230/LIPICS.CSL.2017.18</a>","ama":"Chatterjee K, Dvorák W, Henzinger MH, Loitzenbauer V. Improved set-based symbolic algorithms for parity games. In: Vol 82. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik; 2017. doi:<a href=\"https://doi.org/10.4230/LIPICS.CSL.2017.18\">10.4230/LIPICS.CSL.2017.18</a>","ieee":"K. Chatterjee, W. Dvorák, M. H. Henzinger, and V. Loitzenbauer, “Improved set-based symbolic algorithms for parity games,” presented at the CSL: Conference on Computer Science Logic, Stockholm, Sweden, 2017, vol. 82.","chicago":"Chatterjee, Krishnendu, Wolfgang Dvorák, Monika H Henzinger, and Veronika Loitzenbauer. “Improved Set-Based Symbolic Algorithms for Parity Games,” Vol. 82. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, 2017. <a href=\"https://doi.org/10.4230/LIPICS.CSL.2017.18\">https://doi.org/10.4230/LIPICS.CSL.2017.18</a>.","short":"K. Chatterjee, W. Dvorák, M.H. Henzinger, V. Loitzenbauer, in:, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, 2017.","mla":"Chatterjee, Krishnendu, et al. <i>Improved Set-Based Symbolic Algorithms for Parity Games</i>. Vol. 82, 18, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, 2017, doi:<a href=\"https://doi.org/10.4230/LIPICS.CSL.2017.18\">10.4230/LIPICS.CSL.2017.18</a>.","ista":"Chatterjee K, Dvorák W, Henzinger MH, Loitzenbauer V. 2017. Improved set-based symbolic algorithms for parity games. CSL: Conference on Computer Science Logic vol. 82, 18."},"year":"2017","volume":82,"ddc":["004"],"publication_status":"published","department":[{"_id":"KrCh"}],"article_processing_charge":"No","date_created":"2019-06-04T12:42:43Z","title":"Improved set-based symbolic algorithms for parity games","intvolume":"        82","_id":"6519","scopus_import":"1","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Wolfgang","last_name":"Dvorák","full_name":"Dvorák, Wolfgang"},{"orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H","first_name":"Monika H","last_name":"Henzinger","id":"540c9bbd-f2de-11ec-812d-d04a5be85630"},{"full_name":"Loitzenbauer, Veronika","first_name":"Veronika","last_name":"Loitzenbauer"}],"publisher":"Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik","quality_controlled":"1","ec_funded":1,"file_date_updated":"2020-07-14T12:47:33Z"}]