[{"ec_funded":1,"article_processing_charge":"No","date_published":"2017-11-21T00:00:00Z","month":"11","title":"Optional interactions and suspicious behaviour facilitates trustful cooperation in prisoners dilemma","date_updated":"2023-09-27T12:29:02Z","external_id":{"pmid":["28867224"],"isi":["000412039800007"]},"date_created":"2018-12-11T11:48:16Z","project":[{"name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734","call_identifier":"FP7"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"}],"_id":"744","page":"64 - 72","publication":" Journal of Theoretical Biology","file_date_updated":"2020-07-14T12:47:58Z","oa":1,"intvolume":"       433","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","volume":433,"license":"https://creativecommons.org/licenses/by-nc-nd/4.0/","scopus_import":"1","year":"2017","isi":1,"author":[{"id":"3C869AA0-F248-11E8-B48F-1D18A9856A87","first_name":"Tadeas","last_name":"Priklopil","full_name":"Priklopil, Tadeas"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"last_name":"Nowak","full_name":"Nowak, Martin","first_name":"Martin"}],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","short":"CC BY-NC-ND (4.0)","image":"/images/cc_by_nc_nd.png"},"publication_identifier":{"issn":["00225193"]},"department":[{"_id":"KrCh"}],"day":"21","publisher":"Elsevier","oa_version":"Submitted Version","doi":"10.1016/j.jtbi.2017.08.025","quality_controlled":"1","pmid":1,"status":"public","has_accepted_license":"1","language":[{"iso":"eng"}],"publist_id":"6923","abstract":[{"text":"In evolutionary game theory interactions between individuals are often assumed obligatory. However, in many real-life situations, individuals can decide to opt out of an interaction depending on the information they have about the opponent. We consider a simple evolutionary game theoretic model to study such a scenario, where at each encounter between two individuals the type of the opponent (cooperator/defector) is known with some probability, and where each individual either accepts or opts out of the interaction. If the type of the opponent is unknown, a trustful individual accepts the interaction, whereas a suspicious individual opts out of the interaction. If either of the two individuals opt out both individuals remain without an interaction. We show that in the prisoners dilemma optional interactions along with suspicious behaviour facilitates the emergence of trustful cooperation.","lang":"eng"}],"publication_status":"published","article_type":"original","ddc":["000","570"],"citation":{"ieee":"T. Priklopil, K. Chatterjee, and M. Nowak, “Optional interactions and suspicious behaviour facilitates trustful cooperation in prisoners dilemma,” <i> Journal of Theoretical Biology</i>, vol. 433. Elsevier, pp. 64–72, 2017.","short":"T. Priklopil, K. Chatterjee, M. Nowak,  Journal of Theoretical Biology 433 (2017) 64–72.","apa":"Priklopil, T., Chatterjee, K., &#38; Nowak, M. (2017). Optional interactions and suspicious behaviour facilitates trustful cooperation in prisoners dilemma. <i> Journal of Theoretical Biology</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.jtbi.2017.08.025\">https://doi.org/10.1016/j.jtbi.2017.08.025</a>","mla":"Priklopil, Tadeas, et al. “Optional Interactions and Suspicious Behaviour Facilitates Trustful Cooperation in Prisoners Dilemma.” <i> Journal of Theoretical Biology</i>, vol. 433, Elsevier, 2017, pp. 64–72, doi:<a href=\"https://doi.org/10.1016/j.jtbi.2017.08.025\">10.1016/j.jtbi.2017.08.025</a>.","ista":"Priklopil T, Chatterjee K, Nowak M. 2017. Optional interactions and suspicious behaviour facilitates trustful cooperation in prisoners dilemma.  Journal of Theoretical Biology. 433, 64–72.","ama":"Priklopil T, Chatterjee K, Nowak M. Optional interactions and suspicious behaviour facilitates trustful cooperation in prisoners dilemma. <i> Journal of Theoretical Biology</i>. 2017;433:64-72. doi:<a href=\"https://doi.org/10.1016/j.jtbi.2017.08.025\">10.1016/j.jtbi.2017.08.025</a>","chicago":"Priklopil, Tadeas, Krishnendu Chatterjee, and Martin Nowak. “Optional Interactions and Suspicious Behaviour Facilitates Trustful Cooperation in Prisoners Dilemma.” <i> Journal of Theoretical Biology</i>. Elsevier, 2017. <a href=\"https://doi.org/10.1016/j.jtbi.2017.08.025\">https://doi.org/10.1016/j.jtbi.2017.08.025</a>."},"type":"journal_article","file":[{"file_id":"7047","creator":"dernst","date_created":"2019-11-19T07:57:39Z","relation":"main_file","checksum":"4b43af1615ebf1a861840cb03d8a320c","content_type":"application/pdf","date_updated":"2020-07-14T12:47:58Z","file_size":537323,"file_name":"2017_JournTheoretBio_Priklopil.pdf","access_level":"open_access"}]},{"title":"Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games","date_updated":"2023-09-20T09:43:09Z","month":"02","date_published":"2017-02-01T00:00:00Z","article_processing_charge":"No","ec_funded":1,"publication":"Nonlinear Analysis: Hybrid Systems","page":"230 - 253","project":[{"_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734","call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme"},{"call_identifier":"FP7","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"_id":"1407","date_created":"2018-12-11T11:51:50Z","external_id":{"isi":["000390637000014"],"arxiv":["1410.5387"]},"volume":23,"related_material":{"record":[{"id":"1689","relation":"earlier_version","status":"public"}]},"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1410.5387"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","issue":"2","intvolume":"        23","oa":1,"scopus_import":"1","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"isi":1,"author":[{"first_name":"Mária","full_name":"Svoreňová, Mária","last_name":"Svoreňová"},{"last_name":"Kretinsky","orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan"},{"full_name":"Chmelik, Martin","last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87","first_name":"Martin"},{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"first_name":"Ivana","last_name":"Cěrná","full_name":"Cěrná, Ivana"},{"full_name":"Belta, Cǎlin","last_name":"Belta","first_name":"Cǎlin"}],"year":"2017","doi":"10.1016/j.nahs.2016.04.006","arxiv":1,"oa_version":"Preprint","publisher":"Elsevier","day":"01","publication_status":"published","abstract":[{"text":"We consider the problem of computing the set of initial states of a dynamical system such that there exists a control strategy to ensure that the trajectories satisfy a temporal logic specification with probability 1 (almost-surely). We focus on discrete-time, stochastic linear dynamics and specifications given as formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over linear predicates in the states of the system. We propose a solution based on iterative abstraction-refinement, and turn-based 2-player probabilistic games. While the theoretical guarantee of our algorithm after any finite number of iterations is only a partial solution, we show that if our algorithm terminates, then the result is the set of all satisfying initial states. Moreover, for any (partial) solution our algorithm synthesizes witness control strategies to ensure almost-sure satisfaction of the temporal logic specification. While the proposed algorithm guarantees progress and soundness in every iteration, it is computationally demanding. We offer an alternative, more efficient solution for the reachability properties that decomposes the problem into a series of smaller problems of the same type. All algorithms are demonstrated on an illustrative case study.","lang":"eng"}],"publist_id":"5800","language":[{"iso":"eng"}],"status":"public","quality_controlled":"1","type":"journal_article","citation":{"mla":"Svoreňová, Mária, et al. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 23, no. 2, Elsevier, 2017, pp. 230–53, doi:<a href=\"https://doi.org/10.1016/j.nahs.2016.04.006\">10.1016/j.nahs.2016.04.006</a>.","ista":"Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. 2017. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Nonlinear Analysis: Hybrid Systems. 23(2), 230–253.","chicago":"Svoreňová, Mária, Jan Kretinsky, Martin Chmelik, Krishnendu Chatterjee, Ivana Cěrná, and Cǎlin Belta. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier, 2017. <a href=\"https://doi.org/10.1016/j.nahs.2016.04.006\">https://doi.org/10.1016/j.nahs.2016.04.006</a>.","ama":"Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. <i>Nonlinear Analysis: Hybrid Systems</i>. 2017;23(2):230-253. doi:<a href=\"https://doi.org/10.1016/j.nahs.2016.04.006\">10.1016/j.nahs.2016.04.006</a>","ieee":"M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, and C. Belta, “Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games,” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 23, no. 2. Elsevier, pp. 230–253, 2017.","short":"M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, C. Belta, Nonlinear Analysis: Hybrid Systems 23 (2017) 230–253.","apa":"Svoreňová, M., Kretinsky, J., Chmelik, M., Chatterjee, K., Cěrná, I., &#38; Belta, C. (2017). Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.nahs.2016.04.006\">https://doi.org/10.1016/j.nahs.2016.04.006</a>"}},{"month":"10","date_updated":"2023-02-21T15:54:10Z","title":"Optimal Dyck reachability for data-dependence and alias analysis","date_published":"2017-10-23T00:00:00Z","article_processing_charge":"No","page":"37","file_date_updated":"2020-07-14T12:46:59Z","pubrep_id":"870","date_created":"2018-12-12T11:39:26Z","_id":"5455","alternative_title":["IST Austria Technical Report"],"related_material":{"record":[{"status":"public","relation":"later_version","id":"10416"}]},"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","oa":1,"department":[{"_id":"KrCh"}],"publication_identifier":{"issn":["2664-1690"]},"author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"last_name":"Choudhary","full_name":"Choudhary, Bhavya","first_name":"Bhavya"},{"full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"}],"year":"2017","oa_version":"Published Version","doi":"10.15479/AT:IST-2017-870-v1-1","day":"23","publisher":"IST Austria","language":[{"iso":"eng"}],"has_accepted_license":"1","status":"public","publication_status":"published","abstract":[{"lang":"eng","text":"A fundamental algorithmic problem at the heart of static analysis is Dyck reachability. The input is a graphwhere the edges are labeled with different types of opening and closing parentheses, and the reachabilityinformation is computed via paths whose parentheses are properly matched. We present new results for Dyckreachability problems with applications to alias analysis and data-dependence analysis. Our main contributions,that include improved upper bounds as well as lower bounds that establish optimality guarantees, are asfollows:First, we consider Dyck reachability on bidirected graphs, which is the standard way of performing field-sensitive points-to analysis. Given a bidirected graph withnnodes andmedges, we present: (i) an algorithmwith worst-case running timeO(m+n·α(n)), whereα(n)is the inverse Ackermann function, improving thepreviously knownO(n2)time bound; (ii) a matching lower bound that shows that our algorithm is optimalwrt to worst-case complexity; and (iii) an optimal average-case upper bound ofO(m)time, improving thepreviously knownO(m·logn)bound.Second, we consider the problem of context-sensitive data-dependence analysis, where the task is to obtainanalysis summaries of library code in the presence of callbacks. Our algorithm preprocesses libraries in almostlinear time, after which the contribution of the library in the complexity of the client analysis is only linear,and only wrt the number of call sites.Third, we prove that combinatorial algorithms for Dyck reachability on general graphs with truly sub-cubic bounds cannot be obtained without obtaining sub-cubic combinatorial algorithms for Boolean MatrixMultiplication, which is a long-standing open problem. Thus we establish that the existing combinatorialalgorithms for Dyck reachability are (conditionally) optimal for general graphs. We also show that the samehardness holds for graphs of constant treewidth.Finally, we provide a prototype implementation of our algorithms for both alias analysis and data-dependenceanalysis. Our experimental evaluation demonstrates that the new algorithms significantly outperform allexisting methods on the two problems, over real-world benchmarks."}],"citation":{"ieee":"K. Chatterjee, B. Choudhary, and A. Pavlogiannis, <i>Optimal Dyck reachability for data-dependence and alias analysis</i>. IST Austria, 2017.","apa":"Chatterjee, K., Choudhary, B., &#38; Pavlogiannis, A. (2017). <i>Optimal Dyck reachability for data-dependence and alias analysis</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2017-870-v1-1\">https://doi.org/10.15479/AT:IST-2017-870-v1-1</a>","short":"K. Chatterjee, B. Choudhary, A. Pavlogiannis, Optimal Dyck Reachability for Data-Dependence and Alias Analysis, IST Austria, 2017.","ista":"Chatterjee K, Choudhary B, Pavlogiannis A. 2017. Optimal Dyck reachability for data-dependence and alias analysis, IST Austria, 37p.","mla":"Chatterjee, Krishnendu, et al. <i>Optimal Dyck Reachability for Data-Dependence and Alias Analysis</i>. IST Austria, 2017, doi:<a href=\"https://doi.org/10.15479/AT:IST-2017-870-v1-1\">10.15479/AT:IST-2017-870-v1-1</a>.","ama":"Chatterjee K, Choudhary B, Pavlogiannis A. <i>Optimal Dyck Reachability for Data-Dependence and Alias Analysis</i>. IST Austria; 2017. doi:<a href=\"https://doi.org/10.15479/AT:IST-2017-870-v1-1\">10.15479/AT:IST-2017-870-v1-1</a>","chicago":"Chatterjee, Krishnendu, Bhavya Choudhary, and Andreas Pavlogiannis. <i>Optimal Dyck Reachability for Data-Dependence and Alias Analysis</i>. IST Austria, 2017. <a href=\"https://doi.org/10.15479/AT:IST-2017-870-v1-1\">https://doi.org/10.15479/AT:IST-2017-870-v1-1</a>."},"type":"technical_report","file":[{"file_name":"IST-2017-870-v1+1_main.pdf","access_level":"open_access","relation":"main_file","checksum":"177a84a46e3ac17e87b31534ad16a4c9","date_updated":"2020-07-14T12:46:59Z","content_type":"application/pdf","file_size":960491,"date_created":"2018-12-12T11:54:02Z","creator":"system","file_id":"5524"}],"ddc":["000"]},{"month":"10","publication_identifier":{"issn":["2664-1690"]},"department":[{"_id":"KrCh"}],"date_updated":"2023-02-23T12:26:54Z","title":"Data-centric dynamic partial order reduction","year":"2017","date_published":"2017-10-23T00:00:00Z","author":[{"last_name":"Chalupa","full_name":"Chalupa, Marek","first_name":"Marek"},{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722"},{"last_name":"Sinha","full_name":"Sinha, Nishant","first_name":"Nishant"},{"last_name":"Vaidya","full_name":"Vaidya, Kapil","first_name":"Kapil"}],"oa_version":"Published Version","page":"36","doi":"10.15479/AT:IST-2017-872-v1-1","file_date_updated":"2020-07-14T12:46:59Z","pubrep_id":"872","day":"23","date_created":"2018-12-12T11:39:26Z","publisher":"IST Austria","_id":"5456","has_accepted_license":"1","status":"public","language":[{"iso":"eng"}],"related_material":{"record":[{"id":"10417","relation":"later_version","status":"public"},{"id":"5448","status":"public","relation":"earlier_version"}]},"publication_status":"published","alternative_title":["IST Austria Technical Report"],"abstract":[{"text":"We present a new dynamic partial-order reduction method for stateless model checking of concurrent programs. A common approach for exploring program behaviors relies on enumerating the traces of the program, without storing the visited states (aka stateless exploration). As the number of distinct traces grows exponentially, dynamic partial-order reduction (DPOR) techniques have been successfully used to partition the space of traces into equivalence classes (Mazurkiewicz partitioning), with the goal of exploring only few representative traces from each class.\r\nWe introduce a new equivalence on traces under sequential consistency semantics, which we call the observation equivalence. Two traces are observationally equivalent if every read event observes the same write event in both traces. While the traditional Mazurkiewicz equivalence is control-centric, our new definition is data-centric. We show that our observation equivalence is coarser than the Mazurkiewicz equivalence, and in many cases even exponentially coarser. We devise a DPOR exploration of the trace space, called data-centric DPOR, based on the observation equivalence.\r\n1. For acyclic architectures, our algorithm is guaranteed to explore exactly one representative trace from each observation class, while spending polynomial time per class. Hence, our algorithm is optimal wrt the observation equivalence, and in several cases explores exponentially fewer traces than any enumerative method based on the Mazurkiewicz equivalence.\r\n2. For cyclic architectures, we consider an equivalence between traces which is finer than the observation equivalence; but coarser than the Mazurkiewicz equivalence, and in some cases is exponentially coarser. Our data-centric DPOR algorithm remains optimal under this trace equivalence. \r\nFinally, we perform a basic experimental comparison between the existing Mazurkiewicz-based DPOR and our data-centric DPOR on a set of academic benchmarks. Our results show a significant reduction in both running time and the number of explored equivalence classes.","lang":"eng"}],"oa":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ama":"Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. <i>Data-Centric Dynamic Partial Order Reduction</i>. IST Austria; 2017. doi:<a href=\"https://doi.org/10.15479/AT:IST-2017-872-v1-1\">10.15479/AT:IST-2017-872-v1-1</a>","chicago":"Chalupa, Marek, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya. <i>Data-Centric Dynamic Partial Order Reduction</i>. IST Austria, 2017. <a href=\"https://doi.org/10.15479/AT:IST-2017-872-v1-1\">https://doi.org/10.15479/AT:IST-2017-872-v1-1</a>.","ista":"Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. 2017. Data-centric dynamic partial order reduction, IST Austria, 36p.","mla":"Chalupa, Marek, et al. <i>Data-Centric Dynamic Partial Order Reduction</i>. IST Austria, 2017, doi:<a href=\"https://doi.org/10.15479/AT:IST-2017-872-v1-1\">10.15479/AT:IST-2017-872-v1-1</a>.","short":"M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, K. Vaidya, Data-Centric Dynamic Partial Order Reduction, IST Austria, 2017.","apa":"Chalupa, M., Chatterjee, K., Pavlogiannis, A., Sinha, N., &#38; Vaidya, K. (2017). <i>Data-centric dynamic partial order reduction</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2017-872-v1-1\">https://doi.org/10.15479/AT:IST-2017-872-v1-1</a>","ieee":"M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya, <i>Data-centric dynamic partial order reduction</i>. IST Austria, 2017."},"type":"technical_report","file":[{"file_id":"5487","creator":"system","date_created":"2018-12-12T11:53:26Z","file_size":910347,"date_updated":"2020-07-14T12:46:59Z","content_type":"application/pdf","checksum":"d2635c4cf013000f0a1b09e80f9e4ab7","relation":"main_file","access_level":"open_access","file_name":"IST-2017-872-v1+1_main.pdf"}],"ddc":["000"]},{"scopus_import":1,"license":"https://creativecommons.org/licenses/by/4.0/","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","intvolume":"        83","oa":1,"article_number":"61","alternative_title":["LIPIcs"],"volume":83,"date_created":"2018-12-11T11:47:08Z","_id":"551","pubrep_id":"924","file_date_updated":"2020-07-14T12:47:00Z","publication":"Leibniz International Proceedings in Informatics","date_published":"2017-11-01T00:00:00Z","month":"11","date_updated":"2021-01-12T08:02:34Z","title":"Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs","ddc":["004"],"citation":{"ista":"Chatterjee K, Ibsen-Jensen R, Nowak M. 2017. Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs. Leibniz International Proceedings in Informatics. MFCS: Mathematical Foundations of Computer Science (SG), LIPIcs, vol. 83, 61.","mla":"Chatterjee, Krishnendu, et al. “Faster Monte Carlo Algorithms for Fixation Probability of the Moran Process on Undirected Graphs.” <i>Leibniz International Proceedings in Informatics</i>, vol. 83, 61, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.61\">10.4230/LIPIcs.MFCS.2017.61</a>.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Martin Nowak. “Faster Monte Carlo Algorithms for Fixation Probability of the Moran Process on Undirected Graphs.” In <i>Leibniz International Proceedings in Informatics</i>, Vol. 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.61\">https://doi.org/10.4230/LIPIcs.MFCS.2017.61</a>.","ama":"Chatterjee K, Ibsen-Jensen R, Nowak M. Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs. In: <i>Leibniz International Proceedings in Informatics</i>. Vol 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.61\">10.4230/LIPIcs.MFCS.2017.61</a>","ieee":"K. Chatterjee, R. Ibsen-Jensen, and M. Nowak, “Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs,” in <i>Leibniz International Proceedings in Informatics</i>, Aalborg, Denmark, 2017, vol. 83.","apa":"Chatterjee, K., Ibsen-Jensen, R., &#38; Nowak, M. (2017). Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs. In <i>Leibniz International Proceedings in Informatics</i> (Vol. 83). Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.61\">https://doi.org/10.4230/LIPIcs.MFCS.2017.61</a>","short":"K. Chatterjee, R. Ibsen-Jensen, M. Nowak, in:, Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017."},"type":"conference","file":[{"date_created":"2018-12-12T10:18:04Z","creator":"system","file_id":"5322","file_name":"IST-2018-924-v1+1_LIPIcs-MFCS-2017-61.pdf","access_level":"open_access","checksum":"2eed5224c0e4e259484a1d71acb8ba6a","relation":"main_file","content_type":"application/pdf","date_updated":"2020-07-14T12:47:00Z","file_size":535077}],"quality_controlled":"1","language":[{"iso":"eng"}],"status":"public","has_accepted_license":"1","publication_status":"published","abstract":[{"lang":"eng","text":"Evolutionary graph theory studies the evolutionary dynamics in a population structure given as a connected graph. Each node of the graph represents an individual of the population, and edges determine how offspring are placed. We consider the classical birth-death Moran process where there are two types of individuals, namely, the residents with fitness 1 and mutants with fitness r. The fitness indicates the reproductive strength. The evolutionary dynamics happens as follows: in the initial step, in a population of all resident individuals a mutant is introduced, and then at each step, an individual is chosen proportional to the fitness of its type to reproduce, and the offspring replaces a neighbor uniformly at random. The process stops when all individuals are either residents or mutants. The probability that all individuals in the end are mutants is called the fixation probability, which is a key factor in the rate of evolution. We consider the problem of approximating the fixation probability. The class of algorithms that is extremely relevant for approximation of the fixation probabilities is the Monte-Carlo simulation of the process. Previous results present a polynomial-time Monte-Carlo algorithm for undirected graphs when r is given in unary. First, we present a simple modification: instead of simulating each step, we discard ineffective steps, where no node changes type (i.e., either residents replace residents, or mutants replace mutants). Using the above simple modification and our result that the number of effective steps is concentrated around the expected number of effective steps, we present faster polynomial-time Monte-Carlo algorithms for undirected graphs. Our algorithms are always at least a factor O(n2/ log n) faster as compared to the previous algorithms, where n is the number of nodes, and is polynomial even if r is given in binary. We also present lower bounds showing that the upper bound on the expected number of effective steps we present is asymptotically tight for undirected graphs. "}],"publist_id":"7263","day":"01","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","oa_version":"Published Version","doi":"10.4230/LIPIcs.MFCS.2017.61","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus"},{"first_name":"Martin","full_name":"Nowak, Martin","last_name":"Nowak"}],"year":"2017","conference":{"location":"Aalborg, Denmark","start_date":"2017-08-21","end_date":"2017-08-25","name":"MFCS: Mathematical Foundations of Computer Science (SG)"},"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"department":[{"_id":"KrCh"}],"publication_identifier":{"isbn":["978-395977046-0"]}},{"day":"01","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","oa_version":"Published Version","doi":"10.4230/LIPIcs.MFCS.2017.39","conference":{"name":"MFCS: Mathematical Foundations of Computer Science (SG)","location":"Aalborg, Denmark","start_date":"2017-08-21","end_date":"2017-08-25"},"year":"2017","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"first_name":"Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H","last_name":"Henzinger"},{"first_name":"Alexander","full_name":"Svozil, Alexander","last_name":"Svozil"}],"tmp":{"short":"CC BY (3.0)","name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)","legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode","image":"/images/cc_by.png"},"department":[{"_id":"KrCh"}],"publication_identifier":{"isbn":["978-395977046-0"]},"ddc":["004"],"citation":{"ieee":"K. Chatterjee, M. H. Henzinger, and A. Svozil, “Faster algorithms for mean-payoff parity games,” in <i>Leibniz International Proceedings in Informatics</i>, Aalborg, Denmark, 2017, vol. 83.","apa":"Chatterjee, K., Henzinger, M. H., &#38; Svozil, A. (2017). Faster algorithms for mean-payoff parity games. In <i>Leibniz International Proceedings in Informatics</i> (Vol. 83). Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.39\">https://doi.org/10.4230/LIPIcs.MFCS.2017.39</a>","short":"K. Chatterjee, M.H. Henzinger, A. Svozil, in:, Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.","ista":"Chatterjee K, Henzinger MH, Svozil A. 2017. Faster algorithms for mean-payoff parity games. Leibniz International Proceedings in Informatics. MFCS: Mathematical Foundations of Computer Science (SG), LIPIcs, vol. 83, 39.","mla":"Chatterjee, Krishnendu, et al. “Faster Algorithms for Mean-Payoff Parity Games.” <i>Leibniz International Proceedings in Informatics</i>, vol. 83, 39, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.39\">10.4230/LIPIcs.MFCS.2017.39</a>.","chicago":"Chatterjee, Krishnendu, Monika H Henzinger, and Alexander Svozil. “Faster Algorithms for Mean-Payoff Parity Games.” In <i>Leibniz International Proceedings in Informatics</i>, Vol. 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.39\">https://doi.org/10.4230/LIPIcs.MFCS.2017.39</a>.","ama":"Chatterjee K, Henzinger MH, Svozil A. Faster algorithms for mean-payoff parity games. In: <i>Leibniz International Proceedings in Informatics</i>. Vol 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.39\">10.4230/LIPIcs.MFCS.2017.39</a>"},"type":"conference","file":[{"content_type":"application/pdf","date_updated":"2020-07-14T12:47:00Z","file_size":610339,"relation":"main_file","checksum":"c67f4866ddbfd555afef1f63ae9a8fc7","access_level":"open_access","file_name":"IST-2018-923-v1+1_LIPIcs-MFCS-2017-39.pdf","file_id":"5248","date_created":"2018-12-12T10:16:57Z","creator":"system"}],"quality_controlled":"1","status":"public","has_accepted_license":"1","language":[{"iso":"eng"}],"publist_id":"7262","publication_status":"published","abstract":[{"lang":"eng","text":"Graph games provide the foundation for modeling and synthesis of reactive processes. Such games are played over graphs where the vertices are controlled by two adversarial players. We consider graph games where the objective of the first player is the conjunction of a qualitative objective (specified as a parity condition) and a quantitative objective (specified as a meanpayoff condition). There are two variants of the problem, namely, the threshold problem where the quantitative goal is to ensure that the mean-payoff value is above a threshold, and the value problem where the quantitative goal is to ensure the optimal mean-payoff value; in both cases ensuring the qualitative parity objective. The previous best-known algorithms for game graphs with n vertices, m edges, parity objectives with d priorities, and maximal absolute reward value W for mean-payoff objectives, are as follows: O(nd+1 . m . w) for the threshold problem, and O(nd+2 · m · W) for the value problem. Our main contributions are faster algorithms, and the running times of our algorithms are as follows: O(nd-1 · m ·W) for the threshold problem, and O(nd · m · W · log(n · W)) for the value problem. For mean-payoff parity objectives with two priorities, our algorithms match the best-known bounds of the algorithms for mean-payoff games (without conjunction with parity objectives). Our results are relevant in synthesis of reactive systems with both functional requirement (given as a qualitative objective) and performance requirement (given as a quantitative objective)."}],"date_created":"2018-12-11T11:47:08Z","_id":"552","project":[{"name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"publication":"Leibniz International Proceedings in Informatics","file_date_updated":"2020-07-14T12:47:00Z","pubrep_id":"923","ec_funded":1,"article_processing_charge":"No","date_published":"2017-11-01T00:00:00Z","month":"11","title":"Faster algorithms for mean-payoff parity games","date_updated":"2023-02-14T10:06:46Z","license":"https://creativecommons.org/licenses/by/3.0/","scopus_import":"1","intvolume":"        83","oa":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_number":"39","alternative_title":["LIPIcs"],"volume":83},{"publication":"Leibniz International Proceedings in Informatics","pubrep_id":"922","file_date_updated":"2020-07-14T12:47:00Z","_id":"553","date_created":"2018-12-11T11:47:08Z","date_updated":"2021-01-12T08:02:35Z","title":"Strategy complexity of concurrent safety games","month":"11","date_published":"2017-11-01T00:00:00Z","scopus_import":1,"main_file_link":[{"url":"https://arxiv.org/abs/1506.02434","open_access":"1"}],"volume":83,"alternative_title":["LIPIcs"],"article_number":"55","intvolume":"        83","oa":1,"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","doi":"10.4230/LIPIcs.MFCS.2017.55","oa_version":"Published Version","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","day":"01","publication_identifier":{"isbn":["978-395977046-0"]},"department":[{"_id":"KrCh"}],"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"year":"2017","conference":{"end_date":"2017-08-25","location":"Aalborg, Denmark","start_date":"2017-08-21","name":"MFCS: Mathematical Foundations of Computer Science (SG)"},"author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Hansen, Kristofer","last_name":"Hansen","first_name":"Kristofer"},{"first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus"}],"file":[{"checksum":"7101facb56ade363205c695d72dbd173","relation":"main_file","file_size":549967,"date_updated":"2020-07-14T12:47:00Z","content_type":"application/pdf","file_name":"IST-2018-922-v1+1_LIPIcs-MFCS-2017-55.pdf","access_level":"open_access","file_id":"4753","creator":"system","date_created":"2018-12-12T10:09:29Z"}],"type":"conference","citation":{"ista":"Chatterjee K, Hansen K, Ibsen-Jensen R. 2017. Strategy complexity of concurrent safety games. Leibniz International Proceedings in Informatics. MFCS: Mathematical Foundations of Computer Science (SG), LIPIcs, vol. 83, 55.","mla":"Chatterjee, Krishnendu, et al. “Strategy Complexity of Concurrent Safety Games.” <i>Leibniz International Proceedings in Informatics</i>, vol. 83, 55, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.55\">10.4230/LIPIcs.MFCS.2017.55</a>.","ama":"Chatterjee K, Hansen K, Ibsen-Jensen R. Strategy complexity of concurrent safety games. In: <i>Leibniz International Proceedings in Informatics</i>. Vol 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.55\">10.4230/LIPIcs.MFCS.2017.55</a>","chicago":"Chatterjee, Krishnendu, Kristofer Hansen, and Rasmus Ibsen-Jensen. “Strategy Complexity of Concurrent Safety Games.” In <i>Leibniz International Proceedings in Informatics</i>, Vol. 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.55\">https://doi.org/10.4230/LIPIcs.MFCS.2017.55</a>.","ieee":"K. Chatterjee, K. Hansen, and R. Ibsen-Jensen, “Strategy complexity of concurrent safety games,” in <i>Leibniz International Proceedings in Informatics</i>, Aalborg, Denmark, 2017, vol. 83.","apa":"Chatterjee, K., Hansen, K., &#38; Ibsen-Jensen, R. (2017). Strategy complexity of concurrent safety games. In <i>Leibniz International Proceedings in Informatics</i> (Vol. 83). Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2017.55\">https://doi.org/10.4230/LIPIcs.MFCS.2017.55</a>","short":"K. Chatterjee, K. Hansen, R. Ibsen-Jensen, in:, Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017."},"ddc":["004"],"publist_id":"7261","publication_status":"published","abstract":[{"text":"We consider two player, zero-sum, finite-state concurrent reachability games, played for an infinite number of rounds, where in every round, each player simultaneously and independently of the other players chooses an action, whereafter the successor state is determined by a probability distribution given by the current state and the chosen actions. Player 1 wins iff a designated goal state is eventually visited. We are interested in the complexity of stationary strategies measured by their patience, which is defined as the inverse of the smallest non-zero probability employed. Our main results are as follows: We show that: (i) the optimal bound on the patience of optimal and -optimal strategies, for both players is doubly exponential; and (ii) even in games with a single non-absorbing state exponential (in the number of actions) patience is necessary. ","lang":"eng"}],"status":"public","has_accepted_license":"1","language":[{"iso":"eng"}],"quality_controlled":"1"},{"oa_version":"Published Version","doi":"10.15479/AT:ISTA:51","file_date_updated":"2020-07-14T12:47:02Z","day":"02","date_created":"2018-12-12T12:31:32Z","publisher":"Institute of Science and Technology Austria","_id":"5559","project":[{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7"}],"month":"01","department":[{"_id":"KrCh"}],"date_updated":"2024-02-21T13:48:42Z","title":"Strong amplifiers of natural selection","ec_funded":1,"article_processing_charge":"No","year":"2017","keyword":["natural selection"],"date_published":"2017-01-02T00:00:00Z","author":[{"orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","full_name":"Tkadlec, Josef","orcid":"0000-0002-1097-9684","last_name":"Tkadlec"},{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"last_name":"Nowak ","full_name":"Nowak , Martin","first_name":"Martin"}],"type":"research_data","citation":{"chicago":"Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak . “Strong Amplifiers of Natural Selection.” Institute of Science and Technology Austria, 2017. <a href=\"https://doi.org/10.15479/AT:ISTA:51\">https://doi.org/10.15479/AT:ISTA:51</a>.","ama":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak  M. Strong amplifiers of natural selection. 2017. doi:<a href=\"https://doi.org/10.15479/AT:ISTA:51\">10.15479/AT:ISTA:51</a>","ista":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak  M. 2017. Strong amplifiers of natural selection, Institute of Science and Technology Austria, <a href=\"https://doi.org/10.15479/AT:ISTA:51\">10.15479/AT:ISTA:51</a>.","mla":"Pavlogiannis, Andreas, et al. <i>Strong Amplifiers of Natural Selection</i>. Institute of Science and Technology Austria, 2017, doi:<a href=\"https://doi.org/10.15479/AT:ISTA:51\">10.15479/AT:ISTA:51</a>.","apa":"Pavlogiannis, A., Tkadlec, J., Chatterjee, K., &#38; Nowak , M. (2017). Strong amplifiers of natural selection. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT:ISTA:51\">https://doi.org/10.15479/AT:ISTA:51</a>","short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak , (2017).","ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak , “Strong amplifiers of natural selection.” Institute of Science and Technology Austria, 2017."},"file":[{"access_level":"open_access","file_name":"IST-2017-51-v1+2_illustration.mp4","content_type":"video/mp4","date_updated":"2020-07-14T12:47:02Z","file_size":32987015,"relation":"main_file","checksum":"b427dd46a30096a1911b245640c47af8","date_created":"2018-12-12T13:05:18Z","creator":"system","file_id":"5644"}],"ddc":["519"],"datarep_id":"51","has_accepted_license":"1","status":"public","related_material":{"record":[{"id":"5452","status":"public","relation":"research_paper"},{"id":"5751","relation":"research_paper","status":"public"}]},"abstract":[{"text":"Strong amplifiers of natural selection","lang":"eng"}],"oa":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"page":"367 - 381","file_date_updated":"2020-07-14T12:47:25Z","publication":"Models, Algorithms, Logics and Tools","date_created":"2018-12-11T11:47:34Z","project":[{"name":"Moderne Concurrency Paradigms","call_identifier":"FWF","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory"},{"name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","call_identifier":"FWF"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"_id":"625","month":"07","title":"The cost of exactness in quantitative reachability","date_updated":"2025-06-02T08:53:45Z","ec_funded":1,"date_published":"2017-07-25T00:00:00Z","article_processing_charge":"No","scopus_import":"1","volume":10460,"alternative_title":["LNCS"],"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.","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":"     10460","oa":1,"oa_version":"Submitted Version","doi":"10.1007/978-3-319-63121-9_18","day":"25","series_title":"Theoretical Computer Science and General Issues","publisher":"Springer","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publication_identifier":{"isbn":["978-3-319-63120-2"],"issn":["0302-9743"]},"editor":[{"first_name":"Luca","full_name":"Aceto, Luca","last_name":"Aceto"},{"last_name":"Bacci","full_name":"Bacci, Giorgio","first_name":"Giorgio"},{"first_name":"Anna","last_name":"Ingólfsdóttir","full_name":"Ingólfsdóttir, Anna"},{"full_name":"Legay, Axel","last_name":"Legay","first_name":"Axel"},{"first_name":"Radu","full_name":"Mardare, Radu","last_name":"Mardare"}],"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"full_name":"Doyen, Laurent","last_name":"Doyen","first_name":"Laurent"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"}],"year":"2017","citation":{"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>","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>.","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.","mla":"Chatterjee, Krishnendu, et al. “The Cost of Exactness in Quantitative Reachability.” <i>Models, Algorithms, Logics and Tools</i>, edited by Luca Aceto et al., vol. 10460, Springer, 2017, pp. 367–81, doi:<a href=\"https://doi.org/10.1007/978-3-319-63121-9_18\">10.1007/978-3-319-63121-9_18</a>.","short":"K. Chatterjee, L. Doyen, T.A. Henzinger, in:, L. Aceto, G. Bacci, A. Ingólfsdóttir, A. Legay, R. Mardare (Eds.), Models, Algorithms, Logics and Tools, Springer, 2017, pp. 367–381.","apa":"Chatterjee, K., Doyen, L., &#38; Henzinger, T. A. (2017). The cost of exactness in quantitative reachability. In L. Aceto, G. Bacci, A. Ingólfsdóttir, A. Legay, &#38; R. Mardare (Eds.), <i>Models, Algorithms, Logics and Tools</i> (Vol. 10460, pp. 367–381). Springer. <a href=\"https://doi.org/10.1007/978-3-319-63121-9_18\">https://doi.org/10.1007/978-3-319-63121-9_18</a>","ieee":"K. Chatterjee, L. Doyen, and T. A. Henzinger, “The cost of exactness in quantitative reachability,” in <i>Models, Algorithms, Logics and Tools</i>, vol. 10460, L. Aceto, G. Bacci, A. Ingólfsdóttir, A. Legay, and R. Mardare, Eds. Springer, 2017, pp. 367–381."},"type":"book_chapter","file":[{"access_level":"open_access","file_name":"2017_ModelsAlgorithms_Chatterjee.pdf","content_type":"application/pdf","date_updated":"2020-07-14T12:47:25Z","file_size":192826,"checksum":"b2402766ec02c79801aac634bd8f9f6c","relation":"main_file","creator":"dernst","date_created":"2019-11-19T08:06:50Z","file_id":"7048"}],"ddc":["000"],"language":[{"iso":"eng"}],"has_accepted_license":"1","status":"public","publication_status":"published","abstract":[{"lang":"eng","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."}],"publist_id":"7170","quality_controlled":"1"},{"project":[{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"}],"_id":"628","date_created":"2018-12-11T11:47:35Z","page":"118 - 139","date_published":"2017-01-01T00:00:00Z","ec_funded":1,"title":"Automated recurrence analysis for almost linear expected runtime bounds","date_updated":"2021-01-12T08:06:55Z","month":"01","scopus_import":1,"oa":1,"intvolume":"     10426","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1705.00314"}],"alternative_title":["LNCS"],"volume":10426,"publisher":"Springer","day":"01","doi":"10.1007/978-3-319-63387-9_6","oa_version":"Submitted Version","conference":{"location":"Heidelberg, Germany","start_date":"2017-07-24","end_date":"2017-07-28","name":"CAV: Computer Aided Verification"},"year":"2017","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Hongfei","last_name":"Fu","full_name":"Fu, Hongfei"},{"full_name":"Murhekar, Aniket","last_name":"Murhekar","first_name":"Aniket"}],"editor":[{"first_name":"Rupak","full_name":"Majumdar, Rupak","last_name":"Majumdar"},{"first_name":"Viktor","last_name":"Kunčak","full_name":"Kunčak, Viktor"}],"department":[{"_id":"KrCh"}],"publication_identifier":{"isbn":["978-331963386-2"]},"type":"conference","citation":{"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>.","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>","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."},"quality_controlled":"1","publist_id":"7166","abstract":[{"lang":"eng","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."}],"publication_status":"published","status":"public","language":[{"iso":"eng"}]},{"month":"01","date_updated":"2025-06-02T08:53:47Z","title":"Non-polynomial worst case analysis of recursive programs","ec_funded":1,"article_processing_charge":"No","date_published":"2017-01-01T00:00:00Z","page":"41 - 63","external_id":{"arxiv":["1705.00317"]},"date_created":"2018-12-11T11:47:39Z","project":[{"name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"}],"_id":"639","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1705.00317"}],"related_material":{"record":[{"id":"8934","status":"public","relation":"dissertation_contains"},{"status":"public","relation":"later_version","id":"7014"}]},"alternative_title":["LNCS"],"volume":10427,"oa":1,"intvolume":"     10427","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"publication_identifier":{"isbn":["978-331963389-3"]},"department":[{"_id":"KrCh"}],"editor":[{"full_name":"Majumdar, Rupak","last_name":"Majumdar","first_name":"Rupak"},{"full_name":"Kunčak, Viktor","last_name":"Kunčak","first_name":"Viktor"}],"year":"2017","conference":{"name":"CAV: Computer Aided Verification","end_date":"2017-07-28","location":"Heidelberg, Germany","start_date":"2017-07-24"},"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"full_name":"Fu, Hongfei","last_name":"Fu","first_name":"Hongfei"},{"orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir","last_name":"Goharshady","id":"391365CE-F248-11E8-B48F-1D18A9856A87","first_name":"Amir"}],"arxiv":1,"oa_version":"Submitted Version","doi":"10.1007/978-3-319-63390-9_3","day":"01","publisher":"Springer","status":"public","language":[{"iso":"eng"}],"publist_id":"7149","publication_status":"published","abstract":[{"lang":"eng","text":"We study the problem of developing efficient approaches for proving worst-case bounds of non-deterministic recursive programs. Ranking functions are sound and complete for proving termination and worst-case bounds of non-recursive programs. First, we apply ranking functions to recursion, resulting in measure functions, and show that they provide a sound and complete approach to prove worst-case bounds of non-deterministic recursive programs. Our second contribution is the synthesis of measure functions in non-polynomial forms. We show that non-polynomial measure functions with logarithm and exponentiation can be synthesized through abstraction of logarithmic or exponentiation terms, Farkas’ Lemma, and Handelman’s Theorem using linear programming. While previous methods obtain worst-case polynomial bounds, our approach can synthesize bounds of the form O(n log n) as well as O(nr) where r is not an integer. We present experimental results to demonstrate that our approach can efficiently obtain worst-case bounds of classical recursive algorithms such as Merge-Sort, Closest-Pair, Karatsuba’s algorithm and Strassen’s algorithm."}],"quality_controlled":"1","citation":{"ieee":"K. Chatterjee, H. Fu, and A. K. Goharshady, “Non-polynomial worst case analysis of recursive programs,” presented at the CAV: Computer Aided Verification, Heidelberg, Germany, 2017, vol. 10427, pp. 41–63.","apa":"Chatterjee, K., Fu, H., &#38; Goharshady, A. K. (2017). Non-polynomial worst case analysis of recursive programs. In R. Majumdar &#38; V. Kunčak (Eds.) (Vol. 10427, pp. 41–63). Presented at the CAV: Computer Aided Verification, Heidelberg, Germany: Springer. <a href=\"https://doi.org/10.1007/978-3-319-63390-9_3\">https://doi.org/10.1007/978-3-319-63390-9_3</a>","short":"K. Chatterjee, H. Fu, A.K. Goharshady, in:, R. Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 41–63.","ista":"Chatterjee K, Fu H, Goharshady AK. 2017. Non-polynomial worst case analysis of recursive programs. CAV: Computer Aided Verification, LNCS, vol. 10427, 41–63.","mla":"Chatterjee, Krishnendu, et al. <i>Non-Polynomial Worst Case Analysis of Recursive Programs</i>. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10427, Springer, 2017, pp. 41–63, doi:<a href=\"https://doi.org/10.1007/978-3-319-63390-9_3\">10.1007/978-3-319-63390-9_3</a>.","ama":"Chatterjee K, Fu H, Goharshady AK. Non-polynomial worst case analysis of recursive programs. In: Majumdar R, Kunčak V, eds. Vol 10427. Springer; 2017:41-63. doi:<a href=\"https://doi.org/10.1007/978-3-319-63390-9_3\">10.1007/978-3-319-63390-9_3</a>","chicago":"Chatterjee, Krishnendu, Hongfei Fu, and Amir Kafshdar Goharshady. “Non-Polynomial Worst Case Analysis of Recursive Programs.” edited by Rupak Majumdar and Viktor Kunčak, 10427:41–63. Springer, 2017. <a href=\"https://doi.org/10.1007/978-3-319-63390-9_3\">https://doi.org/10.1007/978-3-319-63390-9_3</a>."},"type":"conference"},{"type":"conference","citation":{"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.","short":"P. Ashok, K. Chatterjee, P. Daca, J. Kretinsky, T. Meggendorfer, in:, R. Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 201–221.","apa":"Ashok, P., Chatterjee, K., Daca, P., Kretinsky, J., &#38; Meggendorfer, T. (2017). Value iteration for long run average reward in markov decision processes. In R. Majumdar &#38; V. Kunčak (Eds.) (Vol. 10426, pp. 201–221). Presented at the CAV: Computer Aided Verification, Heidelberg, Germany: Springer. <a href=\"https://doi.org/10.1007/978-3-319-63387-9_10\">https://doi.org/10.1007/978-3-319-63387-9_10</a>","mla":"Ashok, Pranav, et al. <i>Value Iteration for Long Run Average Reward in Markov Decision Processes</i>. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10426, Springer, 2017, pp. 201–21, doi:<a href=\"https://doi.org/10.1007/978-3-319-63387-9_10\">10.1007/978-3-319-63387-9_10</a>.","ista":"Ashok P, Chatterjee K, Daca P, Kretinsky J, Meggendorfer T. 2017. Value iteration for long run average reward in markov decision processes. CAV: Computer Aided Verification, LNCS, vol. 10426, 201–221.","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>.","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>"},"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."}],"publication_status":"published","publist_id":"7135","language":[{"iso":"eng"}],"status":"public","quality_controlled":"1","doi":"10.1007/978-3-319-63387-9_10","oa_version":"Submitted Version","publisher":"Springer","day":"13","publication_identifier":{"isbn":["978-331963386-2"]},"department":[{"_id":"KrCh"}],"author":[{"last_name":"Ashok","full_name":"Ashok, Pranav","first_name":"Pranav"},{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"last_name":"Daca","full_name":"Daca, Przemyslaw","first_name":"Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan","last_name":"Kretinsky"},{"first_name":"Tobias","full_name":"Meggendorfer, Tobias","last_name":"Meggendorfer"}],"conference":{"name":"CAV: Computer Aided Verification","end_date":"2017-07-28","location":"Heidelberg, Germany","start_date":"2017-07-24"},"year":"2017","editor":[{"first_name":"Rupak","full_name":"Majumdar, Rupak","last_name":"Majumdar"},{"last_name":"Kunčak","full_name":"Kunčak, Viktor","first_name":"Viktor"}],"scopus_import":1,"volume":10426,"alternative_title":["LNCS"],"main_file_link":[{"url":"https://arxiv.org/abs/1705.02326","open_access":"1"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","oa":1,"intvolume":"     10426","page":"201 - 221","_id":"645","project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"}],"date_created":"2018-12-11T11:47:41Z","title":"Value iteration for long run average reward in markov decision processes","date_updated":"2021-01-12T08:07:32Z","month":"07","date_published":"2017-07-13T00:00:00Z","ec_funded":1},{"ec_funded":1,"date_published":"2017-08-01T00:00:00Z","article_processing_charge":"No","month":"08","title":"Improved set-based symbolic algorithms for parity games","date_updated":"2025-06-02T08:53:46Z","date_created":"2019-06-04T12:42:43Z","project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7"},{"name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003"}],"_id":"6519","file_date_updated":"2020-07-14T12:47:33Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa":1,"intvolume":"        82","article_number":"18","volume":82,"scopus_import":"1","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"first_name":"Wolfgang","full_name":"Dvorák, Wolfgang","last_name":"Dvorák"},{"first_name":"Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","last_name":"Henzinger","orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H"},{"full_name":"Loitzenbauer, Veronika","last_name":"Loitzenbauer","first_name":"Veronika"}],"conference":{"start_date":"2017-08-20","location":"Stockholm, Sweden","end_date":"2017-08-24","name":"CSL: Conference on Computer Science Logic"},"year":"2017","tmp":{"short":"CC BY (3.0)","name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)","legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode","image":"/images/cc_by.png"},"department":[{"_id":"KrCh"}],"day":"01","publisher":"Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik","oa_version":"Published Version","doi":"10.4230/LIPICS.CSL.2017.18","quality_controlled":"1","language":[{"iso":"eng"}],"status":"public","has_accepted_license":"1","publication_status":"published","abstract":[{"text":"Graph games with omega-regular winning conditions provide a mathematical framework to analyze a wide range of problems in the analysis of reactive systems and programs (such as the synthesis of reactive systems, program repair, and the verification of branching time properties). Parity conditions are canonical forms to specify omega-regular winning conditions. Graph games with parity conditions are equivalent to mu-calculus model checking, and thus a very important algorithmic problem. Symbolic algorithms are of great significance because they provide scalable algorithms for the analysis of large finite-state systems, as well as algorithms for the analysis of infinite-state systems with finite quotient. A set-based symbolic algorithm uses the basic set operations and the one-step predecessor operators. We consider graph games with n vertices and parity conditions with c priorities (equivalently, a mu-calculus formula with c alternations of least and greatest fixed points). While many explicit algorithms exist for graph games with parity conditions, for set-based symbolic algorithms there are only two algorithms (notice that we use space to refer to the number of sets stored by a symbolic algorithm): (a) the basic algorithm that requires O(n^c) symbolic operations and linear space; and (b) an improved algorithm that requires O(n^{c/2+1}) symbolic operations but also O(n^{c/2+1}) space (i.e., exponential space). In this work we present two set-based symbolic algorithms for parity games: (a) our first algorithm requires O(n^{c/2+1}) symbolic operations and only requires linear space; and (b) developing on our first algorithm, we present an algorithm that requires O(n^{c/3+1}) symbolic operations and only linear space. We also present the first linear space set-based symbolic algorithm for parity games that requires at most a sub-exponential number of symbolic operations. ","lang":"eng"}],"ddc":["004"],"type":"conference","citation":{"ieee":"K. Chatterjee, W. Dvorák, M. H. Henzinger, and V. Loitzenbauer, “Improved set-based symbolic algorithms for parity games,” presented at the CSL: Conference on Computer Science Logic, Stockholm, Sweden, 2017, vol. 82.","apa":"Chatterjee, K., Dvorák, W., Henzinger, M. H., &#38; Loitzenbauer, V. (2017). Improved set-based symbolic algorithms for parity games (Vol. 82). Presented at the CSL: Conference on Computer Science Logic, Stockholm, Sweden: Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik. <a href=\"https://doi.org/10.4230/LIPICS.CSL.2017.18\">https://doi.org/10.4230/LIPICS.CSL.2017.18</a>","short":"K. Chatterjee, W. Dvorák, M.H. Henzinger, V. Loitzenbauer, in:, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, 2017.","ista":"Chatterjee K, Dvorák W, Henzinger MH, Loitzenbauer V. 2017. Improved set-based symbolic algorithms for parity games. CSL: Conference on Computer Science Logic vol. 82, 18.","mla":"Chatterjee, Krishnendu, et al. <i>Improved Set-Based Symbolic Algorithms for Parity Games</i>. Vol. 82, 18, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, 2017, doi:<a href=\"https://doi.org/10.4230/LIPICS.CSL.2017.18\">10.4230/LIPICS.CSL.2017.18</a>.","chicago":"Chatterjee, Krishnendu, Wolfgang Dvorák, Monika H Henzinger, and Veronika Loitzenbauer. “Improved Set-Based Symbolic Algorithms for Parity Games,” Vol. 82. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, 2017. <a href=\"https://doi.org/10.4230/LIPICS.CSL.2017.18\">https://doi.org/10.4230/LIPICS.CSL.2017.18</a>.","ama":"Chatterjee K, Dvorák W, Henzinger MH, Loitzenbauer V. Improved set-based symbolic algorithms for parity games. In: Vol 82. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik; 2017. doi:<a href=\"https://doi.org/10.4230/LIPICS.CSL.2017.18\">10.4230/LIPICS.CSL.2017.18</a>"},"file":[{"access_level":"open_access","file_name":"2017_LIPIcs-Chatterjee.pdf","file_size":710185,"date_updated":"2020-07-14T12:47:33Z","content_type":"application/pdf","relation":"main_file","checksum":"7c2c9d09970af79026d7e37d9b632ef8","creator":"kschuh","date_created":"2019-06-04T12:56:52Z","file_id":"6520"}]},{"scopus_import":"1","oa":1,"intvolume":"        49","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.).","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","issue":"3","volume":49,"_id":"653","project":[{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Game Theory","call_identifier":"FWF","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"}],"external_id":{"pmid":["28092682"]},"date_created":"2018-12-11T11:47:43Z","publication":"Nature Genetics","file_date_updated":"2020-07-14T12:47:33Z","page":"358 - 366","article_processing_charge":"No","date_published":"2017-03-01T00:00:00Z","ec_funded":1,"date_updated":"2022-06-10T09:55:08Z","title":"Limited heterogeneity of known driver gene mutations among the metastases of individual patients with pancreatic cancer","month":"03","ddc":["000"],"article_type":"original","file":[{"file_id":"7050","date_created":"2019-11-19T08:13:50Z","creator":"dernst","file_size":908099,"content_type":"application/pdf","date_updated":"2020-07-14T12:47:33Z","relation":"main_file","checksum":"e442dc3b7420a36ec805e9bb45cc1a2e","access_level":"open_access","file_name":"2017_NatureGenetics_Makohon.pdf"}],"type":"journal_article","citation":{"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.","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.","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>.","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.","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>.","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>"},"quality_controlled":"1","publist_id":"7092","publication_status":"published","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."}],"has_accepted_license":"1","status":"public","pmid":1,"language":[{"iso":"eng"}],"publisher":"Nature Publishing Group","day":"01","doi":"10.1038/ng.3764","oa_version":"Submitted Version","year":"2017","author":[{"first_name":"Alvin","full_name":"Makohon Moore, Alvin","last_name":"Makohon Moore"},{"first_name":"Ming","last_name":"Zhang","full_name":"Zhang, Ming"},{"first_name":"Johannes","id":"4A918E98-F248-11E8-B48F-1D18A9856A87","full_name":"Reiter, Johannes","orcid":"0000-0002-0170-7353","last_name":"Reiter"},{"last_name":"Božić","full_name":"Božić, Ivana","first_name":"Ivana"},{"last_name":"Allen","full_name":"Allen, Benjamin","first_name":"Benjamin"},{"id":"1d4c0f4f-e8a3-11ec-a351-e36772758c45","first_name":"Deepanjan","full_name":"Kundu, Deepanjan","last_name":"Kundu"},{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"full_name":"Wong, Fay","last_name":"Wong","first_name":"Fay"},{"full_name":"Jiao, Yuchen","last_name":"Jiao","first_name":"Yuchen"},{"first_name":"Zachary","last_name":"Kohutek","full_name":"Kohutek, Zachary"},{"last_name":"Hong","full_name":"Hong, Jungeui","first_name":"Jungeui"},{"first_name":"Marc","last_name":"Attiyeh","full_name":"Attiyeh, Marc"},{"first_name":"Breanna","full_name":"Javier, Breanna","last_name":"Javier"},{"first_name":"Laura","last_name":"Wood","full_name":"Wood, Laura"},{"first_name":"Ralph","full_name":"Hruban, Ralph","last_name":"Hruban"},{"first_name":"Martin","full_name":"Nowak, Martin","last_name":"Nowak"},{"first_name":"Nickolas","full_name":"Papadopoulos, Nickolas","last_name":"Papadopoulos"},{"last_name":"Kinzler","full_name":"Kinzler, Kenneth","first_name":"Kenneth"},{"first_name":"Bert","full_name":"Vogelstein, Bert","last_name":"Vogelstein"},{"last_name":"Iacobuzio Donahue","full_name":"Iacobuzio Donahue, Christine","first_name":"Christine"}],"department":[{"_id":"KrCh"}],"publication_identifier":{"issn":["10614036"]}},{"type":"journal_article","citation":{"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>.","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>.","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>","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.","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."},"quality_controlled":"1","language":[{"iso":"eng"}],"status":"public","pmid":1,"publication_status":"published","abstract":[{"lang":"eng","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."}],"publist_id":"7053","day":"02","publisher":"National Academy of Sciences","oa_version":"Published Version","doi":"10.1073/pnas.1621239114","author":[{"first_name":"Christian","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5116-955X","full_name":"Hilbe, Christian","last_name":"Hilbe"},{"last_name":"Martinez","full_name":"Martinez, Vaquero","first_name":"Vaquero"},{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"first_name":"Martin","full_name":"Nowak, Martin","last_name":"Nowak"}],"year":"2017","department":[{"_id":"KrCh"}],"publication_identifier":{"issn":["00278424"]},"scopus_import":1,"issue":"18","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","intvolume":"       114","oa":1,"volume":114,"main_file_link":[{"open_access":"1","url":"https://www.ncbi.nlm.nih.gov/pmc/articles/PMC5422766/"}],"date_created":"2018-12-11T11:47:50Z","external_id":{"pmid":["28420786"]},"_id":"671","project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"page":"4715 - 4720","publication":"PNAS","ec_funded":1,"date_published":"2017-05-02T00:00:00Z","article_processing_charge":"Yes (in subscription journal)","month":"05","date_updated":"2021-01-12T08:08:37Z","title":"Memory-n strategies of direct reciprocity"},{"publication":"Information and Computation","page":"296 - 315","_id":"681","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF"},{"name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734","call_identifier":"FP7"}],"date_created":"2018-12-11T11:47:53Z","external_id":{"arxiv":["1311.3238"]},"date_updated":"2023-02-21T16:06:02Z","title":"Doomsday equilibria for omega-regular games","month":"06","date_published":"2017-06-01T00:00:00Z","article_processing_charge":"No","ec_funded":1,"scopus_import":"1","volume":254,"main_file_link":[{"url":"https://arxiv.org/abs/1311.3238","open_access":"1"}],"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"10885"}]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa":1,"intvolume":"       254","doi":"10.1016/j.ic.2016.10.012","arxiv":1,"oa_version":"Submitted Version","publisher":"Elsevier","day":"01","department":[{"_id":"KrCh"}],"publication_identifier":{"issn":["08905401"]},"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"first_name":"Laurent","full_name":"Doyen, Laurent","last_name":"Doyen"},{"last_name":"Filiot","full_name":"Filiot, Emmanuel","first_name":"Emmanuel"},{"first_name":"Jean","full_name":"Raskin, Jean","last_name":"Raskin"}],"year":"2017","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>","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>.","ista":"Chatterjee K, Doyen L, Filiot E, Raskin J. 2017. Doomsday equilibria for omega-regular games. Information and Computation. 254, 296–315.","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>.","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>","short":"K. Chatterjee, L. Doyen, E. Filiot, J. Raskin, Information and Computation 254 (2017) 296–315.","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."},"type":"journal_article","article_type":"original","abstract":[{"lang":"eng","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."}],"publication_status":"published","publist_id":"7036","language":[{"iso":"eng"}],"status":"public","quality_controlled":"1"},{"citation":{"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>.","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>","ista":"Chatterjee K, Piterman N. 2017. Obligation blackwell games and p-automata. Journal of Symbolic Logic. 82(2), 420–452.","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>.","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.","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."},"type":"journal_article","quality_controlled":"1","language":[{"iso":"eng"}],"status":"public","publication_status":"published","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."}],"publist_id":"7026","day":"01","publisher":"Cambridge University Press","oa_version":"Submitted Version","doi":"10.1017/jsl.2016.71","author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"first_name":"Nir","last_name":"Piterman","full_name":"Piterman, Nir"}],"year":"2017","department":[{"_id":"KrCh"}],"publication_identifier":{"eissn":["1943-5886"],"issn":["0022-4812"]},"scopus_import":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","issue":"2","oa":1,"intvolume":"        82","volume":82,"main_file_link":[{"url":"https://arxiv.org/abs/1206.5174","open_access":"1"}],"date_created":"2018-12-11T11:47:54Z","_id":"684","page":"420 - 452","publication":"Journal of Symbolic Logic","date_published":"2017-06-01T00:00:00Z","article_processing_charge":"No","month":"06","date_updated":"2021-04-16T12:10:53Z","title":"Obligation blackwell games and p-automata"},{"scopus_import":"1","main_file_link":[{"open_access":"1","url":"http://www.aaai.org/ocs/index.php/AAAI/AAAI17/paper/download/14354/14092"}],"volume":5,"oa":1,"intvolume":"         5","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","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].","publication":"Proceedings of the 31st AAAI Conference on Artificial Intelligence","page":"3725 - 3732","project":[{"name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734","call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"}],"_id":"1009","external_id":{"isi":["000485630703107"]},"date_created":"2018-12-11T11:49:40Z","date_updated":"2025-06-02T08:53:49Z","title":"Optimizing expectation with guarantees in POMDPs","month":"01","article_processing_charge":"No","date_published":"2017-01-01T00:00:00Z","ec_funded":1,"citation":{"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.","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.","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.","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.","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.","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."},"type":"conference","publist_id":"6387","publication_status":"published","abstract":[{"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.","lang":"eng"}],"status":"public","language":[{"iso":"eng"}],"quality_controlled":"1","oa_version":"Submitted Version","publisher":"AAAI Press","day":"01","department":[{"_id":"KrCh"}],"year":"2017","conference":{"location":"San Francisco, CA, United States","start_date":"2017-02-04","end_date":"2017-02-10","name":"AAAI: Conference on Artificial Intelligence"},"isi":1,"author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"full_name":"Novotny, Petr","last_name":"Novotny","first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Pérez, Guillermo","last_name":"Pérez","first_name":"Guillermo"},{"first_name":"Jean","full_name":"Raskin, Jean","last_name":"Raskin"},{"full_name":"Zikelic, Djordje","last_name":"Zikelic","first_name":"Djordje"}]},{"external_id":{"isi":["000681702400011"]},"date_created":"2018-12-11T11:49:41Z","_id":"1011","project":[{"name":"Moderne Concurrency Paradigms","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","call_identifier":"FWF"},{"name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","call_identifier":"FWF"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"call_identifier":"FWF","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"}],"page":"287 - 313","ec_funded":1,"article_processing_charge":"No","date_published":"2017-03-19T00:00:00Z","month":"03","date_updated":"2023-09-22T09:44:50Z","title":"Faster algorithms for weighted recursive state machines","scopus_import":"1","oa":1,"intvolume":"     10201","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","main_file_link":[{"url":"https://arxiv.org/abs/1701.04914","open_access":"1"}],"alternative_title":["LNCS"],"volume":10201,"day":"19","publisher":"Springer","oa_version":"Submitted Version","doi":"10.1007/978-3-662-54434-1_11","editor":[{"last_name":"Yang","full_name":"Yang, Hongseok","first_name":"Hongseok"}],"year":"2017","conference":{"name":"ESOP: European Symposium on Programming","start_date":"2017-04-22","location":"Uppsala, Sweden","end_date":"2017-04-29"},"isi":1,"author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"id":"320FC952-F248-11E8-B48F-1D18A9856A87","first_name":"Bernhard","full_name":"Kragl, Bernhard","orcid":"0000-0001-7745-9117","last_name":"Kragl"},{"last_name":"Mishra","full_name":"Mishra, Samarth","first_name":"Samarth"},{"orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"}],"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publication_identifier":{"issn":["03029743"]},"citation":{"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.","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>","short":"K. Chatterjee, B. Kragl, S. Mishra, A. Pavlogiannis, in:, H. Yang (Ed.), Springer, 2017, pp. 287–313.","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>.","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>.","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>"},"type":"conference","quality_controlled":"1","status":"public","language":[{"iso":"eng"}],"publist_id":"6384","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."}],"publication_status":"published"},{"article_number":"30","intvolume":"         2","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","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","issue":"POPL","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"5455"}]},"volume":2,"scopus_import":"1","article_processing_charge":"No","date_published":"2017-12-27T00:00:00Z","ec_funded":1,"title":"Optimal Dyck reachability for data-dependence and Alias analysis","date_updated":"2023-02-23T12:27:13Z","month":"12","_id":"10416","project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"}],"external_id":{"arxiv":["1910.00241"]},"date_created":"2021-12-05T23:01:48Z","publication":"Proceedings of the ACM on Programming Languages","file_date_updated":"2021-12-07T08:06:28Z","quality_controlled":"1","publication_status":"published","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."}],"status":"public","has_accepted_license":"1","language":[{"iso":"eng"}],"ddc":["000"],"article_type":"original","file":[{"file_id":"10421","date_created":"2021-12-07T08:06:28Z","creator":"cchlebak","relation":"main_file","checksum":"faa3f7b3fe8aab84b50ed805c26a0ee5","content_type":"application/pdf","date_updated":"2021-12-07T08:06:28Z","file_size":460188,"file_name":"2017_ACMProgLang_Chatterjee.pdf","success":1,"access_level":"open_access"}],"type":"journal_article","citation":{"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.","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>","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.","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>","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>."},"year":"2017","conference":{"name":"POPL: Programming Languages","location":"Los Angeles, CA, United States","start_date":"2018-01-07","end_date":"2018-01-13"},"author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"first_name":"Bhavya","last_name":"Choudhary","full_name":"Choudhary, Bhavya"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas"}],"publication_identifier":{"eissn":["2475-1421"]},"department":[{"_id":"KrCh"}],"tmp":{"image":"/images/cc_by.png","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"publisher":"Association for Computing Machinery","day":"27","doi":"10.1145/3158118","oa_version":"Published Version","arxiv":1}]