[{"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"}],"page":"367 - 381","ddc":["000"],"publication_status":"published","oa_version":"Submitted Version","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"doi":"10.1007/978-3-319-63121-9_18","publist_id":"7170","day":"25","has_accepted_license":"1","oa":1,"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.","status":"public","publication_identifier":{"isbn":["978-3-319-63120-2"],"issn":["0302-9743"]},"alternative_title":["LNCS"],"publication":"Models, Algorithms, Logics and Tools","scopus_import":"1","series_title":"Theoretical Computer Science and General Issues","quality_controlled":"1","ec_funded":1,"citation":{"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.","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>","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.","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>.","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>.","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>"},"publisher":"Springer","project":[{"name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","call_identifier":"FWF"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"date_updated":"2025-04-15T06:26:15Z","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"last_name":"Doyen","first_name":"Laurent","full_name":"Doyen, Laurent"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A"}],"file":[{"checksum":"b2402766ec02c79801aac634bd8f9f6c","date_created":"2019-11-19T08:06:50Z","access_level":"open_access","creator":"dernst","file_size":192826,"content_type":"application/pdf","file_name":"2017_ModelsAlgorithms_Chatterjee.pdf","file_id":"7048","date_updated":"2020-07-14T12:47:25Z","relation":"main_file"}],"month":"07","article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2018-12-11T11:47:34Z","type":"book_chapter","intvolume":"     10460","language":[{"iso":"eng"}],"volume":10460,"date_published":"2017-07-25T00:00:00Z","_id":"625","title":"The cost of exactness in quantitative reachability","year":"2017","editor":[{"first_name":"Luca","full_name":"Aceto, Luca","last_name":"Aceto"},{"full_name":"Bacci, Giorgio","first_name":"Giorgio","last_name":"Bacci"},{"full_name":"Ingólfsdóttir, Anna","first_name":"Anna","last_name":"Ingólfsdóttir"},{"first_name":"Axel","full_name":"Legay, Axel","last_name":"Legay"},{"full_name":"Mardare, Radu","first_name":"Radu","last_name":"Mardare"}],"file_date_updated":"2020-07-14T12:47:25Z"},{"type":"conference","date_created":"2018-12-11T11:47:35Z","article_processing_charge":"No","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","month":"01","main_file_link":[{"url":"https://arxiv.org/abs/1705.00314","open_access":"1"}],"volume":10426,"intvolume":"     10426","language":[{"iso":"eng"}],"_id":"628","date_published":"2017-01-01T00:00:00Z","external_id":{"isi":["000432196400006"],"arxiv":["1705.00314"]},"year":"2017","editor":[{"full_name":"Majumdar, Rupak","first_name":"Rupak","last_name":"Majumdar"},{"last_name":"Kunčak","first_name":"Viktor","full_name":"Kunčak, Viktor"}],"title":"Automated recurrence analysis for almost linear expected runtime bounds","arxiv":1,"oa_version":"Submitted Version","publication_status":"published","page":"118 - 139","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"}],"day":"01","publist_id":"7166","doi":"10.1007/978-3-319-63387-9_6","conference":{"end_date":"2017-07-28","start_date":"2017-07-24","name":"CAV: Computer Aided Verification","location":"Heidelberg, Germany"},"department":[{"_id":"KrCh"}],"isi":1,"scopus_import":"1","alternative_title":["LNCS"],"publication_identifier":{"isbn":["978-331963386-2"]},"status":"public","oa":1,"project":[{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"}],"date_updated":"2025-09-11T07:28:26Z","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"last_name":"Fu","first_name":"Hongfei","full_name":"Fu, Hongfei"},{"last_name":"Murhekar","first_name":"Aniket","full_name":"Murhekar, Aniket"}],"citation":{"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>","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>.","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.","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>.","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.","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>","short":"K. Chatterjee, H. Fu, A. Murhekar, in:, R. Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 118–139."},"publisher":"Springer","ec_funded":1,"quality_controlled":"1"},{"date_published":"2017-01-01T00:00:00Z","_id":"1009","title":"Optimizing expectation with guarantees in POMDPs","year":"2017","external_id":{"isi":["000485630703107"]},"month":"01","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","article_processing_charge":"No","date_created":"2018-12-11T11:49:40Z","type":"conference","intvolume":"         5","language":[{"iso":"eng"}],"volume":5,"main_file_link":[{"open_access":"1","url":"http://www.aaai.org/ocs/index.php/AAAI/AAAI17/paper/download/14354/14092"}],"oa":1,"acknowledgement":"he research leading to these results was supported by the Austrian Science Fund (FWF) NFN Grant no. S11407-N23 (RiSE/SHiNE); two ERC Starting grants (279307: Graph Games, 279499: inVEST); the Vienna Science and Tech- nology Fund (WWTF) through project ICT15-003; and the People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007-2013) under REA grant agreement no. [291734].","status":"public","publication":"Proceedings of the 31st AAAI Conference on Artificial Intelligence","scopus_import":"1","ec_funded":1,"quality_controlled":"1","publisher":"AAAI Press","citation":{"ama":"Chatterjee K, Novotný P, Pérez G, Raskin J, Zikelic D. Optimizing expectation with guarantees in POMDPs. In: <i>Proceedings of the 31st AAAI Conference on Artificial Intelligence</i>. Vol 5. AAAI Press; 2017:3725-3732.","mla":"Chatterjee, Krishnendu, et al. “Optimizing Expectation with Guarantees in POMDPs.” <i>Proceedings of the 31st AAAI Conference on Artificial Intelligence</i>, vol. 5, AAAI Press, 2017, pp. 3725–32.","ieee":"K. Chatterjee, P. Novotný, G. Pérez, J. Raskin, and D. Zikelic, “Optimizing expectation with guarantees in POMDPs,” in <i>Proceedings of the 31st AAAI Conference on Artificial Intelligence</i>, San Francisco, CA, United States, 2017, vol. 5, pp. 3725–3732.","chicago":"Chatterjee, Krishnendu, Petr Novotný, Guillermo Pérez, Jean Raskin, and Djordje Zikelic. “Optimizing Expectation with Guarantees in POMDPs.” In <i>Proceedings of the 31st AAAI Conference on Artificial Intelligence</i>, 5:3725–32. AAAI Press, 2017.","ista":"Chatterjee K, Novotný P, Pérez G, Raskin J, Zikelic D. 2017. Optimizing expectation with guarantees in POMDPs. Proceedings of the 31st AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 5, 3725–3732.","apa":"Chatterjee, K., Novotný, P., Pérez, G., Raskin, J., &#38; Zikelic, D. (2017). Optimizing expectation with guarantees in POMDPs. In <i>Proceedings of the 31st AAAI Conference on Artificial Intelligence</i> (Vol. 5, pp. 3725–3732). San Francisco, CA, United States: AAAI Press.","short":"K. Chatterjee, P. Novotný, G. Pérez, J. Raskin, D. Zikelic, in:, Proceedings of the 31st AAAI Conference on Artificial Intelligence, AAAI Press, 2017, pp. 3725–3732."},"project":[{"name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"},{"call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734","name":"International IST Postdoc Fellowship Programme"},{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"}],"date_updated":"2025-04-14T13:51:03Z","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Novotny, Petr","first_name":"Petr","last_name":"Novotny","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Pérez","full_name":"Pérez, Guillermo","first_name":"Guillermo"},{"full_name":"Raskin, Jean","first_name":"Jean","last_name":"Raskin"},{"full_name":"Zikelic, Djordje","first_name":"Djordje","last_name":"Zikelic"}],"abstract":[{"lang":"eng","text":"A standard objective in partially-observable Markov decision processes (POMDPs) is to find a policy that maximizes the expected discounted-sum payoff. However, such policies may still permit unlikely but highly undesirable outcomes, which is problematic especially in safety-critical applications. Recently, there has been a surge of interest in POMDPs where the goal is to maximize the probability to ensure that the payoff is at least a given threshold, but these approaches do not consider any optimization beyond satisfying this threshold constraint. In this work we go beyond both the “expectation” and “threshold” approaches and consider a “guaranteed payoff optimization (GPO)” problem for POMDPs, where we are given a threshold t and the objective is to find a policy σ such that a) each possible outcome of σ yields a discounted-sum payoff of at least t, and b) the expected discounted-sum payoff of σ is optimal (or near-optimal) among all policies satisfying a). We present a practical approach to tackle the GPO problem and evaluate it on standard POMDP benchmarks."}],"page":"3725 - 3732","publication_status":"published","oa_version":"Submitted Version","isi":1,"department":[{"_id":"KrCh"}],"conference":{"start_date":"2017-02-04","end_date":"2017-02-10","location":"San Francisco, CA, United States","name":"AAAI: Conference on Artificial Intelligence"},"day":"01","publist_id":"6387"},{"publist_id":"6384","day":"19","doi":"10.1007/978-3-662-54434-1_11","conference":{"end_date":"2017-04-29","start_date":"2017-04-22","location":"Uppsala, Sweden","name":"ESOP: European Symposium on Programming"},"isi":1,"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"oa_version":"Submitted Version","publication_status":"published","abstract":[{"lang":"eng","text":"Pushdown systems (PDSs) and recursive state machines (RSMs), which are linearly equivalent, are standard models for interprocedural analysis. Yet RSMs are more convenient as they (a) explicitly model function calls and returns, and (b) specify many natural parameters for algorithmic analysis, e.g., the number of entries and exits. We consider a general framework where RSM transitions are labeled from a semiring and path properties are algebraic with semiring operations, which can model, e.g., interprocedural reachability and dataflow analysis problems. Our main contributions are new algorithms for several fundamental problems. As compared to a direct translation of RSMs to PDSs and the best-known existing bounds of PDSs, our analysis algorithm improves the complexity for finite-height semirings (that subsumes reachability and standard dataflow properties). We further consider the problem of extracting distance values from the representation structures computed by our algorithm, and give efficient algorithms that distinguish the complexity of a one-time preprocessing from the complexity of each individual query. Another advantage of our algorithm is that our improvements carry over to the concurrent setting, where we improve the bestknown complexity for the context-bounded analysis of concurrent RSMs. Finally, we provide a prototype implementation that gives a significant speed-up on several benchmarks from the SLAM/SDV project."}],"page":"287 - 313","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Kragl","id":"320FC952-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-7745-9117","first_name":"Bernhard","full_name":"Kragl, Bernhard"},{"last_name":"Mishra","full_name":"Mishra, Samarth","first_name":"Samarth"},{"full_name":"Pavlogiannis, Andreas","first_name":"Andreas","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87"}],"project":[{"call_identifier":"FWF","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory"},{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"}],"date_updated":"2025-06-04T08:09:18Z","citation":{"ista":"Chatterjee K, Kragl B, Mishra S, Pavlogiannis A. 2017. Faster algorithms for weighted recursive state machines. ESOP: European Symposium on Programming, LNCS, vol. 10201, 287–313.","chicago":"Chatterjee, Krishnendu, Bernhard Kragl, Samarth Mishra, and Andreas Pavlogiannis. “Faster Algorithms for Weighted Recursive State Machines.” edited by Hongseok Yang, 10201:287–313. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-662-54434-1_11\">https://doi.org/10.1007/978-3-662-54434-1_11</a>.","ieee":"K. Chatterjee, B. Kragl, S. Mishra, and A. Pavlogiannis, “Faster algorithms for weighted recursive state machines,” presented at the ESOP: European Symposium on Programming, Uppsala, Sweden, 2017, vol. 10201, pp. 287–313.","short":"K. Chatterjee, B. Kragl, S. Mishra, A. Pavlogiannis, in:, H. Yang (Ed.), Springer, 2017, pp. 287–313.","apa":"Chatterjee, K., Kragl, B., Mishra, S., &#38; Pavlogiannis, A. (2017). Faster algorithms for weighted recursive state machines. In H. Yang (Ed.) (Vol. 10201, pp. 287–313). Presented at the ESOP: European Symposium on Programming, Uppsala, Sweden: Springer. <a href=\"https://doi.org/10.1007/978-3-662-54434-1_11\">https://doi.org/10.1007/978-3-662-54434-1_11</a>","ama":"Chatterjee K, Kragl B, Mishra S, Pavlogiannis A. Faster algorithms for weighted recursive state machines. In: Yang H, ed. Vol 10201. Springer; 2017:287-313. doi:<a href=\"https://doi.org/10.1007/978-3-662-54434-1_11\">10.1007/978-3-662-54434-1_11</a>","mla":"Chatterjee, Krishnendu, et al. <i>Faster Algorithms for Weighted Recursive State Machines</i>. Edited by Hongseok Yang, vol. 10201, Springer, 2017, pp. 287–313, doi:<a href=\"https://doi.org/10.1007/978-3-662-54434-1_11\">10.1007/978-3-662-54434-1_11</a>."},"publisher":"Springer","quality_controlled":"1","ec_funded":1,"alternative_title":["LNCS"],"scopus_import":"1","status":"public","publication_identifier":{"issn":["0302-9743"]},"oa":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1701.04914"}],"volume":10201,"language":[{"iso":"eng"}],"intvolume":"     10201","type":"conference","date_created":"2018-12-11T11:49:41Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","month":"03","external_id":{"arxiv":["1701.04914"],"isi":["000681702400011"]},"year":"2017","editor":[{"full_name":"Yang, Hongseok","first_name":"Hongseok","last_name":"Yang"}],"arxiv":1,"title":"Faster algorithms for weighted recursive state machines","_id":"1011","date_published":"2017-03-19T00:00:00Z"},{"abstract":[{"lang":"eng","text":"A fundamental algorithmic problem at the heart of static analysis is Dyck reachability. The input is a graph where the edges are labeled with different types of opening and closing parentheses, and the reachability information is computed via paths whose parentheses are properly matched. We present new results for Dyck reachability 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 as follows: First, we consider Dyck reachability on bidirected graphs, which is the standard way of performing field-sensitive points-to analysis. Given a bidirected graph with n nodes and m edges, we present: (i) an algorithm with worst-case running time O(m + n · α(n)), where α(n) is the inverse Ackermann function, improving the previously known O(n2) time bound; (ii) a matching lower bound that shows that our algorithm is optimal wrt to worst-case complexity; and (iii) an optimal average-case upper bound of O(m) time, improving the previously known O(m · logn) bound. Second, we consider the problem of context-sensitive data-dependence analysis, where the task is to obtain analysis summaries of library code in the presence of callbacks. Our algorithm preprocesses libraries in almost linear 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 Matrix Multiplication, which is a long-standing open problem. Thus we establish that the existing combinatorial algorithms for Dyck reachability are (conditionally) optimal for general graphs. We also show that the same hardness holds for graphs of constant treewidth. Finally, we provide a prototype implementation of our algorithms for both alias analysis and data-dependence analysis. Our experimental evaluation demonstrates that the new algorithms significantly outperform all existing methods on the two problems, over real-world benchmarks."}],"corr_author":"1","publication_status":"published","ddc":["000"],"oa_version":"Published Version","department":[{"_id":"KrCh"}],"conference":{"start_date":"2018-01-07","end_date":"2018-01-13","name":"POPL: Programming Languages","location":"Los Angeles, CA, United States"},"doi":"10.1145/3158118","article_number":"30","has_accepted_license":"1","day":"27","oa":1,"acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No P23499-N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE), and ERC Start grant (279307: Graph Games).\r\n","publication_identifier":{"eissn":["2475-1421"]},"status":"public","publication":"Proceedings of the ACM on Programming Languages","scopus_import":"1","quality_controlled":"1","ec_funded":1,"related_material":{"record":[{"relation":"earlier_version","id":"5455","status":"public"}]},"publisher":"Association for Computing Machinery","citation":{"mla":"Chatterjee, Krishnendu, et al. “Optimal Dyck Reachability for Data-Dependence and Alias Analysis.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 2, no. POPL, 30, Association for Computing Machinery, 2017, doi:<a href=\"https://doi.org/10.1145/3158118\">10.1145/3158118</a>.","ama":"Chatterjee K, Choudhary B, Pavlogiannis A. Optimal Dyck reachability for data-dependence and Alias analysis. <i>Proceedings of the ACM on Programming Languages</i>. 2017;2(POPL). doi:<a href=\"https://doi.org/10.1145/3158118\">10.1145/3158118</a>","short":"K. Chatterjee, B. Choudhary, A. Pavlogiannis, Proceedings of the ACM on Programming Languages 2 (2017).","apa":"Chatterjee, K., Choudhary, B., &#38; Pavlogiannis, A. (2017). Optimal Dyck reachability for data-dependence and Alias analysis. <i>Proceedings of the ACM on Programming Languages</i>. Los Angeles, CA, United States: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3158118\">https://doi.org/10.1145/3158118</a>","ieee":"K. Chatterjee, B. Choudhary, and A. Pavlogiannis, “Optimal Dyck reachability for data-dependence and Alias analysis,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 2, no. POPL. Association for Computing Machinery, 2017.","ista":"Chatterjee K, Choudhary B, Pavlogiannis A. 2017. Optimal Dyck reachability for data-dependence and Alias analysis. Proceedings of the ACM on Programming Languages. 2(POPL), 30.","chicago":"Chatterjee, Krishnendu, Bhavya Choudhary, and Andreas Pavlogiannis. “Optimal Dyck Reachability for Data-Dependence and Alias Analysis.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2017. <a href=\"https://doi.org/10.1145/3158118\">https://doi.org/10.1145/3158118</a>."},"project":[{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"}],"author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"first_name":"Bhavya","full_name":"Choudhary, Bhavya","last_name":"Choudhary"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","first_name":"Andreas"}],"date_updated":"2025-04-15T07:26:20Z","file":[{"content_type":"application/pdf","file_size":460188,"creator":"cchlebak","access_level":"open_access","date_created":"2021-12-07T08:06:28Z","checksum":"faa3f7b3fe8aab84b50ed805c26a0ee5","relation":"main_file","date_updated":"2021-12-07T08:06:28Z","file_id":"10421","success":1,"file_name":"2017_ACMProgLang_Chatterjee.pdf"}],"article_type":"original","month":"12","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","article_processing_charge":"No","date_created":"2021-12-05T23:01:48Z","type":"journal_article","intvolume":"         2","language":[{"iso":"eng"}],"volume":2,"issue":"POPL","date_published":"2017-12-27T00:00:00Z","_id":"10416","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)"},"title":"Optimal Dyck reachability for data-dependence and Alias analysis","arxiv":1,"year":"2017","external_id":{"arxiv":["1910.00241"]},"file_date_updated":"2021-12-07T08:06:28Z"},{"doi":"10.1145/3158121","article_number":"33","day":"07","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"conference":{"end_date":"2018-01-13","start_date":"2018-01-07","location":"Los Angeles, CA, United States","name":"POPL: Programming Languages"},"oa_version":"Published Version","abstract":[{"text":"We present a new proof rule for proving almost-sure termination of probabilistic programs, including those that contain demonic non-determinism. An important question for a probabilistic program is whether the probability mass of all its diverging runs is zero, that is that it terminates \"almost surely\". Proving that can be hard, and this paper presents a new method for doing so. It applies directly to the program's source code, even if the program contains demonic choice. Like others, we use variant functions (a.k.a. \"super-martingales\") that are real-valued and decrease randomly on each loop iteration; but our key innovation is that the amount as well as the probability of the decrease are parametric. We prove the soundness of the new rule, indicate where its applicability goes beyond existing rules, and explain its connection to classical results on denumerable (non-demonic) Markov chains.","lang":"eng"}],"corr_author":"1","publication_status":"published","ddc":["000"],"citation":{"mla":"Mciver, Annabelle, et al. “A New Proof Rule for Almost-Sure Termination.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 2, no. POPL, 33, Association for Computing Machinery, 2017, doi:<a href=\"https://doi.org/10.1145/3158121\">10.1145/3158121</a>.","ama":"Mciver A, Morgan C, Kaminski BL, Katoen JP. A new proof rule for almost-sure termination. <i>Proceedings of the ACM on Programming Languages</i>. 2017;2(POPL). doi:<a href=\"https://doi.org/10.1145/3158121\">10.1145/3158121</a>","short":"A. Mciver, C. Morgan, B.L. Kaminski, J.P. Katoen, Proceedings of the ACM on Programming Languages 2 (2017).","apa":"Mciver, A., Morgan, C., Kaminski, B. L., &#38; Katoen, J. P. (2017). A new proof rule for almost-sure termination. <i>Proceedings of the ACM on Programming Languages</i>. Los Angeles, CA, United States: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3158121\">https://doi.org/10.1145/3158121</a>","ieee":"A. Mciver, C. Morgan, B. L. Kaminski, and J. P. Katoen, “A new proof rule for almost-sure termination,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 2, no. POPL. Association for Computing Machinery, 2017.","chicago":"Mciver, Annabelle, Carroll Morgan, Benjamin Lucien Kaminski, and Joost P Katoen. “A New Proof Rule for Almost-Sure Termination.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2017. <a href=\"https://doi.org/10.1145/3158121\">https://doi.org/10.1145/3158121</a>.","ista":"Mciver A, Morgan C, Kaminski BL, Katoen JP. 2017. A new proof rule for almost-sure termination. Proceedings of the ACM on Programming Languages. 2(POPL), 33."},"publisher":"Association for Computing Machinery","author":[{"full_name":"Mciver, Annabelle","first_name":"Annabelle","last_name":"Mciver"},{"first_name":"Carroll","full_name":"Morgan, Carroll","last_name":"Morgan"},{"last_name":"Kaminski","full_name":"Kaminski, Benjamin Lucien","first_name":"Benjamin Lucien"},{"last_name":"Katoen","id":"4524F760-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-6143-1926","first_name":"Joost P","full_name":"Katoen, Joost P"}],"date_updated":"2026-06-18T08:40:04Z","quality_controlled":"1","publication":"Proceedings of the ACM on Programming Languages","scopus_import":"1","oa":1,"acknowledgement":"McIver and Morgan are grateful to David Basin and the Information Security Group at ETH Zürich for hosting a six-month stay in Switzerland, during part of which this work began. And thanks particularly to Andreas Lochbihler, who shared with us the probabilistic termination problem that led to it. They acknowledge the support of ARC grant DP140101119. Part of this work was carried out during the Workshop on Probabilistic Programming Semantics\r\nat McGill University’s Bellairs Research Institute on Barbados organised by Alexandra Silva and\r\nPrakash Panangaden. Kaminski and Katoen are grateful to Sebastian Junges for spotting a flaw in §5.4.","publication_identifier":{"eissn":["2475-1421"]},"status":"public","issue":"POPL","main_file_link":[{"open_access":"1","url":"https://dl.acm.org/doi/10.1145/3158121"}],"language":[{"iso":"eng"}],"intvolume":"         2","volume":2,"date_created":"2021-12-05T23:01:49Z","type":"journal_article","month":"12","article_type":"original","article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","external_id":{"arxiv":["1711.03588"]},"title":"A new proof rule for almost-sure termination","arxiv":1,"year":"2017","date_published":"2017-12-07T00:00:00Z","_id":"10418"},{"volume":122,"language":[{"iso":"eng"}],"intvolume":"       122","type":"journal_article","date_created":"2018-12-11T11:49:57Z","article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"06","file":[{"creator":"system","date_created":"2018-12-12T10:13:17Z","access_level":"open_access","content_type":"application/pdf","file_size":247657,"file_name":"IST-2018-991-v1+2_2018_Chatterjee_Pushdown_PREPRINT.pdf","file_id":"4998","relation":"main_file","date_updated":"2019-10-15T07:44:51Z"}],"file_date_updated":"2019-10-15T07:44:51Z","external_id":{"isi":["000399506600005"]},"year":"2017","title":"Pushdown reachability with constant treewidth","_id":"1065","date_published":"2017-06-01T00:00:00Z","has_accepted_license":"1","publist_id":"6323","day":"01","doi":"10.1016/j.ipl.2017.02.003","isi":1,"department":[{"_id":"KrCh"},{"_id":"HeEd"}],"oa_version":"Submitted Version","ddc":["000"],"publication_status":"published","abstract":[{"lang":"eng","text":"We consider the problem of reachability in pushdown graphs. We study the problem for pushdown graphs with constant treewidth. Even for pushdown graphs with treewidth 1, for the reachability problem we establish the following: (i) the problem is PTIME-complete, and (ii) any subcubic algorithm for the problem would contradict the k-clique conjecture and imply faster combinatorial algorithms for cliques in graphs."}],"page":"25 - 29","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407"},{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7"}],"pubrep_id":"991","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"orcid":"0000-0002-8882-5116","id":"464B40D6-F248-11E8-B48F-1D18A9856A87","last_name":"Osang","first_name":"Georg F","full_name":"Osang, Georg F"}],"date_updated":"2025-07-10T11:49:53Z","publisher":"Elsevier","citation":{"mla":"Chatterjee, Krishnendu, and Georg F. Osang. “Pushdown Reachability with Constant Treewidth.” <i>Information Processing Letters</i>, vol. 122, Elsevier, 2017, pp. 25–29, doi:<a href=\"https://doi.org/10.1016/j.ipl.2017.02.003\">10.1016/j.ipl.2017.02.003</a>.","ama":"Chatterjee K, Osang GF. Pushdown reachability with constant treewidth. <i>Information Processing Letters</i>. 2017;122:25-29. doi:<a href=\"https://doi.org/10.1016/j.ipl.2017.02.003\">10.1016/j.ipl.2017.02.003</a>","apa":"Chatterjee, K., &#38; Osang, G. F. (2017). Pushdown reachability with constant treewidth. <i>Information Processing Letters</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ipl.2017.02.003\">https://doi.org/10.1016/j.ipl.2017.02.003</a>","short":"K. Chatterjee, G.F. Osang, Information Processing Letters 122 (2017) 25–29.","ieee":"K. Chatterjee and G. F. Osang, “Pushdown reachability with constant treewidth,” <i>Information Processing Letters</i>, vol. 122. Elsevier, pp. 25–29, 2017.","chicago":"Chatterjee, Krishnendu, and Georg F Osang. “Pushdown Reachability with Constant Treewidth.” <i>Information Processing Letters</i>. Elsevier, 2017. <a href=\"https://doi.org/10.1016/j.ipl.2017.02.003\">https://doi.org/10.1016/j.ipl.2017.02.003</a>.","ista":"Chatterjee K, Osang GF. 2017. Pushdown reachability with constant treewidth. Information Processing Letters. 122, 25–29."},"quality_controlled":"1","ec_funded":1,"publication":"Information Processing Letters","scopus_import":"1","status":"public","publication_identifier":{"issn":["0020-0190"]},"oa":1},{"page":"143 - 166","abstract":[{"lang":"eng","text":"Simulation is an attractive alternative to language inclusion for automata as it is an under-approximation of language inclusion, but usually has much lower complexity. Simulation has also been extended in two orthogonal directions, namely, (1) fair simulation, for simulation over specified set of infinite runs; and (2) quantitative simulation, for simulation between weighted automata. While fair trace inclusion is PSPACE-complete, fair simulation can be computed in polynomial time. For weighted automata, the (quantitative) language inclusion problem is undecidable in general, whereas the (quantitative) simulation reduces to quantitative games, which admit pseudo-polynomial time algorithms.\r\n\r\nIn this work, we study (quantitative) simulation for weighted automata with Büchi acceptance conditions, i.e., we generalize fair simulation from non-weighted automata to weighted automata. We show that imposing Büchi acceptance conditions on weighted automata changes many fundamental properties of the simulation games, yet they still admit pseudo-polynomial time algorithms."}],"corr_author":"1","publication_status":"published","ddc":["000"],"oa_version":"Published Version","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"isi":1,"doi":"10.1016/j.ic.2016.10.006","day":"01","publist_id":"6322","acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreements 267989 (QUAREM), 279307 (Graph Games), by the Austrian Science Fund (FWF) projects S11402-N23 (RiSE), S11407-N23 (RiSE), P23499-N23, and Microsoft faculty fellows award.","oa":1,"status":"public","OA_type":"free access","scopus_import":"1","publication":"Information and Computation","quality_controlled":"1","ec_funded":1,"publisher":"Elsevier","related_material":{"record":[{"id":"5428","status":"public","relation":"earlier_version"}]},"citation":{"apa":"Chatterjee, K., Henzinger, T. A., Otop, J., &#38; Velner, Y. (2017). Quantitative fair simulation games. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2016.10.006\">https://doi.org/10.1016/j.ic.2016.10.006</a>","short":"K. Chatterjee, T.A. Henzinger, J. Otop, Y. Velner, Information and Computation 254 (2017) 143–166.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Yaron Velner. “Quantitative Fair Simulation Games.” <i>Information and Computation</i>. Elsevier, 2017. <a href=\"https://doi.org/10.1016/j.ic.2016.10.006\">https://doi.org/10.1016/j.ic.2016.10.006</a>.","ieee":"K. Chatterjee, T. A. Henzinger, J. Otop, and Y. Velner, “Quantitative fair simulation games,” <i>Information and Computation</i>, vol. 254, no. 2. Elsevier, pp. 143–166, 2017.","ista":"Chatterjee K, Henzinger TA, Otop J, Velner Y. 2017. Quantitative fair simulation games. Information and Computation. 254(2), 143–166.","mla":"Chatterjee, Krishnendu, et al. “Quantitative Fair Simulation Games.” <i>Information and Computation</i>, vol. 254, no. 2, Elsevier, 2017, pp. 143–66, doi:<a href=\"https://doi.org/10.1016/j.ic.2016.10.006\">10.1016/j.ic.2016.10.006</a>.","ama":"Chatterjee K, Henzinger TA, Otop J, Velner Y. Quantitative fair simulation games. <i>Information and Computation</i>. 2017;254(2):143-166. doi:<a href=\"https://doi.org/10.1016/j.ic.2016.10.006\">10.1016/j.ic.2016.10.006</a>"},"project":[{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","full_name":"Otop, Jan","first_name":"Jan"},{"last_name":"Velner","full_name":"Velner, Yaron","first_name":"Yaron"}],"date_updated":"2026-06-18T08:47:01Z","article_type":"original","month":"06","article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2018-12-11T11:49:58Z","type":"journal_article","intvolume":"       254","language":[{"iso":"eng"}],"volume":254,"issue":"2","OA_place":"publisher","main_file_link":[{"open_access":"1","url":"https://doi.org/10.1016/j.ic.2016.10.006"}],"date_published":"2017-06-01T00:00:00Z","_id":"1066","title":"Quantitative fair simulation games","year":"2017","external_id":{"isi":["000402025600002"]}},{"date_published":"2017-01-31T00:00:00Z","_id":"1080","title":"Reconstructing metastatic seeding patterns of human cancers","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)"},"year":"2017","external_id":{"isi":["000393096600001"]},"file_date_updated":"2018-12-12T10:15:15Z","file":[{"file_name":"IST-2017-786-v1+1_ncomms14114.pdf","file_id":"5133","date_updated":"2018-12-12T10:15:15Z","relation":"main_file","access_level":"open_access","creator":"system","date_created":"2018-12-12T10:15:15Z","file_size":897050,"content_type":"application/pdf"}],"month":"01","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","date_created":"2018-12-11T11:50:02Z","type":"journal_article","language":[{"iso":"eng"}],"intvolume":"         8","volume":8,"oa":1,"status":"public","publication_identifier":{"issn":["2041-1723"]},"scopus_import":"1","publication":"Nature Communications","ec_funded":1,"quality_controlled":"1","publisher":"Nature Publishing Group","citation":{"ista":"Reiter J, Makohon Moore A, Gerold J, Božić I, Chatterjee K, Iacobuzio Donahue C, Vogelstein B, Nowak M. 2017. Reconstructing metastatic seeding patterns of human cancers. Nature Communications. 8, 14114.","ieee":"J. Reiter <i>et al.</i>, “Reconstructing metastatic seeding patterns of human cancers,” <i>Nature Communications</i>, vol. 8. Nature Publishing Group, 2017.","chicago":"Reiter, Johannes, Alvin Makohon Moore, Jeffrey Gerold, Ivana Božić, Krishnendu Chatterjee, Christine Iacobuzio Donahue, Bert Vogelstein, and Martin Nowak. “Reconstructing Metastatic Seeding Patterns of Human Cancers.” <i>Nature Communications</i>. Nature Publishing Group, 2017. <a href=\"https://doi.org/10.1038/ncomms14114\">https://doi.org/10.1038/ncomms14114</a>.","apa":"Reiter, J., Makohon Moore, A., Gerold, J., Božić, I., Chatterjee, K., Iacobuzio Donahue, C., … Nowak, M. (2017). Reconstructing metastatic seeding patterns of human cancers. <i>Nature Communications</i>. Nature Publishing Group. <a href=\"https://doi.org/10.1038/ncomms14114\">https://doi.org/10.1038/ncomms14114</a>","short":"J. Reiter, A. Makohon Moore, J. Gerold, I. Božić, K. Chatterjee, C. Iacobuzio Donahue, B. Vogelstein, M. Nowak, Nature Communications 8 (2017).","ama":"Reiter J, Makohon Moore A, Gerold J, et al. Reconstructing metastatic seeding patterns of human cancers. <i>Nature Communications</i>. 2017;8. doi:<a href=\"https://doi.org/10.1038/ncomms14114\">10.1038/ncomms14114</a>","mla":"Reiter, Johannes, et al. “Reconstructing Metastatic Seeding Patterns of Human Cancers.” <i>Nature Communications</i>, vol. 8, 14114, Nature Publishing Group, 2017, doi:<a href=\"https://doi.org/10.1038/ncomms14114\">10.1038/ncomms14114</a>."},"author":[{"id":"4A918E98-F248-11E8-B48F-1D18A9856A87","last_name":"Reiter","orcid":"0000-0002-0170-7353","first_name":"Johannes","full_name":"Reiter, Johannes"},{"last_name":"Makohon Moore","first_name":"Alvin","full_name":"Makohon Moore, Alvin"},{"full_name":"Gerold, Jeffrey","first_name":"Jeffrey","last_name":"Gerold"},{"last_name":"Božić","full_name":"Božić, Ivana","first_name":"Ivana"},{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"first_name":"Christine","full_name":"Iacobuzio Donahue, Christine","last_name":"Iacobuzio Donahue"},{"full_name":"Vogelstein, Bert","first_name":"Bert","last_name":"Vogelstein"},{"full_name":"Nowak, Martin","first_name":"Martin","last_name":"Nowak"}],"project":[{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7"},{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"call_identifier":"FWF","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory"}],"pubrep_id":"786","date_updated":"2025-07-10T11:50:00Z","abstract":[{"lang":"eng","text":"Reconstructing the evolutionary history of metastases is critical for understanding their basic biological principles and has profound clinical implications. Genome-wide sequencing data has enabled modern phylogenomic methods to accurately dissect subclones and their phylogenies from noisy and impure bulk tumour samples at unprecedented depth. However, existing methods are not designed to infer metastatic seeding patterns. Here we develop a tool, called Treeomics, to reconstruct the phylogeny of metastases and map subclones to their anatomic locations. Treeomics infers comprehensive seeding patterns for pancreatic, ovarian, and prostate cancers. Moreover, Treeomics correctly disambiguates true seeding patterns from sequencing artifacts; 7% of variants were misclassified by conventional statistical methods. These artifacts can skew phylogenies by creating illusory tumour heterogeneity among distinct samples. In silico benchmarking on simulated tumour phylogenies across a wide range of sample purities (15–95%) and sequencing depths (25-800 × ) demonstrates the accuracy of Treeomics compared with existing methods."}],"ddc":["004","006"],"publication_status":"published","oa_version":"Published Version","isi":1,"department":[{"_id":"KrCh"}],"article_number":"14114","doi":"10.1038/ncomms14114","day":"31","has_accepted_license":"1","publist_id":"6301"},{"file_date_updated":"2020-07-14T12:48:10Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode","short":"CC BY-ND (4.0)","image":"/image/cc_by_nd.png","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)"},"title":"Algorithmic advances in program analysis and their applications","year":"2017","date_published":"2017-08-09T00:00:00Z","_id":"821","OA_place":"publisher","language":[{"iso":"eng"}],"degree_awarded":"PhD","date_created":"2018-12-11T11:48:41Z","type":"dissertation","file":[{"file_name":"IST-2017-854-v1+1_Pavlogiannis_Thesis_PubRep.pdf","file_id":"4900","date_updated":"2020-07-14T12:48:10Z","relation":"main_file","checksum":"3a3ec003f6ee73f41f82a544d63dfc77","date_created":"2018-12-12T10:11:44Z","access_level":"open_access","creator":"system","file_size":4103115,"content_type":"application/pdf"},{"file_name":"2017_thesis_Pavlogiannis.zip","file_id":"6201","relation":"source_file","date_updated":"2020-07-14T12:48:10Z","checksum":"bd2facc45ff8a2e20c5ed313c2ccaa83","creator":"dernst","access_level":"closed","date_created":"2019-04-05T07:59:31Z","content_type":"application/zip","file_size":14744374}],"month":"08","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","article_processing_charge":"No","related_material":{"record":[{"relation":"part_of_dissertation","status":"public","id":"1602"},{"status":"public","id":"1604","relation":"part_of_dissertation"},{"relation":"part_of_dissertation","status":"public","id":"1437"},{"relation":"part_of_dissertation","status":"public","id":"1071"},{"relation":"part_of_dissertation","status":"public","id":"1607"},{"id":"1714","status":"public","relation":"part_of_dissertation"}]},"publisher":"Institute of Science and Technology Austria","citation":{"ama":"Pavlogiannis A. Algorithmic advances in program analysis and their applications. 2017. doi:<a href=\"https://doi.org/10.15479/AT:ISTA:th_854\">10.15479/AT:ISTA:th_854</a>","mla":"Pavlogiannis, Andreas. <i>Algorithmic Advances in Program Analysis and Their Applications</i>. Institute of Science and Technology Austria, 2017, doi:<a href=\"https://doi.org/10.15479/AT:ISTA:th_854\">10.15479/AT:ISTA:th_854</a>.","chicago":"Pavlogiannis, Andreas. “Algorithmic Advances in Program Analysis and Their Applications.” Institute of Science and Technology Austria, 2017. <a href=\"https://doi.org/10.15479/AT:ISTA:th_854\">https://doi.org/10.15479/AT:ISTA:th_854</a>.","ista":"Pavlogiannis A. 2017. Algorithmic advances in program analysis and their applications. Institute of Science and Technology Austria.","ieee":"A. Pavlogiannis, “Algorithmic advances in program analysis and their applications,” Institute of Science and Technology Austria, 2017.","short":"A. Pavlogiannis, Algorithmic Advances in Program Analysis and Their Applications, Institute of Science and Technology Austria, 2017.","apa":"Pavlogiannis, A. (2017). <i>Algorithmic advances in program analysis and their applications</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT:ISTA:th_854\">https://doi.org/10.15479/AT:ISTA:th_854</a>"},"date_updated":"2026-04-08T14:22:17Z","pubrep_id":"854","project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"author":[{"last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","first_name":"Andreas"}],"ec_funded":1,"alternative_title":["ISTA Thesis"],"oa":1,"acknowledgement":"First, I am thankful to my advisor, Krishnendu Chatterjee, for offering me the opportunity to\r\nmaterialize my scientific curiosity in a remarkably wide range of interesting topics, as well as for his constant availability and continuous support throughout my doctoral studies. I have had the privilege of collaborating with, discussing and getting inspired by all members of my committee: Thomas A. Henzinger, Ulrich Schmid and Martin A. Nowak. The role of the above four people has been very instrumental both to the research carried out for this dissertation, and to the researcher I evolved to in the process.\r\nI have greatly enjoyed my numerous brainstorming sessions with Rasmus Ibsen-Jensen, many\r\nof which led to results on low-treewidth graphs presented here.  I thank Alex Kößler for our\r\ndiscussions on modeling and analyzing real-time scheduling algorithms, Yaron Velner for our\r\ncollaboration on the Quantitative Interprocedural Analysis framework, and Nishant Sinha for our initial discussions on partial order reduction techniques in stateless model checking. I also thank Jan Otop, Ben Adlam, Bernhard Kragl and Josef Tkadlec for our fruitful collaborations on\r\ntopics outside the scope of this dissertation, as well as the interns Prateesh Goyal, Amir Kafshdar Goharshady, Samarth Mishra, Bhavya Choudhary and Marek Chalupa, with whom I have shared my excitement on various research topics. Together with my collaborators, I thank officemates and members of the Chatterjee and Henzinger groups throughout the years, Thorsten Tarrach, Ventsi Chonev, Roopsha Samanta, Przemek Daca, Mirco Giacobbe, Tanja Petrov, Ashutosh\r\nGupta,  Arjun Radhakrishna,  Petr Novontý,  Christian Hilbe,  Jakob Ruess,  Martin Chmelik,\r\nCezara Dragoi, Johannes Reiter, Andrey Kupriyanov, Guy Avni, Sasha Rubin, Jessica Davies, Hongfei Fu, Thomas Ferrère, Pavol Cerný, Ali Sezgin, Jan Kretínský, Sergiy Bogomolov, Hui\r\nKong, Benjamin Aminof, Duc-Hiep Chu, and Damien Zufferey.  Besides collaborations and office spaces, with many of the above people I have been fortunate to share numerous whiteboard\r\ndiscussions, as well as memorable long walks and amicable meals accompanied by stimulating\r\nconversations. I am highly indebted to Elisabeth Hacker for her continuous assistance in matters\r\nthat often exceeded her official duties, and who made my integration in Austria a smooth process.","publication_identifier":{"issn":["2663-337X"]},"status":"public","doi":"10.15479/AT:ISTA:th_854","has_accepted_license":"1","day":"09","publist_id":"6828","department":[{"_id":"KrCh"}],"oa_version":"Published Version","supervisor":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"}],"page":"418","corr_author":"1","abstract":[{"text":"This dissertation focuses on algorithmic aspects of program verification, and presents modeling and complexity advances on several problems related to the\r\nstatic analysis of programs, the stateless model checking of concurrent programs, and the competitive analysis of real-time scheduling algorithms.\r\nOur contributions can be broadly grouped into five categories.\r\n\r\nOur first contribution is a set of new algorithms and data structures for the quantitative and data-flow analysis of programs, based on the graph-theoretic notion of treewidth.\r\nIt has been observed that the control-flow graphs of typical programs have special structure, and are characterized as graphs of small treewidth.\r\nWe utilize this structural property to provide faster algorithms for the quantitative and data-flow analysis of recursive and concurrent programs.\r\nIn most cases we make an algebraic treatment of the considered problem,\r\nwhere several interesting analyses, such as the reachability, shortest path, and certain kind of data-flow analysis problems follow as special cases. \r\nWe exploit the constant-treewidth property to obtain algorithmic improvements for on-demand versions of the problems, \r\nand provide data structures with various tradeoffs between the resources spent in the preprocessing and querying phase.\r\nWe also improve on the algorithmic complexity of quantitative problems outside the algebraic path framework,\r\nnamely of the minimum mean-payoff, minimum ratio, and minimum initial credit for energy problems.\r\n\r\n\r\nOur second contribution is a set of algorithms for Dyck reachability with applications to data-dependence analysis and alias analysis.\r\nIn particular, we develop an optimal algorithm for Dyck reachability on bidirected graphs, which are ubiquitous in context-insensitive, field-sensitive points-to analysis.\r\nAdditionally, we develop an efficient algorithm for context-sensitive data-dependence analysis via Dyck reachability,\r\nwhere the task is to obtain analysis summaries of library code in the presence of callbacks.\r\nOur algorithm preprocesses libraries in almost linear time, after which the contribution of the library in the complexity of the client analysis is (i)~linear in the number of call sites and (ii)~only logarithmic in the size of the whole library, as opposed to linear in the size of the whole library.\r\nFinally, we prove that Dyck reachability is Boolean Matrix Multiplication-hard in general, and the hardness also holds for graphs of constant treewidth.\r\nThis hardness result strongly indicates that there exist no combinatorial algorithms for Dyck reachability with truly subcubic complexity.\r\n\r\n\r\nOur third contribution is the formalization and algorithmic treatment of the Quantitative Interprocedural Analysis framework.\r\nIn this framework, the transitions of a recursive program are annotated as good, bad or neutral, and receive a weight which measures\r\nthe magnitude of their respective effect.\r\nThe Quantitative Interprocedural Analysis problem asks to determine whether there exists an infinite run of the program where the long-run ratio of the bad weights over the good weights is above a given threshold.\r\nWe illustrate how several quantitative problems related to static analysis of recursive programs can be instantiated in this framework,\r\nand present some case studies to this direction.\r\n\r\n\r\nOur fourth contribution is a new dynamic partial-order reduction for the stateless model checking of concurrent programs. Traditional approaches rely on the standard Mazurkiewicz equivalence between  traces, by means of partitioning the trace space into equivalence classes, and attempting to explore a few representatives from each class.\r\nWe present a new dynamic partial-order reduction method  called the Data-centric Partial Order Reduction (DC-DPOR).\r\nOur algorithm is based on a new equivalence between traces, called the observation equivalence.\r\nDC-DPOR explores a coarser partitioning of the trace space than any exploration method based on the standard Mazurkiewicz equivalence.\r\nDepending on the program, the new partitioning can be even exponentially coarser.\r\nAdditionally, DC-DPOR spends only polynomial time in each explored class.\r\n\r\n\r\nOur fifth contribution is the use of automata and game-theoretic verification techniques in the competitive analysis and synthesis of real-time scheduling algorithms for firm-deadline tasks.\r\nOn the analysis side, we leverage automata on infinite words to compute the competitive ratio of real-time schedulers subject to various environmental constraints.\r\nOn the synthesis side, we introduce a new instance of two-player mean-payoff partial-information games, and show\r\nhow the synthesis of an optimal real-time scheduler can be reduced to computing winning strategies in this new type of games.","lang":"eng"}],"publication_status":"published","ddc":["000"]},{"oa":1,"publication_identifier":{"issn":["1868-8969"]},"status":"public","scopus_import":1,"alternative_title":["LIPIcs"],"quality_controlled":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","related_material":{"record":[{"id":"6752","status":"public","relation":"later_version"}]},"citation":{"apa":"Avni, G., Henzinger, T. A., &#38; Chonev, V. K. (2017). Infinite-duration bidding games (Vol. 85). Presented at the CONCUR: Concurrency Theory, Berlin, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2017.21\">https://doi.org/10.4230/LIPIcs.CONCUR.2017.21</a>","short":"G. Avni, T.A. Henzinger, V.K. Chonev, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.","chicago":"Avni, Guy, Thomas A Henzinger, and Ventsislav K Chonev. “Infinite-Duration Bidding Games,” Vol. 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2017.21\">https://doi.org/10.4230/LIPIcs.CONCUR.2017.21</a>.","ieee":"G. Avni, T. A. Henzinger, and V. K. Chonev, “Infinite-duration bidding games,” presented at the CONCUR: Concurrency Theory, Berlin, Germany, 2017, vol. 85.","ista":"Avni G, Henzinger TA, Chonev VK. 2017. Infinite-duration bidding games. CONCUR: Concurrency Theory, LIPIcs, vol. 85, 17.","mla":"Avni, Guy, et al. <i>Infinite-Duration Bidding Games</i>. Vol. 85, 17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2017.21\">10.4230/LIPIcs.CONCUR.2017.21</a>.","ama":"Avni G, Henzinger TA, Chonev VK. Infinite-duration bidding games. In: Vol 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2017.21\">10.4230/LIPIcs.CONCUR.2017.21</a>"},"project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF"}],"author":[{"last_name":"Avni","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","first_name":"Guy","full_name":"Avni, Guy"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724"},{"full_name":"Chonev, Ventsislav K","first_name":"Ventsislav K","last_name":"Chonev","id":"36CBE2E6-F248-11E8-B48F-1D18A9856A87"}],"pubrep_id":"844","date_updated":"2025-07-10T11:53:48Z","abstract":[{"text":"Two-player games on graphs are widely studied in formal methods as they model the interaction between a system and its environment. The game is played by moving a token throughout a graph to produce an infinite path. There are several common modes to determine how the players move the token through the graph; e.g., in turn-based games the players alternate turns in moving the token. We study the bidding mode of moving the token, which, to the best of our knowledge, has never been studied in infinite-duration games. Both players have separate budgets, which sum up to $1$. In each turn, a bidding takes place. Both players submit bids simultaneously, and a bid is legal if it does not exceed the available budget. The winner of the bidding pays his bid to the other player and moves the token. For reachability objectives, repeated bidding games have been studied and are called Richman games. There, a central question is the existence and computation of threshold budgets; namely, a value t\\in [0,1] such that if\\PO's budget exceeds $t$, he can win the game, and if\\PT's budget exceeds 1-t, he can win the game. We focus on parity games and mean-payoff games. We show the existence of threshold budgets in these games, and reduce the problem of finding them to Richman games. We also determine the strategy-complexity of an optimal strategy. Our most interesting result shows that memoryless strategies suffice for mean-payoff bidding games. \r\n","lang":"eng"}],"publication_status":"published","ddc":["000"],"oa_version":"Published Version","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"conference":{"location":"Berlin, Germany","name":"CONCUR: Concurrency Theory","end_date":"2017-09-07","start_date":"2017-09-05"},"doi":"10.4230/LIPIcs.CONCUR.2017.21","article_number":"17","publist_id":"6466","has_accepted_license":"1","day":"01","date_published":"2017-09-01T00:00:00Z","_id":"950","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)"},"title":"Infinite-duration bidding games","arxiv":1,"year":"2017","external_id":{"arxiv":["1705.01433"]},"file_date_updated":"2020-07-14T12:48:16Z","file":[{"file_name":"IST-2017-844-v1+1_concur-cr.pdf","file_id":"5318","date_updated":"2020-07-14T12:48:16Z","relation":"main_file","checksum":"6d5cccf755207b91ccbef95d8275b013","date_created":"2018-12-12T10:18:00Z","creator":"system","access_level":"open_access","file_size":335170,"content_type":"application/pdf"}],"month":"09","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2018-12-11T11:49:22Z","type":"conference","intvolume":"        85","language":[{"iso":"eng"}],"volume":85},{"publication_identifier":{"isbn":["978-331963386-2"]},"status":"public","oa":1,"scopus_import":"1","alternative_title":["LNCS"],"quality_controlled":"1","ec_funded":1,"author":[{"first_name":"Pranav","full_name":"Ashok, Pranav","last_name":"Ashok"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"id":"49351290-F248-11E8-B48F-1D18A9856A87","last_name":"Daca","full_name":"Daca, Przemyslaw","first_name":"Przemyslaw"},{"orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky","full_name":"Kretinsky, Jan","first_name":"Jan"},{"first_name":"Tobias","full_name":"Meggendorfer, Tobias","last_name":"Meggendorfer"}],"project":[{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","call_identifier":"FWF"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"date_updated":"2025-09-11T07:18:04Z","citation":{"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>","short":"P. Ashok, K. Chatterjee, P. Daca, J. Kretinsky, T. Meggendorfer, in:, R. Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 201–221.","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.","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.","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>.","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>.","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>"},"publisher":"Springer","publication_status":"published","page":"201 - 221","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."}],"oa_version":"Submitted Version","conference":{"start_date":"2017-07-24","end_date":"2017-07-28","location":"Heidelberg, Germany","name":"CAV: Computer Aided Verification"},"department":[{"_id":"KrCh"}],"isi":1,"day":"13","publist_id":"7135","doi":"10.1007/978-3-319-63387-9_10","_id":"645","date_published":"2017-07-13T00:00:00Z","year":"2017","editor":[{"last_name":"Majumdar","full_name":"Majumdar, Rupak","first_name":"Rupak"},{"last_name":"Kunčak","full_name":"Kunčak, Viktor","first_name":"Viktor"}],"title":"Value iteration for long run average reward in markov decision processes","arxiv":1,"external_id":{"isi":["000432196400010"],"arxiv":["1705.02326"]},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","article_processing_charge":"No","month":"07","type":"conference","date_created":"2018-12-11T11:47:41Z","volume":10426,"intvolume":"     10426","language":[{"iso":"eng"}],"main_file_link":[{"url":"https://arxiv.org/abs/1705.02326","open_access":"1"}]},{"intvolume":"        82","language":[{"iso":"eng"}],"volume":82,"date_created":"2019-06-04T12:42:43Z","license":"https://creativecommons.org/licenses/by/3.0/","type":"conference","file":[{"file_name":"2017_LIPIcs-Chatterjee.pdf","date_updated":"2020-07-14T12:47:33Z","relation":"main_file","file_id":"6520","checksum":"7c2c9d09970af79026d7e37d9b632ef8","file_size":710185,"content_type":"application/pdf","creator":"kschuh","access_level":"open_access","date_created":"2019-06-04T12:56:52Z"}],"month":"08","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","file_date_updated":"2020-07-14T12:47:33Z","tmp":{"image":"/images/cc_by.png","name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)","legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode","short":"CC BY (3.0)"},"title":"Improved set-based symbolic algorithms for parity games","year":"2017","date_published":"2017-08-01T00:00:00Z","_id":"6519","doi":"10.4230/LIPICS.CSL.2017.18","article_number":"18","day":"01","has_accepted_license":"1","department":[{"_id":"KrCh"}],"conference":{"name":"CSL: Conference on Computer Science Logic","location":"Stockholm, Sweden","end_date":"2017-08-24","start_date":"2017-08-20"},"oa_version":"Published Version","abstract":[{"lang":"eng","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. "}],"publication_status":"published","ddc":["004"],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","citation":{"apa":"Chatterjee, K., Dvorák, W., Henzinger, M., &#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 für Informatik. <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. Henzinger, V. Loitzenbauer, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.","ista":"Chatterjee K, Dvorák W, Henzinger M, Loitzenbauer V. 2017. Improved set-based symbolic algorithms for parity games. CSL: Conference on Computer Science Logic vol. 82, 18.","ieee":"K. Chatterjee, W. Dvorák, M. 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 Henzinger, and Veronika Loitzenbauer. “Improved Set-Based Symbolic Algorithms for Parity Games,” Vol. 82. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. <a href=\"https://doi.org/10.4230/LIPICS.CSL.2017.18\">https://doi.org/10.4230/LIPICS.CSL.2017.18</a>.","mla":"Chatterjee, Krishnendu, et al. <i>Improved Set-Based Symbolic Algorithms for Parity Games</i>. Vol. 82, 18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:<a href=\"https://doi.org/10.4230/LIPICS.CSL.2017.18\">10.4230/LIPICS.CSL.2017.18</a>.","ama":"Chatterjee K, Dvorák W, Henzinger M, Loitzenbauer V. Improved set-based symbolic algorithms for parity games. In: Vol 82. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:<a href=\"https://doi.org/10.4230/LIPICS.CSL.2017.18\">10.4230/LIPICS.CSL.2017.18</a>"},"date_updated":"2025-05-14T10:53:47Z","author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"full_name":"Dvorák, Wolfgang","first_name":"Wolfgang","last_name":"Dvorák"},{"id":"540c9bbd-f2de-11ec-812d-d04a5be85630","orcid":"0000-0002-5008-6530","last_name":"Henzinger","full_name":"Henzinger, Monika H","first_name":"Monika H"},{"first_name":"Veronika","full_name":"Loitzenbauer, Veronika","last_name":"Loitzenbauer"}],"project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","ec_funded":1,"scopus_import":"1","oa":1,"status":"public"},{"project":[{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory"}],"author":[{"last_name":"Makohon Moore","first_name":"Alvin","full_name":"Makohon Moore, Alvin"},{"last_name":"Zhang","first_name":"Ming","full_name":"Zhang, Ming"},{"id":"4A918E98-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0170-7353","last_name":"Reiter","first_name":"Johannes","full_name":"Reiter, Johannes"},{"last_name":"Božić","first_name":"Ivana","full_name":"Božić, Ivana"},{"last_name":"Allen","full_name":"Allen, Benjamin","first_name":"Benjamin"},{"id":"1d4c0f4f-e8a3-11ec-a351-e36772758c45","last_name":"Kundu","full_name":"Kundu, Deepanjan","first_name":"Deepanjan"},{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"full_name":"Wong, Fay","first_name":"Fay","last_name":"Wong"},{"first_name":"Yuchen","full_name":"Jiao, Yuchen","last_name":"Jiao"},{"full_name":"Kohutek, Zachary","first_name":"Zachary","last_name":"Kohutek"},{"last_name":"Hong","full_name":"Hong, Jungeui","first_name":"Jungeui"},{"first_name":"Marc","full_name":"Attiyeh, Marc","last_name":"Attiyeh"},{"full_name":"Javier, Breanna","first_name":"Breanna","last_name":"Javier"},{"last_name":"Wood","full_name":"Wood, Laura","first_name":"Laura"},{"first_name":"Ralph","full_name":"Hruban, Ralph","last_name":"Hruban"},{"first_name":"Martin","full_name":"Nowak, Martin","last_name":"Nowak"},{"last_name":"Papadopoulos","full_name":"Papadopoulos, Nickolas","first_name":"Nickolas"},{"last_name":"Kinzler","first_name":"Kenneth","full_name":"Kinzler, Kenneth"},{"full_name":"Vogelstein, Bert","first_name":"Bert","last_name":"Vogelstein"},{"first_name":"Christine","full_name":"Iacobuzio Donahue, Christine","last_name":"Iacobuzio Donahue"}],"date_updated":"2025-09-11T07:12:56Z","publisher":"Nature Publishing Group","citation":{"chicago":"Makohon Moore, Alvin, Ming Zhang, Johannes Reiter, Ivana Božić, Benjamin Allen, Deepanjan Kundu, Krishnendu Chatterjee, et al. “Limited Heterogeneity of Known Driver Gene Mutations among the Metastases of Individual Patients with Pancreatic Cancer.” <i>Nature Genetics</i>. Nature Publishing Group, 2017. <a href=\"https://doi.org/10.1038/ng.3764\">https://doi.org/10.1038/ng.3764</a>.","ieee":"A. Makohon Moore <i>et al.</i>, “Limited heterogeneity of known driver gene mutations among the metastases of individual patients with pancreatic cancer,” <i>Nature Genetics</i>, vol. 49, no. 3. Nature Publishing Group, pp. 358–366, 2017.","ista":"Makohon Moore A, Zhang M, Reiter J, Božić I, Allen B, Kundu D, Chatterjee K, Wong F, Jiao Y, Kohutek Z, Hong J, Attiyeh M, Javier B, Wood L, Hruban R, Nowak M, Papadopoulos N, Kinzler K, Vogelstein B, Iacobuzio Donahue C. 2017. Limited heterogeneity of known driver gene mutations among the metastases of individual patients with pancreatic cancer. Nature Genetics. 49(3), 358–366.","apa":"Makohon Moore, A., Zhang, M., Reiter, J., Božić, I., Allen, B., Kundu, D., … Iacobuzio Donahue, C. (2017). Limited heterogeneity of known driver gene mutations among the metastases of individual patients with pancreatic cancer. <i>Nature Genetics</i>. Nature Publishing Group. <a href=\"https://doi.org/10.1038/ng.3764\">https://doi.org/10.1038/ng.3764</a>","short":"A. Makohon Moore, M. Zhang, J. Reiter, I. Božić, B. Allen, D. Kundu, K. Chatterjee, F. Wong, Y. Jiao, Z. Kohutek, J. Hong, M. Attiyeh, B. Javier, L. Wood, R. Hruban, M. Nowak, N. Papadopoulos, K. Kinzler, B. Vogelstein, C. Iacobuzio Donahue, Nature Genetics 49 (2017) 358–366.","ama":"Makohon Moore A, Zhang M, Reiter J, et al. Limited heterogeneity of known driver gene mutations among the metastases of individual patients with pancreatic cancer. <i>Nature Genetics</i>. 2017;49(3):358-366. doi:<a href=\"https://doi.org/10.1038/ng.3764\">10.1038/ng.3764</a>","mla":"Makohon Moore, Alvin, et al. “Limited Heterogeneity of Known Driver Gene Mutations among the Metastases of Individual Patients with Pancreatic Cancer.” <i>Nature Genetics</i>, vol. 49, no. 3, Nature Publishing Group, 2017, pp. 358–66, doi:<a href=\"https://doi.org/10.1038/ng.3764\">10.1038/ng.3764</a>."},"quality_controlled":"1","ec_funded":1,"pmid":1,"publication":"Nature Genetics","scopus_import":"1","publication_identifier":{"issn":["1061-4036"]},"status":"public","oa":1,"acknowledgement":"We thank the Memorial Sloan Kettering Cancer Center Molecular Cytology core facility for immunohistochemistry staining. This work was supported by Office of Naval Research grant N00014-16-1-2914, the Bill and Melinda Gates Foundation (OPP1148627), and a gift from B. Wu and E. Larson (M.A.N.), National Institutes of Health grants CA179991 (C.A.I.-D. and I.B.), F31 CA180682 (A.P.M.-M.), CA43460 (B.V.), and P50 CA62924, the Monastra Foundation, the Virginia and D.K. Ludwig Fund for Cancer Research, the Lustgarten Foundation for Pancreatic Cancer Research, the Sol Goldman Center for Pancreatic Cancer Research, the Sol Goldman Sequencing Center, ERC Start grant 279307: Graph Games (J.G.R., D.K., and C.K.), Austrian Science Fund (FWF) grant P23499-N23 (J.G.R., D.K., and C.K.), and FWF NFN grant S11407-N23 RiSE/SHiNE (J.G.R., D.K., and C.K.).","day":"01","has_accepted_license":"1","publist_id":"7092","doi":"10.1038/ng.3764","department":[{"_id":"KrCh"}],"isi":1,"oa_version":"Submitted Version","publication_status":"published","ddc":["000"],"page":"358 - 366","abstract":[{"lang":"eng","text":"The extent of heterogeneity among driver gene mutations present in naturally occurring metastases - that is, treatment-naive metastatic disease - is largely unknown. To address this issue, we carried out 60× whole-genome sequencing of 26 metastases from four patients with pancreatic cancer. We found that identical mutations in known driver genes were present in every metastatic lesion for each patient studied. Passenger gene mutations, which do not have known or predicted functional consequences, accounted for all intratumoral heterogeneity. Even with respect to these passenger mutations, our analysis suggests that the genetic similarity among the founding cells of metastases was higher than that expected for any two cells randomly taken from a normal tissue. The uniformity of known driver gene mutations among metastases in the same patient has critical and encouraging implications for the success of future targeted therapies in advanced-stage disease."}],"file_date_updated":"2020-07-14T12:47:33Z","external_id":{"isi":["000394917800009"],"pmid":["28092682"]},"year":"2017","title":"Limited heterogeneity of known driver gene mutations among the metastases of individual patients with pancreatic cancer","_id":"653","date_published":"2017-03-01T00:00:00Z","issue":"3","volume":49,"language":[{"iso":"eng"}],"intvolume":"        49","type":"journal_article","date_created":"2018-12-11T11:47:43Z","article_processing_charge":"No","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","article_type":"original","file":[{"file_name":"2017_NatureGenetics_Makohon.pdf","relation":"main_file","date_updated":"2020-07-14T12:47:33Z","file_id":"7050","checksum":"e442dc3b7420a36ec805e9bb45cc1a2e","content_type":"application/pdf","file_size":908099,"creator":"dernst","date_created":"2019-11-19T08:13:50Z","access_level":"open_access"}],"month":"03"},{"volume":114,"language":[{"iso":"eng"}],"intvolume":"       114","main_file_link":[{"url":"https://www.ncbi.nlm.nih.gov/pmc/articles/PMC5422766/","open_access":"1"}],"issue":"18","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"Yes (in subscription journal)","month":"05","type":"journal_article","date_created":"2018-12-11T11:47:50Z","year":"2017","title":"Memory-n strategies of direct reciprocity","external_id":{"pmid":["28420786"],"isi":["000400358000050"]},"_id":"671","date_published":"2017-05-02T00:00:00Z","isi":1,"department":[{"_id":"KrCh"}],"publist_id":"7053","day":"02","doi":"10.1073/pnas.1621239114","ddc":["000"],"publication_status":"published","corr_author":"1","abstract":[{"text":"Humans routinely use conditionally cooperative strategies when interacting in repeated social dilemmas. They are more likely to cooperate if others cooperated before, and are ready to retaliate if others defected. To capture the emergence of reciprocity, most previous models consider subjects who can only choose from a restricted set of representative strategies, or who react to the outcome of the very last round only. As players memorize more rounds, the dimension of the strategy space increases exponentially. This increasing computational complexity renders simulations for individuals with higher cognitive abilities infeasible, especially if multiplayer interactions are taken into account. Here, we take an axiomatic approach instead. We propose several properties that a robust cooperative strategy for a repeated multiplayer dilemma should have. These properties naturally lead to a unique class of cooperative strategies, which contains the classical Win-Stay Lose-Shift rule as a special case. A comprehensive numerical analysis for the prisoner's dilemma and for the public goods game suggests that strategies of this class readily evolve across various memory-n spaces. Our results reveal that successful strategies depend not only on how cooperative others were in the past but also on the respective context of cooperation.","lang":"eng"}],"page":"4715 - 4720","oa_version":"Published Version","ec_funded":1,"quality_controlled":"1","pmid":1,"author":[{"last_name":"Hilbe","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5116-955X","full_name":"Hilbe, Christian","first_name":"Christian"},{"full_name":"Martinez, Vaquero","first_name":"Vaquero","last_name":"Martinez"},{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"full_name":"Nowak, Martin","first_name":"Martin","last_name":"Nowak"}],"project":[{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"call_identifier":"FWF","name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"}],"date_updated":"2026-06-18T19:11:14Z","publisher":"National Academy of Sciences","citation":{"ieee":"C. Hilbe, V. Martinez, K. Chatterjee, and M. Nowak, “Memory-n strategies of direct reciprocity,” <i>PNAS</i>, vol. 114, no. 18. National Academy of Sciences, pp. 4715–4720, 2017.","ista":"Hilbe C, Martinez V, Chatterjee K, Nowak M. 2017. Memory-n strategies of direct reciprocity. PNAS. 114(18), 4715–4720.","chicago":"Hilbe, Christian, Vaquero Martinez, Krishnendu Chatterjee, and Martin Nowak. “Memory-n Strategies of Direct Reciprocity.” <i>PNAS</i>. National Academy of Sciences, 2017. <a href=\"https://doi.org/10.1073/pnas.1621239114\">https://doi.org/10.1073/pnas.1621239114</a>.","apa":"Hilbe, C., Martinez, V., Chatterjee, K., &#38; Nowak, M. (2017). Memory-n strategies of direct reciprocity. <i>PNAS</i>. National Academy of Sciences. <a href=\"https://doi.org/10.1073/pnas.1621239114\">https://doi.org/10.1073/pnas.1621239114</a>","short":"C. Hilbe, V. Martinez, K. Chatterjee, M. Nowak, PNAS 114 (2017) 4715–4720.","ama":"Hilbe C, Martinez V, Chatterjee K, Nowak M. Memory-n strategies of direct reciprocity. <i>PNAS</i>. 2017;114(18):4715-4720. doi:<a href=\"https://doi.org/10.1073/pnas.1621239114\">10.1073/pnas.1621239114</a>","mla":"Hilbe, Christian, et al. “Memory-n Strategies of Direct Reciprocity.” <i>PNAS</i>, vol. 114, no. 18, National Academy of Sciences, 2017, pp. 4715–20, doi:<a href=\"https://doi.org/10.1073/pnas.1621239114\">10.1073/pnas.1621239114</a>."},"status":"public","publication_identifier":{"issn":["0027-8424"]},"oa":1,"publication":"PNAS","scopus_import":"1"},{"volume":254,"intvolume":"       254","language":[{"iso":"eng"}],"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1311.3238"}],"user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","article_processing_charge":"No","article_type":"original","month":"06","type":"journal_article","date_created":"2018-12-11T11:47:53Z","year":"2017","title":"Doomsday equilibria for omega-regular games","arxiv":1,"external_id":{"isi":["000402025600008"],"arxiv":["1311.3238"]},"_id":"681","date_published":"2017-06-01T00:00:00Z","department":[{"_id":"KrCh"}],"isi":1,"day":"01","publist_id":"7036","doi":"10.1016/j.ic.2016.10.012","publication_status":"published","page":"296 - 315","abstract":[{"text":"Two-player games on graphs provide the theoretical framework for many important problems such as reactive synthesis. While the traditional study of two-player zero-sum games has been extended to multi-player games with several notions of equilibria, they are decidable only for perfect-information games, whereas several applications require imperfect-information. In this paper we propose a new notion of equilibria, called doomsday equilibria, which is a strategy profile where all players satisfy their own objective, and if any coalition of players deviates and violates even one of the players' objective, then the objective of every player is violated. We present algorithms and complexity results for deciding the existence of doomsday equilibria for various classes of ω-regular objectives, both for imperfect-information games, and for perfect-information games. We provide optimal complexity bounds for imperfect-information games, and in most cases for perfect-information games.","lang":"eng"}],"corr_author":"1","oa_version":"Submitted Version","ec_funded":1,"quality_controlled":"1","date_updated":"2026-04-16T10:00:03Z","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"last_name":"Doyen","full_name":"Doyen, Laurent","first_name":"Laurent"},{"first_name":"Emmanuel","full_name":"Filiot, Emmanuel","last_name":"Filiot"},{"last_name":"Raskin","full_name":"Raskin, Jean","first_name":"Jean"}],"project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"call_identifier":"FWF","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"grant_number":"291734","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"citation":{"ama":"Chatterjee K, Doyen L, Filiot E, Raskin J. Doomsday equilibria for omega-regular games. <i>Information and Computation</i>. 2017;254:296-315. doi:<a href=\"https://doi.org/10.1016/j.ic.2016.10.012\">10.1016/j.ic.2016.10.012</a>","mla":"Chatterjee, Krishnendu, et al. “Doomsday Equilibria for Omega-Regular Games.” <i>Information and Computation</i>, vol. 254, Elsevier, 2017, pp. 296–315, doi:<a href=\"https://doi.org/10.1016/j.ic.2016.10.012\">10.1016/j.ic.2016.10.012</a>.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, Emmanuel Filiot, and Jean Raskin. “Doomsday Equilibria for Omega-Regular Games.” <i>Information and Computation</i>. Elsevier, 2017. <a href=\"https://doi.org/10.1016/j.ic.2016.10.012\">https://doi.org/10.1016/j.ic.2016.10.012</a>.","ieee":"K. Chatterjee, L. Doyen, E. Filiot, and J. Raskin, “Doomsday equilibria for omega-regular games,” <i>Information and Computation</i>, vol. 254. Elsevier, pp. 296–315, 2017.","ista":"Chatterjee K, Doyen L, Filiot E, Raskin J. 2017. Doomsday equilibria for omega-regular games. Information and Computation. 254, 296–315.","short":"K. Chatterjee, L. Doyen, E. Filiot, J. Raskin, Information and Computation 254 (2017) 296–315.","apa":"Chatterjee, K., Doyen, L., Filiot, E., &#38; Raskin, J. (2017). Doomsday equilibria for omega-regular games. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2016.10.012\">https://doi.org/10.1016/j.ic.2016.10.012</a>"},"publisher":"Elsevier","related_material":{"record":[{"relation":"earlier_version","id":"10885","status":"public"}]},"publication_identifier":{"issn":["0890-5401"]},"status":"public","oa":1,"publication":"Information and Computation","scopus_import":"1"},{"quality_controlled":"1","author":[{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"last_name":"Piterman","first_name":"Nir","full_name":"Piterman, Nir"}],"date_updated":"2025-09-10T14:18:30Z","publisher":"Cambridge University Press","citation":{"ama":"Chatterjee K, Piterman N. Obligation blackwell games and p-automata. <i>Journal of Symbolic Logic</i>. 2017;82(2):420-452. doi:<a href=\"https://doi.org/10.1017/jsl.2016.71\">10.1017/jsl.2016.71</a>","mla":"Chatterjee, Krishnendu, and Nir Piterman. “Obligation Blackwell Games and P-Automata.” <i>Journal of Symbolic Logic</i>, vol. 82, no. 2, Cambridge University Press, 2017, pp. 420–52, doi:<a href=\"https://doi.org/10.1017/jsl.2016.71\">10.1017/jsl.2016.71</a>.","ista":"Chatterjee K, Piterman N. 2017. Obligation blackwell games and p-automata. Journal of Symbolic Logic. 82(2), 420–452.","chicago":"Chatterjee, Krishnendu, and Nir Piterman. “Obligation Blackwell Games and P-Automata.” <i>Journal of Symbolic Logic</i>. Cambridge University Press, 2017. <a href=\"https://doi.org/10.1017/jsl.2016.71\">https://doi.org/10.1017/jsl.2016.71</a>.","ieee":"K. Chatterjee and N. Piterman, “Obligation blackwell games and p-automata,” <i>Journal of Symbolic Logic</i>, vol. 82, no. 2. Cambridge University Press, pp. 420–452, 2017.","apa":"Chatterjee, K., &#38; Piterman, N. (2017). Obligation blackwell games and p-automata. <i>Journal of Symbolic Logic</i>. Cambridge University Press. <a href=\"https://doi.org/10.1017/jsl.2016.71\">https://doi.org/10.1017/jsl.2016.71</a>","short":"K. Chatterjee, N. Piterman, Journal of Symbolic Logic 82 (2017) 420–452."},"status":"public","publication_identifier":{"issn":["0022-4812"],"eissn":["1943-5886"]},"oa":1,"publication":"Journal of Symbolic Logic","scopus_import":"1","isi":1,"department":[{"_id":"KrCh"}],"day":"01","publist_id":"7026","doi":"10.1017/jsl.2016.71","publication_status":"published","corr_author":"1","abstract":[{"lang":"eng","text":"We generalize winning conditions in two-player games by adding a structural acceptance condition called obligations. Obligations are orthogonal to the linear winning conditions that define whether a play is winning. Obligations are a declaration that player 0 can achieve a certain value from a configuration. If the obligation is met, the value of that configuration for player 0 is 1. We define the value in such games and show that obligation games are determined. For Markov chains with Borel objectives and obligations, and finite turn-based stochastic parity games with obligations we give an alternative and simpler characterization of the value function. Based on this simpler definition we show that the decision problem of winning finite turn-based stochastic parity games with obligations is in NP∩co-NP. We also show that obligation games provide a game framework for reasoning about p-automata. © 2017 The Association for Symbolic Logic."}],"page":"420 - 452","oa_version":"Submitted Version","year":"2017","arxiv":1,"title":"Obligation blackwell games and p-automata","external_id":{"isi":["000403796700002"],"arxiv":["1206.5174"]},"_id":"684","date_published":"2017-06-01T00:00:00Z","volume":82,"language":[{"iso":"eng"}],"intvolume":"        82","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1206.5174"}],"issue":"2","article_processing_charge":"No","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","month":"06","type":"journal_article","date_created":"2018-12-11T11:47:54Z"},{"isi":1,"department":[{"_id":"KrCh"}],"day":"03","publist_id":"7002","doi":"10.1073/pnas.1702020114","publication_status":"published","abstract":[{"text":"In antagonistic symbioses, such as host–parasite interactions, one population’s success is the other’s loss. In mutualistic symbioses, such as division of labor, both parties can gain, but they might have different preferences over the possible mutualistic arrangements. The rates of evolution of the two populations in a symbiosis are important determinants of which population will be more successful: Faster evolution is thought to be favored in antagonistic symbioses (the “Red Queen effect”), but disfavored in certain mutualistic symbioses (the “Red King effect”). However, it remains unclear which biological parameters drive these effects. Here, we analyze the effects of the various determinants of evolutionary rate: generation time, mutation rate, population size, and the intensity of natural selection. Our main results hold for the case where mutation is infrequent. Slower evolution causes a long-term advantage in an important class of mutualistic interactions. Surprisingly, less intense selection is the strongest driver of this Red King effect, whereas relative mutation rates and generation times have little effect. In antagonistic interactions, faster evolution by any means is beneficial. Our results provide insight into the demographic evolution of symbionts. ","lang":"eng"}],"page":"E5396 - E5405","oa_version":"Submitted Version","quality_controlled":"1","pmid":1,"author":[{"first_name":"Carl","full_name":"Veller, Carl","last_name":"Veller"},{"last_name":"Hayward","first_name":"Laura","full_name":"Hayward, Laura"},{"last_name":"Nowak","full_name":"Nowak, Martin","first_name":"Martin"},{"id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5116-955X","last_name":"Hilbe","full_name":"Hilbe, Christian","first_name":"Christian"}],"date_updated":"2025-09-10T11:11:07Z","citation":{"ieee":"C. Veller, L. Hayward, M. Nowak, and C. Hilbe, “The red queen and king in finite populations,” <i>PNAS</i>, vol. 114, no. 27. National Academy of Sciences, pp. E5396–E5405, 2017.","chicago":"Veller, Carl, Laura Hayward, Martin Nowak, and Christian Hilbe. “The Red Queen and King in Finite Populations.” <i>PNAS</i>. National Academy of Sciences, 2017. <a href=\"https://doi.org/10.1073/pnas.1702020114\">https://doi.org/10.1073/pnas.1702020114</a>.","ista":"Veller C, Hayward L, Nowak M, Hilbe C. 2017. The red queen and king in finite populations. PNAS. 114(27), E5396–E5405.","apa":"Veller, C., Hayward, L., Nowak, M., &#38; Hilbe, C. (2017). The red queen and king in finite populations. <i>PNAS</i>. National Academy of Sciences. <a href=\"https://doi.org/10.1073/pnas.1702020114\">https://doi.org/10.1073/pnas.1702020114</a>","short":"C. Veller, L. Hayward, M. Nowak, C. Hilbe, PNAS 114 (2017) E5396–E5405.","ama":"Veller C, Hayward L, Nowak M, Hilbe C. The red queen and king in finite populations. <i>PNAS</i>. 2017;114(27):E5396-E5405. doi:<a href=\"https://doi.org/10.1073/pnas.1702020114\">10.1073/pnas.1702020114</a>","mla":"Veller, Carl, et al. “The Red Queen and King in Finite Populations.” <i>PNAS</i>, vol. 114, no. 27, National Academy of Sciences, 2017, pp. E5396–405, doi:<a href=\"https://doi.org/10.1073/pnas.1702020114\">10.1073/pnas.1702020114</a>."},"publisher":"National Academy of Sciences","status":"public","publication_identifier":{"issn":["0027-8424"]},"oa":1,"publication":"PNAS","scopus_import":"1","volume":114,"intvolume":"       114","language":[{"iso":"eng"}],"main_file_link":[{"url":"https://www.ncbi.nlm.nih.gov/pmc/articles/PMC5502615/","open_access":"1"}],"issue":"27","article_processing_charge":"No","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","month":"07","type":"journal_article","date_created":"2018-12-11T11:48:00Z","year":"2017","title":"The red queen and king in finite populations","external_id":{"pmid":["28630336"],"isi":["000404576100017"]},"_id":"699","date_published":"2017-07-03T00:00:00Z"},{"date_published":"2017-08-01T00:00:00Z","_id":"711","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)"},"title":"Bidirectional nested weighted automata","year":"2017","file_date_updated":"2020-07-14T12:47:49Z","file":[{"content_type":"application/pdf","file_size":570294,"creator":"system","date_created":"2018-12-12T10:08:02Z","access_level":"open_access","checksum":"d2bda4783821a6358333fe27f11f4737","relation":"main_file","date_updated":"2020-07-14T12:47:49Z","file_id":"4661","file_name":"IST-2017-886-v1+1_LIPIcs-CONCUR-2017-5.pdf"}],"month":"08","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","date_created":"2018-12-11T11:48:04Z","type":"conference","language":[{"iso":"eng"}],"intvolume":"        85","volume":85,"oa":1,"status":"public","publication_identifier":{"issn":["1868-8969"]},"alternative_title":["LIPIcs"],"scopus_import":"1","quality_controlled":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","citation":{"short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2017). Bidirectional nested weighted automata (Vol. 85). Presented at the 28th International Conference on Concurrency Theory, CONCUR, Berlin, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2017.5\">https://doi.org/10.4230/LIPIcs.CONCUR.2017.5</a>","ista":"Chatterjee K, Henzinger TA, Otop J. 2017. Bidirectional nested weighted automata. 28th International Conference on Concurrency Theory, CONCUR, LIPIcs, vol. 85, 5.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Bidirectional Nested Weighted Automata,” Vol. 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2017.5\">https://doi.org/10.4230/LIPIcs.CONCUR.2017.5</a>.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Bidirectional nested weighted automata,” presented at the 28th International Conference on Concurrency Theory, CONCUR, Berlin, Germany, 2017, vol. 85.","mla":"Chatterjee, Krishnendu, et al. <i>Bidirectional Nested Weighted Automata</i>. Vol. 85, 5, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2017.5\">10.4230/LIPIcs.CONCUR.2017.5</a>.","ama":"Chatterjee K, Henzinger TA, Otop J. Bidirectional nested weighted automata. In: Vol 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2017.5\">10.4230/LIPIcs.CONCUR.2017.5</a>"},"pubrep_id":"886","date_updated":"2025-07-10T11:54:15Z","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"full_name":"Otop, Jan","first_name":"Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop"}],"abstract":[{"lang":"eng","text":"Nested weighted automata (NWA) present a robust and convenient automata-theoretic formalism for quantitative specifications. Previous works have considered NWA that processed input words only in the forward direction. It is natural to allow the automata to process input words backwards as well, for example, to measure the maximal or average time between a response and the preceding request. We therefore introduce and study bidirectional NWA that can process input words in both directions. First, we show that bidirectional NWA can express interesting quantitative properties that are not expressible by forward-only NWA. Second, for the fundamental decision problems of emptiness and universality, we establish decidability and complexity results for the new framework which match the best-known results for the special case of forward-only NWA. Thus, for NWA, the increased expressiveness of bidirectionality is achieved at no additional computational complexity. This is in stark contrast to the unweighted case, where bidirectional finite automata are no more expressive but exponentially more succinct than their forward-only counterparts."}],"corr_author":"1","ddc":["004","005"],"publication_status":"published","oa_version":"Published Version","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"conference":{"location":"Berlin, Germany","name":"28th International Conference on Concurrency Theory, CONCUR","end_date":"2017-09-08","start_date":"2017-09-05"},"article_number":"5","doi":"10.4230/LIPIcs.CONCUR.2017.5","day":"01","publist_id":"6976","has_accepted_license":"1"},{"date_published":"2017-09-01T00:00:00Z","_id":"716","external_id":{"arxiv":["1201.2829"],"isi":["000443590400005"]},"arxiv":1,"title":"The complexity of mean-payoff pushdown games","year":"2017","date_created":"2018-12-11T11:48:06Z","type":"journal_article","article_type":"original","month":"09","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","article_processing_charge":"No","issue":"5","main_file_link":[{"url":"https://arxiv.org/abs/1201.2829","open_access":"1"}],"intvolume":"        64","language":[{"iso":"eng"}],"volume":64,"scopus_import":"1","publication":"Journal of the ACM","oa":1,"status":"public","publication_identifier":{"issn":["0004-5411"]},"publisher":"ACM","citation":{"ista":"Chatterjee K, Velner Y. 2017. The complexity of mean-payoff pushdown games. Journal of the ACM. 64(5), 34.","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>.","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.","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>","short":"K. Chatterjee, Y. Velner, Journal of the ACM 64 (2017) 34.","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>","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>."},"project":[{"call_identifier":"FWF","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"call_identifier":"FWF","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"}],"author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"first_name":"Yaron","full_name":"Velner, Yaron","last_name":"Velner"}],"date_updated":"2025-09-10T11:01:10Z","ec_funded":1,"quality_controlled":"1","oa_version":"Preprint","corr_author":"1","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."}],"page":"34","publication_status":"published","doi":"10.1145/3121408","day":"01","publist_id":"6964","isi":1,"department":[{"_id":"KrCh"}]}]