[{"status":"public","pubrep_id":"170","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"file_date_updated":"2020-07-14T12:46:48Z","oa":1,"publisher":"IST Austria","publication_status":"published","date_published":"2014-02-19T00:00:00Z","_id":"5415","date_created":"2018-12-12T11:39:12Z","abstract":[{"text":"Recently there has been a significant effort to add quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, perhaps surprisingly, several basic system properties such as average response time cannot be expressed with weighted automata. In this work, we introduce nested weighted automata as a new formalism for expressing important quantitative properties such as average response time. We establish an almost complete decidability picture for the basic decision problems for nested weighted automata, and illustrate its applicability in several domains.  ","lang":"eng"}],"month":"02","file":[{"file_name":"IST-2014-170-v1+1_main.pdf","file_size":573457,"creator":"system","date_updated":"2020-07-14T12:46:48Z","access_level":"open_access","checksum":"31f90dcf2cf899c3f8c6427cfcc2b3c7","content_type":"application/pdf","file_id":"5497","relation":"main_file","date_created":"2018-12-12T11:53:36Z"}],"page":"27","publication_identifier":{"issn":["2664-1690"]},"doi":"10.15479/AT:IST-2014-170-v1-1","ddc":["004"],"language":[{"iso":"eng"}],"date_updated":"2023-02-23T12:26:19Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"status":"public","id":"1656","relation":"later_version"},{"status":"public","id":"467","relation":"later_version"},{"relation":"later_version","id":"5436","status":"public"}]},"author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Otop, Jan","first_name":"Jan","last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"}],"type":"technical_report","alternative_title":["IST Austria Technical Report"],"oa_version":"Published Version","year":"2014","has_accepted_license":"1","day":"19","title":"Nested weighted automata","citation":{"short":"K. Chatterjee, T.A. Henzinger, J. Otop, Nested Weighted Automata, IST Austria, 2014.","apa":"Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2014). <i>Nested weighted automata</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2014-170-v1-1\">https://doi.org/10.15479/AT:IST-2014-170-v1-1</a>","ama":"Chatterjee K, Henzinger TA, Otop J. <i>Nested Weighted Automata</i>. IST Austria; 2014. doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-170-v1-1\">10.15479/AT:IST-2014-170-v1-1</a>","ista":"Chatterjee K, Henzinger TA, Otop J. 2014. Nested weighted automata, IST Austria, 27p.","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, <i>Nested weighted automata</i>. IST Austria, 2014.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. <i>Nested Weighted Automata</i>. IST Austria, 2014. <a href=\"https://doi.org/10.15479/AT:IST-2014-170-v1-1\">https://doi.org/10.15479/AT:IST-2014-170-v1-1</a>.","mla":"Chatterjee, Krishnendu, et al. <i>Nested Weighted Automata</i>. IST Austria, 2014, doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-170-v1-1\">10.15479/AT:IST-2014-170-v1-1</a>."}},{"ddc":["000","005"],"doi":"10.15479/AT:IST-2014-176-v1-1","publication_identifier":{"issn":["2664-1690"]},"language":[{"iso":"eng"}],"date_updated":"2023-02-23T10:30:58Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"id":"2163","relation":"later_version","status":"public"}]},"has_accepted_license":"1","oa_version":"Published Version","year":"2014","alternative_title":["IST Austria Technical Report"],"type":"technical_report","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"full_name":"Doyen, Laurent","first_name":"Laurent","last_name":"Doyen"}],"day":"22","title":"Games with a weak adversary","citation":{"ama":"Chatterjee K, Doyen L. <i>Games with a Weak Adversary</i>. IST Austria; 2014. doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-176-v1-1\">10.15479/AT:IST-2014-176-v1-1</a>","apa":"Chatterjee, K., &#38; Doyen, L. (2014). <i>Games with a weak adversary</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2014-176-v1-1\">https://doi.org/10.15479/AT:IST-2014-176-v1-1</a>","short":"K. Chatterjee, L. Doyen, Games with a Weak Adversary, IST Austria, 2014.","mla":"Chatterjee, Krishnendu, and Laurent Doyen. <i>Games with a Weak Adversary</i>. IST Austria, 2014, doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-176-v1-1\">10.15479/AT:IST-2014-176-v1-1</a>.","chicago":"Chatterjee, Krishnendu, and Laurent Doyen. <i>Games with a Weak Adversary</i>. IST Austria, 2014. <a href=\"https://doi.org/10.15479/AT:IST-2014-176-v1-1\">https://doi.org/10.15479/AT:IST-2014-176-v1-1</a>.","ista":"Chatterjee K, Doyen L. 2014. Games with a weak adversary, IST Austria, 18p.","ieee":"K. Chatterjee and L. Doyen, <i>Games with a weak adversary</i>. IST Austria, 2014."},"status":"public","pubrep_id":"176","department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:46:49Z","oa":1,"publisher":"IST Austria","publication_status":"published","date_published":"2014-03-22T00:00:00Z","_id":"5418","date_created":"2018-12-12T11:39:13Z","abstract":[{"text":"We consider multi-player graph games with partial-observation and parity objective. While the decision problem for three-player games with a coalition of the first and second players against the third player is undecidable, we present a decidability result for partial-observation games where the first and third player are in a coalition against the second player, thus where the second player is adversarial but weaker due to partial-observation. We establish tight complexity bounds in the case where player 1 is less informed than player 2, namely 2-EXPTIME-completeness for parity objectives. The symmetric case of player 1 more informed than player 2 is much more complicated, and we show that already in the case where player 1 has perfect observation, memory of size non-elementary is necessary in general for reachability objectives, and the problem is decidable for safety and reachability objectives. Our results have tight connections with partial-observation stochastic games for which we derive new complexity results.","lang":"eng"}],"file":[{"date_created":"2018-12-12T11:53:07Z","relation":"main_file","file_id":"5468","content_type":"application/pdf","access_level":"open_access","date_updated":"2020-07-14T12:46:49Z","checksum":"1d6958aa60050e1c3e932c6e5f34c39f","file_size":328253,"creator":"system","file_name":"IST-2014-176-v1+1_icalp_14.pdf"}],"month":"03","page":"18"},{"pubrep_id":"187","status":"public","department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:46:50Z","oa":1,"publication_status":"published","publisher":"IST Austria","date_published":"2014-04-14T00:00:00Z","_id":"5419","abstract":[{"text":"We consider the reachability and shortest path problems on low tree-width graphs, with n nodes, m edges, and tree-width t, on a standard RAM with wordsize W. We use O to hide polynomial factors of the inverse of the Ackermann function. Our main contributions are three fold:\r\n1. For reachability, we present an algorithm that requires O(n·t2·log(n/t)) preprocessing time, O(n·(t·log(n/t))/W) space, and O(t/W) time for pair queries and O((n·t)/W) time for single-source queries. Note that for constant t our algorithm uses O(n·logn) time for preprocessing; and O(n/W) time for single-source queries, which is faster than depth first search/breath first search (after the preprocessing).\r\n2. We present an algorithm for shortest path that requires O(n·t2) preprocessing time, O(n·t) space, and O(t2) time for pair queries and O(n·t) time single-source queries.\r\n3. We give a space versus query time trade-off algorithm for shortest path that, given any constant >0, requires O(n·t2) preprocessing time, O(n·t2) space, and O(n1−·t2) time for pair queries.\r\nOur algorithms improve all existing results, and use very simple data structures.","lang":"eng"}],"date_created":"2018-12-12T11:39:13Z","file":[{"file_name":"IST-2014-187-v1+1_main_full_tech.pdf","file_size":670031,"creator":"system","checksum":"c608e66030a4bf51d2d99b451f539b99","date_updated":"2020-07-14T12:46:50Z","access_level":"open_access","content_type":"application/pdf","relation":"main_file","file_id":"5548","date_created":"2018-12-12T11:54:25Z"}],"month":"04","page":"34","doi":"10.15479/AT:IST-2014-187-v1-1","ddc":["000"],"publication_identifier":{"issn":["2664-1690"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"date_updated":"2021-01-12T08:02:03Z","year":"2014","oa_version":"Published Version","has_accepted_license":"1","alternative_title":["IST Austria Technical Report"],"author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","last_name":"Ibsen-Jensen"},{"last_name":"Pavlogiannis","first_name":"Andreas","full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722"}],"type":"technical_report","day":"14","title":"Improved algorithms for reachability and shortest path on low tree-width graphs","citation":{"apa":"Chatterjee, K., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2014). <i>Improved algorithms for reachability and shortest path on low tree-width graphs</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2014-187-v1-1\">https://doi.org/10.15479/AT:IST-2014-187-v1-1</a>","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. <i>Improved Algorithms for Reachability and Shortest Path on Low Tree-Width Graphs</i>. IST Austria; 2014. doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-187-v1-1\">10.15479/AT:IST-2014-187-v1-1</a>","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Improved Algorithms for Reachability and Shortest Path on Low Tree-Width Graphs, IST Austria, 2014.","mla":"Chatterjee, Krishnendu, et al. <i>Improved Algorithms for Reachability and Shortest Path on Low Tree-Width Graphs</i>. IST Austria, 2014, doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-187-v1-1\">10.15479/AT:IST-2014-187-v1-1</a>.","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2014. Improved algorithms for reachability and shortest path on low tree-width graphs, IST Austria, 34p.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, <i>Improved algorithms for reachability and shortest path on low tree-width graphs</i>. IST Austria, 2014.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. <i>Improved Algorithms for Reachability and Shortest Path on Low Tree-Width Graphs</i>. IST Austria, 2014. <a href=\"https://doi.org/10.15479/AT:IST-2014-187-v1-1\">https://doi.org/10.15479/AT:IST-2014-187-v1-1</a>."}},{"date_updated":"2021-01-12T08:02:05Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"doi":"10.15479/AT:IST-2014-191-v1-1","ddc":["000","005"],"publication_identifier":{"issn":["2664-1690"]},"day":"14","year":"2014","alternative_title":["IST Austria Technical Report"],"has_accepted_license":"1","oa_version":"Published Version","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"last_name":"Ibsen-Jensen","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87"}],"type":"technical_report","citation":{"short":"K. Chatterjee, R. Ibsen-Jensen, The Value 1 Problem for Concurrent Mean-Payoff Games, IST Austria, 2014.","ama":"Chatterjee K, Ibsen-Jensen R. <i>The Value 1 Problem for Concurrent Mean-Payoff Games</i>. IST Austria; 2014. doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-191-v1-1\">10.15479/AT:IST-2014-191-v1-1</a>","apa":"Chatterjee, K., &#38; Ibsen-Jensen, R. (2014). <i>The value 1 problem for concurrent mean-payoff games</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2014-191-v1-1\">https://doi.org/10.15479/AT:IST-2014-191-v1-1</a>","chicago":"Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. <i>The Value 1 Problem for Concurrent Mean-Payoff Games</i>. IST Austria, 2014. <a href=\"https://doi.org/10.15479/AT:IST-2014-191-v1-1\">https://doi.org/10.15479/AT:IST-2014-191-v1-1</a>.","ista":"Chatterjee K, Ibsen-Jensen R. 2014. The value 1 problem for concurrent mean-payoff games, IST Austria, 49p.","ieee":"K. Chatterjee and R. Ibsen-Jensen, <i>The value 1 problem for concurrent mean-payoff games</i>. IST Austria, 2014.","mla":"Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. <i>The Value 1 Problem for Concurrent Mean-Payoff Games</i>. IST Austria, 2014, doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-191-v1-1\">10.15479/AT:IST-2014-191-v1-1</a>."},"title":"The value 1 problem for concurrent mean-payoff games","file_date_updated":"2020-07-14T12:46:50Z","department":[{"_id":"KrCh"}],"pubrep_id":"191","status":"public","publication_status":"published","publisher":"IST Austria","oa":1,"file":[{"content_type":"application/pdf","file_id":"5520","relation":"main_file","date_created":"2018-12-12T11:53:58Z","file_name":"IST-2014-191-v1+1_main_full.pdf","file_size":584368,"creator":"system","date_updated":"2020-07-14T12:46:50Z","access_level":"open_access","checksum":"49e0fd3e62650346daf7dc04604f7a0a"}],"month":"04","_id":"5420","abstract":[{"text":"We consider concurrent mean-payoff games, a very well-studied class of two-player (player 1 vs player 2) zero-sum games on finite-state graphs where every transition is assigned a reward between 0 and 1, and the payoff function is the long-run average of the rewards. The value is the maximal expected payoff that player 1 can guarantee against all strategies of player 2. We consider the computation of the set of states with value 1 under finite-memory strategies for player 1, and our main results for the problem are as follows: (1) we present a polynomial-time algorithm; (2) we show that whenever there is a finite-memory strategy, there is a stationary strategy that does not need memory at all; and (3) we present an optimal bound (which is double exponential) on the patience of stationary strategies (where patience of a distribution is the inverse of the smallest positive probability and represents a complexity measure of a stationary strategy).","lang":"eng"}],"date_published":"2014-04-14T00:00:00Z","date_created":"2018-12-12T11:39:14Z","page":"49"},{"oa":1,"publisher":"IST Austria","publication_status":"published","pubrep_id":"190","status":"public","department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:46:50Z","page":"27","_id":"5421","abstract":[{"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 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. 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: (1) We show that the qualitative question is NP-complete and the quantitative approximation question is #P-hard in the special case when the interaction and the replacement graphs coincide and even with the restriction that the resident individuals do not reproduce (which corresponds to an invading population taking over an empty structure). (2) We show that in general the qualitative question is PSPACE-complete and the quantitative approximation question is PSPACE-hard and can be solved in exponential time.","lang":"eng"}],"date_published":"2014-04-18T00:00:00Z","date_created":"2018-12-12T11:39:14Z","month":"04","file":[{"date_updated":"2020-07-14T12:46:50Z","access_level":"open_access","checksum":"42f3d8b563286eb0d903832bd9a848d3","file_name":"IST-2014-190-v2+2_main_full.pdf","file_size":443529,"creator":"system","date_created":"2018-12-12T11:54:16Z","content_type":"application/pdf","file_id":"5538","relation":"main_file"},{"date_updated":"2020-07-14T12:46:50Z","access_level":"open_access","checksum":"0c9a2fd822309719634495a35957e34d","file_name":"IST-2014-190-v1+1_main_full.pdf","file_size":440911,"creator":"kschuh","date_created":"2019-09-06T07:30:20Z","content_type":"application/pdf","relation":"main_file","file_id":"6852"}],"related_material":{"record":[{"status":"public","id":"5432","relation":"later_version"},{"status":"public","id":"5440","relation":"later_version"}]},"publication_identifier":{"issn":["2664-1690"]},"doi":"10.15479/AT:IST-2014-190-v2-2","ddc":["000","005"],"date_updated":"2023-02-23T12:26:33Z","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"title":"The complexity of evolution on graphs","citation":{"short":"K. Chatterjee, R. Ibsen-Jensen, M. Nowak, The Complexity of Evolution on Graphs, IST Austria, 2014.","apa":"Chatterjee, K., Ibsen-Jensen, R., &#38; Nowak, M. (2014). <i>The complexity of evolution on graphs</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2014-190-v2-2\">https://doi.org/10.15479/AT:IST-2014-190-v2-2</a>","ama":"Chatterjee K, Ibsen-Jensen R, Nowak M. <i>The Complexity of Evolution on Graphs</i>. IST Austria; 2014. doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-190-v2-2\">10.15479/AT:IST-2014-190-v2-2</a>","ieee":"K. Chatterjee, R. Ibsen-Jensen, and M. Nowak, <i>The complexity of evolution on graphs</i>. IST Austria, 2014.","ista":"Chatterjee K, Ibsen-Jensen R, Nowak M. 2014. The complexity of evolution on graphs, IST Austria, 27p.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Martin Nowak. <i>The Complexity of Evolution on Graphs</i>. IST Austria, 2014. <a href=\"https://doi.org/10.15479/AT:IST-2014-190-v2-2\">https://doi.org/10.15479/AT:IST-2014-190-v2-2</a>.","mla":"Chatterjee, Krishnendu, et al. <i>The Complexity of Evolution on Graphs</i>. IST Austria, 2014, doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-190-v2-2\">10.15479/AT:IST-2014-190-v2-2</a>."},"author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"last_name":"Ibsen-Jensen","first_name":"Rasmus","full_name":"Ibsen-Jensen, Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389"},{"last_name":"Nowak","first_name":"Martin","full_name":"Nowak, Martin"}],"type":"technical_report","has_accepted_license":"1","year":"2014","alternative_title":["IST Austria Technical Report"],"oa_version":"Published Version","day":"18"},{"citation":{"mla":"Chatterjee, Krishnendu, et al. <i>A Framework for Automated Competitive Analysis of On-Line Scheduling of Firm-Deadline Tasks</i>. IST Austria, 2014, doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-300-v1-1\">10.15479/AT:IST-2014-300-v1-1</a>.","ista":"Chatterjee K, Kössler A, Pavlogiannis A, Schmid U. 2014. A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks, IST Austria, 14p.","ieee":"K. Chatterjee, A. Kössler, A. Pavlogiannis, and U. Schmid, <i>A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks</i>. IST Austria, 2014.","chicago":"Chatterjee, Krishnendu, Alexander Kössler, Andreas Pavlogiannis, and Ulrich Schmid. <i>A Framework for Automated Competitive Analysis of On-Line Scheduling of Firm-Deadline Tasks</i>. IST Austria, 2014. <a href=\"https://doi.org/10.15479/AT:IST-2014-300-v1-1\">https://doi.org/10.15479/AT:IST-2014-300-v1-1</a>.","apa":"Chatterjee, K., Kössler, A., Pavlogiannis, A., &#38; Schmid, U. (2014). <i>A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2014-300-v1-1\">https://doi.org/10.15479/AT:IST-2014-300-v1-1</a>","ama":"Chatterjee K, Kössler A, Pavlogiannis A, Schmid U. <i>A Framework for Automated Competitive Analysis of On-Line Scheduling of Firm-Deadline Tasks</i>. IST Austria; 2014. doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-300-v1-1\">10.15479/AT:IST-2014-300-v1-1</a>","short":"K. Chatterjee, A. Kössler, A. Pavlogiannis, U. Schmid, A Framework for Automated Competitive Analysis of On-Line Scheduling of Firm-Deadline Tasks, IST Austria, 2014."},"title":"A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks","day":"29","type":"technical_report","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu"},{"full_name":"Kössler, Alexander","first_name":"Alexander","last_name":"Kössler"},{"orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis"},{"last_name":"Schmid","full_name":"Schmid, Ulrich","first_name":"Ulrich"}],"year":"2014","oa_version":"Published Version","has_accepted_license":"1","alternative_title":["IST Austria Technical Report"],"related_material":{"record":[{"id":"1714","relation":"later_version","status":"public"}]},"date_updated":"2023-02-23T10:11:15Z","language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_identifier":{"issn":["2664-1690"]},"ddc":["005"],"doi":"10.15479/AT:IST-2014-300-v1-1","page":"14","month":"07","file":[{"file_id":"5514","relation":"main_file","content_type":"application/pdf","date_created":"2018-12-12T11:53:53Z","creator":"system","file_size":1270021,"file_name":"IST-2014-300-v1+1_main.pdf","checksum":"4b8fde4d9ef6653837f6803921d83032","access_level":"open_access","date_updated":"2020-07-14T12:46:50Z"}],"_id":"5423","abstract":[{"lang":"eng","text":"We present a flexible framework for the automated competitive analysis of on-line scheduling algorithms for firm- deadline real-time tasks based on multi-objective graphs: Given a taskset and an on-line scheduling algorithm specified as a labeled transition system, along with some optional safety, liveness, and/or limit-average constraints for the adversary, we automatically compute the competitive ratio of the algorithm w.r.t. a clairvoyant scheduler. We demonstrate the flexibility and power of our approach by comparing the competitive ratio of several on-line algorithms, including D(over), that have been proposed in the past, for various tasksets. Our experimental results reveal that none of these algorithms is universally optimal, in the sense that there are tasksets where other schedulers provide better performance. Our framework is hence a very useful design tool for selecting optimal algorithms for a given application. "}],"date_published":"2014-07-29T00:00:00Z","date_created":"2018-12-12T11:39:15Z","publication_status":"published","publisher":"IST Austria","oa":1,"file_date_updated":"2020-07-14T12:46:50Z","department":[{"_id":"KrCh"}],"status":"public","pubrep_id":"300"},{"related_material":{"record":[{"status":"public","id":"1732","relation":"later_version"},{"id":"5426","relation":"later_version","status":"public"}]},"ddc":["005"],"doi":"10.15479/AT:IST-2014-305-v1-1","publication_identifier":{"issn":["2664-1690"]},"date_updated":"2023-02-23T12:25:52Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"title":"Qualitative analysis of POMDPs with temporal logic specifications for robotics applications","citation":{"mla":"Chatterjee, Krishnendu, et al. <i>Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications</i>. IST Austria, 2014, doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-305-v1-1\">10.15479/AT:IST-2014-305-v1-1</a>.","ista":"Chatterjee K, Chmelik M, Gupta R, Kanodia A. 2014. Qualitative analysis of POMDPs with temporal logic specifications for robotics applications, IST Austria, 12p.","ieee":"K. Chatterjee, M. Chmelik, R. Gupta, and A. Kanodia, <i>Qualitative analysis of POMDPs with temporal logic specifications for robotics applications</i>. IST Austria, 2014.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, Raghav Gupta, and Ayush Kanodia. <i>Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications</i>. IST Austria, 2014. <a href=\"https://doi.org/10.15479/AT:IST-2014-305-v1-1\">https://doi.org/10.15479/AT:IST-2014-305-v1-1</a>.","apa":"Chatterjee, K., Chmelik, M., Gupta, R., &#38; Kanodia, A. (2014). <i>Qualitative analysis of POMDPs with temporal logic specifications for robotics applications</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2014-305-v1-1\">https://doi.org/10.15479/AT:IST-2014-305-v1-1</a>","ama":"Chatterjee K, Chmelik M, Gupta R, Kanodia A. <i>Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications</i>. IST Austria; 2014. doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-305-v1-1\">10.15479/AT:IST-2014-305-v1-1</a>","short":"K. Chatterjee, M. Chmelik, R. Gupta, A. Kanodia, Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications, IST Austria, 2014."},"alternative_title":["IST Austria Technical Report"],"has_accepted_license":"1","oa_version":"Published Version","year":"2014","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik","first_name":"Martin","full_name":"Chmelik, Martin"},{"full_name":"Gupta, Raghav","first_name":"Raghav","last_name":"Gupta"},{"last_name":"Kanodia","first_name":"Ayush","full_name":"Kanodia, Ayush"}],"type":"technical_report","day":"09","oa":1,"publication_status":"published","publisher":"IST Austria","status":"public","pubrep_id":"305","department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:46:51Z","page":"12","_id":"5424","abstract":[{"text":"We consider partially observable Markov decision processes (POMDPs), that are a standard framework for robotics applications to model uncertainties present in the real world, with temporal logic specifications. All temporal logic specifications in linear-time temporal logic (LTL) can be expressed as parity objectives. We study the qualitative analysis problem for POMDPs with parity objectives that asks whether there is a controller (policy) to ensure that the objective holds with probability 1 (almost-surely). While the qualitative analysis of POMDPs with parity objectives is undecidable, recent results show that when restricted to finite-memory policies the problem is EXPTIME-complete. While the problem is intractable in theory, we present a practical approach to solve the qualitative analysis problem. We designed several heuristics to deal with the exponential complexity, and have used our implementation on a number of well-known POMDP examples for robotics applications. Our results provide the first practical approach to solve the qualitative analysis of robot motion planning with LTL properties in the presence of uncertainty.","lang":"eng"}],"date_created":"2018-12-12T11:39:15Z","date_published":"2014-09-09T00:00:00Z","file":[{"date_created":"2018-12-12T11:53:51Z","relation":"main_file","file_id":"5512","content_type":"application/pdf","checksum":"35009d5fad01198341e6c1a3353481b7","access_level":"open_access","date_updated":"2020-07-14T12:46:51Z","creator":"system","file_size":655774,"file_name":"IST-2014-305-v1+1_main.pdf"}],"month":"09"},{"page":"10","file":[{"checksum":"730c0a8e97cf2712a884b2cc423f3919","access_level":"open_access","date_updated":"2020-07-14T12:46:51Z","creator":"system","file_size":656019,"file_name":"IST-2014-305-v2+1_main2.pdf","date_created":"2018-12-12T11:54:15Z","file_id":"5537","relation":"main_file","content_type":"application/pdf"}],"month":"09","date_created":"2018-12-12T11:39:16Z","_id":"5426","abstract":[{"lang":"eng","text":"We consider partially observable Markov decision processes (POMDPs), that are a standard framework for robotics applications to model uncertainties present in the real world, with temporal logic specifications. All temporal logic specifications in linear-time temporal logic (LTL) can be expressed as parity objectives. We study the qualitative analysis problem for POMDPs with parity objectives that asks whether there is a controller (policy) to ensure that the objective holds with probability 1 (almost-surely). While the qualitative analysis of POMDPs with parity objectives is undecidable, recent results show that when restricted to finite-memory policies the problem is EXPTIME-complete. While the problem is intractable in theory, we present a practical approach to solve the qualitative analysis problem. We designed several heuristics to deal with the exponential complexity, and have used our implementation on a number of well-known POMDP examples for robotics applications. Our results provide the first practical approach to solve the qualitative analysis of robot motion planning with LTL properties in the presence of uncertainty."}],"date_published":"2014-09-29T00:00:00Z","publication_status":"published","publisher":"IST Austria","oa":1,"file_date_updated":"2020-07-14T12:46:51Z","department":[{"_id":"KrCh"}],"pubrep_id":"311","status":"public","citation":{"chicago":"Chatterjee, Krishnendu, Martin Chmelik, Raghav Gupta, and Ayush Kanodia. <i>Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications</i>. IST Austria, 2014. <a href=\"https://doi.org/10.15479/AT:IST-2014-305-v2-1\">https://doi.org/10.15479/AT:IST-2014-305-v2-1</a>.","ieee":"K. Chatterjee, M. Chmelik, R. Gupta, and A. Kanodia, <i>Qualitative analysis of POMDPs with temporal logic specifications for robotics applications</i>. IST Austria, 2014.","ista":"Chatterjee K, Chmelik M, Gupta R, Kanodia A. 2014. Qualitative analysis of POMDPs with temporal logic specifications for robotics applications, IST Austria, 10p.","mla":"Chatterjee, Krishnendu, et al. <i>Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications</i>. IST Austria, 2014, doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-305-v2-1\">10.15479/AT:IST-2014-305-v2-1</a>.","short":"K. Chatterjee, M. Chmelik, R. Gupta, A. Kanodia, Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications, IST Austria, 2014.","ama":"Chatterjee K, Chmelik M, Gupta R, Kanodia A. <i>Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications</i>. IST Austria; 2014. doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-305-v2-1\">10.15479/AT:IST-2014-305-v2-1</a>","apa":"Chatterjee, K., Chmelik, M., Gupta, R., &#38; Kanodia, A. (2014). <i>Qualitative analysis of POMDPs with temporal logic specifications for robotics applications</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2014-305-v2-1\">https://doi.org/10.15479/AT:IST-2014-305-v2-1</a>"},"title":"Qualitative analysis of POMDPs with temporal logic specifications for robotics applications","day":"29","year":"2014","oa_version":"Published Version","alternative_title":["IST Austria Technical Report"],"has_accepted_license":"1","type":"technical_report","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee"},{"id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik","full_name":"Chmelik, Martin","first_name":"Martin"},{"last_name":"Gupta","full_name":"Gupta, Raghav","first_name":"Raghav"},{"last_name":"Kanodia","full_name":"Kanodia, Ayush","first_name":"Ayush"}],"related_material":{"record":[{"id":"1732","relation":"later_version","status":"public"},{"status":"public","relation":"earlier_version","id":"5424"}]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-02-23T12:25:47Z","language":[{"iso":"eng"}],"doi":"10.15479/AT:IST-2014-305-v2-1","ddc":["005"],"publication_identifier":{"issn":["2664-1690"]}},{"page":"24","month":"11","file":[{"file_id":"5471","relation":"main_file","content_type":"application/pdf","date_created":"2018-12-12T11:53:10Z","creator":"system","file_size":405561,"file_name":"IST-2014-314-v1+1_long.pdf","checksum":"9d3b90bf4fff74664f182f2d95ef727a","access_level":"open_access","date_updated":"2020-07-14T12:46:52Z"}],"_id":"5427","date_created":"2018-12-12T11:39:16Z","date_published":"2014-11-05T00:00:00Z","abstract":[{"text":"We consider graphs with n nodes together with their tree-decomposition that has b = O ( n ) bags and width t , on the standard RAM computational model with wordsize W = Θ (log n ) . Our contributions are two-fold: Our first contribution is an algorithm that given a graph and its tree-decomposition as input, computes a binary and balanced tree-decomposition of width at most 4 · t + 3 of the graph in O ( b ) time and space, improving a long-standing (from 1992) bound of O ( n · log n ) time for constant treewidth graphs. Our second contribution is on reachability queries for low treewidth graphs. We build on our tree-balancing algorithm and present a data-structure for graph reachability that requires O ( n · t 2 ) preprocessing time, O ( n · t ) space, and O ( d t/ log n e ) time for pair queries, and O ( n · t · log t/ log n ) time for single-source queries. For constant t our data-structure uses O ( n ) time for preprocessing, O (1) time for pair queries, and O ( n/ log n ) time for single-source queries. This is (asymptotically) optimal and is faster than DFS/BFS when answering more than a constant number of single-source queries.","lang":"eng"}],"publisher":"IST Austria","publication_status":"published","oa":1,"department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:46:52Z","status":"public","pubrep_id":"314","citation":{"apa":"Chatterjee, K., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2014). <i>Optimal tree-decomposition balancing and reachability on low treewidth graphs</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2014-314-v1-1\">https://doi.org/10.15479/AT:IST-2014-314-v1-1</a>","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. <i>Optimal Tree-Decomposition Balancing and Reachability on Low Treewidth Graphs</i>. IST Austria; 2014. doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-314-v1-1\">10.15479/AT:IST-2014-314-v1-1</a>","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Optimal Tree-Decomposition Balancing and Reachability on Low Treewidth Graphs, IST Austria, 2014.","mla":"Chatterjee, Krishnendu, et al. <i>Optimal Tree-Decomposition Balancing and Reachability on Low Treewidth Graphs</i>. IST Austria, 2014, doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-314-v1-1\">10.15479/AT:IST-2014-314-v1-1</a>.","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2014. Optimal tree-decomposition balancing and reachability on low treewidth graphs, IST Austria, 24p.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, <i>Optimal tree-decomposition balancing and reachability on low treewidth graphs</i>. IST Austria, 2014.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. <i>Optimal Tree-Decomposition Balancing and Reachability on Low Treewidth Graphs</i>. IST Austria, 2014. <a href=\"https://doi.org/10.15479/AT:IST-2014-314-v1-1\">https://doi.org/10.15479/AT:IST-2014-314-v1-1</a>."},"title":"Optimal tree-decomposition balancing and reachability on low treewidth graphs","day":"05","type":"technical_report","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","full_name":"Pavlogiannis, Andreas","first_name":"Andreas","last_name":"Pavlogiannis"}],"has_accepted_license":"1","alternative_title":["IST Austria Technical Report"],"oa_version":"Published Version","year":"2014","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","language":[{"iso":"eng"}],"date_updated":"2021-01-12T08:02:09Z","publication_identifier":{"issn":["2664-1690"]},"ddc":["000"],"doi":"10.15479/AT:IST-2014-314-v1-1"},{"oa":1,"publisher":"IST Austria","publication_status":"published","pubrep_id":"315","status":"public","file_date_updated":"2020-07-14T12:46:52Z","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"page":"26","_id":"5428","date_published":"2014-12-05T00:00:00Z","date_created":"2018-12-12T11:39:16Z","abstract":[{"text":"Simulation is an attractive alternative for language inclusion for automata as it is an under-approximation of language inclusion, but usually has much lower complexity. For non-deterministic automata, while language inclusion is PSPACE-complete, simulation can be computed in polynomial time. Simulation has also been extended in two orthogonal directions, namely, (1) fair simulation, for simulation over specified set of infinite runs; and (2) quantitative simulation, for simulation between weighted automata. Again, while fair trace inclusion is PSPACE-complete, fair simulation can be computed in polynomial time. For weighted automata, the (quantitative) language inclusion problem is undecidable for mean-payoff automata and the decidability is open for discounted-sum automata, whereas the (quantitative) simulation reduce to mean-payoff games and discounted-sum games, which admit pseudo-polynomial time algorithms.\r\n\r\nIn this work, we study (quantitative) simulation for weighted automata with Büchi acceptance conditions, i.e., we generalize fair simulation from non-weighted automata to weighted automata. We show that imposing Büchi acceptance conditions on weighted automata changes many fundamental properties of the simulation games. For example, whereas for mean-payoff and discounted-sum games, the players do not need memory to play optimally; we show in contrast that for simulation games with Büchi acceptance conditions, (i) for mean-payoff objectives, optimal strategies for both players require infinite memory in general, and (ii) for discounted-sum objectives, optimal strategies need not exist for both players. While the simulation games with Büchi acceptance conditions are more complicated (e.g., due to infinite-memory requirements for mean-payoff objectives) as compared to their counterpart without Büchi acceptance conditions, we still present pseudo-polynomial time algorithms to solve simulation games with Büchi acceptance conditions for both weighted mean-payoff and weighted discounted-sum automata.","lang":"eng"}],"file":[{"checksum":"b1d573bc04365625ff9974880c0aa807","access_level":"open_access","date_updated":"2020-07-14T12:46:52Z","creator":"system","file_size":531046,"file_name":"IST-2014-315-v1+1_report.pdf","date_created":"2018-12-12T11:53:59Z","relation":"main_file","file_id":"5521","content_type":"application/pdf"}],"month":"12","related_material":{"record":[{"status":"public","relation":"later_version","id":"1066"}]},"ddc":["004"],"doi":"10.15479/AT:IST-2014-315-v1-1","publication_identifier":{"issn":["2664-1690"]},"date_updated":"2023-09-20T12:07:48Z","language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Quantitative fair simulation games","citation":{"ieee":"K. Chatterjee, T. A. Henzinger, J. Otop, and Y. Velner, <i>Quantitative fair simulation games</i>. IST Austria, 2014.","ista":"Chatterjee K, Henzinger TA, Otop J, Velner Y. 2014. Quantitative fair simulation games, IST Austria, 26p.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Yaron Velner. <i>Quantitative Fair Simulation Games</i>. IST Austria, 2014. <a href=\"https://doi.org/10.15479/AT:IST-2014-315-v1-1\">https://doi.org/10.15479/AT:IST-2014-315-v1-1</a>.","mla":"Chatterjee, Krishnendu, et al. <i>Quantitative Fair Simulation Games</i>. IST Austria, 2014, doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-315-v1-1\">10.15479/AT:IST-2014-315-v1-1</a>.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, Y. Velner, Quantitative Fair Simulation Games, IST Austria, 2014.","apa":"Chatterjee, K., Henzinger, T. A., Otop, J., &#38; Velner, Y. (2014). <i>Quantitative fair simulation games</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:IST-2014-315-v1-1\">https://doi.org/10.15479/AT:IST-2014-315-v1-1</a>","ama":"Chatterjee K, Henzinger TA, Otop J, Velner Y. <i>Quantitative Fair Simulation Games</i>. IST Austria; 2014. doi:<a href=\"https://doi.org/10.15479/AT:IST-2014-315-v1-1\">10.15479/AT:IST-2014-315-v1-1</a>"},"alternative_title":["IST Austria Technical Report"],"oa_version":"Published Version","year":"2014","has_accepted_license":"1","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"first_name":"Jan","full_name":"Otop, Jan","last_name":"Otop","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Yaron","full_name":"Velner, Yaron","last_name":"Velner"}],"type":"technical_report","day":"05"},{"project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"grant_number":"S11407","name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"doi":"10.1016/j.tcs.2014.06.031","language":[{"iso":"eng"}],"title":"Approximating the minimum cycle mean","citation":{"short":"K. Chatterjee, M.H. Henzinger, S. Krinninger, V. Loitzenbauer, M. Raskin, Theoretical Computer Science 547 (2014) 104–116.","ama":"Chatterjee K, Henzinger MH, Krinninger S, Loitzenbauer V, Raskin M. Approximating the minimum cycle mean. <i>Theoretical Computer Science</i>. 2014;547(C):104-116. doi:<a href=\"https://doi.org/10.1016/j.tcs.2014.06.031\">10.1016/j.tcs.2014.06.031</a>","apa":"Chatterjee, K., Henzinger, M. H., Krinninger, S., Loitzenbauer, V., &#38; Raskin, M. (2014). Approximating the minimum cycle mean. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.tcs.2014.06.031\">https://doi.org/10.1016/j.tcs.2014.06.031</a>","chicago":"Chatterjee, Krishnendu, Monika H Henzinger, Sebastian Krinninger, Veronika Loitzenbauer, and Michael Raskin. “Approximating the Minimum Cycle Mean.” <i>Theoretical Computer Science</i>. Elsevier, 2014. <a href=\"https://doi.org/10.1016/j.tcs.2014.06.031\">https://doi.org/10.1016/j.tcs.2014.06.031</a>.","ista":"Chatterjee K, Henzinger MH, Krinninger S, Loitzenbauer V, Raskin M. 2014. Approximating the minimum cycle mean. Theoretical Computer Science. 547(C), 104–116.","ieee":"K. Chatterjee, M. H. Henzinger, S. Krinninger, V. Loitzenbauer, and M. Raskin, “Approximating the minimum cycle mean,” <i>Theoretical Computer Science</i>, vol. 547, no. C. Elsevier, pp. 104–116, 2014.","mla":"Chatterjee, Krishnendu, et al. “Approximating the Minimum Cycle Mean.” <i>Theoretical Computer Science</i>, vol. 547, no. C, Elsevier, 2014, pp. 104–16, doi:<a href=\"https://doi.org/10.1016/j.tcs.2014.06.031\">10.1016/j.tcs.2014.06.031</a>."},"ec_funded":1,"type":"journal_article","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"id":"540c9bbd-f2de-11ec-812d-d04a5be85630","orcid":"0000-0002-5008-6530","last_name":"Henzinger","full_name":"Henzinger, Monika H","first_name":"Monika H"},{"last_name":"Krinninger","first_name":"Sebastian","full_name":"Krinninger, Sebastian"},{"full_name":"Loitzenbauer, Veronika","first_name":"Veronika","last_name":"Loitzenbauer"},{"last_name":"Raskin","full_name":"Raskin, Michael","first_name":"Michael"}],"day":"28","publisher":"Elsevier","status":"public","intvolume":"       547","publication":"Theoretical Computer Science","quality_controlled":"1","department":[{"_id":"KrCh"}],"page":"104 - 116","date_created":"2018-12-11T11:51:40Z","month":"08","scopus_import":"1","external_id":{"arxiv":["1307.4473"]},"date_updated":"2022-09-09T11:50:58Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Preprint","year":"2014","article_type":"original","publist_id":"5836","main_file_link":[{"url":"http://arxiv.org/abs/1307.4473","open_access":"1"}],"oa":1,"publication_status":"published","volume":547,"article_processing_charge":"No","issue":"C","arxiv":1,"_id":"1375","abstract":[{"lang":"eng","text":"We consider directed graphs where each edge is labeled with an integer weight and study the fundamental algorithmic question of computing the value of a cycle with minimum mean weight. Our contributions are twofold: (1) First we show that the algorithmic question is reducible to the problem of a logarithmic number of min-plus matrix multiplications of n×n-matrices, where n is the number of vertices of the graph. (2) Second, when the weights are nonnegative, we present the first (1+ε)-approximation algorithm for the problem and the running time of our algorithm is Õ(nωlog3(nW/ε)/ε),1 where O(nω) is the time required for the classic n×n-matrix multiplication and W is the maximum value of the weights. With an additional O(log(nW/ε)) factor in space a cycle with approximately optimal weight can be computed within the same time bound."}],"date_published":"2014-08-28T00:00:00Z"},{"doi":"10.1371/journal.pcbi.1003818.s001","date_updated":"2023-02-23T10:25:37Z","user_id":"6785fbc1-c503-11eb-8a32-93094b40e1cf","related_material":{"record":[{"status":"public","relation":"used_in_publication","id":"2039"}]},"author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","first_name":"Andreas","full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis"},{"full_name":"Adlam, Ben","first_name":"Ben","last_name":"Adlam"},{"last_name":"Novak","full_name":"Novak, Martin","first_name":"Martin"}],"type":"research_data_reference","year":"2014","oa_version":"Published Version","day":"11","title":"Detailed proofs for “The time scale of evolutionary innovation”","citation":{"apa":"Chatterjee, K., Pavlogiannis, A., Adlam, B., &#38; Novak, M. (2014). Detailed proofs for “The time scale of evolutionary innovation.” Public Library of Science. <a href=\"https://doi.org/10.1371/journal.pcbi.1003818.s001\">https://doi.org/10.1371/journal.pcbi.1003818.s001</a>","ama":"Chatterjee K, Pavlogiannis A, Adlam B, Novak M. Detailed proofs for “The time scale of evolutionary innovation.” 2014. doi:<a href=\"https://doi.org/10.1371/journal.pcbi.1003818.s001\">10.1371/journal.pcbi.1003818.s001</a>","short":"K. Chatterjee, A. Pavlogiannis, B. Adlam, M. Novak, (2014).","mla":"Chatterjee, Krishnendu, et al. <i>Detailed Proofs for “The Time Scale of Evolutionary Innovation.”</i> Public Library of Science, 2014, doi:<a href=\"https://doi.org/10.1371/journal.pcbi.1003818.s001\">10.1371/journal.pcbi.1003818.s001</a>.","ieee":"K. Chatterjee, A. Pavlogiannis, B. Adlam, and M. Novak, “Detailed proofs for ‘The time scale of evolutionary innovation.’” Public Library of Science, 2014.","ista":"Chatterjee K, Pavlogiannis A, Adlam B, Novak M. 2014. Detailed proofs for “The time scale of evolutionary innovation”, Public Library of Science, <a href=\"https://doi.org/10.1371/journal.pcbi.1003818.s001\">10.1371/journal.pcbi.1003818.s001</a>.","chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, Ben Adlam, and Martin Novak. “Detailed Proofs for ‘The Time Scale of Evolutionary Innovation.’” Public Library of Science, 2014. <a href=\"https://doi.org/10.1371/journal.pcbi.1003818.s001\">https://doi.org/10.1371/journal.pcbi.1003818.s001</a>."},"status":"public","department":[{"_id":"KrCh"}],"publisher":"Public Library of Science","date_published":"2014-09-11T00:00:00Z","_id":"9739","date_created":"2021-07-28T08:13:57Z","month":"09","article_processing_charge":"No"},{"doi":"10.1007/978-3-642-39799-8_36","language":[{"iso":"eng"}],"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","name":"Game Theory","grant_number":"S11407"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"alternative_title":["LNCS"],"author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Jakub","full_name":"Ła̧Cki, Jakub","last_name":"Ła̧Cki"}],"type":"conference","day":"01","conference":{"location":"St. Petersburg, Russia","name":"CAV: Computer Aided Verification","start_date":"2013-07-13","end_date":"2013-07-19"},"title":"Faster algorithms for Markov decision processes with low treewidth","ec_funded":1,"citation":{"ama":"Chatterjee K, Ła̧Cki J. Faster algorithms for Markov decision processes with low treewidth. 2013;8044:543-558. doi:<a href=\"https://doi.org/10.1007/978-3-642-39799-8_36\">10.1007/978-3-642-39799-8_36</a>","apa":"Chatterjee, K., &#38; Ła̧Cki, J. (2013). Faster algorithms for Markov decision processes with low treewidth. Presented at the CAV: Computer Aided Verification, St. Petersburg, Russia: Springer. <a href=\"https://doi.org/10.1007/978-3-642-39799-8_36\">https://doi.org/10.1007/978-3-642-39799-8_36</a>","short":"K. Chatterjee, J. Ła̧Cki, 8044 (2013) 543–558.","mla":"Chatterjee, Krishnendu, and Jakub Ła̧Cki. <i>Faster Algorithms for Markov Decision Processes with Low Treewidth</i>. Vol. 8044, Springer, 2013, pp. 543–58, doi:<a href=\"https://doi.org/10.1007/978-3-642-39799-8_36\">10.1007/978-3-642-39799-8_36</a>.","chicago":"Chatterjee, Krishnendu, and Jakub Ła̧Cki. “Faster Algorithms for Markov Decision Processes with Low Treewidth.” Lecture Notes in Computer Science. Springer, 2013. <a href=\"https://doi.org/10.1007/978-3-642-39799-8_36\">https://doi.org/10.1007/978-3-642-39799-8_36</a>.","ista":"Chatterjee K, Ła̧Cki J. 2013. Faster algorithms for Markov decision processes with low treewidth. 8044, 543–558.","ieee":"K. Chatterjee and J. Ła̧Cki, “Faster algorithms for Markov decision processes with low treewidth,” vol. 8044. Springer, pp. 543–558, 2013."},"status":"public","intvolume":"      8044","department":[{"_id":"KrCh"}],"quality_controlled":"1","publisher":"Springer","date_created":"2018-12-11T11:57:42Z","series_title":"Lecture Notes in Computer Science","month":"07","page":"543 - 558","date_updated":"2020-08-11T10:09:47Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"external_id":{"arxiv":["1304.0084"]},"year":"2013","oa_version":"Preprint","publist_id":"4459","volume":8044,"oa":1,"main_file_link":[{"url":"http://arxiv.org/abs/1304.0084","open_access":"1"}],"publication_status":"published","date_published":"2013-07-01T00:00:00Z","_id":"2444","abstract":[{"lang":"eng","text":"We consider two core algorithmic problems for probabilistic verification: the maximal end-component decomposition and the almost-sure reachability set computation for Markov decision processes (MDPs). For MDPs with treewidth k, we present two improved static algorithms for both the problems that run in time O(n·k 2.38·2k ) and O(m·logn· k), respectively, where n is the number of states and m is the number of edges, significantly improving the previous known O(n·k·√n· k) bound for low treewidth. We also present decremental algorithms for both problems for MDPs with constant treewidth that run in amortized logarithmic time, which is a huge improvement over the previously known algorithms that require amortized linear time."}],"arxiv":1},{"arxiv":1,"date_published":"2013-07-01T00:00:00Z","_id":"2446","abstract":[{"text":"The model-checking problem for probabilistic systems crucially relies on the translation of LTL to deterministic Rabin automata (DRW). Our recent Safraless translation [KE12, GKE12] for the LTL(F,G) fragment produces smaller automata as compared to the traditional approach. In this work, instead of DRW we consider deterministic automata with acceptance condition given as disjunction of generalized Rabin pairs (DGRW). The Safraless translation of LTL(F,G) formulas to DGRW results in smaller automata as compared to DRW. We present algorithms for probabilistic model-checking as well as game solving for DGRW conditions. Our new algorithms lead to improvement both in terms of theoretical bounds as well as practical evaluation. We compare PRISM with and without our new translation, and show that the new translation leads to significant improvements.","lang":"eng"}],"main_file_link":[{"url":"http://arxiv.org/abs/1304.5281","open_access":"1"}],"oa":1,"publication_status":"published","volume":8044,"year":"2013","oa_version":"Preprint","publist_id":"4457","date_updated":"2020-08-11T10:09:47Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"external_id":{"arxiv":["1304.5281"]},"page":"559 - 575","date_created":"2018-12-11T11:57:42Z","series_title":"Lecture Notes in Computer Science","month":"07","publisher":"Springer","intvolume":"      8044","status":"public","department":[{"_id":"KrCh"}],"quality_controlled":"1","conference":{"location":"St. Petersburg, Russia","end_date":"2013-07-19","start_date":"2013-07-13","name":"CAV: Computer Aided Verification"},"title":"Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis","ec_funded":1,"citation":{"apa":"Chatterjee, K., Gaiser, A., &#38; Kretinsky, J. (2013). Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. Presented at the CAV: Computer Aided Verification, St. Petersburg, Russia: Springer. <a href=\"https://doi.org/10.1007/978-3-642-39799-8_37\">https://doi.org/10.1007/978-3-642-39799-8_37</a>","ama":"Chatterjee K, Gaiser A, Kretinsky J. Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. 2013;8044:559-575. doi:<a href=\"https://doi.org/10.1007/978-3-642-39799-8_37\">10.1007/978-3-642-39799-8_37</a>","short":"K. Chatterjee, A. Gaiser, J. Kretinsky, 8044 (2013) 559–575.","mla":"Chatterjee, Krishnendu, et al. <i>Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis</i>. Vol. 8044, Springer, 2013, pp. 559–75, doi:<a href=\"https://doi.org/10.1007/978-3-642-39799-8_37\">10.1007/978-3-642-39799-8_37</a>.","ieee":"K. Chatterjee, A. Gaiser, and J. Kretinsky, “Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis,” vol. 8044. Springer, pp. 559–575, 2013.","ista":"Chatterjee K, Gaiser A, Kretinsky J. 2013. Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. 8044, 559–575.","chicago":"Chatterjee, Krishnendu, Andreas Gaiser, and Jan Kretinsky. “Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis.” Lecture Notes in Computer Science. Springer, 2013. <a href=\"https://doi.org/10.1007/978-3-642-39799-8_37\">https://doi.org/10.1007/978-3-642-39799-8_37</a>."},"alternative_title":["LNCS"],"author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"full_name":"Gaiser, Andreas","first_name":"Andreas","last_name":"Gaiser"},{"full_name":"Kretinsky, Jan","first_name":"Jan","last_name":"Kretinsky","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"}],"type":"conference","day":"01","project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"doi":"10.1007/978-3-642-39799-8_37","language":[{"iso":"eng"}]},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T06:59:54Z","external_id":{"arxiv":["0804.4525"]},"scopus_import":1,"year":"2013","oa_version":"Preprint","publist_id":"4070","oa":1,"main_file_link":[{"url":"https://arxiv.org/abs/0804.4525","open_access":"1"}],"publication_status":"published","volume":24,"issue":"2","arxiv":1,"_id":"2814","abstract":[{"lang":"eng","text":"We study the problem of generating a test sequence that achieves maximal coverage for a reactive system under test. We formulate the problem as a repeated game between the tester and the system, where the system state space is partitioned according to some coverage criterion and the objective of the tester is to maximize the set of partitions (or coverage goals) visited during the game. We show the complexity of the maximal coverage problem for non-deterministic systems is PSPACE-complete, but is NP-complete for deterministic systems. For the special case of non-deterministic systems with a re-initializing &quot;reset&quot; action, which represent running a new test input on a re-initialized system, we show that the complexity is coNP-complete. Our proof technique for reset games uses randomized testing strategies that circumvent the exponentially large memory requirement of deterministic testing strategies. We also discuss the memory requirement for deterministic strategies and extensions of our results to other models, such as pushdown systems and timed systems."}],"date_published":"2013-02-01T00:00:00Z","project":[{"name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"doi":"10.1142/S0129054113400066","language":[{"iso":"eng"}],"title":"The complexity of coverage","ec_funded":1,"citation":{"ista":"Chatterjee K, Alfaro L, Majumdar R. 2013. The complexity of coverage. International Journal of Foundations of Computer Science. 24(2), 165–185.","ieee":"K. Chatterjee, L. Alfaro, and R. Majumdar, “The complexity of coverage,” <i>International Journal of Foundations of Computer Science</i>, vol. 24, no. 2. World Scientific Publishing, pp. 165–185, 2013.","chicago":"Chatterjee, Krishnendu, Luca Alfaro, and Ritankar Majumdar. “The Complexity of Coverage.” <i>International Journal of Foundations of Computer Science</i>. World Scientific Publishing, 2013. <a href=\"https://doi.org/10.1142/S0129054113400066\">https://doi.org/10.1142/S0129054113400066</a>.","mla":"Chatterjee, Krishnendu, et al. “The Complexity of Coverage.” <i>International Journal of Foundations of Computer Science</i>, vol. 24, no. 2, World Scientific Publishing, 2013, pp. 165–85, doi:<a href=\"https://doi.org/10.1142/S0129054113400066\">10.1142/S0129054113400066</a>.","short":"K. Chatterjee, L. Alfaro, R. Majumdar, International Journal of Foundations of Computer Science 24 (2013) 165–185.","apa":"Chatterjee, K., Alfaro, L., &#38; Majumdar, R. (2013). The complexity of coverage. <i>International Journal of Foundations of Computer Science</i>. World Scientific Publishing. <a href=\"https://doi.org/10.1142/S0129054113400066\">https://doi.org/10.1142/S0129054113400066</a>","ama":"Chatterjee K, Alfaro L, Majumdar R. The complexity of coverage. <i>International Journal of Foundations of Computer Science</i>. 2013;24(2):165-185. doi:<a href=\"https://doi.org/10.1142/S0129054113400066\">10.1142/S0129054113400066</a>"},"type":"journal_article","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"},{"first_name":"Luca","full_name":"Alfaro, Luca","last_name":"Alfaro"},{"first_name":"Ritankar","full_name":"Majumdar, Ritankar","last_name":"Majumdar"}],"day":"01","publisher":"World Scientific Publishing","intvolume":"        24","status":"public","quality_controlled":"1","department":[{"_id":"KrCh"}],"publication":"International Journal of Foundations of Computer Science","page":"165 - 185","date_created":"2018-12-11T11:59:44Z","month":"02"},{"related_material":{"record":[{"id":"1400","relation":"dissertation_contains","status":"public"}]},"ddc":["570","610"],"doi":"10.7554/eLife.00747","language":[{"iso":"eng"}],"title":"Evolutionary dynamics of cancer in response to targeted combination therapy","citation":{"ieee":"I. Božić <i>et al.</i>, “Evolutionary dynamics of cancer in response to targeted combination therapy,” <i>eLife</i>, vol. 2. eLife Sciences Publications, 2013.","ista":"Božić I, Reiter J, Allen B, Antal T, Chatterjee K, Shah P, Moon Y, Yaqubie A, Kelly N, Le D, Lipson E, Chapman P, Diaz L, Vogelstein B, Nowak M. 2013. Evolutionary dynamics of cancer in response to targeted combination therapy. eLife. 2, e00747.","chicago":"Božić, Ivana, Johannes Reiter, Benjamin Allen, Tibor Antal, Krishnendu Chatterjee, Preya Shah, Yo Moon, et al. “Evolutionary Dynamics of Cancer in Response to Targeted Combination Therapy.” <i>ELife</i>. eLife Sciences Publications, 2013. <a href=\"https://doi.org/10.7554/eLife.00747\">https://doi.org/10.7554/eLife.00747</a>.","mla":"Božić, Ivana, et al. “Evolutionary Dynamics of Cancer in Response to Targeted Combination Therapy.” <i>ELife</i>, vol. 2, e00747, eLife Sciences Publications, 2013, doi:<a href=\"https://doi.org/10.7554/eLife.00747\">10.7554/eLife.00747</a>.","short":"I. Božić, J. Reiter, B. Allen, T. Antal, K. Chatterjee, P. Shah, Y. Moon, A. Yaqubie, N. Kelly, D. Le, E. Lipson, P. Chapman, L. Diaz, B. Vogelstein, M. Nowak, ELife 2 (2013).","apa":"Božić, I., Reiter, J., Allen, B., Antal, T., Chatterjee, K., Shah, P., … Nowak, M. (2013). Evolutionary dynamics of cancer in response to targeted combination therapy. <i>ELife</i>. eLife Sciences Publications. <a href=\"https://doi.org/10.7554/eLife.00747\">https://doi.org/10.7554/eLife.00747</a>","ama":"Božić I, Reiter J, Allen B, et al. Evolutionary dynamics of cancer in response to targeted combination therapy. <i>eLife</i>. 2013;2. doi:<a href=\"https://doi.org/10.7554/eLife.00747\">10.7554/eLife.00747</a>"},"author":[{"full_name":"Božić, Ivana","first_name":"Ivana","last_name":"Božić"},{"id":"4A918E98-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0170-7353","last_name":"Reiter","full_name":"Reiter, Johannes","first_name":"Johannes"},{"first_name":"Benjamin","full_name":"Allen, Benjamin","last_name":"Allen"},{"full_name":"Antal, Tibor","first_name":"Tibor","last_name":"Antal"},{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Shah, Preya","first_name":"Preya","last_name":"Shah"},{"full_name":"Moon, Yo","first_name":"Yo","last_name":"Moon"},{"first_name":"Amin","full_name":"Yaqubie, Amin","last_name":"Yaqubie"},{"full_name":"Kelly, Nicole","first_name":"Nicole","last_name":"Kelly"},{"last_name":"Le","full_name":"Le, Dung","first_name":"Dung"},{"last_name":"Lipson","first_name":"Evan","full_name":"Lipson, Evan"},{"last_name":"Chapman","first_name":"Paul","full_name":"Chapman, Paul"},{"first_name":"Luis","full_name":"Diaz, Luis","last_name":"Diaz"},{"full_name":"Vogelstein, Bert","first_name":"Bert","last_name":"Vogelstein"},{"full_name":"Nowak, Martin","first_name":"Martin","last_name":"Nowak"}],"type":"journal_article","day":"25","publisher":"eLife Sciences Publications","status":"public","intvolume":"         2","publication":"eLife","quality_controlled":"1","department":[{"_id":"KrCh"}],"date_created":"2018-12-11T11:59:45Z","month":"06","scopus_import":1,"date_updated":"2023-09-07T11:40:43Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Published Version","year":"2013","has_accepted_license":"1","publist_id":"3985","oa":1,"publication_status":"published","pubrep_id":"134","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"volume":2,"file_date_updated":"2020-07-14T12:45:49Z","abstract":[{"text":"In solid tumors, targeted treatments can lead to dramatic regressions, but responses are often short-lived because resistant cancer cells arise. The major strategy proposed for overcoming resistance is combination therapy. We present a mathematical model describing the evolutionary dynamics of lesions in response to treatment. We first studied 20 melanoma patients receiving vemurafenib. We then applied our model to an independent set of pancreatic, colorectal, and melanoma cancer patients with metastatic disease. We find that dual therapy results in long-term disease control for most patients, if there are no single mutations that cause cross-resistance to both drugs; in patients with large disease burden, triple therapy is needed. We also find that simultaneous therapy with two drugs is much more effective than sequential therapy. Our results provide realistic expectations for the efficacy of new drug combinations and inform the design of trials for new cancer therapeutics.","lang":"eng"}],"_id":"2816","date_published":"2013-06-25T00:00:00Z","file":[{"date_updated":"2020-07-14T12:45:49Z","access_level":"open_access","checksum":"2c38c47815eacd8fa66cb8b404cf7c61","file_name":"IST-2013-134-v1+1_e00747.full.pdf","creator":"system","file_size":3358321,"date_created":"2018-12-12T10:12:48Z","content_type":"application/pdf","file_id":"4967","relation":"main_file"}],"article_number":"e00747"},{"publisher":"Elsevier","intvolume":"       334","status":"public","publication":"Journal of Theoretical Biology","quality_controlled":"1","department":[{"_id":"NiBa"},{"_id":"KrCh"}],"page":"26 - 34","date_created":"2018-12-11T11:59:45Z","month":"10","project":[{"call_identifier":"FP7","_id":"25B07788-B435-11E9-9278-68D0E5697425","name":"Limits to selection in biology and in evolutionary computation","grant_number":"250152"},{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"doi":"10.1016/j.jtbi.2013.05.029","ddc":["000"],"language":[{"iso":"eng"}],"title":"Density games","citation":{"mla":"Novak, Sebastian, et al. “Density Games.” <i>Journal of Theoretical Biology</i>, vol. 334, Elsevier, 2013, pp. 26–34, doi:<a href=\"https://doi.org/10.1016/j.jtbi.2013.05.029\">10.1016/j.jtbi.2013.05.029</a>.","chicago":"Novak, Sebastian, Krishnendu Chatterjee, and Martin Nowak. “Density Games.” <i>Journal of Theoretical Biology</i>. Elsevier, 2013. <a href=\"https://doi.org/10.1016/j.jtbi.2013.05.029\">https://doi.org/10.1016/j.jtbi.2013.05.029</a>.","ista":"Novak S, Chatterjee K, Nowak M. 2013. Density games. Journal of Theoretical Biology. 334, 26–34.","ieee":"S. Novak, K. Chatterjee, and M. Nowak, “Density games,” <i>Journal of Theoretical Biology</i>, vol. 334. Elsevier, pp. 26–34, 2013.","ama":"Novak S, Chatterjee K, Nowak M. Density games. <i>Journal of Theoretical Biology</i>. 2013;334:26-34. doi:<a href=\"https://doi.org/10.1016/j.jtbi.2013.05.029\">10.1016/j.jtbi.2013.05.029</a>","apa":"Novak, S., Chatterjee, K., &#38; Nowak, M. (2013). Density games. <i>Journal of Theoretical Biology</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.jtbi.2013.05.029\">https://doi.org/10.1016/j.jtbi.2013.05.029</a>","short":"S. Novak, K. Chatterjee, M. Nowak, Journal of Theoretical Biology 334 (2013) 26–34."},"ec_funded":1,"author":[{"orcid":"0000-0002-2519-824X","id":"461468AE-F248-11E8-B48F-1D18A9856A87","first_name":"Sebastian","full_name":"Novak, Sebastian","last_name":"Novak"},{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Martin","full_name":"Nowak, Martin","last_name":"Nowak"}],"type":"journal_article","day":"07","oa":1,"publication_status":"published","pubrep_id":"400","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"volume":334,"file_date_updated":"2020-07-14T12:45:49Z","abstract":[{"lang":"eng","text":"The basic idea of evolutionary game theory is that payoff determines reproductive rate. Successful individuals have a higher payoff and produce more offspring. But in evolutionary and ecological situations there is not only reproductive rate but also carrying capacity. Individuals may differ in their exposure to density limiting effects. Here we explore an alternative approach to evolutionary game theory by assuming that the payoff from the game determines the carrying capacity of individual phenotypes. Successful strategies are less affected by density limitation (crowding) and reach higher equilibrium abundance. We demonstrate similarities and differences between our framework and the standard replicator equation. Our equation is defined on the positive orthant, instead of the simplex, but has the same equilibrium points as the replicator equation. Linear stability analysis produces the classical conditions for asymptotic stability of pure strategies, but the stability properties of internal equilibria can differ in the two frameworks. For example, in a two-strategy game with an internal equilibrium that is always stable under the replicator equation, the corresponding equilibrium can be unstable in the new framework resulting in a limit cycle."}],"_id":"2817","date_published":"2013-10-07T00:00:00Z","file":[{"checksum":"3c29059ab03a4b8f97a07646b817ddbb","date_updated":"2020-07-14T12:45:49Z","access_level":"open_access","file_name":"IST-2016-400-v1+1_1-s2.0-S0022519313002609-main.pdf","creator":"system","file_size":834604,"date_created":"2018-12-12T10:14:54Z","content_type":"application/pdf","relation":"main_file","file_id":"5110"}],"scopus_import":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2025-05-28T11:42:43Z","has_accepted_license":"1","year":"2013","oa_version":"Published Version","publist_id":"3984"},{"volume":1,"oa":1,"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1212.6556"}],"publication_status":"published","_id":"2819","date_published":"2013-04-01T00:00:00Z","abstract":[{"text":"We introduce quantatitive timed refinement metrics and quantitative timed simulation functions, incorporating zenoness checks, for timed systems. These functions assign positive real numbers between zero and infinity which quantify the timing mismatches between two timed systems, amongst non-zeno runs. We quantify timing mismatches in three ways: (1) the maximum timing mismatch that can arise, (2) the &quot;steady-state&quot; maximum timing mismatches, where initial transient timing mismatches are ignored; and (3) the (long-run) average timing mismatches amongst two systems. These three kinds of mismatches constitute three important types of timing differences. Our event times are the global times, measured from the start of the system execution, not just the time durations of individual steps. We present algorithms over timed automata for computing the three quantitative simulation functions to within any desired degree of accuracy. In order to compute the values of the quantitative simulation functions, we use a game theoretic formulation. We introduce two new kinds of objectives for two player games on finite state game graphs: (1) eventual debit-sum level objectives, and (2) average debit-sum level objectives. We present algorithms for computing the optimal values for these objectives for player 1, and then use these algorithms to compute the values of the quantitative timed simulation functions. ","lang":"eng"}],"date_updated":"2021-01-12T06:59:56Z","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","scopus_import":1,"year":"2013","oa_version":"Preprint","publist_id":"3982","status":"public","intvolume":"         1","department":[{"_id":"KrCh"}],"quality_controlled":"1","publication":"Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control","publisher":"Springer","date_created":"2018-12-11T11:59:46Z","month":"04","page":"273 - 282","doi":"10.1145/2461328.2461370","language":[{"iso":"eng"}],"acknowledgement":"This work has been financially supported in part by the European Commission FP7-ICT Cognitive Systems, Interaction, and Robotics under the contract # 270180 (NOP-TILUS); by Fundacao para Ciencia e Tecnologia under project PTDC/EEA-CRO/104901/2008 (Modeling and control of Networked vehicle systems in persistent autonomous operations); by Austrian Science Fund (FWF) Grant No P 23499-N23 on Modern Graph Algorithmic Techniques in Formal Verification; FWF NFN Grant No S11407-N23 (RiSE); ERC Start grant (279307: Graph Games); and the Microsoft faculty fellows award","project":[{"name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"author":[{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"first_name":"Vinayak","full_name":"Prabhu, Vinayak","last_name":"Prabhu"}],"type":"conference","day":"01","conference":{"location":"Philadelphia, PA USA","name":"HSCC: Hybrid Systems - Computation and Control","end_date":"2013-04-11","start_date":"2013-04-08"},"title":"Quantitative timed simulation functions and refinement metrics for real-time systems","ec_funded":1,"citation":{"chicago":"Chatterjee, Krishnendu, and Vinayak Prabhu. “Quantitative Timed Simulation Functions and Refinement Metrics for Real-Time Systems.” In <i>Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control</i>, 1:273–82. Springer, 2013. <a href=\"https://doi.org/10.1145/2461328.2461370\">https://doi.org/10.1145/2461328.2461370</a>.","ista":"Chatterjee K, Prabhu V. 2013. Quantitative timed simulation functions and refinement metrics for real-time systems. Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems - Computation and Control vol. 1, 273–282.","ieee":"K. Chatterjee and V. Prabhu, “Quantitative timed simulation functions and refinement metrics for real-time systems,” in <i>Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control</i>, Philadelphia, PA USA, 2013, vol. 1, pp. 273–282.","mla":"Chatterjee, Krishnendu, and Vinayak Prabhu. “Quantitative Timed Simulation Functions and Refinement Metrics for Real-Time Systems.” <i>Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control</i>, vol. 1, Springer, 2013, pp. 273–82, doi:<a href=\"https://doi.org/10.1145/2461328.2461370\">10.1145/2461328.2461370</a>.","short":"K. Chatterjee, V. Prabhu, in:, Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, Springer, 2013, pp. 273–282.","ama":"Chatterjee K, Prabhu V. Quantitative timed simulation functions and refinement metrics for real-time systems. In: <i>Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control</i>. Vol 1. Springer; 2013:273-282. doi:<a href=\"https://doi.org/10.1145/2461328.2461370\">10.1145/2461328.2461370</a>","apa":"Chatterjee, K., &#38; Prabhu, V. (2013). Quantitative timed simulation functions and refinement metrics for real-time systems. In <i>Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control</i> (Vol. 1, pp. 273–282). Philadelphia, PA USA: Springer. <a href=\"https://doi.org/10.1145/2461328.2461370\">https://doi.org/10.1145/2461328.2461370</a>"}},{"publication":"Proceedings of the 16th International conference on Hybrid systems: Computation and control","department":[{"_id":"KrCh"}],"quality_controlled":"1","status":"public","publication_status":"published","publisher":"ACM","month":"04","date_published":"2013-04-01T00:00:00Z","_id":"2820","date_created":"2018-12-11T11:59:46Z","abstract":[{"lang":"eng","text":"In this paper, we introduce the powerful framework of graph games for the analysis of real-time scheduling with firm deadlines. We introduce a novel instance of a partial-observation game that is suitable for this purpose, and prove decidability of all the involved decision problems. We derive a graph game that allows the automated computation of the competitive ratio (along with an optimal witness algorithm for the competitive ratio) and establish an NP-completeness proof for the graph game problem. For a given on-line algorithm, we present polynomial time solution for computing (i) the worst-case utility; (ii) the worst-case utility ratio w.r.t. a clairvoyant off-line algorithm; and (iii) the competitive ratio. A major strength of the proposed approach lies in its flexibility w.r.t. incorporating additional constraints on the adversary and/or the algorithm, including limited maximum or average load, finiteness of periods of overload, etc., which are easily added by means of additional instances of standard objective functions for graph games. "}],"page":"163 - 172","scopus_import":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2023-09-27T12:52:38Z","language":[{"iso":"eng"}],"publication_identifier":{"isbn":["978-1-4503-1567-8 "]},"doi":"10.1145/2461328.2461356","project":[{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Microsoft Research Faculty Fellowship","_id":"2587B514-B435-11E9-9278-68D0E5697425"}],"related_material":{"record":[{"id":"738","relation":"later_version","status":"public"}]},"day":"01","publist_id":"3981","type":"conference","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Kößler","full_name":"Kößler, Alexander","first_name":"Alexander"},{"full_name":"Schmid, Ulrich","first_name":"Ulrich","last_name":"Schmid"}],"year":"2013","oa_version":"None","citation":{"mla":"Chatterjee, Krishnendu, et al. “Automated Analysis of Real-Time Scheduling Using Graph Games.” <i>Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control</i>, ACM, 2013, pp. 163–72, doi:<a href=\"https://doi.org/10.1145/2461328.2461356\">10.1145/2461328.2461356</a>.","ista":"Chatterjee K, Kößler A, Schmid U. 2013. Automated analysis of real-time scheduling using graph games. Proceedings of the 16th International conference on Hybrid systems: Computation and control. HSCC: Hybrid Systems - Computation and Control, 163–172.","ieee":"K. Chatterjee, A. Kößler, and U. Schmid, “Automated analysis of real-time scheduling using graph games,” in <i>Proceedings of the 16th International conference on Hybrid systems: Computation and control</i>, Philadelphia, PA, United States, 2013, pp. 163–172.","chicago":"Chatterjee, Krishnendu, Alexander Kößler, and Ulrich Schmid. “Automated Analysis of Real-Time Scheduling Using Graph Games.” In <i>Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control</i>, 163–72. ACM, 2013. <a href=\"https://doi.org/10.1145/2461328.2461356\">https://doi.org/10.1145/2461328.2461356</a>.","apa":"Chatterjee, K., Kößler, A., &#38; Schmid, U. (2013). Automated analysis of real-time scheduling using graph games. In <i>Proceedings of the 16th International conference on Hybrid systems: Computation and control</i> (pp. 163–172). Philadelphia, PA, United States: ACM. <a href=\"https://doi.org/10.1145/2461328.2461356\">https://doi.org/10.1145/2461328.2461356</a>","ama":"Chatterjee K, Kößler A, Schmid U. Automated analysis of real-time scheduling using graph games. In: <i>Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control</i>. ACM; 2013:163-172. doi:<a href=\"https://doi.org/10.1145/2461328.2461356\">10.1145/2461328.2461356</a>","short":"K. Chatterjee, A. Kößler, U. Schmid, in:, Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, ACM, 2013, pp. 163–172."},"ec_funded":1,"title":"Automated analysis of real-time scheduling using graph games","conference":{"end_date":"2013-04-11","start_date":"2013-04-08","name":"HSCC: Hybrid Systems - Computation and Control","location":"Philadelphia, PA, United States"}},{"citation":{"mla":"Chatterjee, Krishnendu, and Vinayak Prabhu. “Synthesis of Memory-Efficient, Clock-Memory Free, and Non-Zeno Safety Controllers for Timed Systems.” <i>Information and Computation</i>, vol. 228–229, Elsevier, 2013, pp. 83–119, doi:<a href=\"https://doi.org/10.1016/j.ic.2013.04.003\">10.1016/j.ic.2013.04.003</a>.","chicago":"Chatterjee, Krishnendu, and Vinayak Prabhu. “Synthesis of Memory-Efficient, Clock-Memory Free, and Non-Zeno Safety Controllers for Timed Systems.” <i>Information and Computation</i>. Elsevier, 2013. <a href=\"https://doi.org/10.1016/j.ic.2013.04.003\">https://doi.org/10.1016/j.ic.2013.04.003</a>.","ista":"Chatterjee K, Prabhu V. 2013. Synthesis of memory-efficient, clock-memory free, and non-Zeno safety controllers for timed systems. Information and Computation. 228–229, 83–119.","ieee":"K. Chatterjee and V. Prabhu, “Synthesis of memory-efficient, clock-memory free, and non-Zeno safety controllers for timed systems,” <i>Information and Computation</i>, vol. 228–229. Elsevier, pp. 83–119, 2013.","ama":"Chatterjee K, Prabhu V. Synthesis of memory-efficient, clock-memory free, and non-Zeno safety controllers for timed systems. <i>Information and Computation</i>. 2013;228-229:83-119. doi:<a href=\"https://doi.org/10.1016/j.ic.2013.04.003\">10.1016/j.ic.2013.04.003</a>","apa":"Chatterjee, K., &#38; Prabhu, V. (2013). Synthesis of memory-efficient, clock-memory free, and non-Zeno safety controllers for timed systems. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.ic.2013.04.003\">https://doi.org/10.1016/j.ic.2013.04.003</a>","short":"K. Chatterjee, V. Prabhu, Information and Computation 228–229 (2013) 83–119."},"ec_funded":1,"title":"Synthesis of memory-efficient, clock-memory free, and non-Zeno safety controllers for timed systems","day":"24","publist_id":"3977","author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Prabhu, Vinayak","first_name":"Vinayak","last_name":"Prabhu"}],"type":"journal_article","oa_version":"None","year":"2013","project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"scopus_import":1,"date_updated":"2021-01-12T06:59:58Z","language":[{"iso":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","doi":"10.1016/j.ic.2013.04.003","page":"83-119","month":"04","_id":"2824","date_created":"2018-12-11T11:59:47Z","date_published":"2013-04-24T00:00:00Z","abstract":[{"text":"We study synthesis of controllers for real-time systems, where the objective is to stay in a given safe set. The problem is solved by obtaining winning strategies in the setting of concurrent two player timed automaton games with safety objectives. To prevent a player from winning by blocking time, we restrict each player to strategies that ensure that the player cannot be responsible for causing a Zeno run. We construct winning strategies for the controller which require access only to (1) the system clocks (thus, controllers which require their own internal infinitely precise clocks are not necessary), and (2) a logarithmic (in the number of clocks) number of memory bits (i.e. a linear number of memory states). Precisely, we show that for safety objectives, a memory of size (3 + lg (| C | + 1)) bits suffices for winning controller strategies, where C is the set of clocks of the timed automaton game, significantly improving the previous known exponential memory states bound. We also settle the open question of whether winning region-based strategies require memory for safety objectives by showing with an example the necessity of memory for such strategies to win for safety objectives. Finally, we show that the decision problem of determining if there exists a receptive player-1 winning strategy for safety objectives is EXPTIME-complete over timed automaton games.","lang":"eng"}],"publisher":"Elsevier","publication_status":"published","publication":"Information and Computation","department":[{"_id":"KrCh"}],"quality_controlled":"1","status":"public","volume":"228-229"}]