[{"status":"public","external_id":{"arxiv":["1604.07169"],"isi":["000387731200001"]},"abstract":[{"lang":"eng","text":"We consider nondeterministic probabilistic programs with the most basic liveness property of termination. We present efficient methods for termination analysis of nondeterministic probabilistic programs with polynomial guards and assignments. Our approach is through synthesis of polynomial ranking supermartingales, that on one hand significantly generalizes linear ranking supermartingales and on the other hand is a counterpart of polynomial ranking-functions for proving termination of nonprobabilistic programs. The approach synthesizes polynomial ranking-supermartingales through Positivstellensatz's, yielding an efficient method which is not only sound, but also semi-complete over a large subclass of programs. We show experimental results to demonstrate that our approach can handle several classical programs with complex polynomial guards and assignments, and can synthesize efficient quadratic ranking-supermartingales when a linear one does not exist even for simple affine programs."}],"corr_author":"1","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1604.07169"}],"type":"conference","date_created":"2018-12-11T11:51:43Z","publist_id":"5824","scopus_import":"1","oa_version":"Preprint","language":[{"iso":"eng"}],"ec_funded":1,"citation":{"mla":"Chatterjee, Krishnendu, et al. <i>Termination Analysis of Probabilistic Programs through Positivstellensatz’s</i>. Vol. 9779, Springer, 2016, pp. 3–22, doi:<a href=\"https://doi.org/10.1007/978-3-319-41528-4_1\">10.1007/978-3-319-41528-4_1</a>.","short":"K. Chatterjee, H. Fu, A.K. Goharshady, in:, Springer, 2016, pp. 3–22.","apa":"Chatterjee, K., Fu, H., &#38; Goharshady, A. K. (2016). Termination analysis of probabilistic programs through Positivstellensatz’s (Vol. 9779, pp. 3–22). Presented at the CAV: Computer Aided Verification, Toronto, Canada: Springer. <a href=\"https://doi.org/10.1007/978-3-319-41528-4_1\">https://doi.org/10.1007/978-3-319-41528-4_1</a>","ieee":"K. Chatterjee, H. Fu, and A. K. Goharshady, “Termination analysis of probabilistic programs through Positivstellensatz’s,” presented at the CAV: Computer Aided Verification, Toronto, Canada, 2016, vol. 9779, pp. 3–22.","ama":"Chatterjee K, Fu H, Goharshady AK. Termination analysis of probabilistic programs through Positivstellensatz’s. In: Vol 9779. Springer; 2016:3-22. doi:<a href=\"https://doi.org/10.1007/978-3-319-41528-4_1\">10.1007/978-3-319-41528-4_1</a>","ista":"Chatterjee K, Fu H, Goharshady AK. 2016. Termination analysis of probabilistic programs through Positivstellensatz’s. CAV: Computer Aided Verification, LNCS, vol. 9779, 3–22.","chicago":"Chatterjee, Krishnendu, Hongfei Fu, and Amir Kafshdar Goharshady. “Termination Analysis of Probabilistic Programs through Positivstellensatz’s,” 9779:3–22. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-319-41528-4_1\">https://doi.org/10.1007/978-3-319-41528-4_1</a>."},"arxiv":1,"date_updated":"2026-09-03T22:31:02Z","intvolume":"      9779","project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"last_name":"Fu","first_name":"Hongfei","id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","full_name":"Fu, Hongfei"},{"first_name":"Amir","orcid":"0000-0003-1702-6584","last_name":"Goharshady","id":"391365CE-F248-11E8-B48F-1D18A9856A87","full_name":"Goharshady, Amir"}],"alternative_title":["LNCS"],"page":"3 - 22","publication_status":"published","year":"2016","month":"07","volume":9779,"related_material":{"record":[{"status":"public","id":"8934","relation":"dissertation_contains"}]},"date_published":"2016-07-01T00:00:00Z","_id":"1386","quality_controlled":"1","conference":{"name":"CAV: Computer Aided Verification","start_date":"2016-07-17","location":"Toronto, Canada","end_date":"2016-07-23"},"publisher":"Springer","doi":"10.1007/978-3-319-41528-4_1","isi":1,"article_processing_charge":"No","title":"Termination analysis of probabilistic programs through Positivstellensatz's","oa":1,"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","department":[{"_id":"KrCh"}],"day":"01"},{"publication_status":"published","year":"2015","month":"01","related_material":{"record":[{"relation":"earlier_version","id":"5410","status":"public"}]},"volume":2,"author":[{"full_name":"Ahmed, Umair","first_name":"Umair","last_name":"Ahmed"},{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Gulwani, Sumit","first_name":"Sumit","last_name":"Gulwani"}],"page":"745 - 752","date_updated":"2025-05-19T11:10:17Z","arxiv":1,"intvolume":"         2","project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"abstract":[{"lang":"eng","text":"Simple board games, like Tic-Tac-Toe and CONNECT-4, play an important role not only in the development of mathematical and logical skills, but also in the emotional and social development. In this paper, we address the problem of generating targeted starting positions for such games. This can facilitate new approaches for bringing novice players to mastery, and also leads to discovery of interesting game variants. We present an approach that generates starting states of varying hardness levels for player 1 in a two-player board game, given rules of the board game, the desired number of steps required for player 1 to win, and the expertise levels of the two players. Our approach leverages symbolic methods and iterative simulation to efficiently search the extremely large state space. We present experimental results that include discovery of states of varying hardness levels for several simple grid-based board games. The presence of such states for standard game variants like 4×4 Tic-Tac-Toe opens up new games to be played that have never been played as the default start state is heavily biased. "}],"external_id":{"arxiv":["1411.4023"]},"status":"public","oa_version":"None","date_created":"2018-12-11T11:52:16Z","publication":"Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence","scopus_import":"1","publist_id":"5713","type":"conference","main_file_link":[{"open_access":"1","url":"https://www.aaai.org/ocs/index.php/AAAI/AAAI15/paper/download/9523/9300"}],"citation":{"chicago":"Ahmed, Umair, Krishnendu Chatterjee, and Sumit Gulwani. “Automatic Generation of Alternative Starting Positions for Simple Traditional Board Games.” In <i>Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence</i>, 2:745–52. AAAI Press, 2015.","ama":"Ahmed U, Chatterjee K, Gulwani S. Automatic generation of alternative starting positions for simple traditional board games. In: <i>Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence</i>. Vol 2. AAAI Press; 2015:745-752.","ista":"Ahmed U, Chatterjee K, Gulwani S. 2015. Automatic generation of alternative starting positions for simple traditional board games. Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 2, 745–752.","ieee":"U. Ahmed, K. Chatterjee, and S. Gulwani, “Automatic generation of alternative starting positions for simple traditional board games,” in <i>Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence</i>, Austin, TX, USA, 2015, vol. 2, pp. 745–752.","apa":"Ahmed, U., Chatterjee, K., &#38; Gulwani, S. (2015). Automatic generation of alternative starting positions for simple traditional board games. In <i>Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence</i> (Vol. 2, pp. 745–752). Austin, TX, USA: AAAI Press.","short":"U. Ahmed, K. Chatterjee, S. Gulwani, in:, Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, AAAI Press, 2015, pp. 745–752.","mla":"Ahmed, Umair, et al. “Automatic Generation of Alternative Starting Positions for Simple Traditional Board Games.” <i>Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence</i>, vol. 2, AAAI Press, 2015, pp. 745–52."},"ec_funded":1,"language":[{"iso":"eng"}],"oa":1,"title":"Automatic generation of alternative starting positions for simple traditional board games","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"KrCh"}],"day":"01","article_processing_charge":"No","conference":{"start_date":"2015-01-25","location":"Austin, TX, USA","end_date":"2015-01-30","name":"AAAI: Conference on Artificial Intelligence"},"publisher":"AAAI Press","acknowledgement":"A Technical Report of this paper is available at: \r\nhttps://repository.ist.ac.at/id/eprint/146.\r\n","date_published":"2015-01-01T00:00:00Z","_id":"1481","quality_controlled":"1"},{"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"day":"01","oa":1,"title":"Polynomial time decidability of weighted synchronization under partial observability","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","tmp":{"short":"CC BY (4.0)","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)"},"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","file":[{"date_updated":"2020-07-14T12:44:58Z","file_name":"IST-2016-498-v1+1_32.pdf","file_id":"4672","checksum":"49eb5021caafaabe5356c65b9c5f8c9c","file_size":623563,"content_type":"application/pdf","date_created":"2018-12-12T10:08:12Z","access_level":"open_access","relation":"main_file","creator":"system"}],"acknowledgement":"The research leading to these results has received funding from the European Union Seventh Framework Programme (FP7/2007-2013) under grant agreement 601148 (CASSTING), EU FP7 FET project SENSATION, Sino-Danish Basic Research Center IDAE4CPS, the European Research Council (ERC) under grant agreement 267989 (QUAREM), the Austrian Science Fund (FWF) project S11402-N23 (RiSE) and Z211-N23 (Wittgenstein Award), the Czech Science Foundation under grant agreement P202/12/G061, and People Programme (Marie Curie Actions) of the European Union’s Seventh Framework\r\nProgramme (FP7/2007-2013) REA Grant No 291734.","doi":"10.4230/LIPIcs.CONCUR.2015.142","conference":{"name":"CONCUR: Concurrency Theory","location":"Madrid, Spain","start_date":"2015-09-01","end_date":"2015-09-04"},"quality_controlled":"1","_id":"1499","date_published":"2015-01-01T00:00:00Z","month":"01","volume":42,"publication_status":"published","file_date_updated":"2020-07-14T12:44:58Z","year":"2015","page":"142 - 154","author":[{"last_name":"Kretinsky","orcid":"0000-0002-8122-2881","first_name":"Jan","full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Larsen, Kim","last_name":"Larsen","first_name":"Kim"},{"full_name":"Laursen, Simon","last_name":"Laursen","first_name":"Simon"},{"full_name":"Srba, Jiří","last_name":"Srba","first_name":"Jiří"}],"alternative_title":["LIPIcs"],"project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"grant_number":"291734","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425"}],"date_updated":"2025-04-15T06:26:02Z","ddc":["000","003"],"pubrep_id":"498","intvolume":"        42","ec_funded":1,"citation":{"apa":"Kretinsky, J., Larsen, K., Laursen, S., &#38; Srba, J. (2015). Polynomial time decidability of weighted synchronization under partial observability (Vol. 42, pp. 142–154). Presented at the CONCUR: Concurrency Theory, Madrid, Spain: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2015.142\">https://doi.org/10.4230/LIPIcs.CONCUR.2015.142</a>","ieee":"J. Kretinsky, K. Larsen, S. Laursen, and J. Srba, “Polynomial time decidability of weighted synchronization under partial observability,” presented at the CONCUR: Concurrency Theory, Madrid, Spain, 2015, vol. 42, pp. 142–154.","ista":"Kretinsky J, Larsen K, Laursen S, Srba J. 2015. Polynomial time decidability of weighted synchronization under partial observability. CONCUR: Concurrency Theory, LIPIcs, vol. 42, 142–154.","ama":"Kretinsky J, Larsen K, Laursen S, Srba J. Polynomial time decidability of weighted synchronization under partial observability. In: Vol 42. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2015:142-154. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2015.142\">10.4230/LIPIcs.CONCUR.2015.142</a>","mla":"Kretinsky, Jan, et al. <i>Polynomial Time Decidability of Weighted Synchronization under Partial Observability</i>. Vol. 42, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pp. 142–54, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2015.142\">10.4230/LIPIcs.CONCUR.2015.142</a>.","short":"J. Kretinsky, K. Larsen, S. Laursen, J. Srba, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pp. 142–154.","chicago":"Kretinsky, Jan, Kim Larsen, Simon Laursen, and Jiří Srba. “Polynomial Time Decidability of Weighted Synchronization under Partial Observability,” 42:142–54. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2015.142\">https://doi.org/10.4230/LIPIcs.CONCUR.2015.142</a>."},"language":[{"iso":"eng"}],"abstract":[{"text":"We consider weighted automata with both positive and negative integer weights on edges and\r\nstudy the problem of synchronization using adaptive strategies that may only observe whether\r\nthe current weight-level is negative or nonnegative. We show that the synchronization problem is decidable in polynomial time for deterministic weighted automata.","lang":"eng"}],"has_accepted_license":"1","status":"public","publist_id":"5680","scopus_import":1,"oa_version":"Published Version","date_created":"2018-12-11T11:52:22Z","type":"conference"},{"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Chmelik","first_name":"Martin","full_name":"Chmelik, Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"id":"49351290-F248-11E8-B48F-1D18A9856A87","full_name":"Daca, Przemyslaw","last_name":"Daca","first_name":"Przemyslaw"}],"page":"230 - 264","year":"2015","publication_status":"published","volume":47,"issue":"2","related_material":{"record":[{"status":"public","id":"1155","relation":"dissertation_contains"}]},"month":"10","main_file_link":[{"url":"https://arxiv.org/abs/1405.0835","open_access":"1"}],"corr_author":"1","type":"journal_article","publist_id":"5677","scopus_import":"1","date_created":"2018-12-11T11:52:23Z","publication":"Formal Methods in System Design","oa_version":"Preprint","status":"public","external_id":{"isi":["000361752300003"],"arxiv":["1405.0835"]},"abstract":[{"text":"We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems. We focus on qualitative properties for MDPs that can express that desired behaviors of the system arise almost-surely (with probability 1) or with positive probability. We introduce a new simulation relation to capture the refinement relation of MDPs with respect to qualitative properties, and present discrete graph algorithms with quadratic complexity to compute the simulation relation. We present an automated technique for assume-guarantee style reasoning for compositional analysis of two-player games by giving a counterexample guided abstraction-refinement approach to compute our new simulation relation. We show a tight link between two-player games and MDPs, and as a consequence the results for games are lifted to MDPs with qualitative properties. We have implemented our algorithms and show that the compositional analysis leads to significant improvements. ","lang":"eng"}],"language":[{"iso":"eng"}],"ec_funded":1,"citation":{"chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Przemyslaw Daca. “CEGAR for Compositional Analysis of Qualitative Properties in Markov Decision Processes.” <i>Formal Methods in System Design</i>. Springer, 2015. <a href=\"https://doi.org/10.1007/s10703-015-0235-2\">https://doi.org/10.1007/s10703-015-0235-2</a>.","apa":"Chatterjee, K., Chmelik, M., &#38; Daca, P. (2015). CEGAR for compositional analysis of qualitative properties in Markov decision processes. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1007/s10703-015-0235-2\">https://doi.org/10.1007/s10703-015-0235-2</a>","ista":"Chatterjee K, Chmelik M, Daca P. 2015. CEGAR for compositional analysis of qualitative properties in Markov decision processes. Formal Methods in System Design. 47(2), 230–264.","ama":"Chatterjee K, Chmelik M, Daca P. CEGAR for compositional analysis of qualitative properties in Markov decision processes. <i>Formal Methods in System Design</i>. 2015;47(2):230-264. doi:<a href=\"https://doi.org/10.1007/s10703-015-0235-2\">10.1007/s10703-015-0235-2</a>","ieee":"K. Chatterjee, M. Chmelik, and P. Daca, “CEGAR for compositional analysis of qualitative properties in Markov decision processes,” <i>Formal Methods in System Design</i>, vol. 47, no. 2. Springer, pp. 230–264, 2015.","mla":"Chatterjee, Krishnendu, et al. “CEGAR for Compositional Analysis of Qualitative Properties in Markov Decision Processes.” <i>Formal Methods in System Design</i>, vol. 47, no. 2, Springer, 2015, pp. 230–64, doi:<a href=\"https://doi.org/10.1007/s10703-015-0235-2\">10.1007/s10703-015-0235-2</a>.","short":"K. Chatterjee, M. Chmelik, P. Daca, Formal Methods in System Design 47 (2015) 230–264."},"intvolume":"        47","arxiv":1,"date_updated":"2026-04-15T10:02:12Z","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","grant_number":"267989"}],"article_processing_charge":"No","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","title":"CEGAR for compositional analysis of qualitative properties in Markov decision processes","oa":1,"day":"01","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"date_published":"2015-10-01T00:00:00Z","_id":"1501","quality_controlled":"1","isi":1,"acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No. P23499- N23, FWF NFN Grant No. S11407-N23, FWF Grant S11403-N23 (RiSE), and FWF Grant Z211-N23 (Wittgenstein Award), ERC Start Grant (279307: Graph Games), Microsoft faculty fellows award, the ERC Advanced Grant QUAREM (Quantitative Reactive Modeling).","doi":"10.1007/s10703-015-0235-2","publisher":"Springer"},{"related_material":{"record":[{"status":"public","id":"1155","relation":"dissertation_contains"}]},"month":"05","year":"2015","publication_status":"published","file_date_updated":"2020-07-14T12:44:59Z","page":"101 - 110","alternative_title":["Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering "],"author":[{"full_name":"Beneš, Nikola","last_name":"Beneš","first_name":"Nikola"},{"full_name":"Daca, Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87","first_name":"Przemyslaw","last_name":"Daca"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky","orcid":"0000-0002-8122-2881","first_name":"Jan"},{"last_name":"Nickovic","first_name":"Dejan","full_name":"Nickovic, Dejan"}],"project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"grant_number":"Z211","name":"Formal methods for the design and analysis of complex systems","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"grant_number":"291734","call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425"}],"ddc":["000"],"pubrep_id":"625","date_updated":"2026-04-15T10:02:12Z","language":[{"iso":"eng"}],"citation":{"chicago":"Beneš, Nikola, Przemyslaw Daca, Thomas A Henzinger, Jan Kretinsky, and Dejan Nickovic. “Complete Composition Operators for IOCO-Testing Theory,” 101–10. ACM, 2015. <a href=\"https://doi.org/10.1145/2737166.2737175\">https://doi.org/10.1145/2737166.2737175</a>.","ista":"Beneš N, Daca P, Henzinger TA, Kretinsky J, Nickovic D. 2015. Complete composition operators for IOCO-testing theory. CBSE: Component-Based Software Engineering , Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering , , 101–110.","ama":"Beneš N, Daca P, Henzinger TA, Kretinsky J, Nickovic D. Complete composition operators for IOCO-testing theory. In: ACM; 2015:101-110. doi:<a href=\"https://doi.org/10.1145/2737166.2737175\">10.1145/2737166.2737175</a>","ieee":"N. Beneš, P. Daca, T. A. Henzinger, J. Kretinsky, and D. Nickovic, “Complete composition operators for IOCO-testing theory,” presented at the CBSE: Component-Based Software Engineering , Montreal, QC, Canada, 2015, pp. 101–110.","apa":"Beneš, N., Daca, P., Henzinger, T. A., Kretinsky, J., &#38; Nickovic, D. (2015). Complete composition operators for IOCO-testing theory (pp. 101–110). Presented at the CBSE: Component-Based Software Engineering , Montreal, QC, Canada: ACM. <a href=\"https://doi.org/10.1145/2737166.2737175\">https://doi.org/10.1145/2737166.2737175</a>","short":"N. Beneš, P. Daca, T.A. Henzinger, J. Kretinsky, D. Nickovic, in:, ACM, 2015, pp. 101–110.","mla":"Beneš, Nikola, et al. <i>Complete Composition Operators for IOCO-Testing Theory</i>. ACM, 2015, pp. 101–10, doi:<a href=\"https://doi.org/10.1145/2737166.2737175\">10.1145/2737166.2737175</a>."},"ec_funded":1,"type":"conference","oa_version":"Submitted Version","scopus_import":"1","publist_id":"5676","date_created":"2018-12-11T11:52:24Z","status":"public","external_id":{"isi":["000380554800013"]},"has_accepted_license":"1","abstract":[{"lang":"eng","text":"We extend the theory of input-output conformance with operators for merge and quotient. The former is useful when testing against multiple requirements or views. The latter can be used to generate tests for patches of an already tested system. Both operators can combine systems with different action alphabets, which is usually the case when constructing complex systems and specifications from parts, for instance different views as well as newly defined functionality of a~previous version of the system."}],"day":"01","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","title":"Complete composition operators for IOCO-testing theory","oa":1,"article_processing_charge":"No","publication_identifier":{"isbn":["978-1-4503-3471-6"]},"doi":"10.1145/2737166.2737175","isi":1,"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 (Wittgestein Award), by People Programme (Marie Curie Actions) of the European Union's Seventh Framework Programme (FP7/2007-2013) under REA grant agreement 291734, and by the ARTEMIS JU under grant agreement 295373 (nSafeCer).  Jan Křetínský has been partially supported by the Czech Science Foundation, grant No.  P202/12/G061.  Nikola Beneš has been supported by the\r\nMEYS project No. CZ.1.07/2.3.00/30.0009 Employment of Newly Graduated Doctors of Science for Scientific Excellence.","file":[{"date_created":"2018-12-12T10:17:46Z","content_type":"application/pdf","access_level":"open_access","relation":"main_file","creator":"system","date_updated":"2020-07-14T12:44:59Z","file_name":"IST-2016-625-v1+1_conf-cbse-BenesDHKN15.pdf","file_id":"5303","checksum":"c6ce681035c163a158751f240cb7d389","file_size":467561}],"publisher":"ACM","conference":{"start_date":"2015-05-04","location":"Montreal, QC, Canada","end_date":"2015-05-08","name":"CBSE: Component-Based Software Engineering "},"date_published":"2015-05-01T00:00:00Z","_id":"1502","quality_controlled":"1"},{"article_processing_charge":"No","day":"22","department":[{"_id":"KrCh"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","title":"Computational complexity of ecological and evolutionary spatial dynamics","oa":1,"_id":"1559","date_published":"2015-12-22T00:00:00Z","quality_controlled":"1","isi":1,"doi":"10.1073/pnas.1511366112","publisher":"National Academy of Sciences","pmid":1,"page":"15636 - 15641","author":[{"last_name":"Ibsen-Jensen","first_name":"Rasmus","orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus"},{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"last_name":"Nowak","first_name":"Martin","full_name":"Nowak, Martin"}],"volume":112,"issue":"51","month":"12","year":"2015","publication_status":"published","language":[{"iso":"eng"}],"citation":{"ista":"Ibsen-Jensen R, Chatterjee K, Nowak M. 2015. Computational complexity of ecological and evolutionary spatial dynamics. PNAS. 112(51), 15636–15641.","ama":"Ibsen-Jensen R, Chatterjee K, Nowak M. Computational complexity of ecological and evolutionary spatial dynamics. <i>PNAS</i>. 2015;112(51):15636-15641. doi:<a href=\"https://doi.org/10.1073/pnas.1511366112\">10.1073/pnas.1511366112</a>","ieee":"R. Ibsen-Jensen, K. Chatterjee, and M. Nowak, “Computational complexity of ecological and evolutionary spatial dynamics,” <i>PNAS</i>, vol. 112, no. 51. National Academy of Sciences, pp. 15636–15641, 2015.","apa":"Ibsen-Jensen, R., Chatterjee, K., &#38; Nowak, M. (2015). Computational complexity of ecological and evolutionary spatial dynamics. <i>PNAS</i>. National Academy of Sciences. <a href=\"https://doi.org/10.1073/pnas.1511366112\">https://doi.org/10.1073/pnas.1511366112</a>","short":"R. Ibsen-Jensen, K. Chatterjee, M. Nowak, PNAS 112 (2015) 15636–15641.","mla":"Ibsen-Jensen, Rasmus, et al. “Computational Complexity of Ecological and Evolutionary Spatial Dynamics.” <i>PNAS</i>, vol. 112, no. 51, National Academy of Sciences, 2015, pp. 15636–41, doi:<a href=\"https://doi.org/10.1073/pnas.1511366112\">10.1073/pnas.1511366112</a>.","chicago":"Ibsen-Jensen, Rasmus, Krishnendu Chatterjee, and Martin Nowak. “Computational Complexity of Ecological and Evolutionary Spatial Dynamics.” <i>PNAS</i>. National Academy of Sciences, 2015. <a href=\"https://doi.org/10.1073/pnas.1511366112\">https://doi.org/10.1073/pnas.1511366112</a>."},"main_file_link":[{"open_access":"1","url":"http://www.ncbi.nlm.nih.gov/pmc/articles/PMC4697423/"}],"type":"journal_article","corr_author":"1","publication":"PNAS","date_created":"2018-12-11T11:52:43Z","publist_id":"5612","scopus_import":"1","oa_version":"Submitted Version","external_id":{"pmid":["26644569"],"isi":["000366916000044"]},"status":"public","abstract":[{"text":"There are deep, yet largely unexplored, connections between computer science and biology. Both disciplines examine how information proliferates in time and space. Central results in computer science describe the complexity of algorithms that solve certain classes of problems. An algorithm is deemed efficient if it can solve a problem in polynomial time, which means the running time of the algorithm is a polynomial function of the length of the input. There are classes of harder problems for which the fastest possible algorithm requires exponential time. Another criterion is the space requirement of the algorithm. There is a crucial distinction between algorithms that can find a solution, verify a solution, or list several distinct solutions in given time and space. The complexity hierarchy that is generated in this way is the foundation of theoretical computer science. Precise complexity results can be notoriously difficult. The famous question whether polynomial time equals nondeterministic polynomial time (i.e., P = NP) is one of the hardest open problems in computer science and all of mathematics. Here, we consider simple processes of ecological and evolutionary spatial dynamics. The basic question is: What is the probability that a new invader (or a new mutant)will take over a resident population?We derive precise complexity results for a variety of scenarios. We therefore show that some fundamental questions in this area cannot be answered by simple equations (assuming that P is not equal to NP).","lang":"eng"}],"intvolume":"       112","date_updated":"2025-09-23T08:20:08Z"},{"volume":9450,"month":"11","year":"2015","publication_status":"published","page":"162 - 177","alternative_title":["LNCS"],"author":[{"last_name":"Forejt","first_name":"Vojtěch","full_name":"Forejt, Vojtěch"},{"full_name":"Krčál, Jan","first_name":"Jan","last_name":"Krčál"},{"first_name":"Jan","orcid":"0000-0002-8122-2881","last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","full_name":"Kretinsky, Jan"}],"project":[{"_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","grant_number":"291734"},{"grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"}],"intvolume":"      9450","date_updated":"2025-09-23T08:21:59Z","citation":{"ista":"Forejt V, Krčál J, Kretinsky J. 2015. Controller synthesis for MDPs and frequency LTL\\GU. LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, LNCS, vol. 9450, 162–177.","ieee":"V. Forejt, J. Krčál, and J. Kretinsky, “Controller synthesis for MDPs and frequency LTL\\GU,” presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Suva, Fiji, 2015, vol. 9450, pp. 162–177.","ama":"Forejt V, Krčál J, Kretinsky J. Controller synthesis for MDPs and frequency LTL\\GU. In: Vol 9450. Springer; 2015:162-177. doi:<a href=\"https://doi.org/10.1007/978-3-662-48899-7_12\">10.1007/978-3-662-48899-7_12</a>","apa":"Forejt, V., Krčál, J., &#38; Kretinsky, J. (2015). Controller synthesis for MDPs and frequency LTL\\GU (Vol. 9450, pp. 162–177). Presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Suva, Fiji: Springer. <a href=\"https://doi.org/10.1007/978-3-662-48899-7_12\">https://doi.org/10.1007/978-3-662-48899-7_12</a>","short":"V. Forejt, J. Krčál, J. Kretinsky, in:, Springer, 2015, pp. 162–177.","mla":"Forejt, Vojtěch, et al. <i>Controller Synthesis for MDPs and Frequency LTL\\GU</i>. Vol. 9450, Springer, 2015, pp. 162–77, doi:<a href=\"https://doi.org/10.1007/978-3-662-48899-7_12\">10.1007/978-3-662-48899-7_12</a>.","chicago":"Forejt, Vojtěch, Jan Krčál, and Jan Kretinsky. “Controller Synthesis for MDPs and Frequency LTL\\GU,” 9450:162–77. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-662-48899-7_12\">https://doi.org/10.1007/978-3-662-48899-7_12</a>."},"ec_funded":1,"language":[{"iso":"eng"}],"publist_id":"5577","oa_version":"None","date_created":"2018-12-11T11:52:55Z","scopus_import":"1","type":"conference","abstract":[{"text":"Quantitative extensions of temporal logics have recently attracted significant attention. In this work, we study frequency LTL (fLTL), an extension of LTL which allows to speak about frequencies of events along an execution. Such an extension is particularly useful for probabilistic systems that often cannot fulfil strict qualitative guarantees on the behaviour. It has been recently shown that controller synthesis for Markov decision processes and fLTL is decidable when all the bounds on frequencies are 1. As a step towards a complete quantitative solution, we show that the problem is decidable for the fragment fLTL\\GU, where U does not occur in the scope of G (but still F can). Our solution is based on a novel translation of such quantitative formulae into equivalent deterministic automata.","lang":"eng"}],"status":"public","external_id":{"isi":["000375574900012"]},"day":"22","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","title":"Controller synthesis for MDPs and frequency LTL\\GU","article_processing_charge":"No","doi":"10.1007/978-3-662-48899-7_12","acknowledgement":"This work is partly supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center AVACS (SFB/TR 14), by the Czech Science Foundation under grant agreement P202/12/G061, by the EU 7th Framework Programme under grant agreement no. 295261 (MEALS) and 318490 (SENSATION), by the CDZ project 1023 (CAP), by the CAS/SAFEA International Partnership Program for Creative Research Teams, by the EPSRC grant EP/M023656/1, by the People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007–2013) REA Grant No 291734, by the Austrian Science Fund (FWF) S11407-N23 (RiSE/SHiNE), and by the ERC Start Grant (279307: Graph Games).\r\n","isi":1,"publisher":"Springer","conference":{"end_date":"2015-11-28","start_date":"2015-11-24","location":"Suva, Fiji","name":"LPAR: Logic for Programming, Artificial Intelligence, and Reasoning"},"quality_controlled":"1","_id":"1594","date_published":"2015-11-22T00:00:00Z"},{"day":"30","department":[{"_id":"KrCh"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","oa":1,"title":"Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives","article_processing_charge":"No","doi":"10.1016/j.tcs.2015.01.050","acknowledgement":"The research was supported by FWF Grant No. P 23499-N23, FWF NFN Grant No. S11407-N23 (RiSE), ERC Start Grant (279307: Graph Games), and the Microsoft Faculty Fellows Award. Nisarg Shah is also supported by NSF Grant CCF-1215883.\r\n","isi":1,"publisher":"Elsevier","quality_controlled":"1","_id":"1598","date_published":"2015-03-30T00:00:00Z","issue":"3","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"2715"}]},"volume":573,"month":"03","year":"2015","publication_status":"published","page":"71 - 89","author":[{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Joglekar, Manas","last_name":"Joglekar","first_name":"Manas"},{"first_name":"Nisarg","last_name":"Shah","full_name":"Shah, Nisarg"}],"project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"intvolume":"       573","date_updated":"2025-09-23T08:00:31Z","arxiv":1,"citation":{"chicago":"Chatterjee, Krishnendu, Manas Joglekar, and Nisarg Shah. “Average Case Analysis of the Classical Algorithm for Markov Decision Processes with Büchi Objectives.” <i>Theoretical Computer Science</i>. Elsevier, 2015. <a href=\"https://doi.org/10.1016/j.tcs.2015.01.050\">https://doi.org/10.1016/j.tcs.2015.01.050</a>.","short":"K. Chatterjee, M. Joglekar, N. Shah, Theoretical Computer Science 573 (2015) 71–89.","mla":"Chatterjee, Krishnendu, et al. “Average Case Analysis of the Classical Algorithm for Markov Decision Processes with Büchi Objectives.” <i>Theoretical Computer Science</i>, vol. 573, no. 3, Elsevier, 2015, pp. 71–89, doi:<a href=\"https://doi.org/10.1016/j.tcs.2015.01.050\">10.1016/j.tcs.2015.01.050</a>.","ieee":"K. Chatterjee, M. Joglekar, and N. Shah, “Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives,” <i>Theoretical Computer Science</i>, vol. 573, no. 3. Elsevier, pp. 71–89, 2015.","ama":"Chatterjee K, Joglekar M, Shah N. Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives. <i>Theoretical Computer Science</i>. 2015;573(3):71-89. doi:<a href=\"https://doi.org/10.1016/j.tcs.2015.01.050\">10.1016/j.tcs.2015.01.050</a>","ista":"Chatterjee K, Joglekar M, Shah N. 2015. Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives. Theoretical Computer Science. 573(3), 71–89.","apa":"Chatterjee, K., Joglekar, M., &#38; Shah, N. (2015). Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2015.01.050\">https://doi.org/10.1016/j.tcs.2015.01.050</a>"},"ec_funded":1,"language":[{"iso":"eng"}],"publication":"Theoretical Computer Science","oa_version":"Preprint","publist_id":"5571","date_created":"2018-12-11T11:52:56Z","scopus_import":"1","type":"journal_article","main_file_link":[{"url":"http://arxiv.org/abs/1202.4175","open_access":"1"}],"abstract":[{"text":"We consider Markov decision processes (MDPs) with specifications given as Büchi (liveness) objectives, and examine the problem of computing the set of almost-sure winning vertices such that the objective can be ensured with probability 1 from these vertices. We study for the first time the average-case complexity of the classical algorithm for computing the set of almost-sure winning vertices for MDPs with Büchi objectives. Our contributions are as follows: First, we show that for MDPs with constant out-degree the expected number of iterations is at most logarithmic and the average-case running time is linear (as compared to the worst-case linear number of iterations and quadratic time complexity). Second, for the average-case analysis over all MDPs we show that the expected number of iterations is constant and the average-case running time is linear (again as compared to the worst-case linear number of iterations and quadratic time complexity). Finally we also show that when all MDPs are equally likely, the probability that the classical algorithm requires more than a constant number of iterations is exponentially small.","lang":"eng"}],"status":"public","external_id":{"arxiv":["1202.4175"],"isi":["000350835500007"]}},{"conference":{"name":"CAV: Computer Aided Verification","start_date":"2015-07-18","location":"San Francisco, CA, United States","end_date":"2015-07-24"},"doi":"10.1007/978-3-319-21690-4_31","isi":1,"file":[{"file_size":1651779,"checksum":"5885236fa88a439baba9ac6f3e801e93","date_updated":"2020-07-14T12:45:04Z","file_id":"7850","file_name":"2015_CAV_Babiak.pdf","relation":"main_file","creator":"dernst","access_level":"open_access","date_created":"2020-05-15T08:38:12Z","content_type":"application/pdf"}],"publisher":"Springer","date_published":"2015-07-16T00:00:00Z","_id":"1601","quality_controlled":"1","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","oa":1,"title":"The Hanoi omega-automata format","day":"16","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"article_processing_charge":"No","intvolume":"      9206","date_updated":"2025-09-23T13:50:55Z","ddc":["000"],"project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211"},{"grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme"},{"grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"}],"date_created":"2018-12-11T11:52:57Z","scopus_import":"1","oa_version":"Submitted Version","publist_id":"5566","type":"conference","abstract":[{"text":"We propose a flexible exchange format for ω-automata, as typically used in formal verification, and implement support for it in a range of established tools. Our aim is to simplify the interaction of tools, helping the research community to build upon other people’s work. A key feature of the format is the use of very generic acceptance conditions, specified by Boolean combinations of acceptance primitives, rather than being limited to common cases such as Büchi, Streett, or Rabin. Such flexibility in the choice of acceptance conditions can be exploited in applications, for example in probabilistic model checking, and furthermore encourages the development of acceptance-agnostic tools for automata manipulations. The format allows acceptance conditions that are either state-based or transition-based, and also supports alternating automata.","lang":"eng"}],"status":"public","external_id":{"isi":["000364182900031"]},"has_accepted_license":"1","ec_funded":1,"citation":{"chicago":"Babiak, Tomáš, František Blahoudek, Alexandre Duret Lutz, Joachim Klein, Jan Kretinsky, Daniel Mueller, David Parker, and Jan Strejček. “The Hanoi Omega-Automata Format,” 9206:479–86. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_31\">https://doi.org/10.1007/978-3-319-21690-4_31</a>.","apa":"Babiak, T., Blahoudek, F., Duret Lutz, A., Klein, J., Kretinsky, J., Mueller, D., … Strejček, J. (2015). The Hanoi omega-automata format (Vol. 9206, pp. 479–486). Presented at the CAV: Computer Aided Verification, San Francisco, CA, United States: Springer. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_31\">https://doi.org/10.1007/978-3-319-21690-4_31</a>","ista":"Babiak T, Blahoudek F, Duret Lutz A, Klein J, Kretinsky J, Mueller D, Parker D, Strejček J. 2015. The Hanoi omega-automata format. CAV: Computer Aided Verification, LNCS, vol. 9206, 479–486.","ieee":"T. Babiak <i>et al.</i>, “The Hanoi omega-automata format,” presented at the CAV: Computer Aided Verification, San Francisco, CA, United States, 2015, vol. 9206, pp. 479–486.","ama":"Babiak T, Blahoudek F, Duret Lutz A, et al. The Hanoi omega-automata format. In: Vol 9206. Springer; 2015:479-486. doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_31\">10.1007/978-3-319-21690-4_31</a>","mla":"Babiak, Tomáš, et al. <i>The Hanoi Omega-Automata Format</i>. Vol. 9206, Springer, 2015, pp. 479–86, doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_31\">10.1007/978-3-319-21690-4_31</a>.","short":"T. Babiak, F. Blahoudek, A. Duret Lutz, J. Klein, J. Kretinsky, D. Mueller, D. Parker, J. Strejček, in:, Springer, 2015, pp. 479–486."},"language":[{"iso":"eng"}],"year":"2015","file_date_updated":"2020-07-14T12:45:04Z","publication_status":"published","volume":9206,"month":"07","alternative_title":["LNCS"],"author":[{"full_name":"Babiak, Tomáš","first_name":"Tomáš","last_name":"Babiak"},{"last_name":"Blahoudek","first_name":"František","full_name":"Blahoudek, František"},{"first_name":"Alexandre","last_name":"Duret Lutz","full_name":"Duret Lutz, Alexandre"},{"full_name":"Klein, Joachim","first_name":"Joachim","last_name":"Klein"},{"full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8122-2881","first_name":"Jan","last_name":"Kretinsky"},{"first_name":"Daniel","last_name":"Mueller","full_name":"Mueller, Daniel"},{"full_name":"Parker, David","last_name":"Parker","first_name":"David"},{"last_name":"Strejček","first_name":"Jan","full_name":"Strejček, Jan"}],"page":"479 - 486"},{"author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen"},{"full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","first_name":"Andreas"},{"first_name":"Prateesh","last_name":"Goyal","full_name":"Goyal, Prateesh"}],"page":"97 - 109","year":"2015","publication_status":"published","volume":50,"issue":"1","related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"821"}]},"month":"01","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1410.7724"}],"type":"journal_article","publist_id":"5565","publication":"ACM SIGPLAN Notices","date_created":"2018-12-11T11:52:58Z","oa_version":"Preprint","scopus_import":1,"status":"public","external_id":{"arxiv":["1410.7724"]},"abstract":[{"lang":"eng","text":"Interprocedural analysis is at the heart of numerous applications in programming languages, such as alias analysis, constant propagation, etc. Recursive state machines (RSMs) are standard models for interprocedural analysis. We consider a general framework with RSMs where the transitions are labeled from a semiring, and path properties are algebraic with semiring operations. RSMs with algebraic path properties can model interprocedural dataflow analysis problems, the shortest path problem, the most probable path problem, etc. The traditional algorithms for interprocedural analysis focus on path properties where the starting point is fixed as the entry point of a specific method. In this work, we consider possible multiple queries as required in many applications such as in alias analysis. The study of multiple queries allows us to bring in a very important algorithmic distinction between the resource usage of the one-time preprocessing vs for each individual query. The second aspect that we consider is that the control flow graphs for most programs have constant treewidth. Our main contributions are simple and implementable algorithms that supportmultiple queries for algebraic path properties for RSMs that have constant treewidth. Our theoretical results show that our algorithms have small additional one-time preprocessing, but can answer subsequent queries significantly faster as compared to the current best-known solutions for several important problems, such as interprocedural reachability and shortest path. We provide a prototype implementation for interprocedural reachability and intraprocedural shortest path that gives a significant speed-up on several benchmarks."}],"language":[{"iso":"eng"}],"ec_funded":1,"citation":{"apa":"Chatterjee, K., Ibsen-Jensen, R., Pavlogiannis, A., &#38; Goyal, P. (2015). Faster algorithms for algebraic path properties in recursive state machines with constant treewidth. <i>ACM SIGPLAN Notices</i>. Mumbai, India: ACM. <a href=\"https://doi.org/10.1145/2676726.2676979\">https://doi.org/10.1145/2676726.2676979</a>","ieee":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, and P. Goyal, “Faster algorithms for algebraic path properties in recursive state machines with constant treewidth,” <i>ACM SIGPLAN Notices</i>, vol. 50, no. 1. ACM, pp. 97–109, 2015.","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A, Goyal P. Faster algorithms for algebraic path properties in recursive state machines with constant treewidth. <i>ACM SIGPLAN Notices</i>. 2015;50(1):97-109. doi:<a href=\"https://doi.org/10.1145/2676726.2676979\">10.1145/2676726.2676979</a>","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A, Goyal P. 2015. Faster algorithms for algebraic path properties in recursive state machines with constant treewidth. ACM SIGPLAN Notices. 50(1), 97–109.","mla":"Chatterjee, Krishnendu, et al. “Faster Algorithms for Algebraic Path Properties in Recursive State Machines with Constant Treewidth.” <i>ACM SIGPLAN Notices</i>, vol. 50, no. 1, ACM, 2015, pp. 97–109, doi:<a href=\"https://doi.org/10.1145/2676726.2676979\">10.1145/2676726.2676979</a>.","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, P. Goyal, ACM SIGPLAN Notices 50 (2015) 97–109.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Andreas Pavlogiannis, and Prateesh Goyal. “Faster Algorithms for Algebraic Path Properties in Recursive State Machines with Constant Treewidth.” <i>ACM SIGPLAN Notices</i>. ACM, 2015. <a href=\"https://doi.org/10.1145/2676726.2676979\">https://doi.org/10.1145/2676726.2676979</a>."},"intvolume":"        50","arxiv":1,"date_updated":"2026-04-08T14:22:16Z","project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Faster algorithms for algebraic path properties in recursive state machines with constant treewidth","oa":1,"day":"01","department":[{"_id":"KrCh"}],"date_published":"2015-01-01T00:00:00Z","_id":"1602","quality_controlled":"1","conference":{"name":"SIGPLAN: Symposium on Principles of Programming Languages","end_date":"2015-01-17","start_date":"2015-01-15","location":"Mumbai, India"},"doi":"10.1145/2676726.2676979","acknowledgement":"We thank anonymous reviewers for helpful comments to improve the presentation of the paper.","publisher":"ACM"},{"_id":"1603","quality_controlled":"1","date_published":"2015-07-16T00:00:00Z","publisher":"Springer","isi":1,"acknowledgement":"This research was funded in part by Austrian Science Fund (FWF) Grant No P 23499-N23, FWF NFN Grant No S11407-N23 (RiSE) and Z211-N23 (Wittgenstein Award), European Research Council (ERC) Grant No 279307 (Graph Games), ERC Grant No 267989 (QUAREM), the Czech Science Foundation Grant No P202/12/G061, and People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007–2013) REA Grant No 291734.","doi":"10.1007/978-3-319-21690-4_10","conference":{"name":"CAV: Computer Aided Verification","start_date":"2015-07-18","location":"San Francisco, CA, United States","end_date":"2015-07-24"},"publication_identifier":{"eisbn":["978-3-319-21690-4"]},"article_processing_charge":"No","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"day":"16","oa":1,"title":"Counterexample explanation by learning small strategies in Markov decision processes","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","ec_funded":1,"citation":{"apa":"Brázdil, T., Chatterjee, K., Chmelik, M., Fellner, A., &#38; Kretinsky, J. (2015). Counterexample explanation by learning small strategies in Markov decision processes (Vol. 9206, pp. 158–177). Presented at the CAV: Computer Aided Verification, San Francisco, CA, United States: Springer. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_10\">https://doi.org/10.1007/978-3-319-21690-4_10</a>","ieee":"T. Brázdil, K. Chatterjee, M. Chmelik, A. Fellner, and J. Kretinsky, “Counterexample explanation by learning small strategies in Markov decision processes,” presented at the CAV: Computer Aided Verification, San Francisco, CA, United States, 2015, vol. 9206, pp. 158–177.","ama":"Brázdil T, Chatterjee K, Chmelik M, Fellner A, Kretinsky J. Counterexample explanation by learning small strategies in Markov decision processes. In: Vol 9206. Springer; 2015:158-177. doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_10\">10.1007/978-3-319-21690-4_10</a>","ista":"Brázdil T, Chatterjee K, Chmelik M, Fellner A, Kretinsky J. 2015. Counterexample explanation by learning small strategies in Markov decision processes. CAV: Computer Aided Verification, LNCS, vol. 9206, 158–177.","mla":"Brázdil, Tomáš, et al. <i>Counterexample Explanation by Learning Small Strategies in Markov Decision Processes</i>. Vol. 9206, Springer, 2015, pp. 158–77, doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_10\">10.1007/978-3-319-21690-4_10</a>.","short":"T. Brázdil, K. Chatterjee, M. Chmelik, A. Fellner, J. Kretinsky, in:, Springer, 2015, pp. 158–177.","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Andreas Fellner, and Jan Kretinsky. “Counterexample Explanation by Learning Small Strategies in Markov Decision Processes,” 9206:158–77. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_10\">https://doi.org/10.1007/978-3-319-21690-4_10</a>."},"language":[{"iso":"eng"}],"abstract":[{"lang":"eng","text":"For deterministic systems, a counterexample to a property can simply be an error trace, whereas counterexamples in probabilistic systems are necessarily more complex. For instance, a set of erroneous traces with a sufficient cumulative probability mass can be used. Since these are too large objects to understand and manipulate, compact representations such as subchains have been considered. In the case of probabilistic systems with non-determinism, the situation is even more complex. While a subchain for a given strategy (or scheduler, resolving non-determinism) is a straightforward choice, we take a different approach. Instead, we focus on the strategy itself, and extract the most important decisions it makes, and present its succinct representation.\r\nThe key tools we employ to achieve this are (1) introducing a concept of importance of a state w.r.t. the strategy, and (2) learning using decision trees. There are three main consequent advantages of our approach. Firstly, it exploits the quantitative information on states, stressing the more important decisions. Secondly, it leads to a greater variability and degree of freedom in representing the strategies. Thirdly, the representation uses a self-explanatory data structure. In summary, our approach produces more succinct and more explainable strategies, as opposed to e.g. binary decision diagrams. Finally, our experimental results show that we can extract several rules describing the strategy even for very large systems that do not fit in memory, and based on the rules explain the erroneous behaviour."}],"status":"public","external_id":{"isi":["000364182900010"],"arxiv":["1502.02834"]},"oa_version":"Preprint","date_created":"2018-12-11T11:52:58Z","publist_id":"5564","scopus_import":"1","corr_author":"1","type":"conference","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1502.02834"}],"project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling"},{"name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"291734"}],"date_updated":"2025-09-23T08:23:16Z","arxiv":1,"intvolume":"      9206","page":"158 - 177","author":[{"first_name":"Tomáš","last_name":"Brázdil","full_name":"Brázdil, Tomáš"},{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"id":"3624234E-F248-11E8-B48F-1D18A9856A87","full_name":"Chmelik, Martin","first_name":"Martin","last_name":"Chmelik"},{"id":"42BABFB4-F248-11E8-B48F-1D18A9856A87","full_name":"Fellner, Andreas","last_name":"Fellner","first_name":"Andreas"},{"full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky","orcid":"0000-0002-8122-2881","first_name":"Jan"}],"alternative_title":["LNCS"],"month":"07","related_material":{"record":[{"relation":"research_paper","id":"5549","status":"public"}]},"volume":9206,"publication_status":"published","year":"2015"},{"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"}],"status":"public","publist_id":"5563","scopus_import":1,"oa_version":"None","publication":"Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT ","date_created":"2018-12-11T11:52:59Z","type":"journal_article","corr_author":"1","ec_funded":1,"citation":{"ama":"Chatterjee K, Pavlogiannis A, Velner Y. Quantitative interprocedural analysis. <i>Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT </i>. 2015;50(1):539-551. doi:<a href=\"https://doi.org/10.1145/2676726.2676968\">10.1145/2676726.2676968</a>","ieee":"K. Chatterjee, A. Pavlogiannis, and Y. Velner, “Quantitative interprocedural analysis,” <i>Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT </i>, vol. 50, no. 1. ACM, pp. 539–551, 2015.","ista":"Chatterjee K, Pavlogiannis A, Velner Y. 2015. Quantitative interprocedural analysis. Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT . 50(1), 539–551.","apa":"Chatterjee, K., Pavlogiannis, A., &#38; Velner, Y. (2015). Quantitative interprocedural analysis. <i>Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT </i>. Mumbai, India: ACM. <a href=\"https://doi.org/10.1145/2676726.2676968\">https://doi.org/10.1145/2676726.2676968</a>","short":"K. Chatterjee, A. Pavlogiannis, Y. Velner, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT  50 (2015) 539–551.","mla":"Chatterjee, Krishnendu, et al. “Quantitative Interprocedural Analysis.” <i>Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT </i>, vol. 50, no. 1, ACM, 2015, pp. 539–51, doi:<a href=\"https://doi.org/10.1145/2676726.2676968\">10.1145/2676726.2676968</a>.","chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, and Yaron Velner. “Quantitative Interprocedural Analysis.” <i>Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT </i>. ACM, 2015. <a href=\"https://doi.org/10.1145/2676726.2676968\">https://doi.org/10.1145/2676726.2676968</a>."},"language":[{"iso":"eng"}],"date_updated":"2026-04-08T14:22:16Z","pubrep_id":"523","intvolume":"        50","project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","first_name":"Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis"},{"full_name":"Velner, Yaron","last_name":"Velner","first_name":"Yaron"}],"page":"539 - 551","publication_status":"published","year":"2015","month":"01","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"5445"},{"relation":"dissertation_contains","status":"public","id":"821"}]},"issue":"1","volume":50,"quality_controlled":"1","_id":"1604","date_published":"2015-01-01T00:00:00Z","conference":{"start_date":"2015-01-15","location":"Mumbai, India","end_date":"2015-01-17","name":"SIGPLAN: Symposium on Principles of Programming Languages"},"publisher":"ACM","doi":"10.1145/2676726.2676968","publication_identifier":{"isbn":["978-1-4503-3300-9"]},"title":"Quantitative interprocedural analysis","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"KrCh"}],"day":"01"},{"article_processing_charge":"No","day":"16","department":[{"_id":"KrCh"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","title":"Faster algorithms for quantitative verification in constant treewidth graphs","oa":1,"date_published":"2015-07-16T00:00:00Z","_id":"1607","quality_controlled":"1","acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No P23499- N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.","isi":1,"doi":"10.1007/978-3-319-21690-4_9","publisher":"Springer","conference":{"name":"CAV: Computer Aided Verification","end_date":"2015-07-24","location":"San Francisco, CA, United States","start_date":"2015-07-18"},"page":"140 - 157","alternative_title":["LNCS"],"author":[{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389","first_name":"Rasmus"},{"last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","first_name":"Andreas","full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"}],"volume":9206,"related_material":{"record":[{"status":"public","id":"5430","relation":"earlier_version"},{"relation":"earlier_version","id":"5437","status":"public"},{"relation":"dissertation_contains","id":"821","status":"public"}]},"month":"07","year":"2015","publication_status":"published","language":[{"iso":"eng"}],"citation":{"ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Faster algorithms for quantitative verification in constant treewidth graphs,” presented at the CAV: Computer Aided Verification, San Francisco, CA, United States, 2015, vol. 9206, pp. 140–157.","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Faster algorithms for quantitative verification in constant treewidth graphs. In: Vol 9206. Springer; 2015:140-157. doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_9\">10.1007/978-3-319-21690-4_9</a>","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2015. Faster algorithms for quantitative verification in constant treewidth graphs. CAV: Computer Aided Verification, LNCS, vol. 9206, 140–157.","apa":"Chatterjee, K., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2015). Faster algorithms for quantitative verification in constant treewidth graphs (Vol. 9206, pp. 140–157). Presented at the CAV: Computer Aided Verification, San Francisco, CA, United States: Springer. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_9\">https://doi.org/10.1007/978-3-319-21690-4_9</a>","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, in:, Springer, 2015, pp. 140–157.","mla":"Chatterjee, Krishnendu, et al. <i>Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs</i>. Vol. 9206, Springer, 2015, pp. 140–57, doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_9\">10.1007/978-3-319-21690-4_9</a>.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs,” 9206:140–57. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_9\">https://doi.org/10.1007/978-3-319-21690-4_9</a>."},"ec_funded":1,"type":"conference","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1504.07384"}],"corr_author":"1","publist_id":"5560","date_created":"2018-12-11T11:52:59Z","scopus_import":"1","oa_version":"Preprint","status":"public","external_id":{"isi":["000364182900009"],"arxiv":["1504.07384"]},"abstract":[{"lang":"eng","text":"We consider the core algorithmic problems related to verification of systems with respect to three classical quantitative properties, namely, the mean-payoff property, the ratio property, and the minimum initial credit for energy property. The algorithmic problem given a graph and a quantitative property asks to compute the optimal value (the infimum value over all traces) from every node of the graph. We consider graphs with constant treewidth, and it is well-known that the control-flow graphs of most programs have constant treewidth. Let n denote the number of nodes of a graph, m the number of edges (for constant treewidth graphs m=O(n)) and W the largest absolute value of the weights. Our main theoretical results are as follows. First, for constant treewidth graphs we present an algorithm that approximates the mean-payoff value within a multiplicative factor of ϵ in time O(n⋅log(n/ϵ)) and linear space, as compared to the classical algorithms that require quadratic time. Second, for the ratio property we present an algorithm that for constant treewidth graphs works in time O(n⋅log(|a⋅b|))=O(n⋅log(n⋅W)), when the output is ab, as compared to the previously best known algorithm with running time O(n2⋅log(n⋅W)). Third, for the minimum initial credit problem we show that (i) for general graphs the problem can be solved in O(n2⋅m) time and the associated decision problem can be solved in O(n⋅m) time, improving the previous known O(n3⋅m⋅log(n⋅W)) and O(n2⋅m) bounds, respectively; and (ii) for constant treewidth graphs we present an algorithm that requires O(n⋅logn) time, improving the previous known O(n4⋅log(n⋅W)) bound. We have implemented some of our algorithms and show that they present a significant speedup on standard benchmarks."}],"project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"intvolume":"      9206","arxiv":1,"date_updated":"2026-04-08T14:22:16Z"},{"_id":"1609","quality_controlled":"1","date_published":"2015-06-20T00:00:00Z","conference":{"location":"Kyoto, Japan","start_date":"2015-07-06","end_date":"2015-07-10","name":"ICALP: Automata, Languages and Programming"},"doi":"10.1007/978-3-662-47666-6_9","acknowledgement":"This research was supported by Austrian Science Fund (FWF) Grant No P23499- N23, FWF NFN Grant No S11407-N23 (SHiNE), ERC Start grant (279307: Graph Games), EU FP7 Project Cassting, NSF grants CNS 1049862 and CCF-1139011, by NSF Expeditions in Computing project “ExCAPE: Expeditions in Computer Augmented Program Engineering”, by BSF grant 9800096, and by gift from Intel.","isi":1,"publisher":"Springer Nature","article_processing_charge":"No","publication_identifier":{"isbn":["978-3-662-47665-9"]},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","oa":1,"title":"The complexity of synthesis from probabilistic components","day":"20","department":[{"_id":"KrCh"}],"publist_id":"5557","oa_version":"Preprint","date_created":"2018-12-11T11:53:00Z","publication":"42nd International Colloquium","scopus_import":"1","corr_author":"1","main_file_link":[{"url":"http://arxiv.org/abs/1502.04844","open_access":"1"}],"type":"conference","abstract":[{"lang":"eng","text":"The synthesis problem asks for the automatic construction of a system from its specification. In the traditional setting, the system is “constructed from scratch” rather than composed from reusable components. However, this is rare in practice, and almost every non-trivial software system relies heavily on the use of libraries of reusable components. Recently, Lustig and Vardi introduced dataflow and controlflow synthesis from libraries of reusable components. They proved that dataflow synthesis is undecidable, while controlflow synthesis is decidable. The problem of controlflow synthesis from libraries of probabilistic components was considered by Nain, Lustig and Vardi, and was shown to be decidable for qualitative analysis (that asks that the specification be satisfied with probability 1). Our main contribution for controlflow synthesis from probabilistic components is to establish better complexity bounds for the qualitative analysis problem, and to show that the more general quantitative problem is undecidable. For the qualitative analysis, we show that the problem (i) is EXPTIME-complete when the specification is given as a deterministic parity word automaton, improving the previously known 2EXPTIME upper bound; and (ii) belongs to UP ∩ coUP and is parity-games hard, when the specification is given directly as a parity condition on the components, improving the previously known EXPTIME upper bound."}],"status":"public","external_id":{"arxiv":["1502.04844"],"isi":["000364317900009"]},"ec_funded":1,"citation":{"short":"K. Chatterjee, L. Doyen, M. Vardi, in:, 42nd International Colloquium, Springer Nature, 2015, pp. 108–120.","mla":"Chatterjee, Krishnendu, et al. “The Complexity of Synthesis from Probabilistic Components.” <i>42nd International Colloquium</i>, vol. 9135, Springer Nature, 2015, pp. 108–20, doi:<a href=\"https://doi.org/10.1007/978-3-662-47666-6_9\">10.1007/978-3-662-47666-6_9</a>.","ista":"Chatterjee K, Doyen L, Vardi M. 2015. The complexity of synthesis from probabilistic components. 42nd International Colloquium. ICALP: Automata, Languages and Programming, LNCS, vol. 9135, 108–120.","ieee":"K. Chatterjee, L. Doyen, and M. Vardi, “The complexity of synthesis from probabilistic components,” in <i>42nd International Colloquium</i>, Kyoto, Japan, 2015, vol. 9135, pp. 108–120.","ama":"Chatterjee K, Doyen L, Vardi M. The complexity of synthesis from probabilistic components. In: <i>42nd International Colloquium</i>. Vol 9135. Springer Nature; 2015:108-120. doi:<a href=\"https://doi.org/10.1007/978-3-662-47666-6_9\">10.1007/978-3-662-47666-6_9</a>","apa":"Chatterjee, K., Doyen, L., &#38; Vardi, M. (2015). The complexity of synthesis from probabilistic components. In <i>42nd International Colloquium</i> (Vol. 9135, pp. 108–120). Kyoto, Japan: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-662-47666-6_9\">https://doi.org/10.1007/978-3-662-47666-6_9</a>","chicago":"Chatterjee, Krishnendu, Laurent Doyen, and Moshe Vardi. “The Complexity of Synthesis from Probabilistic Components.” In <i>42nd International Colloquium</i>, 9135:108–20. Springer Nature, 2015. <a href=\"https://doi.org/10.1007/978-3-662-47666-6_9\">https://doi.org/10.1007/978-3-662-47666-6_9</a>."},"language":[{"iso":"eng"}],"intvolume":"      9135","date_updated":"2025-09-23T13:48:35Z","arxiv":1,"project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"}],"alternative_title":["LNCS"],"author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"full_name":"Doyen, Laurent","last_name":"Doyen","first_name":"Laurent"},{"last_name":"Vardi","first_name":"Moshe","full_name":"Vardi, Moshe"}],"page":"108 - 120","year":"2015","publication_status":"published","volume":9135,"month":"06"},{"ddc":["000"],"pubrep_id":"466","date_updated":"2025-09-23T08:13:52Z","intvolume":"         5","project":[{"grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"status":"public","external_id":{"isi":["000365299500001"]},"has_accepted_license":"1","abstract":[{"text":"Population structure can facilitate evolution of cooperation. In a structured population, cooperators can form clusters which resist exploitation by defectors. Recently, it was observed that a shift update rule is an extremely strong amplifier of cooperation in a one dimensional spatial model. For the shift update rule, an individual is chosen for reproduction proportional to fecundity; the offspring is placed next to the parent; a random individual dies. Subsequently, the population is rearranged (shifted) until all individual cells are again evenly spaced out. For large population size and a one dimensional population structure, the shift update rule favors cooperation for any benefit-to-cost ratio greater than one. But every attempt to generalize shift updating to higher dimensions while maintaining its strong effect has failed. The reason is that in two dimensions the clusters are fragmented by the movements caused by rearranging the cells. Here we introduce the natural phenomenon of a repulsive force between cells of different types. After a birth and death event, the cells are being rearranged minimizing the overall energy expenditure. If the repulsive force is sufficiently high, shift becomes a strong promoter of cooperation in two dimensions.","lang":"eng"}],"type":"journal_article","corr_author":"1","oa_version":"Published Version","date_created":"2018-12-11T11:53:06Z","publist_id":"5536","scopus_import":"1","publication":"Scientific Reports","language":[{"iso":"eng"}],"ec_funded":1,"citation":{"ista":"Pavlogiannis A, Chatterjee K, Adlam B, Nowak M. 2015. Cellular cooperation with shift updating and repulsion. Scientific Reports. 5, 17147.","ieee":"A. Pavlogiannis, K. Chatterjee, B. Adlam, and M. Nowak, “Cellular cooperation with shift updating and repulsion,” <i>Scientific Reports</i>, vol. 5. Nature Publishing Group, 2015.","ama":"Pavlogiannis A, Chatterjee K, Adlam B, Nowak M. Cellular cooperation with shift updating and repulsion. <i>Scientific Reports</i>. 2015;5. doi:<a href=\"https://doi.org/10.1038/srep17147\">10.1038/srep17147</a>","apa":"Pavlogiannis, A., Chatterjee, K., Adlam, B., &#38; Nowak, M. (2015). Cellular cooperation with shift updating and repulsion. <i>Scientific Reports</i>. Nature Publishing Group. <a href=\"https://doi.org/10.1038/srep17147\">https://doi.org/10.1038/srep17147</a>","short":"A. Pavlogiannis, K. Chatterjee, B. Adlam, M. Nowak, Scientific Reports 5 (2015).","mla":"Pavlogiannis, Andreas, et al. “Cellular Cooperation with Shift Updating and Repulsion.” <i>Scientific Reports</i>, vol. 5, 17147, Nature Publishing Group, 2015, doi:<a href=\"https://doi.org/10.1038/srep17147\">10.1038/srep17147</a>.","chicago":"Pavlogiannis, Andreas, Krishnendu Chatterjee, Ben Adlam, and Martin Nowak. “Cellular Cooperation with Shift Updating and Repulsion.” <i>Scientific Reports</i>. Nature Publishing Group, 2015. <a href=\"https://doi.org/10.1038/srep17147\">https://doi.org/10.1038/srep17147</a>."},"publication_status":"published","file_date_updated":"2020-07-14T12:45:07Z","year":"2015","month":"11","volume":5,"author":[{"full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","first_name":"Andreas"},{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"last_name":"Adlam","first_name":"Ben","full_name":"Adlam, Ben"},{"full_name":"Nowak, Martin","last_name":"Nowak","first_name":"Martin"}],"publisher":"Nature Publishing Group","file":[{"content_type":"application/pdf","date_created":"2018-12-12T10:12:29Z","relation":"main_file","creator":"system","access_level":"open_access","checksum":"38e06d8310d2087cae5f6d4d4bfe082b","date_updated":"2020-07-14T12:45:07Z","file_name":"IST-2016-466-v1+1_srep17147.pdf","file_id":"4947","file_size":1021931}],"acknowledgement":"The research was supported by the Austrian Science Fund (FWF) Grant No P23499-N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant (279307: Graph Games), and Microsoft Faculty Fellows award. Support from the John Templeton foundation is gratefully acknowledged.","doi":"10.1038/srep17147","isi":1,"article_number":"17147","date_published":"2015-11-25T00:00:00Z","_id":"1624","quality_controlled":"1","title":"Cellular cooperation with shift updating and repulsion","oa":1,"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","department":[{"_id":"KrCh"}],"day":"25","tmp":{"short":"CC BY (4.0)","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)"},"article_processing_charge":"No"},{"author":[{"first_name":"Tomáš","last_name":"Brázdil","full_name":"Brázdil, Tomáš"},{"last_name":"Kiefer","first_name":"Stefan","full_name":"Kiefer, Stefan"},{"full_name":"Kučera, Antonín","first_name":"Antonín","last_name":"Kučera"},{"id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotny, Petr","last_name":"Novotny","first_name":"Petr"}],"alternative_title":["LICS"],"page":"44 - 55","publication_status":"published","year":"2015","month":"07","abstract":[{"text":"We study the pattern frequency vector for runs in probabilistic Vector Addition Systems with States (pVASS). Intuitively, each configuration of a given pVASS is assigned one of finitely many patterns, and every run can thus be seen as an infinite sequence of these patterns. The pattern frequency vector assigns to each run the limit of pattern frequencies computed for longer and longer prefixes of the run. If the limit does not exist, then the vector is undefined. We show that for one-counter pVASS, the pattern frequency vector is defined and takes one of finitely many values for almost all runs. Further, these values and their associated probabilities can be approximated up to an arbitrarily small relative error in polynomial time. For stable two-counter pVASS, we show the same result, but we do not provide any upper complexity bound. As a byproduct of our study, we discover counterexamples falsifying some classical results about stochastic Petri nets published in the 80s.","lang":"eng"}],"status":"public","external_id":{"arxiv":["1505.02655"],"isi":["000380427100007"]},"date_created":"2018-12-11T11:53:19Z","scopus_import":"1","oa_version":"Preprint","publist_id":"5490","type":"conference","main_file_link":[{"url":"http://arxiv.org/abs/1505.02655","open_access":"1"}],"ec_funded":1,"citation":{"chicago":"Brázdil, Tomáš, Stefan Kiefer, Antonín Kučera, and Petr Novotný. “Long-Run Average Behaviour of Probabilistic Vector Addition Systems,” 44–55. IEEE, 2015. <a href=\"https://doi.org/10.1109/LICS.2015.15\">https://doi.org/10.1109/LICS.2015.15</a>.","short":"T. Brázdil, S. Kiefer, A. Kučera, P. Novotný, in:, IEEE, 2015, pp. 44–55.","mla":"Brázdil, Tomáš, et al. <i>Long-Run Average Behaviour of Probabilistic Vector Addition Systems</i>. IEEE, 2015, pp. 44–55, doi:<a href=\"https://doi.org/10.1109/LICS.2015.15\">10.1109/LICS.2015.15</a>.","ieee":"T. Brázdil, S. Kiefer, A. Kučera, and P. Novotný, “Long-run average behaviour of probabilistic vector addition systems,” presented at the LICS: Logic in Computer Science, Kyoto, Japan, 2015, pp. 44–55.","ama":"Brázdil T, Kiefer S, Kučera A, Novotný P. Long-run average behaviour of probabilistic vector addition systems. In: IEEE; 2015:44-55. doi:<a href=\"https://doi.org/10.1109/LICS.2015.15\">10.1109/LICS.2015.15</a>","ista":"Brázdil T, Kiefer S, Kučera A, Novotný P. 2015. Long-run average behaviour of probabilistic vector addition systems. LICS: Logic in Computer Science, LICS, , 44–55.","apa":"Brázdil, T., Kiefer, S., Kučera, A., &#38; Novotný, P. (2015). Long-run average behaviour of probabilistic vector addition systems (pp. 44–55). Presented at the LICS: Logic in Computer Science, Kyoto, Japan: IEEE. <a href=\"https://doi.org/10.1109/LICS.2015.15\">https://doi.org/10.1109/LICS.2015.15</a>"},"language":[{"iso":"eng"}],"date_updated":"2025-09-23T09:27:49Z","arxiv":1,"project":[{"grant_number":"291734","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425"}],"article_processing_charge":"No","oa":1,"title":"Long-run average behaviour of probabilistic vector addition systems","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","department":[{"_id":"KrCh"}],"day":"01","date_published":"2015-07-01T00:00:00Z","_id":"1660","quality_controlled":"1","conference":{"end_date":"2015-07-10","location":"Kyoto, Japan","start_date":"2015-07-06","name":"LICS: Logic in Computer Science"},"publisher":"IEEE","doi":"10.1109/LICS.2015.15","isi":1},{"article_processing_charge":"No","day":"22","department":[{"_id":"KrCh"}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","oa":1,"title":"Mutations driving CLL and their evolution in progression and relapse","date_published":"2015-10-22T00:00:00Z","_id":"1665","quality_controlled":"1","doi":"10.1038/nature15395","isi":1,"publisher":"Nature Publishing Group","pmid":1,"page":"525 - 530","author":[{"last_name":"Landau","first_name":"Dan","full_name":"Landau, Dan"},{"full_name":"Tausch, Eugen","last_name":"Tausch","first_name":"Eugen"},{"full_name":"Taylor Weiner, Amaro","first_name":"Amaro","last_name":"Taylor Weiner"},{"first_name":"Chip","last_name":"Stewart","full_name":"Stewart, Chip"},{"full_name":"Reiter, Johannes","id":"4A918E98-F248-11E8-B48F-1D18A9856A87","last_name":"Reiter","orcid":"0000-0002-0170-7353","first_name":"Johannes"},{"last_name":"Bahlo","first_name":"Jasmin","full_name":"Bahlo, Jasmin"},{"full_name":"Kluth, Sandra","first_name":"Sandra","last_name":"Kluth"},{"first_name":"Ivana","last_name":"Božić","full_name":"Božić, Ivana"},{"last_name":"Lawrence","first_name":"Michael","full_name":"Lawrence, Michael"},{"last_name":"Böttcher","first_name":"Sebastian","full_name":"Böttcher, Sebastian"},{"full_name":"Carter, Scott","last_name":"Carter","first_name":"Scott"},{"last_name":"Cibulskis","first_name":"Kristian","full_name":"Cibulskis, Kristian"},{"last_name":"Mertens","first_name":"Daniel","full_name":"Mertens, Daniel"},{"last_name":"Sougnez","first_name":"Carrie","full_name":"Sougnez, Carrie"},{"full_name":"Rosenberg, Mara","last_name":"Rosenberg","first_name":"Mara"},{"last_name":"Hess","first_name":"Julian","full_name":"Hess, Julian"},{"full_name":"Edelmann, Jennifer","last_name":"Edelmann","first_name":"Jennifer"},{"full_name":"Kless, Sabrina","last_name":"Kless","first_name":"Sabrina"},{"first_name":"Michael","last_name":"Kneba","full_name":"Kneba, Michael"},{"first_name":"Matthias","last_name":"Ritgen","full_name":"Ritgen, Matthias"},{"full_name":"Fink, Anna","first_name":"Anna","last_name":"Fink"},{"first_name":"Kirsten","last_name":"Fischer","full_name":"Fischer, Kirsten"},{"full_name":"Gabriel, Stacey","last_name":"Gabriel","first_name":"Stacey"},{"last_name":"Lander","first_name":"Eric","full_name":"Lander, Eric"},{"last_name":"Nowak","first_name":"Martin","full_name":"Nowak, Martin"},{"last_name":"Döhner","first_name":"Hartmut","full_name":"Döhner, Hartmut"},{"first_name":"Michael","last_name":"Hallek","full_name":"Hallek, Michael"},{"full_name":"Neuberg, Donna","last_name":"Neuberg","first_name":"Donna"},{"full_name":"Getz, Gad","last_name":"Getz","first_name":"Gad"},{"full_name":"Stilgenbauer, Stephan","first_name":"Stephan","last_name":"Stilgenbauer"},{"full_name":"Wu, Catherine","first_name":"Catherine","last_name":"Wu"}],"issue":"7574","volume":526,"month":"10","year":"2015","publication_status":"published","article_type":"original","citation":{"chicago":"Landau, Dan, Eugen Tausch, Amaro Taylor Weiner, Chip Stewart, Johannes Reiter, Jasmin Bahlo, Sandra Kluth, et al. “Mutations Driving CLL and Their Evolution in Progression and Relapse.” <i>Nature</i>. Nature Publishing Group, 2015. <a href=\"https://doi.org/10.1038/nature15395\">https://doi.org/10.1038/nature15395</a>.","apa":"Landau, D., Tausch, E., Taylor Weiner, A., Stewart, C., Reiter, J., Bahlo, J., … Wu, C. (2015). Mutations driving CLL and their evolution in progression and relapse. <i>Nature</i>. Nature Publishing Group. <a href=\"https://doi.org/10.1038/nature15395\">https://doi.org/10.1038/nature15395</a>","ama":"Landau D, Tausch E, Taylor Weiner A, et al. Mutations driving CLL and their evolution in progression and relapse. <i>Nature</i>. 2015;526(7574):525-530. doi:<a href=\"https://doi.org/10.1038/nature15395\">10.1038/nature15395</a>","ista":"Landau D, Tausch E, Taylor Weiner A, Stewart C, Reiter J, Bahlo J, Kluth S, Božić I, Lawrence M, Böttcher S, Carter S, Cibulskis K, Mertens D, Sougnez C, Rosenberg M, Hess J, Edelmann J, Kless S, Kneba M, Ritgen M, Fink A, Fischer K, Gabriel S, Lander E, Nowak M, Döhner H, Hallek M, Neuberg D, Getz G, Stilgenbauer S, Wu C. 2015. Mutations driving CLL and their evolution in progression and relapse. Nature. 526(7574), 525–530.","ieee":"D. Landau <i>et al.</i>, “Mutations driving CLL and their evolution in progression and relapse,” <i>Nature</i>, vol. 526, no. 7574. Nature Publishing Group, pp. 525–530, 2015.","mla":"Landau, Dan, et al. “Mutations Driving CLL and Their Evolution in Progression and Relapse.” <i>Nature</i>, vol. 526, no. 7574, Nature Publishing Group, 2015, pp. 525–30, doi:<a href=\"https://doi.org/10.1038/nature15395\">10.1038/nature15395</a>.","short":"D. Landau, E. Tausch, A. Taylor Weiner, C. Stewart, J. Reiter, J. Bahlo, S. Kluth, I. Božić, M. Lawrence, S. Böttcher, S. Carter, K. Cibulskis, D. Mertens, C. Sougnez, M. Rosenberg, J. Hess, J. Edelmann, S. Kless, M. Kneba, M. Ritgen, A. Fink, K. Fischer, S. Gabriel, E. Lander, M. Nowak, H. Döhner, M. Hallek, D. Neuberg, G. Getz, S. Stilgenbauer, C. Wu, Nature 526 (2015) 525–530."},"ec_funded":1,"language":[{"iso":"eng"}],"oa_version":"Submitted Version","scopus_import":"1","date_created":"2018-12-11T11:53:21Z","publist_id":"5484","publication":"Nature","type":"journal_article","main_file_link":[{"url":"https://www.ncbi.nlm.nih.gov/pmc/articles/PMC4815041/","open_access":"1"}],"abstract":[{"text":"Which genetic alterations drive tumorigenesis and how they evolve over the course of disease and therapy are central questions in cancer biology. Here we identify 44 recurrently mutated genes and 11 recurrent somatic copy number variations through whole-exome sequencing of 538 chronic lymphocytic leukaemia (CLL) and matched germline DNA samples, 278 of which were collected in a prospective clinical trial. These include previously unrecognized putative cancer drivers (RPS15, IKZF3), and collectively identify RNA processing and export, MYC activity, and MAPK signalling as central pathways involved in CLL. Clonality analysis of this large data set further enabled reconstruction of temporal relationships between driver events. Direct comparison between matched pre-treatment and relapse samples from 59 patients demonstrated highly frequent clonal evolution. Thus, large sequencing data sets of clinically informative samples enable the discovery of novel genes associated with cancer, the network of relationships between the driver events, and their impact on disease relapse and clinical outcome.","lang":"eng"}],"external_id":{"isi":["000364026100040"],"pmid":["26466571"]},"status":"public","project":[{"grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"}],"intvolume":"       526","date_updated":"2025-09-23T09:37:33Z"},{"title":"Optimizing performance of continuous-time stochastic systems using timeout synthesis","oa":1,"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","department":[{"_id":"KrCh"}],"day":"22","article_processing_charge":"No","conference":{"end_date":"2015-09-03","start_date":"2015-09-01","location":"Madrid, Spain","name":"QEST: Quantitative Evaluation of Systems"},"publisher":"Springer","doi":"10.1007/978-3-319-22264-6_10","acknowledgement":"The research leading to these results has received funding from the People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007-2013) under REA grant agreement n∘ [291734]. This work is partly supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center AVACS (SFB/TR 14), by the EU 7th Framework Programme under grant agreement no. 295261 (MEALS) and 318490 (SENSATION), by the Czech Science Foundation, grant No. 15-17564S, and by the CAS/SAFEA International Partnership Program for Creative Research Teams.","isi":1,"_id":"1667","date_published":"2015-08-22T00:00:00Z","quality_controlled":"1","publication_status":"published","year":"2015","series_title":"Lecture Notes in Computer Science","month":"08","volume":9259,"author":[{"first_name":"Tomáš","last_name":"Brázdil","full_name":"Brázdil, Tomáš"},{"full_name":"Korenčiak, L'Uboš","last_name":"Korenčiak","first_name":"L'Uboš"},{"last_name":"Krčál","first_name":"Jan","full_name":"Krčál, Jan"},{"full_name":"Novotny, Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","first_name":"Petr","last_name":"Novotny"},{"full_name":"Řehák, Vojtěch","last_name":"Řehák","first_name":"Vojtěch"}],"alternative_title":["LNCS"],"page":"141 - 159","arxiv":1,"date_updated":"2025-09-23T09:46:46Z","intvolume":"      9259","project":[{"name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734"}],"status":"public","external_id":{"isi":["000363574600012"],"arxiv":["1407.4777"]},"abstract":[{"lang":"eng","text":"We consider parametric version of fixed-delay continuoustime Markov chains (or equivalently deterministic and stochastic Petri nets, DSPN) where fixed-delay transitions are specified by parameters, rather than concrete values. Our goal is to synthesize values of these parameters that, for a given cost function, minimise expected total cost incurred before reaching a given set of target states. We show that under mild assumptions, optimal values of parameters can be effectively approximated using translation to a Markov decision process (MDP) whose actions correspond to discretized values of these parameters. To this end we identify and overcome several interesting phenomena arising in systems with fixed delays."}],"type":"conference","main_file_link":[{"url":"http://arxiv.org/abs/1407.4777","open_access":"1"}],"publist_id":"5482","oa_version":"Preprint","scopus_import":"1","date_created":"2018-12-11T11:53:22Z","language":[{"iso":"eng"}],"citation":{"chicago":"Brázdil, Tomáš, L’Uboš Korenčiak, Jan Krčál, Petr Novotný, and Vojtěch Řehák. “Optimizing Performance of Continuous-Time Stochastic Systems Using Timeout Synthesis.” Lecture Notes in Computer Science. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-22264-6_10\">https://doi.org/10.1007/978-3-319-22264-6_10</a>.","short":"T. Brázdil, L. Korenčiak, J. Krčál, P. Novotný, V. Řehák, 9259 (2015) 141–159.","mla":"Brázdil, Tomáš, et al. <i>Optimizing Performance of Continuous-Time Stochastic Systems Using Timeout Synthesis</i>. Vol. 9259, Springer, 2015, pp. 141–59, doi:<a href=\"https://doi.org/10.1007/978-3-319-22264-6_10\">10.1007/978-3-319-22264-6_10</a>.","ama":"Brázdil T, Korenčiak L, Krčál J, Novotný P, Řehák V. Optimizing performance of continuous-time stochastic systems using timeout synthesis. 2015;9259:141-159. doi:<a href=\"https://doi.org/10.1007/978-3-319-22264-6_10\">10.1007/978-3-319-22264-6_10</a>","ista":"Brázdil T, Korenčiak L, Krčál J, Novotný P, Řehák V. 2015. Optimizing performance of continuous-time stochastic systems using timeout synthesis. 9259, 141–159.","ieee":"T. Brázdil, L. Korenčiak, J. Krčál, P. Novotný, and V. Řehák, “Optimizing performance of continuous-time stochastic systems using timeout synthesis,” vol. 9259. Springer, pp. 141–159, 2015.","apa":"Brázdil, T., Korenčiak, L., Krčál, J., Novotný, P., &#38; Řehák, V. (2015). Optimizing performance of continuous-time stochastic systems using timeout synthesis. Presented at the QEST: Quantitative Evaluation of Systems, Madrid, Spain: Springer. <a href=\"https://doi.org/10.1007/978-3-319-22264-6_10\">https://doi.org/10.1007/978-3-319-22264-6_10</a>"},"ec_funded":1},{"intvolume":"       471","date_updated":"2025-09-23T07:46:22Z","ddc":["000"],"project":[{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"date_created":"2018-12-11T11:53:24Z","publication":"Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences","scopus_import":"1","publist_id":"5477","oa_version":"Published Version","type":"journal_article","abstract":[{"text":"When a new mutant arises in a population, there is a probability it outcompetes the residents and fixes. The structure of the population can affect this fixation probability. Suppressing population structures reduce the difference between two competing variants, while amplifying population structures enhance the difference. Suppressors are ubiquitous and easy to construct, but amplifiers for the large population limit are more elusive and only a few examples have been discovered. Whether or not a population structure is an amplifier of selection depends on the probability distribution for the placement of the invading mutant. First, we prove that there exist only bounded amplifiers for adversarial placement-that is, for arbitrary initial conditions. Next, we show that the Star population structure, which is known to amplify for mutants placed uniformly at random, does not amplify for mutants that arise through reproduction and are therefore placed proportional to the temperatures of the vertices. Finally, we construct population structures that amplify for all mutational events that arise through reproduction, uniformly at random, or through some combination of the two. ","lang":"eng"}],"has_accepted_license":"1","status":"public","external_id":{"isi":["000363482200005"]},"citation":{"ieee":"B. Adlam, K. Chatterjee, and M. Nowak, “Amplifiers of selection,” <i>Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences</i>, vol. 471, no. 2181. Royal Society of London, 2015.","ama":"Adlam B, Chatterjee K, Nowak M. Amplifiers of selection. <i>Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences</i>. 2015;471(2181). doi:<a href=\"https://doi.org/10.1098/rspa.2015.0114\">10.1098/rspa.2015.0114</a>","ista":"Adlam B, Chatterjee K, Nowak M. 2015. Amplifiers of selection. Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences. 471(2181), 20150114.","apa":"Adlam, B., Chatterjee, K., &#38; Nowak, M. (2015). Amplifiers of selection. <i>Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences</i>. Royal Society of London. <a href=\"https://doi.org/10.1098/rspa.2015.0114\">https://doi.org/10.1098/rspa.2015.0114</a>","short":"B. Adlam, K. Chatterjee, M. Nowak, Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences 471 (2015).","mla":"Adlam, Ben, et al. “Amplifiers of Selection.” <i>Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences</i>, vol. 471, no. 2181, 20150114, Royal Society of London, 2015, doi:<a href=\"https://doi.org/10.1098/rspa.2015.0114\">10.1098/rspa.2015.0114</a>.","chicago":"Adlam, Ben, Krishnendu Chatterjee, and Martin Nowak. “Amplifiers of Selection.” <i>Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences</i>. Royal Society of London, 2015. <a href=\"https://doi.org/10.1098/rspa.2015.0114\">https://doi.org/10.1098/rspa.2015.0114</a>."},"ec_funded":1,"language":[{"iso":"eng"}],"year":"2015","file_date_updated":"2020-07-14T12:45:11Z","publication_status":"published","issue":"2181","volume":471,"month":"09","author":[{"full_name":"Adlam, Ben","last_name":"Adlam","first_name":"Ben"},{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Nowak","first_name":"Martin","full_name":"Nowak, Martin"}],"isi":1,"file":[{"date_created":"2019-04-18T12:39:56Z","content_type":"application/pdf","access_level":"open_access","creator":"kschuh","relation":"main_file","file_name":"2015_rspa_Adlam.pdf","file_id":"6342","date_updated":"2020-07-14T12:45:11Z","checksum":"e613d94d283c776322403a28aad11bdd","file_size":391466}],"doi":"10.1098/rspa.2015.0114","acknowledgement":"K.C. gratefully acknowledges support from ERC Start grant no. (279307: Graph Games), Austrian Science Fund (FWF) grant no. P23499-N23, and FWF NFN grant no. S11407-N23 (RiSE). ","publisher":"Royal Society of London","_id":"1673","date_published":"2015-09-08T00:00:00Z","quality_controlled":"1","article_number":"20150114","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","oa":1,"title":"Amplifiers of selection","day":"08","department":[{"_id":"KrCh"}],"article_processing_charge":"No"},{"project":[{"grant_number":"291734","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425"},{"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"}],"intvolume":"         6","ddc":["000"],"pubrep_id":"448","date_updated":"2025-04-15T06:50:21Z","language":[{"iso":"eng"}],"citation":{"chicago":"Priklopil, Tadeas, and Krishnendu Chatterjee. “Evolution of Decisions in Population Games with Sequentially Searching Individuals.” <i>Games</i>. MDPI, 2015. <a href=\"https://doi.org/10.3390/g6040413\">https://doi.org/10.3390/g6040413</a>.","apa":"Priklopil, T., &#38; Chatterjee, K. (2015). Evolution of decisions in population games with sequentially searching individuals. <i>Games</i>. MDPI. <a href=\"https://doi.org/10.3390/g6040413\">https://doi.org/10.3390/g6040413</a>","ista":"Priklopil T, Chatterjee K. 2015. Evolution of decisions in population games with sequentially searching individuals. Games. 6(4), 413–437.","ieee":"T. Priklopil and K. Chatterjee, “Evolution of decisions in population games with sequentially searching individuals,” <i>Games</i>, vol. 6, no. 4. MDPI, pp. 413–437, 2015.","ama":"Priklopil T, Chatterjee K. Evolution of decisions in population games with sequentially searching individuals. <i>Games</i>. 2015;6(4):413-437. doi:<a href=\"https://doi.org/10.3390/g6040413\">10.3390/g6040413</a>","mla":"Priklopil, Tadeas, and Krishnendu Chatterjee. “Evolution of Decisions in Population Games with Sequentially Searching Individuals.” <i>Games</i>, vol. 6, no. 4, MDPI, 2015, pp. 413–37, doi:<a href=\"https://doi.org/10.3390/g6040413\">10.3390/g6040413</a>.","short":"T. Priklopil, K. Chatterjee, Games 6 (2015) 413–437."},"article_type":"original","ec_funded":1,"type":"journal_article","corr_author":"1","oa_version":"Published Version","scopus_import":"1","publication":"Games","publist_id":"5467","date_created":"2018-12-11T11:53:26Z","status":"public","has_accepted_license":"1","abstract":[{"text":"In many social situations, individuals endeavor to find the single best possible partner, but are constrained to evaluate the candidates in sequence. Examples include the search for mates, economic partnerships, or any other long-term ties where the choice to interact involves two parties. Surprisingly, however, previous theoretical work on mutual choice problems focuses on finding equilibrium solutions, while ignoring the evolutionary dynamics of decisions. Empirically, this may be of high importance, as some equilibrium solutions can never be reached unless the population undergoes radical changes and a sufficient number of individuals change their decisions simultaneously. To address this question, we apply a mutual choice sequential search problem in an evolutionary game-theoretical model that allows one to find solutions that are favored by evolution. As an example, we study the influence of sequential search on the evolutionary dynamics of cooperation. For this, we focus on the classic snowdrift game and the prisoner’s dilemma game.","lang":"eng"}],"volume":6,"issue":"4","month":"09","year":"2015","publication_status":"published","file_date_updated":"2020-07-14T12:45:12Z","page":"413 - 437","author":[{"id":"3C869AA0-F248-11E8-B48F-1D18A9856A87","full_name":"Priklopil, Tadeas","first_name":"Tadeas","last_name":"Priklopil"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"}],"file":[{"content_type":"application/pdf","date_created":"2018-12-12T10:12:41Z","creator":"system","relation":"main_file","access_level":"open_access","checksum":"912e1acbaf201100f447a43e4d5958bd","file_id":"4959","file_name":"IST-2016-448-v1+1_games-06-00413.pdf","date_updated":"2020-07-14T12:45:12Z","file_size":518832}],"doi":"10.3390/g6040413","publisher":"MDPI","quality_controlled":"1","_id":"1681","date_published":"2015-09-29T00:00:00Z","day":"29","department":[{"_id":"NiBa"},{"_id":"KrCh"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Evolution of decisions in population games with sequentially searching individuals","oa":1,"article_processing_charge":"No","tmp":{"short":"CC BY (4.0)","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)"},"publication_identifier":{"eissn":["2073-4336"]}}]