[{"scopus_import":"1","quality_controlled":"1","date_created":"2018-12-11T11:53:06Z","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"volume":5,"status":"public","citation":{"ista":"Pavlogiannis A, Chatterjee K, Adlam B, Nowak M. 2015. Cellular cooperation with shift updating and repulsion. Scientific Reports. 5, 17147.","short":"A. Pavlogiannis, K. Chatterjee, B. Adlam, M. Nowak, Scientific Reports 5 (2015).","ama":"Pavlogiannis A, Chatterjee K, Adlam B, Nowak M. Cellular cooperation with shift updating and repulsion. <i>Scientific Reports</i>. 2015;5. doi:<a href=\"https://doi.org/10.1038/srep17147\">10.1038/srep17147</a>","mla":"Pavlogiannis, Andreas, et al. “Cellular Cooperation with Shift Updating and Repulsion.” <i>Scientific Reports</i>, vol. 5, 17147, Nature Publishing Group, 2015, doi:<a href=\"https://doi.org/10.1038/srep17147\">10.1038/srep17147</a>.","ieee":"A. Pavlogiannis, K. Chatterjee, B. Adlam, and M. Nowak, “Cellular cooperation with shift updating and repulsion,” <i>Scientific Reports</i>, vol. 5. Nature Publishing Group, 2015.","apa":"Pavlogiannis, A., Chatterjee, K., Adlam, B., &#38; Nowak, M. (2015). Cellular cooperation with shift updating and repulsion. <i>Scientific Reports</i>. Nature Publishing Group. <a href=\"https://doi.org/10.1038/srep17147\">https://doi.org/10.1038/srep17147</a>","chicago":"Pavlogiannis, Andreas, Krishnendu Chatterjee, Ben Adlam, and Martin Nowak. “Cellular Cooperation with Shift Updating and Repulsion.” <i>Scientific Reports</i>. Nature Publishing Group, 2015. <a href=\"https://doi.org/10.1038/srep17147\">https://doi.org/10.1038/srep17147</a>."},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","year":"2015","type":"journal_article","title":"Cellular cooperation with shift updating and repulsion","corr_author":"1","publication":"Scientific Reports","language":[{"iso":"eng"}],"file":[{"file_name":"IST-2016-466-v1+1_srep17147.pdf","checksum":"38e06d8310d2087cae5f6d4d4bfe082b","relation":"main_file","file_size":1021931,"content_type":"application/pdf","date_created":"2018-12-12T10:12:29Z","date_updated":"2020-07-14T12:45:07Z","access_level":"open_access","file_id":"4947","creator":"system"}],"intvolume":"         5","publist_id":"5536","date_published":"2015-11-25T00:00:00Z","article_number":"17147","department":[{"_id":"KrCh"}],"isi":1,"license":"https://creativecommons.org/licenses/by/4.0/","day":"25","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"_id":"1624","publication_status":"published","publisher":"Nature Publishing Group","author":[{"id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","first_name":"Andreas"},{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"last_name":"Adlam","first_name":"Ben","full_name":"Adlam, Ben"},{"last_name":"Nowak","full_name":"Nowak, Martin","first_name":"Martin"}],"external_id":{"isi":["000365299500001"]},"article_processing_charge":"No","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."}],"doi":"10.1038/srep17147","ddc":["000"],"ec_funded":1,"month":"11","date_updated":"2025-09-23T08:13:52Z","has_accepted_license":"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.","oa":1,"pubrep_id":"466","file_date_updated":"2020-07-14T12:45:07Z","oa_version":"Published Version"},{"date_updated":"2025-09-23T09:39:59Z","month":"07","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.1606.03598"}],"OA_type":"green","acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF) projects S11402-N23 (RiSE), Z211-N23 (Wittgenstein Award), FWF Grant No P23499- N23, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.\r\nA Technical Report of the paper is available at: \r\nhttps://repository.ist.ac.at/331/\r\n","oa":1,"oa_version":"Preprint","external_id":{"arxiv":["1606.03598"],"isi":["000380427100064"]},"_id":"1656","publication_status":"published","author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","first_name":"Thomas A"},{"first_name":"Jan","full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop"}],"publisher":"IEEE","conference":{"name":"LICS: Logic in Computer Science","start_date":"2015-07-06","location":"Kyoto, Japan","end_date":"2015-07-10"},"day":"31","project":[{"grant_number":"267989","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling"},{"grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"},{"name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","grant_number":"P 23499-N23"},{"call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"abstract":[{"lang":"eng","text":"Recently there has been a significant effort to handle quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, perhaps surprisingly, some basic system properties such as average response time cannot be expressed using weighted automata, nor in any other know decidable formalism. In this work, we introduce nested weighted automata as a natural extension of weighted automata which makes it possible to express important quantitative properties such as average response time. In nested weighted automata, a master automaton spins off and collects results from weighted slave automata, each of which computes a quantity along a finite portion of an infinite word. Nested weighted automata can be viewed as the quantitative analogue of monitor automata, which are used in run-time verification. We establish an almost complete decidability picture for the basic decision problems about nested weighted automata, and illustrate their applicability in several domains. In particular, nested weighted automata can be used to decide average response time properties."}],"article_processing_charge":"No","doi":"10.1109/LICS.2015.72","ec_funded":1,"publist_id":"5494","arxiv":1,"date_published":"2015-07-31T00:00:00Z","article_number":"7174926","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"isi":1,"OA_place":"repository","date_created":"2018-12-11T11:53:17Z","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"5415"},{"relation":"earlier_version","status":"public","id":"5436"},{"relation":"later_version","id":"467","status":"public"}]},"quality_controlled":"1","scopus_import":"1","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","citation":{"ista":"Chatterjee K, Henzinger TA, Otop J. 2015. Nested weighted automata. Proceedings - Symposium on Logic in Computer Science. LICS: Logic in Computer Science vol. 2015–July, 7174926.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Proceedings - Symposium on Logic in Computer Science, IEEE, 2015.","mla":"Chatterjee, Krishnendu, et al. “Nested Weighted Automata.” <i>Proceedings - Symposium on Logic in Computer Science</i>, vol. 2015–July, 7174926, IEEE, 2015, doi:<a href=\"https://doi.org/10.1109/LICS.2015.72\">10.1109/LICS.2015.72</a>.","ama":"Chatterjee K, Henzinger TA, Otop J. Nested weighted automata. In: <i>Proceedings - Symposium on Logic in Computer Science</i>. Vol 2015-July. IEEE; 2015. doi:<a href=\"https://doi.org/10.1109/LICS.2015.72\">10.1109/LICS.2015.72</a>","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2015). Nested weighted automata. In <i>Proceedings - Symposium on Logic in Computer Science</i> (Vol. 2015–July). Kyoto, Japan: IEEE. <a href=\"https://doi.org/10.1109/LICS.2015.72\">https://doi.org/10.1109/LICS.2015.72</a>","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted automata,” in <i>Proceedings - Symposium on Logic in Computer Science</i>, Kyoto, Japan, 2015, vol. 2015–July.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted Automata.” In <i>Proceedings - Symposium on Logic in Computer Science</i>, Vol. 2015–July. IEEE, 2015. <a href=\"https://doi.org/10.1109/LICS.2015.72\">https://doi.org/10.1109/LICS.2015.72</a>."},"volume":"2015-July","status":"public","year":"2015","type":"conference","language":[{"iso":"eng"}],"title":"Nested weighted automata","corr_author":"1","publication":"Proceedings - Symposium on Logic in Computer Science"},{"isi":1,"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"OA_place":"repository","publist_id":"5493","alternative_title":["LICS"],"date_published":"2015-07-01T00:00:00Z","page":"244 - 256","type":"conference","year":"2015","title":"Unifying two views on multiple mean-payoff objectives in Markov decision processes","language":[{"iso":"eng"}],"scopus_import":"1","quality_controlled":"1","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"5429"},{"status":"public","id":"5435","relation":"earlier_version"},{"status":"public","id":"466","relation":"later_version"}]},"series_title":"LICS","date_created":"2018-12-11T11:53:18Z","status":"public","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","citation":{"chicago":"Chatterjee, Krishnendu, Zuzana Komárková, and Jan Kretinsky. “Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.” LICS. IEEE, 2015. <a href=\"https://doi.org/10.1109/LICS.2015.32\">https://doi.org/10.1109/LICS.2015.32</a>.","apa":"Chatterjee, K., Komárková, Z., &#38; Kretinsky, J. (2015). Unifying two views on multiple mean-payoff objectives in Markov decision processes. Presented at the LICS: Logic in Computer Science, Kyoto, Japan: IEEE. <a href=\"https://doi.org/10.1109/LICS.2015.32\">https://doi.org/10.1109/LICS.2015.32</a>","ieee":"K. Chatterjee, Z. Komárková, and J. Kretinsky, “Unifying two views on multiple mean-payoff objectives in Markov decision processes.” IEEE, pp. 244–256, 2015.","mla":"Chatterjee, Krishnendu, et al. <i>Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes</i>. IEEE, 2015, pp. 244–56, doi:<a href=\"https://doi.org/10.1109/LICS.2015.32\">10.1109/LICS.2015.32</a>.","ama":"Chatterjee K, Komárková Z, Kretinsky J. Unifying two views on multiple mean-payoff objectives in Markov decision processes. 2015:244-256. doi:<a href=\"https://doi.org/10.1109/LICS.2015.32\">10.1109/LICS.2015.32</a>","short":"K. Chatterjee, Z. Komárková, J. Kretinsky, (2015) 244–256.","ista":"Chatterjee K, Komárková Z, Kretinsky J. 2015. Unifying two views on multiple mean-payoff objectives in Markov decision processes. , 244–256."},"oa":1,"oa_version":"Preprint","month":"07","date_updated":"2025-09-29T11:00:43Z","acknowledgement":"A Technical Report of this paper is available at DOI: 10.15479/AT:IST-2015-318-v1-1\r\n","main_file_link":[{"open_access":"1","url":"https://doi.org/10.15479/AT:IST-2015-318-v1-1"}],"OA_type":"green","ec_funded":1,"project":[{"call_identifier":"FWF","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"},{"name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","call_identifier":"FWF"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7","grant_number":"267989"},{"grant_number":"291734","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme"}],"day":"01","conference":{"name":"LICS: Logic in Computer Science","location":"Kyoto, Japan","start_date":"2015-07-06","end_date":"2015-07-10"},"external_id":{"isi":["000380427100024"]},"_id":"1657","publication_status":"published","publisher":"IEEE","author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"last_name":"Komárková","first_name":"Zuzana","full_name":"Komárková, Zuzana"},{"first_name":"Jan","full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky"}],"doi":"10.1109/LICS.2015.32","abstract":[{"text":"We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. There exist two different views: (i) ~the expectation semantics, where the goal is to optimize the expected mean-payoff objective, and (ii) ~the satisfaction semantics, where the goal is to maximize the probability of runs such that the mean-payoff value stays above a given vector. We consider optimization with respect to both objectives at once, thus unifying the existing semantics. Precisely, the goal is to optimize the expectation while ensuring the satisfaction constraint. Our problem captures the notion of optimization with respect to strategies that are risk-averse (i.e., Ensure certain probabilistic guarantee). Our main results are as follows: First, we present algorithms for the decision problems, which are always polynomial in the size of the MDP. We also show that an approximation of the Pareto curve can be computed in time polynomial in the size of the MDP, and the approximation factor, but exponential in the number of dimensions. Second, we present a complete characterization of the strategy complexity (in terms of memory bounds and randomization) required to solve our problem. ","lang":"eng"}],"article_processing_charge":"No"},{"title":"Long-run average behaviour of probabilistic vector addition systems","language":[{"iso":"eng"}],"year":"2015","type":"conference","status":"public","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","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.","apa":"Brázdil, T., Kiefer, S., Kučera, A., &#38; Novotný, P. (2015). Long-run average behaviour of probabilistic vector addition systems (pp. 44–55). Presented at the LICS: Logic in Computer Science, Kyoto, Japan: IEEE. <a href=\"https://doi.org/10.1109/LICS.2015.15\">https://doi.org/10.1109/LICS.2015.15</a>","chicago":"Brázdil, Tomáš, Stefan Kiefer, Antonín Kučera, and Petr Novotný. “Long-Run Average Behaviour of Probabilistic Vector Addition Systems,” 44–55. IEEE, 2015. <a href=\"https://doi.org/10.1109/LICS.2015.15\">https://doi.org/10.1109/LICS.2015.15</a>.","short":"T. Brázdil, S. Kiefer, A. Kučera, P. Novotný, in:, IEEE, 2015, pp. 44–55.","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.","ama":"Brázdil T, Kiefer S, Kučera A, Novotný P. Long-run average behaviour of probabilistic vector addition systems. In: IEEE; 2015:44-55. doi:<a href=\"https://doi.org/10.1109/LICS.2015.15\">10.1109/LICS.2015.15</a>","mla":"Brázdil, Tomáš, et al. <i>Long-Run Average Behaviour of Probabilistic Vector Addition Systems</i>. IEEE, 2015, pp. 44–55, doi:<a href=\"https://doi.org/10.1109/LICS.2015.15\">10.1109/LICS.2015.15</a>."},"quality_controlled":"1","scopus_import":"1","date_created":"2018-12-11T11:53:19Z","isi":1,"department":[{"_id":"KrCh"}],"alternative_title":["LICS"],"date_published":"2015-07-01T00:00:00Z","page":"44 - 55","arxiv":1,"publist_id":"5490","ec_funded":1,"doi":"10.1109/LICS.2015.15","article_processing_charge":"No","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"}],"project":[{"name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"291734"}],"day":"01","conference":{"end_date":"2015-07-10","name":"LICS: Logic in Computer Science","start_date":"2015-07-06","location":"Kyoto, Japan"},"_id":"1660","author":[{"last_name":"Brázdil","full_name":"Brázdil, Tomáš","first_name":"Tomáš"},{"last_name":"Kiefer","full_name":"Kiefer, Stefan","first_name":"Stefan"},{"last_name":"Kučera","first_name":"Antonín","full_name":"Kučera, Antonín"},{"id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","last_name":"Novotny","first_name":"Petr","full_name":"Novotny, Petr"}],"publication_status":"published","publisher":"IEEE","external_id":{"arxiv":["1505.02655"],"isi":["000380427100007"]},"oa_version":"Preprint","oa":1,"main_file_link":[{"url":"http://arxiv.org/abs/1505.02655","open_access":"1"}],"month":"07","date_updated":"2025-09-23T09:27:49Z"},{"ec_funded":1,"day":"01","conference":{"name":"LICS: Logic in Computer Science","start_date":"2015-07-06","location":"Kyoto, Japan","end_date":"2015-07-10"},"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF"},{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23"},{"name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7"}],"_id":"1661","author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"full_name":"Henzinger, Monika H","orcid":"0000-0002-5008-6530","first_name":"Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","last_name":"Henzinger"},{"first_name":"Veronika","full_name":"Loitzenbauer, Veronika","last_name":"Loitzenbauer"}],"publisher":"IEEE","external_id":{"isi":["000380427100026"]},"publication_status":"published","article_processing_charge":"No","abstract":[{"text":"The computation of the winning set for one-pair Streett objectives and for k-pair Streett objectives in (standard) graphs as well as in game graphs are central problems in computer-aided verification, with application to the verification of closed systems with strong fairness conditions, the verification of open systems, checking interface compatibility, well-formed ness of specifications, and the synthesis of reactive systems. We give faster algorithms for the computation of the winning set for (1) one-pair Streett objectives (aka parity-3 problem) in game graphs and (2) for k-pair Streett objectives in graphs. For both problems this represents the first improvement in asymptotic running time in 15 years.","lang":"eng"}],"doi":"10.1109/LICS.2015.34","oa":1,"oa_version":"Submitted Version","month":"07","date_updated":"2025-09-23T09:20:53Z","acknowledgement":"K. C. is supported by the Austrian Science Fund (FWF): P23499-N23 and S11407-N23 (RiSE), an ERC Start Grant (279307: Graph Games), and a Microsoft Faculty Fellows Award. M. H. is supported by the Austrian Science Fund (FWF): P23499-N23 and the Vienna Science and Technology Fund (WWTF) grant ICT10-002. V. L. is supported by the Vienna Science and Technology Fund (WWTF) grant ICT10-002. The research leading to these results has received funding from the European Research Council under the European Union’s Seventh Framework Programme (FP/2007-2013) / ERC Grant Agreement no. 340506.","main_file_link":[{"open_access":"1","url":"https://eprints.cs.univie.ac.at/4368/"}],"year":"2015","type":"conference","title":"Improved algorithms for one-pair and k-pair Streett objectives","publication":"Proceedings - Symposium on Logic in Computer Science","language":[{"iso":"eng"}],"related_material":{"record":[{"relation":"later_version","status":"public","id":"464"}]},"quality_controlled":"1","scopus_import":"1","date_created":"2018-12-11T11:53:19Z","volume":"2015-July","status":"public","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","citation":{"apa":"Chatterjee, K., Henzinger, M., &#38; Loitzenbauer, V. (2015). Improved algorithms for one-pair and k-pair Streett objectives. In <i>Proceedings - Symposium on Logic in Computer Science</i> (Vol. 2015–July). Kyoto, Japan: IEEE. <a href=\"https://doi.org/10.1109/LICS.2015.34\">https://doi.org/10.1109/LICS.2015.34</a>","ieee":"K. Chatterjee, M. Henzinger, and V. Loitzenbauer, “Improved algorithms for one-pair and k-pair Streett objectives,” in <i>Proceedings - Symposium on Logic in Computer Science</i>, Kyoto, Japan, 2015, vol. 2015–July.","chicago":"Chatterjee, Krishnendu, Monika Henzinger, and Veronika Loitzenbauer. “Improved Algorithms for One-Pair and k-Pair Streett Objectives.” In <i>Proceedings - Symposium on Logic in Computer Science</i>, Vol. 2015–July. IEEE, 2015. <a href=\"https://doi.org/10.1109/LICS.2015.34\">https://doi.org/10.1109/LICS.2015.34</a>.","short":"K. Chatterjee, M. Henzinger, V. Loitzenbauer, in:, Proceedings - Symposium on Logic in Computer Science, IEEE, 2015.","ista":"Chatterjee K, Henzinger M, Loitzenbauer V. 2015. Improved algorithms for one-pair and k-pair Streett objectives. Proceedings - Symposium on Logic in Computer Science. LICS: Logic in Computer Science vol. 2015–July, 7174888.","mla":"Chatterjee, Krishnendu, et al. “Improved Algorithms for One-Pair and k-Pair Streett Objectives.” <i>Proceedings - Symposium on Logic in Computer Science</i>, vol. 2015–July, 7174888, IEEE, 2015, doi:<a href=\"https://doi.org/10.1109/LICS.2015.34\">10.1109/LICS.2015.34</a>.","ama":"Chatterjee K, Henzinger M, Loitzenbauer V. Improved algorithms for one-pair and k-pair Streett objectives. In: <i>Proceedings - Symposium on Logic in Computer Science</i>. Vol 2015-July. IEEE; 2015. doi:<a href=\"https://doi.org/10.1109/LICS.2015.34\">10.1109/LICS.2015.34</a>"},"department":[{"_id":"KrCh"}],"isi":1,"publist_id":"5489","date_published":"2015-07-01T00:00:00Z","article_number":"7174888"},{"oa_version":"Submitted Version","oa":1,"article_type":"original","main_file_link":[{"open_access":"1","url":"https://www.ncbi.nlm.nih.gov/pmc/articles/PMC4815041/"}],"date_updated":"2025-09-23T09:37:33Z","month":"10","ec_funded":1,"article_processing_charge":"No","abstract":[{"text":"Which genetic alterations drive tumorigenesis and how they evolve over the course of disease and therapy are central questions in cancer biology. Here we identify 44 recurrently mutated genes and 11 recurrent somatic copy number variations through whole-exome sequencing of 538 chronic lymphocytic leukaemia (CLL) and matched germline DNA samples, 278 of which were collected in a prospective clinical trial. These include previously unrecognized putative cancer drivers (RPS15, IKZF3), and collectively identify RNA processing and export, MYC activity, and MAPK signalling as central pathways involved in CLL. Clonality analysis of this large data set further enabled reconstruction of temporal relationships between driver events. Direct comparison between matched pre-treatment and relapse samples from 59 patients demonstrated highly frequent clonal evolution. Thus, large sequencing data sets of clinically informative samples enable the discovery of novel genes associated with cancer, the network of relationships between the driver events, and their impact on disease relapse and clinical outcome.","lang":"eng"}],"doi":"10.1038/nature15395","_id":"1665","external_id":{"isi":["000364026100040"],"pmid":["26466571"]},"author":[{"last_name":"Landau","full_name":"Landau, Dan","first_name":"Dan"},{"full_name":"Tausch, Eugen","first_name":"Eugen","last_name":"Tausch"},{"full_name":"Taylor Weiner, Amaro","first_name":"Amaro","last_name":"Taylor Weiner"},{"first_name":"Chip","full_name":"Stewart, Chip","last_name":"Stewart"},{"id":"4A918E98-F248-11E8-B48F-1D18A9856A87","last_name":"Reiter","first_name":"Johannes","full_name":"Reiter, Johannes","orcid":"0000-0002-0170-7353"},{"last_name":"Bahlo","full_name":"Bahlo, Jasmin","first_name":"Jasmin"},{"full_name":"Kluth, Sandra","first_name":"Sandra","last_name":"Kluth"},{"full_name":"Božić, Ivana","first_name":"Ivana","last_name":"Božić"},{"last_name":"Lawrence","first_name":"Michael","full_name":"Lawrence, Michael"},{"last_name":"Böttcher","full_name":"Böttcher, Sebastian","first_name":"Sebastian"},{"last_name":"Carter","full_name":"Carter, Scott","first_name":"Scott"},{"last_name":"Cibulskis","first_name":"Kristian","full_name":"Cibulskis, Kristian"},{"last_name":"Mertens","first_name":"Daniel","full_name":"Mertens, Daniel"},{"full_name":"Sougnez, Carrie","first_name":"Carrie","last_name":"Sougnez"},{"first_name":"Mara","full_name":"Rosenberg, Mara","last_name":"Rosenberg"},{"last_name":"Hess","full_name":"Hess, Julian","first_name":"Julian"},{"last_name":"Edelmann","first_name":"Jennifer","full_name":"Edelmann, Jennifer"},{"first_name":"Sabrina","full_name":"Kless, Sabrina","last_name":"Kless"},{"last_name":"Kneba","full_name":"Kneba, Michael","first_name":"Michael"},{"last_name":"Ritgen","first_name":"Matthias","full_name":"Ritgen, Matthias"},{"first_name":"Anna","full_name":"Fink, Anna","last_name":"Fink"},{"first_name":"Kirsten","full_name":"Fischer, Kirsten","last_name":"Fischer"},{"first_name":"Stacey","full_name":"Gabriel, Stacey","last_name":"Gabriel"},{"last_name":"Lander","first_name":"Eric","full_name":"Lander, Eric"},{"last_name":"Nowak","full_name":"Nowak, Martin","first_name":"Martin"},{"last_name":"Döhner","first_name":"Hartmut","full_name":"Döhner, Hartmut"},{"last_name":"Hallek","first_name":"Michael","full_name":"Hallek, Michael"},{"last_name":"Neuberg","first_name":"Donna","full_name":"Neuberg, Donna"},{"first_name":"Gad","full_name":"Getz, Gad","last_name":"Getz"},{"first_name":"Stephan","full_name":"Stilgenbauer, Stephan","last_name":"Stilgenbauer"},{"last_name":"Wu","full_name":"Wu, Catherine","first_name":"Catherine"}],"publication_status":"published","publisher":"Nature Publishing Group","day":"22","project":[{"call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"},{"call_identifier":"FWF","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23"}],"department":[{"_id":"KrCh"}],"isi":1,"page":"525 - 530","date_published":"2015-10-22T00:00:00Z","publist_id":"5484","intvolume":"       526","language":[{"iso":"eng"}],"title":"Mutations driving CLL and their evolution in progression and relapse","publication":"Nature","year":"2015","issue":"7574","type":"journal_article","pmid":1,"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","citation":{"apa":"Landau, D., Tausch, E., Taylor Weiner, A., Stewart, C., Reiter, J., Bahlo, J., … Wu, C. (2015). Mutations driving CLL and their evolution in progression and relapse. <i>Nature</i>. Nature Publishing Group. <a href=\"https://doi.org/10.1038/nature15395\">https://doi.org/10.1038/nature15395</a>","ieee":"D. Landau <i>et al.</i>, “Mutations driving CLL and their evolution in progression and relapse,” <i>Nature</i>, vol. 526, no. 7574. Nature Publishing Group, pp. 525–530, 2015.","chicago":"Landau, Dan, Eugen Tausch, Amaro Taylor Weiner, Chip Stewart, Johannes Reiter, Jasmin Bahlo, Sandra Kluth, et al. “Mutations Driving CLL and Their Evolution in Progression and Relapse.” <i>Nature</i>. Nature Publishing Group, 2015. <a href=\"https://doi.org/10.1038/nature15395\">https://doi.org/10.1038/nature15395</a>.","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.","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.","mla":"Landau, Dan, et al. “Mutations Driving CLL and Their Evolution in Progression and Relapse.” <i>Nature</i>, vol. 526, no. 7574, Nature Publishing Group, 2015, pp. 525–30, doi:<a href=\"https://doi.org/10.1038/nature15395\">10.1038/nature15395</a>.","ama":"Landau D, Tausch E, Taylor Weiner A, et al. Mutations driving CLL and their evolution in progression and relapse. <i>Nature</i>. 2015;526(7574):525-530. doi:<a href=\"https://doi.org/10.1038/nature15395\">10.1038/nature15395</a>"},"volume":526,"status":"public","date_created":"2018-12-11T11:53:21Z","quality_controlled":"1","scopus_import":"1"},{"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","citation":{"chicago":"Brázdil, Tomáš, L’Uboš Korenčiak, Jan Krčál, Petr Novotný, and Vojtěch Řehák. “Optimizing Performance of Continuous-Time Stochastic Systems Using Timeout Synthesis.” Lecture Notes in Computer Science. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-22264-6_10\">https://doi.org/10.1007/978-3-319-22264-6_10</a>.","apa":"Brázdil, T., Korenčiak, L., Krčál, J., Novotný, P., &#38; Řehák, V. (2015). Optimizing performance of continuous-time stochastic systems using timeout synthesis. Presented at the QEST: Quantitative Evaluation of Systems, Madrid, Spain: Springer. <a href=\"https://doi.org/10.1007/978-3-319-22264-6_10\">https://doi.org/10.1007/978-3-319-22264-6_10</a>","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.","mla":"Brázdil, Tomáš, et al. <i>Optimizing Performance of Continuous-Time Stochastic Systems Using Timeout Synthesis</i>. Vol. 9259, Springer, 2015, pp. 141–59, doi:<a href=\"https://doi.org/10.1007/978-3-319-22264-6_10\">10.1007/978-3-319-22264-6_10</a>.","ama":"Brázdil T, Korenčiak L, Krčál J, Novotný P, Řehák V. Optimizing performance of continuous-time stochastic systems using timeout synthesis. 2015;9259:141-159. doi:<a href=\"https://doi.org/10.1007/978-3-319-22264-6_10\">10.1007/978-3-319-22264-6_10</a>","short":"T. Brázdil, L. Korenčiak, J. Krčál, P. Novotný, V. Řehák, 9259 (2015) 141–159.","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."},"volume":9259,"status":"public","date_created":"2018-12-11T11:53:22Z","series_title":"Lecture Notes in Computer Science","quality_controlled":"1","scopus_import":"1","language":[{"iso":"eng"}],"title":"Optimizing performance of continuous-time stochastic systems using timeout synthesis","year":"2015","type":"conference","page":"141 - 159","arxiv":1,"date_published":"2015-08-22T00:00:00Z","alternative_title":["LNCS"],"publist_id":"5482","intvolume":"      9259","department":[{"_id":"KrCh"}],"isi":1,"article_processing_charge":"No","abstract":[{"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.","lang":"eng"}],"doi":"10.1007/978-3-319-22264-6_10","_id":"1667","publisher":"Springer","publication_status":"published","external_id":{"arxiv":["1407.4777"],"isi":["000363574600012"]},"author":[{"first_name":"Tomáš","full_name":"Brázdil, Tomáš","last_name":"Brázdil"},{"last_name":"Korenčiak","full_name":"Korenčiak, L'Uboš","first_name":"L'Uboš"},{"full_name":"Krčál, Jan","first_name":"Jan","last_name":"Krčál"},{"id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","last_name":"Novotny","first_name":"Petr","full_name":"Novotny, Petr"},{"first_name":"Vojtěch","full_name":"Řehák, Vojtěch","last_name":"Řehák"}],"day":"22","conference":{"end_date":"2015-09-03","name":"QEST: Quantitative Evaluation of Systems","location":"Madrid, Spain","start_date":"2015-09-01"},"project":[{"call_identifier":"FP7","grant_number":"291734","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425"}],"ec_funded":1,"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1407.4777"}],"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.","date_updated":"2025-09-23T09:46:46Z","month":"08","oa_version":"Preprint","oa":1},{"type":"journal_article","year":"2015","issue":"2181","file":[{"content_type":"application/pdf","date_updated":"2020-07-14T12:45:11Z","date_created":"2019-04-18T12:39:56Z","checksum":"e613d94d283c776322403a28aad11bdd","file_name":"2015_rspa_Adlam.pdf","file_size":391466,"relation":"main_file","creator":"kschuh","access_level":"open_access","file_id":"6342"}],"language":[{"iso":"eng"}],"publication":"Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences","title":"Amplifiers of selection","date_created":"2018-12-11T11:53:24Z","scopus_import":"1","quality_controlled":"1","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","citation":{"ama":"Adlam B, Chatterjee K, Nowak M. Amplifiers of selection. <i>Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences</i>. 2015;471(2181). doi:<a href=\"https://doi.org/10.1098/rspa.2015.0114\">10.1098/rspa.2015.0114</a>","mla":"Adlam, Ben, et al. “Amplifiers of Selection.” <i>Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences</i>, vol. 471, no. 2181, 20150114, Royal Society of London, 2015, doi:<a href=\"https://doi.org/10.1098/rspa.2015.0114\">10.1098/rspa.2015.0114</a>.","short":"B. Adlam, K. Chatterjee, M. Nowak, Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences 471 (2015).","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.” <i>Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences</i>. Royal Society of London, 2015. <a href=\"https://doi.org/10.1098/rspa.2015.0114\">https://doi.org/10.1098/rspa.2015.0114</a>.","ieee":"B. Adlam, K. Chatterjee, and M. Nowak, “Amplifiers of selection,” <i>Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences</i>, vol. 471, no. 2181. Royal Society of London, 2015.","apa":"Adlam, B., Chatterjee, K., &#38; Nowak, M. (2015). Amplifiers of selection. <i>Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences</i>. Royal Society of London. <a href=\"https://doi.org/10.1098/rspa.2015.0114\">https://doi.org/10.1098/rspa.2015.0114</a>"},"status":"public","volume":471,"isi":1,"department":[{"_id":"KrCh"}],"publist_id":"5477","intvolume":"       471","date_published":"2015-09-08T00:00:00Z","article_number":"20150114","ddc":["000"],"ec_funded":1,"_id":"1673","author":[{"full_name":"Adlam, Ben","first_name":"Ben","last_name":"Adlam"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","first_name":"Krishnendu"},{"last_name":"Nowak","full_name":"Nowak, Martin","first_name":"Martin"}],"external_id":{"isi":["000363482200005"]},"publication_status":"published","publisher":"Royal Society of London","project":[{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF"},{"call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"day":"08","doi":"10.1098/rspa.2015.0114","article_processing_charge":"No","abstract":[{"text":"When a new mutant arises in a population, there is a probability it outcompetes the residents and fixes. The structure of the population can affect this fixation probability. Suppressing population structures reduce the difference between two competing variants, while amplifying population structures enhance the difference. Suppressors are ubiquitous and easy to construct, but amplifiers for the large population limit are more elusive and only a few examples have been discovered. Whether or not a population structure is an amplifier of selection depends on the probability distribution for the placement of the invading mutant. First, we prove that there exist only bounded amplifiers for adversarial placement-that is, for arbitrary initial conditions. Next, we show that the Star population structure, which is known to amplify for mutants placed uniformly at random, does not amplify for mutants that arise through reproduction and are therefore placed proportional to the temperatures of the vertices. Finally, we construct population structures that amplify for all mutational events that arise through reproduction, uniformly at random, or through some combination of the two. ","lang":"eng"}],"oa":1,"oa_version":"Published Version","file_date_updated":"2020-07-14T12:45:11Z","has_accepted_license":"1","date_updated":"2025-09-23T07:46:22Z","month":"09","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). "},{"month":"09","date_updated":"2025-04-15T06:50:21Z","has_accepted_license":"1","pubrep_id":"448","file_date_updated":"2020-07-14T12:45:12Z","oa_version":"Published Version","oa":1,"article_type":"original","article_processing_charge":"No","abstract":[{"lang":"eng","text":"In many social situations, individuals endeavor to find the single best possible partner, but are constrained to evaluate the candidates in sequence. Examples include the search for mates, economic partnerships, or any other long-term ties where the choice to interact involves two parties. Surprisingly, however, previous theoretical work on mutual choice problems focuses on finding equilibrium solutions, while ignoring the evolutionary dynamics of decisions. Empirically, this may be of high importance, as some equilibrium solutions can never be reached unless the population undergoes radical changes and a sufficient number of individuals change their decisions simultaneously. To address this question, we apply a mutual choice sequential search problem in an evolutionary game-theoretical model that allows one to find solutions that are favored by evolution. As an example, we study the influence of sequential search on the evolutionary dynamics of cooperation. For this, we focus on the classic snowdrift game and the prisoner’s dilemma game."}],"doi":"10.3390/g6040413","day":"29","project":[{"_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","grant_number":"291734","call_identifier":"FP7"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF"},{"grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"}],"_id":"1681","publisher":"MDPI","author":[{"full_name":"Priklopil, Tadeas","first_name":"Tadeas","last_name":"Priklopil","id":"3C869AA0-F248-11E8-B48F-1D18A9856A87"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"}],"publication_status":"published","ec_funded":1,"ddc":["000"],"date_published":"2015-09-29T00:00:00Z","page":"413 - 437","intvolume":"         6","publist_id":"5467","department":[{"_id":"NiBa"},{"_id":"KrCh"}],"publication_identifier":{"eissn":["2073-4336"]},"volume":6,"status":"public","citation":{"chicago":"Priklopil, Tadeas, and Krishnendu Chatterjee. “Evolution of Decisions in Population Games with Sequentially Searching Individuals.” <i>Games</i>. MDPI, 2015. <a href=\"https://doi.org/10.3390/g6040413\">https://doi.org/10.3390/g6040413</a>.","ieee":"T. Priklopil and K. Chatterjee, “Evolution of decisions in population games with sequentially searching individuals,” <i>Games</i>, vol. 6, no. 4. MDPI, pp. 413–437, 2015.","apa":"Priklopil, T., &#38; Chatterjee, K. (2015). Evolution of decisions in population games with sequentially searching individuals. <i>Games</i>. MDPI. <a href=\"https://doi.org/10.3390/g6040413\">https://doi.org/10.3390/g6040413</a>","ama":"Priklopil T, Chatterjee K. Evolution of decisions in population games with sequentially searching individuals. <i>Games</i>. 2015;6(4):413-437. doi:<a href=\"https://doi.org/10.3390/g6040413\">10.3390/g6040413</a>","mla":"Priklopil, Tadeas, and Krishnendu Chatterjee. “Evolution of Decisions in Population Games with Sequentially Searching Individuals.” <i>Games</i>, vol. 6, no. 4, MDPI, 2015, pp. 413–37, doi:<a href=\"https://doi.org/10.3390/g6040413\">10.3390/g6040413</a>.","short":"T. Priklopil, K. Chatterjee, Games 6 (2015) 413–437.","ista":"Priklopil T, Chatterjee K. 2015. Evolution of decisions in population games with sequentially searching individuals. Games. 6(4), 413–437."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":"1","quality_controlled":"1","date_created":"2018-12-11T11:53:26Z","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"title":"Evolution of decisions in population games with sequentially searching individuals","publication":"Games","corr_author":"1","language":[{"iso":"eng"}],"file":[{"content_type":"application/pdf","date_updated":"2020-07-14T12:45:12Z","date_created":"2018-12-12T10:12:41Z","checksum":"912e1acbaf201100f447a43e4d5958bd","file_name":"IST-2016-448-v1+1_games-06-00413.pdf","file_size":518832,"relation":"main_file","creator":"system","access_level":"open_access","file_id":"4959"}],"year":"2015","issue":"4","type":"journal_article"},{"ec_funded":1,"doi":"10.1145/2728606.2728608","article_processing_charge":"No","abstract":[{"lang":"eng","text":"We consider the problem of computing the set of initial states of a dynamical system such that there exists a control strategy to ensure that the trajectories satisfy a temporal logic specification with probability 1 (almost-surely). We focus on discrete-time, stochastic linear dynamics and specifications given as formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over linear predicates in the states of the system. We propose a solution based on iterative abstraction-refinement, and turn-based 2-player probabilistic games. While the theoretical guarantee of our algorithm after any finite number of iterations is only a partial solution, we show that if our algorithm terminates, then the result is the set of satisfying initial states. Moreover, for any (partial) solution our algorithm synthesizes witness control strategies to ensure almost-sure satisfaction of the temporal logic specification. We demonstrate our approach on an illustrative case study."}],"publisher":"ACM","_id":"1689","author":[{"full_name":"Svoreňová, Mária","first_name":"Mária","last_name":"Svoreňová"},{"first_name":"Jan","orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan","last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Martin","full_name":"Chmelik, Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Cěrná","full_name":"Cěrná, Ivana","first_name":"Ivana"},{"last_name":"Belta","first_name":"Cǎlin","full_name":"Belta, Cǎlin"}],"external_id":{"arxiv":["1410.5387"]},"publication_status":"published","project":[{"_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","grant_number":"291734","call_identifier":"FP7"},{"grant_number":"267989","call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling"},{"call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"},{"call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23"},{"grant_number":"S11407","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory"}],"conference":{"end_date":"2015-04-16","location":"Seattle, WA, United States","start_date":"2015-04-14","name":"HSCC: Hybrid Systems - Computation and Control"},"day":"14","oa_version":"Preprint","oa":1,"main_file_link":[{"url":"http://arxiv.org/abs/1410.5387","open_access":"1"}],"date_updated":"2025-06-11T06:33:00Z","month":"04","language":[{"iso":"eng"}],"publication":"Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control","title":"Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games","year":"2015","type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ista":"Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. 2015. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems - Computation and Control, 259–268.","short":"M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, C. Belta, in:, Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, ACM, 2015, pp. 259–268.","ama":"Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. In: <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i>. ACM; 2015:259-268. doi:<a href=\"https://doi.org/10.1145/2728606.2728608\">10.1145/2728606.2728608</a>","mla":"Svoreňová, Mária, et al. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i>, ACM, 2015, pp. 259–68, doi:<a href=\"https://doi.org/10.1145/2728606.2728608\">10.1145/2728606.2728608</a>.","ieee":"M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, and C. Belta, “Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games,” in <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i>, Seattle, WA, United States, 2015, pp. 259–268.","apa":"Svoreňová, M., Kretinsky, J., Chmelik, M., Chatterjee, K., Cěrná, I., &#38; Belta, C. (2015). Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. In <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i> (pp. 259–268). Seattle, WA, United States: ACM. <a href=\"https://doi.org/10.1145/2728606.2728608\">https://doi.org/10.1145/2728606.2728608</a>","chicago":"Svoreňová, Mária, Jan Kretinsky, Martin Chmelik, Krishnendu Chatterjee, Ivana Cěrná, and Cǎlin Belta. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” In <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i>, 259–68. ACM, 2015. <a href=\"https://doi.org/10.1145/2728606.2728608\">https://doi.org/10.1145/2728606.2728608</a>."},"status":"public","date_created":"2018-12-11T11:53:29Z","scopus_import":"1","related_material":{"record":[{"relation":"later_version","status":"public","id":"1407"}]},"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"page":"259 - 268","arxiv":1,"date_published":"2015-04-14T00:00:00Z","publist_id":"5456"},{"department":[{"_id":"KrCh"}],"oa_version":"None","date_updated":"2021-01-12T06:52:33Z","publist_id":"5453","month":"04","page":"233 - 238","date_published":"2015-04-14T00:00:00Z","type":"conference","year":"2015","language":[{"iso":"eng"}],"title":"Temporal logic motion planning using POMDPs with parity objectives: Case study paper","ec_funded":1,"publication":"Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control","_id":"1691","publication_status":"published","date_created":"2018-12-11T11:53:29Z","publisher":"ACM","author":[{"last_name":"Svoreňová","full_name":"Svoreňová, Mária","first_name":"Mária"},{"id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik","full_name":"Chmelik, Martin","first_name":"Martin"},{"last_name":"Leahy","full_name":"Leahy, Kevin","first_name":"Kevin"},{"full_name":"Eniser, Hasan","first_name":"Hasan","last_name":"Eniser"},{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Ivana","full_name":"Cěrná, Ivana","last_name":"Cěrná"},{"last_name":"Belta","full_name":"Belta, Cǎlin","first_name":"Cǎlin"}],"day":"14","conference":{"end_date":"2015-04-16","name":"HSCC: Hybrid Systems - Computation and Control","location":"Seattle, WA, United States","start_date":"2015-04-14"},"project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF"},{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307"}],"scopus_import":1,"citation":{"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 <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i>, 233–38. ACM, 2015. <a href=\"https://doi.org/10.1145/2728606.2728617\">https://doi.org/10.1145/2728606.2728617</a>.","ieee":"M. Svoreňová <i>et al.</i>, “Temporal logic motion planning using POMDPs with parity objectives: Case study paper,” in <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i>, Seattle, WA, United States, 2015, pp. 233–238.","apa":"Svoreňová, M., Chmelik, M., Leahy, K., Eniser, H., Chatterjee, K., Cěrná, I., &#38; Belta, C. (2015). Temporal logic motion planning using POMDPs with parity objectives: Case study paper. In <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i> (pp. 233–238). Seattle, WA, United States: ACM. <a href=\"https://doi.org/10.1145/2728606.2728617\">https://doi.org/10.1145/2728606.2728617</a>","ama":"Svoreňová M, Chmelik M, Leahy K, et al. Temporal logic motion planning using POMDPs with parity objectives: Case study paper. In: <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i>. ACM; 2015:233-238. doi:<a href=\"https://doi.org/10.1145/2728606.2728617\">10.1145/2728606.2728617</a>","mla":"Svoreňová, Mária, et al. “Temporal Logic Motion Planning Using POMDPs with Parity Objectives: Case Study Paper.” <i>Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control</i>, ACM, 2015, pp. 233–38, doi:<a href=\"https://doi.org/10.1145/2728606.2728617\">10.1145/2728606.2728617</a>.","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.","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."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","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"}],"doi":"10.1145/2728606.2728617","status":"public"},{"department":[{"_id":"KrCh"}],"isi":1,"publist_id":"5450","intvolume":"        60","page":"2291 - 2306","date_published":"2015-02-24T00:00:00Z","type":"journal_article","issue":"9","year":"2015","language":[{"iso":"eng"}],"title":"Quantitative temporal simulation and refinement distances for timed systems","publication":"IEEE Transactions on Automatic Control","date_created":"2018-12-11T11:53:30Z","quality_controlled":"1","scopus_import":"1","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","citation":{"ieee":"K. Chatterjee and V. Prabhu, “Quantitative temporal simulation and refinement distances for timed systems,” <i>IEEE Transactions on Automatic Control</i>, vol. 60, no. 9. IEEE, pp. 2291–2306, 2015.","apa":"Chatterjee, K., &#38; Prabhu, V. (2015). Quantitative temporal simulation and refinement distances for timed systems. <i>IEEE Transactions on Automatic Control</i>. IEEE. <a href=\"https://doi.org/10.1109/TAC.2015.2404612\">https://doi.org/10.1109/TAC.2015.2404612</a>","chicago":"Chatterjee, Krishnendu, and Vinayak Prabhu. “Quantitative Temporal Simulation and Refinement Distances for Timed Systems.” <i>IEEE Transactions on Automatic Control</i>. IEEE, 2015. <a href=\"https://doi.org/10.1109/TAC.2015.2404612\">https://doi.org/10.1109/TAC.2015.2404612</a>.","ista":"Chatterjee K, Prabhu V. 2015. Quantitative temporal simulation and refinement distances for timed systems. IEEE Transactions on Automatic Control. 60(9), 2291–2306.","short":"K. Chatterjee, V. Prabhu, IEEE Transactions on Automatic Control 60 (2015) 2291–2306.","ama":"Chatterjee K, Prabhu V. Quantitative temporal simulation and refinement distances for timed systems. <i>IEEE Transactions on Automatic Control</i>. 2015;60(9):2291-2306. doi:<a href=\"https://doi.org/10.1109/TAC.2015.2404612\">10.1109/TAC.2015.2404612</a>","mla":"Chatterjee, Krishnendu, and Vinayak Prabhu. “Quantitative Temporal Simulation and Refinement Distances for Timed Systems.” <i>IEEE Transactions on Automatic Control</i>, vol. 60, no. 9, IEEE, 2015, pp. 2291–306, doi:<a href=\"https://doi.org/10.1109/TAC.2015.2404612\">10.1109/TAC.2015.2404612</a>."},"volume":60,"status":"public","oa_version":"None","date_updated":"2025-09-23T10:00:03Z","month":"02","ec_funded":1,"author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"last_name":"Prabhu","first_name":"Vinayak","full_name":"Prabhu, Vinayak"}],"_id":"1694","publication_status":"published","publisher":"IEEE","external_id":{"isi":["000360501800001"]},"day":"24","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF"},{"grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"article_processing_charge":"No","abstract":[{"lang":"eng","text":"We 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"}],"doi":"10.1109/TAC.2015.2404612"},{"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","citation":{"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,” <i>Information and Computation</i>, vol. 241, no. 4. Elsevier, pp. 177–196, 2015.","apa":"Velner, Y., Chatterjee, K., Doyen, L., Henzinger, T. A., Rabinovich, A., &#38; Raskin, J. (2015). The complexity of multi-mean-payoff and multi-energy games. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2015.03.001\">https://doi.org/10.1016/j.ic.2015.03.001</a>","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.” <i>Information and Computation</i>. Elsevier, 2015. <a href=\"https://doi.org/10.1016/j.ic.2015.03.001\">https://doi.org/10.1016/j.ic.2015.03.001</a>.","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.","short":"Y. Velner, K. Chatterjee, L. Doyen, T.A. Henzinger, A. Rabinovich, J. Raskin, Information and Computation 241 (2015) 177–196.","ama":"Velner Y, Chatterjee K, Doyen L, Henzinger TA, Rabinovich A, Raskin J. The complexity of multi-mean-payoff and multi-energy games. <i>Information and Computation</i>. 2015;241(4):177-196. doi:<a href=\"https://doi.org/10.1016/j.ic.2015.03.001\">10.1016/j.ic.2015.03.001</a>","mla":"Velner, Yaron, et al. “The Complexity of Multi-Mean-Payoff and Multi-Energy Games.” <i>Information and Computation</i>, vol. 241, no. 4, Elsevier, 2015, pp. 177–96, doi:<a href=\"https://doi.org/10.1016/j.ic.2015.03.001\">10.1016/j.ic.2015.03.001</a>."},"status":"public","volume":241,"date_created":"2018-12-11T11:53:32Z","quality_controlled":"1","scopus_import":"1","language":[{"iso":"eng"}],"publication":"Information and Computation","corr_author":"1","title":"The complexity of multi-mean-payoff and multi-energy games","year":"2015","issue":"4","type":"journal_article","arxiv":1,"page":"177 - 196","date_published":"2015-04-01T00:00:00Z","publist_id":"5443","intvolume":"       241","isi":1,"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"doi":"10.1016/j.ic.2015.03.001","article_processing_charge":"No","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"}],"_id":"1698","external_id":{"isi":["000353352800008"],"arxiv":["1209.3234"]},"author":[{"full_name":"Velner, Yaron","first_name":"Yaron","last_name":"Velner"},{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"last_name":"Doyen","full_name":"Doyen, Laurent","first_name":"Laurent"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"last_name":"Rabinovich","full_name":"Rabinovich, Alexander","first_name":"Alexander"},{"last_name":"Raskin","full_name":"Raskin, Jean","first_name":"Jean"}],"publication_status":"published","publisher":"Elsevier","project":[{"grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"grant_number":"S11407","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23"},{"call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"},{"call_identifier":"FP7","grant_number":"267989","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425"}],"day":"01","ec_funded":1,"main_file_link":[{"url":"http://arxiv.org/abs/1209.3234","open_access":"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_updated":"2025-09-23T13:47:20Z","month":"04","oa_version":"Preprint","oa":1},{"date_updated":"2026-04-09T14:26:23Z","month":"07","main_file_link":[{"url":"http://www.ncbi.nlm.nih.gov/pmc/articles/PMC4528522/","open_access":"1"}],"acknowledgement":"This work was supported by grants from the John Templeton Foundation, ERC Start Grant (279307: Graph Games), FWF NFN Grant (No S11407N23 RiSE/SHiNE), FWF Grant (No P23499N23) and a Microsoft faculty fellows award.","article_type":"original","oa":1,"oa_version":"Submitted Version","_id":"1709","publication_status":"published","external_id":{"isi":["000362305500021"],"pmid":["26180069"]},"publisher":"Royal Society","author":[{"id":"4A918E98-F248-11E8-B48F-1D18A9856A87","last_name":"Reiter","full_name":"Reiter, Johannes","orcid":"0000-0002-0170-7353","first_name":"Johannes"},{"last_name":"Kanodia","full_name":"Kanodia, Ayush","first_name":"Ayush"},{"first_name":"Raghav","full_name":"Gupta, Raghav","last_name":"Gupta"},{"last_name":"Nowak","first_name":"Martin","full_name":"Nowak, Martin"},{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"}],"project":[{"grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"day":"15","doi":"10.1098/rspb.2015.1041","article_processing_charge":"No","abstract":[{"lang":"eng","text":"The competition for resources among cells, individuals or species is a fundamental characteristic of evolution. Biological all-pay auctions have been used to model situations where multiple individuals compete for a single resource. However, in many situations multiple resources with various values exist and single reward auctions are not applicable. We generalize the model to multiple rewards and study the evolution of strategies. In biological all-pay auctions the bid of an individual corresponds to its strategy and is equivalent to its payment in the auction. The decreasingly ordered rewards are distributed according to the decreasingly ordered bids of the participating individuals. The reproductive success of an individual is proportional to its fitness given by the sum of the rewards won minus its payments. Hence, successful bidding strategies spread in the population. We find that the results for the multiple reward case are very different from the single reward case. While the mixed strategy equilibrium in the single reward case with more than two players consists of mostly low-bidding individuals, we show that the equilibrium can convert to many high-bidding individuals and a few low-bidding individuals in the multiple reward case. Some reward values lead to a specialization among the individuals where one subpopulation competes for the rewards and the other subpopulation largely avoids costly competitions. Whether the mixed strategy equilibrium is an evolutionarily stable strategy (ESS) depends on the specific values of the rewards."}],"publist_id":"5425","intvolume":"       282","date_published":"2015-07-15T00:00:00Z","isi":1,"department":[{"_id":"KrCh"}],"date_created":"2018-12-11T11:53:35Z","scopus_import":"1","quality_controlled":"1","related_material":{"record":[{"relation":"dissertation_contains","id":"1400","status":"public"}]},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","citation":{"ieee":"J. Reiter, A. Kanodia, R. Gupta, M. Nowak, and K. Chatterjee, “Biological auctions with multiple rewards,” <i>Proceedings of the Royal Society of London Series B Biological Sciences</i>, vol. 282, no. 1812. Royal Society, 2015.","apa":"Reiter, J., Kanodia, A., Gupta, R., Nowak, M., &#38; Chatterjee, K. (2015). Biological auctions with multiple rewards. <i>Proceedings of the Royal Society of London Series B Biological Sciences</i>. Royal Society. <a href=\"https://doi.org/10.1098/rspb.2015.1041\">https://doi.org/10.1098/rspb.2015.1041</a>","chicago":"Reiter, Johannes, Ayush Kanodia, Raghav Gupta, Martin Nowak, and Krishnendu Chatterjee. “Biological Auctions with Multiple Rewards.” <i>Proceedings of the Royal Society of London Series B Biological Sciences</i>. Royal Society, 2015. <a href=\"https://doi.org/10.1098/rspb.2015.1041\">https://doi.org/10.1098/rspb.2015.1041</a>.","short":"J. Reiter, A. Kanodia, R. Gupta, M. Nowak, K. Chatterjee, Proceedings of the Royal Society of London Series B Biological Sciences 282 (2015).","ista":"Reiter J, Kanodia A, Gupta R, Nowak M, Chatterjee K. 2015. Biological auctions with multiple rewards. Proceedings of the Royal Society of London Series B Biological Sciences. 282(1812).","ama":"Reiter J, Kanodia A, Gupta R, Nowak M, Chatterjee K. Biological auctions with multiple rewards. <i>Proceedings of the Royal Society of London Series B Biological Sciences</i>. 2015;282(1812). doi:<a href=\"https://doi.org/10.1098/rspb.2015.1041\">10.1098/rspb.2015.1041</a>","mla":"Reiter, Johannes, et al. “Biological Auctions with Multiple Rewards.” <i>Proceedings of the Royal Society of London Series B Biological Sciences</i>, vol. 282, no. 1812, Royal Society, 2015, doi:<a href=\"https://doi.org/10.1098/rspb.2015.1041\">10.1098/rspb.2015.1041</a>."},"status":"public","volume":282,"year":"2015","issue":"1812","type":"journal_article","pmid":1,"language":[{"iso":"eng"}],"corr_author":"1","publication":"Proceedings of the Royal Society of London Series B Biological Sciences","title":"Biological auctions with multiple rewards"},{"abstract":[{"text":"We present a flexible framework for the automated competitive analysis of on-line scheduling algorithms for firm-deadline real-time tasks based on multi-objective graphs: Given a task set and an on-line scheduling algorithm specified as a labeled transition system, along with some optional safety, liveness, and/or limit-average constraints for the adversary, we automatically compute the competitive ratio of the algorithm w.r.t. A clairvoyant scheduler. We demonstrate the flexibility and power of our approach by comparing the competitive ratio of several on-line algorithms, including Dover, that have been proposed in the past, for various task sets. Our experimental results reveal that none of these algorithms is universally optimal, in the sense that there are task sets where other schedulers provide better performance. Our framework is hence a very useful design tool for selecting optimal algorithms for a given application.","lang":"eng"}],"article_processing_charge":"No","doi":"10.1109/RTSS.2014.9","day":"15","conference":{"name":"RTSS: Real-Time Systems Symposium","location":"Rome, Italy","start_date":"2014-12-02","end_date":"2014-12-05"},"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas"},{"last_name":"Kößler","first_name":"Alexander","full_name":"Kößler, Alexander"},{"last_name":"Schmid","full_name":"Schmid, Ulrich","first_name":"Ulrich"}],"_id":"1714","publisher":"IEEE","external_id":{"isi":["000569750000012"]},"publication_status":"published","month":"01","date_updated":"2026-04-08T14:22:16Z","oa_version":"None","volume":2015,"status":"public","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","citation":{"chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, Alexander Kößler, and Ulrich Schmid. “A Framework for Automated Competitive Analysis of On-Line Scheduling of Firm-Deadline Tasks.” In <i>Real-Time Systems Symposium</i>, 2015:118–27. IEEE, 2015. <a href=\"https://doi.org/10.1109/RTSS.2014.9\">https://doi.org/10.1109/RTSS.2014.9</a>.","ieee":"K. Chatterjee, A. Pavlogiannis, A. Kößler, and U. Schmid, “A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks,” in <i>Real-Time Systems Symposium</i>, Rome, Italy, 2015, vol. 2015, no. January, pp. 118–127.","apa":"Chatterjee, K., Pavlogiannis, A., Kößler, A., &#38; Schmid, U. (2015). A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks. In <i>Real-Time Systems Symposium</i> (Vol. 2015, pp. 118–127). Rome, Italy: IEEE. <a href=\"https://doi.org/10.1109/RTSS.2014.9\">https://doi.org/10.1109/RTSS.2014.9</a>","ama":"Chatterjee K, Pavlogiannis A, Kößler A, Schmid U. A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks. In: <i>Real-Time Systems Symposium</i>. Vol 2015. IEEE; 2015:118-127. doi:<a href=\"https://doi.org/10.1109/RTSS.2014.9\">10.1109/RTSS.2014.9</a>","mla":"Chatterjee, Krishnendu, et al. “A Framework for Automated Competitive Analysis of On-Line Scheduling of Firm-Deadline Tasks.” <i>Real-Time Systems Symposium</i>, vol. 2015, no. January, IEEE, 2015, pp. 118–27, doi:<a href=\"https://doi.org/10.1109/RTSS.2014.9\">10.1109/RTSS.2014.9</a>.","short":"K. Chatterjee, A. Pavlogiannis, A. Kößler, U. Schmid, in:, Real-Time Systems Symposium, IEEE, 2015, pp. 118–127.","ista":"Chatterjee K, Pavlogiannis A, Kößler A, Schmid U. 2015. A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks. Real-Time Systems Symposium. RTSS: Real-Time Systems Symposium vol. 2015, 118–127."},"related_material":{"record":[{"status":"public","id":"5423","relation":"earlier_version"},{"relation":"dissertation_contains","status":"public","id":"821"}]},"scopus_import":"1","quality_controlled":"1","date_created":"2018-12-11T11:53:37Z","title":"A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks","publication":"Real-Time Systems Symposium","language":[{"iso":"eng"}],"year":"2015","type":"conference","issue":"January","date_published":"2015-01-15T00:00:00Z","page":"118 - 127","intvolume":"      2015","publist_id":"5417","department":[{"_id":"KrCh"}],"isi":1},{"intvolume":"        52","publist_id":"5255","date_published":"2015-04-01T00:00:00Z","page":"269 - 297","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"isi":1,"quality_controlled":"1","scopus_import":"1","date_created":"2018-12-11T11:54:20Z","volume":52,"status":"public","citation":{"ieee":"N. Beneš, J. Kretinsky, K. Larsen, M. Möller, S. Sickert, and J. Srba, “Refinement checking on parametric modal transition systems,” <i>Acta Informatica</i>, vol. 52, no. 2–3. Springer, pp. 269–297, 2015.","apa":"Beneš, N., Kretinsky, J., Larsen, K., Möller, M., Sickert, S., &#38; Srba, J. (2015). Refinement checking on parametric modal transition systems. <i>Acta Informatica</i>. Springer. <a href=\"https://doi.org/10.1007/s00236-015-0215-4\">https://doi.org/10.1007/s00236-015-0215-4</a>","chicago":"Beneš, Nikola, Jan Kretinsky, Kim Larsen, Mikael Möller, Salomon Sickert, and Jiří Srba. “Refinement Checking on Parametric Modal Transition Systems.” <i>Acta Informatica</i>. Springer, 2015. <a href=\"https://doi.org/10.1007/s00236-015-0215-4\">https://doi.org/10.1007/s00236-015-0215-4</a>.","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.","short":"N. Beneš, J. Kretinsky, K. Larsen, M. Möller, S. Sickert, J. Srba, Acta Informatica 52 (2015) 269–297.","ama":"Beneš N, Kretinsky J, Larsen K, Möller M, Sickert S, Srba J. Refinement checking on parametric modal transition systems. <i>Acta Informatica</i>. 2015;52(2-3):269-297. doi:<a href=\"https://doi.org/10.1007/s00236-015-0215-4\">10.1007/s00236-015-0215-4</a>","mla":"Beneš, Nikola, et al. “Refinement Checking on Parametric Modal Transition Systems.” <i>Acta Informatica</i>, vol. 52, no. 2–3, Springer, 2015, pp. 269–97, doi:<a href=\"https://doi.org/10.1007/s00236-015-0215-4\">10.1007/s00236-015-0215-4</a>."},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","issue":"2-3","type":"journal_article","year":"2015","title":"Refinement checking on parametric modal transition systems","publication":"Acta Informatica","corr_author":"1","language":[{"iso":"eng"}],"file":[{"file_name":"2015_ActaInfo_Benes.pdf","checksum":"fb4037ddc4fc05f33080dd3547ede350","relation":"main_file","file_size":488482,"content_type":"application/pdf","date_created":"2020-05-15T08:57:44Z","date_updated":"2020-07-14T12:45:19Z","access_level":"open_access","file_id":"7854","creator":"dernst"}],"month":"04","date_updated":"2025-09-23T10:33:12Z","has_accepted_license":"1","oa":1,"article_type":"original","oa_version":"Submitted Version","file_date_updated":"2020-07-14T12:45:19Z","day":"01","project":[{"call_identifier":"FP7","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling"},{"call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"author":[{"last_name":"Beneš","first_name":"Nikola","full_name":"Beneš, Nikola"},{"full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","first_name":"Jan","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky"},{"last_name":"Larsen","full_name":"Larsen, Kim","first_name":"Kim"},{"last_name":"Möller","full_name":"Möller, Mikael","first_name":"Mikael"},{"last_name":"Sickert","full_name":"Sickert, Salomon","first_name":"Salomon"},{"last_name":"Srba","full_name":"Srba, Jiří","first_name":"Jiří"}],"_id":"1846","external_id":{"isi":["000351160200008"]},"publisher":"Springer","publication_status":"published","abstract":[{"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.","lang":"eng"}],"article_processing_charge":"No","doi":"10.1007/s00236-015-0215-4","ddc":["000"],"ec_funded":1},{"project":[{"name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734","call_identifier":"FP7"}],"day":"09","_id":"1851","publisher":"Wiley","author":[{"id":"3C869AA0-F248-11E8-B48F-1D18A9856A87","last_name":"Priklopil","full_name":"Priklopil, Tadeas","first_name":"Tadeas"},{"first_name":"Eva","full_name":"Kisdi, Eva","last_name":"Kisdi"},{"last_name":"Gyllenberg","first_name":"Mats","full_name":"Gyllenberg, Mats"}],"external_id":{"isi":["000353236000014"],"pmid":["25662095"]},"publication_status":"published","doi":"10.1111/evo.12618","abstract":[{"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.","lang":"eng"}],"article_processing_charge":"No","ddc":["570"],"ec_funded":1,"month":"02","has_accepted_license":"1","date_updated":"2025-09-22T14:27:30Z","oa":1,"article_type":"original","oa_version":"Submitted Version","file_date_updated":"2020-07-14T12:45:19Z","scopus_import":"1","quality_controlled":"1","date_created":"2018-12-11T11:54:21Z","status":"public","volume":69,"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","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.” <i>Evolution</i>. Wiley, 2015. <a href=\"https://doi.org/10.1111/evo.12618\">https://doi.org/10.1111/evo.12618</a>.","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,” <i>Evolution</i>, vol. 69, no. 4. Wiley, pp. 1015–1026, 2015.","apa":"Priklopil, T., Kisdi, E., &#38; Gyllenberg, M. (2015). Evolutionarily stable mating decisions for sequentially searching females and the stability of reproductive isolation by assortative mating. <i>Evolution</i>. Wiley. <a href=\"https://doi.org/10.1111/evo.12618\">https://doi.org/10.1111/evo.12618</a>","ama":"Priklopil T, Kisdi E, Gyllenberg M. Evolutionarily stable mating decisions for sequentially searching females and the stability of reproductive isolation by assortative mating. <i>Evolution</i>. 2015;69(4):1015-1026. doi:<a href=\"https://doi.org/10.1111/evo.12618\">10.1111/evo.12618</a>","mla":"Priklopil, Tadeas, et al. “Evolutionarily Stable Mating Decisions for Sequentially Searching Females and the Stability of Reproductive Isolation by Assortative Mating.” <i>Evolution</i>, vol. 69, no. 4, Wiley, 2015, pp. 1015–26, doi:<a href=\"https://doi.org/10.1111/evo.12618\">10.1111/evo.12618</a>.","short":"T. Priklopil, E. Kisdi, M. Gyllenberg, Evolution 69 (2015) 1015–1026.","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."},"pmid":1,"type":"journal_article","issue":"4","year":"2015","corr_author":"1","publication":"Evolution","title":"Evolutionarily stable mating decisions for sequentially searching females and the stability of reproductive isolation by assortative mating","file":[{"creator":"dernst","access_level":"open_access","file_id":"7855","date_created":"2020-05-15T09:05:34Z","date_updated":"2020-07-14T12:45:19Z","content_type":"application/pdf","file_size":967214,"relation":"main_file","file_name":"2015_Evolution_Priklopil.pdf","checksum":"1e8be0b1d7598a78cd2623d8ee8e7798"}],"language":[{"iso":"eng"}],"intvolume":"        69","publist_id":"5249","date_published":"2015-02-09T00:00:00Z","page":"1015 - 1026","isi":1,"department":[{"_id":"NiBa"},{"_id":"KrCh"}],"publication_identifier":{"eissn":["1558-5646"],"issn":["0014-3820"]}},{"doi":"10.1145/2699430","abstract":[{"text":"The traditional synthesis question given a specification asks for the automatic construction of a system that satisfies the specification, whereas often there exists a preference order among the different systems that satisfy the given specification. Under a probabilistic assumption about the possible inputs, such a preference order is naturally expressed by a weighted automaton, which assigns to each word a value, such that a system is preferred if it generates a higher expected value. We solve the following optimal synthesis problem: given an omega-regular specification, a Markov chain that describes the distribution of inputs, and a weighted automaton that measures how well a system satisfies the given specification under the input assumption, synthesize a system that optimizes the measured value. For safety specifications and quantitative measures that are defined by mean-payoff automata, the optimal synthesis problem reduces to finding a strategy in a Markov decision process (MDP) that is optimal for a long-run average reward objective, which can be achieved in polynomial time. For general omega-regular specifications along with mean-payoff automata, the solution rests on a new, polynomial-time algorithm for computing optimal strategies in MDPs with mean-payoff parity objectives. Our algorithm constructs optimal strategies that consist of two memoryless strategies and a counter. The counter is in general not bounded. To obtain a finite-state system, we show how to construct an ε-optimal strategy with a bounded counter, for all ε &gt; 0. Furthermore, we show how to decide in polynomial time if it is possible to construct an optimal finite-state system (i.e., a system without a counter) for a given specification. We have implemented our approach and the underlying algorithms in a tool that takes qualitative and quantitative specifications and automatically constructs a system that satisfies the qualitative specification and optimizes the quantitative specification, if such a system exists. We present some experimental results showing optimal systems that were automatically generated in this way.","lang":"eng"}],"article_processing_charge":"No","project":[{"name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989"},{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF"},{"call_identifier":"FWF","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"grant_number":"S11407","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory"},{"call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"day":"01","publication_status":"published","_id":"1856","author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Jobstmann","full_name":"Jobstmann, Barbara","first_name":"Barbara"},{"first_name":"Rohit","full_name":"Singh, Rohit","last_name":"Singh"}],"external_id":{"arxiv":["1004.0739"],"isi":["000350563000009"]},"publisher":"ACM","ec_funded":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1004.0739"}],"month":"02","date_updated":"2025-09-23T09:33:01Z","oa_version":"Preprint","oa":1,"status":"public","volume":62,"citation":{"ama":"Chatterjee K, Henzinger TA, Jobstmann B, Singh R. Measuring and synthesizing systems in probabilistic environments. <i>Journal of the ACM</i>. 2015;62(1). doi:<a href=\"https://doi.org/10.1145/2699430\">10.1145/2699430</a>","mla":"Chatterjee, Krishnendu, et al. “Measuring and Synthesizing Systems in Probabilistic Environments.” <i>Journal of the ACM</i>, vol. 62, no. 1, 9, ACM, 2015, doi:<a href=\"https://doi.org/10.1145/2699430\">10.1145/2699430</a>.","short":"K. Chatterjee, T.A. Henzinger, B. Jobstmann, R. Singh, Journal of the ACM 62 (2015).","ista":"Chatterjee K, Henzinger TA, Jobstmann B, Singh R. 2015. Measuring and synthesizing systems in probabilistic environments. Journal of the ACM. 62(1), 9.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Barbara Jobstmann, and Rohit Singh. “Measuring and Synthesizing Systems in Probabilistic Environments.” <i>Journal of the ACM</i>. ACM, 2015. <a href=\"https://doi.org/10.1145/2699430\">https://doi.org/10.1145/2699430</a>.","ieee":"K. Chatterjee, T. A. Henzinger, B. Jobstmann, and R. Singh, “Measuring and synthesizing systems in probabilistic environments,” <i>Journal of the ACM</i>, vol. 62, no. 1. ACM, 2015.","apa":"Chatterjee, K., Henzinger, T. A., Jobstmann, B., &#38; Singh, R. (2015). Measuring and synthesizing systems in probabilistic environments. <i>Journal of the ACM</i>. ACM. <a href=\"https://doi.org/10.1145/2699430\">https://doi.org/10.1145/2699430</a>"},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","quality_controlled":"1","scopus_import":"1","related_material":{"record":[{"id":"3864","status":"public","relation":"earlier_version"}]},"date_created":"2018-12-11T11:54:23Z","publication":"Journal of the ACM","title":"Measuring and synthesizing systems in probabilistic environments","language":[{"iso":"eng"}],"issue":"1","type":"journal_article","year":"2015","date_published":"2015-02-01T00:00:00Z","article_number":"9","arxiv":1,"intvolume":"        62","publist_id":"5244","isi":1,"department":[{"_id":"KrCh"},{"_id":"ToHe"}]},{"abstract":[{"lang":"eng","text":"We consider partially observable Markov decision processes (POMDPs) with limit-average payoff, where a reward value in the interval [0,1] is associated with 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 constraint defines the set of paths where the payoff is at least a given threshold λ1ε(0,1]; and (ii) a qualitative constraint which is a special case of the quantitative constraint with λ1=1. We consider the computation of the almost-sure winning set, where the controller needs to ensure that the path constraint is satisfied with probability 1. Our main results for qualitative path constraints 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 path constraints we show that the problem of deciding the existence of a finite-memory controller is undecidable. We also present a prototype implementation of our EXPTIME algorithm and experimental results on several examples."}],"article_processing_charge":"No","doi":"10.1016/j.artint.2014.12.009","day":"01","external_id":{"isi":["000350782300003"],"arxiv":["1408.2058"]},"_id":"1873","publisher":"Elsevier","author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Martin","full_name":"Chmelik, Martin","last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87"}],"publication_status":"published","oa_version":"Preprint","oa":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1408.2058"}],"month":"04","date_updated":"2025-09-23T09:52:31Z","title":"POMDPs under probabilistic semantics","corr_author":"1","publication":"Artificial Intelligence","language":[{"iso":"eng"}],"year":"2015","type":"journal_article","volume":221,"status":"public","citation":{"ama":"Chatterjee K, Chmelik M. POMDPs under probabilistic semantics. <i>Artificial Intelligence</i>. 2015;221:46-72. doi:<a href=\"https://doi.org/10.1016/j.artint.2014.12.009\">10.1016/j.artint.2014.12.009</a>","mla":"Chatterjee, Krishnendu, and Martin Chmelik. “POMDPs under Probabilistic Semantics.” <i>Artificial Intelligence</i>, vol. 221, Elsevier, 2015, pp. 46–72, doi:<a href=\"https://doi.org/10.1016/j.artint.2014.12.009\">10.1016/j.artint.2014.12.009</a>.","ista":"Chatterjee K, Chmelik M. 2015. POMDPs under probabilistic semantics. Artificial Intelligence. 221, 46–72.","short":"K. Chatterjee, M. Chmelik, Artificial Intelligence 221 (2015) 46–72.","chicago":"Chatterjee, Krishnendu, and Martin Chmelik. “POMDPs under Probabilistic Semantics.” <i>Artificial Intelligence</i>. Elsevier, 2015. <a href=\"https://doi.org/10.1016/j.artint.2014.12.009\">https://doi.org/10.1016/j.artint.2014.12.009</a>.","ieee":"K. Chatterjee and M. Chmelik, “POMDPs under probabilistic semantics,” <i>Artificial Intelligence</i>, vol. 221. Elsevier, pp. 46–72, 2015.","apa":"Chatterjee, K., &#38; Chmelik, M. (2015). POMDPs under probabilistic semantics. <i>Artificial Intelligence</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.artint.2014.12.009\">https://doi.org/10.1016/j.artint.2014.12.009</a>"},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","quality_controlled":"1","scopus_import":"1","date_created":"2018-12-11T11:54:28Z","department":[{"_id":"KrCh"}],"isi":1,"date_published":"2015-04-01T00:00:00Z","page":"46 - 72","arxiv":1,"intvolume":"       221","publist_id":"5224"},{"oa":1,"oa_version":"Preprint","month":"01","date_updated":"2025-06-11T07:22:00Z","acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM), by the Austrian Science Fund (FWF) project S11402-N23 (RiSE), and by the Czech Science Foundation, grant No. P202/12/G061.","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1408.1256"}],"ec_funded":1,"project":[{"name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"267989"},{"name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF"}],"day":"30","conference":{"location":"Bertinoro, Italy","start_date":"2014-09-10","name":"FACS: Formal Aspects of Component Software","end_date":"2014-09-12"},"external_id":{"arxiv":["1408.1256"]},"_id":"1882","author":[{"first_name":"Uli","full_name":"Fahrenberg, Uli","last_name":"Fahrenberg"},{"last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","orcid":"0000-0002-8122-2881","full_name":"Kretinsky, Jan"},{"full_name":"Legay, Axel","first_name":"Axel","last_name":"Legay"},{"last_name":"Traonouez","first_name":"Louis","full_name":"Traonouez, Louis"}],"publisher":"Springer","publication_status":"published","doi":"10.1007/978-3-319-15317-9_19","article_processing_charge":"No","abstract":[{"text":"We provide a framework for compositional and iterative design and verification of systems with quantitative information, such as rewards, time or energy. It is based on disjunctive modal transition systems where we allow actions to bear various types of quantitative information. Throughout the design process the actions can be further refined and the information made more precise. We show how to compute the results of standard operations on the systems, including the quotient (residual), which has not been previously considered for quantitative non-deterministic systems. Our quantitative framework has close connections to the modal nu-calculus and is compositional with respect to general notions of distances between systems and the standard operations.","lang":"eng"}],"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"intvolume":"      8997","publist_id":"5216","alternative_title":["LNCS"],"date_published":"2015-01-30T00:00:00Z","page":"306 - 324","arxiv":1,"year":"2015","type":"conference","corr_author":"1","title":"Compositionality for quantitative specifications","language":[{"iso":"eng"}],"scopus_import":"1","quality_controlled":"1","date_created":"2018-12-11T11:54:31Z","status":"public","volume":8997,"citation":{"ista":"Fahrenberg U, Kretinsky J, Legay A, Traonouez L. 2015. Compositionality for quantitative specifications. FACS: Formal Aspects of Component Software, LNCS, vol. 8997, 306–324.","short":"U. Fahrenberg, J. Kretinsky, A. Legay, L. Traonouez, in:, Springer, 2015, pp. 306–324.","ama":"Fahrenberg U, Kretinsky J, Legay A, Traonouez L. Compositionality for quantitative specifications. In: Vol 8997. Springer; 2015:306-324. doi:<a href=\"https://doi.org/10.1007/978-3-319-15317-9_19\">10.1007/978-3-319-15317-9_19</a>","mla":"Fahrenberg, Uli, et al. <i>Compositionality for Quantitative Specifications</i>. Vol. 8997, Springer, 2015, pp. 306–24, doi:<a href=\"https://doi.org/10.1007/978-3-319-15317-9_19\">10.1007/978-3-319-15317-9_19</a>.","ieee":"U. Fahrenberg, J. Kretinsky, A. Legay, and L. Traonouez, “Compositionality for quantitative specifications,” presented at the FACS: Formal Aspects of Component Software, Bertinoro, Italy, 2015, vol. 8997, pp. 306–324.","apa":"Fahrenberg, U., Kretinsky, J., Legay, A., &#38; Traonouez, L. (2015). Compositionality for quantitative specifications (Vol. 8997, pp. 306–324). Presented at the FACS: Formal Aspects of Component Software, Bertinoro, Italy: Springer. <a href=\"https://doi.org/10.1007/978-3-319-15317-9_19\">https://doi.org/10.1007/978-3-319-15317-9_19</a>","chicago":"Fahrenberg, Uli, Jan Kretinsky, Axel Legay, and Louis Traonouez. “Compositionality for Quantitative Specifications,” 8997:306–24. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-15317-9_19\">https://doi.org/10.1007/978-3-319-15317-9_19</a>."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"}]