[{"doi":"10.1007/978-3-319-21690-4_31","_id":"1601","file_date_updated":"2020-07-14T12:45:04Z","ec_funded":1,"year":"2015","date_created":"2018-12-11T11:52:57Z","citation":{"chicago":"Babiak, Tomáš, František Blahoudek, Alexandre Duret Lutz, Joachim Klein, Jan Kretinsky, Daniel Mueller, David Parker, and Jan Strejček. “The Hanoi Omega-Automata Format,” 9206:479–86. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_31\">https://doi.org/10.1007/978-3-319-21690-4_31</a>.","ista":"Babiak T, Blahoudek F, Duret Lutz A, Klein J, Kretinsky J, Mueller D, Parker D, Strejček J. 2015. The Hanoi omega-automata format. CAV: Computer Aided Verification, LNCS, vol. 9206, 479–486.","mla":"Babiak, Tomáš, et al. <i>The Hanoi Omega-Automata Format</i>. Vol. 9206, Springer, 2015, pp. 479–86, doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_31\">10.1007/978-3-319-21690-4_31</a>.","ieee":"T. Babiak <i>et al.</i>, “The Hanoi omega-automata format,” presented at the CAV: Computer Aided Verification, San Francisco, CA, United States, 2015, vol. 9206, pp. 479–486.","ama":"Babiak T, Blahoudek F, Duret Lutz A, et al. The Hanoi omega-automata format. In: Vol 9206. Springer; 2015:479-486. doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_31\">10.1007/978-3-319-21690-4_31</a>","short":"T. Babiak, F. Blahoudek, A. Duret Lutz, J. Klein, J. Kretinsky, D. Mueller, D. Parker, J. Strejček, in:, Springer, 2015, pp. 479–486.","apa":"Babiak, T., Blahoudek, F., Duret Lutz, A., Klein, J., Kretinsky, J., Mueller, D., … Strejček, J. (2015). The Hanoi omega-automata format (Vol. 9206, pp. 479–486). Presented at the CAV: Computer Aided Verification, San Francisco, CA, United States: Springer. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_31\">https://doi.org/10.1007/978-3-319-21690-4_31</a>"},"publist_id":"5566","date_published":"2015-07-16T00:00:00Z","publisher":"Springer","quality_controlled":"1","volume":9206,"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"page":"479 - 486","project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"}],"ddc":["000"],"abstract":[{"lang":"eng","text":"We propose a flexible exchange format for ω-automata, as typically used in formal verification, and implement support for it in a range of established tools. Our aim is to simplify the interaction of tools, helping the research community to build upon other people’s work. A key feature of the format is the use of very generic acceptance conditions, specified by Boolean combinations of acceptance primitives, rather than being limited to common cases such as Büchi, Streett, or Rabin. Such flexibility in the choice of acceptance conditions can be exploited in applications, for example in probabilistic model checking, and furthermore encourages the development of acceptance-agnostic tools for automata manipulations. The format allows acceptance conditions that are either state-based or transition-based, and also supports alternating automata."}],"publication_status":"published","language":[{"iso":"eng"}],"has_accepted_license":"1","intvolume":"      9206","scopus_import":1,"article_processing_charge":"No","oa":1,"date_updated":"2021-01-12T06:51:54Z","title":"The Hanoi omega-automata format","status":"public","type":"conference","alternative_title":["LNCS"],"month":"07","conference":{"end_date":"2015-07-24","location":"San Francisco, CA, United States","start_date":"2015-07-18","name":"CAV: Computer Aided Verification"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"content_type":"application/pdf","access_level":"open_access","relation":"main_file","file_size":1651779,"creator":"dernst","date_updated":"2020-07-14T12:45:04Z","date_created":"2020-05-15T08:38:12Z","checksum":"5885236fa88a439baba9ac6f3e801e93","file_id":"7850","file_name":"2015_CAV_Babiak.pdf"}],"day":"16","oa_version":"Submitted Version","author":[{"full_name":"Babiak, Tomáš","first_name":"Tomáš","last_name":"Babiak"},{"full_name":"Blahoudek, František","first_name":"František","last_name":"Blahoudek"},{"last_name":"Duret Lutz","full_name":"Duret Lutz, Alexandre","first_name":"Alexandre"},{"first_name":"Joachim","full_name":"Klein, Joachim","last_name":"Klein"},{"orcid":"0000-0002-8122-2881","last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","full_name":"Kretinsky, Jan","first_name":"Jan"},{"full_name":"Mueller, Daniel","first_name":"Daniel","last_name":"Mueller"},{"last_name":"Parker","full_name":"Parker, David","first_name":"David"},{"last_name":"Strejček","first_name":"Jan","full_name":"Strejček, Jan"}]},{"language":[{"iso":"eng"}],"publication":"ACM SIGPLAN Notices","title":"Faster algorithms for algebraic path properties in recursive state machines with constant treewidth","date_updated":"2023-09-07T12:01:58Z","oa":1,"issue":"1","intvolume":"        50","scopus_import":1,"status":"public","type":"journal_article","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus"},{"full_name":"Pavlogiannis, Andreas","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722"},{"first_name":"Prateesh","full_name":"Goyal, Prateesh","last_name":"Goyal"}],"arxiv":1,"oa_version":"Preprint","day":"01","main_file_link":[{"url":"https://arxiv.org/abs/1410.7724","open_access":"1"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"name":"SIGPLAN: Symposium on Principles of Programming Languages","start_date":"2015-01-15","location":"Mumbai, India","end_date":"2015-01-17"},"month":"01","_id":"1602","doi":"10.1145/2676726.2676979","publist_id":"5565","date_created":"2018-12-11T11:52:58Z","citation":{"apa":"Chatterjee, K., Ibsen-Jensen, R., Pavlogiannis, A., &#38; Goyal, P. (2015). Faster algorithms for algebraic path properties in recursive state machines with constant treewidth. <i>ACM SIGPLAN Notices</i>. Mumbai, India: ACM. <a href=\"https://doi.org/10.1145/2676726.2676979\">https://doi.org/10.1145/2676726.2676979</a>","ieee":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, and P. Goyal, “Faster algorithms for algebraic path properties in recursive state machines with constant treewidth,” <i>ACM SIGPLAN Notices</i>, vol. 50, no. 1. ACM, pp. 97–109, 2015.","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A, Goyal P. Faster algorithms for algebraic path properties in recursive state machines with constant treewidth. <i>ACM SIGPLAN Notices</i>. 2015;50(1):97-109. doi:<a href=\"https://doi.org/10.1145/2676726.2676979\">10.1145/2676726.2676979</a>","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, P. Goyal, ACM SIGPLAN Notices 50 (2015) 97–109.","mla":"Chatterjee, Krishnendu, et al. “Faster Algorithms for Algebraic Path Properties in Recursive State Machines with Constant Treewidth.” <i>ACM SIGPLAN Notices</i>, vol. 50, no. 1, ACM, 2015, pp. 97–109, doi:<a href=\"https://doi.org/10.1145/2676726.2676979\">10.1145/2676726.2676979</a>.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Andreas Pavlogiannis, and Prateesh Goyal. “Faster Algorithms for Algebraic Path Properties in Recursive State Machines with Constant Treewidth.” <i>ACM SIGPLAN Notices</i>. ACM, 2015. <a href=\"https://doi.org/10.1145/2676726.2676979\">https://doi.org/10.1145/2676726.2676979</a>.","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A, Goyal P. 2015. Faster algorithms for algebraic path properties in recursive state machines with constant treewidth. ACM SIGPLAN Notices. 50(1), 97–109."},"acknowledgement":"We thank anonymous reviewers for helpful comments to improve the presentation of the paper.","year":"2015","ec_funded":1,"related_material":{"record":[{"relation":"dissertation_contains","id":"821","status":"public"}]},"project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"department":[{"_id":"KrCh"}],"page":"97 - 109","quality_controlled":"1","volume":50,"publisher":"ACM","date_published":"2015-01-01T00:00:00Z","publication_status":"published","external_id":{"arxiv":["1410.7724"]},"abstract":[{"lang":"eng","text":"Interprocedural analysis is at the heart of numerous applications in programming languages, such as alias analysis, constant propagation, etc. Recursive state machines (RSMs) are standard models for interprocedural analysis. We consider a general framework with RSMs where the transitions are labeled from a semiring, and path properties are algebraic with semiring operations. RSMs with algebraic path properties can model interprocedural dataflow analysis problems, the shortest path problem, the most probable path problem, etc. The traditional algorithms for interprocedural analysis focus on path properties where the starting point is fixed as the entry point of a specific method. In this work, we consider possible multiple queries as required in many applications such as in alias analysis. The study of multiple queries allows us to bring in a very important algorithmic distinction between the resource usage of the one-time preprocessing vs for each individual query. The second aspect that we consider is that the control flow graphs for most programs have constant treewidth. Our main contributions are simple and implementable algorithms that supportmultiple queries for algebraic path properties for RSMs that have constant treewidth. Our theoretical results show that our algorithms have small additional one-time preprocessing, but can answer subsequent queries significantly faster as compared to the current best-known solutions for several important problems, such as interprocedural reachability and shortest path. We provide a prototype implementation for interprocedural reachability and intraprocedural shortest path that gives a significant speed-up on several benchmarks."}]},{"author":[{"last_name":"Brázdil","first_name":"Tomáš","full_name":"Brázdil, Tomáš"},{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Chmelik, Martin","first_name":"Martin","last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Andreas","full_name":"Fellner, Andreas","id":"42BABFB4-F248-11E8-B48F-1D18A9856A87","last_name":"Fellner"},{"orcid":"0000-0002-8122-2881","last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","full_name":"Kretinsky, Jan"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Preprint","day":"16","main_file_link":[{"url":"http://arxiv.org/abs/1502.02834","open_access":"1"}],"publication_identifier":{"eisbn":["978-3-319-21690-4"]},"month":"07","conference":{"start_date":"2015-07-18","name":"CAV: Computer Aided Verification","end_date":"2015-07-24","location":"San Francisco, CA, United States"},"type":"conference","status":"public","alternative_title":["LNCS"],"title":"Counterexample explanation by learning small strategies in Markov decision processes","date_updated":"2024-02-21T13:52:07Z","oa":1,"scopus_import":1,"intvolume":"      9206","language":[{"iso":"eng"}],"publication_status":"published","abstract":[{"text":"For deterministic systems, a counterexample to a property can simply be an error trace, whereas counterexamples in probabilistic systems are necessarily more complex. For instance, a set of erroneous traces with a sufficient cumulative probability mass can be used. Since these are too large objects to understand and manipulate, compact representations such as subchains have been considered. In the case of probabilistic systems with non-determinism, the situation is even more complex. While a subchain for a given strategy (or scheduler, resolving non-determinism) is a straightforward choice, we take a different approach. Instead, we focus on the strategy itself, and extract the most important decisions it makes, and present its succinct representation.\r\nThe key tools we employ to achieve this are (1) introducing a concept of importance of a state w.r.t. the strategy, and (2) learning using decision trees. There are three main consequent advantages of our approach. Firstly, it exploits the quantitative information on states, stressing the more important decisions. Secondly, it leads to a greater variability and degree of freedom in representing the strategies. Thirdly, the representation uses a self-explanatory data structure. In summary, our approach produces more succinct and more explainable strategies, as opposed to e.g. binary decision diagrams. Finally, our experimental results show that we can extract several rules describing the strategy even for very large systems that do not fit in memory, and based on the rules explain the erroneous behaviour.","lang":"eng"}],"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734"}],"volume":9206,"quality_controlled":"1","page":"158 - 177","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"date_published":"2015-07-16T00:00:00Z","publisher":"Springer","date_created":"2018-12-11T11:52:58Z","publist_id":"5564","citation":{"short":"T. Brázdil, K. Chatterjee, M. Chmelik, A. Fellner, J. Kretinsky, in:, Springer, 2015, pp. 158–177.","ieee":"T. Brázdil, K. Chatterjee, M. Chmelik, A. Fellner, and J. Kretinsky, “Counterexample explanation by learning small strategies in Markov decision processes,” presented at the CAV: Computer Aided Verification, San Francisco, CA, United States, 2015, vol. 9206, pp. 158–177.","ama":"Brázdil T, Chatterjee K, Chmelik M, Fellner A, Kretinsky J. Counterexample explanation by learning small strategies in Markov decision processes. In: Vol 9206. Springer; 2015:158-177. doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_10\">10.1007/978-3-319-21690-4_10</a>","mla":"Brázdil, Tomáš, et al. <i>Counterexample Explanation by Learning Small Strategies in Markov Decision Processes</i>. Vol. 9206, Springer, 2015, pp. 158–77, doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_10\">10.1007/978-3-319-21690-4_10</a>.","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Andreas Fellner, and Jan Kretinsky. “Counterexample Explanation by Learning Small Strategies in Markov Decision Processes,” 9206:158–77. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_10\">https://doi.org/10.1007/978-3-319-21690-4_10</a>.","ista":"Brázdil T, Chatterjee K, Chmelik M, Fellner A, Kretinsky J. 2015. Counterexample explanation by learning small strategies in Markov decision processes. CAV: Computer Aided Verification, LNCS, vol. 9206, 158–177.","apa":"Brázdil, T., Chatterjee, K., Chmelik, M., Fellner, A., &#38; Kretinsky, J. (2015). Counterexample explanation by learning small strategies in Markov decision processes (Vol. 9206, pp. 158–177). Presented at the CAV: Computer Aided Verification, San Francisco, CA, United States: Springer. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_10\">https://doi.org/10.1007/978-3-319-21690-4_10</a>"},"year":"2015","acknowledgement":"This research was funded in part by Austrian Science Fund (FWF) Grant No P 23499-N23, FWF NFN Grant No S11407-N23 (RiSE) and Z211-N23 (Wittgenstein Award), European Research Council (ERC) Grant No 279307 (Graph Games), ERC Grant No 267989 (QUAREM), the Czech Science Foundation Grant No P202/12/G061, and People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007–2013) REA Grant No 291734.","related_material":{"record":[{"status":"public","id":"5549","relation":"research_paper"}]},"ec_funded":1,"_id":"1603","doi":"10.1007/978-3-319-21690-4_10"},{"day":"01","oa_version":"None","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"start_date":"2015-01-15","name":"SIGPLAN: Symposium on Principles of Programming Languages","end_date":"2015-01-17","location":"Mumbai, India"},"month":"01","publication_identifier":{"isbn":["978-1-4503-3300-9"]},"author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"first_name":"Andreas","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis"},{"full_name":"Velner, Yaron","first_name":"Yaron","last_name":"Velner"}],"status":"public","type":"journal_article","scopus_import":1,"intvolume":"        50","title":"Quantitative interprocedural analysis","pubrep_id":"523","date_updated":"2023-09-07T12:01:59Z","issue":"1","publication":"Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT ","language":[{"iso":"eng"}],"abstract":[{"text":"We consider the quantitative analysis problem for interprocedural control-flow graphs (ICFGs). The input consists of an ICFG, a positive weight function that assigns every transition a positive integer-valued number, and a labelling of the transitions (events) as good, bad, and neutral events. The weight function assigns to each transition a numerical value that represents ameasure of how good or bad an event is. The quantitative analysis problem asks whether there is a run of the ICFG where the ratio of the sum of the numerical weights of good events versus the sum of weights of bad events in the long-run is at least a given threshold (or equivalently, to compute the maximal ratio among all valid paths in the ICFG). The quantitative analysis problem for ICFGs can be solved in polynomial time, and we present an efficient and practical algorithm for the problem. We show that several problems relevant for static program analysis, such as estimating the worst-case execution time of a program or the average energy consumption of a mobile application, can be modeled in our framework. We have implemented our algorithm as a tool in the Java Soot framework. We demonstrate the effectiveness of our approach with two case studies. First, we show that our framework provides a sound approach (no false positives) for the analysis of inefficiently-used containers. Second, we show that our approach can also be used for static profiling of programs which reasons about methods that are frequently invoked. Our experimental results show that our tool scales to relatively large benchmarks, and discovers relevant and useful information that can be used to optimize performance of the programs.","lang":"eng"}],"publication_status":"published","page":"539 - 551","department":[{"_id":"KrCh"}],"volume":50,"quality_controlled":"1","publisher":"ACM","date_published":"2015-01-01T00:00:00Z","project":[{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"ec_funded":1,"related_material":{"record":[{"id":"5445","relation":"earlier_version","status":"public"},{"id":"821","relation":"dissertation_contains","status":"public"}]},"date_created":"2018-12-11T11:52:59Z","citation":{"apa":"Chatterjee, K., Pavlogiannis, A., &#38; Velner, Y. (2015). Quantitative interprocedural analysis. <i>Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT </i>. Mumbai, India: ACM. <a href=\"https://doi.org/10.1145/2676726.2676968\">https://doi.org/10.1145/2676726.2676968</a>","mla":"Chatterjee, Krishnendu, et al. “Quantitative Interprocedural Analysis.” <i>Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT </i>, vol. 50, no. 1, ACM, 2015, pp. 539–51, doi:<a href=\"https://doi.org/10.1145/2676726.2676968\">10.1145/2676726.2676968</a>.","ista":"Chatterjee K, Pavlogiannis A, Velner Y. 2015. Quantitative interprocedural analysis. Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT . 50(1), 539–551.","chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, and Yaron Velner. “Quantitative Interprocedural Analysis.” <i>Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT </i>. ACM, 2015. <a href=\"https://doi.org/10.1145/2676726.2676968\">https://doi.org/10.1145/2676726.2676968</a>.","short":"K. Chatterjee, A. Pavlogiannis, Y. Velner, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT  50 (2015) 539–551.","ieee":"K. Chatterjee, A. Pavlogiannis, and Y. Velner, “Quantitative interprocedural analysis,” <i>Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT </i>, vol. 50, no. 1. ACM, pp. 539–551, 2015.","ama":"Chatterjee K, Pavlogiannis A, Velner Y. Quantitative interprocedural analysis. <i>Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT </i>. 2015;50(1):539-551. doi:<a href=\"https://doi.org/10.1145/2676726.2676968\">10.1145/2676726.2676968</a>"},"publist_id":"5563","year":"2015","doi":"10.1145/2676726.2676968","_id":"1604"},{"_id":"1607","doi":"10.1007/978-3-319-21690-4_9","citation":{"mla":"Chatterjee, Krishnendu, et al. <i>Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs</i>. Vol. 9206, Springer, 2015, pp. 140–57, doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_9\">10.1007/978-3-319-21690-4_9</a>.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. “Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs,” 9206:140–57. Springer, 2015. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_9\">https://doi.org/10.1007/978-3-319-21690-4_9</a>.","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2015. Faster algorithms for quantitative verification in constant treewidth graphs. CAV: Computer Aided Verification, LNCS, vol. 9206, 140–157.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Faster algorithms for quantitative verification in constant treewidth graphs,” presented at the CAV: Computer Aided Verification, San Francisco, CA, USA, 2015, vol. 9206, pp. 140–157.","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Faster algorithms for quantitative verification in constant treewidth graphs. In: Vol 9206. Springer; 2015:140-157. doi:<a href=\"https://doi.org/10.1007/978-3-319-21690-4_9\">10.1007/978-3-319-21690-4_9</a>","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, in:, Springer, 2015, pp. 140–157.","apa":"Chatterjee, K., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2015). Faster algorithms for quantitative verification in constant treewidth graphs (Vol. 9206, pp. 140–157). Presented at the CAV: Computer Aided Verification, San Francisco, CA, USA: Springer. <a href=\"https://doi.org/10.1007/978-3-319-21690-4_9\">https://doi.org/10.1007/978-3-319-21690-4_9</a>"},"date_created":"2018-12-11T11:52:59Z","publist_id":"5560","year":"2015","acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No P23499- N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"5430"},{"relation":"earlier_version","id":"5437","status":"public"},{"status":"public","id":"821","relation":"dissertation_contains"}]},"ec_funded":1,"project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","volume":9206,"page":"140 - 157","department":[{"_id":"KrCh"}],"date_published":"2015-07-16T00:00:00Z","publisher":"Springer","publication_status":"published","abstract":[{"lang":"eng","text":"We consider the core algorithmic problems related to verification of systems with respect to three classical quantitative properties, namely, the mean-payoff property, the ratio property, and the minimum initial credit for energy property. The algorithmic problem given a graph and a quantitative property asks to compute the optimal value (the infimum value over all traces) from every node of the graph. We consider graphs with constant treewidth, and it is well-known that the control-flow graphs of most programs have constant treewidth. Let n denote the number of nodes of a graph, m the number of edges (for constant treewidth graphs m=O(n)) and W the largest absolute value of the weights. Our main theoretical results are as follows. First, for constant treewidth graphs we present an algorithm that approximates the mean-payoff value within a multiplicative factor of ϵ in time O(n⋅log(n/ϵ)) and linear space, as compared to the classical algorithms that require quadratic time. Second, for the ratio property we present an algorithm that for constant treewidth graphs works in time O(n⋅log(|a⋅b|))=O(n⋅log(n⋅W)), when the output is ab, as compared to the previously best known algorithm with running time O(n2⋅log(n⋅W)). Third, for the minimum initial credit problem we show that (i) for general graphs the problem can be solved in O(n2⋅m) time and the associated decision problem can be solved in O(n⋅m) time, improving the previous known O(n3⋅m⋅log(n⋅W)) and O(n2⋅m) bounds, respectively; and (ii) for constant treewidth graphs we present an algorithm that requires O(n⋅logn) time, improving the previous known O(n4⋅log(n⋅W)) bound. We have implemented some of our algorithms and show that they present a significant speedup on standard benchmarks."}],"language":[{"iso":"eng"}],"title":"Faster algorithms for quantitative verification in constant treewidth graphs","oa":1,"date_updated":"2023-09-07T12:01:59Z","intvolume":"      9206","scopus_import":1,"status":"public","type":"conference","alternative_title":["LNCS"],"author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","first_name":"Andreas"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","oa_version":"Preprint","day":"16","main_file_link":[{"url":"http://arxiv.org/abs/1504.07384","open_access":"1"}],"month":"07","conference":{"name":"CAV: Computer Aided Verification","start_date":"2015-07-18","location":"San Francisco, CA, USA","end_date":"2015-07-24"}},{"abstract":[{"text":"The synthesis problem asks for the automatic construction of a system from its specification. In the traditional setting, the system is “constructed from scratch” rather than composed from reusable components. However, this is rare in practice, and almost every non-trivial software system relies heavily on the use of libraries of reusable components. Recently, Lustig and Vardi introduced dataflow and controlflow synthesis from libraries of reusable components. They proved that dataflow synthesis is undecidable, while controlflow synthesis is decidable. The problem of controlflow synthesis from libraries of probabilistic components was considered by Nain, Lustig and Vardi, and was shown to be decidable for qualitative analysis (that asks that the specification be satisfied with probability 1). Our main contribution for controlflow synthesis from probabilistic components is to establish better complexity bounds for the qualitative analysis problem, and to show that the more general quantitative problem is undecidable. For the qualitative analysis, we show that the problem (i) is EXPTIME-complete when the specification is given as a deterministic parity word automaton, improving the previously known 2EXPTIME upper bound; and (ii) belongs to UP ∩ coUP and is parity-games hard, when the specification is given directly as a parity condition on the components, improving the previously known EXPTIME upper bound.","lang":"eng"}],"publication_status":"published","volume":9135,"quality_controlled":"1","department":[{"_id":"KrCh"}],"page":"108 - 120","date_published":"2015-06-20T00:00:00Z","publisher":"Springer Nature","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"ec_funded":1,"publist_id":"5557","date_created":"2018-12-11T11:53:00Z","citation":{"ista":"Chatterjee K, Doyen L, Vardi M. 2015. The complexity of synthesis from probabilistic components. 42nd International Colloquium. ICALP: Automata, Languages and Programming, LNCS, vol. 9135, 108–120.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, and Moshe Vardi. “The Complexity of Synthesis from Probabilistic Components.” In <i>42nd International Colloquium</i>, 9135:108–20. Springer Nature, 2015. <a href=\"https://doi.org/10.1007/978-3-662-47666-6_9\">https://doi.org/10.1007/978-3-662-47666-6_9</a>.","mla":"Chatterjee, Krishnendu, et al. “The Complexity of Synthesis from Probabilistic Components.” <i>42nd International Colloquium</i>, vol. 9135, Springer Nature, 2015, pp. 108–20, doi:<a href=\"https://doi.org/10.1007/978-3-662-47666-6_9\">10.1007/978-3-662-47666-6_9</a>.","ieee":"K. Chatterjee, L. Doyen, and M. Vardi, “The complexity of synthesis from probabilistic components,” in <i>42nd International Colloquium</i>, Kyoto, Japan, 2015, vol. 9135, pp. 108–120.","ama":"Chatterjee K, Doyen L, Vardi M. The complexity of synthesis from probabilistic components. In: <i>42nd International Colloquium</i>. Vol 9135. Springer Nature; 2015:108-120. doi:<a href=\"https://doi.org/10.1007/978-3-662-47666-6_9\">10.1007/978-3-662-47666-6_9</a>","short":"K. Chatterjee, L. Doyen, M. Vardi, in:, 42nd International Colloquium, Springer Nature, 2015, pp. 108–120.","apa":"Chatterjee, K., Doyen, L., &#38; Vardi, M. (2015). The complexity of synthesis from probabilistic components. In <i>42nd International Colloquium</i> (Vol. 9135, pp. 108–120). Kyoto, Japan: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-662-47666-6_9\">https://doi.org/10.1007/978-3-662-47666-6_9</a>"},"year":"2015","acknowledgement":"This research was supported by Austrian Science Fund (FWF) Grant No P23499- N23, FWF NFN Grant No S11407-N23 (SHiNE), ERC Start grant (279307: Graph Games), EU FP7 Project Cassting, NSF grants CNS 1049862 and CCF-1139011, by NSF Expeditions in Computing project “ExCAPE: Expeditions in Computer Augmented Program Engineering”, by BSF grant 9800096, and by gift from Intel.","doi":"10.1007/978-3-662-47666-6_9","_id":"1609","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","main_file_link":[{"url":"http://arxiv.org/abs/1502.04844","open_access":"1"}],"oa_version":"Preprint","day":"20","publication_identifier":{"isbn":["978-3-662-47665-9"]},"month":"06","conference":{"name":"ICALP: Automata, Languages and Programming","start_date":"2015-07-06","location":"Kyoto, Japan","end_date":"2015-07-10"},"author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"full_name":"Doyen, Laurent","first_name":"Laurent","last_name":"Doyen"},{"full_name":"Vardi, Moshe","first_name":"Moshe","last_name":"Vardi"}],"type":"conference","status":"public","alternative_title":["LNCS"],"intvolume":"      9135","scopus_import":"1","title":"The complexity of synthesis from probabilistic components","article_processing_charge":"No","oa":1,"date_updated":"2022-02-01T15:04:44Z","publication":"42nd International Colloquium","language":[{"iso":"eng"}]},{"language":[{"iso":"eng"}],"publication":"42nd International Colloquium","issue":"Part II","article_processing_charge":"No","oa":1,"pubrep_id":"321","date_updated":"2023-02-23T12:26:24Z","title":"Edit distance for pushdown automata","scopus_import":"1","intvolume":"      9135","type":"conference","status":"public","alternative_title":["LNCS"],"arxiv":1,"author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389"},{"full_name":"Otop, Jan","first_name":"Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop"}],"month":"07","publication_identifier":{"isbn":["978-3-662-47665-9"]},"conference":{"name":"ICALP: Automata, Languages and Programming","start_date":"2015-07-06","location":"Kyoto, Japan","end_date":"2015-07-10"},"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","oa_version":"None","main_file_link":[{"url":"https://arxiv.org/abs/1504.08259","open_access":"1"}],"day":"01","_id":"1610","doi":"10.1007/978-3-662-47666-6_10","year":"2015","date_created":"2018-12-11T11:53:01Z","citation":{"apa":"Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., &#38; Otop, J. (2015). Edit distance for pushdown automata. In <i>42nd International Colloquium</i> (Vol. 9135, pp. 121–133). Kyoto, Japan: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">https://doi.org/10.1007/978-3-662-47666-6_10</a>","mla":"Chatterjee, Krishnendu, et al. “Edit Distance for Pushdown Automata.” <i>42nd International Colloquium</i>, vol. 9135, no. Part II, Springer Nature, 2015, pp. 121–33, doi:<a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">10.1007/978-3-662-47666-6_10</a>.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan Otop. “Edit Distance for Pushdown Automata.” In <i>42nd International Colloquium</i>, 9135:121–33. Springer Nature, 2015. <a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">https://doi.org/10.1007/978-3-662-47666-6_10</a>.","ista":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2015. Edit distance for pushdown automata. 42nd International Colloquium. ICALP: Automata, Languages and Programming, LNCS, vol. 9135, 121–133.","ieee":"K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, “Edit distance for pushdown automata,” in <i>42nd International Colloquium</i>, Kyoto, Japan, 2015, vol. 9135, no. Part II, pp. 121–133.","ama":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. Edit distance for pushdown automata. In: <i>42nd International Colloquium</i>. Vol 9135. Springer Nature; 2015:121-133. doi:<a href=\"https://doi.org/10.1007/978-3-662-47666-6_10\">10.1007/978-3-662-47666-6_10</a>","short":"K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, in:, 42nd International Colloquium, Springer Nature, 2015, pp. 121–133."},"publist_id":"5556","related_material":{"record":[{"id":"465","relation":"later_version","status":"public"},{"relation":"earlier_version","id":"5438","status":"public"}]},"ec_funded":1,"project":[{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"name":"The Wittgenstein Prize","call_identifier":"FWF","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","call_identifier":"FWF"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"}],"date_published":"2015-07-01T00:00:00Z","publisher":"Springer Nature","quality_controlled":"1","volume":9135,"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"page":"121 - 133","publication_status":"published","abstract":[{"text":"The edit distance between two words w1, w2 is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform w1 to w2. The edit distance generalizes to languages L1,L2, where the edit distance is the minimal number k such that for every word from L1 there exists a word in L2 with edit distance at most k. We study the edit distance computation problem between pushdown automata and their subclasses. The problem of computing edit distance to pushdown automata is undecidable, and in practice, the interesting question is to compute the edit distance from a pushdown automaton (the implementation, a standard model for programs with recursion) to a regular language (the specification). In this work, we present a complete picture of decidability and complexity for deciding whether, for a given threshold k, the edit distance from a pushdown automaton to a finite automaton is at most k.","lang":"eng"}],"external_id":{"arxiv":["1504.08259"]}},{"ec_funded":1,"article_number":"17147","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.","year":"2015","publist_id":"5536","citation":{"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>","ieee":"A. Pavlogiannis, K. Chatterjee, B. Adlam, and M. Nowak, “Cellular cooperation with shift updating and repulsion,” <i>Scientific Reports</i>, vol. 5. Nature Publishing Group, 2015.","ama":"Pavlogiannis A, Chatterjee K, Adlam B, Nowak M. Cellular cooperation with shift updating and repulsion. <i>Scientific Reports</i>. 2015;5. doi:<a href=\"https://doi.org/10.1038/srep17147\">10.1038/srep17147</a>","short":"A. Pavlogiannis, K. Chatterjee, B. Adlam, M. Nowak, Scientific Reports 5 (2015).","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>.","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>.","ista":"Pavlogiannis A, Chatterjee K, Adlam B, Nowak M. 2015. Cellular cooperation with shift updating and repulsion. Scientific Reports. 5, 17147."},"date_created":"2018-12-11T11:53:06Z","doi":"10.1038/srep17147","file_date_updated":"2020-07-14T12:45:07Z","_id":"1624","ddc":["000"],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"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."}],"publication_status":"published","publisher":"Nature Publishing Group","date_published":"2015-11-25T00:00:00Z","department":[{"_id":"KrCh"}],"volume":5,"quality_controlled":"1","project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"scopus_import":1,"intvolume":"         5","has_accepted_license":"1","pubrep_id":"466","oa":1,"date_updated":"2021-01-12T06:52:05Z","title":"Cellular cooperation with shift updating and repulsion","publication":"Scientific Reports","language":[{"iso":"eng"}],"month":"11","day":"25","oa_version":"Published Version","file":[{"content_type":"application/pdf","file_size":1021931,"relation":"main_file","access_level":"open_access","creator":"system","date_updated":"2020-07-14T12:45:07Z","date_created":"2018-12-12T10:12:29Z","file_name":"IST-2016-466-v1+1_srep17147.pdf","file_id":"4947","checksum":"38e06d8310d2087cae5f6d4d4bfe082b"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"full_name":"Pavlogiannis, Andreas","first_name":"Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"first_name":"Ben","full_name":"Adlam, Ben","last_name":"Adlam"},{"last_name":"Nowak","first_name":"Martin","full_name":"Nowak, Martin"}],"type":"journal_article","status":"public"},{"arxiv":1,"author":[{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","full_name":"Otop, Jan","first_name":"Jan"}],"month":"07","conference":{"name":"LICS: Logic in Computer Science","start_date":"2015-07-06","location":"Kyoto, Japan","end_date":"2015-07-10"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"None","day":"31","type":"conference","status":"public","date_updated":"2023-02-23T12:26:19Z","title":"Nested weighted automata","scopus_import":1,"language":[{"iso":"eng"}],"publication":"Proceedings - Symposium on Logic in Computer Science","publication_status":"published","abstract":[{"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.","lang":"eng"}],"external_id":{"arxiv":["1606.03598"]},"project":[{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"date_published":"2015-07-31T00:00:00Z","publisher":"IEEE","quality_controlled":"1","volume":"2015-July","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"year":"2015","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","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.","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>.","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>.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, in:, Proceedings - Symposium on Logic in Computer Science, IEEE, 2015.","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>","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.","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>"},"publist_id":"5494","date_created":"2018-12-11T11:53:17Z","related_material":{"record":[{"id":"467","relation":"later_version","status":"public"},{"status":"public","id":"5415","relation":"earlier_version"},{"status":"public","id":"5436","relation":"earlier_version"}]},"article_number":"7174926","ec_funded":1,"_id":"1656","doi":"10.1109/LICS.2015.72"},{"alternative_title":["LICS"],"status":"public","type":"conference","conference":{"name":"LICS: Logic in Computer Science","start_date":"2015-07-06","location":"Kyoto, Japan","end_date":"2015-07-10"},"month":"07","oa_version":"None","day":"01","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Komárková","full_name":"Komárková, Zuzana","first_name":"Zuzana"},{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky","orcid":"0000-0002-8122-2881","first_name":"Jan","full_name":"Kretinsky, Jan"}],"language":[{"iso":"eng"}],"scopus_import":1,"date_updated":"2023-02-23T12:26:16Z","title":"Unifying two views on multiple mean-payoff objectives in Markov decision processes","publisher":"IEEE","date_published":"2015-07-01T00:00:00Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"page":"244 - 256","quality_controlled":"1","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","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","call_identifier":"FWF"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7"}],"series_title":"LICS","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"}],"publication_status":"published","doi":"10.1109/LICS.2015.32","_id":"1657","ec_funded":1,"related_material":{"record":[{"status":"public","id":"466","relation":"later_version"},{"status":"public","relation":"earlier_version","id":"5429"},{"id":"5435","relation":"earlier_version","status":"public"}]},"acknowledgement":"A Technical Report of this paper is available at:  https://repository.ist.ac.at/327\r\n","year":"2015","citation":{"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.","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.","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>.","ista":"Chatterjee K, Komárková Z, Kretinsky J. 2015. Unifying two views on multiple mean-payoff objectives in Markov decision processes. , 244–256.","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>."},"publist_id":"5493","date_created":"2018-12-11T11:53:18Z"},{"date_published":"2015-07-01T00:00:00Z","status":"public","type":"conference","publisher":"IEEE","alternative_title":["LICS"],"quality_controlled":"1","department":[{"_id":"KrCh"}],"page":"44 - 55","project":[{"_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7"}],"month":"07","conference":{"end_date":"2015-07-10","location":"Kyoto, Japan","start_date":"2015-07-06","name":"LICS: Logic in Computer Science"},"abstract":[{"lang":"eng","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."}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Preprint","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1505.02655"}],"day":"01","publication_status":"published","author":[{"last_name":"Brázdil","first_name":"Tomáš","full_name":"Brázdil, Tomáš"},{"full_name":"Kiefer, Stefan","first_name":"Stefan","last_name":"Kiefer"},{"first_name":"Antonín","full_name":"Kučera, Antonín","last_name":"Kučera"},{"last_name":"Novotny","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotny, Petr","first_name":"Petr"}],"doi":"10.1109/LICS.2015.15","language":[{"iso":"eng"}],"_id":"1660","scopus_import":1,"ec_funded":1,"year":"2015","oa":1,"date_updated":"2021-01-12T06:52:20Z","title":"Long-run average behaviour of probabilistic vector addition systems","publist_id":"5490","citation":{"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.","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>.","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>.","ieee":"T. Brázdil, S. Kiefer, A. Kučera, and P. Novotný, “Long-run average behaviour of probabilistic vector addition systems,” presented at the LICS: Logic in Computer Science, Kyoto, Japan, 2015, pp. 44–55.","ama":"Brázdil T, Kiefer S, Kučera A, Novotný P. Long-run average behaviour of probabilistic vector addition systems. In: IEEE; 2015:44-55. doi:<a href=\"https://doi.org/10.1109/LICS.2015.15\">10.1109/LICS.2015.15</a>","short":"T. Brázdil, S. Kiefer, A. Kučera, P. Novotný, in:, IEEE, 2015, pp. 44–55.","apa":"Brázdil, T., Kiefer, S., Kučera, A., &#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>"},"date_created":"2018-12-11T11:53:19Z"},{"scopus_import":"1","date_updated":"2025-06-02T08:53:41Z","oa":1,"article_processing_charge":"No","title":"Improved algorithms for one-pair and k-pair Streett objectives","publication":"Proceedings - Symposium on Logic in Computer Science","language":[{"iso":"eng"}],"conference":{"end_date":"2015-07-10","location":"Kyoto, Japan","start_date":"2015-07-06","name":"LICS: Logic in Computer Science"},"month":"07","oa_version":"Submitted Version","main_file_link":[{"open_access":"1","url":"https://eprints.cs.univie.ac.at/4368/"}],"day":"01","user_id":"6785fbc1-c503-11eb-8a32-93094b40e1cf","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"orcid":"0000-0002-5008-6530","last_name":"Henzinger","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","full_name":"Henzinger, Monika H","first_name":"Monika H"},{"full_name":"Loitzenbauer, Veronika","first_name":"Veronika","last_name":"Loitzenbauer"}],"status":"public","type":"conference","ec_funded":1,"related_material":{"record":[{"status":"public","id":"464","relation":"later_version"}]},"article_number":"7174888","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.","year":"2015","date_created":"2018-12-11T11:53:19Z","citation":{"apa":"Chatterjee, K., Henzinger, M. H., &#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. H. 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.","ama":"Chatterjee K, Henzinger MH, 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>","short":"K. Chatterjee, M.H. Henzinger, V. Loitzenbauer, in:, Proceedings - Symposium on Logic in Computer Science, IEEE, 2015.","ista":"Chatterjee K, Henzinger MH, 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>.","chicago":"Chatterjee, Krishnendu, Monika H 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>."},"publist_id":"5489","doi":"10.1109/LICS.2015.34","_id":"1661","abstract":[{"lang":"eng","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."}],"publication_status":"published","publisher":"IEEE","date_published":"2015-07-01T00:00:00Z","department":[{"_id":"KrCh"}],"volume":"2015-July","quality_controlled":"1","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"}]},{"page":"525 - 530","department":[{"_id":"KrCh"}],"volume":526,"quality_controlled":"1","publisher":"Nature Publishing Group","date_published":"2015-10-22T00:00:00Z","project":[{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"}],"external_id":{"pmid":["26466571"]},"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"}],"publication_status":"published","doi":"10.1038/nature15395","_id":"1665","article_type":"original","ec_funded":1,"date_created":"2018-12-11T11:53:21Z","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>","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>.","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>.","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.","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>","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.","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."},"publist_id":"5484","year":"2015","pmid":1,"type":"journal_article","status":"public","day":"22","main_file_link":[{"open_access":"1","url":"https://www.ncbi.nlm.nih.gov/pmc/articles/PMC4815041/"}],"oa_version":"Submitted Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"10","author":[{"first_name":"Dan","full_name":"Landau, Dan","last_name":"Landau"},{"last_name":"Tausch","full_name":"Tausch, Eugen","first_name":"Eugen"},{"last_name":"Taylor Weiner","full_name":"Taylor Weiner, Amaro","first_name":"Amaro"},{"last_name":"Stewart","first_name":"Chip","full_name":"Stewart, Chip"},{"full_name":"Reiter, Johannes","first_name":"Johannes","orcid":"0000-0002-0170-7353","id":"4A918E98-F248-11E8-B48F-1D18A9856A87","last_name":"Reiter"},{"last_name":"Bahlo","full_name":"Bahlo, Jasmin","first_name":"Jasmin"},{"last_name":"Kluth","full_name":"Kluth, Sandra","first_name":"Sandra"},{"last_name":"Božić","full_name":"Božić, Ivana","first_name":"Ivana"},{"first_name":"Michael","full_name":"Lawrence, Michael","last_name":"Lawrence"},{"first_name":"Sebastian","full_name":"Böttcher, Sebastian","last_name":"Böttcher"},{"first_name":"Scott","full_name":"Carter, Scott","last_name":"Carter"},{"first_name":"Kristian","full_name":"Cibulskis, Kristian","last_name":"Cibulskis"},{"last_name":"Mertens","full_name":"Mertens, Daniel","first_name":"Daniel"},{"first_name":"Carrie","full_name":"Sougnez, Carrie","last_name":"Sougnez"},{"full_name":"Rosenberg, Mara","first_name":"Mara","last_name":"Rosenberg"},{"first_name":"Julian","full_name":"Hess, Julian","last_name":"Hess"},{"last_name":"Edelmann","full_name":"Edelmann, Jennifer","first_name":"Jennifer"},{"last_name":"Kless","first_name":"Sabrina","full_name":"Kless, Sabrina"},{"full_name":"Kneba, Michael","first_name":"Michael","last_name":"Kneba"},{"last_name":"Ritgen","full_name":"Ritgen, Matthias","first_name":"Matthias"},{"full_name":"Fink, Anna","first_name":"Anna","last_name":"Fink"},{"last_name":"Fischer","first_name":"Kirsten","full_name":"Fischer, Kirsten"},{"last_name":"Gabriel","full_name":"Gabriel, Stacey","first_name":"Stacey"},{"full_name":"Lander, Eric","first_name":"Eric","last_name":"Lander"},{"first_name":"Martin","full_name":"Nowak, Martin","last_name":"Nowak"},{"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"},{"last_name":"Getz","first_name":"Gad","full_name":"Getz, Gad"},{"first_name":"Stephan","full_name":"Stilgenbauer, Stephan","last_name":"Stilgenbauer"},{"first_name":"Catherine","full_name":"Wu, Catherine","last_name":"Wu"}],"publication":"Nature","language":[{"iso":"eng"}],"intvolume":"       526","scopus_import":1,"title":"Mutations driving CLL and their evolution in progression and relapse","date_updated":"2021-01-12T06:52:23Z","oa":1,"issue":"7574","article_processing_charge":"No"},{"scopus_import":1,"intvolume":"      9259","title":"Optimizing performance of continuous-time stochastic systems using timeout synthesis","date_updated":"2021-01-12T06:52:24Z","oa":1,"language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"22","main_file_link":[{"url":"http://arxiv.org/abs/1407.4777","open_access":"1"}],"oa_version":"Preprint","month":"08","conference":{"location":"Madrid, Spain","end_date":"2015-09-03","name":"QEST: Quantitative Evaluation of Systems","start_date":"2015-09-01"},"author":[{"last_name":"Brázdil","full_name":"Brázdil, Tomáš","first_name":"Tomáš"},{"full_name":"Korenčiak, L'Uboš","first_name":"L'Uboš","last_name":"Korenčiak"},{"last_name":"Krčál","full_name":"Krčál, Jan","first_name":"Jan"},{"first_name":"Petr","full_name":"Novotny, Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","last_name":"Novotny"},{"last_name":"Řehák","first_name":"Vojtěch","full_name":"Řehák, Vojtěch"}],"type":"conference","status":"public","alternative_title":["LNCS"],"ec_funded":1,"date_created":"2018-12-11T11:53:22Z","publist_id":"5482","citation":{"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>","short":"T. Brázdil, L. Korenčiak, J. Krčál, P. Novotný, V. Řehák, 9259 (2015) 141–159.","ieee":"T. Brázdil, L. Korenčiak, J. Krčál, P. Novotný, and V. Řehák, “Optimizing performance of continuous-time stochastic systems using timeout synthesis,” vol. 9259. Springer, pp. 141–159, 2015.","ama":"Brázdil T, Korenčiak L, Krčál J, Novotný P, Řehák V. Optimizing performance of continuous-time stochastic systems using timeout synthesis. 2015;9259:141-159. doi:<a href=\"https://doi.org/10.1007/978-3-319-22264-6_10\">10.1007/978-3-319-22264-6_10</a>","ista":"Brázdil T, Korenčiak L, Krčál J, Novotný P, Řehák V. 2015. Optimizing performance of continuous-time stochastic systems using timeout synthesis. 9259, 141–159.","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>.","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>."},"year":"2015","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.","doi":"10.1007/978-3-319-22264-6_10","_id":"1667","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"}],"series_title":"Lecture Notes in Computer Science","publication_status":"published","volume":9259,"quality_controlled":"1","department":[{"_id":"KrCh"}],"page":"141 - 159","date_published":"2015-08-22T00:00:00Z","publisher":"Springer","project":[{"_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7"}]},{"citation":{"apa":"Adlam, B., Chatterjee, K., &#38; Nowak, M. (2015). Amplifiers of selection. <i>Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences</i>. Royal Society of London. <a href=\"https://doi.org/10.1098/rspa.2015.0114\">https://doi.org/10.1098/rspa.2015.0114</a>","short":"B. Adlam, K. Chatterjee, M. Nowak, Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences 471 (2015).","ieee":"B. Adlam, K. Chatterjee, and M. Nowak, “Amplifiers of selection,” <i>Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences</i>, vol. 471, no. 2181. Royal Society of London, 2015.","ama":"Adlam B, Chatterjee K, Nowak M. Amplifiers of selection. <i>Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences</i>. 2015;471(2181). doi:<a href=\"https://doi.org/10.1098/rspa.2015.0114\">10.1098/rspa.2015.0114</a>","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>.","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.","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>."},"publist_id":"5477","date_created":"2018-12-11T11:53:24Z","year":"2015","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). ","article_number":"20150114","ec_funded":1,"_id":"1673","file_date_updated":"2020-07-14T12:45:11Z","doi":"10.1098/rspa.2015.0114","publication_status":"published","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"}],"ddc":["000"],"project":[{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"}],"quality_controlled":"1","volume":471,"department":[{"_id":"KrCh"}],"date_published":"2015-09-08T00:00:00Z","publisher":"Royal Society of London","title":"Amplifiers of selection","issue":"2181","date_updated":"2021-01-12T06:52:26Z","oa":1,"has_accepted_license":"1","intvolume":"       471","scopus_import":1,"language":[{"iso":"eng"}],"publication":"Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences","author":[{"first_name":"Ben","full_name":"Adlam, Ben","last_name":"Adlam"},{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"last_name":"Nowak","full_name":"Nowak, Martin","first_name":"Martin"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","file":[{"file_name":"2015_rspa_Adlam.pdf","checksum":"e613d94d283c776322403a28aad11bdd","file_id":"6342","date_updated":"2020-07-14T12:45:11Z","date_created":"2019-04-18T12:39:56Z","creator":"kschuh","relation":"main_file","access_level":"open_access","file_size":391466,"content_type":"application/pdf"}],"oa_version":"Published Version","day":"08","month":"09","status":"public","type":"journal_article"},{"article_type":"original","_id":"1681","file_date_updated":"2020-07-14T12:45:12Z","doi":"10.3390/g6040413","year":"2015","citation":{"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>","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.","short":"T. Priklopil, K. Chatterjee, Games 6 (2015) 413–437.","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>.","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>.","ista":"Priklopil T, Chatterjee K. 2015. Evolution of decisions in population games with sequentially searching individuals. Games. 6(4), 413–437."},"date_created":"2018-12-11T11:53:26Z","publist_id":"5467","ec_funded":1,"project":[{"name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"}],"date_published":"2015-09-29T00:00:00Z","publisher":"MDPI","quality_controlled":"1","volume":6,"department":[{"_id":"NiBa"},{"_id":"KrCh"}],"page":"413 - 437","publication_status":"published","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"ddc":["000"],"abstract":[{"text":"In many social situations, individuals endeavor to find the single best possible partner, but are constrained to evaluate the candidates in sequence. Examples include the search for mates, economic partnerships, or any other long-term ties where the choice to interact involves two parties. Surprisingly, however, previous theoretical work on mutual choice problems focuses on finding equilibrium solutions, while ignoring the evolutionary dynamics of decisions. Empirically, this may be of high importance, as some equilibrium solutions can never be reached unless the population undergoes radical changes and a sufficient number of individuals change their decisions simultaneously. To address this question, we apply a mutual choice sequential search problem in an evolutionary game-theoretical model that allows one to find solutions that are favored by evolution. As an example, we study the influence of sequential search on the evolutionary dynamics of cooperation. For this, we focus on the classic snowdrift game and the prisoner’s dilemma game.","lang":"eng"}],"language":[{"iso":"eng"}],"publication":"Games","issue":"4","article_processing_charge":"No","oa":1,"date_updated":"2023-10-17T11:42:52Z","pubrep_id":"448","title":"Evolution of decisions in population games with sequentially searching individuals","has_accepted_license":"1","scopus_import":"1","intvolume":"         6","status":"public","type":"journal_article","author":[{"full_name":"Priklopil, Tadeas","first_name":"Tadeas","last_name":"Priklopil","id":"3C869AA0-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"}],"month":"09","publication_identifier":{"eissn":["2073-4336"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"checksum":"912e1acbaf201100f447a43e4d5958bd","file_name":"IST-2016-448-v1+1_games-06-00413.pdf","file_id":"4959","date_updated":"2020-07-14T12:45:12Z","date_created":"2018-12-12T10:12:41Z","creator":"system","relation":"main_file","content_type":"application/pdf","file_size":518832,"access_level":"open_access"}],"day":"29","oa_version":"Published Version"},{"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"page":"259 - 268","publisher":"ACM","type":"conference","date_published":"2015-04-14T00:00:00Z","status":"public","project":[{"grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7"},{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"}],"main_file_link":[{"url":"http://arxiv.org/abs/1410.5387","open_access":"1"}],"day":"14","oa_version":"Preprint","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","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."}],"conference":{"name":"HSCC: Hybrid Systems - Computation and Control","start_date":"2015-04-14","location":"Seattle, WA, United States","end_date":"2015-04-16"},"month":"04","author":[{"last_name":"Svoreňová","full_name":"Svoreňová, Mária","first_name":"Mária"},{"first_name":"Jan","full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"},{"id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik","first_name":"Martin","full_name":"Chmelik, Martin"},{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"full_name":"Cěrná, Ivana","first_name":"Ivana","last_name":"Cěrná"},{"full_name":"Belta, Cǎlin","first_name":"Cǎlin","last_name":"Belta"}],"publication_status":"published","doi":"10.1145/2728606.2728608","publication":"Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control","_id":"1689","language":[{"iso":"eng"}],"ec_funded":1,"related_material":{"record":[{"id":"1407","relation":"later_version","status":"public"}]},"scopus_import":1,"date_created":"2018-12-11T11:53:29Z","publist_id":"5456","title":"Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games","citation":{"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>.","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>.","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>","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."},"oa":1,"date_updated":"2023-09-20T09:43:09Z","year":"2015"},{"scopus_import":1,"ec_funded":1,"date_created":"2018-12-11T11:53:29Z","publist_id":"5453","citation":{"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>","short":"M. Svoreňová, M. Chmelik, K. Leahy, H. Eniser, K. Chatterjee, I. Cěrná, C. Belta, in:, Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, ACM, 2015, pp. 233–238.","ama":"Svoreňová M, Chmelik M, Leahy K, et al. Temporal logic motion planning using POMDPs with parity objectives: Case study paper. In: <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>","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.","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>.","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>.","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."},"title":"Temporal logic motion planning using POMDPs with parity objectives: Case study paper","year":"2015","date_updated":"2021-01-12T06:52:33Z","doi":"10.1145/2728606.2728617","publication":"Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control","_id":"1691","language":[{"iso":"eng"}],"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"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"14","oa_version":"None","month":"04","conference":{"name":"HSCC: Hybrid Systems - Computation and Control","start_date":"2015-04-14","location":"Seattle, WA, United States","end_date":"2015-04-16"},"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"},{"first_name":"Kevin","full_name":"Leahy, Kevin","last_name":"Leahy"},{"last_name":"Eniser","first_name":"Hasan","full_name":"Eniser, Hasan"},{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"full_name":"Cěrná, Ivana","first_name":"Ivana","last_name":"Cěrná"},{"last_name":"Belta","full_name":"Belta, Cǎlin","first_name":"Cǎlin"}],"publication_status":"published","page":"233 - 238","department":[{"_id":"KrCh"}],"date_published":"2015-04-14T00:00:00Z","type":"conference","status":"public","publisher":"ACM","project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"}]},{"citation":{"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>.","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.","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.","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>","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>"},"date_created":"2018-12-11T11:53:30Z","publist_id":"5450","title":"Quantitative temporal simulation and refinement distances for timed systems","year":"2015","issue":"9","date_updated":"2021-01-12T06:52:34Z","intvolume":"        60","scopus_import":1,"ec_funded":1,"language":[{"iso":"eng"}],"_id":"1694","doi":"10.1109/TAC.2015.2404612","publication":"IEEE Transactions on Automatic Control","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"full_name":"Prabhu, Vinayak","first_name":"Vinayak","last_name":"Prabhu"}],"publication_status":"published","abstract":[{"text":"\r\nWe introduce quantitative timed refinement and timed simulation (directed) metrics, incorporating zenoness checks, for timed systems. These metrics assign positive real numbers which quantify the timing mismatches between two timed systems, amongst non-zeno runs. We quantify timing mismatches in three ways: (1) the maximal timing mismatch that can arise, (2) the “steady-state” maximal timing mismatches, where initial transient timing mismatches are ignored; and (3) the (long-run) average timing mismatches amongst two systems. These three kinds of mismatches constitute three important types of timing differences. Our event times are the global times, measured from the start of the system execution, not just the time durations of individual steps. We present algorithms over timed automata for computing the three quantitative simulation distances to within any desired degree of accuracy. In order to compute the values of the quantitative simulation distances, we use a game theoretic formulation. We introduce two new kinds of objectives for two player games on finite-state game graphs: (1) eventual debit-sum level objectives, and (2) average debit-sum level objectives. We present algorithms for computing the optimal values for these objectives in graph games, and then use these algorithms to compute the values of the timed simulation distances over timed automata.\r\n","lang":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"24","oa_version":"None","month":"02","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"volume":60,"quality_controlled":"1","page":"2291 - 2306","department":[{"_id":"KrCh"}],"status":"public","type":"journal_article","date_published":"2015-02-24T00:00:00Z","publisher":"IEEE"},{"doi":"10.1016/j.ic.2015.03.001","_id":"1698","ec_funded":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).","year":"2015","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.","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>","short":"Y. Velner, K. Chatterjee, L. Doyen, T.A. Henzinger, A. Rabinovich, J. Raskin, Information and Computation 241 (2015) 177–196.","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.","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>.","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>.","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>"},"publist_id":"5443","date_created":"2018-12-11T11:53:32Z","publisher":"Elsevier","date_published":"2015-04-01T00:00:00Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"page":"177 - 196","quality_controlled":"1","volume":241,"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"},{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","call_identifier":"FP7","name":"Quantitative Reactive Modeling"}],"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"}],"publication_status":"published","publication":"Information and Computation","language":[{"iso":"eng"}],"intvolume":"       241","scopus_import":1,"oa":1,"date_updated":"2021-01-12T06:52:36Z","issue":"4","title":"The complexity of multi-mean-payoff and multi-energy games","status":"public","type":"journal_article","month":"04","day":"01","oa_version":"Preprint","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1209.3234"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"last_name":"Velner","full_name":"Velner, Yaron","first_name":"Yaron"},{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Doyen","full_name":"Doyen, Laurent","first_name":"Laurent"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"},{"first_name":"Alexander","full_name":"Rabinovich, Alexander","last_name":"Rabinovich"},{"first_name":"Jean","full_name":"Raskin, Jean","last_name":"Raskin"}]}]