[{"publist_id":"5927","scopus_import":"1","_id":"1340","intvolume":"      9928","oa_version":"Preprint","type":"conference","date_published":"2016-09-01T00:00:00Z","language":[{"iso":"eng"}],"month":"09","date_updated":"2025-09-22T08:18:27Z","arxiv":1,"department":[{"_id":"KrCh"}],"publisher":"Springer","isi":1,"oa":1,"alternative_title":["LNCS"],"day":"01","status":"public","ec_funded":1,"citation":{"ista":"Hansen K, Ibsen-Jensen R, Koucký M. 2016. The big match in small space. SAGT: Symposium on Algorithmic Game Theory, LNCS, vol. 9928, 64–76.","ama":"Hansen K, Ibsen-Jensen R, Koucký M. The big match in small space. In: Vol 9928. Springer; 2016:64-76. doi:<a href=\"https://doi.org/10.1007/978-3-662-53354-3_6\">10.1007/978-3-662-53354-3_6</a>","ieee":"K. Hansen, R. Ibsen-Jensen, and M. Koucký, “The big match in small space,” presented at the SAGT: Symposium on Algorithmic Game Theory, Liverpool, United Kingdom, 2016, vol. 9928, pp. 64–76.","short":"K. Hansen, R. Ibsen-Jensen, M. Koucký, in:, Springer, 2016, pp. 64–76.","mla":"Hansen, Kristoffer, et al. <i>The Big Match in Small Space</i>. Vol. 9928, Springer, 2016, pp. 64–76, doi:<a href=\"https://doi.org/10.1007/978-3-662-53354-3_6\">10.1007/978-3-662-53354-3_6</a>.","chicago":"Hansen, Kristoffer, Rasmus Ibsen-Jensen, and Michal Koucký. “The Big Match in Small Space,” 9928:64–76. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-662-53354-3_6\">https://doi.org/10.1007/978-3-662-53354-3_6</a>.","apa":"Hansen, K., Ibsen-Jensen, R., &#38; Koucký, M. (2016). The big match in small space (Vol. 9928, pp. 64–76). Presented at the SAGT: Symposium on Algorithmic Game Theory, Liverpool, United Kingdom: Springer. <a href=\"https://doi.org/10.1007/978-3-662-53354-3_6\">https://doi.org/10.1007/978-3-662-53354-3_6</a>"},"project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","author":[{"full_name":"Hansen, Kristoffer","last_name":"Hansen","first_name":"Kristoffer"},{"last_name":"Ibsen-Jensen","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389"},{"full_name":"Koucký, Michal","last_name":"Koucký","first_name":"Michal"}],"volume":9928,"title":"The big match in small space","article_processing_charge":"No","page":"64 - 76","publication_status":"published","external_id":{"arxiv":["1604.07634"],"isi":["000389020400006"]},"abstract":[{"text":"We study repeated games with absorbing states, a type of two-player, zero-sum concurrent mean-payoff games with the prototypical example being the Big Match of Gillete (1957). These games may not allow optimal strategies but they always have ε-optimal strategies. In this paper we design ε-optimal strategies for Player 1 in these games that use only O(log log T) space. Furthermore, we construct strategies for Player 1 that use space s(T), for an arbitrary small unbounded non-decreasing function s, and which guarantee an ε-optimal value for Player 1 in the limit superior sense. The previously known strategies use space Ω(log T) and it was known that no strategy can use constant space if it is ε-optimal even in the limit superior sense. We also give a complementary lower bound. Furthermore, we also show that no Markov strategy, even extended with finite memory, can ensure value greater than 0 in the Big Match, answering a question posed by Neyman [11].","lang":"eng"}],"doi":"10.1007/978-3-662-53354-3_6","date_created":"2018-12-11T11:51:28Z","year":"2016","main_file_link":[{"url":"https://arxiv.org/abs/1604.07634","open_access":"1"}],"conference":{"start_date":"2016-09-19","name":"SAGT: Symposium on Algorithmic Game Theory","location":"Liverpool, United Kingdom","end_date":"2016-09-21"},"quality_controlled":"1"},{"title":"On the complexity of the orbit problem","abstract":[{"lang":"eng","text":"We consider higher-dimensional versions of Kannan and Lipton's Orbit Problem - determining whether a target vector space V may be reached from a starting point x under repeated applications of a linear transformation A. Answering two questions posed by Kannan and Lipton in the 1980s, we show that when V has dimension one, this problem is solvable in polynomial time, and when V has dimension two or three, the problem is in NPRP."}],"external_id":{"isi":["000382753300004"],"arxiv":["1303.2981"]},"publication_status":"published","article_processing_charge":"No","volume":63,"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","author":[{"first_name":"Ventsislav K","last_name":"Chonev","full_name":"Chonev, Ventsislav K","id":"36CBE2E6-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Ouaknine","first_name":"Joël","full_name":"Ouaknine, Joël"},{"full_name":"Worrell, James","first_name":"James","last_name":"Worrell"}],"main_file_link":[{"url":"http://arxiv.org/abs/1303.2981","open_access":"1"}],"quality_controlled":"1","publication":"Journal of the ACM","issue":"3","doi":"10.1145/2857050","article_number":"23","year":"2016","date_created":"2018-12-11T11:51:41Z","publisher":"ACM","arxiv":1,"department":[{"_id":"KrCh"}],"date_updated":"2025-09-22T07:33:47Z","month":"06","language":[{"iso":"eng"}],"date_published":"2016-06-01T00:00:00Z","oa":1,"isi":1,"_id":"1380","scopus_import":"1","publist_id":"5831","type":"journal_article","intvolume":"        63","oa_version":"Preprint","citation":{"apa":"Chonev, V. K., Ouaknine, J., &#38; Worrell, J. (2016). On the complexity of the orbit problem. <i>Journal of the ACM</i>. ACM. <a href=\"https://doi.org/10.1145/2857050\">https://doi.org/10.1145/2857050</a>","chicago":"Chonev, Ventsislav K, Joël Ouaknine, and James Worrell. “On the Complexity of the Orbit Problem.” <i>Journal of the ACM</i>. ACM, 2016. <a href=\"https://doi.org/10.1145/2857050\">https://doi.org/10.1145/2857050</a>.","mla":"Chonev, Ventsislav K., et al. “On the Complexity of the Orbit Problem.” <i>Journal of the ACM</i>, vol. 63, no. 3, 23, ACM, 2016, doi:<a href=\"https://doi.org/10.1145/2857050\">10.1145/2857050</a>.","ieee":"V. K. Chonev, J. Ouaknine, and J. Worrell, “On the complexity of the orbit problem,” <i>Journal of the ACM</i>, vol. 63, no. 3. ACM, 2016.","short":"V.K. Chonev, J. Ouaknine, J. Worrell, Journal of the ACM 63 (2016).","ama":"Chonev VK, Ouaknine J, Worrell J. On the complexity of the orbit problem. <i>Journal of the ACM</i>. 2016;63(3). doi:<a href=\"https://doi.org/10.1145/2857050\">10.1145/2857050</a>","ista":"Chonev VK, Ouaknine J, Worrell J. 2016. On the complexity of the orbit problem. Journal of the ACM. 63(3), 23."},"day":"01","status":"public"},{"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","author":[{"id":"36CBE2E6-F248-11E8-B48F-1D18A9856A87","full_name":"Chonev, Ventsislav K","last_name":"Chonev","first_name":"Ventsislav K"},{"full_name":"Ouaknine, Joël","first_name":"Joël","last_name":"Ouaknine"},{"last_name":"Worrell","first_name":"James","full_name":"Worrell, James"}],"title":"On recurrent reachability for continuous linear dynamical systems","article_processing_charge":"No","page":"515 - 524","publication_status":"published","external_id":{"isi":["000387609200052"],"arxiv":["1507.03632"]},"abstract":[{"text":"The continuous evolution of a wide variety of systems, including continous-time Markov chains and linear hybrid automata, can be\r\ndescribed in terms of linear differential equations. In this paper we study the decision problem of whether the solution x(t) of a system of linear differential equations dx/dt = Ax reaches a target halfspace infinitely often. This recurrent reachability problem can\r\nequivalently be formulated as the following Infinite Zeros Problem: does a real-valued function f:R≥0 --&gt; R satisfying a given linear\r\ndifferential equation have infinitely many zeros? Our main decidability result is that if the differential equation has order at most 7, then the Infinite Zeros Problem is decidable. On the other hand, we show that a decision procedure for the Infinite Zeros Problem at order 9 (and above) would entail a major breakthrough in Diophantine Approximation, specifically an algorithm for computing the Lagrange constants of arbitrary real algebraic numbers to arbitrary precision.","lang":"eng"}],"doi":"10.1145/2933575.2934548","publication":"LICS '16","date_created":"2018-12-11T11:51:44Z","year":"2016","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1507.03632"}],"conference":{"end_date":"2018-07-08","location":"New York, NY, USA","name":"LICS: Logic in Computer Science","start_date":"2018-07-05"},"quality_controlled":"1","publist_id":"5820","scopus_import":"1","_id":"1389","oa_version":"Preprint","type":"conference","date_published":"2016-07-05T00:00:00Z","language":[{"iso":"eng"}],"month":"07","date_updated":"2025-09-22T07:31:08Z","publisher":"IEEE","department":[{"_id":"KrCh"}],"arxiv":1,"isi":1,"oa":1,"status":"public","day":"05","ec_funded":1,"citation":{"ama":"Chonev VK, Ouaknine J, Worrell J. On recurrent reachability for continuous linear dynamical systems. In: <i>LICS ’16</i>. IEEE; 2016:515-524. doi:<a href=\"https://doi.org/10.1145/2933575.2934548\">10.1145/2933575.2934548</a>","ista":"Chonev VK, Ouaknine J, Worrell J. 2016. On recurrent reachability for continuous linear dynamical systems. LICS ’16. LICS: Logic in Computer Science, 515–524.","ieee":"V. K. Chonev, J. Ouaknine, and J. Worrell, “On recurrent reachability for continuous linear dynamical systems,” in <i>LICS ’16</i>, New York, NY, USA, 2016, pp. 515–524.","short":"V.K. Chonev, J. Ouaknine, J. Worrell, in:, LICS ’16, IEEE, 2016, pp. 515–524.","mla":"Chonev, Ventsislav K., et al. “On Recurrent Reachability for Continuous Linear Dynamical Systems.” <i>LICS ’16</i>, IEEE, 2016, pp. 515–24, doi:<a href=\"https://doi.org/10.1145/2933575.2934548\">10.1145/2933575.2934548</a>.","apa":"Chonev, V. K., Ouaknine, J., &#38; Worrell, J. (2016). On recurrent reachability for continuous linear dynamical systems. In <i>LICS ’16</i> (pp. 515–524). New York, NY, USA: IEEE. <a href=\"https://doi.org/10.1145/2933575.2934548\">https://doi.org/10.1145/2933575.2934548</a>","chicago":"Chonev, Ventsislav K, Joël Ouaknine, and James Worrell. “On Recurrent Reachability for Continuous Linear Dynamical Systems.” In <i>LICS ’16</i>, 515–24. IEEE, 2016. <a href=\"https://doi.org/10.1145/2933575.2934548\">https://doi.org/10.1145/2933575.2934548</a>."},"project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7"}]},{"publication":"Scientific Reports","doi":"10.1038/srep25676","article_number":"25676","date_created":"2018-12-11T11:51:56Z","year":"2016","ddc":["000"],"has_accepted_license":"1","quality_controlled":"1","file":[{"creator":"system","date_created":"2018-12-12T10:18:08Z","content_type":"application/pdf","file_name":"IST-2016-590-v1+1_srep25676.pdf","checksum":"ee17c482370d2e1b3add393710d3c696","relation":"main_file","access_level":"open_access","date_updated":"2020-07-14T12:44:53Z","file_size":1349915,"file_id":"5327"}],"corr_author":"1","volume":6,"author":[{"last_name":"Baek","first_name":"Seung","full_name":"Baek, Seung"},{"full_name":"Jeong, Hyeongchai","first_name":"Hyeongchai","last_name":"Jeong"},{"full_name":"Hilbe, Christian","orcid":"0000-0001-5116-955X","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","first_name":"Christian","last_name":"Hilbe"},{"full_name":"Nowak, Martin","first_name":"Martin","last_name":"Nowak"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","title":"Comparing reactive and memory-one strategies of direct reciprocity","external_id":{"isi":["000375448500002"]},"publication_status":"published","abstract":[{"lang":"eng","text":"Direct reciprocity is a mechanism for the evolution of cooperation based on repeated interactions. When individuals meet repeatedly, they can use conditional strategies to enforce cooperative outcomes that would not be feasible in one-shot social dilemmas. Direct reciprocity requires that individuals keep track of their past interactions and find the right response. However, there are natural bounds on strategic complexity: Humans find it difficult to remember past interactions accurately, especially over long timespans. Given these limitations, it is natural to ask how complex strategies need to be for cooperation to evolve. Here, we study stochastic evolutionary game dynamics in finite populations to systematically compare the evolutionary performance of reactive strategies, which only respond to the co-player's previous move, and memory-one strategies, which take into account the own and the co-player's previous move. In both cases, we compare deterministic strategy and stochastic strategy spaces. For reactive strategies and small costs, we find that stochasticity benefits cooperation, because it allows for generous-tit-for-tat. For memory one strategies and small costs, we find that stochasticity does not increase the propensity for cooperation, because the deterministic rule of win-stay, lose-shift works best. For memory one strategies and large costs, however, stochasticity can augment cooperation."}],"article_processing_charge":"No","status":"public","day":"10","pubrep_id":"590","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"citation":{"mla":"Baek, Seung, et al. “Comparing Reactive and Memory-One Strategies of Direct Reciprocity.” <i>Scientific Reports</i>, vol. 6, 25676, Nature Publishing Group, 2016, doi:<a href=\"https://doi.org/10.1038/srep25676\">10.1038/srep25676</a>.","apa":"Baek, S., Jeong, H., Hilbe, C., &#38; Nowak, M. (2016). Comparing reactive and memory-one strategies of direct reciprocity. <i>Scientific Reports</i>. Nature Publishing Group. <a href=\"https://doi.org/10.1038/srep25676\">https://doi.org/10.1038/srep25676</a>","chicago":"Baek, Seung, Hyeongchai Jeong, Christian Hilbe, and Martin Nowak. “Comparing Reactive and Memory-One Strategies of Direct Reciprocity.” <i>Scientific Reports</i>. Nature Publishing Group, 2016. <a href=\"https://doi.org/10.1038/srep25676\">https://doi.org/10.1038/srep25676</a>.","ama":"Baek S, Jeong H, Hilbe C, Nowak M. Comparing reactive and memory-one strategies of direct reciprocity. <i>Scientific Reports</i>. 2016;6. doi:<a href=\"https://doi.org/10.1038/srep25676\">10.1038/srep25676</a>","ista":"Baek S, Jeong H, Hilbe C, Nowak M. 2016. Comparing reactive and memory-one strategies of direct reciprocity. Scientific Reports. 6, 25676.","short":"S. Baek, H. Jeong, C. Hilbe, M. Nowak, Scientific Reports 6 (2016).","ieee":"S. Baek, H. Jeong, C. Hilbe, and M. Nowak, “Comparing reactive and memory-one strategies of direct reciprocity,” <i>Scientific Reports</i>, vol. 6. Nature Publishing Group, 2016."},"scopus_import":"1","_id":"1423","publist_id":"5784","type":"journal_article","acknowledgement":"C.H. acknowledges generous funding from the Schrödinger scholarship of the Austrian Science Fund (FWF), J3475.","oa_version":"Published Version","intvolume":"         6","date_updated":"2025-09-18T14:15:33Z","publisher":"Nature Publishing Group","department":[{"_id":"KrCh"}],"date_published":"2016-05-10T00:00:00Z","month":"05","language":[{"iso":"eng"}],"file_date_updated":"2020-07-14T12:44:53Z","oa":1,"isi":1},{"oa_version":"Preprint","type":"conference","acknowledgement":"Supported by the Natural Science Foundation of China (NSFC) under Grant No. 61532019 ","publist_id":"5760","scopus_import":1,"_id":"1438","oa":1,"date_published":"2016-01-11T00:00:00Z","language":[{"iso":"eng"}],"month":"01","date_updated":"2025-04-15T08:12:22Z","department":[{"_id":"KrCh"}],"publisher":"ACM","arxiv":1,"ec_funded":1,"alternative_title":["POPL"],"day":"11","status":"public","citation":{"mla":"Chatterjee, Krishnendu, et al. <i>Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs</i>. Vol. 20–22, ACM, 2016, pp. 327–42, doi:<a href=\"https://doi.org/10.1145/2837614.2837639\">10.1145/2837614.2837639</a>.","apa":"Chatterjee, K., Fu, H., Novotný, P., &#38; Hasheminezhad, R. (2016). Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs (Vol. 20–22, pp. 327–342). Presented at the POPL: Principles of Programming Languages, St. Petersburg, FL, USA: ACM. <a href=\"https://doi.org/10.1145/2837614.2837639\">https://doi.org/10.1145/2837614.2837639</a>","chicago":"Chatterjee, Krishnendu, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad. “Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs,” 20–22:327–42. ACM, 2016. <a href=\"https://doi.org/10.1145/2837614.2837639\">https://doi.org/10.1145/2837614.2837639</a>.","ista":"Chatterjee K, Fu H, Novotný P, Hasheminezhad R. 2016. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. POPL: Principles of Programming Languages, POPL, vol. 20–22, 327–342.","ama":"Chatterjee K, Fu H, Novotný P, Hasheminezhad R. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. In: Vol 20-22. ACM; 2016:327-342. doi:<a href=\"https://doi.org/10.1145/2837614.2837639\">10.1145/2837614.2837639</a>","ieee":"K. Chatterjee, H. Fu, P. Novotný, and R. Hasheminezhad, “Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs,” presented at the POPL: Principles of Programming Languages, St. Petersburg, FL, USA, 2016, vol. 20–22, pp. 327–342.","short":"K. Chatterjee, H. Fu, P. Novotný, R. Hasheminezhad, in:, ACM, 2016, pp. 327–342."},"project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Fu","first_name":"Hongfei","id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","full_name":"Fu, Hongfei"},{"first_name":"Petr","last_name":"Novotny","full_name":"Novotny, Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Hasheminezhad","first_name":"Rouzbeh","full_name":"Hasheminezhad, Rouzbeh"}],"volume":"20-22","related_material":{"record":[{"id":"5993","relation":"later_version","status":"public"}]},"page":"327 - 342","publication_status":"published","external_id":{"arxiv":["1510.08517"]},"abstract":[{"text":"In this paper, we consider termination of probabilistic programs with real-valued variables. The questions concerned are: (a) qualitative ones that ask (i) whether the program terminates with probability 1 (almost-sure termination) and (ii) whether the expected termination time is finite (finite termination); (b) quantitative ones that ask (i) to approximate the expected termination time (expectation problem) and (ii) to compute a bound B such that the probability to terminate after B steps decreases exponentially (concentration problem). To solve these questions, we utilize the notion of ranking supermartingales which is a powerful approach for proving termination of probabilistic programs. In detail, we focus on algorithmic synthesis of linear ranking-supermartingales over affine probabilistic programs (APP's) with both angelic and demonic non-determinism. An important subclass of APP's is LRAPP which is defined as the class of all APP's over which a linear ranking-supermartingale exists. Our main contributions are as follows. Firstly, we show that the membership problem of LRAPP (i) can be decided in polynomial time for APP's with at most demonic non-determinism, and (ii) is NP-hard and in PSPACE for APP's with angelic non-determinism; moreover, the NP-hardness result holds already for APP's without probability and demonic non-determinism. Secondly, we show that the concentration problem over LRAPP can be solved in the same complexity as for the membership problem of LRAPP. Finally, we show that the expectation problem over LRAPP can be solved in 2EXPTIME and is PSPACE-hard even for APP's without probability and non-determinism (i.e., deterministic programs). Our experimental results demonstrate the effectiveness of our approach to answer the qualitative and quantitative questions over APP's with at most demonic non-determinism.","lang":"eng"}],"title":"Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs","date_created":"2018-12-11T11:52:01Z","year":"2016","doi":"10.1145/2837614.2837639","quality_controlled":"1","main_file_link":[{"url":"http://arxiv.org/abs/1510.08517","open_access":"1"}],"conference":{"location":"St. Petersburg, FL, USA","end_date":"2016-01-22","name":"POPL: Principles of Programming Languages","start_date":"2016-01-20"}},{"article_processing_charge":"No","page":"878 - 911","external_id":{"arxiv":["1309.2802"],"isi":["000374425900015"]},"publication_status":"published","abstract":[{"text":"We consider partially observable Markov decision processes (POMDPs) with ω-regular conditions specified as parity objectives. The class of ω-regular languages provides a robust specification language to express properties in verification, and parity objectives are canonical forms to express them. The qualitative analysis problem given a POMDP and a parity objective asks whether there is a strategy to ensure that the objective is satisfied with probability 1 (resp. positive probability). While the qualitative analysis problems are undecidable even for special cases of parity objectives, we establish decidability (with optimal complexity) for POMDPs with all parity objectives under finite-memory strategies. We establish optimal (exponential) memory bounds and EXPTIME-completeness of the qualitative analysis problems under finite-memory strategies for POMDPs with parity objectives. We also present a practical approach, where we design heuristics to deal with the exponential complexity, and have applied our implementation on a number of POMDP examples.","lang":"eng"}],"title":"What is decidable about partially observable Markov decision processes with ω-regular objectives","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee"},{"id":"3624234E-F248-11E8-B48F-1D18A9856A87","full_name":"Chmelik, Martin","last_name":"Chmelik","first_name":"Martin"},{"first_name":"Mathieu","last_name":"Tracol","full_name":"Tracol, Mathieu","id":"3F54FA38-F248-11E8-B48F-1D18A9856A87"}],"volume":82,"related_material":{"record":[{"status":"public","id":"2295","relation":"earlier_version"},{"id":"5400","relation":"earlier_version","status":"public"}]},"corr_author":"1","quality_controlled":"1","main_file_link":[{"url":"https://arxiv.org/abs/1309.2802","open_access":"1"}],"date_created":"2018-12-11T11:52:15Z","year":"2016","doi":"10.1016/j.jcss.2016.02.009","issue":"5","publication":"Journal of Computer and System Sciences","isi":1,"oa":1,"date_published":"2016-08-01T00:00:00Z","language":[{"iso":"eng"}],"month":"08","date_updated":"2025-09-18T11:38:39Z","department":[{"_id":"KrCh"}],"arxiv":1,"publisher":"Elsevier","intvolume":"        82","oa_version":"Preprint","type":"journal_article","publist_id":"5718","scopus_import":"1","_id":"1477","citation":{"chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Mathieu Tracol. “What Is Decidable about Partially Observable Markov Decision Processes with ω-Regular Objectives.” <i>Journal of Computer and System Sciences</i>. Elsevier, 2016. <a href=\"https://doi.org/10.1016/j.jcss.2016.02.009\">https://doi.org/10.1016/j.jcss.2016.02.009</a>.","apa":"Chatterjee, K., Chmelik, M., &#38; Tracol, M. (2016). What is decidable about partially observable Markov decision processes with ω-regular objectives. <i>Journal of Computer and System Sciences</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.jcss.2016.02.009\">https://doi.org/10.1016/j.jcss.2016.02.009</a>","mla":"Chatterjee, Krishnendu, et al. “What Is Decidable about Partially Observable Markov Decision Processes with ω-Regular Objectives.” <i>Journal of Computer and System Sciences</i>, vol. 82, no. 5, Elsevier, 2016, pp. 878–911, doi:<a href=\"https://doi.org/10.1016/j.jcss.2016.02.009\">10.1016/j.jcss.2016.02.009</a>.","short":"K. Chatterjee, M. Chmelik, M. Tracol, Journal of Computer and System Sciences 82 (2016) 878–911.","ieee":"K. Chatterjee, M. Chmelik, and M. Tracol, “What is decidable about partially observable Markov decision processes with ω-regular objectives,” <i>Journal of Computer and System Sciences</i>, vol. 82, no. 5. Elsevier, pp. 878–911, 2016.","ama":"Chatterjee K, Chmelik M, Tracol M. What is decidable about partially observable Markov decision processes with ω-regular objectives. <i>Journal of Computer and System Sciences</i>. 2016;82(5):878-911. doi:<a href=\"https://doi.org/10.1016/j.jcss.2016.02.009\">10.1016/j.jcss.2016.02.009</a>","ista":"Chatterjee K, Chmelik M, Tracol M. 2016. What is decidable about partially observable Markov decision processes with ω-regular objectives. Journal of Computer and System Sciences. 82(5), 878–911."},"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Game Theory","call_identifier":"FWF","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"ec_funded":1,"day":"01","status":"public"},{"citation":{"mla":"Lohse, Konrad, et al. “Efficient Strategies for Calculating Blockwise Likelihoods under the Coalescent.” <i>Genetics</i>, vol. 202, no. 2, Genetics Society of America, 2016, pp. 775–86, doi:<a href=\"https://doi.org/10.1534/genetics.115.183814\">10.1534/genetics.115.183814</a>.","apa":"Lohse, K., Chmelik, M., Martin, S., &#38; Barton, N. H. (2016). Efficient strategies for calculating blockwise likelihoods under the coalescent. <i>Genetics</i>. Genetics Society of America. <a href=\"https://doi.org/10.1534/genetics.115.183814\">https://doi.org/10.1534/genetics.115.183814</a>","chicago":"Lohse, Konrad, Martin Chmelik, Simon Martin, and Nicholas H Barton. “Efficient Strategies for Calculating Blockwise Likelihoods under the Coalescent.” <i>Genetics</i>. Genetics Society of America, 2016. <a href=\"https://doi.org/10.1534/genetics.115.183814\">https://doi.org/10.1534/genetics.115.183814</a>.","ista":"Lohse K, Chmelik M, Martin S, Barton NH. 2016. Efficient strategies for calculating blockwise likelihoods under the coalescent. Genetics. 202(2), 775–786.","ama":"Lohse K, Chmelik M, Martin S, Barton NH. Efficient strategies for calculating blockwise likelihoods under the coalescent. <i>Genetics</i>. 2016;202(2):775-786. doi:<a href=\"https://doi.org/10.1534/genetics.115.183814\">10.1534/genetics.115.183814</a>","short":"K. Lohse, M. Chmelik, S. Martin, N.H. Barton, Genetics 202 (2016) 775–786.","ieee":"K. Lohse, M. Chmelik, S. Martin, and N. H. Barton, “Efficient strategies for calculating blockwise likelihoods under the coalescent,” <i>Genetics</i>, vol. 202, no. 2. Genetics Society of America, pp. 775–786, 2016."},"project":[{"grant_number":"250152","_id":"25B07788-B435-11E9-9278-68D0E5697425","name":"Limits to selection in biology and in evolutionary computation","call_identifier":"FP7"}],"ec_funded":1,"day":"01","status":"public","pubrep_id":"561","isi":1,"oa":1,"file_date_updated":"2020-07-14T12:45:00Z","language":[{"iso":"eng"}],"month":"02","date_published":"2016-02-01T00:00:00Z","publisher":"Genetics Society of America","department":[{"_id":"KrCh"},{"_id":"NiBa"}],"date_updated":"2025-09-18T11:09:34Z","article_type":"original","oa_version":"Preprint","intvolume":"       202","acknowledgement":"We thank Lynsey Bunnefeld for discussions throughout the project and Joshua Schraiber and one anonymous reviewer\r\nfor constructive comments on an earlier version of this manuscript. This work was supported by funding from the\r\nUnited Kingdom Natural Environment Research Council (to K.L.) (NE/I020288/1) and a grant from the European\r\nResearch Council (250152) (to N.H.B.).","type":"journal_article","publist_id":"5658","_id":"1518","scopus_import":"1","quality_controlled":"1","file":[{"file_id":"5241","access_level":"open_access","checksum":"41c9b5d72e7fe4624dd22dfe622337d5","relation":"main_file","file_size":957466,"date_updated":"2020-07-14T12:45:00Z","date_created":"2018-12-12T10:16:51Z","content_type":"application/pdf","file_name":"IST-2016-561-v1+1_Lohse_et_al_Genetics_2015.pdf","creator":"system"}],"has_accepted_license":"1","ddc":["570"],"year":"2016","date_created":"2018-12-11T11:52:29Z","issue":"2","doi":"10.1534/genetics.115.183814","publication":"Genetics","page":"775 - 786","article_processing_charge":"No","abstract":[{"text":"The inference of demographic history from genome data is hindered by a lack of efficient computational approaches. In particular, it has proved difficult to exploit the information contained in the distribution of genealogies across the genome. We have previously shown that the generating function (GF) of genealogies can be used to analytically compute likelihoods of demographic models from configurations of mutations in short sequence blocks (Lohse et al. 2011). Although the GF has a simple, recursive form, the size of such likelihood calculations explodes quickly with the number of individuals and applications of this framework have so far been mainly limited to small samples (pairs and triplets) for which the GF can be written by hand. Here we investigate several strategies for exploiting the inherent symmetries of the coalescent. In particular, we show that the GF of genealogies can be decomposed into a set of equivalence classes that allows likelihood calculations from nontrivial samples. Using this strategy, we automated blockwise likelihood calculations for a general set of demographic scenarios in Mathematica. These histories may involve population size changes, continuous migration, discrete divergence, and admixture between multiple populations. To give a concrete example, we calculate the likelihood for a model of isolation with migration (IM), assuming two diploid samples without phase and outgroup information. We demonstrate the new inference scheme with an analysis of two individual butterfly genomes from the sister species Heliconius melpomene rosina and H. cydno.","lang":"eng"}],"external_id":{"isi":["000371304600032"],"pmid":["26715666"]},"publication_status":"published","title":"Efficient strategies for calculating blockwise likelihoods under the coalescent","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","author":[{"full_name":"Lohse, Konrad","last_name":"Lohse","first_name":"Konrad"},{"full_name":"Chmelik, Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik","first_name":"Martin"},{"last_name":"Martin","first_name":"Simon","full_name":"Martin, Simon"},{"id":"4880FE40-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8548-5240","full_name":"Barton, Nicholas H","first_name":"Nicholas H","last_name":"Barton"}],"volume":202,"pmid":1},{"department":[{"_id":"KrCh"}],"publisher":"IOS Press","date_updated":"2025-09-22T14:26:27Z","month":"01","language":[{"iso":"eng"}],"date_published":"2016-01-01T00:00:00Z","oa":1,"file_date_updated":"2020-07-14T12:46:35Z","isi":1,"_id":"478","scopus_import":"1","publist_id":"7342","type":"conference","oa_version":"Published Version","intvolume":"       285","citation":{"chicago":"Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. “The Complexity of Deciding Legality of a Single Step of Magic: The Gathering,” 285:1432–39. IOS Press, 2016. <a href=\"https://doi.org/10.3233/978-1-61499-672-9-1432\">https://doi.org/10.3233/978-1-61499-672-9-1432</a>.","apa":"Chatterjee, K., &#38; Ibsen-Jensen, R. (2016). The complexity of deciding legality of a single step of magic: The gathering (Vol. 285, pp. 1432–1439). Presented at the ECAI: European Conference on Artificial Intelligence, The Hague, Netherlands: IOS Press. <a href=\"https://doi.org/10.3233/978-1-61499-672-9-1432\">https://doi.org/10.3233/978-1-61499-672-9-1432</a>","mla":"Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. <i>The Complexity of Deciding Legality of a Single Step of Magic: The Gathering</i>. Vol. 285, IOS Press, 2016, pp. 1432–39, doi:<a href=\"https://doi.org/10.3233/978-1-61499-672-9-1432\">10.3233/978-1-61499-672-9-1432</a>.","ieee":"K. Chatterjee and R. Ibsen-Jensen, “The complexity of deciding legality of a single step of magic: The gathering,” presented at the ECAI: European Conference on Artificial Intelligence, The Hague, Netherlands, 2016, vol. 285, pp. 1432–1439.","short":"K. Chatterjee, R. Ibsen-Jensen, in:, IOS Press, 2016, pp. 1432–1439.","ista":"Chatterjee K, Ibsen-Jensen R. 2016. The complexity of deciding legality of a single step of magic: The gathering. ECAI: European Conference on Artificial Intelligence, Frontiers in Artificial Intelligence and Applications, vol. 285, 1432–1439.","ama":"Chatterjee K, Ibsen-Jensen R. The complexity of deciding legality of a single step of magic: The gathering. In: Vol 285. IOS Press; 2016:1432-1439. doi:<a href=\"https://doi.org/10.3233/978-1-61499-672-9-1432\">10.3233/978-1-61499-672-9-1432</a>"},"day":"01","pubrep_id":"950","status":"public","alternative_title":["Frontiers in Artificial Intelligence and Applications"],"tmp":{"short":"CC BY-NC (4.0)","name":"Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)","image":"/images/cc_by_nc.png","legal_code_url":"https://creativecommons.org/licenses/by-nc/4.0/legalcode"},"title":"The complexity of deciding legality of a single step of magic: The gathering","abstract":[{"text":"Magic: the Gathering is a game about magical combat for any number of players. Formally it is a zero-sum, imperfect information stochastic game that consists of a potentially unbounded number of steps. We consider the problem of deciding if a move is legal in a given single step of Magic. We show that the problem is (a) coNP-complete in general; and (b) in P if either of two small sets of cards are not used. Our lower bound holds even for single-player Magic games. The significant aspects of our results are as follows: First, in most real-life game problems, the task of deciding whether a given move is legal in a single step is trivial, and the computationally hard task is to find the best sequence of legal moves in the presence of multiple players. In contrast, quite uniquely our hardness result holds for single step and with only one-player. Second, we establish efficient algorithms for important special cases of Magic.","lang":"eng"}],"publication_status":"published","external_id":{"isi":["000385793700166"]},"page":"1432 - 1439","article_processing_charge":"No","license":"https://creativecommons.org/licenses/by-nc/4.0/","volume":285,"author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Rasmus","last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","ddc":["004"],"conference":{"name":"ECAI: European Conference on Artificial Intelligence","start_date":"2016-08-29","end_date":"2016-09-02","location":"The Hague, Netherlands"},"has_accepted_license":"1","file":[{"date_updated":"2020-07-14T12:46:35Z","file_size":2116225,"relation":"main_file","checksum":"848043c812ace05e459579c923f3d3cf","access_level":"open_access","file_id":"4658","creator":"system","content_type":"application/pdf","file_name":"IST-2018-950-v1+1_2016_Chatterjee_The_complexity.pdf","date_created":"2018-12-12T10:07:59Z"}],"quality_controlled":"1","corr_author":"1","doi":"10.3233/978-1-61499-672-9-1432","year":"2016","date_created":"2018-12-11T11:46:41Z"},{"author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu"},{"last_name":"Doyen","first_name":"Laurent","full_name":"Doyen, Laurent"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","volume":"05-08-July-2016","page":"247 - 256","article_processing_charge":"No","abstract":[{"text":"Graph games provide the foundation for modeling and synthesizing reactive processes. In the synthesis of stochastic reactive processes, the traditional model is perfect-information stochastic games, where some transitions of the game graph are controlled by two adversarial players, and the other transitions are executed probabilistically. We consider such games where the objective is the conjunction of several quantitative objectives (specified as mean-payoff conditions), which we refer to as generalized mean-payoff objectives. The basic decision problem asks for the existence of a finite-memory strategy for a player that ensures the generalized mean-payoff objective be satisfied with a desired probability against all strategies of the opponent. A special case of the decision problem is the almost-sure problem where the desired probability is 1. Previous results presented a semi-decision procedure for -approximations of the almost-sure problem. In this work, we show that both the almost-sure problem as well as the general basic decision problem are coNP-complete, significantly improving the previous results. Moreover, we show that in the case of 1-player stochastic games, randomized memoryless strategies are sufficient and the problem can be solved in polynomial time. In contrast, in two-player stochastic games, we show that even with randomized strategies exponential memory is required in general, and present a matching exponential upper bound. We also study the basic decision problem with infinite-memory strategies and present computational complexity results for the problem. Our results are relevant in the synthesis of stochastic reactive systems with multiple quantitative requirements.","lang":"eng"}],"external_id":{"arxiv":["1604.06376"],"isi":["000387609200025"]},"publication_status":"published","title":"Perfect-information stochastic games with generalized mean-payoff objectives","year":"2016","date_created":"2018-12-11T11:46:42Z","doi":"10.1145/2933575.2934513","quality_controlled":"1","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1604.06376"}],"conference":{"start_date":"2016-07-05","name":"LICS: Logic in Computer Science","end_date":"2016-07-08","location":"New York, NY, USA"},"oa_version":"Preprint","type":"conference","publist_id":"7340","_id":"480","scopus_import":"1","isi":1,"oa":1,"month":"07","language":[{"iso":"eng"}],"date_published":"2016-07-05T00:00:00Z","arxiv":1,"department":[{"_id":"KrCh"}],"publisher":"IEEE","date_updated":"2025-09-22T14:22:08Z","ec_funded":1,"alternative_title":["Proceedings Symposium on Logic in Computer Science"],"day":"05","status":"public","citation":{"chicago":"Chatterjee, Krishnendu, and Laurent Doyen. “Perfect-Information Stochastic Games with Generalized Mean-Payoff Objectives,” 05-08-July-2016:247–56. IEEE, 2016. <a href=\"https://doi.org/10.1145/2933575.2934513\">https://doi.org/10.1145/2933575.2934513</a>.","apa":"Chatterjee, K., &#38; Doyen, L. (2016). Perfect-information stochastic games with generalized mean-payoff objectives (Vol. 05-08-July-2016, pp. 247–256). Presented at the LICS: Logic in Computer Science, New York, NY, USA: IEEE. <a href=\"https://doi.org/10.1145/2933575.2934513\">https://doi.org/10.1145/2933575.2934513</a>","mla":"Chatterjee, Krishnendu, and Laurent Doyen. <i>Perfect-Information Stochastic Games with Generalized Mean-Payoff Objectives</i>. Vol. 05-08-July-2016, IEEE, 2016, pp. 247–56, doi:<a href=\"https://doi.org/10.1145/2933575.2934513\">10.1145/2933575.2934513</a>.","ieee":"K. Chatterjee and L. Doyen, “Perfect-information stochastic games with generalized mean-payoff objectives,” presented at the LICS: Logic in Computer Science, New York, NY, USA, 2016, vol. 05-08-July-2016, pp. 247–256.","short":"K. Chatterjee, L. Doyen, in:, IEEE, 2016, pp. 247–256.","ista":"Chatterjee K, Doyen L. 2016. Perfect-information stochastic games with generalized mean-payoff objectives. LICS: Logic in Computer Science, Proceedings Symposium on Logic in Computer Science, vol. 05-08-July-2016, 247–256.","ama":"Chatterjee K, Doyen L. Perfect-information stochastic games with generalized mean-payoff objectives. In: Vol 05-08-July-2016. IEEE; 2016:247-256. doi:<a href=\"https://doi.org/10.1145/2933575.2934513\">10.1145/2933575.2934513</a>"},"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}]},{"author":[{"first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","first_name":"Andreas","last_name":"Pavlogiannis"},{"full_name":"Velner, Yaron","first_name":"Yaron","last_name":"Velner"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Published Version","type":"technical_report","related_material":{"record":[{"status":"public","id":"1604","relation":"later_version"}]},"_id":"5445","page":"33","abstract":[{"text":"We consider the quantitative analysis problem for interprocedural control-flow graphs (ICFGs). The input consists of an ICFG, a positive weight function that assigns every transition a positive integer-valued number, and a labelling of the transitions (events) as good, bad, and neutral events. The weight function assigns to each transition a numerical value that represents ameasure of how good or bad an event is. The quantitative analysis problem asks whether there is a run of the ICFG where the ratio of the sum of the numerical weights of good events versus the sum of weights of bad events in the long-run is at least a given threshold (or equivalently, to compute the maximal ratio among all valid paths in the ICFG). The quantitative analysis problem for ICFGs can be solved in polynomial time, and we present an efficient and practical algorithm for the problem. We show that several problems relevant for static program analysis, such as estimating the worst-case execution time of a program or the average energy consumption of a mobile application, can be modeled in our framework. We have implemented our algorithm as a tool in the Java Soot framework. We demonstrate the effectiveness of our approach with two case studies. First, we show that our framework provides a sound approach (no false positives) for the analysis of inefficiently-used containers. Second, we show that our approach can also be used for static profiling of programs which reasons about methods that are frequently invoked. Our experimental results show that our tool scales to relatively large benchmarks, and discovers relevant and useful information that can be used to optimize performance of the programs. ","lang":"eng"}],"oa":1,"publication_status":"published","file_date_updated":"2020-07-14T12:46:58Z","month":"03","language":[{"iso":"eng"}],"title":"Quantitative interprocedural analysis","date_published":"2016-03-31T00:00:00Z","department":[{"_id":"KrCh"}],"publisher":"IST Austria","date_updated":"2025-04-15T08:11:41Z","year":"2016","date_created":"2018-12-12T11:39:22Z","alternative_title":["IST Austria Technical Report"],"publication_identifier":{"issn":["2664-1690"]},"doi":"10.15479/AT:IST-2016-523-v1-1","status":"public","pubrep_id":"523","day":"31","citation":{"mla":"Chatterjee, Krishnendu, et al. <i>Quantitative Interprocedural Analysis</i>. IST Austria, 2016, doi:<a href=\"https://doi.org/10.15479/AT:IST-2016-523-v1-1\">10.15479/AT:IST-2016-523-v1-1</a>.","apa":"Chatterjee, K., Pavlogiannis, A., &#38; Velner, Y. (2016). <i>Quantitative interprocedural analysis</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2016-523-v1-1\">https://doi.org/10.15479/AT:IST-2016-523-v1-1</a>","chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, and Yaron Velner. <i>Quantitative Interprocedural Analysis</i>. IST Austria, 2016. <a href=\"https://doi.org/10.15479/AT:IST-2016-523-v1-1\">https://doi.org/10.15479/AT:IST-2016-523-v1-1</a>.","ista":"Chatterjee K, Pavlogiannis A, Velner Y. 2016. Quantitative interprocedural analysis, IST Austria, 33p.","ama":"Chatterjee K, Pavlogiannis A, Velner Y. <i>Quantitative Interprocedural Analysis</i>. IST Austria; 2016. doi:<a href=\"https://doi.org/10.15479/AT:IST-2016-523-v1-1\">10.15479/AT:IST-2016-523-v1-1</a>","short":"K. Chatterjee, A. Pavlogiannis, Y. Velner, Quantitative Interprocedural Analysis, IST Austria, 2016.","ieee":"K. Chatterjee, A. Pavlogiannis, and Y. Velner, <i>Quantitative interprocedural analysis</i>. IST Austria, 2016."},"file":[{"creator":"system","date_created":"2018-12-12T11:53:52Z","file_name":"IST-2016-523-v1+1_main.pdf","content_type":"application/pdf","access_level":"open_access","checksum":"cef516fa091925b5868813e355268fb4","relation":"main_file","date_updated":"2020-07-14T12:46:58Z","file_size":1012204,"file_id":"5513"}],"has_accepted_license":"1","ddc":["005"]},{"doi":"10.15479/AT:IST-2016-648-v1-1","publication_identifier":{"issn":["2664-1690"]},"alternative_title":["IST Austria Technical Report"],"status":"public","day":"09","pubrep_id":"648","date_created":"2018-12-12T11:39:24Z","year":"2016","has_accepted_license":"1","ddc":["519"],"citation":{"ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, <i>Amplification on undirected population structures: Comets beat stars</i>. IST Austria, 2016.","short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Amplification on Undirected Population Structures: Comets Beat Stars, IST Austria, 2016.","ama":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. <i>Amplification on Undirected Population Structures: Comets Beat Stars</i>. IST Austria; 2016. doi:<a href=\"https://doi.org/10.15479/AT:IST-2016-648-v1-1\">10.15479/AT:IST-2016-648-v1-1</a>","ista":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Amplification on undirected population structures: Comets beat stars, IST Austria, 22p.","apa":"Pavlogiannis, A., Tkadlec, J., Chatterjee, K., &#38; Nowak, M. (2016). <i>Amplification on undirected population structures: Comets beat stars</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2016-648-v1-1\">https://doi.org/10.15479/AT:IST-2016-648-v1-1</a>","chicago":"Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak. <i>Amplification on Undirected Population Structures: Comets Beat Stars</i>. IST Austria, 2016. <a href=\"https://doi.org/10.15479/AT:IST-2016-648-v1-1\">https://doi.org/10.15479/AT:IST-2016-648-v1-1</a>.","mla":"Pavlogiannis, Andreas, et al. <i>Amplification on Undirected Population Structures: Comets Beat Stars</i>. IST Austria, 2016, doi:<a href=\"https://doi.org/10.15479/AT:IST-2016-648-v1-1\">10.15479/AT:IST-2016-648-v1-1</a>."},"file":[{"date_created":"2018-12-12T11:54:07Z","file_name":"IST-2016-648-v1+1_tr.pdf","content_type":"application/pdf","creator":"system","file_id":"5529","access_level":"open_access","relation":"main_file","checksum":"8345a8c1e7d7f0cd92516d182b7fc59e","file_size":1264221,"date_updated":"2020-07-14T12:46:58Z"}],"related_material":{"record":[{"status":"public","id":"512","relation":"later_version"}]},"_id":"5449","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","first_name":"Andreas"},{"full_name":"Tkadlec, Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-1097-9684","first_name":"Josef","last_name":"Tkadlec"},{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Nowak, Martin","last_name":"Nowak","first_name":"Martin"}],"oa_version":"Updated Version","type":"technical_report","date_published":"2016-11-09T00:00:00Z","title":"Amplification on undirected population structures: Comets beat stars","language":[{"iso":"eng"}],"month":"11","date_updated":"2025-09-18T09:50:09Z","publisher":"IST Austria","department":[{"_id":"KrCh"}],"page":"22","publication_status":"published","file_date_updated":"2020-07-14T12:46:58Z","abstract":[{"lang":"eng","text":"The fixation probability is the probability that a new mutant introduced in a homogeneous population eventually takes over the entire population.\r\nThe fixation probability is a fundamental quantity of natural selection, and known to depend on the population structure.\r\nAmplifiers of natural selection are population structures which increase the fixation probability of advantageous mutants, as compared to the baseline case of well-mixed populations. In this work we focus on symmetric population structures represented as undirected graphs. In the regime of undirected graphs, the strongest amplifier known has been the Star graph, and the existence of undirected graphs with stronger amplification properties has remained open for over a decade.\r\nIn this work we present the Comet and Comet-swarm families of undirected graphs. We show that for a range of fitness values of the mutants, the Comet and Comet-swarm graphs have fixation probability strictly larger than the fixation probability of the Star graph, for fixed population size and at the limit of large populations, respectively."}],"oa":1},{"type":"technical_report","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"first_name":"Andreas","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-1097-9684","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","full_name":"Tkadlec, Josef","first_name":"Josef","last_name":"Tkadlec"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu"},{"full_name":"Nowak, Martin","last_name":"Nowak","first_name":"Martin"}],"oa_version":"Published Version","_id":"5451","oa":1,"file_date_updated":"2020-07-14T12:46:59Z","publication_status":"published","page":"34","publisher":"IST Austria","department":[{"_id":"KrCh"}],"date_updated":"2023-02-23T12:27:05Z","title":"Strong amplifiers of natural selection","month":"12","language":[{"iso":"eng"}],"date_published":"2016-12-30T00:00:00Z","year":"2016","date_created":"2018-12-12T11:39:24Z","pubrep_id":"728","status":"public","day":"30","alternative_title":["IST Austria Technical Report"],"doi":"10.15479/AT:IST-2016-728-v1-1","publication_identifier":{"issn":["2664-1690"]},"file":[{"creator":"system","date_created":"2018-12-12T11:53:04Z","content_type":"application/pdf","file_name":"IST-2016-728-v1+1_main.pdf","access_level":"open_access","relation":"main_file","checksum":"7b8bb17c322c0556acba6ac169fa71c1","date_updated":"2020-07-14T12:46:59Z","file_size":1014732,"file_id":"5465"}],"citation":{"chicago":"Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak. <i>Strong Amplifiers of Natural Selection</i>. IST Austria, 2016. <a href=\"https://doi.org/10.15479/AT:IST-2016-728-v1-1\">https://doi.org/10.15479/AT:IST-2016-728-v1-1</a>.","apa":"Pavlogiannis, A., Tkadlec, J., Chatterjee, K., &#38; Nowak, M. (2016). <i>Strong amplifiers of natural selection</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2016-728-v1-1\">https://doi.org/10.15479/AT:IST-2016-728-v1-1</a>","mla":"Pavlogiannis, Andreas, et al. <i>Strong Amplifiers of Natural Selection</i>. IST Austria, 2016, doi:<a href=\"https://doi.org/10.15479/AT:IST-2016-728-v1-1\">10.15479/AT:IST-2016-728-v1-1</a>.","short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Strong Amplifiers of Natural Selection, IST Austria, 2016.","ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, <i>Strong amplifiers of natural selection</i>. IST Austria, 2016.","ista":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Strong amplifiers of natural selection, IST Austria, 34p.","ama":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. <i>Strong Amplifiers of Natural Selection</i>. IST Austria; 2016. doi:<a href=\"https://doi.org/10.15479/AT:IST-2016-728-v1-1\">10.15479/AT:IST-2016-728-v1-1</a>"},"ddc":["000"],"has_accepted_license":"1"},{"alternative_title":["IST Austria Technical Report"],"day":"30","status":"public","pubrep_id":"750","ec_funded":1,"citation":{"ista":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Arbitrarily strong amplifiers of natural selection, IST Austria, 32p.","ama":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. <i>Arbitrarily Strong Amplifiers of Natural Selection</i>. IST Austria; 2016. doi:<a href=\"https://doi.org/10.15479/AT:IST-2017-728-v2-1\">10.15479/AT:IST-2017-728-v2-1</a>","ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, <i>Arbitrarily strong amplifiers of natural selection</i>. IST Austria, 2016.","short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Arbitrarily Strong Amplifiers of Natural Selection, IST Austria, 2016.","mla":"Pavlogiannis, Andreas, et al. <i>Arbitrarily Strong Amplifiers of Natural Selection</i>. IST Austria, 2016, doi:<a href=\"https://doi.org/10.15479/AT:IST-2017-728-v2-1\">10.15479/AT:IST-2017-728-v2-1</a>.","chicago":"Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak. <i>Arbitrarily Strong Amplifiers of Natural Selection</i>. IST Austria, 2016. <a href=\"https://doi.org/10.15479/AT:IST-2017-728-v2-1\">https://doi.org/10.15479/AT:IST-2017-728-v2-1</a>.","apa":"Pavlogiannis, A., Tkadlec, J., Chatterjee, K., &#38; Nowak, M. (2016). <i>Arbitrarily strong amplifiers of natural selection</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2017-728-v2-1\">https://doi.org/10.15479/AT:IST-2017-728-v2-1</a>"},"project":[{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"}],"_id":"5452","oa_version":"Published Version","type":"technical_report","language":[{"iso":"eng"}],"month":"12","date_published":"2016-12-30T00:00:00Z","department":[{"_id":"KrCh"}],"publisher":"IST Austria","date_updated":"2025-04-15T07:55:39Z","oa":1,"file_date_updated":"2020-07-14T12:46:59Z","publication_identifier":{"issn":["2664-1690"]},"doi":"10.15479/AT:IST-2017-728-v2-1","year":"2016","date_created":"2018-12-12T11:39:25Z","has_accepted_license":"1","ddc":["000"],"file":[{"file_name":"IST-2017-728-v2+1_main.pdf","content_type":"application/pdf","date_created":"2018-12-12T11:52:59Z","creator":"system","file_id":"5460","file_size":811558,"date_updated":"2020-07-14T12:46:59Z","checksum":"58e895f26c82f560c0f0989bf8b08599","relation":"main_file","access_level":"open_access"}],"related_material":{"record":[{"status":"public","id":"5453","relation":"later_version"},{"relation":"popular_science","id":"5559","status":"public"}]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis","first_name":"Andreas"},{"id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-1097-9684","full_name":"Tkadlec, Josef","first_name":"Josef","last_name":"Tkadlec"},{"first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Nowak, Martin","first_name":"Martin","last_name":"Nowak"}],"title":"Arbitrarily strong amplifiers of natural selection","page":"32","article_processing_charge":"No","publication_status":"published"},{"ddc":["000"],"has_accepted_license":"1","file":[{"checksum":"83b0313dab3bff4bdb6ac38695026fda","relation":"main_file","access_level":"open_access","date_updated":"2020-07-14T12:46:59Z","file_size":1015647,"file_id":"5474","creator":"system","date_created":"2018-12-12T11:53:13Z","file_name":"IST-2017-749-v3+1_main.pdf","content_type":"application/pdf"}],"citation":{"mla":"Pavlogiannis, Andreas, et al. <i>Arbitrarily Strong Amplifiers of Natural Selection</i>. IST Austria, 2016, doi:<a href=\"https://doi.org/10.15479/AT:IST-2017-749-v3-1\">10.15479/AT:IST-2017-749-v3-1</a>.","apa":"Pavlogiannis, A., Tkadlec, J., Chatterjee, K., &#38; Nowak, M. (2016). <i>Arbitrarily strong amplifiers of natural selection</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2017-749-v3-1\">https://doi.org/10.15479/AT:IST-2017-749-v3-1</a>","chicago":"Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak. <i>Arbitrarily Strong Amplifiers of Natural Selection</i>. IST Austria, 2016. <a href=\"https://doi.org/10.15479/AT:IST-2017-749-v3-1\">https://doi.org/10.15479/AT:IST-2017-749-v3-1</a>.","ista":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Arbitrarily strong amplifiers of natural selection, IST Austria, 34p.","ama":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. <i>Arbitrarily Strong Amplifiers of Natural Selection</i>. IST Austria; 2016. doi:<a href=\"https://doi.org/10.15479/AT:IST-2017-749-v3-1\">10.15479/AT:IST-2017-749-v3-1</a>","ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, <i>Arbitrarily strong amplifiers of natural selection</i>. IST Austria, 2016.","short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Arbitrarily Strong Amplifiers of Natural Selection, IST Austria, 2016."},"pubrep_id":"755","day":"30","status":"public","alternative_title":["IST Austria Technical Report"],"publication_identifier":{"issn":["2664-1690"]},"doi":"10.15479/AT:IST-2017-749-v3-1","year":"2016","date_created":"2018-12-12T11:39:25Z","publisher":"IST Austria","department":[{"_id":"KrCh"}],"date_updated":"2025-04-15T07:55:37Z","language":[{"iso":"eng"}],"title":"Arbitrarily strong amplifiers of natural selection","month":"12","date_published":"2016-12-30T00:00:00Z","oa":1,"publication_status":"published","file_date_updated":"2020-07-14T12:46:59Z","page":"34","related_material":{"record":[{"status":"public","id":"5452","relation":"earlier_version"}]},"_id":"5453","type":"technical_report","oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"last_name":"Pavlogiannis","first_name":"Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas"},{"last_name":"Tkadlec","first_name":"Josef","full_name":"Tkadlec, Josef","orcid":"0000-0002-1097-9684","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Nowak","first_name":"Martin","full_name":"Nowak, Martin"}]},{"intvolume":"        58","oa_version":"Published Version","acknowledgement":"K. C., M. H., and W. D. are partially supported by the Vienna Science and Technology Fund (WWTF) through project ICT15-003. K. C. is partially supported by the Austrian Science Fund (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE) and an ERC Start grant (279307","type":"conference","publist_id":"6317","_id":"1068","scopus_import":"1","oa":1,"file_date_updated":"2018-12-12T10:16:02Z","month":"08","language":[{"iso":"eng"}],"date_published":"2016-08-01T00:00:00Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","department":[{"_id":"KrCh"}],"date_updated":"2025-07-10T11:49:55Z","ec_funded":1,"tmp":{"short":"CC BY (3.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/3.0/legalcode","name":"Creative Commons Attribution 3.0 Unported (CC BY 3.0)"},"alternative_title":["LIPIcs"],"pubrep_id":"779","day":"01","status":"public","citation":{"mla":"Chatterjee, Krishnendu, et al. <i>Conditionally Optimal Algorithms for Generalized Büchi Games</i>. Vol. 58, 25, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.25\">10.4230/LIPIcs.MFCS.2016.25</a>.","chicago":"Chatterjee, Krishnendu, Wolfgang Dvorák, Monika Henzinger, and Veronika Loitzenbauer. “Conditionally Optimal Algorithms for Generalized Büchi Games,” Vol. 58. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.25\">https://doi.org/10.4230/LIPIcs.MFCS.2016.25</a>.","apa":"Chatterjee, K., Dvorák, W., Henzinger, M., &#38; Loitzenbauer, V. (2016). Conditionally optimal algorithms for generalized Büchi Games (Vol. 58). Presented at the MFCS: Mathematical Foundations of Computer Science, Krakow, Poland: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.25\">https://doi.org/10.4230/LIPIcs.MFCS.2016.25</a>","ista":"Chatterjee K, Dvorák W, Henzinger M, Loitzenbauer V. 2016. Conditionally optimal algorithms for generalized Büchi Games. MFCS: Mathematical Foundations of Computer Science, LIPIcs, vol. 58, 25.","ama":"Chatterjee K, Dvorák W, Henzinger M, Loitzenbauer V. Conditionally optimal algorithms for generalized Büchi Games. In: Vol 58. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2016.25\">10.4230/LIPIcs.MFCS.2016.25</a>","ieee":"K. Chatterjee, W. Dvorák, M. Henzinger, and V. Loitzenbauer, “Conditionally optimal algorithms for generalized Büchi Games,” presented at the MFCS: Mathematical Foundations of Computer Science, Krakow, Poland, 2016, vol. 58.","short":"K. Chatterjee, W. Dvorák, M. Henzinger, V. Loitzenbauer, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016."},"project":[{"name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"full_name":"Dvorák, Wolfgang","last_name":"Dvorák","first_name":"Wolfgang"},{"first_name":"Monika H","last_name":"Henzinger","orcid":"0000-0002-5008-6530","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","full_name":"Henzinger, Monika H"},{"full_name":"Loitzenbauer, Veronika","first_name":"Veronika","last_name":"Loitzenbauer"}],"volume":58,"article_processing_charge":"No","license":"https://creativecommons.org/licenses/by/3.0/","abstract":[{"text":"Games on graphs provide the appropriate framework to study several central problems in computer science, such as verification and synthesis of reactive systems. One of the most basic objectives for games on graphs is the liveness (or Büchi) objective that given a target set of vertices requires that some vertex in the target set is visited infinitely often. We study generalized Büchi objectives (i.e., conjunction of liveness objectives), and implications between two generalized Büchi objectives (known as GR(1) objectives), that arise in numerous applications in computer-aided verification. We present improved algorithms and conditional super-linear lower bounds based on widely believed assumptions about the complexity of (A1) combinatorial Boolean matrix multiplication and (A2) CNF-SAT. We consider graph games with n vertices, m edges, and generalized Büchi objectives with k conjunctions. First, we present an algorithm with running time O(k*n^2), improving the previously known O(k*n*m) and O(k^2*n^2) worst-case bounds. Our algorithm is optimal for dense graphs under (A1). Second, we show that the basic algorithm for the problem is optimal for sparse graphs when the target sets have constant size under (A2). Finally, we consider GR(1) objectives, with k_1 conjunctions in the antecedent and k_2 conjunctions in the consequent, and present an O(k_1 k_2 n^{2.5})-time algorithm, improving the previously known O(k_1*k_2*n*m)-time algorithm for m &gt; n^{1.5}. ","lang":"eng"}],"publication_status":"published","title":"Conditionally optimal algorithms for generalized Büchi Games","year":"2016","date_created":"2018-12-11T11:49:58Z","article_number":"25","doi":"10.4230/LIPIcs.MFCS.2016.25","quality_controlled":"1","file":[{"file_name":"IST-2017-779-v1+1_LIPIcs-MFCS-2016-25.pdf","content_type":"application/pdf","date_created":"2018-12-12T10:16:02Z","creator":"system","file_id":"5187","file_size":632786,"date_updated":"2018-12-12T10:16:02Z","relation":"main_file","access_level":"open_access"}],"has_accepted_license":"1","ddc":["000","004","006"],"conference":{"end_date":"2016-08-26","location":"Krakow, Poland","start_date":"2016-08-22","name":"MFCS: Mathematical Foundations of Computer Science"}},{"citation":{"chicago":"Chonev, Ventsislav K, Joël Ouaknine, and James Worrell. “On the Skolem Problem for Continuous Linear Dynamical Systems,” Vol. 55. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. <a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2016.100\">https://doi.org/10.4230/LIPIcs.ICALP.2016.100</a>.","apa":"Chonev, V. K., Ouaknine, J., &#38; Worrell, J. (2016). On the skolem problem for continuous linear dynamical systems (Vol. 55). Presented at the ICALP: Automata, Languages and Programming, Rome, Italy: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2016.100\">https://doi.org/10.4230/LIPIcs.ICALP.2016.100</a>","mla":"Chonev, Ventsislav K., et al. <i>On the Skolem Problem for Continuous Linear Dynamical Systems</i>. Vol. 55, 100, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:<a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2016.100\">10.4230/LIPIcs.ICALP.2016.100</a>.","short":"V.K. Chonev, J. Ouaknine, J. Worrell, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","ieee":"V. K. Chonev, J. Ouaknine, and J. Worrell, “On the skolem problem for continuous linear dynamical systems,” presented at the ICALP: Automata, Languages and Programming, Rome, Italy, 2016, vol. 55.","ista":"Chonev VK, Ouaknine J, Worrell J. 2016. On the skolem problem for continuous linear dynamical systems. ICALP: Automata, Languages and Programming, LIPIcs, vol. 55, 100.","ama":"Chonev VK, Ouaknine J, Worrell J. On the skolem problem for continuous linear dynamical systems. In: Vol 55. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:<a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2016.100\">10.4230/LIPIcs.ICALP.2016.100</a>"},"project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7"}],"ec_funded":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"alternative_title":["LIPIcs"],"status":"public","day":"01","pubrep_id":"778","oa":1,"file_date_updated":"2018-12-12T10:16:26Z","month":"08","language":[{"iso":"eng"}],"date_published":"2016-08-01T00:00:00Z","department":[{"_id":"KrCh"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_updated":"2025-06-03T11:32:08Z","intvolume":"        55","oa_version":"Published Version","acknowledgement":"Ventsislav Chonev is supported by Austrian Science Fund (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant (279307:  Graph Games), and ERC Advanced Grant (267989: QUAREM).","type":"conference","publist_id":"6314","_id":"1069","scopus_import":"1","file":[{"file_id":"5213","access_level":"open_access","relation":"main_file","date_updated":"2018-12-12T10:16:26Z","file_size":521415,"date_created":"2018-12-12T10:16:26Z","content_type":"application/pdf","file_name":"IST-2017-778-v1+1_LIPIcs-ICALP-2016-100.pdf","creator":"system"}],"quality_controlled":"1","has_accepted_license":"1","conference":{"start_date":"2016-07-12","name":"ICALP: Automata, Languages and Programming","location":"Rome, Italy","end_date":"2016-07-15"},"ddc":["004","006"],"year":"2016","date_created":"2018-12-11T11:49:59Z","article_number":"100","doi":"10.4230/LIPIcs.ICALP.2016.100","article_processing_charge":"No","abstract":[{"text":"The Continuous Skolem Problem asks whether a real-valued function satisfying a linear differen-\r\ntial equation has a zero in a given interval of real numbers. This is a fundamental reachability\r\nproblem for continuous linear dynamical systems, such as linear hybrid automata and continuous-\r\ntime Markov chains. Decidability of the problem is currently open – indeed decidability is open\r\neven for the sub-problem in which a zero is sought in a bounded interval. In this paper we show\r\ndecidability of the bounded problem subject to Schanuel’s Conjecture, a unifying conjecture in\r\ntranscendental number theory. We furthermore analyse the unbounded problem in terms of the\r\nfrequencies of the differential equation, that is, the imaginary parts of the characteristic roots.\r\nWe show that the unbounded problem can be reduced to the bounded problem if there is at most\r\none rationally linearly independent frequency, or if there are two rationally linearly independent\r\nfrequencies and all characteristic roots are simple. We complete the picture by showing that de-\r\ncidability of the unbounded problem in the case of two (or more) rationally linearly independent\r\nfrequencies would entail a major new effectiveness result in Diophantine approximation, namely\r\ncomputability of the Diophantine-approximation types of all real algebraic numbers.","lang":"eng"}],"publication_status":"published","title":"On the skolem problem for continuous linear dynamical systems","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"first_name":"Ventsislav K","last_name":"Chonev","id":"36CBE2E6-F248-11E8-B48F-1D18A9856A87","full_name":"Chonev, Ventsislav K"},{"full_name":"Ouaknine, Joël","first_name":"Joël","last_name":"Ouaknine"},{"full_name":"Worrell, James","last_name":"Worrell","first_name":"James"}],"volume":55},{"alternative_title":["LIPIcs"],"day":"01","pubrep_id":"812","status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"ec_funded":1,"citation":{"mla":"Chatterjee, Krishnendu, and Laurent Doyen. <i>Computation Tree Logic for Synchronization Properties</i>. Vol. 55, 98, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:<a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2016.98\">10.4230/LIPIcs.ICALP.2016.98</a>.","chicago":"Chatterjee, Krishnendu, and Laurent Doyen. “Computation Tree Logic for Synchronization Properties,” Vol. 55. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. <a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2016.98\">https://doi.org/10.4230/LIPIcs.ICALP.2016.98</a>.","apa":"Chatterjee, K., &#38; Doyen, L. (2016). Computation tree logic for synchronization properties (Vol. 55). Presented at the ICALP: Automata, Languages and Programming, Rome, Italy: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2016.98\">https://doi.org/10.4230/LIPIcs.ICALP.2016.98</a>","ista":"Chatterjee K, Doyen L. 2016. Computation tree logic for synchronization properties. ICALP: Automata, Languages and Programming, LIPIcs, vol. 55, 98.","ama":"Chatterjee K, Doyen L. Computation tree logic for synchronization properties. In: Vol 55. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:<a href=\"https://doi.org/10.4230/LIPIcs.ICALP.2016.98\">10.4230/LIPIcs.ICALP.2016.98</a>","ieee":"K. Chatterjee and L. Doyen, “Computation tree logic for synchronization properties,” presented at the ICALP: Automata, Languages and Programming, Rome, Italy, 2016, vol. 55.","short":"K. Chatterjee, L. Doyen, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016."},"project":[{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"}],"publist_id":"6313","scopus_import":"1","_id":"1070","oa_version":"Published Version","intvolume":"        55","acknowledgement":"This research was partially supported by Austrian Science Fund (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant (279307: Graph Games), Vienna Science and Technology Fund (WWTF) through project ICT15-003, and European project Cassting (FP7-601148).\r\n\r\nWe thank Stefan Göller and anonymous reviewers for their insightful\r\ncomments and suggestions.\r\n","type":"conference","date_published":"2016-01-01T00:00:00Z","language":[{"iso":"eng"}],"month":"01","date_updated":"2025-06-03T11:18:54Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","department":[{"_id":"KrCh"}],"file_date_updated":"2018-12-12T10:08:52Z","oa":1,"doi":"10.4230/LIPIcs.ICALP.2016.98","date_created":"2018-12-11T11:49:59Z","year":"2016","article_number":"98","has_accepted_license":"1","conference":{"location":"Rome, Italy","end_date":"2016-07-15","name":"ICALP: Automata, Languages and Programming","start_date":"2016-07-12"},"ddc":["005"],"file":[{"date_created":"2018-12-12T10:08:52Z","content_type":"application/pdf","file_name":"IST-2017-812-v1+1_LIPIcs-ICALP-2016-98.pdf","creator":"system","file_id":"4714","access_level":"open_access","relation":"main_file","date_updated":"2018-12-12T10:08:52Z","file_size":546133}],"quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Doyen, Laurent","last_name":"Doyen","first_name":"Laurent"}],"volume":55,"title":"Computation tree logic for synchronization properties","article_processing_charge":"No","publication_status":"published","abstract":[{"lang":"eng","text":"We present a logic that extends CTL (Computation Tree Logic) with operators that express synchronization properties. A property is synchronized in a system if it holds in all paths of a certain length. The new logic is obtained by using the same path quantifiers and temporal operators as in CTL, but allowing a different order of the quantifiers. This small syntactic variation induces a logic that can express non-regular properties for which known extensions of MSO with equality of path length are undecidable. We show that our variant of CTL is decidable and that the model-checking problem is in Delta_3^P = P^{NP^NP}, and is DP-hard. We analogously consider quantifier exchange in extensions of CTL, and we present operators defined using basic operators of CTL* that express the occurrence of infinitely many synchronization points. We show that the model-checking problem remains in Delta_3^P. The distinguishing power of CTL and of our new logic coincide if the Next operator is allowed in the logics, thus the classical bisimulation quotient can be used for state-space reduction before model checking. "}]},{"citation":{"mla":"Chatterjee, Krishnendu, et al. <i>Optimal Reachability and a Space Time Tradeoff for Distance Queries in Constant Treewidth Graphs</i>. Vol. 57, 28, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:<a href=\"https://doi.org/10.4230/LIPIcs.ESA.2016.28\">10.4230/LIPIcs.ESA.2016.28</a>.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Optimal Reachability and a Space Time Tradeoff for Distance Queries in Constant Treewidth Graphs,” Vol. 57. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. <a href=\"https://doi.org/10.4230/LIPIcs.ESA.2016.28\">https://doi.org/10.4230/LIPIcs.ESA.2016.28</a>.","apa":"Chatterjee, K., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2016). Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs (Vol. 57). Presented at the ESA: European Symposium on Algorithms, Aarhus, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.ESA.2016.28\">https://doi.org/10.4230/LIPIcs.ESA.2016.28</a>","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs. In: Vol 57. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:<a href=\"https://doi.org/10.4230/LIPIcs.ESA.2016.28\">10.4230/LIPIcs.ESA.2016.28</a>","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2016. Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs. ESA: European Symposium on Algorithms, LIPIcs, vol. 57, 28.","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs,” presented at the ESA: European Symposium on Algorithms, Aarhus, Denmark, 2016, vol. 57."},"project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"}],"alternative_title":["LIPIcs"],"day":"01","pubrep_id":"777","status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"ec_funded":1,"date_published":"2016-08-01T00:00:00Z","language":[{"iso":"eng"}],"month":"08","date_updated":"2026-04-08T14:22:16Z","department":[{"_id":"KrCh"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","file_date_updated":"2018-12-12T10:14:31Z","oa":1,"publist_id":"6312","scopus_import":"1","_id":"1071","intvolume":"        57","oa_version":"Published Version","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).","type":"conference","has_accepted_license":"1","conference":{"end_date":"2016-08-24","location":"Aarhus, Denmark","name":"ESA: European Symposium on Algorithms","start_date":"2016-08-22"},"ddc":["004","006"],"file":[{"file_id":"5084","file_size":579225,"date_updated":"2018-12-12T10:14:31Z","access_level":"open_access","relation":"main_file","content_type":"application/pdf","file_name":"IST-2017-777-v1+1_LIPIcs-ESA-2016-28.pdf","date_created":"2018-12-12T10:14:31Z","creator":"system"}],"quality_controlled":"1","doi":"10.4230/LIPIcs.ESA.2016.28","date_created":"2018-12-11T11:49:59Z","year":"2016","article_number":"28","title":"Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs","article_processing_charge":"No","publication_status":"published","abstract":[{"lang":"eng","text":"We consider data-structures for answering reachability and distance queries on constant-treewidth graphs with n nodes, on the standard RAM computational model with wordsize W=Theta(log n). Our first contribution is a data-structure that after O(n) preprocessing time, allows (1) pair reachability queries in O(1) time; and (2) single-source reachability queries in O(n/log n) time. This is (asymptotically) optimal and is faster than DFS/BFS when answering more than a constant number of single-source queries. The data-structure uses at all times O(n) space. Our second contribution is a space-time tradeoff data-structure for distance queries. For any epsilon in [1/2,1], we provide a data-structure with polynomial preprocessing time that allows pair queries in O(n^{1-\\epsilon} alpha(n)) time, where alpha is the inverse of the Ackermann function, and at all times uses O(n^epsilon) space. The input graph G is not considered in the space complexity. "}],"related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"821"}]},"author":[{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen","first_name":"Rasmus"},{"last_name":"Pavlogiannis","first_name":"Andreas","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","volume":57},{"doi":"10.1371/journal.pone.0163867.s008","day":"04","status":"public","year":"2016","date_created":"2021-08-10T08:42:00Z","citation":{"ama":"Hilbe C, Hagel K, Milinski M. Experimental game instructions. 2016. doi:<a href=\"https://doi.org/10.1371/journal.pone.0163867.s008\">10.1371/journal.pone.0163867.s008</a>","ista":"Hilbe C, Hagel K, Milinski M. 2016. Experimental game instructions, Public Library of Science, <a href=\"https://doi.org/10.1371/journal.pone.0163867.s008\">10.1371/journal.pone.0163867.s008</a>.","ieee":"C. Hilbe, K. Hagel, and M. Milinski, “Experimental game instructions.” Public Library of Science, 2016.","short":"C. Hilbe, K. Hagel, M. Milinski, (2016).","mla":"Hilbe, Christian, et al. <i>Experimental Game Instructions</i>. Public Library of Science, 2016, doi:<a href=\"https://doi.org/10.1371/journal.pone.0163867.s008\">10.1371/journal.pone.0163867.s008</a>.","apa":"Hilbe, C., Hagel, K., &#38; Milinski, M. (2016). Experimental game instructions. Public Library of Science. <a href=\"https://doi.org/10.1371/journal.pone.0163867.s008\">https://doi.org/10.1371/journal.pone.0163867.s008</a>","chicago":"Hilbe, Christian, Kristin Hagel, and Manfred Milinski. “Experimental Game Instructions.” Public Library of Science, 2016. <a href=\"https://doi.org/10.1371/journal.pone.0163867.s008\">https://doi.org/10.1371/journal.pone.0163867.s008</a>."},"related_material":{"record":[{"status":"public","id":"1322","relation":"used_in_publication"}]},"_id":"9867","oa_version":"Published Version","author":[{"last_name":"Hilbe","first_name":"Christian","full_name":"Hilbe, Christian","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5116-955X"},{"full_name":"Hagel, Kristin","last_name":"Hagel","first_name":"Kristin"},{"full_name":"Milinski, Manfred","first_name":"Manfred","last_name":"Milinski"}],"user_id":"6785fbc1-c503-11eb-8a32-93094b40e1cf","type":"research_data_reference","title":"Experimental game instructions","month":"10","department":[{"_id":"KrCh"}],"publisher":"Public Library of Science","date_updated":"2025-09-22T08:27:00Z","article_processing_charge":"No","abstract":[{"text":"In the beginning of our experiment, subjects were asked to read a few pages on their computer screens that would explain the rules of the subsequent game. Here, we provide these instructions, translated from German.","lang":"eng"}]},{"user_id":"6785fbc1-c503-11eb-8a32-93094b40e1cf","oa_version":"Published Version","author":[{"last_name":"Hilbe","first_name":"Christian","orcid":"0000-0001-5116-955X","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","full_name":"Hilbe, Christian"},{"full_name":"Hagel, Kristin","last_name":"Hagel","first_name":"Kristin"},{"first_name":"Manfred","last_name":"Milinski","full_name":"Milinski, Manfred"}],"type":"research_data_reference","related_material":{"record":[{"status":"public","id":"1322","relation":"used_in_publication"}]},"_id":"9868","article_processing_charge":"No","abstract":[{"text":"The raw data file containing the experimental decisions of all our study subjects.","lang":"eng"}],"month":"10","title":"Experimental data","date_published":"2016-10-04T00:00:00Z","publisher":"Public Library of Science","department":[{"_id":"KrCh"}],"date_updated":"2025-09-22T08:27:00Z","year":"2016","date_created":"2021-08-10T08:45:00Z","doi":"10.1371/journal.pone.0163867.s009","day":"04","status":"public","citation":{"chicago":"Hilbe, Christian, Kristin Hagel, and Manfred Milinski. “Experimental Data.” Public Library of Science, 2016. <a href=\"https://doi.org/10.1371/journal.pone.0163867.s009\">https://doi.org/10.1371/journal.pone.0163867.s009</a>.","apa":"Hilbe, C., Hagel, K., &#38; Milinski, M. (2016). Experimental data. Public Library of Science. <a href=\"https://doi.org/10.1371/journal.pone.0163867.s009\">https://doi.org/10.1371/journal.pone.0163867.s009</a>","mla":"Hilbe, Christian, et al. <i>Experimental Data</i>. Public Library of Science, 2016, doi:<a href=\"https://doi.org/10.1371/journal.pone.0163867.s009\">10.1371/journal.pone.0163867.s009</a>.","ieee":"C. Hilbe, K. Hagel, and M. Milinski, “Experimental data.” Public Library of Science, 2016.","short":"C. Hilbe, K. Hagel, M. Milinski, (2016).","ista":"Hilbe C, Hagel K, Milinski M. 2016. Experimental data, Public Library of Science, <a href=\"https://doi.org/10.1371/journal.pone.0163867.s009\">10.1371/journal.pone.0163867.s009</a>.","ama":"Hilbe C, Hagel K, Milinski M. Experimental data. 2016. doi:<a href=\"https://doi.org/10.1371/journal.pone.0163867.s009\">10.1371/journal.pone.0163867.s009</a>"}}]