[{"language":[{"iso":"eng"}],"file":[{"creator":"system","file_size":553648,"date_updated":"2020-07-14T12:44:44Z","file_name":"IST-2016-665-v1+1_Forejt_et_al__Stability_in_graphs_and_games.pdf","date_created":"2018-12-12T10:16:40Z","relation":"main_file","access_level":"open_access","content_type":"application/pdf","checksum":"3c2dc6ab0358f8aa8f7aa7d6c1293159","file_id":"5229"}],"publication_status":"published","ec_funded":1,"volume":59,"oa_version":"Published Version","abstract":[{"lang":"eng","text":"We study graphs and two-player games in which rewards are assigned to states, and the goal of the players is to satisfy or dissatisfy certain property of the generated outcome, given as a mean payoff property. Since the notion of mean-payoff does not reflect possible fluctuations from the mean-payoff along a run, we propose definitions and algorithms for capturing the stability of the system, and give algorithms for deciding if a given mean payoff and stability objective can be ensured in the system."}],"intvolume":" 59","month":"08","alternative_title":["LIPIcs"],"scopus_import":1,"ddc":["004"],"date_updated":"2021-01-12T06:49:53Z","file_date_updated":"2020-07-14T12:44:44Z","department":[{"_id":"KrCh"}],"_id":"1325","pubrep_id":"665","status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"name":"CONCUR: Concurrency Theory","start_date":"2016-08-23","location":"Quebec City, Canada","end_date":"2016-08-26"},"type":"conference","day":"01","year":"2016","has_accepted_license":"1","date_created":"2018-12-11T11:51:23Z","date_published":"2016-08-01T00:00:00Z","doi":"10.4230/LIPIcs.CONCUR.2016.10","acknowledgement":"The work has been supported by the Czech Science Foundation, grant No. 15-17564S, by EPSRC grant\r\nEP/M023656/1, and by the People Programme (Marie Curie Actions) of the European Union’s Seventh\r\nFramework Programme (FP7/2007-2013) under REA grant agreement no [291734]","oa":1,"quality_controlled":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","citation":{"short":"T. Brázdil, V. Forejt, A. Kučera, P. Novotný, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","ieee":"T. Brázdil, V. Forejt, A. Kučera, and P. Novotný, “Stability in graphs and games,” presented at the CONCUR: Concurrency Theory, Quebec City, Canada, 2016, vol. 59.","apa":"Brázdil, T., Forejt, V., Kučera, A., & Novotný, P. (2016). Stability in graphs and games (Vol. 59). Presented at the CONCUR: Concurrency Theory, Quebec City, Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2016.10","ama":"Brázdil T, Forejt V, Kučera A, Novotný P. Stability in graphs and games. In: Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:10.4230/LIPIcs.CONCUR.2016.10","mla":"Brázdil, Tomáš, et al. Stability in Graphs and Games. Vol. 59, 10, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:10.4230/LIPIcs.CONCUR.2016.10.","ista":"Brázdil T, Forejt V, Kučera A, Novotný P. 2016. Stability in graphs and games. CONCUR: Concurrency Theory, LIPIcs, vol. 59, 10.","chicago":"Brázdil, Tomáš, Vojtěch Forejt, Antonín Kučera, and Petr Novotný. “Stability in Graphs and Games,” Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. https://doi.org/10.4230/LIPIcs.CONCUR.2016.10."},"title":"Stability in graphs and games","author":[{"first_name":"Tomáš","full_name":"Brázdil, Tomáš","last_name":"Brázdil"},{"full_name":"Forejt, Vojtěch","last_name":"Forejt","first_name":"Vojtěch"},{"first_name":"Antonín","full_name":"Kučera, Antonín","last_name":"Kučera"},{"last_name":"Novotny","full_name":"Novotny, Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","first_name":"Petr"}],"publist_id":"5944","article_number":"10","project":[{"grant_number":"291734","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425"}]},{"title":"Indefinite-horizon reachability in Goal-DEC-POMDPs","department":[{"_id":"KrCh"}],"author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"last_name":"Chmelik","full_name":"Chmelik, Martin","first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87"}],"publist_id":"5946","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Chatterjee, Krishnendu, and Martin Chmelik. “Indefinite-Horizon Reachability in Goal-DEC-POMDPs.” Proceedings of the Twenty-Sixth International Conference on International Conference on Automated Planning and Scheduling, vol. 2016–January, AAAI Press, 2016, pp. 88–96.","apa":"Chatterjee, K., & Chmelik, M. (2016). Indefinite-horizon reachability in Goal-DEC-POMDPs. In Proceedings of the Twenty-Sixth International Conference on International Conference on Automated Planning and Scheduling (Vol. 2016–January, pp. 88–96). London, United Kingdom: AAAI Press.","ama":"Chatterjee K, Chmelik M. Indefinite-horizon reachability in Goal-DEC-POMDPs. In: Proceedings of the Twenty-Sixth International Conference on International Conference on Automated Planning and Scheduling. Vol 2016-January. AAAI Press; 2016:88-96.","short":"K. Chatterjee, M. Chmelik, in:, Proceedings of the Twenty-Sixth International Conference on International Conference on Automated Planning and Scheduling, AAAI Press, 2016, pp. 88–96.","ieee":"K. Chatterjee and M. Chmelik, “Indefinite-horizon reachability in Goal-DEC-POMDPs,” in Proceedings of the Twenty-Sixth International Conference on International Conference on Automated Planning and Scheduling, London, United Kingdom, 2016, vol. 2016–January, pp. 88–96.","chicago":"Chatterjee, Krishnendu, and Martin Chmelik. “Indefinite-Horizon Reachability in Goal-DEC-POMDPs.” In Proceedings of the Twenty-Sixth International Conference on International Conference on Automated Planning and Scheduling, 2016–January:88–96. AAAI Press, 2016.","ista":"Chatterjee K, Chmelik M. 2016. Indefinite-horizon reachability in Goal-DEC-POMDPs. Proceedings of the Twenty-Sixth International Conference on International Conference on Automated Planning and Scheduling. ICAPS: International Conference on Automated Planning and Scheduling vol. 2016–January, 88–96."},"date_updated":"2021-01-12T06:49:53Z","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"status":"public","type":"conference","conference":{"name":"ICAPS: International Conference on Automated Planning and Scheduling","end_date":"2016-06-17","location":"London, United Kingdom","start_date":"2016-06-12"},"_id":"1324","volume":"2016-January","date_published":"2016-01-01T00:00:00Z","date_created":"2018-12-11T11:51:22Z","ec_funded":1,"page":"88 - 96","day":"01","language":[{"iso":"eng"}],"publication":"Proceedings of the Twenty-Sixth International Conference on International Conference on Automated Planning and Scheduling","year":"2016","publication_status":"published","month":"01","scopus_import":1,"publisher":"AAAI Press","quality_controlled":"1","main_file_link":[{"url":"http://www.aaai.org/ocs/index.php/ICAPS/ICAPS16/paper/view/12999"}],"oa_version":"None","abstract":[{"lang":"eng","text":"DEC-POMDPs extend POMDPs to a multi-agent setting, where several agents operate in an uncertain environment independently to achieve a joint objective. DEC-POMDPs have been studied with finite-horizon and infinite-horizon discounted-sum objectives, and there exist solvers both for exact and approximate solutions. In this work we consider Goal-DEC-POMDPs, where given a set of target states, the objective is to ensure that the target set is reached with minimal cost. We consider the indefinite-horizon (infinite-horizon with either discounted-sum, or undiscounted-sum, where absorbing goal states have zero-cost) problem. We present a new and novel method to solve the problem that extends methods for finite-horizon DEC-POMDPs and the RTDP-Bel approach for POMDPs. We present experimental results on several examples, and show that our approach presents promising results. Copyright "}]},{"day":"01","language":[{"iso":"eng"}],"publication":"Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems","year":"2016","publication_status":"published","date_published":"2016-01-01T00:00:00Z","date_created":"2018-12-11T11:51:23Z","ec_funded":1,"page":"1465 - 1466","oa_version":"Preprint","abstract":[{"text":"We consider partially observable Markov decision processes (POMDPs) with a set of target states and positive integer costs associated with every transition. The traditional optimization objective (stochastic shortest path) asks to minimize the expected total cost until the target set is reached. We extend the traditional framework of POMDPs to model energy consumption, which represents a hard constraint. The energy levels may increase and decrease with transitions, and the hard constraint requires that the energy level must remain positive in all steps till the target is reached. First, we present a novel algorithm for solving POMDPs with energy levels, developing on existing POMDP solvers and using RTDP as its main method. Our second contribution is related to policy representation. For larger POMDP instances the policies computed by existing solvers are too large to be understandable. We present an automated procedure based on machine learning techniques that automatically extracts important decisions of the policy allowing us to compute succinct human readable policies. Finally, we show experimentally that our algorithm performs well and computes succinct policies on a number of POMDP instances from the literature that were naturally enhanced with energy levels. ","lang":"eng"}],"month":"01","scopus_import":1,"quality_controlled":"1","publisher":"ACM","main_file_link":[{"url":"https://arxiv.org/abs/1602.07565","open_access":"1"}],"oa":1,"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T06:49:54Z","citation":{"ista":"Brázdil T, Chatterjee K, Chmelik M, Gupta A, Novotný P. 2016. Stochastic shortest path with energy constraints in POMDPs. Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems. AAMAS: Autonomous Agents & Multiagent Systems, 1465–1466.","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Anchit Gupta, and Petr Novotný. “Stochastic Shortest Path with Energy Constraints in POMDPs.” In Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems, 1465–66. ACM, 2016.","apa":"Brázdil, T., Chatterjee, K., Chmelik, M., Gupta, A., & Novotný, P. (2016). Stochastic shortest path with energy constraints in POMDPs. In Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems (pp. 1465–1466). Singapore: ACM.","ama":"Brázdil T, Chatterjee K, Chmelik M, Gupta A, Novotný P. Stochastic shortest path with energy constraints in POMDPs. In: Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems. ACM; 2016:1465-1466.","short":"T. Brázdil, K. Chatterjee, M. Chmelik, A. Gupta, P. Novotný, in:, Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems, ACM, 2016, pp. 1465–1466.","ieee":"T. Brázdil, K. Chatterjee, M. Chmelik, A. Gupta, and P. Novotný, “Stochastic shortest path with energy constraints in POMDPs,” in Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems, Singapore, 2016, pp. 1465–1466.","mla":"Brázdil, Tomáš, et al. “Stochastic Shortest Path with Energy Constraints in POMDPs.” Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems, ACM, 2016, pp. 1465–66."},"department":[{"_id":"KrCh"}],"title":"Stochastic shortest path with energy constraints in POMDPs","author":[{"first_name":"Tomáš","full_name":"Brázdil, Tomáš","last_name":"Brázdil"},{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"full_name":"Chmelik, Martin","last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87","first_name":"Martin"},{"last_name":"Gupta","full_name":"Gupta, Anchit","first_name":"Anchit"},{"last_name":"Novotny","full_name":"Novotny, Petr","first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"}],"publist_id":"5942","_id":"1327","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"International IST Postdoc Fellowship Programme","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"status":"public","type":"conference","conference":{"name":"AAMAS: Autonomous Agents & Multiagent Systems","location":"Singapore","end_date":"2016-05-13","start_date":"2016-05-09"}},{"intvolume":" 9938","month":"09","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1607.00678"}],"alternative_title":["LNCS"],"scopus_import":1,"oa_version":"Preprint","abstract":[{"text":"Energy Markov Decision Processes (EMDPs) are finite-state Markov decision processes where each transition is assigned an integer counter update and a rational payoff. An EMDP configuration is a pair s(n), where s is a control state and n is the current counter value. The configurations are changed by performing transitions in the standard way. We consider the problem of computing a safe strategy (i.e., a strategy that keeps the counter non-negative) which maximizes the expected mean payoff. ","lang":"eng"}],"ec_funded":1,"volume":9938,"language":[{"iso":"eng"}],"publication_status":"published","status":"public","conference":{"name":"ATVA: Automated Technology for Verification and Analysis","start_date":"2016-10-17","location":"Chiba, Japan","end_date":"2016-10-20"},"type":"conference","_id":"1326","department":[{"_id":"KrCh"}],"date_updated":"2021-01-12T06:49:53Z","oa":1,"quality_controlled":"1","publisher":"Springer","acknowledgement":"The research was funded by the Czech Science Foundation Grant No. P202/12/G061 and by the People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007-2013) under REA grant agreement no [291734].","date_created":"2018-12-11T11:51:23Z","date_published":"2016-09-22T00:00:00Z","doi":"10.1007/978-3-319-46520-3_3","page":"32 - 49","day":"22","year":"2016","project":[{"call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734","name":"International IST Postdoc Fellowship Programme"}],"title":"Optimizing the expected mean payoff in Energy Markov Decision Processes","publist_id":"5943","author":[{"first_name":"Tomáš","last_name":"Brázdil","full_name":"Brázdil, Tomáš"},{"first_name":"Antonín","full_name":"Kučera, Antonín","last_name":"Kučera"},{"last_name":"Novotny","full_name":"Novotny, Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","first_name":"Petr"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","citation":{"ama":"Brázdil T, Kučera A, Novotný P. Optimizing the expected mean payoff in Energy Markov Decision Processes. In: Vol 9938. Springer; 2016:32-49. doi:10.1007/978-3-319-46520-3_3","apa":"Brázdil, T., Kučera, A., & Novotný, P. (2016). Optimizing the expected mean payoff in Energy Markov Decision Processes (Vol. 9938, pp. 32–49). Presented at the ATVA: Automated Technology for Verification and Analysis, Chiba, Japan: Springer. https://doi.org/10.1007/978-3-319-46520-3_3","ieee":"T. Brázdil, A. Kučera, and P. Novotný, “Optimizing the expected mean payoff in Energy Markov Decision Processes,” presented at the ATVA: Automated Technology for Verification and Analysis, Chiba, Japan, 2016, vol. 9938, pp. 32–49.","short":"T. Brázdil, A. Kučera, P. Novotný, in:, Springer, 2016, pp. 32–49.","mla":"Brázdil, Tomáš, et al. Optimizing the Expected Mean Payoff in Energy Markov Decision Processes. Vol. 9938, Springer, 2016, pp. 32–49, doi:10.1007/978-3-319-46520-3_3.","ista":"Brázdil T, Kučera A, Novotný P. 2016. Optimizing the expected mean payoff in Energy Markov Decision Processes. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 9938, 32–49.","chicago":"Brázdil, Tomáš, Antonín Kučera, and Petr Novotný. “Optimizing the Expected Mean Payoff in Energy Markov Decision Processes,” 9938:32–49. Springer, 2016. https://doi.org/10.1007/978-3-319-46520-3_3."}},{"article_number":"10915","citation":{"ista":"Milinski M, Hilbe C, Semmann D, Sommerfeld R, Marotzke J. 2016. Humans choose representatives who enforce cooperation in social dilemmas through extortion. Nature Communications. 7, 10915.","chicago":"Milinski, Manfred, Christian Hilbe, Dirk Semmann, Ralf Sommerfeld, and Jochem Marotzke. “Humans Choose Representatives Who Enforce Cooperation in Social Dilemmas through Extortion.” Nature Communications. Nature Publishing Group, 2016. https://doi.org/10.1038/ncomms10915.","apa":"Milinski, M., Hilbe, C., Semmann, D., Sommerfeld, R., & Marotzke, J. (2016). Humans choose representatives who enforce cooperation in social dilemmas through extortion. Nature Communications. Nature Publishing Group. https://doi.org/10.1038/ncomms10915","ama":"Milinski M, Hilbe C, Semmann D, Sommerfeld R, Marotzke J. Humans choose representatives who enforce cooperation in social dilemmas through extortion. Nature Communications. 2016;7. doi:10.1038/ncomms10915","ieee":"M. Milinski, C. Hilbe, D. Semmann, R. Sommerfeld, and J. Marotzke, “Humans choose representatives who enforce cooperation in social dilemmas through extortion,” Nature Communications, vol. 7. Nature Publishing Group, 2016.","short":"M. Milinski, C. Hilbe, D. Semmann, R. Sommerfeld, J. Marotzke, Nature Communications 7 (2016).","mla":"Milinski, Manfred, et al. “Humans Choose Representatives Who Enforce Cooperation in Social Dilemmas through Extortion.” Nature Communications, vol. 7, 10915, Nature Publishing Group, 2016, doi:10.1038/ncomms10915."},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","publist_id":"5935","author":[{"first_name":"Manfred","full_name":"Milinski, Manfred","last_name":"Milinski"},{"id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","first_name":"Christian","orcid":"0000-0001-5116-955X","full_name":"Hilbe, Christian","last_name":"Hilbe"},{"full_name":"Semmann, Dirk","last_name":"Semmann","first_name":"Dirk"},{"first_name":"Ralf","last_name":"Sommerfeld","full_name":"Sommerfeld, Ralf"},{"last_name":"Marotzke","full_name":"Marotzke, Jochem","first_name":"Jochem"}],"title":"Humans choose representatives who enforce cooperation in social dilemmas through extortion","acknowledgement":"We thank the students for participation; H.-J. Krambeck for writing the software for the game; H. Arndt, T. Bakker, L. Becks, H. Brendelberger, S. Dobler and T. Reusch for support; and the Max Planck Society for the Advancement of Science for funding.","quality_controlled":"1","publisher":"Nature Publishing Group","oa":1,"has_accepted_license":"1","year":"2016","day":"07","publication":"Nature Communications","doi":"10.1038/ncomms10915","date_published":"2016-03-07T00:00:00Z","date_created":"2018-12-11T11:51:25Z","_id":"1333","type":"journal_article","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"status":"public","pubrep_id":"661","date_updated":"2021-01-12T06:49:57Z","ddc":["519","530","599"],"file_date_updated":"2020-07-14T12:44:44Z","department":[{"_id":"KrCh"}],"abstract":[{"text":"Social dilemmas force players to balance between personal and collective gain. In many dilemmas, such as elected governments negotiating climate-change mitigation measures, the decisions are made not by individual players but by their representatives. However, the behaviour of representatives in social dilemmas has not been investigated experimentally. Here inspired by the negotiations for greenhouse-gas emissions reductions, we experimentally study a collective-risk social dilemma that involves representatives deciding on behalf of their fellow group members. Representatives can be re-elected or voted out after each consecutive collective-risk game. Selfish players are preferentially elected and are hence found most frequently in the "representatives" treatment. Across all treatments, we identify the selfish players as extortioners. As predicted by our mathematical model, their steadfast strategies enforce cooperation from fair players who finally compensate almost completely the deficit caused by the extortionate co-players. Everybody gains, but the extortionate representatives and their groups gain the most.","lang":"eng"}],"oa_version":"Published Version","scopus_import":1,"month":"03","intvolume":" 7","publication_status":"published","file":[{"file_id":"4834","checksum":"9ea0d7ce59a555a1cb8353d5559407cb","content_type":"application/pdf","access_level":"open_access","relation":"main_file","date_created":"2018-12-12T10:10:44Z","file_name":"IST-2016-661-v1+1_ncomms10915.pdf","date_updated":"2020-07-14T12:44:44Z","file_size":1432577,"creator":"system"}],"language":[{"iso":"eng"}],"volume":7},{"oa":1,"publisher":"Springer","quality_controlled":"1","date_created":"2018-12-11T11:51:26Z","date_published":"2016-08-31T00:00:00Z","doi":"10.1007/978-3-662-53413-7_2","page":"23 - 38","day":"31","year":"2016","project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"}],"title":"Quantitative monitor automata","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"last_name":"Otop","full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","first_name":"Jan"}],"publist_id":"5932","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","citation":{"ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Quantitative monitor automata,” presented at the SAS: Static Analysis Symposium, Edinburgh, United Kingdom, 2016, vol. 9837, pp. 23–38.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Springer, 2016, pp. 23–38.","apa":"Chatterjee, K., Henzinger, T. A., & Otop, J. (2016). Quantitative monitor automata (Vol. 9837, pp. 23–38). Presented at the SAS: Static Analysis Symposium, Edinburgh, United Kingdom: Springer. https://doi.org/10.1007/978-3-662-53413-7_2","ama":"Chatterjee K, Henzinger TA, Otop J. Quantitative monitor automata. In: Vol 9837. Springer; 2016:23-38. doi:10.1007/978-3-662-53413-7_2","mla":"Chatterjee, Krishnendu, et al. Quantitative Monitor Automata. Vol. 9837, Springer, 2016, pp. 23–38, doi:10.1007/978-3-662-53413-7_2.","ista":"Chatterjee K, Henzinger TA, Otop J. 2016. Quantitative monitor automata. SAS: Static Analysis Symposium, LNCS, vol. 9837, 23–38.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Quantitative Monitor Automata,” 9837:23–38. Springer, 2016. https://doi.org/10.1007/978-3-662-53413-7_2."},"intvolume":" 9837","month":"08","main_file_link":[{"url":"https://arxiv.org/abs/1604.06764","open_access":"1"}],"alternative_title":["LNCS"],"scopus_import":1,"oa_version":"Preprint","abstract":[{"text":"In this paper we review various automata-theoretic formalisms for expressing quantitative properties. We start with finite-state Boolean automata that express the traditional regular properties. We then consider weighted ω-automata that can measure the average density of events, which finite-state Boolean automata cannot. However, even weighted ω-automata cannot express basic performance properties like average response time. We finally consider two formalisms of weighted ω-automata with monitors, where the monitors are either (a) counters or (b) weighted automata themselves. We present a translation result to establish that these two formalisms are equivalent. Weighted ω-automata with monitors generalize weighted ω-automata, and can express average response time property. They present a natural, robust, and expressive framework for quantitative specifications, with important decidable properties.","lang":"eng"}],"ec_funded":1,"volume":9837,"language":[{"iso":"eng"}],"publication_status":"published","status":"public","conference":{"start_date":"2016-09-08","end_date":"2016-09-10","location":"Edinburgh, United Kingdom","name":"SAS: Static Analysis Symposium"},"type":"conference","_id":"1335","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"date_updated":"2021-01-12T06:49:58Z"},{"department":[{"_id":"KrCh"}],"date_updated":"2021-01-12T06:50:00Z","status":"public","type":"conference","conference":{"name":"SAGT: Symposium on Algorithmic Game Theory","start_date":"2016-09-19","end_date":"2016-09-21","location":"Liverpool, United Kingdom"},"_id":"1340","volume":9928,"ec_funded":1,"language":[{"iso":"eng"}],"publication_status":"published","month":"09","intvolume":" 9928","scopus_import":1,"alternative_title":["LNCS"],"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1604.07634"}],"oa_version":"Preprint","abstract":[{"lang":"eng","text":"We study repeated games with absorbing states, a type of two-player, zero-sum concurrent mean-payoff games with the prototypical example being the Big Match of Gillete (1957). These games may not allow optimal strategies but they always have ε-optimal strategies. In this paper we design ε-optimal strategies for Player 1 in these games that use only O(log log T) space. Furthermore, we construct strategies for Player 1 that use space s(T), for an arbitrary small unbounded non-decreasing function s, and which guarantee an ε-optimal value for Player 1 in the limit superior sense. The previously known strategies use space Ω(log T) and it was known that no strategy can use constant space if it is ε-optimal even in the limit superior sense. We also give a complementary lower bound. Furthermore, we also show that no Markov strategy, even extended with finite memory, can ensure value greater than 0 in the Big Match, answering a question posed by Neyman [11]."}],"title":"The big match in small space","publist_id":"5927","author":[{"last_name":"Hansen","full_name":"Hansen, Kristoffer","first_name":"Kristoffer"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus","last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus"},{"first_name":"Michal","last_name":"Koucký","full_name":"Koucký, Michal"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","citation":{"chicago":"Hansen, Kristoffer, Rasmus Ibsen-Jensen, and Michal Koucký. “The Big Match in Small Space,” 9928:64–76. Springer, 2016. https://doi.org/10.1007/978-3-662-53354-3_6.","ista":"Hansen K, Ibsen-Jensen R, Koucký M. 2016. The big match in small space. SAGT: Symposium on Algorithmic Game Theory, LNCS, vol. 9928, 64–76.","mla":"Hansen, Kristoffer, et al. The Big Match in Small Space. Vol. 9928, Springer, 2016, pp. 64–76, doi:10.1007/978-3-662-53354-3_6.","ieee":"K. Hansen, R. Ibsen-Jensen, and M. Koucký, “The big match in small space,” presented at the SAGT: Symposium on Algorithmic Game Theory, Liverpool, United Kingdom, 2016, vol. 9928, pp. 64–76.","short":"K. Hansen, R. Ibsen-Jensen, M. Koucký, in:, Springer, 2016, pp. 64–76.","apa":"Hansen, K., Ibsen-Jensen, R., & Koucký, M. (2016). The big match in small space (Vol. 9928, pp. 64–76). Presented at the SAGT: Symposium on Algorithmic Game Theory, Liverpool, United Kingdom: Springer. https://doi.org/10.1007/978-3-662-53354-3_6","ama":"Hansen K, Ibsen-Jensen R, Koucký M. The big match in small space. In: Vol 9928. Springer; 2016:64-76. doi:10.1007/978-3-662-53354-3_6"},"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"date_published":"2016-09-01T00:00:00Z","doi":"10.1007/978-3-662-53354-3_6","date_created":"2018-12-11T11:51:28Z","page":"64 - 76","day":"01","year":"2016","publisher":"Springer","quality_controlled":"1","oa":1},{"publication":"Journal of the ACM","language":[{"iso":"eng"}],"day":"01","year":"2016","publication_status":"published","date_created":"2018-12-11T11:51:41Z","doi":"10.1145/2857050","date_published":"2016-06-01T00:00:00Z","volume":63,"issue":"3","oa_version":"Preprint","abstract":[{"lang":"eng","text":"We consider higher-dimensional versions of Kannan and Lipton's Orbit Problem - determining whether a target vector space V may be reached from a starting point x under repeated applications of a linear transformation A. Answering two questions posed by Kannan and Lipton in the 1980s, we show that when V has dimension one, this problem is solvable in polynomial time, and when V has dimension two or three, the problem is in NPRP."}],"intvolume":" 63","month":"06","oa":1,"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1303.2981"}],"quality_controlled":"1","publisher":"ACM","scopus_import":1,"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T06:50:17Z","citation":{"mla":"Chonev, Ventsislav K., et al. “On the Complexity of the Orbit Problem.” Journal of the ACM, vol. 63, no. 3, 23, ACM, 2016, doi:10.1145/2857050.","short":"V.K. Chonev, J. Ouaknine, J. Worrell, Journal of the ACM 63 (2016).","ieee":"V. K. Chonev, J. Ouaknine, and J. Worrell, “On the complexity of the orbit problem,” Journal of the ACM, vol. 63, no. 3. ACM, 2016.","ama":"Chonev VK, Ouaknine J, Worrell J. On the complexity of the orbit problem. Journal of the ACM. 2016;63(3). doi:10.1145/2857050","apa":"Chonev, V. K., Ouaknine, J., & Worrell, J. (2016). On the complexity of the orbit problem. Journal of the ACM. ACM. https://doi.org/10.1145/2857050","chicago":"Chonev, Ventsislav K, Joël Ouaknine, and James Worrell. “On the Complexity of the Orbit Problem.” Journal of the ACM. ACM, 2016. https://doi.org/10.1145/2857050.","ista":"Chonev VK, Ouaknine J, Worrell J. 2016. On the complexity of the orbit problem. Journal of the ACM. 63(3), 23."},"title":"On the complexity of the orbit problem","department":[{"_id":"KrCh"}],"author":[{"full_name":"Chonev, Ventsislav K","last_name":"Chonev","first_name":"Ventsislav K","id":"36CBE2E6-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Joël","full_name":"Ouaknine, Joël","last_name":"Ouaknine"},{"first_name":"James","full_name":"Worrell, James","last_name":"Worrell"}],"publist_id":"5831","article_number":"23","_id":"1380","status":"public","type":"journal_article"},{"page":"515 - 524","ec_funded":1,"date_created":"2018-12-11T11:51:44Z","date_published":"2016-07-05T00:00:00Z","doi":"10.1145/2933575.2934548","year":"2016","publication_status":"published","language":[{"iso":"eng"}],"publication":"LICS '16","day":"05","oa":1,"main_file_link":[{"url":"https://arxiv.org/abs/1507.03632","open_access":"1"}],"scopus_import":1,"quality_controlled":"1","publisher":"IEEE","month":"07","abstract":[{"text":"The continuous evolution of a wide variety of systems, including continous-time Markov chains and linear hybrid automata, can be\r\ndescribed in terms of linear differential equations. In this paper we study the decision problem of whether the solution x(t) of a system of linear differential equations dx/dt = Ax reaches a target halfspace infinitely often. This recurrent reachability problem can\r\nequivalently be formulated as the following Infinite Zeros Problem: does a real-valued function f:R≥0 --> R satisfying a given linear\r\ndifferential equation have infinitely many zeros? Our main decidability result is that if the differential equation has order at most 7, then the Infinite Zeros Problem is decidable. On the other hand, we show that a decision procedure for the Infinite Zeros Problem at order 9 (and above) would entail a major breakthrough in Diophantine Approximation, specifically an algorithm for computing the Lagrange constants of arbitrary real algebraic numbers to arbitrary precision.","lang":"eng"}],"oa_version":"Preprint","author":[{"full_name":"Chonev, Ventsislav K","last_name":"Chonev","first_name":"Ventsislav K","id":"36CBE2E6-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Joël","full_name":"Ouaknine, Joël","last_name":"Ouaknine"},{"last_name":"Worrell","full_name":"Worrell, James","first_name":"James"}],"publist_id":"5820","title":"On recurrent reachability for continuous linear dynamical systems","department":[{"_id":"KrCh"}],"date_updated":"2021-01-12T06:50:20Z","citation":{"mla":"Chonev, Ventsislav K., et al. “On Recurrent Reachability for Continuous Linear Dynamical Systems.” LICS ’16, IEEE, 2016, pp. 515–24, doi:10.1145/2933575.2934548.","short":"V.K. Chonev, J. Ouaknine, J. Worrell, in:, LICS ’16, IEEE, 2016, pp. 515–524.","ieee":"V. K. Chonev, J. Ouaknine, and J. Worrell, “On recurrent reachability for continuous linear dynamical systems,” in LICS ’16, New York, NY, USA, 2016, pp. 515–524.","apa":"Chonev, V. K., Ouaknine, J., & Worrell, J. (2016). On recurrent reachability for continuous linear dynamical systems. In LICS ’16 (pp. 515–524). New York, NY, USA: IEEE. https://doi.org/10.1145/2933575.2934548","ama":"Chonev VK, Ouaknine J, Worrell J. On recurrent reachability for continuous linear dynamical systems. In: LICS ’16. IEEE; 2016:515-524. doi:10.1145/2933575.2934548","chicago":"Chonev, Ventsislav K, Joël Ouaknine, and James Worrell. “On Recurrent Reachability for Continuous Linear Dynamical Systems.” In LICS ’16, 515–24. IEEE, 2016. https://doi.org/10.1145/2933575.2934548.","ista":"Chonev VK, Ouaknine J, Worrell J. 2016. On recurrent reachability for continuous linear dynamical systems. LICS ’16. LICS: Logic in Computer Science, 515–524."},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","conference":{"location":"New York, NY, USA","end_date":"2018-07-08","start_date":"2018-07-05","name":"LICS: Logic in Computer Science"},"type":"conference","project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"}],"status":"public","_id":"1389"},{"article_number":"160036","title":"Coevolutionary interactions between farmers and mafia induce host acceptance of avian brood parasites","publist_id":"5776","author":[{"first_name":"Maria","last_name":"Chakra","full_name":"Chakra, Maria"},{"orcid":"0000-0001-5116-955X","full_name":"Hilbe, Christian","last_name":"Hilbe","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","first_name":"Christian"},{"first_name":"Arne","last_name":"Traulsen","full_name":"Traulsen, Arne"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","citation":{"ama":"Chakra M, Hilbe C, Traulsen A. Coevolutionary interactions between farmers and mafia induce host acceptance of avian brood parasites. Royal Society Open Science. 2016;3(5). doi:10.1098/rsos.160036","apa":"Chakra, M., Hilbe, C., & Traulsen, A. (2016). Coevolutionary interactions between farmers and mafia induce host acceptance of avian brood parasites. Royal Society Open Science. Royal Society, The. https://doi.org/10.1098/rsos.160036","short":"M. Chakra, C. Hilbe, A. Traulsen, Royal Society Open Science 3 (2016).","ieee":"M. Chakra, C. Hilbe, and A. Traulsen, “Coevolutionary interactions between farmers and mafia induce host acceptance of avian brood parasites,” Royal Society Open Science, vol. 3, no. 5. Royal Society, The, 2016.","mla":"Chakra, Maria, et al. “Coevolutionary Interactions between Farmers and Mafia Induce Host Acceptance of Avian Brood Parasites.” Royal Society Open Science, vol. 3, no. 5, 160036, Royal Society, The, 2016, doi:10.1098/rsos.160036.","ista":"Chakra M, Hilbe C, Traulsen A. 2016. Coevolutionary interactions between farmers and mafia induce host acceptance of avian brood parasites. Royal Society Open Science. 3(5), 160036.","chicago":"Chakra, Maria, Christian Hilbe, and Arne Traulsen. “Coevolutionary Interactions between Farmers and Mafia Induce Host Acceptance of Avian Brood Parasites.” Royal Society Open Science. Royal Society, The, 2016. https://doi.org/10.1098/rsos.160036."},"oa":1,"publisher":"Royal Society, The","quality_controlled":"1","acknowledgement":"C.H. gratefully acknowledges funding by the Schrödinger scholarship of the Austrian Science Fund (FWF) J3475.","date_created":"2018-12-11T11:51:57Z","doi":"10.1098/rsos.160036","date_published":"2016-05-01T00:00:00Z","publication":"Royal Society Open Science","day":"01","year":"2016","has_accepted_license":"1","pubrep_id":"589","status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"type":"journal_article","_id":"1426","file_date_updated":"2020-07-14T12:44:53Z","department":[{"_id":"KrCh"}],"ddc":["000"],"date_updated":"2021-01-12T06:50:39Z","intvolume":" 3","month":"05","scopus_import":1,"oa_version":"Published Version","abstract":[{"text":"Brood parasites exploit their host in order to increase their own fitness. Typically, this results in an arms race between parasite trickery and host defence. Thus, it is puzzling to observe hosts that accept parasitism without any resistance. The ‘mafia’ hypothesis suggests that these hosts accept parasitism to avoid retaliation. Retaliation has been shown to evolve when the hosts condition their response to mafia parasites, who use depredation as a targeted response to rejection. However, it is unclear if acceptance would also emerge when ‘farming’ parasites are present in the population. Farming parasites use depredation to synchronize the timing with the host, destroying mature clutches to force the host to re-nest. Herein, we develop an evolutionary model to analyse the interaction between depredatory parasites and their hosts. We show that coevolutionary cycles between farmers and mafia can still induce host acceptance of brood parasites. However, this equilibrium is unstable and in the long-run the dynamics of this host–parasite interaction exhibits strong oscillations: when farmers are the majority, accepters conditional to mafia (the host will reject first and only accept after retaliation by the parasite) have a higher fitness than unconditional accepters (the host always accepts parasitism). This leads to an increase in mafia parasites’ fitness and in turn induce an optimal environment for accepter hosts.","lang":"eng"}],"volume":3,"issue":"5","language":[{"iso":"eng"}],"file":[{"creator":"system","date_updated":"2020-07-14T12:44:53Z","file_size":937002,"date_created":"2018-12-12T10:14:49Z","file_name":"IST-2016-589-v1+1_160036.full.pdf","access_level":"open_access","relation":"main_file","content_type":"application/pdf","checksum":"bf84211b31fe87451e738ba301d729c3","file_id":"5104"}],"publication_status":"published"},{"publisher":"Nature Publishing Group","quality_controlled":"1","oa":1,"acknowledgement":"C.H. acknowledges generous funding from the Schrödinger scholarship of the Austrian Science Fund (FWF), J3475.","doi":"10.1038/srep25676","date_published":"2016-05-10T00:00:00Z","date_created":"2018-12-11T11:51:56Z","has_accepted_license":"1","year":"2016","day":"10","publication":"Scientific Reports","article_number":"25676","publist_id":"5784","author":[{"first_name":"Seung","last_name":"Baek","full_name":"Baek, Seung"},{"full_name":"Jeong, Hyeongchai","last_name":"Jeong","first_name":"Hyeongchai"},{"last_name":"Hilbe","orcid":"0000-0001-5116-955X","full_name":"Hilbe, Christian","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","first_name":"Christian"},{"last_name":"Nowak","full_name":"Nowak, Martin","first_name":"Martin"}],"title":"Comparing reactive and memory-one strategies of direct reciprocity","citation":{"chicago":"Baek, Seung, Hyeongchai Jeong, Christian Hilbe, and Martin Nowak. “Comparing Reactive and Memory-One Strategies of Direct Reciprocity.” Scientific Reports. Nature Publishing Group, 2016. https://doi.org/10.1038/srep25676.","ista":"Baek S, Jeong H, Hilbe C, Nowak M. 2016. Comparing reactive and memory-one strategies of direct reciprocity. Scientific Reports. 6, 25676.","mla":"Baek, Seung, et al. “Comparing Reactive and Memory-One Strategies of Direct Reciprocity.” Scientific Reports, vol. 6, 25676, Nature Publishing Group, 2016, doi:10.1038/srep25676.","ieee":"S. Baek, H. Jeong, C. Hilbe, and M. Nowak, “Comparing reactive and memory-one strategies of direct reciprocity,” Scientific Reports, vol. 6. Nature Publishing Group, 2016.","short":"S. Baek, H. Jeong, C. Hilbe, M. Nowak, Scientific Reports 6 (2016).","apa":"Baek, S., Jeong, H., Hilbe, C., & Nowak, M. (2016). Comparing reactive and memory-one strategies of direct reciprocity. Scientific Reports. Nature Publishing Group. https://doi.org/10.1038/srep25676","ama":"Baek S, Jeong H, Hilbe C, Nowak M. Comparing reactive and memory-one strategies of direct reciprocity. Scientific Reports. 2016;6. doi:10.1038/srep25676"},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"month":"05","intvolume":" 6","abstract":[{"text":"Direct reciprocity is a mechanism for the evolution of cooperation based on repeated interactions. When individuals meet repeatedly, they can use conditional strategies to enforce cooperative outcomes that would not be feasible in one-shot social dilemmas. Direct reciprocity requires that individuals keep track of their past interactions and find the right response. However, there are natural bounds on strategic complexity: Humans find it difficult to remember past interactions accurately, especially over long timespans. Given these limitations, it is natural to ask how complex strategies need to be for cooperation to evolve. Here, we study stochastic evolutionary game dynamics in finite populations to systematically compare the evolutionary performance of reactive strategies, which only respond to the co-player's previous move, and memory-one strategies, which take into account the own and the co-player's previous move. In both cases, we compare deterministic strategy and stochastic strategy spaces. For reactive strategies and small costs, we find that stochasticity benefits cooperation, because it allows for generous-tit-for-tat. For memory one strategies and small costs, we find that stochasticity does not increase the propensity for cooperation, because the deterministic rule of win-stay, lose-shift works best. For memory one strategies and large costs, however, stochasticity can augment cooperation.","lang":"eng"}],"oa_version":"Published Version","volume":6,"publication_status":"published","file":[{"date_created":"2018-12-12T10:18:08Z","file_name":"IST-2016-590-v1+1_srep25676.pdf","date_updated":"2020-07-14T12:44:53Z","file_size":1349915,"creator":"system","checksum":"ee17c482370d2e1b3add393710d3c696","file_id":"5327","content_type":"application/pdf","access_level":"open_access","relation":"main_file"}],"language":[{"iso":"eng"}],"type":"journal_article","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"status":"public","pubrep_id":"590","_id":"1423","department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:44:53Z","date_updated":"2021-01-12T06:50:38Z","ddc":["000"]},{"language":[{"iso":"eng"}],"file":[{"date_updated":"2020-07-14T12:45:00Z","file_size":957466,"creator":"system","date_created":"2018-12-12T10:16:51Z","file_name":"IST-2016-561-v1+1_Lohse_et_al_Genetics_2015.pdf","content_type":"application/pdf","access_level":"open_access","relation":"main_file","file_id":"5241","checksum":"41c9b5d72e7fe4624dd22dfe622337d5"}],"publication_status":"published","ec_funded":1,"volume":202,"issue":"2","oa_version":"Preprint","pmid":1,"abstract":[{"lang":"eng","text":"The inference of demographic history from genome data is hindered by a lack of efficient computational approaches. In particular, it has proved difficult to exploit the information contained in the distribution of genealogies across the genome. We have previously shown that the generating function (GF) of genealogies can be used to analytically compute likelihoods of demographic models from configurations of mutations in short sequence blocks (Lohse et al. 2011). Although the GF has a simple, recursive form, the size of such likelihood calculations explodes quickly with the number of individuals and applications of this framework have so far been mainly limited to small samples (pairs and triplets) for which the GF can be written by hand. Here we investigate several strategies for exploiting the inherent symmetries of the coalescent. In particular, we show that the GF of genealogies can be decomposed into a set of equivalence classes that allows likelihood calculations from nontrivial samples. Using this strategy, we automated blockwise likelihood calculations for a general set of demographic scenarios in Mathematica. These histories may involve population size changes, continuous migration, discrete divergence, and admixture between multiple populations. To give a concrete example, we calculate the likelihood for a model of isolation with migration (IM), assuming two diploid samples without phase and outgroup information. We demonstrate the new inference scheme with an analysis of two individual butterfly genomes from the sister species Heliconius melpomene rosina and H. cydno."}],"intvolume":" 202","month":"02","scopus_import":"1","ddc":["570"],"date_updated":"2022-05-24T09:16:22Z","department":[{"_id":"KrCh"},{"_id":"NiBa"}],"file_date_updated":"2020-07-14T12:45:00Z","_id":"1518","pubrep_id":"561","status":"public","article_type":"original","type":"journal_article","publication":"Genetics","day":"01","year":"2016","has_accepted_license":"1","date_created":"2018-12-11T11:52:29Z","date_published":"2016-02-01T00:00:00Z","doi":"10.1534/genetics.115.183814","page":"775 - 786","acknowledgement":"We thank Lynsey Bunnefeld for discussions throughout the project and Joshua Schraiber and one anonymous reviewer\r\nfor constructive comments on an earlier version of this manuscript. This work was supported by funding from the\r\nUnited Kingdom Natural Environment Research Council (to K.L.) (NE/I020288/1) and a grant from the European\r\nResearch Council (250152) (to N.H.B.).","oa":1,"quality_controlled":"1","publisher":"Genetics Society of America","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ieee":"K. Lohse, M. Chmelik, S. Martin, and N. H. Barton, “Efficient strategies for calculating blockwise likelihoods under the coalescent,” Genetics, vol. 202, no. 2. Genetics Society of America, pp. 775–786, 2016.","short":"K. Lohse, M. Chmelik, S. Martin, N.H. Barton, Genetics 202 (2016) 775–786.","ama":"Lohse K, Chmelik M, Martin S, Barton NH. Efficient strategies for calculating blockwise likelihoods under the coalescent. Genetics. 2016;202(2):775-786. doi:10.1534/genetics.115.183814","apa":"Lohse, K., Chmelik, M., Martin, S., & Barton, N. H. (2016). Efficient strategies for calculating blockwise likelihoods under the coalescent. Genetics. Genetics Society of America. https://doi.org/10.1534/genetics.115.183814","mla":"Lohse, Konrad, et al. “Efficient Strategies for Calculating Blockwise Likelihoods under the Coalescent.” Genetics, vol. 202, no. 2, Genetics Society of America, 2016, pp. 775–86, doi:10.1534/genetics.115.183814.","ista":"Lohse K, Chmelik M, Martin S, Barton NH. 2016. Efficient strategies for calculating blockwise likelihoods under the coalescent. Genetics. 202(2), 775–786.","chicago":"Lohse, Konrad, Martin Chmelik, Simon Martin, and Nicholas H Barton. “Efficient Strategies for Calculating Blockwise Likelihoods under the Coalescent.” Genetics. Genetics Society of America, 2016. https://doi.org/10.1534/genetics.115.183814."},"title":"Efficient strategies for calculating blockwise likelihoods under the coalescent","article_processing_charge":"No","external_id":{"pmid":["26715666"]},"publist_id":"5658","author":[{"last_name":"Lohse","full_name":"Lohse, Konrad","first_name":"Konrad"},{"full_name":"Chmelik, Martin","last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87","first_name":"Martin"},{"full_name":"Martin, Simon","last_name":"Martin","first_name":"Simon"},{"id":"4880FE40-F248-11E8-B48F-1D18A9856A87","first_name":"Nicholas H","last_name":"Barton","orcid":"0000-0002-8548-5240","full_name":"Barton, Nicholas H"}],"project":[{"name":"Limits to selection in biology and in evolutionary computation","grant_number":"250152","_id":"25B07788-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}]},{"month":"01","intvolume":" 285","alternative_title":["Frontiers in Artificial Intelligence and Applications"],"scopus_import":1,"oa_version":"Published Version","abstract":[{"lang":"eng","text":"Magic: the Gathering is a game about magical combat for any number of players. Formally it is a zero-sum, imperfect information stochastic game that consists of a potentially unbounded number of steps. We consider the problem of deciding if a move is legal in a given single step of Magic. We show that the problem is (a) coNP-complete in general; and (b) in P if either of two small sets of cards are not used. Our lower bound holds even for single-player Magic games. The significant aspects of our results are as follows: First, in most real-life game problems, the task of deciding whether a given move is legal in a single step is trivial, and the computationally hard task is to find the best sequence of legal moves in the presence of multiple players. In contrast, quite uniquely our hardness result holds for single step and with only one-player. Second, we establish efficient algorithms for important special cases of Magic."}],"volume":285,"file":[{"file_name":"IST-2018-950-v1+1_2016_Chatterjee_The_complexity.pdf","date_created":"2018-12-12T10:07:59Z","file_size":2116225,"date_updated":"2020-07-14T12:46:35Z","creator":"system","checksum":"848043c812ace05e459579c923f3d3cf","file_id":"4658","content_type":"application/pdf","relation":"main_file","access_level":"open_access"}],"language":[{"iso":"eng"}],"publication_status":"published","status":"public","pubrep_id":"950","type":"conference","conference":{"start_date":"2016-08-29","location":"The Hague, Netherlands","end_date":"2016-09-02","name":"ECAI: European Conference on Artificial Intelligence"},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nc/4.0/legalcode","image":"/images/cc_by_nc.png","name":"Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)","short":"CC BY-NC (4.0)"},"_id":"478","department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:46:35Z","ddc":["004"],"date_updated":"2021-01-12T08:00:54Z","quality_controlled":"1","publisher":"IOS Press","oa":1,"date_published":"2016-01-01T00:00:00Z","doi":"10.3233/978-1-61499-672-9-1432","date_created":"2018-12-11T11:46:41Z","page":"1432 - 1439","day":"01","has_accepted_license":"1","year":"2016","title":"The complexity of deciding legality of a single step of magic: The gathering","publist_id":"7342","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","last_name":"Ibsen-Jensen","full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","citation":{"ama":"Chatterjee K, Ibsen-Jensen R. The complexity of deciding legality of a single step of magic: The gathering. In: Vol 285. IOS Press; 2016:1432-1439. doi:10.3233/978-1-61499-672-9-1432","apa":"Chatterjee, K., & Ibsen-Jensen, R. (2016). The complexity of deciding legality of a single step of magic: The gathering (Vol. 285, pp. 1432–1439). Presented at the ECAI: European Conference on Artificial Intelligence, The Hague, Netherlands: IOS Press. https://doi.org/10.3233/978-1-61499-672-9-1432","ieee":"K. Chatterjee and R. Ibsen-Jensen, “The complexity of deciding legality of a single step of magic: The gathering,” presented at the ECAI: European Conference on Artificial Intelligence, The Hague, Netherlands, 2016, vol. 285, pp. 1432–1439.","short":"K. Chatterjee, R. Ibsen-Jensen, in:, IOS Press, 2016, pp. 1432–1439.","mla":"Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. The Complexity of Deciding Legality of a Single Step of Magic: The Gathering. Vol. 285, IOS Press, 2016, pp. 1432–39, doi:10.3233/978-1-61499-672-9-1432.","ista":"Chatterjee K, Ibsen-Jensen R. 2016. The complexity of deciding legality of a single step of magic: The gathering. ECAI: European Conference on Artificial Intelligence, Frontiers in Artificial Intelligence and Applications, vol. 285, 1432–1439.","chicago":"Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. “The Complexity of Deciding Legality of a Single Step of Magic: The Gathering,” 285:1432–39. IOS Press, 2016. https://doi.org/10.3233/978-1-61499-672-9-1432."}},{"alternative_title":["Proceedings Symposium on Logic in Computer Science"],"scopus_import":1,"main_file_link":[{"url":"https://arxiv.org/abs/1604.06376","open_access":"1"}],"month":"07","abstract":[{"lang":"eng","text":"Graph games provide the foundation for modeling and synthesizing reactive processes. In the synthesis of stochastic reactive processes, the traditional model is perfect-information stochastic games, where some transitions of the game graph are controlled by two adversarial players, and the other transitions are executed probabilistically. We consider such games where the objective is the conjunction of several quantitative objectives (specified as mean-payoff conditions), which we refer to as generalized mean-payoff objectives. The basic decision problem asks for the existence of a finite-memory strategy for a player that ensures the generalized mean-payoff objective be satisfied with a desired probability against all strategies of the opponent. A special case of the decision problem is the almost-sure problem where the desired probability is 1. Previous results presented a semi-decision procedure for -approximations of the almost-sure problem. In this work, we show that both the almost-sure problem as well as the general basic decision problem are coNP-complete, significantly improving the previous results. Moreover, we show that in the case of 1-player stochastic games, randomized memoryless strategies are sufficient and the problem can be solved in polynomial time. In contrast, in two-player stochastic games, we show that even with randomized strategies exponential memory is required in general, and present a matching exponential upper bound. We also study the basic decision problem with infinite-memory strategies and present computational complexity results for the problem. Our results are relevant in the synthesis of stochastic reactive systems with multiple quantitative requirements."}],"oa_version":"Preprint","volume":"05-08-July-2016","ec_funded":1,"publication_status":"published","language":[{"iso":"eng"}],"type":"conference","conference":{"name":"LICS: Logic in Computer Science","start_date":"2016-07-05","location":"New York, NY, USA","end_date":"2016-07-08"},"status":"public","_id":"480","department":[{"_id":"KrCh"}],"date_updated":"2021-01-12T08:00:56Z","publisher":"IEEE","quality_controlled":"1","oa":1,"page":"247 - 256","date_published":"2016-07-05T00:00:00Z","doi":"10.1145/2933575.2934513","date_created":"2018-12-11T11:46:42Z","year":"2016","day":"05","project":[{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"publist_id":"7340","author":[{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Doyen, Laurent","last_name":"Doyen","first_name":"Laurent"}],"title":"Perfect-information stochastic games with generalized mean-payoff objectives","citation":{"ista":"Chatterjee K, Doyen L. 2016. Perfect-information stochastic games with generalized mean-payoff objectives. LICS: Logic in Computer Science, Proceedings Symposium on Logic in Computer Science, vol. 05-08-July-2016, 247–256.","chicago":"Chatterjee, Krishnendu, and Laurent Doyen. “Perfect-Information Stochastic Games with Generalized Mean-Payoff Objectives,” 05-08-July-2016:247–56. IEEE, 2016. https://doi.org/10.1145/2933575.2934513.","apa":"Chatterjee, K., & Doyen, L. (2016). Perfect-information stochastic games with generalized mean-payoff objectives (Vol. 05-08-July-2016, pp. 247–256). Presented at the LICS: Logic in Computer Science, New York, NY, USA: IEEE. https://doi.org/10.1145/2933575.2934513","ama":"Chatterjee K, Doyen L. Perfect-information stochastic games with generalized mean-payoff objectives. In: Vol 05-08-July-2016. IEEE; 2016:247-256. doi:10.1145/2933575.2934513","short":"K. Chatterjee, L. Doyen, in:, IEEE, 2016, pp. 247–256.","ieee":"K. Chatterjee and L. Doyen, “Perfect-information stochastic games with generalized mean-payoff objectives,” presented at the LICS: Logic in Computer Science, New York, NY, USA, 2016, vol. 05-08-July-2016, pp. 247–256.","mla":"Chatterjee, Krishnendu, and Laurent Doyen. Perfect-Information Stochastic Games with Generalized Mean-Payoff Objectives. Vol. 05-08-July-2016, IEEE, 2016, pp. 247–56, doi:10.1145/2933575.2934513."},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87"},{"citation":{"short":"K. Chatterjee, M. Chmelik, M. Tracol, Journal of Computer and System Sciences 82 (2016) 878–911.","ieee":"K. Chatterjee, M. Chmelik, and M. Tracol, “What is decidable about partially observable Markov decision processes with ω-regular objectives,” Journal of Computer and System Sciences, vol. 82, no. 5. Elsevier, pp. 878–911, 2016.","apa":"Chatterjee, K., Chmelik, M., & Tracol, M. (2016). What is decidable about partially observable Markov decision processes with ω-regular objectives. Journal of Computer and System Sciences. Elsevier. https://doi.org/10.1016/j.jcss.2016.02.009","ama":"Chatterjee K, Chmelik M, Tracol M. What is decidable about partially observable Markov decision processes with ω-regular objectives. Journal of Computer and System Sciences. 2016;82(5):878-911. doi:10.1016/j.jcss.2016.02.009","mla":"Chatterjee, Krishnendu, et al. “What Is Decidable about Partially Observable Markov Decision Processes with ω-Regular Objectives.” Journal of Computer and System Sciences, vol. 82, no. 5, Elsevier, 2016, pp. 878–911, doi:10.1016/j.jcss.2016.02.009.","ista":"Chatterjee K, Chmelik M, Tracol M. 2016. What is decidable about partially observable Markov decision processes with ω-regular objectives. Journal of Computer and System Sciences. 82(5), 878–911.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Mathieu Tracol. “What Is Decidable about Partially Observable Markov Decision Processes with ω-Regular Objectives.” Journal of Computer and System Sciences. Elsevier, 2016. https://doi.org/10.1016/j.jcss.2016.02.009."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publist_id":"5718","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"last_name":"Chmelik","full_name":"Chmelik, Martin","first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Mathieu","id":"3F54FA38-F248-11E8-B48F-1D18A9856A87","last_name":"Tracol","full_name":"Tracol, Mathieu"}],"external_id":{"arxiv":["1309.2802"]},"title":"What is decidable about partially observable Markov decision processes with ω-regular objectives","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"grant_number":"S11407","name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"year":"2016","day":"01","publication":"Journal of Computer and System Sciences","page":"878 - 911","date_published":"2016-08-01T00:00:00Z","doi":"10.1016/j.jcss.2016.02.009","date_created":"2018-12-11T11:52:15Z","quality_controlled":"1","publisher":"Elsevier","oa":1,"date_updated":"2023-02-23T12:24:38Z","department":[{"_id":"KrCh"}],"_id":"1477","type":"journal_article","status":"public","publication_status":"published","language":[{"iso":"eng"}],"issue":"5","volume":82,"related_material":{"record":[{"relation":"earlier_version","status":"public","id":"2295"},{"status":"public","id":"5400","relation":"earlier_version"}]},"ec_funded":1,"abstract":[{"text":"We consider partially observable Markov decision processes (POMDPs) with ω-regular conditions specified as parity objectives. The class of ω-regular languages provides a robust specification language to express properties in verification, and parity objectives are canonical forms to express them. The qualitative analysis problem given a POMDP and a parity objective asks whether there is a strategy to ensure that the objective is satisfied with probability 1 (resp. positive probability). While the qualitative analysis problems are undecidable even for special cases of parity objectives, we establish decidability (with optimal complexity) for POMDPs with all parity objectives under finite-memory strategies. We establish optimal (exponential) memory bounds and EXPTIME-completeness of the qualitative analysis problems under finite-memory strategies for POMDPs with parity objectives. We also present a practical approach, where we design heuristics to deal with the exponential complexity, and have applied our implementation on a number of POMDP examples.","lang":"eng"}],"oa_version":"Preprint","scopus_import":1,"main_file_link":[{"url":"https://arxiv.org/abs/1309.2802","open_access":"1"}],"month":"08","intvolume":" 82"},{"language":[{"iso":"eng"}],"publication_status":"published","ec_funded":1,"volume":234,"related_material":{"record":[{"id":"1820","status":"public","relation":"earlier_version"},{"relation":"earlier_version","id":"5425","status":"public"}]},"oa_version":"Preprint","abstract":[{"text":"We consider partially observable Markov decision processes (POMDPs) with a set of target states and an integer cost associated with every transition. The optimization objective we study asks to minimize the expected total cost of reaching a state in the target set, while ensuring that the target set is reached almost surely (with probability 1). We show that for integer costs approximating the optimal cost is undecidable. For positive costs, our results are as follows: (i) we establish matching lower and upper bounds for the optimal cost, both double exponential in the POMDP state space size; (ii) we show that the problem of approximating the optimal cost is decidable and present approximation algorithms developing on the existing algorithms for POMDPs with finite-horizon objectives. While the worst-case running time of our algorithm is double exponential, we also present efficient stopping criteria for the algorithm and show experimentally that it performs well in many examples of interest.","lang":"eng"}],"intvolume":" 234","month":"05","main_file_link":[{"url":"http://arxiv.org/abs/1411.3880","open_access":"1"}],"scopus_import":1,"date_updated":"2023-02-23T12:25:49Z","department":[{"_id":"KrCh"}],"_id":"1529","status":"public","type":"journal_article","publication":"Artificial Intelligence","day":"01","year":"2016","date_created":"2018-12-11T11:52:33Z","date_published":"2016-05-01T00:00:00Z","doi":"10.1016/j.artint.2016.01.007","page":"26 - 48","acknowledgement":"We thank Blai Bonet for helping us with RTDP-Bel. The research was partly supported by Austrian Science Fund (FWF) Grant No P23499-N23, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.","oa":1,"quality_controlled":"1","publisher":"Elsevier","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ista":"Chatterjee K, Chmelik M, Gupta R, Kanodia A. 2016. Optimal cost almost-sure reachability in POMDPs. Artificial Intelligence. 234, 26–48.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, Raghav Gupta, and Ayush Kanodia. “Optimal Cost Almost-Sure Reachability in POMDPs.” Artificial Intelligence. Elsevier, 2016. https://doi.org/10.1016/j.artint.2016.01.007.","ieee":"K. Chatterjee, M. Chmelik, R. Gupta, and A. Kanodia, “Optimal cost almost-sure reachability in POMDPs,” Artificial Intelligence, vol. 234. Elsevier, pp. 26–48, 2016.","short":"K. Chatterjee, M. Chmelik, R. Gupta, A. Kanodia, Artificial Intelligence 234 (2016) 26–48.","apa":"Chatterjee, K., Chmelik, M., Gupta, R., & Kanodia, A. (2016). Optimal cost almost-sure reachability in POMDPs. Artificial Intelligence. Elsevier. https://doi.org/10.1016/j.artint.2016.01.007","ama":"Chatterjee K, Chmelik M, Gupta R, Kanodia A. Optimal cost almost-sure reachability in POMDPs. Artificial Intelligence. 2016;234:26-48. doi:10.1016/j.artint.2016.01.007","mla":"Chatterjee, Krishnendu, et al. “Optimal Cost Almost-Sure Reachability in POMDPs.” Artificial Intelligence, vol. 234, Elsevier, 2016, pp. 26–48, doi:10.1016/j.artint.2016.01.007."},"title":"Optimal cost almost-sure reachability in POMDPs","article_processing_charge":"No","external_id":{"arxiv":["1411.3880"]},"author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"full_name":"Chmelik, Martin","last_name":"Chmelik","first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Gupta","full_name":"Gupta, Raghav","first_name":"Raghav"},{"first_name":"Ayush","last_name":"Kanodia","full_name":"Kanodia, Ayush"}],"publist_id":"5642","project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}]},{"type":"technical_report","status":"public","pubrep_id":"523","_id":"5445","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis"},{"first_name":"Yaron","full_name":"Velner, Yaron","last_name":"Velner"}],"file_date_updated":"2020-07-14T12:46:58Z","title":"Quantitative interprocedural analysis","department":[{"_id":"KrCh"}],"citation":{"ieee":"K. Chatterjee, A. Pavlogiannis, and Y. Velner, Quantitative interprocedural analysis. IST Austria, 2016.","short":"K. Chatterjee, A. Pavlogiannis, Y. Velner, Quantitative Interprocedural Analysis, IST Austria, 2016.","apa":"Chatterjee, K., Pavlogiannis, A., & Velner, Y. (2016). Quantitative interprocedural analysis. IST Austria. https://doi.org/10.15479/AT:IST-2016-523-v1-1","ama":"Chatterjee K, Pavlogiannis A, Velner Y. Quantitative Interprocedural Analysis. IST Austria; 2016. doi:10.15479/AT:IST-2016-523-v1-1","mla":"Chatterjee, Krishnendu, et al. Quantitative Interprocedural Analysis. IST Austria, 2016, doi:10.15479/AT:IST-2016-523-v1-1.","ista":"Chatterjee K, Pavlogiannis A, Velner Y. 2016. Quantitative interprocedural analysis, IST Austria, 33p.","chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, and Yaron Velner. Quantitative Interprocedural Analysis. IST Austria, 2016. https://doi.org/10.15479/AT:IST-2016-523-v1-1."},"date_updated":"2023-02-23T10:06:22Z","ddc":["005"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","oa":1,"month":"03","abstract":[{"lang":"eng","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. "}],"oa_version":"Published Version","page":"33","date_published":"2016-03-31T00:00:00Z","doi":"10.15479/AT:IST-2016-523-v1-1","related_material":{"record":[{"id":"1604","status":"public","relation":"later_version"}]},"date_created":"2018-12-12T11:39:22Z","has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"year":"2016","publication_status":"published","file":[{"file_id":"5513","checksum":"cef516fa091925b5868813e355268fb4","relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_name":"IST-2016-523-v1+1_main.pdf","date_created":"2018-12-12T11:53:52Z","creator":"system","file_size":1012204,"date_updated":"2020-07-14T12:46:58Z"}],"day":"31","language":[{"iso":"eng"}]},{"oa_version":"None","abstract":[{"text":"POMDPs are standard models for probabilistic planning problems, where an agent interacts with an uncertain environment. We study the problem of almost-sure reachability, where given a set of target states, the question is to decide whether there is a policy to ensure that the target set is reached with probability 1 (almost-surely). While in general the problem is EXPTIMEcomplete, in many practical cases policies with a small amount of memory suffice. Moreover, the existing solution to the problem is explicit, which first requires to construct explicitly an exponential reduction to a belief-support MDP. In this work, we first study the existence of observation-stationary strategies, which is NP-complete, and then small-memory strategies. We present a symbolic algorithm by an efficient encoding to SAT and using a SAT solver for the problem. We report experimental results demonstrating the scalability of our symbolic (SAT-based) approach. © 2016, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.","lang":"eng"}],"intvolume":" 2016","month":"12","quality_controlled":"1","publisher":"AAAI Press","language":[{"iso":"eng"}],"publication":"Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence","day":"02","year":"2016","publication_status":"published","date_created":"2018-12-11T11:50:30Z","ec_funded":1,"volume":2016,"date_published":"2016-12-02T00:00:00Z","related_material":{"link":[{"relation":"table_of_contents","url":"https://dl.acm.org/citation.cfm?id=3016355"}],"record":[{"id":"5443","status":"public","relation":"earlier_version"}]},"page":"3225 - 3232","_id":"1166","status":"public","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"}],"conference":{"end_date":"2016-02-17","location":"Phoenix, AZ, USA","start_date":"2016-02-12","name":"AAAI: Conference on Artificial Intelligence"},"type":"conference","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-02-23T12:26:41Z","citation":{"mla":"Chatterjee, Krishnendu, et al. “A Symbolic SAT Based Algorithm for Almost Sure Reachability with Small Strategies in Pomdps.” Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, vol. 2016, AAAI Press, 2016, pp. 3225–32.","short":"K. Chatterjee, M. Chmelik, J. Davies, in:, Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, AAAI Press, 2016, pp. 3225–3232.","ieee":"K. Chatterjee, M. Chmelik, and J. Davies, “A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps,” in Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, Phoenix, AZ, USA, 2016, vol. 2016, pp. 3225–3232.","apa":"Chatterjee, K., Chmelik, M., & Davies, J. (2016). A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps. In Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence (Vol. 2016, pp. 3225–3232). Phoenix, AZ, USA: AAAI Press.","ama":"Chatterjee K, Chmelik M, Davies J. A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps. In: Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence. Vol 2016. AAAI Press; 2016:3225-3232.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Jessica Davies. “A Symbolic SAT Based Algorithm for Almost Sure Reachability with Small Strategies in Pomdps.” In Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, 2016:3225–32. AAAI Press, 2016.","ista":"Chatterjee K, Chmelik M, Davies J. 2016. A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps. Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 2016, 3225–3232."},"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"title":"A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps","publist_id":"6191","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","full_name":"Chmelik, Martin","last_name":"Chmelik"},{"last_name":"Davies","full_name":"Davies, Jessica","first_name":"Jessica","id":"378E0060-F248-11E8-B48F-1D18A9856A87"}]},{"type":"technical_report","pubrep_id":"648","status":"public","_id":"5449","author":[{"full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas"},{"orcid":"0000-0002-1097-9684","full_name":"Tkadlec, Josef","last_name":"Tkadlec","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","first_name":"Josef"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"first_name":"Martin","last_name":"Nowak","full_name":"Nowak, Martin"}],"file_date_updated":"2020-07-14T12:46:58Z","title":"Amplification on undirected population structures: Comets beat stars","department":[{"_id":"KrCh"}],"date_updated":"2023-02-23T12:22:21Z","citation":{"ista":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Amplification on undirected population structures: Comets beat stars, IST Austria, 22p.","chicago":"Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak. Amplification on Undirected Population Structures: Comets Beat Stars. IST Austria, 2016. https://doi.org/10.15479/AT:IST-2016-648-v1-1.","short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Amplification on Undirected Population Structures: Comets Beat Stars, IST Austria, 2016.","ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, Amplification on undirected population structures: Comets beat stars. IST Austria, 2016.","apa":"Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. (2016). Amplification on undirected population structures: Comets beat stars. IST Austria. https://doi.org/10.15479/AT:IST-2016-648-v1-1","ama":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. Amplification on Undirected Population Structures: Comets Beat Stars. IST Austria; 2016. doi:10.15479/AT:IST-2016-648-v1-1","mla":"Pavlogiannis, Andreas, et al. Amplification on Undirected Population Structures: Comets Beat Stars. IST Austria, 2016, doi:10.15479/AT:IST-2016-648-v1-1."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["519"],"oa":1,"publisher":"IST Austria","alternative_title":["IST Austria Technical Report"],"month":"11","abstract":[{"lang":"eng","text":"The fixation probability is the probability that a new mutant introduced in a homogeneous population eventually takes over the entire population.\r\nThe fixation probability is a fundamental quantity of natural selection, and known to depend on the population structure.\r\nAmplifiers of natural selection are population structures which increase the fixation probability of advantageous mutants, as compared to the baseline case of well-mixed populations. In this work we focus on symmetric population structures represented as undirected graphs. In the regime of undirected graphs, the strongest amplifier known has been the Star graph, and the existence of undirected graphs with stronger amplification properties has remained open for over a decade.\r\nIn this work we present the Comet and Comet-swarm families of undirected graphs. We show that for a range of fitness values of the mutants, the Comet and Comet-swarm graphs have fixation probability strictly larger than the fixation probability of the Star graph, for fixed population size and at the limit of large populations, respectively."}],"oa_version":"Updated Version","page":"22","date_created":"2018-12-12T11:39:24Z","doi":"10.15479/AT:IST-2016-648-v1-1","date_published":"2016-11-09T00:00:00Z","related_material":{"record":[{"relation":"later_version","id":"512","status":"public"}]},"year":"2016","publication_status":"published","has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"language":[{"iso":"eng"}],"day":"09","file":[{"relation":"main_file","access_level":"open_access","content_type":"application/pdf","checksum":"8345a8c1e7d7f0cd92516d182b7fc59e","file_id":"5529","creator":"system","file_size":1264221,"date_updated":"2020-07-14T12:46:58Z","file_name":"IST-2016-648-v1+1_tr.pdf","date_created":"2018-12-12T11:54:07Z"}]},{"date_updated":"2023-02-23T12:27:07Z","citation":{"mla":"Pavlogiannis, Andreas, et al. Arbitrarily Strong Amplifiers of Natural Selection. IST Austria, 2016, doi:10.15479/AT:IST-2017-749-v3-1.","apa":"Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. (2016). Arbitrarily strong amplifiers of natural selection. IST Austria. https://doi.org/10.15479/AT:IST-2017-749-v3-1","ama":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. Arbitrarily Strong Amplifiers of Natural Selection. IST Austria; 2016. doi:10.15479/AT:IST-2017-749-v3-1","ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, Arbitrarily strong amplifiers of natural selection. IST Austria, 2016.","short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Arbitrarily Strong Amplifiers of Natural Selection, IST Austria, 2016.","chicago":"Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak. Arbitrarily Strong Amplifiers of Natural Selection. IST Austria, 2016. https://doi.org/10.15479/AT:IST-2017-749-v3-1.","ista":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Arbitrarily strong amplifiers of natural selection, IST Austria, 34p."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000"],"author":[{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis"},{"last_name":"Tkadlec","orcid":"0000-0002-1097-9684","full_name":"Tkadlec, Josef","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","first_name":"Josef"},{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Nowak","full_name":"Nowak, Martin","first_name":"Martin"}],"title":"Arbitrarily strong amplifiers of natural selection","department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:46:59Z","_id":"5453","type":"technical_report","pubrep_id":"755","status":"public","year":"2016","publication_status":"published","has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"language":[{"iso":"eng"}],"file":[{"content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"83b0313dab3bff4bdb6ac38695026fda","file_id":"5474","date_updated":"2020-07-14T12:46:59Z","file_size":1015647,"creator":"system","date_created":"2018-12-12T11:53:13Z","file_name":"IST-2017-749-v3+1_main.pdf"}],"day":"30","page":"34","date_created":"2018-12-12T11:39:25Z","date_published":"2016-12-30T00:00:00Z","doi":"10.15479/AT:IST-2017-749-v3-1","related_material":{"record":[{"id":"5452","status":"public","relation":"earlier_version"}]},"oa_version":"Published Version","oa":1,"alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","month":"12"},{"page":"34","doi":"10.15479/AT:IST-2016-728-v1-1","date_published":"2016-12-30T00:00:00Z","date_created":"2018-12-12T11:39:24Z","publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1","publication_status":"published","year":"2016","day":"30","file":[{"date_updated":"2020-07-14T12:46:59Z","file_size":1014732,"creator":"system","date_created":"2018-12-12T11:53:04Z","file_name":"IST-2016-728-v1+1_main.pdf","content_type":"application/pdf","access_level":"open_access","relation":"main_file","file_id":"5465","checksum":"7b8bb17c322c0556acba6ac169fa71c1"}],"language":[{"iso":"eng"}],"alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","oa":1,"month":"12","oa_version":"Published Version","author":[{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722"},{"id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","first_name":"Josef","last_name":"Tkadlec","orcid":"0000-0002-1097-9684","full_name":"Tkadlec, Josef"},{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Nowak, Martin","last_name":"Nowak","first_name":"Martin"}],"file_date_updated":"2020-07-14T12:46:59Z","department":[{"_id":"KrCh"}],"title":"Strong amplifiers of natural selection","date_updated":"2023-02-23T12:27:05Z","citation":{"mla":"Pavlogiannis, Andreas, et al. Strong Amplifiers of Natural Selection. IST Austria, 2016, doi:10.15479/AT:IST-2016-728-v1-1.","apa":"Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. (2016). Strong amplifiers of natural selection. IST Austria. https://doi.org/10.15479/AT:IST-2016-728-v1-1","ama":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. Strong Amplifiers of Natural Selection. IST Austria; 2016. doi:10.15479/AT:IST-2016-728-v1-1","short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Strong Amplifiers of Natural Selection, IST Austria, 2016.","ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, Strong amplifiers of natural selection. IST Austria, 2016.","chicago":"Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak. Strong Amplifiers of Natural Selection. IST Austria, 2016. https://doi.org/10.15479/AT:IST-2016-728-v1-1.","ista":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Strong amplifiers of natural selection, IST Austria, 34p."},"ddc":["000"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"technical_report","status":"public","pubrep_id":"728","_id":"5451"},{"day":"04","year":"2016","date_created":"2021-08-10T08:42:00Z","related_material":{"record":[{"relation":"used_in_publication","status":"public","id":"1322"}]},"doi":"10.1371/journal.pone.0163867.s008","oa_version":"Published Version","abstract":[{"text":"In the beginning of our experiment, subjects were asked to read a few pages on their computer screens that would explain the rules of the subsequent game. Here, we provide these instructions, translated from German.","lang":"eng"}],"month":"10","publisher":"Public Library of Science","user_id":"6785fbc1-c503-11eb-8a32-93094b40e1cf","citation":{"mla":"Hilbe, Christian, et al. Experimental Game Instructions. Public Library of Science, 2016, doi:10.1371/journal.pone.0163867.s008.","short":"C. Hilbe, K. Hagel, M. Milinski, (2016).","ieee":"C. Hilbe, K. Hagel, and M. Milinski, “Experimental game instructions.” Public Library of Science, 2016.","ama":"Hilbe C, Hagel K, Milinski M. Experimental game instructions. 2016. doi:10.1371/journal.pone.0163867.s008","apa":"Hilbe, C., Hagel, K., & Milinski, M. (2016). Experimental game instructions. Public Library of Science. https://doi.org/10.1371/journal.pone.0163867.s008","chicago":"Hilbe, Christian, Kristin Hagel, and Manfred Milinski. “Experimental Game Instructions.” Public Library of Science, 2016. https://doi.org/10.1371/journal.pone.0163867.s008.","ista":"Hilbe C, Hagel K, Milinski M. 2016. Experimental game instructions, Public Library of Science, 10.1371/journal.pone.0163867.s008."},"date_updated":"2023-02-21T16:59:01Z","title":"Experimental game instructions","department":[{"_id":"KrCh"}],"article_processing_charge":"No","author":[{"last_name":"Hilbe","orcid":"0000-0001-5116-955X","full_name":"Hilbe, Christian","first_name":"Christian","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Kristin","full_name":"Hagel, Kristin","last_name":"Hagel"},{"last_name":"Milinski","full_name":"Milinski, Manfred","first_name":"Manfred"}],"_id":"9867","status":"public","type":"research_data_reference"},{"scopus_import":1,"intvolume":" 11","month":"10","abstract":[{"text":"Direct reciprocity is a major mechanism for the evolution of cooperation. Several classical studies have suggested that humans should quickly learn to adopt reciprocal strategies to establish mutual cooperation in repeated interactions. On the other hand, the recently discovered theory of ZD strategies has found that subjects who use extortionate strategies are able to exploit and subdue cooperators. Although such extortioners have been predicted to succeed in any population of adaptive opponents, theoretical follow-up studies questioned whether extortion can evolve in reality. However, most of these studies presumed that individuals have similar strategic possibilities and comparable outside options, whereas asymmetries are ubiquitous in real world applications. Here we show with a model and an economic experiment that extortionate strategies readily emerge once subjects differ in their strategic power. Our experiment combines a repeated social dilemma with asymmetric partner choice. In our main treatment there is one randomly chosen group member who is unilaterally allowed to exchange one of the other group members after every ten rounds of the social dilemma. We find that this asymmetric replacement opportunity generally promotes cooperation, but often the resulting payoff distribution reflects the underlying power structure. Almost half of the subjects in a better strategic position turn into extortioners, who quickly proceed to exploit their peers. By adapting their cooperation probabilities consistent with ZD theory, extortioners force their co-players to cooperate without being similarly cooperative themselves. Comparison to non-extortionate players under the same conditions indicates a substantial net gain to extortion. Our results thus highlight how power asymmetries can endanger mutually beneficial interactions, and transform them into exploitative relationships. In particular, our results indicate that the extortionate strategies predicted from ZD theory could play a more prominent role in our daily interactions than previously thought.","lang":"eng"}],"oa_version":"Published Version","issue":"10","related_material":{"record":[{"status":"public","id":"9867","relation":"research_data"},{"id":"9868","status":"public","relation":"research_data"}]},"volume":11,"publication_status":"published","language":[{"iso":"eng"}],"file":[{"file_name":"IST-2016-716-v1+1_journal.pone.0163867.PDF","date_created":"2018-12-12T10:08:08Z","creator":"system","file_size":2077905,"date_updated":"2020-07-14T12:44:44Z","file_id":"4668","checksum":"6b33e394003dfe8b4ca6be1858aaa8e3","relation":"main_file","access_level":"open_access","content_type":"application/pdf"}],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"type":"journal_article","pubrep_id":"716","status":"public","_id":"1322","department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:44:44Z","date_updated":"2023-02-23T14:11:27Z","ddc":["004","006"],"oa":1,"publisher":"Public Library of Science","quality_controlled":"1","acknowledgement":"CH was funded by the Schrödinger program of the Austrian Science Fund (FWF) J3475. ","date_created":"2018-12-11T11:51:22Z","date_published":"2016-10-04T00:00:00Z","doi":"10.1371/journal.pone.0163867","year":"2016","has_accepted_license":"1","publication":"PLoS One","day":"04","article_number":"e0163867","publist_id":"5948","author":[{"id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87","first_name":"Christian","last_name":"Hilbe","full_name":"Hilbe, Christian","orcid":"0000-0001-5116-955X"},{"last_name":"Hagel","full_name":"Hagel, Kristin","first_name":"Kristin"},{"last_name":"Milinski","full_name":"Milinski, Manfred","first_name":"Manfred"}],"title":"Asymmetric power boosts extortion in an economic experiment","citation":{"ista":"Hilbe C, Hagel K, Milinski M. 2016. Asymmetric power boosts extortion in an economic experiment. PLoS One. 11(10), e0163867.","chicago":"Hilbe, Christian, Kristin Hagel, and Manfred Milinski. “Asymmetric Power Boosts Extortion in an Economic Experiment.” PLoS One. Public Library of Science, 2016. https://doi.org/10.1371/journal.pone.0163867.","apa":"Hilbe, C., Hagel, K., & Milinski, M. (2016). Asymmetric power boosts extortion in an economic experiment. PLoS One. Public Library of Science. https://doi.org/10.1371/journal.pone.0163867","ama":"Hilbe C, Hagel K, Milinski M. Asymmetric power boosts extortion in an economic experiment. PLoS One. 2016;11(10). doi:10.1371/journal.pone.0163867","ieee":"C. Hilbe, K. Hagel, and M. Milinski, “Asymmetric power boosts extortion in an economic experiment,” PLoS One, vol. 11, no. 10. Public Library of Science, 2016.","short":"C. Hilbe, K. Hagel, M. Milinski, PLoS One 11 (2016).","mla":"Hilbe, Christian, et al. “Asymmetric Power Boosts Extortion in an Economic Experiment.” PLoS One, vol. 11, no. 10, e0163867, Public Library of Science, 2016, doi:10.1371/journal.pone.0163867."},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87"},{"type":"research_data_reference","status":"public","_id":"9868","author":[{"last_name":"Hilbe","full_name":"Hilbe, Christian","orcid":"0000-0001-5116-955X","first_name":"Christian","id":"2FDF8F3C-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Hagel","full_name":"Hagel, Kristin","first_name":"Kristin"},{"first_name":"Manfred","full_name":"Milinski, Manfred","last_name":"Milinski"}],"article_processing_charge":"No","department":[{"_id":"KrCh"}],"title":"Experimental data","citation":{"mla":"Hilbe, Christian, et al. Experimental Data. Public Library of Science, 2016, doi:10.1371/journal.pone.0163867.s009.","ama":"Hilbe C, Hagel K, Milinski M. Experimental data. 2016. doi:10.1371/journal.pone.0163867.s009","apa":"Hilbe, C., Hagel, K., & Milinski, M. (2016). Experimental data. Public Library of Science. https://doi.org/10.1371/journal.pone.0163867.s009","short":"C. Hilbe, K. Hagel, M. Milinski, (2016).","ieee":"C. Hilbe, K. Hagel, and M. Milinski, “Experimental data.” Public Library of Science, 2016.","chicago":"Hilbe, Christian, Kristin Hagel, and Manfred Milinski. “Experimental Data.” Public Library of Science, 2016. https://doi.org/10.1371/journal.pone.0163867.s009.","ista":"Hilbe C, Hagel K, Milinski M. 2016. Experimental data, Public Library of Science, 10.1371/journal.pone.0163867.s009."},"date_updated":"2023-02-21T16:59:01Z","user_id":"6785fbc1-c503-11eb-8a32-93094b40e1cf","publisher":"Public Library of Science","month":"10","abstract":[{"text":"The raw data file containing the experimental decisions of all our study subjects.","lang":"eng"}],"oa_version":"Published Version","date_published":"2016-10-04T00:00:00Z","doi":"10.1371/journal.pone.0163867.s009","related_material":{"record":[{"status":"public","id":"1322","relation":"used_in_publication"}]},"date_created":"2021-08-10T08:45:00Z","year":"2016","day":"04"},{"_id":"1397","type":"dissertation","status":"public","date_updated":"2023-09-07T11:54:58Z","citation":{"chicago":"Chmelik, Martin. “Algorithms for Partially Observable Markov Decision Processes.” Institute of Science and Technology Austria, 2016.","ista":"Chmelik M. 2016. Algorithms for partially observable markov decision processes. Institute of Science and Technology Austria.","mla":"Chmelik, Martin. Algorithms for Partially Observable Markov Decision Processes. Institute of Science and Technology Austria, 2016.","ieee":"M. Chmelik, “Algorithms for partially observable markov decision processes,” Institute of Science and Technology Austria, 2016.","short":"M. Chmelik, Algorithms for Partially Observable Markov Decision Processes, Institute of Science and Technology Austria, 2016.","apa":"Chmelik, M. (2016). Algorithms for partially observable markov decision processes. Institute of Science and Technology Austria.","ama":"Chmelik M. Algorithms for partially observable markov decision processes. 2016."},"supervisor":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","article_processing_charge":"No","author":[{"first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","full_name":"Chmelik, Martin","last_name":"Chmelik"}],"publist_id":"5810","department":[{"_id":"KrCh"}],"title":"Algorithms for partially observable markov decision processes","abstract":[{"lang":"eng","text":"We study partially observable Markov decision processes (POMDPs) with objectives used in verification and artificial intelligence. The qualitative analysis problem given a POMDP and an objective asks whether there is a strategy (policy) to ensure that the objective is satisfied almost surely (with probability 1), resp. with positive probability (with probability greater than 0). For POMDPs with limit-average payoff, where a reward value in the interval [0,1] is associated to every transition, and the payoff of an infinite path is the long-run average of the rewards, we consider two types of path constraints: (i) a quantitative limit-average constraint defines the set of paths where the payoff is at least a given threshold L1 = 1. Our main results for qualitative limit-average constraint under almost-sure winning are as follows: (i) the problem of deciding the existence of a finite-memory controller is EXPTIME-complete; and (ii) the problem of deciding the existence of an infinite-memory controller is undecidable. For quantitative limit-average constraints we show that the problem of deciding the existence of a finite-memory controller is undecidable. We present a prototype implementation of our EXPTIME algorithm. For POMDPs with w-regular conditions specified as parity objectives, while the qualitative analysis problems are known to be undecidable even for very special case of parity objectives, we establish decidability (with optimal complexity) of the qualitative analysis problems for POMDPs with parity objectives under finite-memory strategies. We establish optimal (exponential) memory bounds and EXPTIME-completeness of the qualitative analysis problems under finite-memory strategies for POMDPs with parity objectives. Based on our theoretical algorithms we also present a practical approach, where we design heuristics to deal with the exponential complexity, and have applied our implementation on a number of well-known POMDP examples for robotics applications. For POMDPs with a set of target states and an integer cost associated with every transition, we study the optimization objective that asks to minimize the expected total cost of reaching a state in the target set, while ensuring that the target set is reached almost surely. We show that for general integer costs approximating the optimal cost is undecidable. For positive costs, our results are as follows: (i) we establish matching lower and upper bounds for the optimal cost, both double and exponential in the POMDP state space size; (ii) we show that the problem of approximating the optimal cost is decidable and present approximation algorithms that extend existing algorithms for POMDPs with finite-horizon objectives. We show experimentally that it performs well in many examples of interest. We study more deeply the problem of almost-sure reachability, where given a set of target states, the question is to decide whether there is a strategy to ensure that the target set is reached almost surely. While in general the problem EXPTIME-complete, in many practical cases strategies with a small amount of memory suffice. Moreover, the existing solution to the problem is explicit, which first requires to construct explicitly an exponential reduction to a belief-support MDP. We first study the existence of observation-stationary strategies, which is NP-complete, and then small-memory strategies. We present a symbolic algorithm by an efficient encoding to SAT and using a SAT solver for the problem. We report experimental results demonstrating the scalability of our symbolic (SAT-based) approach. Decentralized POMDPs (DEC-POMDPs) extend POMDPs to a multi-agent setting, where several agents operate in an uncertain environment independently to achieve a joint objective. In this work we consider Goal DEC-POMDPs, where given a set of target states, the objective is to ensure that the target set is reached with minimal cost. We consider the indefinite-horizon (infinite-horizon with either discounted-sum, or undiscounted-sum, where absorbing goal states have zero-cost) problem. We present a new and novel method to solve the problem that extends methods for finite-horizon DEC-POMDPs and the real-time dynamic programming approach for POMDPs. We present experimental results on several examples, and show that our approach presents promising results. In the end we present a short summary of a few other results related to verification of MDPs and POMDPs."}],"oa_version":"None","publisher":"Institute of Science and Technology Austria","alternative_title":["ISTA Thesis"],"month":"02","year":"2016","degree_awarded":"PhD","publication_status":"published","publication_identifier":{"issn":["2663-337X"]},"language":[{"iso":"eng"}],"day":"01","page":"232","date_created":"2018-12-11T11:51:47Z","date_published":"2016-02-01T00:00:00Z"},{"date_created":"2018-12-11T11:50:06Z","doi":"10.4230/LIPIcs.CONCUR.2016.20","date_published":"2016-08-01T00:00:00Z","day":"01","year":"2016","has_accepted_license":"1","oa":1,"quality_controlled":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989\r\n(QUAREM), the Austrian Science Fund (FWF) under grants project S11402-N23 (RiSE and SHiNE)\r\nand Z211-N23 (Wittgenstein Award), by the Czech Science Foundation Grant No. P202/12/G061, and\r\nby the SNSF Advanced Postdoc. Mobility Fellowship – grant number P300P2_161067.","title":"Linear distances between Markov chains","publist_id":"6283","author":[{"last_name":"Daca","full_name":"Daca, Przemyslaw","first_name":"Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","last_name":"Kretinsky","first_name":"Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-9041-0905","full_name":"Petrov, Tatjana","last_name":"Petrov","id":"3D5811FC-F248-11E8-B48F-1D18A9856A87","first_name":"Tatjana"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","citation":{"ista":"Daca P, Henzinger TA, Kretinsky J, Petrov T. 2016. Linear distances between Markov chains. CONCUR: Concurrency Theory, LIPIcs, vol. 59, 20.","chicago":"Daca, Przemyslaw, Thomas A Henzinger, Jan Kretinsky, and Tatjana Petrov. “Linear Distances between Markov Chains,” Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. https://doi.org/10.4230/LIPIcs.CONCUR.2016.20.","apa":"Daca, P., Henzinger, T. A., Kretinsky, J., & Petrov, T. (2016). Linear distances between Markov chains (Vol. 59). Presented at the CONCUR: Concurrency Theory, Quebec City; Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2016.20","ama":"Daca P, Henzinger TA, Kretinsky J, Petrov T. Linear distances between Markov chains. In: Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:10.4230/LIPIcs.CONCUR.2016.20","ieee":"P. Daca, T. A. Henzinger, J. Kretinsky, and T. Petrov, “Linear distances between Markov chains,” presented at the CONCUR: Concurrency Theory, Quebec City; Canada, 2016, vol. 59.","short":"P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","mla":"Daca, Przemyslaw, et al. Linear Distances between Markov Chains. Vol. 59, 20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:10.4230/LIPIcs.CONCUR.2016.20."},"project":[{"name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"}],"article_number":"20","ec_funded":1,"related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"1155"}]},"volume":59,"language":[{"iso":"eng"}],"file":[{"date_created":"2018-12-12T10:11:39Z","file_name":"IST-2017-794-v1+1_LIPIcs-CONCUR-2016-20.pdf","creator":"system","date_updated":"2018-12-12T10:11:39Z","file_size":501827,"file_id":"4895","access_level":"open_access","relation":"main_file","content_type":"application/pdf"}],"publication_status":"published","intvolume":" 59","month":"08","alternative_title":["LIPIcs"],"scopus_import":1,"oa_version":"Published Version","abstract":[{"text":"We introduce a general class of distances (metrics) between Markov chains, which are based on linear behaviour. This class encompasses distances given topologically (such as the total variation distance or trace distance) as well as by temporal logics or automata. We investigate which of the distances can be approximated by observing the systems, i.e. by black-box testing or simulation, and we provide both negative and positive results. ","lang":"eng"}],"department":[{"_id":"ToHe"},{"_id":"KrCh"},{"_id":"CaGu"}],"file_date_updated":"2018-12-12T10:11:39Z","ddc":["004"],"date_updated":"2023-09-07T11:58:33Z","pubrep_id":"794","status":"public","conference":{"name":"CONCUR: Concurrency Theory","start_date":"2016-08-23","location":"Quebec City; Canada","end_date":"2016-08-26"},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"type":"conference","_id":"1093"},{"file_date_updated":"2018-12-12T10:14:31Z","department":[{"_id":"KrCh"}],"ddc":["004","006"],"date_updated":"2023-09-07T12:01:58Z","pubrep_id":"777","status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"start_date":"2016-08-22","end_date":"2016-08-24","location":"Aarhus, Denmark","name":"ESA: European Symposium on Algorithms"},"type":"conference","_id":"1071","ec_funded":1,"volume":57,"related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"821"}]},"language":[{"iso":"eng"}],"file":[{"file_id":"5084","content_type":"application/pdf","relation":"main_file","access_level":"open_access","file_name":"IST-2017-777-v1+1_LIPIcs-ESA-2016-28.pdf","date_created":"2018-12-12T10:14:31Z","file_size":579225,"date_updated":"2018-12-12T10:14:31Z","creator":"system"}],"publication_status":"published","intvolume":" 57","month":"08","scopus_import":1,"alternative_title":["LIPIcs"],"oa_version":"Published Version","abstract":[{"text":"We consider data-structures for answering reachability and distance queries on constant-treewidth graphs with n nodes, on the standard RAM computational model with wordsize W=Theta(log n). Our first contribution is a data-structure that after O(n) preprocessing time, allows (1) pair reachability queries in O(1) time; and (2) single-source reachability queries in O(n/log n) time. This is (asymptotically) optimal and is faster than DFS/BFS when answering more than a constant number of single-source queries. The data-structure uses at all times O(n) space. Our second contribution is a space-time tradeoff data-structure for distance queries. For any epsilon in [1/2,1], we provide a data-structure with polynomial preprocessing time that allows pair queries in O(n^{1-\\epsilon} alpha(n)) time, where alpha is the inverse of the Ackermann function, and at all times uses O(n^epsilon) space. The input graph G is not considered in the space complexity. ","lang":"eng"}],"title":"Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs","author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas"}],"publist_id":"6312","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","citation":{"ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2016. Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs. ESA: European Symposium on Algorithms, LIPIcs, vol. 57, 28.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Optimal Reachability and a Space Time Tradeoff for Distance Queries in Constant Treewidth Graphs,” Vol. 57. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik, 2016. https://doi.org/10.4230/LIPIcs.ESA.2016.28.","apa":"Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2016). Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs (Vol. 57). Presented at the ESA: European Symposium on Algorithms, Aarhus, Denmark: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik. https://doi.org/10.4230/LIPIcs.ESA.2016.28","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs. In: Vol 57. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik; 2016. doi:10.4230/LIPIcs.ESA.2016.28","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, in:, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik, 2016.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Optimal reachability and a space time tradeoff for distance queries in constant treewidth graphs,” presented at the ESA: European Symposium on Algorithms, Aarhus, Denmark, 2016, vol. 57.","mla":"Chatterjee, Krishnendu, et al. Optimal Reachability and a Space Time Tradeoff for Distance Queries in Constant Treewidth Graphs. Vol. 57, 28, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik, 2016, doi:10.4230/LIPIcs.ESA.2016.28."},"project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"article_number":"28","date_created":"2018-12-11T11:49:59Z","doi":"10.4230/LIPIcs.ESA.2016.28","date_published":"2016-08-01T00:00:00Z","day":"01","year":"2016","has_accepted_license":"1","oa":1,"quality_controlled":"1","publisher":"Schloss Dagstuhl- Leibniz-Zentrum fur Informatik","acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No P23499-N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE) and ERC Start grant (279307: Graph Games)."},{"department":[{"_id":"KrCh"}],"date_updated":"2023-09-19T14:38:41Z","conference":{"start_date":"2016-01-20","end_date":"2016-01-22","location":"St. Petersburg, FL, USA","name":"POPL: Principles of Programming Languages"},"type":"conference","status":"public","_id":"1438","ec_funded":1,"volume":"20-22","related_material":{"record":[{"relation":"later_version","status":"public","id":"5993"}]},"publication_status":"published","language":[{"iso":"eng"}],"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1510.08517"}],"alternative_title":["POPL"],"scopus_import":1,"month":"01","abstract":[{"lang":"eng","text":"In this paper, we consider termination of probabilistic programs with real-valued variables. The questions concerned are: (a) qualitative ones that ask (i) whether the program terminates with probability 1 (almost-sure termination) and (ii) whether the expected termination time is finite (finite termination); (b) quantitative ones that ask (i) to approximate the expected termination time (expectation problem) and (ii) to compute a bound B such that the probability to terminate after B steps decreases exponentially (concentration problem). To solve these questions, we utilize the notion of ranking supermartingales which is a powerful approach for proving termination of probabilistic programs. In detail, we focus on algorithmic synthesis of linear ranking-supermartingales over affine probabilistic programs (APP's) with both angelic and demonic non-determinism. An important subclass of APP's is LRAPP which is defined as the class of all APP's over which a linear ranking-supermartingale exists. Our main contributions are as follows. Firstly, we show that the membership problem of LRAPP (i) can be decided in polynomial time for APP's with at most demonic non-determinism, and (ii) is NP-hard and in PSPACE for APP's with angelic non-determinism; moreover, the NP-hardness result holds already for APP's without probability and demonic non-determinism. Secondly, we show that the concentration problem over LRAPP can be solved in the same complexity as for the membership problem of LRAPP. Finally, we show that the expectation problem over LRAPP can be solved in 2EXPTIME and is PSPACE-hard even for APP's without probability and non-determinism (i.e., deterministic programs). Our experimental results demonstrate the effectiveness of our approach to answer the qualitative and quantitative questions over APP's with at most demonic non-determinism."}],"oa_version":"Preprint","external_id":{"arxiv":["1510.08517"]},"publist_id":"5760","author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","first_name":"Hongfei","full_name":"Fu, Hongfei","last_name":"Fu"},{"first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","last_name":"Novotny","full_name":"Novotny, Petr"},{"full_name":"Hasheminezhad, Rouzbeh","last_name":"Hasheminezhad","first_name":"Rouzbeh"}],"title":"Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs","citation":{"ista":"Chatterjee K, Fu H, Novotný P, Hasheminezhad R. 2016. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. POPL: Principles of Programming Languages, POPL, vol. 20–22, 327–342.","chicago":"Chatterjee, Krishnendu, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad. “Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs,” 20–22:327–42. ACM, 2016. https://doi.org/10.1145/2837614.2837639.","ama":"Chatterjee K, Fu H, Novotný P, Hasheminezhad R. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. In: Vol 20-22. ACM; 2016:327-342. doi:10.1145/2837614.2837639","apa":"Chatterjee, K., Fu, H., Novotný, P., & Hasheminezhad, R. (2016). Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs (Vol. 20–22, pp. 327–342). Presented at the POPL: Principles of Programming Languages, St. Petersburg, FL, USA: ACM. https://doi.org/10.1145/2837614.2837639","ieee":"K. Chatterjee, H. Fu, P. Novotný, and R. Hasheminezhad, “Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs,” presented at the POPL: Principles of Programming Languages, St. Petersburg, FL, USA, 2016, vol. 20–22, pp. 327–342.","short":"K. Chatterjee, H. Fu, P. Novotný, R. Hasheminezhad, in:, ACM, 2016, pp. 327–342.","mla":"Chatterjee, Krishnendu, et al. Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs. Vol. 20–22, ACM, 2016, pp. 327–42, doi:10.1145/2837614.2837639."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23","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"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"291734","name":"International IST Postdoc Fellowship Programme"}],"page":"327 - 342","date_created":"2018-12-11T11:52:01Z","date_published":"2016-01-11T00:00:00Z","doi":"10.1145/2837614.2837639","year":"2016","day":"11","oa":1,"publisher":"ACM","quality_controlled":"1","acknowledgement":"Supported by the Natural Science Foundation of China (NSFC) under Grant No. 61532019 "},{"month":"12","alternative_title":["IST Austria Technical Report"],"oa_version":"Published Version","related_material":{"record":[{"status":"public","id":"5453","relation":"later_version"},{"status":"public","id":"5559","relation":"popular_science"}]},"ec_funded":1,"file":[{"file_id":"5460","checksum":"58e895f26c82f560c0f0989bf8b08599","content_type":"application/pdf","relation":"main_file","access_level":"open_access","file_name":"IST-2017-728-v2+1_main.pdf","date_created":"2018-12-12T11:52:59Z","file_size":811558,"date_updated":"2020-07-14T12:46:59Z","creator":"system"}],"language":[{"iso":"eng"}],"publication_identifier":{"issn":["2664-1690"]},"publication_status":"published","status":"public","pubrep_id":"750","type":"technical_report","_id":"5452","file_date_updated":"2020-07-14T12:46:59Z","department":[{"_id":"KrCh"}],"ddc":["000"],"date_updated":"2024-02-21T13:48:42Z","publisher":"IST Austria","oa":1,"doi":"10.15479/AT:IST-2017-728-v2-1","date_published":"2016-12-30T00:00:00Z","date_created":"2018-12-12T11:39:25Z","page":"32","day":"30","has_accepted_license":"1","year":"2016","project":[{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"title":"Arbitrarily strong amplifiers of natural selection","author":[{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722"},{"last_name":"Tkadlec","full_name":"Tkadlec, Josef","orcid":"0000-0002-1097-9684","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","first_name":"Josef"},{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Nowak","full_name":"Nowak, Martin","first_name":"Martin"}],"article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"chicago":"Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak. Arbitrarily Strong Amplifiers of Natural Selection. IST Austria, 2016. https://doi.org/10.15479/AT:IST-2017-728-v2-1.","ista":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Arbitrarily strong amplifiers of natural selection, IST Austria, 32p.","mla":"Pavlogiannis, Andreas, et al. Arbitrarily Strong Amplifiers of Natural Selection. IST Austria, 2016, doi:10.15479/AT:IST-2017-728-v2-1.","short":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Arbitrarily Strong Amplifiers of Natural Selection, IST Austria, 2016.","ieee":"A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, Arbitrarily strong amplifiers of natural selection. IST Austria, 2016.","apa":"Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. (2016). Arbitrarily strong amplifiers of natural selection. IST Austria. https://doi.org/10.15479/AT:IST-2017-728-v2-1","ama":"Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. Arbitrarily Strong Amplifiers of Natural Selection. IST Austria; 2016. doi:10.15479/AT:IST-2017-728-v2-1"}},{"date_updated":"2024-03-27T23:30:32Z","department":[{"_id":"KrCh"}],"_id":"1437","status":"public","type":"conference","conference":{"name":"POPL: Principles of Programming Languages","end_date":"2016-01-22","location":"St. Petersburg, FL, USA","start_date":"2016-01-20"},"language":[{"iso":"eng"}],"publication_status":"published","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"5441"},{"relation":"earlier_version","status":"public","id":"5442"},{"id":"821","status":"public","relation":"dissertation_contains"},{"id":"6009","status":"public","relation":"later_version"},{"relation":"dissertation_contains","id":"8934","status":"public"}]},"volume":"20-22","ec_funded":1,"oa_version":"Preprint","abstract":[{"text":"We study algorithmic questions for concurrent systems where the transitions are labeled from a complete, closed semiring, and path properties are algebraic with semiring operations. The algebraic path properties can model dataflow analysis problems, the shortest path problem, and many other natural problems that arise in program analysis. We consider that each component of the concurrent system is a graph with constant treewidth, a property satisfied by the controlflow graphs of most programs. We allow for multiple possible queries, which arise naturally in demand driven dataflow analysis. The study of multiple queries allows us to consider the tradeoff between the resource usage of the one-time preprocessing and for each individual query. The traditional approach constructs the product graph of all components and applies the best-known graph algorithm on the product. In this approach, even the answer to a single query requires the transitive closure (i.e., the results of all possible queries), which provides no room for tradeoff between preprocessing and query time. Our main contributions are algorithms that significantly improve the worst-case running time of the traditional approach, and provide various tradeoffs depending on the number of queries. For example, in a concurrent system of two components, the traditional approach requires hexic time in the worst case for answering one query as well as computing the transitive closure, whereas we show that with one-time preprocessing in almost cubic time, each subsequent query can be answered in at most linear time, and even the transitive closure can be computed in almost quartic time. Furthermore, we establish conditional optimality results showing that the worst-case running time of our algorithms cannot be improved without achieving major breakthroughs in graph algorithms (i.e., improving the worst-case bound for the shortest path problem in general graphs). Preliminary experimental results show that our algorithms perform favorably on several benchmarks.","lang":"eng"}],"month":"01","alternative_title":["POPL"],"scopus_import":1,"main_file_link":[{"url":"http://arxiv.org/abs/1510.07565","open_access":"1"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Chatterjee, Krishnendu, et al. Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components. Vol. 20–22, ACM, 2016, pp. 733–47, doi:10.1145/2837614.2837624.","apa":"Chatterjee, K., Goharshady, A. K., Ibsen-Jensen, R., & Pavlogiannis, A. (2016). Algorithms for algebraic path properties in concurrent systems of constant treewidth components (Vol. 20–22, pp. 733–747). Presented at the POPL: Principles of Programming Languages, St. Petersburg, FL, USA: ACM. https://doi.org/10.1145/2837614.2837624","ama":"Chatterjee K, Goharshady AK, Ibsen-Jensen R, Pavlogiannis A. Algorithms for algebraic path properties in concurrent systems of constant treewidth components. In: Vol 20-22. ACM; 2016:733-747. doi:10.1145/2837614.2837624","short":"K. Chatterjee, A.K. Goharshady, R. Ibsen-Jensen, A. Pavlogiannis, in:, ACM, 2016, pp. 733–747.","ieee":"K. Chatterjee, A. K. Goharshady, R. Ibsen-Jensen, and A. Pavlogiannis, “Algorithms for algebraic path properties in concurrent systems of constant treewidth components,” presented at the POPL: Principles of Programming Languages, St. Petersburg, FL, USA, 2016, vol. 20–22, pp. 733–747.","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components,” 20–22:733–47. ACM, 2016. https://doi.org/10.1145/2837614.2837624.","ista":"Chatterjee K, Goharshady AK, Ibsen-Jensen R, Pavlogiannis A. 2016. Algorithms for algebraic path properties in concurrent systems of constant treewidth components. POPL: Principles of Programming Languages, POPL, vol. 20–22, 733–747."},"title":"Algorithms for algebraic path properties in concurrent systems of constant treewidth components","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"391365CE-F248-11E8-B48F-1D18A9856A87","first_name":"Amir","last_name":"Goharshady","orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir"},{"last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus"},{"orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"}],"publist_id":"5761","external_id":{"arxiv":["1510.07565"]},"project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"day":"11","year":"2016","doi":"10.1145/2837614.2837624","date_published":"2016-01-11T00:00:00Z","date_created":"2018-12-11T11:52:01Z","page":"733 - 747","quality_controlled":"1","publisher":"ACM","oa":1},{"oa":1,"publisher":"Springer","quality_controlled":"1","day":"01","year":"2016","date_created":"2018-12-11T11:51:43Z","doi":"10.1007/978-3-319-41528-4_1","date_published":"2016-07-01T00:00:00Z","page":"3 - 22","project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Quantitative Reactive Modeling","grant_number":"267989","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","citation":{"short":"K. Chatterjee, H. Fu, A.K. Goharshady, in:, Springer, 2016, pp. 3–22.","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:10.1007/978-3-319-41528-4_1","apa":"Chatterjee, K., Fu, H., & 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. https://doi.org/10.1007/978-3-319-41528-4_1","mla":"Chatterjee, Krishnendu, et al. Termination Analysis of Probabilistic Programs through Positivstellensatz’s. Vol. 9779, Springer, 2016, pp. 3–22, doi:10.1007/978-3-319-41528-4_1.","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. https://doi.org/10.1007/978-3-319-41528-4_1."},"title":"Termination analysis of probabilistic programs through Positivstellensatz's","publist_id":"5824","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Fu, Hongfei","last_name":"Fu","id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","first_name":"Hongfei"},{"orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir","last_name":"Goharshady","first_name":"Amir","id":"391365CE-F248-11E8-B48F-1D18A9856A87"}],"oa_version":"Preprint","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."}],"intvolume":" 9779","month":"07","main_file_link":[{"url":"http://arxiv.org/abs/1604.07169","open_access":"1"}],"alternative_title":["LNCS"],"scopus_import":1,"language":[{"iso":"eng"}],"publication_status":"published","ec_funded":1,"related_material":{"record":[{"id":"8934","status":"public","relation":"dissertation_contains"}]},"volume":9779,"_id":"1386","status":"public","conference":{"name":"CAV: Computer Aided Verification","location":"Toronto, Canada","end_date":"2016-07-23","start_date":"2016-07-17"},"type":"conference","date_updated":"2024-03-27T23:30:32Z","department":[{"_id":"KrCh"}]},{"title":"The value 1 problem under finite-memory strategies for concurrent mean-payoff games","external_id":{"arxiv":["1409.6690"]},"article_processing_charge":"No","author":[{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"short":"K. Chatterjee, R. Ibsen-Jensen, in:, Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms, SIAM, 2015, pp. 1018–1029.","ieee":"K. Chatterjee and R. Ibsen-Jensen, “The value 1 problem under finite-memory strategies for concurrent mean-payoff games,” in Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms, San Diego, CA, United States, 2015, vol. 2015, no. 1, pp. 1018–1029.","ama":"Chatterjee K, Ibsen-Jensen R. The value 1 problem under finite-memory strategies for concurrent mean-payoff games. In: Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms. Vol 2015. SIAM; 2015:1018-1029. doi:10.1137/1.9781611973730.69","apa":"Chatterjee, K., & Ibsen-Jensen, R. (2015). The value 1 problem under finite-memory strategies for concurrent mean-payoff games. In Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms (Vol. 2015, pp. 1018–1029). San Diego, CA, United States: SIAM. https://doi.org/10.1137/1.9781611973730.69","mla":"Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. “The Value 1 Problem under Finite-Memory Strategies for Concurrent Mean-Payoff Games.” Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms, vol. 2015, no. 1, SIAM, 2015, pp. 1018–29, doi:10.1137/1.9781611973730.69.","ista":"Chatterjee K, Ibsen-Jensen R. 2015. The value 1 problem under finite-memory strategies for concurrent mean-payoff games. Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms. SODA: Symposium on Discrete Algorithms vol. 2015, 1018–1029.","chicago":"Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. “The Value 1 Problem under Finite-Memory Strategies for Concurrent Mean-Payoff Games.” In Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms, 2015:1018–29. SIAM, 2015. https://doi.org/10.1137/1.9781611973730.69."},"project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"date_created":"2022-02-25T12:18:43Z","date_published":"2015-01-01T00:00:00Z","doi":"10.1137/1.9781611973730.69","page":"1018-1029","publication":"Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms","day":"01","year":"2015","quality_controlled":"1","publisher":"SIAM","acknowledgement":"The research was partly supported by FWF Grant No P 23499-N23, FWF NFN Grant\r\nNo S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.","department":[{"_id":"KrCh"}],"date_updated":"2022-02-25T12:33:32Z","status":"public","conference":{"name":"SODA: Symposium on Discrete Algorithms","start_date":"2015-01-04","end_date":"2015-01-06","location":"San Diego, CA, United States"},"type":"conference","_id":"10796","ec_funded":1,"issue":"1","volume":2015,"language":[{"iso":"eng"}],"publication_status":"published","publication_identifier":{"isbn":["978-161197374-7"]},"intvolume":" 2015","month":"01","scopus_import":"1","oa_version":"Preprint","abstract":[{"text":"We consider concurrent mean-payoff games, a very well-studied class of two-player (player 1 vs player 2) zero-sum games on finite-state graphs where every transition is assigned a reward between 0 and 1, and the payoff function is the long-run average of the rewards. The value is the maximal expected payoff that player 1 can guarantee against all strategies of player 2. We consider the computation of the set of states with value 1 under finite-memory strategies for player 1, and our main results for the problem are as follows: (1) we present a polynomial-time algorithm; (2) we show that whenever there is a finite-memory strategy, there is a stationary strategy that does not need memory at all; and (3) we present an optimal bound (which is double exponential) on the patience of stationary strategies (where patience of a distribution is the inverse of the smallest positive probability and represents a complexity measure of a stationary strategy).","lang":"eng"}]},{"title":"Polynomial time decidability of weighted synchronization under partial observability","publist_id":"5680","author":[{"last_name":"Kretinsky","orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan"},{"first_name":"Kim","last_name":"Larsen","full_name":"Larsen, Kim"},{"first_name":"Simon","last_name":"Laursen","full_name":"Laursen, Simon"},{"full_name":"Srba, Jiří","last_name":"Srba","first_name":"Jiří"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"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. https://doi.org/10.4230/LIPIcs.CONCUR.2015.142.","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.","mla":"Kretinsky, Jan, et al. Polynomial Time Decidability of Weighted Synchronization under Partial Observability. Vol. 42, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pp. 142–54, doi:10.4230/LIPIcs.CONCUR.2015.142.","short":"J. Kretinsky, K. Larsen, S. Laursen, J. Srba, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pp. 142–154.","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.","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:10.4230/LIPIcs.CONCUR.2015.142","apa":"Kretinsky, J., Larsen, K., Laursen, S., & 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. https://doi.org/10.4230/LIPIcs.CONCUR.2015.142"},"project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize"},{"name":"International IST Postdoc Fellowship Programme","grant_number":"291734","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425"}],"date_created":"2018-12-11T11:52:22Z","date_published":"2015-01-01T00:00:00Z","doi":"10.4230/LIPIcs.CONCUR.2015.142","page":"142 - 154","day":"01","year":"2015","has_accepted_license":"1","oa":1,"quality_controlled":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","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.","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:44:58Z","ddc":["000","003"],"date_updated":"2021-01-12T06:51:10Z","pubrep_id":"498","status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"name":"CONCUR: Concurrency Theory","end_date":"2015-09-04","location":"Madrid, Spain","start_date":"2015-09-01"},"type":"conference","_id":"1499","ec_funded":1,"volume":42,"language":[{"iso":"eng"}],"file":[{"date_created":"2018-12-12T10:08:12Z","file_name":"IST-2016-498-v1+1_32.pdf","date_updated":"2020-07-14T12:44:58Z","file_size":623563,"creator":"system","file_id":"4672","checksum":"49eb5021caafaabe5356c65b9c5f8c9c","content_type":"application/pdf","access_level":"open_access","relation":"main_file"}],"publication_status":"published","intvolume":" 42","month":"01","alternative_title":["LIPIcs"],"scopus_import":1,"oa_version":"Published Version","abstract":[{"lang":"eng","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."}]},{"department":[{"_id":"KrCh"}],"date_updated":"2021-01-12T06:51:36Z","type":"journal_article","status":"public","_id":"1559","volume":112,"issue":"51","publication_status":"published","language":[{"iso":"eng"}],"main_file_link":[{"open_access":"1","url":"http://www.ncbi.nlm.nih.gov/pmc/articles/PMC4697423/"}],"scopus_import":1,"intvolume":" 112","month":"12","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"}],"pmid":1,"oa_version":"Submitted Version","external_id":{"pmid":["26644569"]},"publist_id":"5612","author":[{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus","orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen"},{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"last_name":"Nowak","full_name":"Nowak, Martin","first_name":"Martin"}],"title":"Computational complexity of ecological and evolutionary spatial dynamics","citation":{"ama":"Ibsen-Jensen R, Chatterjee K, Nowak M. Computational complexity of ecological and evolutionary spatial dynamics. PNAS. 2015;112(51):15636-15641. doi:10.1073/pnas.1511366112","apa":"Ibsen-Jensen, R., Chatterjee, K., & Nowak, M. (2015). Computational complexity of ecological and evolutionary spatial dynamics. PNAS. National Academy of Sciences. https://doi.org/10.1073/pnas.1511366112","short":"R. Ibsen-Jensen, K. Chatterjee, M. Nowak, PNAS 112 (2015) 15636–15641.","ieee":"R. Ibsen-Jensen, K. Chatterjee, and M. Nowak, “Computational complexity of ecological and evolutionary spatial dynamics,” PNAS, vol. 112, no. 51. National Academy of Sciences, pp. 15636–15641, 2015.","mla":"Ibsen-Jensen, Rasmus, et al. “Computational Complexity of Ecological and Evolutionary Spatial Dynamics.” PNAS, vol. 112, no. 51, National Academy of Sciences, 2015, pp. 15636–41, doi:10.1073/pnas.1511366112.","ista":"Ibsen-Jensen R, Chatterjee K, Nowak M. 2015. Computational complexity of ecological and evolutionary spatial dynamics. PNAS. 112(51), 15636–15641.","chicago":"Ibsen-Jensen, Rasmus, Krishnendu Chatterjee, and Martin Nowak. “Computational Complexity of Ecological and Evolutionary Spatial Dynamics.” PNAS. National Academy of Sciences, 2015. https://doi.org/10.1073/pnas.1511366112."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","page":"15636 - 15641","date_created":"2018-12-11T11:52:43Z","doi":"10.1073/pnas.1511366112","date_published":"2015-12-22T00:00:00Z","year":"2015","publication":"PNAS","day":"22","oa":1,"quality_controlled":"1","publisher":"National Academy of Sciences"},{"project":[{"call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","grant_number":"291734"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","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.","chicago":"Forejt, Vojtěch, Jan Krčál, and Jan Kretinsky. “Controller Synthesis for MDPs and Frequency LTL\\GU,” 9450:162–77. Springer, 2015. https://doi.org/10.1007/978-3-662-48899-7_12.","short":"V. Forejt, J. Krčál, J. Kretinsky, in:, Springer, 2015, pp. 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.","apa":"Forejt, V., Krčál, J., & 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. https://doi.org/10.1007/978-3-662-48899-7_12","ama":"Forejt V, Krčál J, Kretinsky J. Controller synthesis for MDPs and frequency LTL\\GU. In: Vol 9450. Springer; 2015:162-177. doi:10.1007/978-3-662-48899-7_12","mla":"Forejt, Vojtěch, et al. Controller Synthesis for MDPs and Frequency LTL\\GU. Vol. 9450, Springer, 2015, pp. 162–77, doi:10.1007/978-3-662-48899-7_12."},"title":"Controller synthesis for MDPs and frequency LTL\\GU","publist_id":"5577","author":[{"last_name":"Forejt","full_name":"Forejt, Vojtěch","first_name":"Vojtěch"},{"first_name":"Jan","last_name":"Krčál","full_name":"Krčál, Jan"},{"full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","last_name":"Kretinsky","first_name":"Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"}],"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","publisher":"Springer","quality_controlled":"1","day":"22","year":"2015","date_created":"2018-12-11T11:52:55Z","doi":"10.1007/978-3-662-48899-7_12","date_published":"2015-11-22T00:00:00Z","page":"162 - 177","_id":"1594","status":"public","conference":{"start_date":"2015-11-24","end_date":"2015-11-28","location":"Suva, Fiji","name":"LPAR: Logic for Programming, Artificial Intelligence, and Reasoning"},"type":"conference","date_updated":"2021-01-12T06:51:50Z","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"oa_version":"None","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"}],"intvolume":" 9450","month":"11","scopus_import":1,"alternative_title":["LNCS"],"language":[{"iso":"eng"}],"publication_status":"published","ec_funded":1,"volume":9450},{"conference":{"name":"CAV: Computer Aided Verification","end_date":"2015-07-24","location":"San Francisco, CA, United States","start_date":"2015-07-18"},"type":"conference","status":"public","_id":"1601","file_date_updated":"2020-07-14T12:45:04Z","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"date_updated":"2021-01-12T06:51:54Z","ddc":["000"],"scopus_import":1,"alternative_title":["LNCS"],"intvolume":" 9206","month":"07","abstract":[{"lang":"eng","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."}],"oa_version":"Submitted Version","ec_funded":1,"volume":9206,"publication_status":"published","language":[{"iso":"eng"}],"file":[{"date_created":"2020-05-15T08:38:12Z","file_name":"2015_CAV_Babiak.pdf","date_updated":"2020-07-14T12:45:04Z","file_size":1651779,"creator":"dernst","file_id":"7850","checksum":"5885236fa88a439baba9ac6f3e801e93","content_type":"application/pdf","access_level":"open_access","relation":"main_file"}],"project":[{"grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"},{"grant_number":"291734","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"article_processing_charge":"No","publist_id":"5566","author":[{"first_name":"Tomáš","full_name":"Babiak, Tomáš","last_name":"Babiak"},{"first_name":"František","full_name":"Blahoudek, František","last_name":"Blahoudek"},{"full_name":"Duret Lutz, Alexandre","last_name":"Duret Lutz","first_name":"Alexandre"},{"first_name":"Joachim","full_name":"Klein, Joachim","last_name":"Klein"},{"last_name":"Kretinsky","full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","first_name":"Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Daniel","full_name":"Mueller, Daniel","last_name":"Mueller"},{"full_name":"Parker, David","last_name":"Parker","first_name":"David"},{"first_name":"Jan","full_name":"Strejček, Jan","last_name":"Strejček"}],"title":"The Hanoi omega-automata format","citation":{"mla":"Babiak, Tomáš, et al. The Hanoi Omega-Automata Format. Vol. 9206, Springer, 2015, pp. 479–86, doi:10.1007/978-3-319-21690-4_31.","ieee":"T. Babiak et al., “The Hanoi omega-automata format,” presented at the CAV: Computer Aided Verification, San Francisco, CA, United States, 2015, vol. 9206, pp. 479–486.","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.","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. https://doi.org/10.1007/978-3-319-21690-4_31","ama":"Babiak T, Blahoudek F, Duret Lutz A, et al. The Hanoi omega-automata format. In: Vol 9206. Springer; 2015:479-486. doi:10.1007/978-3-319-21690-4_31","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. https://doi.org/10.1007/978-3-319-21690-4_31.","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."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa":1,"publisher":"Springer","quality_controlled":"1","page":"479 - 486","date_created":"2018-12-11T11:52:57Z","date_published":"2015-07-16T00:00:00Z","doi":"10.1007/978-3-319-21690-4_31","year":"2015","has_accepted_license":"1","day":"16"},{"date_updated":"2022-02-01T15:04:44Z","department":[{"_id":"KrCh"}],"_id":"1609","conference":{"name":"ICALP: Automata, Languages and Programming","start_date":"2015-07-06","end_date":"2015-07-10","location":"Kyoto, Japan"},"type":"conference","status":"public","publication_status":"published","publication_identifier":{"isbn":["978-3-662-47665-9"]},"language":[{"iso":"eng"}],"ec_funded":1,"volume":9135,"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."}],"oa_version":"Preprint","main_file_link":[{"url":"http://arxiv.org/abs/1502.04844","open_access":"1"}],"scopus_import":"1","alternative_title":["LNCS"],"intvolume":" 9135","month":"06","citation":{"chicago":"Chatterjee, Krishnendu, Laurent Doyen, and Moshe Vardi. “The Complexity of Synthesis from Probabilistic Components.” In 42nd International Colloquium, 9135:108–20. Springer Nature, 2015. https://doi.org/10.1007/978-3-662-47666-6_9.","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.","mla":"Chatterjee, Krishnendu, et al. “The Complexity of Synthesis from Probabilistic Components.” 42nd International Colloquium, vol. 9135, Springer Nature, 2015, pp. 108–20, doi:10.1007/978-3-662-47666-6_9.","ama":"Chatterjee K, Doyen L, Vardi M. The complexity of synthesis from probabilistic components. In: 42nd International Colloquium. Vol 9135. Springer Nature; 2015:108-120. doi:10.1007/978-3-662-47666-6_9","apa":"Chatterjee, K., Doyen, L., & Vardi, M. (2015). The complexity of synthesis from probabilistic components. In 42nd International Colloquium (Vol. 9135, pp. 108–120). Kyoto, Japan: Springer Nature. https://doi.org/10.1007/978-3-662-47666-6_9","ieee":"K. Chatterjee, L. Doyen, and M. Vardi, “The complexity of synthesis from probabilistic components,” in 42nd International Colloquium, Kyoto, Japan, 2015, vol. 9135, pp. 108–120.","short":"K. Chatterjee, L. Doyen, M. Vardi, in:, 42nd International Colloquium, Springer Nature, 2015, pp. 108–120."},"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","article_processing_charge":"No","publist_id":"5557","author":[{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"last_name":"Doyen","full_name":"Doyen, Laurent","first_name":"Laurent"},{"first_name":"Moshe","full_name":"Vardi, Moshe","last_name":"Vardi"}],"title":"The complexity of synthesis from probabilistic components","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"}],"year":"2015","publication":"42nd International Colloquium","day":"20","page":"108 - 120","date_created":"2018-12-11T11:53:00Z","doi":"10.1007/978-3-662-47666-6_9","date_published":"2015-06-20T00:00:00Z","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.","oa":1,"publisher":"Springer Nature","quality_controlled":"1"},{"oa":1,"publisher":"Nature Publishing Group","quality_controlled":"1","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.","date_created":"2018-12-11T11:53:06Z","doi":"10.1038/srep17147","date_published":"2015-11-25T00:00:00Z","publication":"Scientific Reports","day":"25","year":"2015","has_accepted_license":"1","project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"article_number":"17147","title":"Cellular cooperation with shift updating and repulsion","publist_id":"5536","author":[{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"last_name":"Adlam","full_name":"Adlam, Ben","first_name":"Ben"},{"full_name":"Nowak, Martin","last_name":"Nowak","first_name":"Martin"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"chicago":"Pavlogiannis, Andreas, Krishnendu Chatterjee, Ben Adlam, and Martin Nowak. “Cellular Cooperation with Shift Updating and Repulsion.” Scientific Reports. Nature Publishing Group, 2015. https://doi.org/10.1038/srep17147.","ista":"Pavlogiannis A, Chatterjee K, Adlam B, Nowak M. 2015. Cellular cooperation with shift updating and repulsion. Scientific Reports. 5, 17147.","mla":"Pavlogiannis, Andreas, et al. “Cellular Cooperation with Shift Updating and Repulsion.” Scientific Reports, vol. 5, 17147, Nature Publishing Group, 2015, doi:10.1038/srep17147.","ieee":"A. Pavlogiannis, K. Chatterjee, B. Adlam, and M. Nowak, “Cellular cooperation with shift updating and repulsion,” Scientific Reports, vol. 5. Nature Publishing Group, 2015.","short":"A. Pavlogiannis, K. Chatterjee, B. Adlam, M. Nowak, Scientific Reports 5 (2015).","apa":"Pavlogiannis, A., Chatterjee, K., Adlam, B., & Nowak, M. (2015). Cellular cooperation with shift updating and repulsion. Scientific Reports. Nature Publishing Group. https://doi.org/10.1038/srep17147","ama":"Pavlogiannis A, Chatterjee K, Adlam B, Nowak M. Cellular cooperation with shift updating and repulsion. Scientific Reports. 2015;5. doi:10.1038/srep17147"},"intvolume":" 5","month":"11","scopus_import":1,"oa_version":"Published Version","abstract":[{"lang":"eng","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."}],"ec_funded":1,"volume":5,"language":[{"iso":"eng"}],"file":[{"file_name":"IST-2016-466-v1+1_srep17147.pdf","date_created":"2018-12-12T10:12:29Z","file_size":1021931,"date_updated":"2020-07-14T12:45:07Z","creator":"system","file_id":"4947","checksum":"38e06d8310d2087cae5f6d4d4bfe082b","content_type":"application/pdf","relation":"main_file","access_level":"open_access"}],"publication_status":"published","pubrep_id":"466","status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"type":"journal_article","_id":"1624","department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:45:07Z","ddc":["000"],"date_updated":"2021-01-12T06:52:05Z"},{"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"}],"oa_version":"Preprint","oa":1,"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1505.02655"}],"alternative_title":["LICS"],"scopus_import":1,"publisher":"IEEE","quality_controlled":"1","month":"07","year":"2015","publication_status":"published","language":[{"iso":"eng"}],"day":"01","page":"44 - 55","ec_funded":1,"date_created":"2018-12-11T11:53:19Z","doi":"10.1109/LICS.2015.15","date_published":"2015-07-01T00:00:00Z","_id":"1660","conference":{"name":"LICS: Logic in Computer Science","start_date":"2015-07-06","location":"Kyoto, Japan","end_date":"2015-07-10"},"type":"conference","status":"public","project":[{"_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme","grant_number":"291734"}],"citation":{"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.","short":"T. Brázdil, S. Kiefer, A. Kučera, P. Novotný, in:, IEEE, 2015, pp. 44–55.","apa":"Brázdil, T., Kiefer, S., Kučera, A., & 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. https://doi.org/10.1109/LICS.2015.15","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:10.1109/LICS.2015.15","mla":"Brázdil, Tomáš, et al. Long-Run Average Behaviour of Probabilistic Vector Addition Systems. IEEE, 2015, pp. 44–55, doi:10.1109/LICS.2015.15.","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.","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. https://doi.org/10.1109/LICS.2015.15."},"date_updated":"2021-01-12T06:52:20Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publist_id":"5490","author":[{"first_name":"Tomáš","last_name":"Brázdil","full_name":"Brázdil, Tomáš"},{"first_name":"Stefan","full_name":"Kiefer, Stefan","last_name":"Kiefer"},{"first_name":"Antonín","last_name":"Kučera","full_name":"Kučera, Antonín"},{"full_name":"Novotny, Petr","last_name":"Novotny","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","first_name":"Petr"}],"department":[{"_id":"KrCh"}],"title":"Long-run average behaviour of probabilistic vector addition systems"},{"title":"Mutations driving CLL and their evolution in progression and relapse","external_id":{"pmid":["26466571"]},"article_processing_charge":"No","publist_id":"5484","author":[{"last_name":"Landau","full_name":"Landau, Dan","first_name":"Dan"},{"first_name":"Eugen","last_name":"Tausch","full_name":"Tausch, Eugen"},{"first_name":"Amaro","full_name":"Taylor Weiner, Amaro","last_name":"Taylor Weiner"},{"first_name":"Chip","full_name":"Stewart, Chip","last_name":"Stewart"},{"first_name":"Johannes","id":"4A918E98-F248-11E8-B48F-1D18A9856A87","full_name":"Reiter, Johannes","orcid":"0000-0002-0170-7353","last_name":"Reiter"},{"last_name":"Bahlo","full_name":"Bahlo, Jasmin","first_name":"Jasmin"},{"first_name":"Sandra","last_name":"Kluth","full_name":"Kluth, Sandra"},{"first_name":"Ivana","last_name":"Božić","full_name":"Božić, Ivana"},{"first_name":"Michael","full_name":"Lawrence, Michael","last_name":"Lawrence"},{"first_name":"Sebastian","full_name":"Böttcher, Sebastian","last_name":"Böttcher"},{"first_name":"Scott","last_name":"Carter","full_name":"Carter, Scott"},{"last_name":"Cibulskis","full_name":"Cibulskis, Kristian","first_name":"Kristian"},{"last_name":"Mertens","full_name":"Mertens, Daniel","first_name":"Daniel"},{"first_name":"Carrie","last_name":"Sougnez","full_name":"Sougnez, Carrie"},{"first_name":"Mara","last_name":"Rosenberg","full_name":"Rosenberg, Mara"},{"last_name":"Hess","full_name":"Hess, Julian","first_name":"Julian"},{"full_name":"Edelmann, Jennifer","last_name":"Edelmann","first_name":"Jennifer"},{"last_name":"Kless","full_name":"Kless, Sabrina","first_name":"Sabrina"},{"full_name":"Kneba, Michael","last_name":"Kneba","first_name":"Michael"},{"first_name":"Matthias","full_name":"Ritgen, Matthias","last_name":"Ritgen"},{"last_name":"Fink","full_name":"Fink, Anna","first_name":"Anna"},{"full_name":"Fischer, Kirsten","last_name":"Fischer","first_name":"Kirsten"},{"full_name":"Gabriel, Stacey","last_name":"Gabriel","first_name":"Stacey"},{"last_name":"Lander","full_name":"Lander, Eric","first_name":"Eric"},{"full_name":"Nowak, Martin","last_name":"Nowak","first_name":"Martin"},{"last_name":"Döhner","full_name":"Döhner, Hartmut","first_name":"Hartmut"},{"first_name":"Michael","last_name":"Hallek","full_name":"Hallek, Michael"},{"first_name":"Donna","full_name":"Neuberg, Donna","last_name":"Neuberg"},{"last_name":"Getz","full_name":"Getz, Gad","first_name":"Gad"},{"full_name":"Stilgenbauer, Stephan","last_name":"Stilgenbauer","first_name":"Stephan"},{"last_name":"Wu","full_name":"Wu, Catherine","first_name":"Catherine"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"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.","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.” Nature. Nature Publishing Group, 2015. https://doi.org/10.1038/nature15395.","ieee":"D. Landau et al., “Mutations driving CLL and their evolution in progression and relapse,” Nature, vol. 526, no. 7574. Nature Publishing Group, pp. 525–530, 2015.","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.","ama":"Landau D, Tausch E, Taylor Weiner A, et al. Mutations driving CLL and their evolution in progression and relapse. Nature. 2015;526(7574):525-530. doi:10.1038/nature15395","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. Nature. Nature Publishing Group. https://doi.org/10.1038/nature15395","mla":"Landau, Dan, et al. “Mutations Driving CLL and Their Evolution in Progression and Relapse.” Nature, vol. 526, no. 7574, Nature Publishing Group, 2015, pp. 525–30, doi:10.1038/nature15395."},"project":[{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"date_created":"2018-12-11T11:53:21Z","date_published":"2015-10-22T00:00:00Z","doi":"10.1038/nature15395","page":"525 - 530","publication":"Nature","day":"22","year":"2015","oa":1,"publisher":"Nature Publishing Group","quality_controlled":"1","department":[{"_id":"KrCh"}],"date_updated":"2021-01-12T06:52:23Z","status":"public","article_type":"original","type":"journal_article","_id":"1665","ec_funded":1,"issue":"7574","volume":526,"language":[{"iso":"eng"}],"publication_status":"published","intvolume":" 526","month":"10","main_file_link":[{"open_access":"1","url":"https://www.ncbi.nlm.nih.gov/pmc/articles/PMC4815041/"}],"scopus_import":1,"oa_version":"Submitted Version","pmid":1,"abstract":[{"lang":"eng","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."}]},{"alternative_title":["LNCS"],"scopus_import":1,"main_file_link":[{"url":"http://arxiv.org/abs/1407.4777","open_access":"1"}],"month":"08","intvolume":" 9259","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."}],"oa_version":"Preprint","volume":9259,"ec_funded":1,"publication_status":"published","language":[{"iso":"eng"}],"type":"conference","conference":{"end_date":"2015-09-03","location":"Madrid, Spain","start_date":"2015-09-01","name":"QEST: Quantitative Evaluation of Systems"},"status":"public","series_title":"Lecture Notes in Computer Science","_id":"1667","department":[{"_id":"KrCh"}],"date_updated":"2021-01-12T06:52:24Z","quality_controlled":"1","publisher":"Springer","oa":1,"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.","page":"141 - 159","date_published":"2015-08-22T00:00:00Z","doi":"10.1007/978-3-319-22264-6_10","date_created":"2018-12-11T11:53:22Z","year":"2015","day":"22","project":[{"call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734","name":"International IST Postdoc Fellowship Programme"}],"author":[{"full_name":"Brázdil, Tomáš","last_name":"Brázdil","first_name":"Tomáš"},{"first_name":"L'Uboš","full_name":"Korenčiak, L'Uboš","last_name":"Korenčiak"},{"last_name":"Krčál","full_name":"Krčál, Jan","first_name":"Jan"},{"id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","first_name":"Petr","last_name":"Novotny","full_name":"Novotny, Petr"},{"last_name":"Řehák","full_name":"Řehák, Vojtěch","first_name":"Vojtěch"}],"publist_id":"5482","title":"Optimizing performance of continuous-time stochastic systems using timeout synthesis","citation":{"mla":"Brázdil, Tomáš, et al. Optimizing Performance of Continuous-Time Stochastic Systems Using Timeout Synthesis. Vol. 9259, Springer, 2015, pp. 141–59, doi:10.1007/978-3-319-22264-6_10.","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.","short":"T. Brázdil, L. Korenčiak, J. Krčál, P. Novotný, V. Řehák, 9259 (2015) 141–159.","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:10.1007/978-3-319-22264-6_10","apa":"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. Presented at the QEST: Quantitative Evaluation of Systems, Madrid, Spain: Springer. https://doi.org/10.1007/978-3-319-22264-6_10","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. https://doi.org/10.1007/978-3-319-22264-6_10.","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."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"day":"08","publication":"Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences","has_accepted_license":"1","year":"2015","doi":"10.1098/rspa.2015.0114","date_published":"2015-09-08T00:00:00Z","date_created":"2018-12-11T11:53:24Z","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","quality_controlled":"1","oa":1,"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","citation":{"ieee":"B. Adlam, K. Chatterjee, and M. Nowak, “Amplifiers of selection,” Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences, vol. 471, no. 2181. Royal Society of London, 2015.","short":"B. Adlam, K. Chatterjee, M. Nowak, Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences 471 (2015).","ama":"Adlam B, Chatterjee K, Nowak M. Amplifiers of selection. Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences. 2015;471(2181). doi:10.1098/rspa.2015.0114","apa":"Adlam, B., Chatterjee, K., & Nowak, M. (2015). Amplifiers of selection. Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences. Royal Society of London. https://doi.org/10.1098/rspa.2015.0114","mla":"Adlam, Ben, et al. “Amplifiers of Selection.” Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences, vol. 471, no. 2181, 20150114, Royal Society of London, 2015, doi:10.1098/rspa.2015.0114.","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.","chicago":"Adlam, Ben, Krishnendu Chatterjee, and Martin Nowak. “Amplifiers of Selection.” Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences. Royal Society of London, 2015. https://doi.org/10.1098/rspa.2015.0114."},"title":"Amplifiers of selection","publist_id":"5477","author":[{"full_name":"Adlam, Ben","last_name":"Adlam","first_name":"Ben"},{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"first_name":"Martin","last_name":"Nowak","full_name":"Nowak, Martin"}],"article_number":"20150114","project":[{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"file":[{"file_id":"6342","checksum":"e613d94d283c776322403a28aad11bdd","content_type":"application/pdf","access_level":"open_access","relation":"main_file","date_created":"2019-04-18T12:39:56Z","file_name":"2015_rspa_Adlam.pdf","date_updated":"2020-07-14T12:45:11Z","file_size":391466,"creator":"kschuh"}],"language":[{"iso":"eng"}],"publication_status":"published","issue":"2181","volume":471,"ec_funded":1,"oa_version":"Published Version","abstract":[{"lang":"eng","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. "}],"month":"09","intvolume":" 471","scopus_import":1,"ddc":["000"],"date_updated":"2021-01-12T06:52:26Z","department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:45:11Z","_id":"1673","status":"public","type":"journal_article"},{"title":"Temporal logic motion planning using POMDPs with parity objectives: Case study paper","department":[{"_id":"KrCh"}],"publist_id":"5453","author":[{"first_name":"Mária","last_name":"Svoreňová","full_name":"Svoreňová, Mária"},{"id":"3624234E-F248-11E8-B48F-1D18A9856A87","first_name":"Martin","full_name":"Chmelik, Martin","last_name":"Chmelik"},{"first_name":"Kevin","last_name":"Leahy","full_name":"Leahy, Kevin"},{"first_name":"Hasan","last_name":"Eniser","full_name":"Eniser, Hasan"},{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Cěrná","full_name":"Cěrná, Ivana","first_name":"Ivana"},{"last_name":"Belta","full_name":"Belta, Cǎlin","first_name":"Cǎlin"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ista":"Svoreňová M, Chmelik M, Leahy K, Eniser H, Chatterjee K, Cěrná I, Belta C. 2015. Temporal logic motion planning using POMDPs with parity objectives: Case study paper. Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems - Computation and Control, 233–238.","chicago":"Svoreňová, Mária, Martin Chmelik, Kevin Leahy, Hasan Eniser, Krishnendu Chatterjee, Ivana Cěrná, and Cǎlin Belta. “Temporal Logic Motion Planning Using POMDPs with Parity Objectives: Case Study Paper.” In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, 233–38. ACM, 2015. https://doi.org/10.1145/2728606.2728617.","ieee":"M. Svoreňová et al., “Temporal logic motion planning using POMDPs with parity objectives: Case study paper,” in Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, Seattle, WA, United States, 2015, pp. 233–238.","short":"M. Svoreňová, M. Chmelik, K. Leahy, H. Eniser, K. Chatterjee, I. Cěrná, C. Belta, in:, Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, ACM, 2015, pp. 233–238.","ama":"Svoreňová M, Chmelik M, Leahy K, et al. Temporal logic motion planning using POMDPs with parity objectives: Case study paper. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. ACM; 2015:233-238. doi:10.1145/2728606.2728617","apa":"Svoreňová, M., Chmelik, M., Leahy, K., Eniser, H., Chatterjee, K., Cěrná, I., & Belta, C. (2015). Temporal logic motion planning using POMDPs with parity objectives: Case study paper. In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control (pp. 233–238). Seattle, WA, United States: ACM. https://doi.org/10.1145/2728606.2728617","mla":"Svoreňová, Mária, et al. “Temporal Logic Motion Planning Using POMDPs with Parity Objectives: Case Study Paper.” Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, ACM, 2015, pp. 233–38, doi:10.1145/2728606.2728617."},"date_updated":"2021-01-12T06:52:33Z","project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"}],"status":"public","conference":{"name":"HSCC: Hybrid Systems - Computation and Control","start_date":"2015-04-14","end_date":"2015-04-16","location":"Seattle, WA, United States"},"type":"conference","_id":"1691","date_created":"2018-12-11T11:53:29Z","ec_funded":1,"doi":"10.1145/2728606.2728617","date_published":"2015-04-14T00:00:00Z","page":"233 - 238","publication":"Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control","language":[{"iso":"eng"}],"day":"14","publication_status":"published","year":"2015","month":"04","scopus_import":1,"publisher":"ACM","oa_version":"None","abstract":[{"text":"We consider a case study of the problem of deploying an autonomous air vehicle in a partially observable, dynamic, indoor environment from a specification given as a linear temporal logic (LTL) formula over regions of interest. We model the motion and sensing capabilities of the vehicle as a partially observable Markov decision process (POMDP). We adapt recent results for solving POMDPs with parity objectives to generate a control policy. We also extend the existing framework with a policy minimization technique to obtain a better implementable policy, while preserving its correctness. The proposed techniques are illustrated in an experimental setup involving an autonomous quadrotor performing surveillance in a dynamic environment.","lang":"eng"}]},{"abstract":[{"lang":"eng","text":"\r\nWe introduce quantitative timed refinement and timed simulation (directed) metrics, incorporating zenoness checks, for timed systems. These metrics assign positive real numbers which quantify the timing mismatches between two timed systems, amongst non-zeno runs. We quantify timing mismatches in three ways: (1) the maximal timing mismatch that can arise, (2) the “steady-state” maximal timing mismatches, where initial transient timing mismatches are ignored; and (3) the (long-run) average timing mismatches amongst two systems. These three kinds of mismatches constitute three important types of timing differences. Our event times are the global times, measured from the start of the system execution, not just the time durations of individual steps. We present algorithms over timed automata for computing the three quantitative simulation distances to within any desired degree of accuracy. In order to compute the values of the quantitative simulation distances, we use a game theoretic formulation. We introduce two new kinds of objectives for two player games on finite-state game graphs: (1) eventual debit-sum level objectives, and (2) average debit-sum level objectives. We present algorithms for computing the optimal values for these objectives in graph games, and then use these algorithms to compute the values of the timed simulation distances over timed automata.\r\n"}],"oa_version":"None","quality_controlled":"1","publisher":"IEEE","scopus_import":1,"intvolume":" 60","month":"02","publication_status":"published","year":"2015","language":[{"iso":"eng"}],"publication":"IEEE Transactions on Automatic Control","day":"24","page":"2291 - 2306","ec_funded":1,"date_created":"2018-12-11T11:53:30Z","volume":60,"date_published":"2015-02-24T00:00:00Z","doi":"10.1109/TAC.2015.2404612","issue":"9","_id":"1694","type":"journal_article","status":"public","project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"citation":{"chicago":"Chatterjee, Krishnendu, and Vinayak Prabhu. “Quantitative Temporal Simulation and Refinement Distances for Timed Systems.” IEEE Transactions on Automatic Control. IEEE, 2015. https://doi.org/10.1109/TAC.2015.2404612.","ista":"Chatterjee K, Prabhu V. 2015. Quantitative temporal simulation and refinement distances for timed systems. IEEE Transactions on Automatic Control. 60(9), 2291–2306.","mla":"Chatterjee, Krishnendu, and Vinayak Prabhu. “Quantitative Temporal Simulation and Refinement Distances for Timed Systems.” IEEE Transactions on Automatic Control, vol. 60, no. 9, IEEE, 2015, pp. 2291–306, doi:10.1109/TAC.2015.2404612.","short":"K. Chatterjee, V. Prabhu, IEEE Transactions on Automatic Control 60 (2015) 2291–2306.","ieee":"K. Chatterjee and V. Prabhu, “Quantitative temporal simulation and refinement distances for timed systems,” IEEE Transactions on Automatic Control, vol. 60, no. 9. IEEE, pp. 2291–2306, 2015.","apa":"Chatterjee, K., & Prabhu, V. (2015). Quantitative temporal simulation and refinement distances for timed systems. IEEE Transactions on Automatic Control. IEEE. https://doi.org/10.1109/TAC.2015.2404612","ama":"Chatterjee K, Prabhu V. Quantitative temporal simulation and refinement distances for timed systems. IEEE Transactions on Automatic Control. 2015;60(9):2291-2306. doi:10.1109/TAC.2015.2404612"},"date_updated":"2021-01-12T06:52:34Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publist_id":"5450","author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Vinayak","full_name":"Prabhu, Vinayak","last_name":"Prabhu"}],"title":"Quantitative temporal simulation and refinement distances for timed systems","department":[{"_id":"KrCh"}]},{"project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory","grant_number":"S11407"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"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"}],"title":"The complexity of multi-mean-payoff and multi-energy games","publist_id":"5443","author":[{"first_name":"Yaron","last_name":"Velner","full_name":"Velner, Yaron"},{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"full_name":"Doyen, Laurent","last_name":"Doyen","first_name":"Laurent"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"first_name":"Alexander","full_name":"Rabinovich, Alexander","last_name":"Rabinovich"},{"last_name":"Raskin","full_name":"Raskin, Jean","first_name":"Jean"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"mla":"Velner, Yaron, et al. “The Complexity of Multi-Mean-Payoff and Multi-Energy Games.” Information and Computation, vol. 241, no. 4, Elsevier, 2015, pp. 177–96, doi:10.1016/j.ic.2015.03.001.","apa":"Velner, Y., Chatterjee, K., Doyen, L., Henzinger, T. A., Rabinovich, A., & Raskin, J. (2015). The complexity of multi-mean-payoff and multi-energy games. Information and Computation. Elsevier. https://doi.org/10.1016/j.ic.2015.03.001","ama":"Velner Y, Chatterjee K, Doyen L, Henzinger TA, Rabinovich A, Raskin J. The complexity of multi-mean-payoff and multi-energy games. Information and Computation. 2015;241(4):177-196. doi:10.1016/j.ic.2015.03.001","ieee":"Y. Velner, K. Chatterjee, L. Doyen, T. A. Henzinger, A. Rabinovich, and J. Raskin, “The complexity of multi-mean-payoff and multi-energy games,” Information and Computation, vol. 241, no. 4. Elsevier, pp. 177–196, 2015.","short":"Y. Velner, K. Chatterjee, L. Doyen, T.A. Henzinger, A. Rabinovich, J. Raskin, Information and Computation 241 (2015) 177–196.","chicago":"Velner, Yaron, Krishnendu Chatterjee, Laurent Doyen, Thomas A Henzinger, Alexander Rabinovich, and Jean Raskin. “The Complexity of Multi-Mean-Payoff and Multi-Energy Games.” Information and Computation. Elsevier, 2015. https://doi.org/10.1016/j.ic.2015.03.001.","ista":"Velner Y, Chatterjee K, Doyen L, Henzinger TA, Rabinovich A, Raskin J. 2015. The complexity of multi-mean-payoff and multi-energy games. Information and Computation. 241(4), 177–196."},"oa":1,"publisher":"Elsevier","quality_controlled":"1","acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No P23499-N23, FWF NFN Grant No S11407-N23 and S11402-N23 (RiSE), ERC Start grant (279307: Graph Games), Microsoft faculty fellows award, the ERC Advanced Grant QUAREM (267989: Quantitative Reactive Modeling), European project Cassting (FP7-601148), ERC Start grant (279499: inVEST).","date_created":"2018-12-11T11:53:32Z","date_published":"2015-04-01T00:00:00Z","doi":"10.1016/j.ic.2015.03.001","page":"177 - 196","publication":"Information and Computation","day":"01","year":"2015","status":"public","type":"journal_article","_id":"1698","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"date_updated":"2021-01-12T06:52:36Z","intvolume":" 241","month":"04","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1209.3234"}],"scopus_import":1,"oa_version":"Preprint","abstract":[{"text":"In mean-payoff games, the objective of the protagonist is to ensure that the limit average of an infinite sequence of numeric weights is nonnegative. In energy games, the objective is to ensure that the running sum of weights is always nonnegative. Multi-mean-payoff and multi-energy games replace individual weights by tuples, and the limit average (resp., running sum) of each coordinate must be (resp., remain) nonnegative. We prove finite-memory determinacy of multi-energy games and show inter-reducibility of multi-mean-payoff and multi-energy games for finite-memory strategies. We improve the computational complexity for solving both classes with finite-memory strategies: we prove coNP-completeness improving the previous known EXPSPACE bound. For memoryless strategies, we show that deciding the existence of a winning strategy for the protagonist is NP-complete. We present the first solution of multi-mean-payoff games with infinite-memory strategies: we show that mean-payoff-sup objectives can be decided in NP∩coNP, whereas mean-payoff-inf objectives are coNP-complete.","lang":"eng"}],"ec_funded":1,"issue":"4","volume":241,"language":[{"iso":"eng"}],"publication_status":"published"},{"page":"3496-3502","date_created":"2018-12-11T11:54:11Z","date_published":"2015-06-01T00:00:00Z","year":"2015","publication":"Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence ","day":"01","oa":1,"publisher":"AAAI Press","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), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.","external_id":{"arxiv":["1411.3880"]},"author":[{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"3624234E-F248-11E8-B48F-1D18A9856A87","first_name":"Martin","last_name":"Chmelik","full_name":"Chmelik, Martin"},{"last_name":"Gupta","full_name":"Gupta, Raghav","first_name":"Raghav"},{"full_name":"Kanodia, Ayush","last_name":"Kanodia","first_name":"Ayush"}],"publist_id":"5286","title":"Optimal cost almost-sure reachability in POMDPs","citation":{"mla":"Chatterjee, Krishnendu, et al. “Optimal Cost Almost-Sure Reachability in POMDPs.” Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence , vol. 5, AAAI Press, 2015, pp. 3496–502.","ama":"Chatterjee K, Chmelik M, Gupta R, Kanodia A. Optimal cost almost-sure reachability in POMDPs. In: Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence . Vol 5. AAAI Press; 2015:3496-3502.","apa":"Chatterjee, K., Chmelik, M., Gupta, R., & Kanodia, A. (2015). Optimal cost almost-sure reachability in POMDPs. In Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence (Vol. 5, pp. 3496–3502). Austin, TX, USA: AAAI Press.","short":"K. Chatterjee, M. Chmelik, R. Gupta, A. Kanodia, in:, Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence , AAAI Press, 2015, pp. 3496–3502.","ieee":"K. Chatterjee, M. Chmelik, R. Gupta, and A. Kanodia, “Optimal cost almost-sure reachability in POMDPs,” in Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence , Austin, TX, USA, 2015, vol. 5, pp. 3496–3502.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, Raghav Gupta, and Ayush Kanodia. “Optimal Cost Almost-Sure Reachability in POMDPs.” In Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence , 5:3496–3502. AAAI Press, 2015.","ista":"Chatterjee K, Chmelik M, Gupta R, Kanodia A. 2015. Optimal cost almost-sure reachability in POMDPs. Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence . IAAI: Innovative Applications of Artificial Intelligence, Artifical Intelligence, vol. 5, 3496–3502."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"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"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"ec_funded":1,"volume":5,"related_material":{"record":[{"relation":"later_version","id":"1529","status":"public"}]},"publication_status":"published","language":[{"iso":"eng"}],"main_file_link":[{"url":"http://arxiv.org/abs/1411.3880","open_access":"1"}],"alternative_title":["Artifical Intelligence"],"scopus_import":1,"intvolume":" 5","month":"06","abstract":[{"text":"We consider partially observable Markov decision processes (POMDPs) with a set of target states and every transition is associated with an integer cost. The optimization objec- tive we study asks to minimize the expected total cost till the target set is reached, while ensuring that the target set is reached almost-surely (with probability 1). We show that for integer costs approximating the optimal cost is undecidable. For positive costs, our results are as follows: (i) we establish matching lower and upper bounds for the optimal cost and the bound is double exponential; (ii) we show that the problem of approximating the optimal cost is decidable and present ap- proximation algorithms developing on the existing algorithms for POMDPs with finite-horizon objectives. While the worst- case running time of our algorithm is double exponential, we present efficient stopping criteria for the algorithm and show experimentally that it performs well in many examples.","lang":"eng"}],"oa_version":"Preprint","department":[{"_id":"KrCh"}],"date_updated":"2023-02-23T10:02:57Z","conference":{"name":"IAAI: Innovative Applications of Artificial Intelligence","end_date":"2015-01-30","location":"Austin, TX, USA","start_date":"2015-01-25"},"type":"conference","status":"public","_id":"1820"},{"citation":{"ista":"Bloem R, Chatterjee K, Jacobs S, Könighofer R. 2015. Assume-guarantee synthesis for concurrent reactive programs with partial information. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 9035, 517–532.","chicago":"Bloem, Roderick, Krishnendu Chatterjee, Swen Jacobs, and Robert Könighofer. “Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information,” 9035:517–32. Springer, 2015. https://doi.org/10.1007/978-3-662-46681-0_50.","short":"R. Bloem, K. Chatterjee, S. Jacobs, R. Könighofer, in:, Springer, 2015, pp. 517–532.","ieee":"R. Bloem, K. Chatterjee, S. Jacobs, and R. Könighofer, “Assume-guarantee synthesis for concurrent reactive programs with partial information,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, London, United Kingdom, 2015, vol. 9035, pp. 517–532.","ama":"Bloem R, Chatterjee K, Jacobs S, Könighofer R. Assume-guarantee synthesis for concurrent reactive programs with partial information. In: Vol 9035. Springer; 2015:517-532. doi:10.1007/978-3-662-46681-0_50","apa":"Bloem, R., Chatterjee, K., Jacobs, S., & Könighofer, R. (2015). Assume-guarantee synthesis for concurrent reactive programs with partial information (Vol. 9035, pp. 517–532). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, London, United Kingdom: Springer. https://doi.org/10.1007/978-3-662-46681-0_50","mla":"Bloem, Roderick, et al. Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information. Vol. 9035, Springer, 2015, pp. 517–32, doi:10.1007/978-3-662-46681-0_50."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publist_id":"5264","author":[{"first_name":"Roderick","full_name":"Bloem, Roderick","last_name":"Bloem"},{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"first_name":"Swen","last_name":"Jacobs","full_name":"Jacobs, Swen"},{"first_name":"Robert","full_name":"Könighofer, Robert","last_name":"Könighofer"}],"title":"Assume-guarantee synthesis for concurrent reactive programs with partial information","project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"year":"2015","day":"01","page":"517 - 532","date_created":"2018-12-11T11:54:17Z","date_published":"2015-01-01T00:00:00Z","doi":"10.1007/978-3-662-46681-0_50","acknowledgement":"This work was supported by the Austrian Science Fund (FWF) through the research network RiSE (S11406-N23, S11407-N23) and grant nr. P23499-N23, by the European Commission through an ERC Start grant (279307: Graph Games) and project STANCE (317753), as well as by the German Research Foundation (DFG) through SFB/TR 14 AVACS and project ASDPS(JA 2357/2-1).","oa":1,"publisher":"Springer","date_updated":"2021-01-12T06:53:32Z","department":[{"_id":"KrCh"}],"_id":"1838","conference":{"start_date":"2015-04-11","end_date":"2015-04-18","location":"London, United Kingdom","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"type":"conference","status":"public","publication_status":"published","language":[{"iso":"eng"}],"ec_funded":1,"volume":9035,"abstract":[{"lang":"eng","text":"Synthesis of program parts is particularly useful for concurrent systems. However, most approaches do not support common design tasks, like modifying a single process without having to re-synthesize or verify the whole system. Assume-guarantee synthesis (AGS) provides robustness against modifications of system parts, but thus far has been limited to the perfect information setting. This means that local variables cannot be hidden from other processes, which renders synthesis results cumbersome or even impossible to realize.We resolve this shortcoming by defining AGS under partial information. We analyze the complexity and decidability in different settings, showing that the problem has a high worstcase complexity and is undecidable in many interesting cases. Based on these observations, we present a pragmatic algorithm based on bounded synthesis, and demonstrate its practical applicability on several examples."}],"oa_version":"Preprint","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1411.4604"}],"scopus_import":1,"alternative_title":["LNCS"],"intvolume":" 9035","month":"01"},{"ec_funded":1,"volume":9035,"publication_status":"published","language":[{"iso":"eng"}],"main_file_link":[{"url":"http://arxiv.org/abs/1501.03093","open_access":"1"}],"alternative_title":["LNCS"],"intvolume":" 9035","month":"01","abstract":[{"lang":"eng","text":"We present MultiGain, a tool to synthesize strategies for Markov decision processes (MDPs) with multiple mean-payoff objectives. Our models are described in PRISM, and our tool uses the existing interface and simulator of PRISM. Our tool extends PRISM by adding novel algorithms for multiple mean-payoff objectives, and also provides features such as (i) generating strategies and exploring them for simulation, and checking them with respect to other properties; and (ii) generating an approximate Pareto curve for two mean-payoff objectives. In addition, we present a new practical algorithm for the analysis of MDPs with multiple mean-payoff objectives under memoryless strategies."}],"oa_version":"Preprint","department":[{"_id":"KrCh"}],"date_updated":"2020-01-21T13:18:52Z","conference":{"location":"London, United Kingdom","end_date":"2015-04-18","start_date":"2015-04-11","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"type":"conference","status":"public","_id":"1839","series_title":"Lecture Notes in Computer Science","page":"181 - 187","date_created":"2018-12-11T11:54:18Z","date_published":"2015-01-01T00:00:00Z","doi":"10.1007/978-3-662-46681-0_12","year":"2015","day":"01","oa":1,"quality_controlled":"1","publisher":"Springer","publist_id":"5263","author":[{"first_name":"Tomáš","last_name":"Brázdil","full_name":"Brázdil, Tomáš"},{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Forejt","full_name":"Forejt, Vojtěch","first_name":"Vojtěch"},{"last_name":"Kučera","full_name":"Kučera, Antonín","first_name":"Antonín"}],"title":"Multigain: A controller synthesis tool for MDPs with multiple mean-payoff objectives","citation":{"mla":"Brázdil, Tomáš, et al. Multigain: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives. Vol. 9035, Springer, 2015, pp. 181–87, doi:10.1007/978-3-662-46681-0_12.","ieee":"T. Brázdil, K. Chatterjee, V. Forejt, and A. Kučera, “Multigain: A controller synthesis tool for MDPs with multiple mean-payoff objectives,” vol. 9035. Springer, pp. 181–187, 2015.","short":"T. Brázdil, K. Chatterjee, V. Forejt, A. Kučera, 9035 (2015) 181–187.","ama":"Brázdil T, Chatterjee K, Forejt V, Kučera A. Multigain: A controller synthesis tool for MDPs with multiple mean-payoff objectives. 2015;9035:181-187. doi:10.1007/978-3-662-46681-0_12","apa":"Brázdil, T., Chatterjee, K., Forejt, V., & Kučera, A. (2015). Multigain: A controller synthesis tool for MDPs with multiple mean-payoff objectives. Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, London, United Kingdom: Springer. https://doi.org/10.1007/978-3-662-46681-0_12","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Vojtěch Forejt, and Antonín Kučera. “Multigain: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives.” Lecture Notes in Computer Science. Springer, 2015. https://doi.org/10.1007/978-3-662-46681-0_12.","ista":"Brázdil T, Chatterjee K, Forejt V, Kučera A. 2015. Multigain: A controller synthesis tool for MDPs with multiple mean-payoff objectives. 9035, 181–187."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"}]},{"publist_id":"5255","author":[{"first_name":"Nikola","full_name":"Beneš, Nikola","last_name":"Beneš"},{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan","last_name":"Kretinsky"},{"full_name":"Larsen, Kim","last_name":"Larsen","first_name":"Kim"},{"first_name":"Mikael","full_name":"Möller, Mikael","last_name":"Möller"},{"last_name":"Sickert","full_name":"Sickert, Salomon","first_name":"Salomon"},{"last_name":"Srba","full_name":"Srba, Jiří","first_name":"Jiří"}],"article_processing_charge":"No","title":"Refinement checking on parametric modal transition systems","citation":{"ista":"Beneš N, Kretinsky J, Larsen K, Möller M, Sickert S, Srba J. 2015. Refinement checking on parametric modal transition systems. Acta Informatica. 52(2–3), 269–297.","chicago":"Beneš, Nikola, Jan Kretinsky, Kim Larsen, Mikael Möller, Salomon Sickert, and Jiří Srba. “Refinement Checking on Parametric Modal Transition Systems.” Acta Informatica. Springer, 2015. https://doi.org/10.1007/s00236-015-0215-4.","short":"N. Beneš, J. Kretinsky, K. Larsen, M. Möller, S. Sickert, J. Srba, Acta Informatica 52 (2015) 269–297.","ieee":"N. Beneš, J. Kretinsky, K. Larsen, M. Möller, S. Sickert, and J. Srba, “Refinement checking on parametric modal transition systems,” Acta Informatica, vol. 52, no. 2–3. Springer, pp. 269–297, 2015.","ama":"Beneš N, Kretinsky J, Larsen K, Möller M, Sickert S, Srba J. Refinement checking on parametric modal transition systems. Acta Informatica. 2015;52(2-3):269-297. doi:10.1007/s00236-015-0215-4","apa":"Beneš, N., Kretinsky, J., Larsen, K., Möller, M., Sickert, S., & Srba, J. (2015). Refinement checking on parametric modal transition systems. Acta Informatica. Springer. https://doi.org/10.1007/s00236-015-0215-4","mla":"Beneš, Nikola, et al. “Refinement Checking on Parametric Modal Transition Systems.” Acta Informatica, vol. 52, no. 2–3, Springer, 2015, pp. 269–97, doi:10.1007/s00236-015-0215-4."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"}],"page":"269 - 297","date_published":"2015-04-01T00:00:00Z","doi":"10.1007/s00236-015-0215-4","date_created":"2018-12-11T11:54:20Z","has_accepted_license":"1","year":"2015","day":"01","publication":"Acta Informatica","publisher":"Springer","quality_controlled":"1","oa":1,"file_date_updated":"2020-07-14T12:45:19Z","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"date_updated":"2021-01-12T06:53:35Z","ddc":["000"],"article_type":"original","type":"journal_article","status":"public","_id":"1846","issue":"2-3","volume":52,"ec_funded":1,"publication_status":"published","file":[{"file_id":"7854","checksum":"fb4037ddc4fc05f33080dd3547ede350","content_type":"application/pdf","relation":"main_file","access_level":"open_access","file_name":"2015_ActaInfo_Benes.pdf","date_created":"2020-05-15T08:57:44Z","file_size":488482,"date_updated":"2020-07-14T12:45:19Z","creator":"dernst"}],"language":[{"iso":"eng"}],"scopus_import":1,"month":"04","intvolume":" 52","abstract":[{"lang":"eng","text":"Modal transition systems (MTS) is a well-studied specification formalism of reactive systems supporting a step-wise refinement methodology. Despite its many advantages, the formalism as well as its currently known extensions are incapable of expressing some practically needed aspects in the refinement process like exclusive, conditional and persistent choices. We introduce a new model called parametric modal transition systems (PMTS) together with a general modal refinement notion that overcomes many of the limitations. We investigate the computational complexity of modal and thorough refinement checking on PMTS and its subclasses and provide a direct encoding of the modal refinement problem into quantified Boolean formulae, allowing us to employ state-of-the-art QBF solvers for modal refinement checking. The experiments we report on show that the feasibility of refinement checking is more influenced by the degree of nondeterminism rather than by the syntactic restrictions on the types of formulae allowed in the description of the PMTS."}],"oa_version":"Submitted Version"},{"publication_identifier":{"issn":["0014-3820"],"eissn":["1558-5646"]},"publication_status":"published","file":[{"date_created":"2020-05-15T09:05:34Z","file_name":"2015_Evolution_Priklopil.pdf","date_updated":"2020-07-14T12:45:19Z","file_size":967214,"creator":"dernst","checksum":"1e8be0b1d7598a78cd2623d8ee8e7798","file_id":"7855","content_type":"application/pdf","access_level":"open_access","relation":"main_file"}],"language":[{"iso":"eng"}],"issue":"4","volume":69,"ec_funded":1,"abstract":[{"lang":"eng","text":"We consider mating strategies for females who search for males sequentially during a season of limited length. We show that the best strategy rejects a given male type if encountered before a time-threshold but accepts him after. For frequency-independent benefits, we obtain the optimal time-thresholds explicitly for both discrete and continuous distributions of males, and allow for mistakes being made in assessing the correct male type. When the benefits are indirect (genes for the offspring) and the population is under frequency-dependent ecological selection, the benefits depend on the mating strategy of other females as well. This case is particularly relevant to speciation models that seek to explore the stability of reproductive isolation by assortative mating under frequency-dependent ecological selection. We show that the indirect benefits are to be quantified by the reproductive values of couples, and describe how the evolutionarily stable time-thresholds can be found. We conclude with an example based on the Levene model, in which we analyze the evolutionarily stable assortative mating strategies and the strength of reproductive isolation provided by them."}],"oa_version":"Submitted Version","pmid":1,"scopus_import":"1","month":"02","intvolume":" 69","date_updated":"2022-06-07T10:52:37Z","ddc":["570"],"file_date_updated":"2020-07-14T12:45:19Z","department":[{"_id":"NiBa"},{"_id":"KrCh"}],"_id":"1851","article_type":"original","type":"journal_article","status":"public","has_accepted_license":"1","year":"2015","day":"09","publication":"Evolution","page":"1015 - 1026","date_published":"2015-02-09T00:00:00Z","doi":"10.1111/evo.12618","date_created":"2018-12-11T11:54:21Z","quality_controlled":"1","publisher":"Wiley","oa":1,"citation":{"chicago":"Priklopil, Tadeas, Eva Kisdi, and Mats Gyllenberg. “Evolutionarily Stable Mating Decisions for Sequentially Searching Females and the Stability of Reproductive Isolation by Assortative Mating.” Evolution. Wiley, 2015. https://doi.org/10.1111/evo.12618.","ista":"Priklopil T, Kisdi E, Gyllenberg M. 2015. Evolutionarily stable mating decisions for sequentially searching females and the stability of reproductive isolation by assortative mating. Evolution. 69(4), 1015–1026.","mla":"Priklopil, Tadeas, et al. “Evolutionarily Stable Mating Decisions for Sequentially Searching Females and the Stability of Reproductive Isolation by Assortative Mating.” Evolution, vol. 69, no. 4, Wiley, 2015, pp. 1015–26, doi:10.1111/evo.12618.","apa":"Priklopil, T., Kisdi, E., & Gyllenberg, M. (2015). Evolutionarily stable mating decisions for sequentially searching females and the stability of reproductive isolation by assortative mating. Evolution. Wiley. https://doi.org/10.1111/evo.12618","ama":"Priklopil T, Kisdi E, Gyllenberg M. Evolutionarily stable mating decisions for sequentially searching females and the stability of reproductive isolation by assortative mating. Evolution. 2015;69(4):1015-1026. doi:10.1111/evo.12618","short":"T. Priklopil, E. Kisdi, M. Gyllenberg, Evolution 69 (2015) 1015–1026.","ieee":"T. Priklopil, E. Kisdi, and M. Gyllenberg, “Evolutionarily stable mating decisions for sequentially searching females and the stability of reproductive isolation by assortative mating,” Evolution, vol. 69, no. 4. Wiley, pp. 1015–1026, 2015."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"first_name":"Tadeas","id":"3C869AA0-F248-11E8-B48F-1D18A9856A87","full_name":"Priklopil, Tadeas","last_name":"Priklopil"},{"first_name":"Eva","last_name":"Kisdi","full_name":"Kisdi, Eva"},{"first_name":"Mats","last_name":"Gyllenberg","full_name":"Gyllenberg, Mats"}],"publist_id":"5249","article_processing_charge":"No","external_id":{"pmid":["25662095"]},"title":"Evolutionarily stable mating decisions for sequentially searching females and the stability of reproductive isolation by assortative mating","project":[{"name":"International IST Postdoc Fellowship Programme","grant_number":"291734","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425"}]}]