[{"article_processing_charge":"No","page":"878 - 911","external_id":{"isi":["000374425900015"],"arxiv":["1309.2802"]},"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","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"last_name":"Chmelik","first_name":"Martin","full_name":"Chmelik, Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Tracol, Mathieu","id":"3F54FA38-F248-11E8-B48F-1D18A9856A87","last_name":"Tracol","first_name":"Mathieu"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","volume":82,"related_material":{"record":[{"relation":"earlier_version","id":"2295","status":"public"},{"status":"public","id":"5400","relation":"earlier_version"}]},"corr_author":"1","quality_controlled":"1","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1309.2802"}],"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","month":"08","language":[{"iso":"eng"}],"date_updated":"2025-09-18T11:38:39Z","publisher":"Elsevier","department":[{"_id":"KrCh"}],"arxiv":1,"intvolume":"        82","oa_version":"Preprint","type":"journal_article","publist_id":"5718","scopus_import":"1","_id":"1477","citation":{"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.","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.","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>","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>","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>.","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>."},"project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","call_identifier":"FWF"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"ec_funded":1,"day":"01","status":"public"},{"day":"01","status":"public","pubrep_id":"561","ec_funded":1,"citation":{"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>.","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>","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>.","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.","short":"K. Lohse, M. Chmelik, S. Martin, N.H. Barton, Genetics 202 (2016) 775–786.","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>"},"project":[{"call_identifier":"FP7","name":"Limits to selection in biology and in evolutionary computation","_id":"25B07788-B435-11E9-9278-68D0E5697425","grant_number":"250152"}],"publist_id":"5658","scopus_import":"1","_id":"1518","oa_version":"Preprint","intvolume":"       202","article_type":"original","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","date_published":"2016-02-01T00:00:00Z","language":[{"iso":"eng"}],"month":"02","date_updated":"2025-09-18T11:09:34Z","publisher":"Genetics Society of America","department":[{"_id":"KrCh"},{"_id":"NiBa"}],"isi":1,"file_date_updated":"2020-07-14T12:45:00Z","oa":1,"doi":"10.1534/genetics.115.183814","issue":"2","publication":"Genetics","date_created":"2018-12-11T11:52:29Z","year":"2016","has_accepted_license":"1","ddc":["570"],"file":[{"creator":"system","date_created":"2018-12-12T10:16:51Z","file_name":"IST-2016-561-v1+1_Lohse_et_al_Genetics_2015.pdf","content_type":"application/pdf","relation":"main_file","checksum":"41c9b5d72e7fe4624dd22dfe622337d5","access_level":"open_access","date_updated":"2020-07-14T12:45:00Z","file_size":957466,"file_id":"5241"}],"quality_controlled":"1","pmid":1,"author":[{"first_name":"Konrad","last_name":"Lohse","full_name":"Lohse, Konrad"},{"full_name":"Chmelik, Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik","first_name":"Martin"},{"first_name":"Simon","last_name":"Martin","full_name":"Martin, Simon"},{"last_name":"Barton","first_name":"Nicholas H","id":"4880FE40-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8548-5240","full_name":"Barton, Nicholas H"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","volume":202,"title":"Efficient strategies for calculating blockwise likelihoods under the coalescent","article_processing_charge":"No","page":"775 - 786","publication_status":"published","external_id":{"pmid":["26715666"],"isi":["000371304600032"]},"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"}]},{"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","last_name":"Ibsen-Jensen"}],"volume":285,"page":"1432 - 1439","license":"https://creativecommons.org/licenses/by-nc/4.0/","article_processing_charge":"No","abstract":[{"lang":"eng","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."}],"external_id":{"isi":["000385793700166"]},"publication_status":"published","title":"The complexity of deciding legality of a single step of magic: The gathering","year":"2016","date_created":"2018-12-11T11:46:41Z","doi":"10.3233/978-1-61499-672-9-1432","corr_author":"1","quality_controlled":"1","file":[{"file_id":"4658","file_size":2116225,"date_updated":"2020-07-14T12:46:35Z","access_level":"open_access","checksum":"848043c812ace05e459579c923f3d3cf","relation":"main_file","file_name":"IST-2018-950-v1+1_2016_Chatterjee_The_complexity.pdf","content_type":"application/pdf","date_created":"2018-12-12T10:07:59Z","creator":"system"}],"has_accepted_license":"1","ddc":["004"],"conference":{"location":"The Hague, Netherlands","end_date":"2016-09-02","start_date":"2016-08-29","name":"ECAI: European Conference on Artificial Intelligence"},"oa_version":"Published Version","intvolume":"       285","type":"conference","publist_id":"7342","_id":"478","scopus_import":"1","isi":1,"oa":1,"file_date_updated":"2020-07-14T12:46:35Z","language":[{"iso":"eng"}],"month":"01","date_published":"2016-01-01T00:00:00Z","publisher":"IOS Press","department":[{"_id":"KrCh"}],"date_updated":"2025-09-22T14:26:27Z","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"},"alternative_title":["Frontiers in Artificial Intelligence and Applications"],"status":"public","day":"01","pubrep_id":"950","citation":{"short":"K. Chatterjee, R. Ibsen-Jensen, in:, IOS Press, 2016, pp. 1432–1439.","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.","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>","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.","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>","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>.","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>."}},{"conference":{"end_date":"2016-07-08","location":"New York, NY, USA","name":"LICS: Logic in Computer Science","start_date":"2016-07-05"},"main_file_link":[{"url":"https://arxiv.org/abs/1604.06376","open_access":"1"}],"quality_controlled":"1","doi":"10.1145/2933575.2934513","date_created":"2018-12-11T11:46:42Z","year":"2016","title":"Perfect-information stochastic games with generalized mean-payoff objectives","external_id":{"arxiv":["1604.06376"],"isi":["000387609200025"]},"publication_status":"published","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"}],"article_processing_charge":"No","page":"247 - 256","volume":"05-08-July-2016","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Doyen, Laurent","first_name":"Laurent","last_name":"Doyen"}],"project":[{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003"}],"citation":{"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>.","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>","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>","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.","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."},"status":"public","day":"05","alternative_title":["Proceedings Symposium on Logic in Computer Science"],"ec_funded":1,"date_updated":"2025-09-22T14:22:08Z","publisher":"IEEE","department":[{"_id":"KrCh"}],"arxiv":1,"date_published":"2016-07-05T00:00:00Z","month":"07","language":[{"iso":"eng"}],"oa":1,"isi":1,"scopus_import":"1","_id":"480","publist_id":"7340","type":"conference","oa_version":"Preprint"},{"has_accepted_license":"1","ddc":["005"],"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":[{"date_created":"2018-12-12T11:53:52Z","content_type":"application/pdf","file_name":"IST-2016-523-v1+1_main.pdf","creator":"system","file_id":"5513","access_level":"open_access","checksum":"cef516fa091925b5868813e355268fb4","relation":"main_file","date_updated":"2020-07-14T12:46:58Z","file_size":1012204}],"alternative_title":["IST Austria Technical Report"],"publication_identifier":{"issn":["2664-1690"]},"doi":"10.15479/AT:IST-2016-523-v1-1","day":"31","status":"public","pubrep_id":"523","year":"2016","date_created":"2018-12-12T11:39:22Z","language":[{"iso":"eng"}],"title":"Quantitative interprocedural analysis","month":"03","date_published":"2016-03-31T00:00:00Z","publisher":"IST Austria","department":[{"_id":"KrCh"}],"date_updated":"2025-04-15T08:11:41Z","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","related_material":{"record":[{"relation":"later_version","id":"1604","status":"public"}]},"_id":"5445","author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"},{"last_name":"Pavlogiannis","first_name":"Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas"},{"last_name":"Velner","first_name":"Yaron","full_name":"Velner, Yaron"}],"oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"technical_report"},{"doi":"10.15479/AT:IST-2016-648-v1-1","publication_identifier":{"issn":["2664-1690"]},"alternative_title":["IST Austria Technical Report"],"pubrep_id":"648","status":"public","day":"09","date_created":"2018-12-12T11:39:24Z","year":"2016","has_accepted_license":"1","ddc":["519"],"citation":{"short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Amplification on Undirected Population Structures: Comets Beat Stars, IST Austria, 2016.","ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, <i>Amplification on undirected population structures: Comets beat stars</i>. 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","content_type":"application/pdf","file_name":"IST-2016-648-v1+1_tr.pdf","creator":"system","file_id":"5529","access_level":"open_access","relation":"main_file","checksum":"8345a8c1e7d7f0cd92516d182b7fc59e","date_updated":"2020-07-14T12:46:58Z","file_size":1264221}],"related_material":{"record":[{"id":"512","relation":"later_version","status":"public"}]},"_id":"5449","oa_version":"Updated Version","author":[{"first_name":"Andreas","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722"},{"id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-1097-9684","full_name":"Tkadlec, Josef","first_name":"Josef","last_name":"Tkadlec"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee"},{"last_name":"Nowak","first_name":"Martin","full_name":"Nowak, Martin"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"technical_report","date_published":"2016-11-09T00:00:00Z","language":[{"iso":"eng"}],"month":"11","title":"Amplification on undirected population structures: Comets beat stars","date_updated":"2025-09-18T09:50:09Z","department":[{"_id":"KrCh"}],"publisher":"IST Austria","page":"22","publication_status":"published","file_date_updated":"2020-07-14T12:46:58Z","abstract":[{"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.","lang":"eng"}],"oa":1},{"day":"30","status":"public","pubrep_id":"728","alternative_title":["IST Austria Technical Report"],"doi":"10.15479/AT:IST-2016-728-v1-1","publication_identifier":{"issn":["2664-1690"]},"year":"2016","date_created":"2018-12-12T11:39:24Z","ddc":["000"],"has_accepted_license":"1","file":[{"creator":"system","content_type":"application/pdf","file_name":"IST-2016-728-v1+1_main.pdf","date_created":"2018-12-12T11:53:04Z","date_updated":"2020-07-14T12:46:59Z","file_size":1014732,"relation":"main_file","checksum":"7b8bb17c322c0556acba6ac169fa71c1","access_level":"open_access","file_id":"5465"}],"citation":{"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>.","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>","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>.","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>","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."},"_id":"5451","type":"technical_report","author":[{"orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","first_name":"Andreas","last_name":"Pavlogiannis"},{"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"},{"last_name":"Nowak","first_name":"Martin","full_name":"Nowak, Martin"}],"oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"IST Austria","department":[{"_id":"KrCh"}],"date_updated":"2023-02-23T12:27:05Z","month":"12","language":[{"iso":"eng"}],"title":"Strong amplifiers of natural selection","date_published":"2016-12-30T00:00:00Z","oa":1,"file_date_updated":"2020-07-14T12:46:59Z","publication_status":"published","page":"34"},{"month":"12","language":[{"iso":"eng"}],"date_published":"2016-12-30T00:00:00Z","publisher":"IST Austria","department":[{"_id":"KrCh"}],"date_updated":"2025-04-15T07:55:39Z","oa":1,"file_date_updated":"2020-07-14T12:46:59Z","_id":"5452","oa_version":"Published Version","type":"technical_report","citation":{"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>","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>.","short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Arbitrarily Strong Amplifiers of Natural Selection, IST Austria, 2016.","ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, <i>Arbitrarily strong amplifiers of natural selection</i>. IST Austria, 2016.","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>","ista":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Arbitrarily strong amplifiers of natural selection, IST Austria, 32p."},"project":[{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"}],"alternative_title":["IST Austria Technical Report"],"status":"public","day":"30","pubrep_id":"750","ec_funded":1,"title":"Arbitrarily strong amplifiers of natural selection","page":"32","article_processing_charge":"No","publication_status":"published","related_material":{"record":[{"relation":"later_version","id":"5453","status":"public"},{"status":"public","relation":"popular_science","id":"5559"}]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"last_name":"Pavlogiannis","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas"},{"full_name":"Tkadlec, Josef","orcid":"0000-0002-1097-9684","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","last_name":"Tkadlec","first_name":"Josef"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee"},{"last_name":"Nowak","first_name":"Martin","full_name":"Nowak, Martin"}],"has_accepted_license":"1","ddc":["000"],"file":[{"date_created":"2018-12-12T11:52:59Z","file_name":"IST-2017-728-v2+1_main.pdf","content_type":"application/pdf","creator":"system","file_id":"5460","access_level":"open_access","checksum":"58e895f26c82f560c0f0989bf8b08599","relation":"main_file","file_size":811558,"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"},{"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"5452"}]},"_id":"5453","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"last_name":"Pavlogiannis","first_name":"Andreas","full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722"},{"orcid":"0000-0002-1097-9684","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","full_name":"Tkadlec, Josef","first_name":"Josef","last_name":"Tkadlec"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Nowak, Martin","first_name":"Martin","last_name":"Nowak"}],"oa_version":"Published Version","type":"technical_report","date_published":"2016-12-30T00:00:00Z","language":[{"iso":"eng"}],"title":"Arbitrarily strong amplifiers of natural selection","month":"12","date_updated":"2025-04-15T07:55:37Z","publisher":"IST Austria","department":[{"_id":"KrCh"}],"page":"34","publication_status":"published","file_date_updated":"2020-07-14T12:46:59Z","oa":1,"doi":"10.15479/AT:IST-2017-749-v3-1","publication_identifier":{"issn":["2664-1690"]},"alternative_title":["IST Austria Technical Report"],"status":"public","pubrep_id":"755","day":"30","date_created":"2018-12-12T11:39:25Z","year":"2016","has_accepted_license":"1","ddc":["000"],"citation":{"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>.","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>","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>.","short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Arbitrarily Strong Amplifiers of Natural Selection, IST Austria, 2016.","ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, <i>Arbitrarily strong amplifiers of natural selection</i>. IST Austria, 2016.","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>"},"file":[{"file_size":1015647,"date_updated":"2020-07-14T12:46:59Z","relation":"main_file","checksum":"83b0313dab3bff4bdb6ac38695026fda","access_level":"open_access","file_id":"5474","creator":"system","content_type":"application/pdf","file_name":"IST-2017-749-v3+1_main.pdf","date_created":"2018-12-12T11:53:13Z"}]},{"doi":"10.4230/LIPIcs.MFCS.2016.25","year":"2016","date_created":"2018-12-11T11:49:58Z","article_number":"25","has_accepted_license":"1","conference":{"location":"Krakow, Poland","end_date":"2016-08-26","start_date":"2016-08-22","name":"MFCS: Mathematical Foundations of Computer Science"},"ddc":["000","004","006"],"quality_controlled":"1","file":[{"relation":"main_file","access_level":"open_access","date_updated":"2018-12-12T10:16:02Z","file_size":632786,"file_id":"5187","creator":"system","date_created":"2018-12-12T10:16:02Z","file_name":"IST-2017-779-v1+1_LIPIcs-MFCS-2016-25.pdf","content_type":"application/pdf"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Dvorák, Wolfgang","first_name":"Wolfgang","last_name":"Dvorák"},{"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,"title":"Conditionally optimal algorithms for generalized Büchi Games","license":"https://creativecommons.org/licenses/by/3.0/","article_processing_charge":"No","abstract":[{"lang":"eng","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}. "}],"publication_status":"published","alternative_title":["LIPIcs"],"day":"01","status":"public","pubrep_id":"779","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)"},"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>.","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>","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>.","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>","short":"K. Chatterjee, W. Dvorák, M. Henzinger, V. Loitzenbauer, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","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."},"project":[{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"}],"publist_id":"6317","_id":"1068","scopus_import":"1","oa_version":"Published Version","intvolume":"        58","type":"conference","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","language":[{"iso":"eng"}],"month":"08","date_published":"2016-08-01T00:00:00Z","department":[{"_id":"KrCh"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_updated":"2025-07-10T11:49:55Z","oa":1,"file_date_updated":"2018-12-12T10:16:02Z"},{"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","citation":{"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>","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.","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.","short":"V.K. Chonev, J. Ouaknine, J. Worrell, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","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>.","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>"},"project":[{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"}],"oa_version":"Published Version","intvolume":"        55","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","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","year":"2016","date_created":"2018-12-11T11:49:59Z","article_number":"100","doi":"10.4230/LIPIcs.ICALP.2016.100","file":[{"file_size":521415,"date_updated":"2018-12-12T10:16:26Z","relation":"main_file","access_level":"open_access","file_id":"5213","creator":"system","file_name":"IST-2017-778-v1+1_LIPIcs-ICALP-2016-100.pdf","content_type":"application/pdf","date_created":"2018-12-12T10:16:26Z"}],"quality_controlled":"1","has_accepted_license":"1","ddc":["004","006"],"conference":{"start_date":"2016-07-12","name":"ICALP: Automata, Languages and Programming","end_date":"2016-07-15","location":"Rome, Italy"},"author":[{"last_name":"Chonev","first_name":"Ventsislav K","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"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","volume":55,"license":"https://creativecommons.org/licenses/by/4.0/","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"},{"scopus_import":"1","_id":"1070","publist_id":"6313","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","oa_version":"Published Version","intvolume":"        55","date_updated":"2025-06-03T11:18:54Z","department":[{"_id":"KrCh"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_published":"2016-01-01T00:00:00Z","language":[{"iso":"eng"}],"month":"01","file_date_updated":"2018-12-12T10:08:52Z","oa":1,"pubrep_id":"812","day":"01","status":"public","alternative_title":["LIPIcs"],"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,"project":[{"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"},{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"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."},"volume":55,"author":[{"last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"last_name":"Doyen","first_name":"Laurent","full_name":"Doyen, Laurent"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Computation tree logic for synchronization properties","publication_status":"published","abstract":[{"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. ","lang":"eng"}],"article_processing_charge":"No","doi":"10.4230/LIPIcs.ICALP.2016.98","article_number":"98","date_created":"2018-12-11T11:49:59Z","year":"2016","ddc":["005"],"conference":{"name":"ICALP: Automata, Languages and Programming","start_date":"2016-07-12","end_date":"2016-07-15","location":"Rome, Italy"},"has_accepted_license":"1","quality_controlled":"1","file":[{"relation":"main_file","access_level":"open_access","file_size":546133,"date_updated":"2018-12-12T10:08:52Z","file_id":"4714","creator":"system","date_created":"2018-12-12T10:08:52Z","file_name":"IST-2017-812-v1+1_LIPIcs-ICALP-2016-98.pdf","content_type":"application/pdf"}]},{"type":"conference","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).","intvolume":"        57","oa_version":"Published Version","_id":"1071","scopus_import":"1","publist_id":"6312","oa":1,"file_date_updated":"2018-12-12T10:14:31Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","department":[{"_id":"KrCh"}],"date_updated":"2026-04-08T14:22:16Z","language":[{"iso":"eng"}],"month":"08","date_published":"2016-08-01T00:00:00Z","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)"},"day":"01","pubrep_id":"777","status":"public","alternative_title":["LIPIcs"],"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"}],"citation":{"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.","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.","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","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>"},"volume":57,"author":[{"first_name":"Krishnendu","last_name":"Chatterjee","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","first_name":"Rasmus","last_name":"Ibsen-Jensen"},{"orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis","first_name":"Andreas"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"status":"public","id":"821","relation":"dissertation_contains"}]},"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. "}],"publication_status":"published","article_processing_charge":"No","title":"Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs","article_number":"28","year":"2016","date_created":"2018-12-11T11:49:59Z","doi":"10.4230/LIPIcs.ESA.2016.28","file":[{"creator":"system","date_created":"2018-12-12T10:14:31Z","content_type":"application/pdf","file_name":"IST-2017-777-v1+1_LIPIcs-ESA-2016-28.pdf","relation":"main_file","access_level":"open_access","file_size":579225,"date_updated":"2018-12-12T10:14:31Z","file_id":"5084"}],"quality_controlled":"1","conference":{"location":"Aarhus, Denmark","end_date":"2016-08-24","name":"ESA: European Symposium on Algorithms","start_date":"2016-08-22"},"ddc":["004","006"],"has_accepted_license":"1"},{"type":"research_data_reference","oa_version":"Published Version","user_id":"6785fbc1-c503-11eb-8a32-93094b40e1cf","author":[{"full_name":"Hilbe, Christian","orcid":"0000-0001-5116-955X","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","first_name":"Christian","last_name":"Hilbe"},{"full_name":"Hagel, Kristin","last_name":"Hagel","first_name":"Kristin"},{"full_name":"Milinski, Manfred","first_name":"Manfred","last_name":"Milinski"}],"_id":"9867","related_material":{"record":[{"status":"public","relation":"used_in_publication","id":"1322"}]},"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"}],"article_processing_charge":"No","department":[{"_id":"KrCh"}],"publisher":"Public Library of Science","date_updated":"2025-09-22T08:27:00Z","month":"10","title":"Experimental game instructions","year":"2016","date_created":"2021-08-10T08:42:00Z","day":"04","status":"public","doi":"10.1371/journal.pone.0163867.s008","citation":{"short":"C. Hilbe, K. Hagel, M. Milinski, (2016).","ieee":"C. Hilbe, K. Hagel, and M. Milinski, “Experimental game instructions.” Public Library of Science, 2016.","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>.","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>","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>.","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>","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>."}},{"citation":{"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>.","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>","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>.","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>","short":"C. Hilbe, K. Hagel, M. Milinski, (2016).","ieee":"C. Hilbe, K. Hagel, and M. Milinski, “Experimental data.” Public Library of Science, 2016."},"doi":"10.1371/journal.pone.0163867.s009","day":"04","status":"public","date_created":"2021-08-10T08:45:00Z","year":"2016","date_published":"2016-10-04T00:00:00Z","month":"10","title":"Experimental data","date_updated":"2025-09-22T08:27:00Z","department":[{"_id":"KrCh"}],"publisher":"Public Library of Science","article_processing_charge":"No","abstract":[{"lang":"eng","text":"The raw data file containing the experimental decisions of all our study subjects."}],"_id":"9868","related_material":{"record":[{"id":"1322","relation":"used_in_publication","status":"public"}]},"oa_version":"Published Version","user_id":"6785fbc1-c503-11eb-8a32-93094b40e1cf","author":[{"first_name":"Christian","last_name":"Hilbe","orcid":"0000-0001-5116-955X","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","full_name":"Hilbe, Christian"},{"last_name":"Hagel","first_name":"Kristin","full_name":"Hagel, Kristin"},{"full_name":"Milinski, Manfred","first_name":"Manfred","last_name":"Milinski"}],"type":"research_data_reference"},{"corr_author":"1","citation":{"short":"M. Chmelik, Algorithms for Partially Observable Markov Decision Processes, Institute of Science and Technology Austria, 2016.","ieee":"M. Chmelik, “Algorithms for partially observable markov decision processes,” Institute of Science and Technology Austria, 2016.","ista":"Chmelik M. 2016. Algorithms for partially observable markov decision processes. Institute of Science and Technology Austria.","ama":"Chmelik M. Algorithms for partially observable markov decision processes. 2016.","chicago":"Chmelik, Martin. “Algorithms for Partially Observable Markov Decision Processes.” Institute of Science and Technology Austria, 2016.","apa":"Chmelik, M. (2016). <i>Algorithms for partially observable markov decision processes</i>. Institute of Science and Technology Austria.","mla":"Chmelik, Martin. <i>Algorithms for Partially Observable Markov Decision Processes</i>. Institute of Science and Technology Austria, 2016."},"year":"2016","date_created":"2018-12-11T11:51:47Z","day":"01","status":"public","alternative_title":["ISTA Thesis"],"publication_identifier":{"issn":["2663-337X"]},"abstract":[{"text":"We study partially observable Markov decision processes (POMDPs) with objectives used in verification and artificial intelligence. The qualitative analysis problem given a POMDP and an objective asks whether there is a strategy (policy) to ensure that the objective is satisfied almost surely (with probability 1), resp. with positive probability (with probability greater than 0). For POMDPs with limit-average payoff, where a reward value in the interval [0,1] is associated to every transition, and the payoff of an infinite path is the long-run average of the rewards, we consider two types of path constraints: (i) a quantitative limit-average constraint defines the set of paths where the payoff is at least a given threshold L1 = 1. Our main results for qualitative limit-average constraint under almost-sure winning are as follows: (i) the problem of deciding the existence of a finite-memory controller is EXPTIME-complete; and (ii) the problem of deciding the existence of an infinite-memory controller is undecidable. For quantitative limit-average constraints we show that the problem of deciding the existence of a finite-memory controller is undecidable. We present a prototype implementation of our EXPTIME algorithm. For POMDPs with w-regular conditions specified as parity objectives, while the qualitative analysis problems are known to be undecidable even for very special case of parity objectives, we establish decidability (with optimal complexity) of the qualitative analysis problems for POMDPs with 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. Based on our theoretical algorithms 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 well-known POMDP examples for robotics applications. For POMDPs with a set of target states and an integer cost associated with every transition, we study the optimization objective that asks to minimize the expected total cost of reaching a state in the target set, while ensuring that the target set is reached almost surely. We show that for general integer costs approximating the optimal cost is undecidable. For positive costs, our results are as follows: (i) we establish matching lower and upper bounds for the optimal cost, both double and exponential in the POMDP state space size; (ii) we show that the problem of approximating the optimal cost is decidable and present approximation algorithms that extend existing algorithms for POMDPs with finite-horizon objectives. We show experimentally that it performs well in many examples of interest. We study more deeply the problem of almost-sure reachability, where  given a set of target states, the question is to decide whether there is a strategy to ensure that the target set is reached almost surely. While in general the problem EXPTIME-complete, in many practical cases strategies with a small amount of memory suffice. Moreover, the existing solution to the problem is explicit, which first requires to construct explicitly an exponential reduction to a belief-support MDP. We first study the existence of observation-stationary strategies, which is NP-complete, and then small-memory strategies. We present a symbolic algorithm by an efficient encoding to SAT and using a SAT solver for the problem. We report experimental results demonstrating the scalability of our symbolic (SAT-based) approach. Decentralized POMDPs (DEC-POMDPs) extend POMDPs to a multi-agent setting, where several agents operate in an uncertain environment independently to achieve a joint objective. In this work we consider Goal DEC-POMDPs, where given a set of target states, the objective is to ensure that the target set is reached with minimal cost. We consider the indefinite-horizon (infinite-horizon with either discounted-sum, or undiscounted-sum, where absorbing goal states have zero-cost) problem. We present a new and novel method to solve the problem that extends methods for finite-horizon DEC-POMDPs and the real-time dynamic programming approach for POMDPs. We present experimental results on several examples, and show that our approach presents promising results. In the end we present a short summary of a few other results related to verification of MDPs and POMDPs.","lang":"eng"}],"publication_status":"published","page":"232","article_processing_charge":"No","department":[{"_id":"KrCh"},{"_id":"GradSch"}],"publisher":"Institute of Science and Technology Austria","date_updated":"2026-07-29T11:15:18Z","month":"02","title":"Algorithms for partially observable markov decision processes","language":[{"iso":"eng"}],"degree_awarded":"PhD","doi_confirm":"1","date_published":"2016-02-01T00:00:00Z","supervisor":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu"}],"type":"dissertation","OA_place":"publisher","author":[{"last_name":"Chmelik","first_name":"Martin","full_name":"Chmelik, Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87"}],"oa_version":"None","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","_id":"1397","publist_id":"5810"},{"date_updated":"2026-08-12T06:24:55Z","department":[{"_id":"KrCh"}],"publisher":"Royal Society","date_published":"2016-05-01T00:00:00Z","month":"05","language":[{"iso":"eng"}],"file_date_updated":"2020-07-14T12:44:53Z","oa":1,"isi":1,"scopus_import":"1","_id":"1426","publist_id":"5776","acknowledgement":"C.H. gratefully acknowledges funding by the Schrödinger scholarship of the Austrian Science Fund (FWF) J3475.","type":"journal_article","oa_version":"Published Version","intvolume":"         3","citation":{"short":"M. Chakra, C. Hilbe, A. Traulsen, Royal Society Open Science 3 (2016).","ieee":"M. Chakra, C. Hilbe, and A. Traulsen, “Coevolutionary interactions between farmers and mafia induce host acceptance of avian brood parasites,” <i>Royal Society Open Science</i>, vol. 3, no. 5. Royal Society, 2016.","ista":"Chakra M, Hilbe C, Traulsen A. 2016. Coevolutionary interactions between farmers and mafia induce host acceptance of avian brood parasites. Royal Society Open Science. 3(5), 160036.","ama":"Chakra M, Hilbe C, Traulsen A. Coevolutionary interactions between farmers and mafia induce host acceptance of avian brood parasites. <i>Royal Society Open Science</i>. 2016;3(5). doi:<a href=\"https://doi.org/10.1098/rsos.160036\">10.1098/rsos.160036</a>","chicago":"Chakra, Maria, Christian Hilbe, and Arne Traulsen. “Coevolutionary Interactions between Farmers and Mafia Induce Host Acceptance of Avian Brood Parasites.” <i>Royal Society Open Science</i>. Royal Society, 2016. <a href=\"https://doi.org/10.1098/rsos.160036\">https://doi.org/10.1098/rsos.160036</a>.","apa":"Chakra, M., Hilbe, C., &#38; Traulsen, A. (2016). Coevolutionary interactions between farmers and mafia induce host acceptance of avian brood parasites. <i>Royal Society Open Science</i>. Royal Society. <a href=\"https://doi.org/10.1098/rsos.160036\">https://doi.org/10.1098/rsos.160036</a>","mla":"Chakra, Maria, et al. “Coevolutionary Interactions between Farmers and Mafia Induce Host Acceptance of Avian Brood Parasites.” <i>Royal Society Open Science</i>, vol. 3, no. 5, 160036, Royal Society, 2016, doi:<a href=\"https://doi.org/10.1098/rsos.160036\">10.1098/rsos.160036</a>."},"pubrep_id":"589","day":"01","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)"},"title":"Coevolutionary interactions between farmers and mafia induce host acceptance of avian brood parasites","external_id":{"isi":["000377969800008"]},"publication_status":"published","abstract":[{"text":"Brood parasites exploit their host in order to increase their own fitness. Typically, this results in an arms race between parasite trickery and host defence. Thus, it is puzzling to observe hosts that accept parasitism without any resistance. The ‘mafia’ hypothesis suggests that these hosts accept parasitism to avoid retaliation. Retaliation has been shown to evolve when the hosts condition their response to mafia parasites, who use depredation as a targeted response to rejection. However, it is unclear if acceptance would also emerge when ‘farming’ parasites are present in the population. Farming parasites use depredation to synchronize the timing with the host, destroying mature clutches to force the host to re-nest. Herein, we develop an evolutionary model to analyse the interaction between depredatory parasites and their hosts. We show that coevolutionary cycles between farmers and mafia can still induce host acceptance of brood parasites. However, this equilibrium is unstable and in the long-run the dynamics of this host–parasite interaction exhibits strong oscillations: when farmers are the majority, accepters conditional to mafia (the host will reject first and only accept after retaliation by the parasite) have a higher fitness than unconditional accepters (the host always accepts parasitism). This leads to an increase in mafia parasites’ fitness and in turn induce an optimal environment for accepter hosts.","lang":"eng"}],"article_processing_charge":"No","volume":3,"author":[{"last_name":"Chakra","first_name":"Maria","full_name":"Chakra, Maria"},{"id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-5116-955X","full_name":"Hilbe, Christian","last_name":"Hilbe","first_name":"Christian"},{"last_name":"Traulsen","first_name":"Arne","full_name":"Traulsen, Arne"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000"],"has_accepted_license":"1","quality_controlled":"1","file":[{"creator":"system","date_created":"2018-12-12T10:14:49Z","content_type":"application/pdf","file_name":"IST-2016-589-v1+1_160036.full.pdf","relation":"main_file","checksum":"bf84211b31fe87451e738ba301d729c3","access_level":"open_access","date_updated":"2020-07-14T12:44:53Z","file_size":937002,"file_id":"5104"}],"publication":"Royal Society Open Science","doi":"10.1098/rsos.160036","issue":"5","article_number":"160036","date_created":"2018-12-11T11:51:57Z","year":"2016"},{"publication":"Proceedings of the 31st Annual ACM/IEEE Symposium","doi":"10.1145/2933575.2933588","year":"2016","date_created":"2018-12-11T11:50:21Z","conference":{"start_date":"2016-07-05","name":"LICS: Logic in Computer Science","end_date":"2016-07-08","location":"New York, NY, USA"},"main_file_link":[{"url":"https://arxiv.org/abs/1604.06764","open_access":"1"}],"quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"},{"first_name":"Jan","last_name":"Otop","full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"title":"Quantitative automata under probabilistic semantics","abstract":[{"lang":"eng","text":"Automata with monitor counters, where the transitions do not depend on counter values, and nested weighted automata are two expressive automata-theoretic frameworks for quantitative properties. For a well-studied and wide class of quantitative functions, we establish that automata with monitor counters and nested weighted automata are equivalent. We study for the first time such quantitative automata under probabilistic semantics. We show that several problems that are undecidable for the classical questions of emptiness and universality become decidable under the probabilistic semantics. We present a complete picture of decidability for such automata, and even an almost-complete picture of computational complexity, for the probabilistic questions we consider."}],"publication_status":"published","external_id":{"isi":["000387609200008"],"arxiv":["1604.06764"]},"page":"76 - 85","article_processing_charge":"No","status":"public","day":"05","ec_funded":1,"project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"}],"citation":{"ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Quantitative automata under probabilistic semantics,” in <i>Proceedings of the 31st Annual ACM/IEEE Symposium</i>, New York, NY, USA, 2016, pp. 76–85.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Proceedings of the 31st Annual ACM/IEEE Symposium, IEEE, 2016, pp. 76–85.","ista":"Chatterjee K, Henzinger TA, Otop J. 2016. Quantitative automata under probabilistic semantics. Proceedings of the 31st Annual ACM/IEEE Symposium. LICS: Logic in Computer Science, 76–85.","ama":"Chatterjee K, Henzinger TA, Otop J. Quantitative automata under probabilistic semantics. In: <i>Proceedings of the 31st Annual ACM/IEEE Symposium</i>. IEEE; 2016:76-85. doi:<a href=\"https://doi.org/10.1145/2933575.2933588\">10.1145/2933575.2933588</a>","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2016). Quantitative automata under probabilistic semantics. In <i>Proceedings of the 31st Annual ACM/IEEE Symposium</i> (pp. 76–85). New York, NY, USA: IEEE. <a href=\"https://doi.org/10.1145/2933575.2933588\">https://doi.org/10.1145/2933575.2933588</a>","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Quantitative Automata under Probabilistic Semantics.” In <i>Proceedings of the 31st Annual ACM/IEEE Symposium</i>, 76–85. IEEE, 2016. <a href=\"https://doi.org/10.1145/2933575.2933588\">https://doi.org/10.1145/2933575.2933588</a>.","mla":"Chatterjee, Krishnendu, et al. “Quantitative Automata under Probabilistic Semantics.” <i>Proceedings of the 31st Annual ACM/IEEE Symposium</i>, IEEE, 2016, pp. 76–85, doi:<a href=\"https://doi.org/10.1145/2933575.2933588\">10.1145/2933575.2933588</a>."},"_id":"1138","scopus_import":"1","publist_id":"6220","acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF) projects S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), FWF Grant No P23499- N23, FWF NFN Grant No S114","type":"conference","oa_version":"Preprint","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"IEEE","arxiv":1,"date_updated":"2026-08-19T09:35:52Z","month":"07","language":[{"iso":"eng"}],"date_published":"2016-07-05T00:00:00Z","oa":1,"isi":1},{"publist_id":"5642","scopus_import":"1","_id":"1529","intvolume":"       234","oa_version":"Preprint","type":"journal_article","acknowledgement":"We thank Blai Bonet for helping us with RTDP-Bel. The research was partly supported by Austrian Science Fund (FWF) Grant No P23499-N23, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.","date_published":"2016-05-01T00:00:00Z","language":[{"iso":"eng"}],"month":"05","date_updated":"2026-08-19T09:31:46Z","publisher":"Elsevier","arxiv":1,"department":[{"_id":"KrCh"}],"isi":1,"oa":1,"status":"public","day":"01","ec_funded":1,"citation":{"ieee":"K. Chatterjee, M. Chmelik, R. Gupta, and A. Kanodia, “Optimal cost almost-sure reachability in POMDPs,” <i>Artificial Intelligence</i>, vol. 234. Elsevier, pp. 26–48, 2016.","short":"K. Chatterjee, M. Chmelik, R. Gupta, A. Kanodia, Artificial Intelligence 234 (2016) 26–48.","ama":"Chatterjee K, Chmelik M, Gupta R, Kanodia A. Optimal cost almost-sure reachability in POMDPs. <i>Artificial Intelligence</i>. 2016;234:26-48. doi:<a href=\"https://doi.org/10.1016/j.artint.2016.01.007\">10.1016/j.artint.2016.01.007</a>","ista":"Chatterjee K, Chmelik M, Gupta R, Kanodia A. 2016. Optimal cost almost-sure reachability in POMDPs. Artificial Intelligence. 234, 26–48.","apa":"Chatterjee, K., Chmelik, M., Gupta, R., &#38; Kanodia, A. (2016). Optimal cost almost-sure reachability in POMDPs. <i>Artificial Intelligence</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.artint.2016.01.007\">https://doi.org/10.1016/j.artint.2016.01.007</a>","chicago":"Chatterjee, Krishnendu, Martin Chmelik, Raghav Gupta, and Ayush Kanodia. “Optimal Cost Almost-Sure Reachability in POMDPs.” <i>Artificial Intelligence</i>. Elsevier, 2016. <a href=\"https://doi.org/10.1016/j.artint.2016.01.007\">https://doi.org/10.1016/j.artint.2016.01.007</a>.","mla":"Chatterjee, Krishnendu, et al. “Optimal Cost Almost-Sure Reachability in POMDPs.” <i>Artificial Intelligence</i>, vol. 234, Elsevier, 2016, pp. 26–48, doi:<a href=\"https://doi.org/10.1016/j.artint.2016.01.007\">10.1016/j.artint.2016.01.007</a>."},"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"}],"related_material":{"record":[{"id":"5425","relation":"earlier_version","status":"public"},{"relation":"earlier_version","id":"1820","status":"public"}]},"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"},{"last_name":"Gupta","first_name":"Raghav","full_name":"Gupta, Raghav"},{"first_name":"Ayush","last_name":"Kanodia","full_name":"Kanodia, Ayush"}],"volume":234,"title":"Optimal cost almost-sure reachability in POMDPs","article_processing_charge":"No","page":"26 - 48","external_id":{"isi":["000372683700002"],"arxiv":["1411.3880"]},"publication_status":"published","abstract":[{"text":"We consider partially observable Markov decision processes (POMDPs) with a set of target states and an integer cost associated with every transition. The optimization objective we study asks to minimize the expected total cost of reaching a state in the target set, while ensuring that the target set is reached almost surely (with probability 1). We show that for integer costs approximating the optimal cost is undecidable. For positive costs, our results are as follows: (i) we establish matching lower and upper bounds for the optimal cost, both double exponential in the POMDP state space size; (ii) we show that the problem of approximating the optimal cost is decidable and present approximation algorithms developing on the existing algorithms for POMDPs with finite-horizon objectives. While the worst-case running time of our algorithm is double exponential, we also present efficient stopping criteria for the algorithm and show experimentally that it performs well in many examples of interest.","lang":"eng"}],"doi":"10.1016/j.artint.2016.01.007","publication":"Artificial Intelligence","date_created":"2018-12-11T11:52:33Z","year":"2016","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1411.3880"}],"corr_author":"1","quality_controlled":"1"},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu"},{"full_name":"Goharshady, Amir","orcid":"0000-0003-1702-6584","id":"391365CE-F248-11E8-B48F-1D18A9856A87","last_name":"Goharshady","first_name":"Amir"},{"last_name":"Ibsen-Jensen","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389"},{"last_name":"Pavlogiannis","first_name":"Andreas","full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722"}],"volume":"20-22","related_material":{"record":[{"relation":"earlier_version","id":"5441","status":"public"},{"status":"public","relation":"earlier_version","id":"5442"},{"status":"public","relation":"later_version","id":"6009"},{"status":"public","relation":"dissertation_contains","id":"821"},{"relation":"dissertation_contains","id":"8934","status":"public"}]},"page":"733 - 747","abstract":[{"text":"We study algorithmic questions for concurrent systems where the transitions are labeled from a complete, closed semiring, and path properties are algebraic with semiring operations. The algebraic path properties can model dataflow analysis problems, the shortest path problem, and many other natural problems that arise in program analysis. We consider that each component of the concurrent system is a graph with constant treewidth, a property satisfied by the controlflow graphs of most programs. We allow for multiple possible queries, which arise naturally in demand driven dataflow analysis. The study of multiple queries allows us to consider the tradeoff between the resource usage of the one-time preprocessing and for each individual query. The traditional approach constructs the product graph of all components and applies the best-known graph algorithm on the product. In this approach, even the answer to a single query requires the transitive closure (i.e., the results of all possible queries), which provides no room for tradeoff between preprocessing and query time. Our main contributions are algorithms that significantly improve the worst-case running time of the traditional approach, and provide various tradeoffs depending on the number of queries. For example, in a concurrent system of two components, the traditional approach requires hexic time in the worst case for answering one query as well as computing the transitive closure, whereas we show that with one-time preprocessing in almost cubic time, each subsequent query can be answered in at most linear time, and even the transitive closure can be computed in almost quartic time. Furthermore, we establish conditional optimality results showing that the worst-case running time of our algorithms cannot be improved without achieving major breakthroughs in graph algorithms (i.e., improving the worst-case bound for the shortest path problem in general graphs). Preliminary experimental results show that our algorithms perform favorably on several benchmarks.","lang":"eng"}],"publication_status":"published","external_id":{"arxiv":["1510.07565"]},"title":"Algorithms for algebraic path properties in concurrent systems of constant treewidth components","year":"2016","date_created":"2018-12-11T11:52:01Z","doi":"10.1145/2837614.2837624","corr_author":"1","quality_controlled":"1","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1510.07565"}],"conference":{"location":"St. Petersburg, FL, USA","end_date":"2016-01-22","name":"POPL: Principles of Programming Languages","start_date":"2016-01-20"},"oa_version":"Preprint","type":"conference","publist_id":"5761","_id":"1437","scopus_import":1,"oa":1,"month":"01","language":[{"iso":"eng"}],"date_published":"2016-01-11T00:00:00Z","publisher":"ACM","department":[{"_id":"KrCh"}],"arxiv":1,"date_updated":"2026-09-04T22:31:00Z","ec_funded":1,"alternative_title":["POPL"],"status":"public","day":"11","citation":{"ieee":"K. Chatterjee, A. K. Goharshady, R. Ibsen-Jensen, and A. Pavlogiannis, “Algorithms for algebraic path properties in concurrent systems of constant treewidth components,” presented at the POPL: Principles of Programming Languages, St. Petersburg, FL, USA, 2016, vol. 20–22, pp. 733–747.","short":"K. Chatterjee, A.K. Goharshady, R. Ibsen-Jensen, A. Pavlogiannis, in:, ACM, 2016, pp. 733–747.","ista":"Chatterjee K, Goharshady AK, Ibsen-Jensen R, Pavlogiannis A. 2016. Algorithms for algebraic path properties in concurrent systems of constant treewidth components. POPL: Principles of Programming Languages, POPL, vol. 20–22, 733–747.","ama":"Chatterjee K, Goharshady AK, Ibsen-Jensen R, Pavlogiannis A. Algorithms for algebraic path properties in concurrent systems of constant treewidth components. In: Vol 20-22. ACM; 2016:733-747. doi:<a href=\"https://doi.org/10.1145/2837614.2837624\">10.1145/2837614.2837624</a>","apa":"Chatterjee, K., Goharshady, A. K., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2016). Algorithms for algebraic path properties in concurrent systems of constant treewidth components (Vol. 20–22, pp. 733–747). Presented at the POPL: Principles of Programming Languages, St. Petersburg, FL, USA: ACM. <a href=\"https://doi.org/10.1145/2837614.2837624\">https://doi.org/10.1145/2837614.2837624</a>","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components,” 20–22:733–47. ACM, 2016. <a href=\"https://doi.org/10.1145/2837614.2837624\">https://doi.org/10.1145/2837614.2837624</a>.","mla":"Chatterjee, Krishnendu, et al. <i>Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components</i>. Vol. 20–22, ACM, 2016, pp. 733–47, doi:<a href=\"https://doi.org/10.1145/2837614.2837624\">10.1145/2837614.2837624</a>."},"project":[{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}]}]