[{"date_published":"2015-04-27T00:00:00Z","type":"technical_report","status":"public","publisher":"IST Austria","alternative_title":["IST Austria Technical Report"],"department":[{"_id":"KrCh"}],"page":"27","month":"04","publication_identifier":{"issn":["2664-1690"]},"ddc":["000"],"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. \r\nThe 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.\r\nOur main theoretical results are as follows.\r\nFirst, for constant treewidth graphs we present an algorithm that approximates the mean-payoff value within a multiplicative factor of $\\epsilon$ in time $O(n \\cdot \\log (n/\\epsilon))$ 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 \\cdot \\log (|a\\cdot b|))=O(n\\cdot\\log (n\\cdot W))$, when the output is $\\frac{a}{b}$, as compared to the previously best known algorithm with running time $O(n^2 \\cdot \\log (n\\cdot W))$. Third, for the minimum initial credit problem we show that (i)~for general graphs the problem can be solved in $O(n^2\\cdot m)$ time and the associated decision problem can be solved in $O(n\\cdot m)$ time, improving the previous known $O(n^3\\cdot m\\cdot \\log (n\\cdot W))$ and $O(n^2 \\cdot m)$ bounds, respectively; and (ii)~for constant treewidth graphs we present an algorithm that requires $O(n\\cdot \\log n)$ time, improving the previous known $O(n^4 \\cdot \\log (n \\cdot W))$ bound.\r\nWe have implemented some of our algorithms and show that they present a significant speedup on standard benchmarks. "}],"file":[{"file_size":1072137,"content_type":"application/pdf","relation":"main_file","access_level":"open_access","creator":"system","date_updated":"2020-07-14T12:46:54Z","date_created":"2018-12-12T11:53:12Z","file_name":"IST-2015-330-v2+1_main.pdf","checksum":"f5917c20f84018b362d385c000a2e123","file_id":"5473"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"27","oa_version":"Published Version","publication_status":"published","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"id":"3B699956-F248-11E8-B48F-1D18A9856A87","last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus"},{"first_name":"Andreas","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722"}],"doi":"10.15479/AT:IST-2015-330-v2-1","language":[{"iso":"eng"}],"_id":"5437","file_date_updated":"2020-07-14T12:46:54Z","related_material":{"record":[{"status":"public","id":"1607","relation":"later_version"},{"status":"public","relation":"earlier_version","id":"5430"}]},"has_accepted_license":"1","year":"2015","pubrep_id":"333","date_updated":"2023-02-23T12:26:05Z","oa":1,"date_created":"2018-12-12T11:39:19Z","citation":{"chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. <i>Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs</i>. IST Austria, 2015. <a href=\"https://doi.org/10.15479/AT:IST-2015-330-v2-1\">https://doi.org/10.15479/AT:IST-2015-330-v2-1</a>.","mla":"Chatterjee, Krishnendu, et al. <i>Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs</i>. IST Austria, 2015, doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-330-v2-1\">10.15479/AT:IST-2015-330-v2-1</a>.","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2015. Faster algorithms for quantitative verification in constant treewidth graphs, IST Austria, 27p.","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs, IST Austria, 2015.","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. <i>Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs</i>. IST Austria; 2015. doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-330-v2-1\">10.15479/AT:IST-2015-330-v2-1</a>","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, <i>Faster algorithms for quantitative verification in constant treewidth graphs</i>. IST Austria, 2015.","apa":"Chatterjee, K., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2015). <i>Faster algorithms for quantitative verification in constant treewidth graphs</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2015-330-v2-1\">https://doi.org/10.15479/AT:IST-2015-330-v2-1</a>"},"title":"Faster algorithms for quantitative verification in constant treewidth graphs"},{"department":[{"_id":"KrCh"}],"page":"15","alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","date_published":"2015-05-05T00:00:00Z","type":"technical_report","status":"public","day":"05","oa_version":"Published Version","file":[{"date_created":"2018-12-12T11:53:56Z","date_updated":"2020-07-14T12:46:55Z","file_name":"IST-2015-334-v1+1_report.pdf","file_id":"5518","checksum":"8a5f2d77560e552af87eb1982437a43b","relation":"main_file","file_size":422573,"content_type":"application/pdf","access_level":"open_access","creator":"system"}],"abstract":[{"lang":"eng","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.\r\nThe problem of computing edit distance to a pushdown automaton 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. "}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["004"],"month":"05","publication_identifier":{"issn":["2664-1690"]},"publication_status":"published","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"},{"first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389"},{"id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","full_name":"Otop, Jan","first_name":"Jan"}],"doi":"10.15479/AT:IST-2015-334-v1-1","file_date_updated":"2020-07-14T12:46:55Z","language":[{"iso":"eng"}],"_id":"5438","has_accepted_license":"1","related_material":{"record":[{"status":"public","id":"1610","relation":"later_version"},{"relation":"later_version","id":"465","status":"public"}]},"title":"Edit distance for pushdown automata","date_created":"2018-12-12T11:39:20Z","citation":{"apa":"Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., &#38; Otop, J. (2015). <i>Edit distance for pushdown automata</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2015-334-v1-1\">https://doi.org/10.15479/AT:IST-2015-334-v1-1</a>","ista":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2015. Edit distance for pushdown automata, IST Austria, 15p.","mla":"Chatterjee, Krishnendu, et al. <i>Edit Distance for Pushdown Automata</i>. IST Austria, 2015, doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-334-v1-1\">10.15479/AT:IST-2015-334-v1-1</a>.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan Otop. <i>Edit Distance for Pushdown Automata</i>. IST Austria, 2015. <a href=\"https://doi.org/10.15479/AT:IST-2015-334-v1-1\">https://doi.org/10.15479/AT:IST-2015-334-v1-1</a>.","short":"K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, Edit Distance for Pushdown Automata, IST Austria, 2015.","ama":"Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. <i>Edit Distance for Pushdown Automata</i>. IST Austria; 2015. doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-334-v1-1\">10.15479/AT:IST-2015-334-v1-1</a>","ieee":"K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, <i>Edit distance for pushdown automata</i>. IST Austria, 2015."},"oa":1,"date_updated":"2023-02-23T12:20:08Z","pubrep_id":"334","year":"2015"},{"page":"18","department":[{"_id":"KrCh"}],"status":"public","type":"technical_report","date_published":"2015-06-16T00:00:00Z","publisher":"IST Austria","alternative_title":["IST Austria Technical Report"],"publication_status":"published","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"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":"Nowak, Martin","first_name":"Martin","last_name":"Nowak"}],"file":[{"relation":"main_file","access_level":"open_access","content_type":"application/pdf","file_size":466161,"creator":"system","date_updated":"2020-07-14T12:46:56Z","date_created":"2018-12-12T11:53:23Z","file_name":"IST-2015-323-v2+2_main.pdf","file_id":"5484","checksum":"66aace7d367032af97c15e35c9be9636"}],"abstract":[{"lang":"eng","text":"Evolution occurs in populations of reproducing individuals. The structure of the population affects the outcome of the evolutionary process. Evolutionary graph theory is a powerful approach to study this phenomenon. There are two graphs. The interaction graph specifies who interacts with whom for payoff in the context of evolution. The replacement graph specifies who competes with whom for reproduction. The vertices of the two graphs are the same, and each vertex corresponds to an individual of the population. The fitness (or the reproductive rate) is a non-negative number, and depends on the payoff. A key quantity is the fixation probability of a new mutant. It is defined as the probability that a newly introduced mutant (on a single vertex) generates a lineage of offspring which eventually takes over the entire population of resident individuals. The basic computational questions are as follows: (i) the qualitative question asks whether the fixation probability is positive; and (ii) the quantitative approximation question asks for an approximation of the fixation probability. Our main results are as follows: First, we consider a special case of the general problem, where the residents do not reproduce. We show that the qualitative question is NP-complete, and the quantitative approximation question is #P-complete, and the hardness results hold even in the special case where the interaction and the replacement graphs coincide. Second, we show that in general both the qualitative and the quantitative approximation questions are PSPACE-complete. The PSPACE-hardness result for quantitative approximation holds even when the fitness is always positive."}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Published Version","day":"16","publication_identifier":{"issn":["2664-1690"]},"month":"06","ddc":["005","576"],"language":[{"iso":"eng"}],"_id":"5440","file_date_updated":"2020-07-14T12:46:56Z","doi":"10.15479/AT:IST-2015-323-v2-2","date_created":"2018-12-12T11:39:21Z","title":"The complexity of evolutionary games on graphs","citation":{"apa":"Chatterjee, K., Ibsen-Jensen, R., &#38; Nowak, M. (2015). <i>The complexity of evolutionary games on graphs</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2015-323-v2-2\">https://doi.org/10.15479/AT:IST-2015-323-v2-2</a>","ista":"Chatterjee K, Ibsen-Jensen R, Nowak M. 2015. The complexity of evolutionary games on graphs, IST Austria, 18p.","mla":"Chatterjee, Krishnendu, et al. <i>The Complexity of Evolutionary Games on Graphs</i>. IST Austria, 2015, doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-323-v2-2\">10.15479/AT:IST-2015-323-v2-2</a>.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Martin Nowak. <i>The Complexity of Evolutionary Games on Graphs</i>. IST Austria, 2015. <a href=\"https://doi.org/10.15479/AT:IST-2015-323-v2-2\">https://doi.org/10.15479/AT:IST-2015-323-v2-2</a>.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and M. Nowak, <i>The complexity of evolutionary games on graphs</i>. IST Austria, 2015.","ama":"Chatterjee K, Ibsen-Jensen R, Nowak M. <i>The Complexity of Evolutionary Games on Graphs</i>. IST Austria; 2015. doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-323-v2-2\">10.15479/AT:IST-2015-323-v2-2</a>","short":"K. Chatterjee, R. Ibsen-Jensen, M. Nowak, The Complexity of Evolutionary Games on Graphs, IST Austria, 2015."},"year":"2015","pubrep_id":"338","oa":1,"date_updated":"2023-02-23T12:26:10Z","has_accepted_license":"1","related_material":{"record":[{"relation":"earlier_version","id":"5421","status":"public"},{"status":"public","relation":"earlier_version","id":"5432"}]}},{"alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","type":"technical_report","date_published":"2015-07-11T00:00:00Z","status":"public","page":"24","department":[{"_id":"KrCh"}],"publication_status":"published","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389"},{"full_name":"Goharshady, Amir","first_name":"Amir","orcid":"0000-0003-1702-6584","last_name":"Goharshady","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Pavlogiannis, Andreas","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722"}],"ddc":["000"],"publication_identifier":{"issn":["2664-1690"]},"month":"07","day":"11","oa_version":"Published Version","abstract":[{"text":"We study algorithmic questions for concurrent systems where the transitions are labeled from a complete, closed semiring, and path properties are algebraic with semiring operations. The algebraic path properties can model dataflow analysis problems, the shortest path problem, and many other natural problems that arise in program analysis. We consider that each component of the concurrent system is a graph with constant treewidth, a property satisfied by the controlflow graphs of most programs. We allow for multiple possible queries, which arise naturally in demand driven dataflow analysis. The study of multiple queries allows us to consider the tradeoff between the resource usage of the one-time preprocessing and for each individual query. The traditional approach constructs the product graph of all components and applies the best-known graph algorithm on the product. In this approach, even the answer to a single query requires the transitive closure (i.e., the results of all possible queries), which provides no room for tradeoff between preprocessing and query time. Our main contributions are algorithms that significantly improve the worst-case running time of the traditional approach, and provide various tradeoffs depending on the number of queries. For example, in a concurrent system of two components, the traditional approach requires hexic time in the worst case for answering one query as well as computing the transitive closure, whereas we show that with one-time preprocessing in almost cubic time, each subsequent query can be answered in at most linear time, and even the transitive closure can be computed in almost quartic time. Furthermore, we establish conditional optimality results showing that the worst-case running time of our algorithms cannot be improved without achieving major breakthroughs in graph algorithms (i.e., improving the worst-case bound for the shortest path problem in general graphs). Preliminary experimental results show that our algorithms perform favorably on several benchmarks.","lang":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"creator":"system","file_size":861396,"access_level":"open_access","content_type":"application/pdf","relation":"main_file","checksum":"df383dc62c94d7b2ea639aba088a76c6","file_name":"IST-2015-340-v1+1_main.pdf","file_id":"5531","date_updated":"2020-07-14T12:46:56Z","date_created":"2018-12-12T11:54:09Z"}],"file_date_updated":"2020-07-14T12:46:56Z","_id":"5441","language":[{"iso":"eng"}],"doi":"10.15479/AT:IST-2015-340-v1-1","pubrep_id":"340","date_updated":"2023-09-19T14:36:19Z","oa":1,"year":"2015","title":"Algorithms for algebraic path properties in concurrent systems of constant treewidth components","date_created":"2018-12-12T11:39:21Z","citation":{"apa":"Chatterjee, K., Ibsen-Jensen, R., Goharshady, A. K., &#38; Pavlogiannis, A. (2015). <i>Algorithms for algebraic path properties in concurrent systems of constant treewidth components</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2015-340-v1-1\">https://doi.org/10.15479/AT:IST-2015-340-v1-1</a>","ama":"Chatterjee K, Ibsen-Jensen R, Goharshady AK, Pavlogiannis A. <i>Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components</i>. IST Austria; 2015. doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-340-v1-1\">10.15479/AT:IST-2015-340-v1-1</a>","ieee":"K. Chatterjee, R. Ibsen-Jensen, A. K. Goharshady, and A. Pavlogiannis, <i>Algorithms for algebraic path properties in concurrent systems of constant treewidth components</i>. IST Austria, 2015.","short":"K. Chatterjee, R. Ibsen-Jensen, A.K. Goharshady, A. Pavlogiannis, Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components, IST Austria, 2015.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Amir Kafshdar Goharshady, and Andreas Pavlogiannis. <i>Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components</i>. IST Austria, 2015. <a href=\"https://doi.org/10.15479/AT:IST-2015-340-v1-1\">https://doi.org/10.15479/AT:IST-2015-340-v1-1</a>.","ista":"Chatterjee K, Ibsen-Jensen R, Goharshady AK, Pavlogiannis A. 2015. Algorithms for algebraic path properties in concurrent systems of constant treewidth components, IST Austria, 24p.","mla":"Chatterjee, Krishnendu, et al. <i>Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components</i>. IST Austria, 2015, doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-340-v1-1\">10.15479/AT:IST-2015-340-v1-1</a>."},"has_accepted_license":"1","related_material":{"record":[{"status":"public","relation":"later_version","id":"1437"},{"status":"public","id":"5442","relation":"earlier_version"},{"status":"public","relation":"later_version","id":"6009"}]}},{"related_material":{"record":[{"status":"public","relation":"later_version","id":"1166"}]},"has_accepted_license":"1","citation":{"apa":"Chatterjee, K., Chmelik, M., &#38; Davies, J. (2015). <i>A symbolic SAT-based algorithm for almost-sure reachability with small strategies in POMDPs</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2015-325-v2-1\">https://doi.org/10.15479/AT:IST-2015-325-v2-1</a>","ista":"Chatterjee K, Chmelik M, Davies J. 2015. A symbolic SAT-based algorithm for almost-sure reachability with small strategies in POMDPs, IST Austria, 23p.","mla":"Chatterjee, Krishnendu, et al. <i>A Symbolic SAT-Based Algorithm for Almost-Sure Reachability with Small Strategies in POMDPs</i>. IST Austria, 2015, doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-325-v2-1\">10.15479/AT:IST-2015-325-v2-1</a>.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Jessica Davies. <i>A Symbolic SAT-Based Algorithm for Almost-Sure Reachability with Small Strategies in POMDPs</i>. IST Austria, 2015. <a href=\"https://doi.org/10.15479/AT:IST-2015-325-v2-1\">https://doi.org/10.15479/AT:IST-2015-325-v2-1</a>.","ama":"Chatterjee K, Chmelik M, Davies J. <i>A Symbolic SAT-Based Algorithm for Almost-Sure Reachability with Small Strategies in POMDPs</i>. IST Austria; 2015. doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-325-v2-1\">10.15479/AT:IST-2015-325-v2-1</a>","ieee":"K. Chatterjee, M. Chmelik, and J. Davies, <i>A symbolic SAT-based algorithm for almost-sure reachability with small strategies in POMDPs</i>. IST Austria, 2015.","short":"K. Chatterjee, M. Chmelik, J. Davies, A Symbolic SAT-Based Algorithm for Almost-Sure Reachability with Small Strategies in POMDPs, IST Austria, 2015."},"date_created":"2018-12-12T11:39:22Z","title":"A symbolic SAT-based algorithm for almost-sure reachability with small strategies in POMDPs","date_updated":"2023-02-21T16:24:05Z","pubrep_id":"362","oa":1,"year":"2015","doi":"10.15479/AT:IST-2015-325-v2-1","file_date_updated":"2020-07-14T12:46:57Z","_id":"5443","language":[{"iso":"eng"}],"day":"06","oa_version":"Published Version","file":[{"creator":"system","access_level":"open_access","file_size":412379,"content_type":"application/pdf","relation":"main_file","checksum":"f0fa31ad8161ed655137e94012123ef9","file_name":"IST-2015-325-v2+1_main.pdf","file_id":"5466","date_updated":"2020-07-14T12:46:57Z","date_created":"2018-12-12T11:53:05Z"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"lang":"eng","text":"POMDPs are standard models for probabilistic planning problems, where an agent interacts with an uncertain environment. We study the problem of almost-sure reachability, where given a set of target states, the question is to decide whether there is a policy to ensure that the target set is reached with probability 1 (almost-surely). While in general the problem is EXPTIME-complete, in many practical cases policies with a small amount of memory suffice. Moreover, the existing solution to the problem is explicit, which first requires to construct explicitly an exponential reduction to a belief-support MDP. In this work, we first study the existence of observation-stationary strategies, which is NP-complete, and then small-memory strategies. We present a symbolic algorithm by an efficient encoding to SAT and using a SAT solver for the problem. We report experimental results demonstrating the scalability of our symbolic (SAT-based) approach."}],"ddc":["000"],"month":"11","publication_identifier":{"issn":["2664-1690"]},"author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"first_name":"Martin","full_name":"Chmelik, Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik"},{"first_name":"Jessica","full_name":"Davies, Jessica","id":"378E0060-F248-11E8-B48F-1D18A9856A87","last_name":"Davies"}],"publication_status":"published","department":[{"_id":"KrCh"}],"page":"23","alternative_title":["IST Austria Technical Report"],"publisher":"IST Austria","type":"technical_report","status":"public","date_published":"2015-11-06T00:00:00Z"},{"ddc":["000","576"],"month":"12","publication_identifier":{"issn":["2664-1690"]},"oa_version":"Published Version","day":"30","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"lang":"eng","text":"A comprehensive understanding of the clonal evolution of cancer is critical for understanding neoplasia. Genome-wide sequencing data enables evolutionary studies at unprecedented depth. However, classical phylogenetic methods often struggle with noisy sequencing data of impure DNA samples and fail to detect subclones that have different evolutionary trajectories. We have developed a tool, called Treeomics, that allows us to reconstruct the phylogeny of a cancer with commonly available sequencing technologies. Using Bayesian inference and Integer Linear Programming, robust phylogenies consistent with the biological processes underlying cancer evolution were obtained for pancreatic, ovarian, and prostate cancers. Furthermore, Treeomics correctly identified sequencing artifacts such as those resulting from low statistical power; nearly 7% of variants were misclassified by conventional statistical methods. These artifacts can skew phylogenies by creating illusory tumor heterogeneity among distinct samples. Importantly, we show that the evolutionary trees generated with Treeomics are mathematically optimal."}],"file":[{"creator":"system","relation":"main_file","access_level":"open_access","file_size":3533200,"content_type":"application/pdf","file_id":"5485","file_name":"IST-2015-399-v1+1_treeomics.pdf","checksum":"c47d33bdda06181753c0af36f16e7b5d","date_updated":"2020-07-14T12:46:58Z","date_created":"2018-12-12T11:53:24Z"}],"author":[{"full_name":"Reiter, Johannes","first_name":"Johannes","orcid":"0000-0002-0170-7353","last_name":"Reiter","id":"4A918E98-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Makohon-Moore","full_name":"Makohon-Moore, Alvin","first_name":"Alvin"},{"last_name":"Gerold","full_name":"Gerold, Jeffrey","first_name":"Jeffrey"},{"full_name":"Bozic, Ivana","first_name":"Ivana","last_name":"Bozic"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"first_name":"Christine","full_name":"Iacobuzio-Donahue, Christine","last_name":"Iacobuzio-Donahue"},{"last_name":"Vogelstein","full_name":"Vogelstein, Bert","first_name":"Bert"},{"last_name":"Nowak","full_name":"Nowak, Martin","first_name":"Martin"}],"publication_status":"published","publisher":"IST Austria","alternative_title":["IST Austria Technical Report"],"date_published":"2015-12-30T00:00:00Z","type":"technical_report","status":"public","department":[{"_id":"KrCh"}],"page":"25","has_accepted_license":"1","oa":1,"date_updated":"2020-07-14T23:05:07Z","pubrep_id":"399","year":"2015","title":"Reconstructing robust phylogenies of metastatic cancers","date_created":"2018-12-12T11:39:22Z","citation":{"short":"J. Reiter, A. Makohon-Moore, J. Gerold, I. Bozic, K. Chatterjee, C. Iacobuzio-Donahue, B. Vogelstein, M. Nowak, Reconstructing Robust Phylogenies of Metastatic Cancers, IST Austria, 2015.","ieee":"J. Reiter <i>et al.</i>, <i>Reconstructing robust phylogenies of metastatic cancers</i>. IST Austria, 2015.","ama":"Reiter J, Makohon-Moore A, Gerold J, et al. <i>Reconstructing Robust Phylogenies of Metastatic Cancers</i>. IST Austria; 2015. doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-399-v1-1\">10.15479/AT:IST-2015-399-v1-1</a>","mla":"Reiter, Johannes, et al. <i>Reconstructing Robust Phylogenies of Metastatic Cancers</i>. IST Austria, 2015, doi:<a href=\"https://doi.org/10.15479/AT:IST-2015-399-v1-1\">10.15479/AT:IST-2015-399-v1-1</a>.","ista":"Reiter J, Makohon-Moore A, Gerold J, Bozic I, Chatterjee K, Iacobuzio-Donahue C, Vogelstein B, Nowak M. 2015. Reconstructing robust phylogenies of metastatic cancers, IST Austria, 25p.","chicago":"Reiter, Johannes, Alvin Makohon-Moore, Jeffrey Gerold, Ivana Bozic, Krishnendu Chatterjee, Christine Iacobuzio-Donahue, Bert Vogelstein, and Martin Nowak. <i>Reconstructing Robust Phylogenies of Metastatic Cancers</i>. IST Austria, 2015. <a href=\"https://doi.org/10.15479/AT:IST-2015-399-v1-1\">https://doi.org/10.15479/AT:IST-2015-399-v1-1</a>.","apa":"Reiter, J., Makohon-Moore, A., Gerold, J., Bozic, I., Chatterjee, K., Iacobuzio-Donahue, C., … Nowak, M. (2015). <i>Reconstructing robust phylogenies of metastatic cancers</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2015-399-v1-1\">https://doi.org/10.15479/AT:IST-2015-399-v1-1</a>"},"doi":"10.15479/AT:IST-2015-399-v1-1","file_date_updated":"2020-07-14T12:46:58Z","_id":"5444","language":[{"iso":"eng"}]},{"related_material":{"record":[{"id":"1603","relation":"popular_science","status":"public"}]},"ec_funded":1,"keyword":["Markov Decision Process","Decision Tree","Probabilistic Verification","Counterexample Explanation"],"citation":{"ista":"Fellner A. 2015. Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes, Institute of Science and Technology Austria, <a href=\"https://doi.org/10.15479/AT:ISTA:28\">10.15479/AT:ISTA:28</a>.","mla":"Fellner, Andreas. <i>Experimental Part of CAV 2015 Publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes</i>. Institute of Science and Technology Austria, 2015, doi:<a href=\"https://doi.org/10.15479/AT:ISTA:28\">10.15479/AT:ISTA:28</a>.","chicago":"Fellner, Andreas. “Experimental Part of CAV 2015 Publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.” Institute of Science and Technology Austria, 2015. <a href=\"https://doi.org/10.15479/AT:ISTA:28\">https://doi.org/10.15479/AT:ISTA:28</a>.","short":"A. Fellner, (2015).","ieee":"A. Fellner, “Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.” Institute of Science and Technology Austria, 2015.","ama":"Fellner A. Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. 2015. doi:<a href=\"https://doi.org/10.15479/AT:ISTA:28\">10.15479/AT:ISTA:28</a>","apa":"Fellner, A. (2015). Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT:ISTA:28\">https://doi.org/10.15479/AT:ISTA:28</a>"},"date_created":"2018-12-12T12:31:29Z","publist_id":"5564","year":"2015","doi":"10.15479/AT:ISTA:28","_id":"5549","file_date_updated":"2020-07-14T12:47:00Z","abstract":[{"lang":"eng","text":"This repository contains the experimental part of the CAV 2015 publication Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.\r\nWe extended the probabilistic model checker PRISM to represent strategies of Markov Decision Processes as Decision Trees.\r\nThe archive contains a java executable version of the extended tool (prism_dectree.jar) together with a few examples of the PRISM benchmark library.\r\nTo execute the program, please have a look at the README.txt, which provides instructions and further information on the archive.\r\nThe archive contains scripts that (if run often enough) reproduces the data presented in the publication."}],"contributor":[{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky","first_name":"Jan"}],"tmp":{"image":"/images/cc_0.png","legal_code_url":"https://creativecommons.org/publicdomain/zero/1.0/legalcode","name":"Creative Commons Public Domain Dedication (CC0 1.0)","short":"CC0 (1.0)"},"ddc":["004"],"department":[{"_id":"KrCh"},{"_id":"ToHe"}],"date_published":"2015-08-13T00:00:00Z","publisher":"Institute of Science and Technology Austria","project":[{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"}],"has_accepted_license":"1","title":"Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes","article_processing_charge":"No","date_updated":"2024-02-21T13:52:07Z","oa":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"access_level":"open_access","content_type":"application/zip","file_size":49557109,"relation":"main_file","creator":"system","date_created":"2018-12-12T13:02:31Z","date_updated":"2020-07-14T12:47:00Z","file_id":"5597","file_name":"IST-2015-28-v1+2_Fellner_DataRep.zip","checksum":"b8bcb43c0893023cda66c1b69c16ac62"}],"datarep_id":"28","oa_version":"Published Version","day":"13","month":"08","author":[{"full_name":"Fellner, Andreas","first_name":"Andreas","id":"42BABFB4-F248-11E8-B48F-1D18A9856A87","last_name":"Fellner"}],"type":"research_data","status":"public"},{"type":"conference","status":"public","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389"}],"arxiv":1,"conference":{"name":"SODA: Symposium on Discrete Algorithms","start_date":"2015-01-04","location":"San Diego, CA, United States","end_date":"2015-01-06"},"publication_identifier":{"isbn":["978-161197374-7"]},"month":"01","oa_version":"Preprint","day":"01","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"publication":"Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms","date_updated":"2022-02-25T12:33:32Z","issue":"1","article_processing_charge":"No","title":"The value 1 problem under finite-memory strategies for concurrent mean-payoff games","scopus_import":"1","intvolume":"      2015","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"name":"Game Theory","call_identifier":"FWF","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"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"}],"publisher":"SIAM","date_published":"2015-01-01T00:00:00Z","page":"1018-1029","department":[{"_id":"KrCh"}],"volume":2015,"quality_controlled":"1","publication_status":"published","external_id":{"arxiv":["1409.6690"]},"abstract":[{"lang":"eng","text":"We consider concurrent mean-payoff games, a very well-studied class of two-player (player 1 vs player 2) zero-sum games on finite-state graphs where every transition is assigned a reward between 0 and 1, and the payoff function is the long-run average of the rewards. The value is the maximal expected payoff that player 1 can guarantee against all strategies of player 2. We consider the computation of the set of states with value 1 under finite-memory strategies for player 1, and our main results for the problem are as follows: (1) we present a polynomial-time algorithm; (2) we show that whenever there is a finite-memory strategy, there is a stationary strategy that does not need memory at all; and (3) we present an optimal bound (which is double exponential) on the patience of stationary strategies (where patience of a distribution is the inverse of the smallest positive probability and represents a complexity measure of a stationary strategy)."}],"_id":"10796","doi":"10.1137/1.9781611973730.69","acknowledgement":"The research was partly supported by FWF Grant No P 23499-N23, FWF NFN Grant\r\nNo S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.","year":"2015","citation":{"mla":"Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. “The Value 1 Problem under Finite-Memory Strategies for Concurrent Mean-Payoff Games.” <i>Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms</i>, vol. 2015, no. 1, SIAM, 2015, pp. 1018–29, doi:<a href=\"https://doi.org/10.1137/1.9781611973730.69\">10.1137/1.9781611973730.69</a>.","chicago":"Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. “The Value 1 Problem under Finite-Memory Strategies for Concurrent Mean-Payoff Games.” In <i>Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms</i>, 2015:1018–29. SIAM, 2015. <a href=\"https://doi.org/10.1137/1.9781611973730.69\">https://doi.org/10.1137/1.9781611973730.69</a>.","ista":"Chatterjee K, Ibsen-Jensen R. 2015. The value 1 problem under finite-memory strategies for concurrent mean-payoff games. Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms. SODA: Symposium on Discrete Algorithms vol. 2015, 1018–1029.","ieee":"K. Chatterjee and R. Ibsen-Jensen, “The value 1 problem under finite-memory strategies for concurrent mean-payoff games,” in <i>Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms</i>, San Diego, CA, United States, 2015, vol. 2015, no. 1, pp. 1018–1029.","ama":"Chatterjee K, Ibsen-Jensen R. The value 1 problem under finite-memory strategies for concurrent mean-payoff games. In: <i>Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms</i>. Vol 2015. SIAM; 2015:1018-1029. doi:<a href=\"https://doi.org/10.1137/1.9781611973730.69\">10.1137/1.9781611973730.69</a>","short":"K. Chatterjee, R. Ibsen-Jensen, in:, Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms, SIAM, 2015, pp. 1018–1029.","apa":"Chatterjee, K., &#38; Ibsen-Jensen, R. (2015). The value 1 problem under finite-memory strategies for concurrent mean-payoff games. In <i>Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms</i> (Vol. 2015, pp. 1018–1029). San Diego, CA, United States: SIAM. <a href=\"https://doi.org/10.1137/1.9781611973730.69\">https://doi.org/10.1137/1.9781611973730.69</a>"},"date_created":"2022-02-25T12:18:43Z","ec_funded":1},{"type":"journal_article","status":"public","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1302.4248"}],"oa_version":"Preprint","day":"24","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"03","author":[{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"full_name":"Doyen, Laurent","first_name":"Laurent","last_name":"Doyen"},{"last_name":"Randour","first_name":"Mickael","full_name":"Randour, Mickael"},{"last_name":"Raskin","first_name":"Jean","full_name":"Raskin, Jean"}],"publication":"Information and Computation","language":[{"iso":"eng"}],"scopus_import":1,"intvolume":"       242","title":"Looking at mean-payoff and total-payoff through windows","oa":1,"date_updated":"2023-02-23T10:36:02Z","issue":"6","department":[{"_id":"KrCh"}],"page":"25 - 52","volume":242,"quality_controlled":"1","publisher":"Elsevier","date_published":"2015-03-24T00:00:00Z","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"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"abstract":[{"lang":"eng","text":"We consider two-player games played on weighted directed graphs with mean-payoff and total-payoff objectives, two classical quantitative objectives. While for single-dimensional games the complexity and memory bounds for both objectives coincide, we show that in contrast to multi-dimensional mean-payoff games that are known to be coNP-complete, multi-dimensional total-payoff games are undecidable. We introduce conservative approximations of these objectives, where the payoff is considered over a local finite window sliding along a play, instead of the whole play. For single dimension, we show that (i) if the window size is polynomial, deciding the winner takes polynomial time, and (ii) the existence of a bounded window can be decided in NP ∩ coNP, and is at least as hard as solving mean-payoff games. For multiple dimensions, we show that (i) the problem with fixed window size is EXPTIME-complete, and (ii) there is no primitive-recursive algorithm to decide the existence of a bounded window."}],"publication_status":"published","doi":"10.1016/j.ic.2015.03.010","_id":"523","ec_funded":1,"related_material":{"record":[{"status":"public","id":"2279","relation":"earlier_version"}]},"date_created":"2018-12-11T11:46:57Z","citation":{"apa":"Chatterjee, K., Doyen, L., Randour, M., &#38; Raskin, J. (2015). Looking at mean-payoff and total-payoff through windows. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2015.03.010\">https://doi.org/10.1016/j.ic.2015.03.010</a>","chicago":"Chatterjee, Krishnendu, Laurent Doyen, Mickael Randour, and Jean Raskin. “Looking at Mean-Payoff and Total-Payoff through Windows.” <i>Information and Computation</i>. Elsevier, 2015. <a href=\"https://doi.org/10.1016/j.ic.2015.03.010\">https://doi.org/10.1016/j.ic.2015.03.010</a>.","ista":"Chatterjee K, Doyen L, Randour M, Raskin J. 2015. Looking at mean-payoff and total-payoff through windows. Information and Computation. 242(6), 25–52.","mla":"Chatterjee, Krishnendu, et al. “Looking at Mean-Payoff and Total-Payoff through Windows.” <i>Information and Computation</i>, vol. 242, no. 6, Elsevier, 2015, pp. 25–52, doi:<a href=\"https://doi.org/10.1016/j.ic.2015.03.010\">10.1016/j.ic.2015.03.010</a>.","short":"K. Chatterjee, L. Doyen, M. Randour, J. Raskin, Information and Computation 242 (2015) 25–52.","ieee":"K. Chatterjee, L. Doyen, M. Randour, and J. Raskin, “Looking at mean-payoff and total-payoff through windows,” <i>Information and Computation</i>, vol. 242, no. 6. Elsevier, pp. 25–52, 2015.","ama":"Chatterjee K, Doyen L, Randour M, Raskin J. Looking at mean-payoff and total-payoff through windows. <i>Information and Computation</i>. 2015;242(6):25-52. doi:<a href=\"https://doi.org/10.1016/j.ic.2015.03.010\">10.1016/j.ic.2015.03.010</a>"},"publist_id":"7296","year":"2015"},{"month":"10","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"11","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1409.5306"}],"oa_version":"Preprint","arxiv":1,"author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus"}],"status":"public","type":"journal_article","intvolume":"       242","scopus_import":1,"issue":"6","oa":1,"date_updated":"2023-02-23T12:24:45Z","title":"Qualitative analysis of concurrent mean payoff games","publication":"Information and Computation","language":[{"iso":"eng"}],"abstract":[{"lang":"eng","text":"We consider concurrent games played by two players on a finite-state graph, where in every round the players simultaneously choose a move, and the current state along with the joint moves determine the successor state. We study the most fundamental objective for concurrent games, namely, mean-payoff or limit-average objective, where a reward is associated to each transition, and the goal of player 1 is to maximize the long-run average of the rewards, and the objective of player 2 is strictly the opposite (i.e., the games are zero-sum). The path constraint for player 1 could be qualitative, i.e., the mean-payoff is the maximal reward, or arbitrarily close to it; or quantitative, i.e., a given threshold between the minimal and maximal reward. We consider the computation of the almost-sure (resp. positive) winning sets, where player 1 can ensure that the path constraint is satisfied with probability 1 (resp. positive probability). Almost-sure winning with qualitative constraint exactly corresponds to the question of whether there exists a strategy to ensure that the payoff is the maximal reward of the game. Our main results for qualitative path constraints are as follows: (1) we establish qualitative determinacy results that show that for every state either player 1 has a strategy to ensure almost-sure (resp. positive) winning against all player-2 strategies, or player 2 has a spoiling strategy to falsify almost-sure (resp. positive) winning against all player-1 strategies; (2) we present optimal strategy complexity results that precisely characterize the classes of strategies required for almost-sure and positive winning for both players; and (3) we present quadratic time algorithms to compute the almost-sure and the positive winning sets, matching the best known bound of the algorithms for much simpler problems (such as reachability objectives). For quantitative constraints we show that a polynomial time solution for the almost-sure or the positive winning set would imply a solution to a long-standing open problem (of solving the value problem of turn-based deterministic mean-payoff games) that is not known to be solvable in polynomial time."}],"external_id":{"arxiv":["1409.5306"]},"publication_status":"published","date_published":"2015-10-11T00:00:00Z","publisher":"Elsevier","volume":242,"quality_controlled":"1","page":"2 - 24","department":[{"_id":"KrCh"}],"related_material":{"record":[{"status":"public","id":"5403","relation":"earlier_version"}]},"year":"2015","date_created":"2018-12-11T11:46:57Z","publist_id":"7295","citation":{"apa":"Chatterjee, K., &#38; Ibsen-Jensen, R. (2015). Qualitative analysis of concurrent mean payoff games. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2015.03.009\">https://doi.org/10.1016/j.ic.2015.03.009</a>","chicago":"Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. “Qualitative Analysis of Concurrent Mean Payoff Games.” <i>Information and Computation</i>. Elsevier, 2015. <a href=\"https://doi.org/10.1016/j.ic.2015.03.009\">https://doi.org/10.1016/j.ic.2015.03.009</a>.","ista":"Chatterjee K, Ibsen-Jensen R. 2015. Qualitative analysis of concurrent mean payoff games. Information and Computation. 242(6), 2–24.","mla":"Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. “Qualitative Analysis of Concurrent Mean Payoff Games.” <i>Information and Computation</i>, vol. 242, no. 6, Elsevier, 2015, pp. 2–24, doi:<a href=\"https://doi.org/10.1016/j.ic.2015.03.009\">10.1016/j.ic.2015.03.009</a>.","ama":"Chatterjee K, Ibsen-Jensen R. Qualitative analysis of concurrent mean payoff games. <i>Information and Computation</i>. 2015;242(6):2-24. doi:<a href=\"https://doi.org/10.1016/j.ic.2015.03.009\">10.1016/j.ic.2015.03.009</a>","ieee":"K. Chatterjee and R. Ibsen-Jensen, “Qualitative analysis of concurrent mean payoff games,” <i>Information and Computation</i>, vol. 242, no. 6. Elsevier, pp. 2–24, 2015.","short":"K. Chatterjee, R. Ibsen-Jensen, Information and Computation 242 (2015) 2–24."},"doi":"10.1016/j.ic.2015.03.009","_id":"524"},{"date_published":"2014-12-04T00:00:00Z","publisher":"Elsevier","volume":560,"quality_controlled":"1","page":"348 - 363","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"project":[{"name":"Quantitative Reactive Modeling","call_identifier":"FP7","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","call_identifier":"FWF"},{"call_identifier":"FWF","name":"Game Theory","grant_number":"S11407","_id":"25863FF4-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"},{"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"}],"abstract":[{"text":"The classical (boolean) notion of refinement for behavioral interfaces of system components is the alternating refinement preorder. In this paper, we define a distance for interfaces, called interface simulation distance. It makes the alternating refinement preorder quantitative by, intuitively, tolerating errors (while counting them) in the alternating simulation game. We show that the interface simulation distance satisfies the triangle inequality, that the distance between two interfaces does not increase under parallel composition with a third interface, that the distance between two interfaces can be bounded from above and below by distances between abstractions of the two interfaces, and how to synthesize an interface from incompatible requirements. We illustrate the framework, and the properties of the distances under composition of interfaces, with two case studies.","lang":"eng"}],"publication_status":"published","doi":"10.1016/j.tcs.2014.08.019","_id":"1733","related_material":{"record":[{"id":"2916","relation":"earlier_version","status":"public"}]},"ec_funded":1,"year":"2014","date_created":"2018-12-11T11:53:43Z","publist_id":"5392","citation":{"ieee":"P. Cerny, M. Chmelik, T. A. Henzinger, and A. Radhakrishna, “Interface simulation distances,” <i>Theoretical Computer Science</i>, vol. 560, no. 3. Elsevier, pp. 348–363, 2014.","ama":"Cerny P, Chmelik M, Henzinger TA, Radhakrishna A. Interface simulation distances. <i>Theoretical Computer Science</i>. 2014;560(3):348-363. doi:<a href=\"https://doi.org/10.1016/j.tcs.2014.08.019\">10.1016/j.tcs.2014.08.019</a>","short":"P. Cerny, M. Chmelik, T.A. Henzinger, A. Radhakrishna, Theoretical Computer Science 560 (2014) 348–363.","mla":"Cerny, Pavol, et al. “Interface Simulation Distances.” <i>Theoretical Computer Science</i>, vol. 560, no. 3, Elsevier, 2014, pp. 348–63, doi:<a href=\"https://doi.org/10.1016/j.tcs.2014.08.019\">10.1016/j.tcs.2014.08.019</a>.","ista":"Cerny P, Chmelik M, Henzinger TA, Radhakrishna A. 2014. Interface simulation distances. Theoretical Computer Science. 560(3), 348–363.","chicago":"Cerny, Pavol, Martin Chmelik, Thomas A Henzinger, and Arjun Radhakrishna. “Interface Simulation Distances.” <i>Theoretical Computer Science</i>. Elsevier, 2014. <a href=\"https://doi.org/10.1016/j.tcs.2014.08.019\">https://doi.org/10.1016/j.tcs.2014.08.019</a>.","apa":"Cerny, P., Chmelik, M., Henzinger, T. A., &#38; Radhakrishna, A. (2014). Interface simulation distances. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2014.08.019\">https://doi.org/10.1016/j.tcs.2014.08.019</a>"},"type":"journal_article","status":"public","month":"12","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","day":"04","main_file_link":[{"url":"http://arxiv.org/abs/1210.2450","open_access":"1"}],"oa_version":"Submitted Version","author":[{"full_name":"Cerny, Pavol","first_name":"Pavol","last_name":"Cerny"},{"last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87","full_name":"Chmelik, Martin","first_name":"Martin"},{"orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"id":"3B51CAC4-F248-11E8-B48F-1D18A9856A87","last_name":"Radhakrishna","full_name":"Radhakrishna, Arjun","first_name":"Arjun"}],"publication":"Theoretical Computer Science","language":[{"iso":"eng"}],"intvolume":"       560","scopus_import":1,"issue":"3","date_updated":"2023-02-23T11:04:00Z","oa":1,"title":"Interface simulation distances"},{"_id":"1853","language":[{"iso":"eng"}],"doi":"10.1109/IOT.2014.7030120","date_created":"2018-12-11T11:54:22Z","title":"Game theoretic secure localization in wireless sensor networks","publist_id":"5247","citation":{"short":"S. Jha, S. Tripakis, S. Seshia, K. Chatterjee, in:, IEEE, 2014, pp. 85–90.","ieee":"S. Jha, S. Tripakis, S. Seshia, and K. Chatterjee, “Game theoretic secure localization in wireless sensor networks,” presented at the IOT: Internet of Things, Cambridge, USA, 2014, pp. 85–90.","ama":"Jha S, Tripakis S, Seshia S, Chatterjee K. Game theoretic secure localization in wireless sensor networks. In: IEEE; 2014:85-90. doi:<a href=\"https://doi.org/10.1109/IOT.2014.7030120\">10.1109/IOT.2014.7030120</a>","chicago":"Jha, Susmit, Stavros Tripakis, Sanjit Seshia, and Krishnendu Chatterjee. “Game Theoretic Secure Localization in Wireless Sensor Networks,” 85–90. IEEE, 2014. <a href=\"https://doi.org/10.1109/IOT.2014.7030120\">https://doi.org/10.1109/IOT.2014.7030120</a>.","mla":"Jha, Susmit, et al. <i>Game Theoretic Secure Localization in Wireless Sensor Networks</i>. IEEE, 2014, pp. 85–90, doi:<a href=\"https://doi.org/10.1109/IOT.2014.7030120\">10.1109/IOT.2014.7030120</a>.","ista":"Jha S, Tripakis S, Seshia S, Chatterjee K. 2014. Game theoretic secure localization in wireless sensor networks. IOT: Internet of Things, 85–90.","apa":"Jha, S., Tripakis, S., Seshia, S., &#38; Chatterjee, K. (2014). Game theoretic secure localization in wireless sensor networks (pp. 85–90). Presented at the IOT: Internet of Things, Cambridge, USA: IEEE. <a href=\"https://doi.org/10.1109/IOT.2014.7030120\">https://doi.org/10.1109/IOT.2014.7030120</a>"},"year":"2014","date_updated":"2021-01-12T06:53:38Z","quality_controlled":"1","department":[{"_id":"KrCh"}],"page":"85 - 90","type":"conference","status":"public","date_published":"2014-02-03T00:00:00Z","publisher":"IEEE","publication_status":"published","author":[{"last_name":"Jha","first_name":"Susmit","full_name":"Jha, Susmit"},{"last_name":"Tripakis","first_name":"Stavros","full_name":"Tripakis, Stavros"},{"full_name":"Seshia, Sanjit","first_name":"Sanjit","last_name":"Seshia"},{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"}],"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","abstract":[{"text":"Wireless sensor networks (WSNs) composed of low-power, low-cost sensor nodes are expected to form the backbone of future intelligent networks for a broad range of civil, industrial and military applications. These sensor nodes are often deployed through random spreading, and function in dynamic environments. Many applications of WSNs such as pollution tracking, forest fire detection, and military surveillance require knowledge of the location of constituent nodes. But the use of technologies such as GPS on all nodes is prohibitive due to power and cost constraints. So, the sensor nodes need to autonomously determine their locations. Most localization techniques use anchor nodes with known locations to determine the position of remaining nodes. Localization techniques have two conflicting requirements. On one hand, an ideal localization technique should be computationally simple and on the other hand, it must be resistant to attacks that compromise anchor nodes. In this paper, we propose a computationally light-weight game theoretic secure localization technique and demonstrate its effectiveness in comparison to existing techniques.","lang":"eng"}],"day":"03","oa_version":"None","month":"02","conference":{"start_date":"2014-10-06","name":"IOT: Internet of Things","end_date":"2014-10-08","location":"Cambridge, USA"}},{"author":[{"full_name":"Landau, Dan","first_name":"Dan","last_name":"Landau"},{"last_name":"Stewart","full_name":"Stewart, Chip","first_name":"Chip"},{"first_name":"Johannes","full_name":"Reiter, Johannes","last_name":"Reiter","id":"4A918E98-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0170-7353"},{"first_name":"Michael","full_name":"Lawrence, Michael","last_name":"Lawrence"},{"full_name":"Sougnez, Carrie","first_name":"Carrie","last_name":"Sougnez"},{"last_name":"Brown","first_name":"Jennifer","full_name":"Brown, Jennifer"},{"last_name":"Lopez Guillermo","full_name":"Lopez Guillermo, Armando","first_name":"Armando"},{"full_name":"Gabriel, Stacey","first_name":"Stacey","last_name":"Gabriel"},{"first_name":"Eric","full_name":"Lander, Eric","last_name":"Lander"},{"full_name":"Neuberg, Donna","first_name":"Donna","last_name":"Neuberg"},{"last_name":"López Otín","full_name":"López Otín, Carlos","first_name":"Carlos"},{"first_name":"Elias","full_name":"Campo, Elias","last_name":"Campo"},{"full_name":"Getz, Gad","first_name":"Gad","last_name":"Getz"},{"first_name":"Catherine","full_name":"Wu, Catherine","last_name":"Wu"}],"publication_status":"published","month":"12","day":"04","main_file_link":[{"url":"http://www.bloodjournal.org/content/124/21/1952?sso-checked=true"}],"oa_version":"None","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","abstract":[{"lang":"eng","text":"Unbiased high-throughput massively parallel sequencing methods have transformed the process of discovery of novel putative driver gene mutations in cancer. In chronic lymphocytic leukemia (CLL), these methods have yielded several unexpected findings, including the driver genes SF3B1, NOTCH1 and POT1. Recent analysis, utilizing down-sampling of existing datasets, has shown that the discovery process of putative drivers is far from complete across cancer. In CLL, while driver gene mutations affecting >10% of patients were efficiently discovered with previously published CLL cohorts of up to 160 samples subjected to whole exome sequencing (WES), this sample size has only 0.78 power to detect drivers affecting 5% of patients, and only 0.12 power for drivers affecting 2% of patients. These calculations emphasize the need to apply unbiased WES to larger patient cohorts."}],"publisher":"American Society of Hematology","type":"journal_article","date_published":"2014-12-04T00:00:00Z","status":"public","page":"1952 - 1952","department":[{"_id":"KrCh"}],"volume":124,"date_updated":"2021-01-12T06:53:50Z","issue":"21","year":"2014","citation":{"apa":"Landau, D., Stewart, C., Reiter, J., Lawrence, M., Sougnez, C., Brown, J., … Wu, C. (2014). Novel putative driver gene mutations in chronic lymphocytic leukemia (CLL): results from a combined analysis of whole exome sequencing of 262 primary CLL aamples. <i>Blood</i>. American Society of Hematology.","ista":"Landau D, Stewart C, Reiter J, Lawrence M, Sougnez C, Brown J, Lopez Guillermo A, Gabriel S, Lander E, Neuberg D, López Otín C, Campo E, Getz G, Wu C. 2014. Novel putative driver gene mutations in chronic lymphocytic leukemia (CLL): results from a combined analysis of whole exome sequencing of 262 primary CLL aamples. Blood. 124(21), 1952–1952.","chicago":"Landau, Dan, Chip Stewart, Johannes Reiter, Michael Lawrence, Carrie Sougnez, Jennifer Brown, Armando Lopez Guillermo, et al. “Novel Putative Driver Gene Mutations in Chronic Lymphocytic Leukemia (CLL): Results from a Combined Analysis of Whole Exome Sequencing of 262 Primary CLL Aamples.” <i>Blood</i>. American Society of Hematology, 2014.","mla":"Landau, Dan, et al. “Novel Putative Driver Gene Mutations in Chronic Lymphocytic Leukemia (CLL): Results from a Combined Analysis of Whole Exome Sequencing of 262 Primary CLL Aamples.” <i>Blood</i>, vol. 124, no. 21, American Society of Hematology, 2014, pp. 1952–1952.","short":"D. Landau, C. Stewart, J. Reiter, M. Lawrence, C. Sougnez, J. Brown, A. Lopez Guillermo, S. Gabriel, E. Lander, D. Neuberg, C. López Otín, E. Campo, G. Getz, C. Wu, Blood 124 (2014) 1952–1952.","ieee":"D. Landau <i>et al.</i>, “Novel putative driver gene mutations in chronic lymphocytic leukemia (CLL): results from a combined analysis of whole exome sequencing of 262 primary CLL aamples,” <i>Blood</i>, vol. 124, no. 21. American Society of Hematology, pp. 1952–1952, 2014.","ama":"Landau D, Stewart C, Reiter J, et al. Novel putative driver gene mutations in chronic lymphocytic leukemia (CLL): results from a combined analysis of whole exome sequencing of 262 primary CLL aamples. <i>Blood</i>. 2014;124(21):1952-1952."},"date_created":"2018-12-11T11:54:32Z","publist_id":"5211","title":"Novel putative driver gene mutations in chronic lymphocytic leukemia (CLL): results from a combined analysis of whole exome sequencing of 262 primary CLL aamples","intvolume":"       124","_id":"1884","language":[{"iso":"eng"}],"publication":"Blood"},{"scopus_import":1,"intvolume":"      8634","issue":"PART 1","pubrep_id":"141","date_updated":"2023-02-23T12:23:43Z","title":"Partial-observation stochastic reachability and parity games","language":[{"iso":"eng"}],"month":"01","conference":{"start_date":"2014-08-25","name":"MFCS: Mathematical Foundations of Computer Science","end_date":"2014-08-29","location":"Budapest, Hungary"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"01","oa_version":"None","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"}],"status":"public","type":"conference","alternative_title":["LNCS"],"related_material":{"record":[{"id":"2211","relation":"later_version","status":"public"},{"status":"public","relation":"earlier_version","id":"5381"}]},"ec_funded":1,"year":"2014","citation":{"mla":"Chatterjee, Krishnendu. <i>Partial-Observation Stochastic Reachability and Parity Games</i>. Vol. 8634, no. PART 1, Springer, 2014, pp. 1–4, doi:<a href=\"https://doi.org/10.1007/978-3-662-44522-8_1\">10.1007/978-3-662-44522-8_1</a>.","chicago":"Chatterjee, Krishnendu. “Partial-Observation Stochastic Reachability and Parity Games,” 8634:1–4. Springer, 2014. <a href=\"https://doi.org/10.1007/978-3-662-44522-8_1\">https://doi.org/10.1007/978-3-662-44522-8_1</a>.","ista":"Chatterjee K. 2014. Partial-observation stochastic reachability and parity games. MFCS: Mathematical Foundations of Computer Science, LNCS, vol. 8634, 1–4.","short":"K. Chatterjee, in:, Springer, 2014, pp. 1–4.","ama":"Chatterjee K. Partial-observation stochastic reachability and parity games. In: Vol 8634. Springer; 2014:1-4. doi:<a href=\"https://doi.org/10.1007/978-3-662-44522-8_1\">10.1007/978-3-662-44522-8_1</a>","ieee":"K. Chatterjee, “Partial-observation stochastic reachability and parity games,” presented at the MFCS: Mathematical Foundations of Computer Science, Budapest, Hungary, 2014, vol. 8634, no. PART 1, pp. 1–4.","apa":"Chatterjee, K. (2014). Partial-observation stochastic reachability and parity games (Vol. 8634, pp. 1–4). Presented at the MFCS: Mathematical Foundations of Computer Science, Budapest, Hungary: Springer. <a href=\"https://doi.org/10.1007/978-3-662-44522-8_1\">https://doi.org/10.1007/978-3-662-44522-8_1</a>"},"publist_id":"5192","date_created":"2018-12-11T11:54:38Z","doi":"10.1007/978-3-662-44522-8_1","_id":"1903","abstract":[{"text":"We consider two-player zero-sum partial-observation stochastic games on graphs. Based on the information available to the players these games can be classified as follows: (a) general partial-observation (both players have partial view of the game); (b) one-sided partial-observation (one player has partial-observation and the other player has complete-observation); and (c) perfect-observation (both players have complete view of the game). The one-sided partial-observation games subsumes the important special case of one-player partial-observation stochastic games (or partial-observation Markov decision processes (POMDPs)). Based on the randomization available for the strategies, (a) the players may not be allowed to use randomization (pure strategies), or (b) they may choose a probability distribution over actions but the actual random choice is external and not visible to the player (actions invisible), or (c) they may use full randomization. We consider all these classes of games with reachability, and parity objectives that can express all ω-regular objectives. The analysis problems are classified into the qualitative analysis that asks for the existence of a strategy that ensures the objective with probability 1; and the quantitative analysis that asks for the existence of a strategy that ensures the objective with probability at least λ (0,1). In this talk we will cover a wide range of results: for perfect-observation games; for POMDPs; for one-sided partial-observation games; and for general partial-observation games.","lang":"eng"}],"publication_status":"published","date_published":"2014-01-01T00:00:00Z","publisher":"Springer","quality_controlled":"1","volume":8634,"page":"1 - 4","department":[{"_id":"KrCh"}],"project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"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"}]},{"abstract":[{"lang":"eng","text":"We present a general framework for applying machine-learning algorithms to the verification of Markov decision processes (MDPs). The primary goal of these techniques is to improve performance by avoiding an exhaustive exploration of the state space. Our framework focuses on probabilistic reachability, which is a core property for verification, and is illustrated through two distinct instantiations. The first assumes that full knowledge of the MDP is available, and performs a heuristic-driven partial exploration of the model, yielding precise lower and upper bounds on the required probability. The second tackles the case where we may only sample the MDP, and yields probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stopping criteria for the approximation. The latter is the first extension of statistical model checking for unbounded properties inMDPs. In contrast with other related techniques, our approach is not restricted to time-bounded (finite-horizon) or discounted properties, nor does it assume any particular properties of the MDP. We also show how our methods extend to LTL objectives. We present experimental results showing the performance of our framework on several examples."}],"publication_status":"published","page":"98 - 114","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"volume":8837,"quality_controlled":"1","publisher":"Society of Industrial and Applied Mathematics","date_published":"2014-11-01T00:00:00Z","project":[{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425"},{"_id":"26241A12-B435-11E9-9278-68D0E5697425","grant_number":"24696","name":"LIGHT-REGULATED LIGAND TRAPS FOR SPATIO-TEMPORAL INHIBITION OF CELL SIGNALING"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Moderne Concurrency Paradigms","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"ec_funded":1,"date_created":"2018-12-11T11:55:17Z","citation":{"apa":"Brázdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Kretinsky, J., Kwiatkowska, M., … Ujma, M. (2014). Verification of markov decision processes using learning algorithms. In F. Cassez &#38; J.-F. Raskin (Eds.), <i> Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i> (Vol. 8837, pp. 98–114). Sydney, Australia: Society of Industrial and Applied Mathematics. <a href=\"https://doi.org/10.1007/978-3-319-11936-6_8\">https://doi.org/10.1007/978-3-319-11936-6_8</a>","ista":"Brázdil T, Chatterjee K, Chmelik M, Forejt V, Kretinsky J, Kwiatkowska M, Parker D, Ujma M. 2014. Verification of markov decision processes using learning algorithms.  Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). ALENEX: Algorithm Engineering and Experiments, LNCS, vol. 8837, 98–114.","mla":"Brázdil, Tomáš, et al. “Verification of Markov Decision Processes Using Learning Algorithms.” <i> Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, edited by Franck Cassez and Jean-François Raskin, vol. 8837, Society of Industrial and Applied Mathematics, 2014, pp. 98–114, doi:<a href=\"https://doi.org/10.1007/978-3-319-11936-6_8\">10.1007/978-3-319-11936-6_8</a>.","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Vojtěch Forejt, Jan Kretinsky, Marta Kwiatkowska, David Parker, and Mateusz Ujma. “Verification of Markov Decision Processes Using Learning Algorithms.” In <i> Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, edited by Franck Cassez and Jean-François Raskin, 8837:98–114. Society of Industrial and Applied Mathematics, 2014. <a href=\"https://doi.org/10.1007/978-3-319-11936-6_8\">https://doi.org/10.1007/978-3-319-11936-6_8</a>.","short":"T. Brázdil, K. Chatterjee, M. Chmelik, V. Forejt, J. Kretinsky, M. Kwiatkowska, D. Parker, M. Ujma, in:, F. Cassez, J.-F. Raskin (Eds.),  Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Society of Industrial and Applied Mathematics, 2014, pp. 98–114.","ieee":"T. Brázdil <i>et al.</i>, “Verification of markov decision processes using learning algorithms,” in <i> Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, Sydney, Australia, 2014, vol. 8837, pp. 98–114.","ama":"Brázdil T, Chatterjee K, Chmelik M, et al. Verification of markov decision processes using learning algorithms. In: Cassez F, Raskin J-F, eds. <i> Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>. Vol 8837. Society of Industrial and Applied Mathematics; 2014:98-114. doi:<a href=\"https://doi.org/10.1007/978-3-319-11936-6_8\">10.1007/978-3-319-11936-6_8</a>"},"publist_id":"5046","acknowledgement":"This research was funded in part by the European Research Council (ERC) under grant agreement 246967 (VERIWARE), by the EU FP7 project HIERATIC, by the Czech Science Foundation grant No P202/12/P612, by EPSRC project EP/K038575/1.","year":"2014","doi":"10.1007/978-3-319-11936-6_8","_id":"2027","oa_version":"Submitted Version","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1402.2967"}],"day":"01","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","conference":{"start_date":"2014-11-03","name":"ALENEX: Algorithm Engineering and Experiments","end_date":"2014-11-07","location":"Sydney, Australia"},"month":"11","author":[{"full_name":"Brázdil, Tomáš","first_name":"Tomáš","last_name":"Brázdil"},{"last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"full_name":"Chmelik, Martin","first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik"},{"full_name":"Forejt, Vojtěch","first_name":"Vojtěch","last_name":"Forejt"},{"id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky","orcid":"0000-0002-8122-2881","first_name":"Jan","full_name":"Kretinsky, Jan"},{"last_name":"Kwiatkowska","full_name":"Kwiatkowska, Marta","first_name":"Marta"},{"full_name":"Parker, David","first_name":"David","last_name":"Parker"},{"last_name":"Ujma","first_name":"Mateusz","full_name":"Ujma, Mateusz"}],"alternative_title":["LNCS"],"type":"conference","status":"public","intvolume":"      8837","editor":[{"first_name":"Franck","full_name":"Cassez, Franck","last_name":"Cassez"},{"first_name":"Jean-François","full_name":"Raskin, Jean-François","last_name":"Raskin"}],"title":"Verification of markov decision processes using learning algorithms","oa":1,"date_updated":"2021-01-12T06:54:49Z","publication":" Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","language":[{"iso":"eng"}]},{"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"3356"},{"status":"public","relation":"earlier_version","id":"5385"}]},"article_number":"27","ec_funded":1,"year":"2014","acknowledgement":"The research was supported in part by ERC Starting grant 278410 (QUALITY).","publist_id":"5013","citation":{"apa":"Boker, U., Chatterjee, K., Henzinger, T. A., &#38; Kupferman, O. (2014). Temporal specifications with accumulative values. <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM. <a href=\"https://doi.org/10.1145/2629686\">https://doi.org/10.1145/2629686</a>","short":"U. Boker, K. Chatterjee, T.A. Henzinger, O. Kupferman, ACM Transactions on Computational Logic (TOCL) 15 (2014).","ieee":"U. Boker, K. Chatterjee, T. A. Henzinger, and O. Kupferman, “Temporal specifications with accumulative values,” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 15, no. 4. ACM, 2014.","ama":"Boker U, Chatterjee K, Henzinger TA, Kupferman O. Temporal specifications with accumulative values. <i>ACM Transactions on Computational Logic (TOCL)</i>. 2014;15(4). doi:<a href=\"https://doi.org/10.1145/2629686\">10.1145/2629686</a>","ista":"Boker U, Chatterjee K, Henzinger TA, Kupferman O. 2014. Temporal specifications with accumulative values. ACM Transactions on Computational Logic (TOCL). 15(4), 27.","mla":"Boker, Udi, et al. “Temporal Specifications with Accumulative Values.” <i>ACM Transactions on Computational Logic (TOCL)</i>, vol. 15, no. 4, 27, ACM, 2014, doi:<a href=\"https://doi.org/10.1145/2629686\">10.1145/2629686</a>.","chicago":"Boker, Udi, Krishnendu Chatterjee, Thomas A Henzinger, and Orna Kupferman. “Temporal Specifications with Accumulative Values.” <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM, 2014. <a href=\"https://doi.org/10.1145/2629686\">https://doi.org/10.1145/2629686</a>."},"date_created":"2018-12-11T11:55:21Z","doi":"10.1145/2629686","article_type":"original","_id":"2038","file_date_updated":"2020-07-14T12:45:26Z","ddc":["000","004"],"abstract":[{"text":"Recently, there has been an effort to add quantitative objectives to formal verification and synthesis. We introduce and investigate the extension of temporal logics with quantitative atomic assertions. At the heart of quantitative objectives lies the accumulation of values along a computation. It is often the accumulated sum, as with energy objectives, or the accumulated average, as with mean-payoff objectives. We investigate the extension of temporal logics with the prefix-accumulation assertions Sum(v) ≥ c and Avg(v) ≥ c, where v is a numeric (or Boolean) variable of the system, c is a constant rational number, and Sum(v) and Avg(v) denote the accumulated sum and average of the values of v from the beginning of the computation up to the current point in time. We also allow the path-accumulation assertions LimInfAvg(v) ≥ c and LimSupAvg(v) ≥ c, referring to the average value along an entire infinite computation. We study the border of decidability for such quantitative extensions of various temporal logics. In particular, we show that extending the fragment of CTL that has only the EX, EF, AX, and AG temporal modalities with both prefix-accumulation assertions, or extending LTL with both path-accumulation assertions, results in temporal logics whose model-checking problem is decidable. Moreover, the prefix-accumulation assertions may be generalized with &quot;controlled accumulation,&quot; allowing, for example, to specify constraints on the average waiting time between a request and a grant. On the negative side, we show that this branching-time logic is, in a sense, the maximal logic with one or both of the prefix-accumulation assertions that permits a decidable model-checking procedure. Extending a temporal logic that has the EG or EU modalities, such as CTL or LTL, makes the problem undecidable.","lang":"eng"}],"publication_status":"published","date_published":"2014-09-16T00:00:00Z","publisher":"ACM","quality_controlled":"1","volume":15,"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms","call_identifier":"FWF"},{"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"},{"call_identifier":"FP7","name":"Quantitative Reactive Modeling","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"has_accepted_license":"1","scopus_import":1,"intvolume":"        15","issue":"4","article_processing_charge":"No","oa":1,"date_updated":"2023-02-23T12:23:54Z","pubrep_id":"192","title":"Temporal specifications with accumulative values","publication":"ACM Transactions on Computational Logic (TOCL)","language":[{"iso":"eng"}],"month":"09","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"file_size":346184,"relation":"main_file","content_type":"application/pdf","access_level":"open_access","creator":"system","date_updated":"2020-07-14T12:45:26Z","date_created":"2018-12-12T10:10:59Z","file_id":"4851","checksum":"354c41d37500b56320afce94cf9a99c2","file_name":"IST-2014-192-v1+1_AccumulativeValues.pdf"}],"day":"16","oa_version":"Submitted Version","author":[{"full_name":"Boker, Udi","first_name":"Udi","id":"31E297B6-F248-11E8-B48F-1D18A9856A87","last_name":"Boker"},{"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":"Kupferman, Orna","first_name":"Orna","last_name":"Kupferman"}],"status":"public","type":"journal_article"},{"status":"public","type":"journal_article","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"first_name":"Andreas","full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Ben","full_name":"Adlam, Ben","last_name":"Adlam"},{"last_name":"Nowak","full_name":"Nowak, Martin","first_name":"Martin"}],"month":"09","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","file":[{"creator":"system","access_level":"open_access","content_type":"application/pdf","file_size":1399093,"relation":"main_file","checksum":"712d4c5787ddf97809cfc962507f0738","file_id":"4890","file_name":"IST-2016-440-v1+1_journal.pcbi.1003818.pdf","date_updated":"2020-07-14T12:45:26Z","date_created":"2018-12-12T10:11:35Z"}],"day":"11","oa_version":"Published Version","language":[{"iso":"eng"}],"publication":"PLoS Computational Biology","issue":"9","pubrep_id":"440","oa":1,"date_updated":"2023-02-23T14:06:36Z","title":"The time scale of evolutionary innovation","scopus_import":1,"has_accepted_license":"1","intvolume":"        10","project":[{"_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","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"date_published":"2014-09-11T00:00:00Z","publisher":"Public Library of Science","quality_controlled":"1","volume":10,"department":[{"_id":"KrCh"}],"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":["510"],"abstract":[{"text":"A fundamental question in biology is the following: what is the time scale that is needed for evolutionary innovations? There are many results that characterize single steps in terms of the fixation time of new mutants arising in populations of certain size and structure. But here we ask a different question, which is concerned with the much longer time scale of evolutionary trajectories: how long does it take for a population exploring a fitness landscape to find target sequences that encode new biological functions? Our key variable is the length, (Formula presented.) of the genetic sequence that undergoes adaptation. In computer science there is a crucial distinction between problems that require algorithms which take polynomial or exponential time. The latter are considered to be intractable. Here we develop a theoretical approach that allows us to estimate the time of evolution as function of (Formula presented.) We show that adaptation on many fitness landscapes takes time that is exponential in (Formula presented.) even if there are broad selection gradients and many targets uniformly distributed in sequence space. These negative results lead us to search for specific mechanisms that allow evolution to work on polynomial time scales. We study a regeneration process and show that it enables evolution to work in polynomial time.","lang":"eng"}],"_id":"2039","file_date_updated":"2020-07-14T12:45:26Z","doi":"10.1371/journal.pcbi.1003818","year":"2014","publist_id":"5012","citation":{"apa":"Chatterjee, K., Pavlogiannis, A., Adlam, B., &#38; Nowak, M. (2014). The time scale of evolutionary innovation. <i>PLoS Computational Biology</i>. Public Library of Science. <a href=\"https://doi.org/10.1371/journal.pcbi.1003818\">https://doi.org/10.1371/journal.pcbi.1003818</a>","ieee":"K. Chatterjee, A. Pavlogiannis, B. Adlam, and M. Nowak, “The time scale of evolutionary innovation,” <i>PLoS Computational Biology</i>, vol. 10, no. 9. Public Library of Science, 2014.","ama":"Chatterjee K, Pavlogiannis A, Adlam B, Nowak M. The time scale of evolutionary innovation. <i>PLoS Computational Biology</i>. 2014;10(9). doi:<a href=\"https://doi.org/10.1371/journal.pcbi.1003818\">10.1371/journal.pcbi.1003818</a>","short":"K. Chatterjee, A. Pavlogiannis, B. Adlam, M. Nowak, PLoS Computational Biology 10 (2014).","mla":"Chatterjee, Krishnendu, et al. “The Time Scale of Evolutionary Innovation.” <i>PLoS Computational Biology</i>, vol. 10, no. 9, 7p, Public Library of Science, 2014, doi:<a href=\"https://doi.org/10.1371/journal.pcbi.1003818\">10.1371/journal.pcbi.1003818</a>.","ista":"Chatterjee K, Pavlogiannis A, Adlam B, Nowak M. 2014. The time scale of evolutionary innovation. PLoS Computational Biology. 10(9), 7p.","chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, Ben Adlam, and Martin Nowak. “The Time Scale of Evolutionary Innovation.” <i>PLoS Computational Biology</i>. Public Library of Science, 2014. <a href=\"https://doi.org/10.1371/journal.pcbi.1003818\">https://doi.org/10.1371/journal.pcbi.1003818</a>."},"date_created":"2018-12-11T11:55:22Z","related_material":{"record":[{"status":"public","id":"9739","relation":"research_data"}]},"article_number":"7p","ec_funded":1},{"publication":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","doi":"10.1007/978-3-662-44584-6_9","_id":"2052","language":[{"iso":"eng"}],"editor":[{"full_name":"Baldan, Paolo","first_name":"Paolo","last_name":"Baldan"},{"last_name":"Gorla","full_name":"Gorla, Daniele","first_name":"Daniele"}],"intvolume":"      8704","year":"2014","date_updated":"2021-01-12T06:54:59Z","acknowledgement":"The second, third, fourth and fifth authors were supported by the Austrian National Research Network S11403-N23 (RiSE) of the Austrian Science Fund (FWF) and by the Vienna Science and Technology Fund (WWTF) through grants PROSEED, ICT12-059, and VRG11-005.","citation":{"apa":"Aminof, B., Kotek, T., Rubin, S., Spegni, F., &#38; Veith, H. (2014). Parameterized model checking of rendezvous systems. In P. Baldan &#38; D. Gorla (Eds.), <i>Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i> (Vol. 8704, pp. 109–124). Rome, Italy: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/978-3-662-44584-6_9\">https://doi.org/10.1007/978-3-662-44584-6_9</a>","short":"B. Aminof, T. Kotek, S. Rubin, F. Spegni, H. Veith, in:, P. Baldan, D. Gorla (Eds.), Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 109–124.","ama":"Aminof B, Kotek T, Rubin S, Spegni F, Veith H. Parameterized model checking of rendezvous systems. In: Baldan P, Gorla D, eds. <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>. Vol 8704. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2014:109-124. doi:<a href=\"https://doi.org/10.1007/978-3-662-44584-6_9\">10.1007/978-3-662-44584-6_9</a>","ieee":"B. Aminof, T. Kotek, S. Rubin, F. Spegni, and H. Veith, “Parameterized model checking of rendezvous systems,” in <i>Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, Rome, Italy, 2014, vol. 8704, pp. 109–124.","chicago":"Aminof, Benjamin, Tomer Kotek, Sacha Rubin, Francesco Spegni, and Helmut Veith. “Parameterized Model Checking of Rendezvous Systems.” In <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, edited by Paolo Baldan and Daniele Gorla, 8704:109–24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. <a href=\"https://doi.org/10.1007/978-3-662-44584-6_9\">https://doi.org/10.1007/978-3-662-44584-6_9</a>.","ista":"Aminof B, Kotek T, Rubin S, Spegni F, Veith H. 2014. Parameterized model checking of rendezvous systems. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). CONCUR: Concurrency Theory, LNCS, vol. 8704, 109–124.","mla":"Aminof, Benjamin, et al. “Parameterized Model Checking of Rendezvous Systems.” <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, edited by Paolo Baldan and Daniele Gorla, vol. 8704, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 109–24, doi:<a href=\"https://doi.org/10.1007/978-3-662-44584-6_9\">10.1007/978-3-662-44584-6_9</a>."},"date_created":"2018-12-11T11:55:26Z","title":"Parameterized model checking of rendezvous systems","publist_id":"4994","date_published":"2014-09-01T00:00:00Z","status":"public","type":"conference","alternative_title":["LNCS"],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","volume":8704,"quality_controlled":"1","department":[{"_id":"KrCh"}],"page":"109 - 124","month":"09","conference":{"end_date":"2014-09-05","location":"Rome, Italy","start_date":"2014-09-02","name":"CONCUR: Concurrency Theory"},"abstract":[{"text":"A standard technique for solving the parameterized model checking problem is to reduce it to the classic model checking problem of finitely many finite-state systems. This work considers some of the theoretical power and limitations of this technique. We focus on concurrent systems in which processes communicate via pairwise rendezvous, as well as the special cases of disjunctive guards and token passing; specifications are expressed in indexed temporal logic without the next operator; and the underlying network topologies are generated by suitable Monadic Second Order Logic formulas and graph operations. First, we settle the exact computational complexity of the parameterized model checking problem for some of our concurrent systems, and establish new decidability results for others. Second, we consider the cases that model checking the parameterized system can be reduced to model checking some fixed number of processes, the number is known as a cutoff. We provide many cases for when such cutoffs can be computed, establish lower bounds on the size of such cutoffs, and identify cases where no cutoff exists. Third, we consider cases for which the parameterized system is equivalent to a single finite-state system (more precisely a Büchi word automaton), and establish tight bounds on the sizes of such automata.","lang":"eng"}],"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","oa_version":"None","day":"01","author":[{"id":"4A55BD00-F248-11E8-B48F-1D18A9856A87","last_name":"Aminof","full_name":"Aminof, Benjamin","first_name":"Benjamin"},{"full_name":"Kotek, Tomer","first_name":"Tomer","last_name":"Kotek"},{"last_name":"Rubin","full_name":"Rubin, Sacha","first_name":"Sacha"},{"last_name":"Spegni","first_name":"Francesco","full_name":"Spegni, Francesco"},{"first_name":"Helmut","full_name":"Veith, Helmut","last_name":"Veith"}],"publication_status":"published"},{"month":"09","conference":{"name":"CONCUR: Concurrency Theory","start_date":"2014-09-02","location":"Rome, Italy","end_date":"2014-09-05"},"user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1404.5084"}],"oa_version":"Submitted Version","day":"01","author":[{"full_name":"Hermanns, Holger","first_name":"Holger","last_name":"Hermanns"},{"first_name":"Jan","full_name":"Krčál, Jan","last_name":"Krčál"},{"first_name":"Jan","full_name":"Kretinsky, Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87","last_name":"Kretinsky"}],"type":"conference","status":"public","alternative_title":["LNCS"],"editor":[{"last_name":"Baldan","first_name":"Paolo","full_name":"Baldan, Paolo"},{"last_name":"Gorla","full_name":"Gorla, Daniele","first_name":"Daniele"}],"intvolume":"      8704","date_updated":"2021-01-12T06:55:00Z","oa":1,"title":"Probabilistic bisimulation: Naturally on distributions","publication":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","language":[{"iso":"eng"}],"abstract":[{"text":"In contrast to the usual understanding of probabilistic systems as stochastic processes, recently these systems have also been regarded as transformers of probabilities. In this paper, we give a natural definition of strong bisimulation for probabilistic systems corresponding to this view that treats probability distributions as first-class citizens. Our definition applies in the same way to discrete systems as well as to systems with uncountable state and action spaces. Several examples demonstrate that our definition refines the understanding of behavioural equivalences of probabilistic systems. In particular, it solves a longstanding open problem concerning the representation of memoryless continuous time by memoryfull continuous time. Finally, we give algorithms for computing this bisimulation not only for finite but also for classes of uncountably infinite systems.","lang":"eng"}],"publication_status":"published","date_published":"2014-09-01T00:00:00Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","volume":8704,"page":"249 - 265","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"project":[{"_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling","call_identifier":"FP7"},{"grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Moderne Concurrency Paradigms"}],"ec_funded":1,"year":"2014","acknowledgement":"This work is supported by the EU 7th Framework Programme under grant agreements 295261 (MEALS) and 318490 (SENSATION), Czech Science Foundation under grant agreement P202/12/G061, the DFG Transregional Collaborative Research Centre SFB/TR 14 AVACS, and by the CAS/SAFEA International Partnership Program for Creative Research Teams.","publist_id":"4993","date_created":"2018-12-11T11:55:27Z","citation":{"short":"H. Hermanns, J. Krčál, J. Kretinsky, in:, P. Baldan, D. Gorla (Eds.), Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 249–265.","ama":"Hermanns H, Krčál J, Kretinsky J. Probabilistic bisimulation: Naturally on distributions. In: Baldan P, Gorla D, eds. <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>. Vol 8704. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2014:249-265. doi:<a href=\"https://doi.org/10.1007/978-3-662-44584-6_18\">10.1007/978-3-662-44584-6_18</a>","ieee":"H. Hermanns, J. Krčál, and J. Kretinsky, “Probabilistic bisimulation: Naturally on distributions,” in <i>Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, Rome, Italy, 2014, vol. 8704, pp. 249–265.","ista":"Hermanns H, Krčál J, Kretinsky J. 2014. Probabilistic bisimulation: Naturally on distributions. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). CONCUR: Concurrency Theory, LNCS, vol. 8704, 249–265.","mla":"Hermanns, Holger, et al. “Probabilistic Bisimulation: Naturally on Distributions.” <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, edited by Paolo Baldan and Daniele Gorla, vol. 8704, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 249–65, doi:<a href=\"https://doi.org/10.1007/978-3-662-44584-6_18\">10.1007/978-3-662-44584-6_18</a>.","chicago":"Hermanns, Holger, Jan Krčál, and Jan Kretinsky. “Probabilistic Bisimulation: Naturally on Distributions.” In <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, edited by Paolo Baldan and Daniele Gorla, 8704:249–65. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. <a href=\"https://doi.org/10.1007/978-3-662-44584-6_18\">https://doi.org/10.1007/978-3-662-44584-6_18</a>.","apa":"Hermanns, H., Krčál, J., &#38; Kretinsky, J. (2014). Probabilistic bisimulation: Naturally on distributions. In P. Baldan &#38; D. Gorla (Eds.), <i>Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i> (Vol. 8704, pp. 249–265). Rome, Italy: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/978-3-662-44584-6_18\">https://doi.org/10.1007/978-3-662-44584-6_18</a>"},"doi":"10.1007/978-3-662-44584-6_18","_id":"2053"},{"doi":"10.1007/978-3-662-44584-6_37","_id":"2054","ec_funded":1,"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"3354"}]},"citation":{"chicago":"Chatterjee, Krishnendu. “Qualitative Concurrent Parity Games: Bounded Rationality.” In <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, edited by Paolo Baldan and Daniele Gorla, 8704:544–59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. <a href=\"https://doi.org/10.1007/978-3-662-44584-6_37\">https://doi.org/10.1007/978-3-662-44584-6_37</a>.","ista":"Chatterjee K. 2014. Qualitative concurrent parity games: Bounded rationality. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). CONCUR: Concurrency Theory, LNCS, vol. 8704, 544–559.","mla":"Chatterjee, Krishnendu. “Qualitative Concurrent Parity Games: Bounded Rationality.” <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, edited by Paolo Baldan and Daniele Gorla, vol. 8704, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 544–59, doi:<a href=\"https://doi.org/10.1007/978-3-662-44584-6_37\">10.1007/978-3-662-44584-6_37</a>.","short":"K. Chatterjee, in:, P. Baldan, D. Gorla (Eds.), Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 544–559.","ama":"Chatterjee K. Qualitative concurrent parity games: Bounded rationality. In: Baldan P, Gorla D, eds. <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>. Vol 8704. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2014:544-559. doi:<a href=\"https://doi.org/10.1007/978-3-662-44584-6_37\">10.1007/978-3-662-44584-6_37</a>","ieee":"K. Chatterjee, “Qualitative concurrent parity games: Bounded rationality,” in <i>Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, Rome, Italy, 2014, vol. 8704, pp. 544–559.","apa":"Chatterjee, K. (2014). Qualitative concurrent parity games: Bounded rationality. In P. Baldan &#38; D. Gorla (Eds.), <i>Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i> (Vol. 8704, pp. 544–559). Rome, Italy: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/978-3-662-44584-6_37\">https://doi.org/10.1007/978-3-662-44584-6_37</a>"},"date_created":"2018-12-11T11:55:27Z","publist_id":"4992","year":"2014","department":[{"_id":"KrCh"}],"page":"544 - 559","quality_controlled":"1","volume":8704,"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","date_published":"2014-09-01T00:00:00Z","project":[{"_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","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"abstract":[{"text":"We study two-player concurrent games on finite-state graphs played for an infinite number of rounds, where in each round, the two players (player 1 and player 2) choose their moves independently and simultaneously; the current state and the two moves determine the successor state. The objectives are ω-regular winning conditions specified as parity objectives. We consider the qualitative analysis problems: the computation of the almost-sure and limit-sure winning set of states, where player 1 can ensure to win with probability 1 and with probability arbitrarily close to 1, respectively. In general the almost-sure and limit-sure winning strategies require both infinite-memory as well as infinite-precision (to describe probabilities). While the qualitative analysis problem for concurrent parity games with infinite-memory, infinite-precision randomized strategies was studied before, we study the bounded-rationality problem for qualitative analysis of concurrent parity games, where the strategy set for player 1 is restricted to bounded-resource strategies. In terms of precision, strategies can be deterministic, uniform, finite-precision, or infinite-precision; and in terms of memory, strategies can be memoryless, finite-memory, or infinite-memory. We present a precise and complete characterization of the qualitative winning sets for all combinations of classes of strategies. In particular, we show that uniform memoryless strategies are as powerful as finite-precision infinite-memory strategies, and infinite-precision memoryless strategies are as powerful as infinite-precision finite-memory strategies. We show that the winning sets can be computed in (n2d+3) time, where n is the size of the game structure and 2d is the number of priorities (or colors), and our algorithms are symbolic. The membership problem of whether a state belongs to a winning set can be decided in NP ∩ coNP. Our symbolic algorithms are based on a characterization of the winning sets as μ-calculus formulas, however, our μ-calculus formulas are crucially different from the ones for concurrent parity games (without bounded rationality); and our memoryless witness strategy constructions are significantly different from the infinite-memory witness strategy constructions for concurrent parity games.","lang":"eng"}],"publication_status":"published","publication":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","language":[{"iso":"eng"}],"intvolume":"      8704","editor":[{"full_name":"Baldan, Paolo","first_name":"Paolo","last_name":"Baldan"},{"last_name":"Gorla","first_name":"Daniele","full_name":"Gorla, Daniele"}],"title":"Qualitative concurrent parity games: Bounded rationality","date_updated":"2023-02-23T11:23:36Z","alternative_title":["LNCS"],"status":"public","type":"conference","oa_version":"None","day":"01","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","conference":{"name":"CONCUR: Concurrency Theory","start_date":"2014-09-02","location":"Rome, Italy","end_date":"2014-09-05"},"month":"09","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"}]}]