[{"doi":"10.15479/AT:IST-2014-187-v1-1","date_published":"2014-04-14T00:00:00Z","language":[{"iso":"eng"}],"oa":1,"citation":{"apa":"Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2014). Improved algorithms for reachability and shortest path on low tree-width graphs. IST Austria. https://doi.org/10.15479/AT:IST-2014-187-v1-1","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, Improved algorithms for reachability and shortest path on low tree-width graphs. IST Austria, 2014.","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2014. Improved algorithms for reachability and shortest path on low tree-width graphs, IST Austria, 34p.","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Improved Algorithms for Reachability and Shortest Path on Low Tree-Width Graphs. IST Austria; 2014. doi:10.15479/AT:IST-2014-187-v1-1","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. Improved Algorithms for Reachability and Shortest Path on Low Tree-Width Graphs. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-187-v1-1.","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. Improved Algorithms for Reachability and Shortest Path on Low Tree-Width Graphs. IST Austria, 2014, doi:10.15479/AT:IST-2014-187-v1-1."},"page":"34","publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1","month":"04","day":"14","pubrep_id":"187","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"first_name":"Rasmus","last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389","full_name":"Ibsen-Jensen, Rasmus"},{"full_name":"Pavlogiannis, Andreas","first_name":"Andreas","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722"}],"file":[{"access_level":"open_access","file_name":"IST-2014-187-v1+1_main_full_tech.pdf","content_type":"application/pdf","file_size":670031,"creator":"system","relation":"main_file","file_id":"5548","checksum":"c608e66030a4bf51d2d99b451f539b99","date_updated":"2020-07-14T12:46:50Z","date_created":"2018-12-12T11:54:25Z"}],"oa_version":"Published Version","date_updated":"2021-01-12T08:02:03Z","date_created":"2018-12-12T11:39:13Z","_id":"5419","year":"2014","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"IST Austria","department":[{"_id":"KrCh"}],"title":"Improved algorithms for reachability and shortest path on low tree-width graphs","ddc":["000"],"status":"public","publication_status":"published","file_date_updated":"2020-07-14T12:46:50Z","abstract":[{"lang":"eng","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."}],"type":"technical_report","alternative_title":["IST Austria Technical Report"]},{"author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu"},{"full_name":"Doyen, Laurent","last_name":"Doyen","first_name":"Laurent"}],"related_material":{"record":[{"status":"public","relation":"later_version","id":"2163"}]},"pubrep_id":"176","date_updated":"2023-02-23T10:30:58Z","date_created":"2018-12-12T11:39:13Z","file":[{"date_updated":"2020-07-14T12:46:49Z","date_created":"2018-12-12T11:53:07Z","checksum":"1d6958aa60050e1c3e932c6e5f34c39f","relation":"main_file","file_id":"5468","content_type":"application/pdf","file_size":328253,"creator":"system","file_name":"IST-2014-176-v1+1_icalp_14.pdf","access_level":"open_access"}],"oa_version":"Published Version","_id":"5418","year":"2014","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Games with a weak adversary","publication_status":"published","ddc":["000","005"],"status":"public","department":[{"_id":"KrCh"}],"publisher":"IST Austria","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_updated":"2020-07-14T12:46:49Z","type":"technical_report","alternative_title":["IST Austria Technical Report"],"date_published":"2014-03-22T00:00:00Z","doi":"10.15479/AT:IST-2014-176-v1-1","language":[{"iso":"eng"}],"citation":{"chicago":"Chatterjee, Krishnendu, and Laurent Doyen. Games with a Weak Adversary. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-176-v1-1.","mla":"Chatterjee, Krishnendu, and Laurent Doyen. Games with a Weak Adversary. IST Austria, 2014, doi:10.15479/AT:IST-2014-176-v1-1.","short":"K. Chatterjee, L. Doyen, Games with a Weak Adversary, IST Austria, 2014.","ista":"Chatterjee K, Doyen L. 2014. Games with a weak adversary, IST Austria, 18p.","apa":"Chatterjee, K., & Doyen, L. (2014). Games with a weak adversary. IST Austria. https://doi.org/10.15479/AT:IST-2014-176-v1-1","ieee":"K. Chatterjee and L. Doyen, Games with a weak adversary. IST Austria, 2014.","ama":"Chatterjee K, Doyen L. Games with a Weak Adversary. IST Austria; 2014. doi:10.15479/AT:IST-2014-176-v1-1"},"oa":1,"page":"18","day":"22","month":"03","publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1"},{"file_date_updated":"2020-07-14T12:46:50Z","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"}],"type":"technical_report","alternative_title":["IST Austria Technical Report"],"author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Ibsen-Jensen, Rasmus","last_name":"Ibsen-Jensen","first_name":"Rasmus","orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87"}],"pubrep_id":"191","date_created":"2018-12-12T11:39:14Z","date_updated":"2021-01-12T08:02:05Z","file":[{"access_level":"open_access","file_name":"IST-2014-191-v1+1_main_full.pdf","content_type":"application/pdf","file_size":584368,"creator":"system","relation":"main_file","file_id":"5520","checksum":"49e0fd3e62650346daf7dc04604f7a0a","date_created":"2018-12-12T11:53:58Z","date_updated":"2020-07-14T12:46:50Z"}],"oa_version":"Published Version","year":"2014","_id":"5420","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000","005"],"status":"public","title":"The value 1 problem for concurrent mean-payoff games","publication_status":"published","publisher":"IST Austria","department":[{"_id":"KrCh"}],"month":"04","day":"14","publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1","doi":"10.15479/AT:IST-2014-191-v1-1","date_published":"2014-04-14T00:00:00Z","language":[{"iso":"eng"}],"oa":1,"citation":{"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, The value 1 problem for concurrent mean-payoff games. IST Austria, 2014.","apa":"Chatterjee, K., & Ibsen-Jensen, R. (2014). The value 1 problem for concurrent mean-payoff games. IST Austria. https://doi.org/10.15479/AT:IST-2014-191-v1-1","ama":"Chatterjee K, Ibsen-Jensen R. The Value 1 Problem for Concurrent Mean-Payoff Games. IST Austria; 2014. doi:10.15479/AT:IST-2014-191-v1-1","chicago":"Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. The Value 1 Problem for Concurrent Mean-Payoff Games. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-191-v1-1.","mla":"Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. The Value 1 Problem for Concurrent Mean-Payoff Games. IST Austria, 2014, doi:10.15479/AT:IST-2014-191-v1-1.","short":"K. Chatterjee, R. Ibsen-Jensen, The Value 1 Problem for Concurrent Mean-Payoff Games, IST Austria, 2014."},"page":"49"},{"file_date_updated":"2020-07-14T12:46:51Z","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"}],"type":"technical_report","alternative_title":["IST Austria Technical Report"],"related_material":{"record":[{"relation":"later_version","status":"public","id":"1732"},{"status":"public","relation":"later_version","id":"5426"}]},"pubrep_id":"305","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu"},{"first_name":"Martin","last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87","full_name":"Chmelik, Martin"},{"last_name":"Gupta","first_name":"Raghav","full_name":"Gupta, Raghav"},{"first_name":"Ayush","last_name":"Kanodia","full_name":"Kanodia, Ayush"}],"oa_version":"Published Version","file":[{"file_size":655774,"content_type":"application/pdf","creator":"system","access_level":"open_access","file_name":"IST-2014-305-v1+1_main.pdf","checksum":"35009d5fad01198341e6c1a3353481b7","date_created":"2018-12-12T11:53:51Z","date_updated":"2020-07-14T12:46:51Z","relation":"main_file","file_id":"5512"}],"date_created":"2018-12-12T11:39:15Z","date_updated":"2023-02-23T12:25:52Z","year":"2014","_id":"5424","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"IST Austria","department":[{"_id":"KrCh"}],"ddc":["005"],"publication_status":"published","status":"public","title":"Qualitative analysis of POMDPs with temporal logic specifications for robotics applications","has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"month":"09","day":"09","doi":"10.15479/AT:IST-2014-305-v1-1","date_published":"2014-09-09T00:00:00Z","language":[{"iso":"eng"}],"oa":1,"citation":{"chicago":"Chatterjee, Krishnendu, Martin Chmelik, Raghav Gupta, and Ayush Kanodia. Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-305-v1-1.","mla":"Chatterjee, Krishnendu, et al. Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications. IST Austria, 2014, doi:10.15479/AT:IST-2014-305-v1-1.","short":"K. Chatterjee, M. Chmelik, R. Gupta, A. Kanodia, Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications, 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, 12p.","ieee":"K. Chatterjee, M. Chmelik, R. Gupta, and A. Kanodia, Qualitative analysis of POMDPs with temporal logic specifications for robotics applications. IST Austria, 2014.","apa":"Chatterjee, K., Chmelik, M., Gupta, R., & Kanodia, A. (2014). Qualitative analysis of POMDPs with temporal logic specifications for robotics applications. IST Austria. https://doi.org/10.15479/AT:IST-2014-305-v1-1","ama":"Chatterjee K, Chmelik M, Gupta R, Kanodia A. Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications. IST Austria; 2014. doi:10.15479/AT:IST-2014-305-v1-1"},"page":"12"},{"doi":"10.15479/AT:IST-2014-305-v2-1","date_published":"2014-09-29T00:00:00Z","language":[{"iso":"eng"}],"oa":1,"citation":{"short":"K. Chatterjee, M. Chmelik, R. Gupta, A. Kanodia, Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications, IST Austria, 2014.","mla":"Chatterjee, Krishnendu, et al. Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications. IST Austria, 2014, doi:10.15479/AT:IST-2014-305-v2-1.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, Raghav Gupta, and Ayush Kanodia. Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-305-v2-1.","ama":"Chatterjee K, Chmelik M, Gupta R, Kanodia A. Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications. IST Austria; 2014. doi:10.15479/AT:IST-2014-305-v2-1","ieee":"K. Chatterjee, M. Chmelik, R. Gupta, and A. Kanodia, Qualitative analysis of POMDPs with temporal logic specifications for robotics applications. IST Austria, 2014.","apa":"Chatterjee, K., Chmelik, M., Gupta, R., & Kanodia, A. (2014). Qualitative analysis of POMDPs with temporal logic specifications for robotics applications. IST Austria. https://doi.org/10.15479/AT:IST-2014-305-v2-1","ista":"Chatterjee K, Chmelik M, Gupta R, Kanodia A. 2014. Qualitative analysis of POMDPs with temporal logic specifications for robotics applications, IST Austria, 10p."},"page":"10","month":"09","day":"29","has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"author":[{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu"},{"full_name":"Chmelik, Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik","first_name":"Martin"},{"full_name":"Gupta, Raghav","last_name":"Gupta","first_name":"Raghav"},{"full_name":"Kanodia, Ayush","last_name":"Kanodia","first_name":"Ayush"}],"related_material":{"record":[{"status":"public","relation":"later_version","id":"1732"},{"id":"5424","relation":"earlier_version","status":"public"}]},"pubrep_id":"311","date_updated":"2023-02-23T12:25:47Z","date_created":"2018-12-12T11:39:16Z","file":[{"file_name":"IST-2014-305-v2+1_main2.pdf","access_level":"open_access","creator":"system","content_type":"application/pdf","file_size":656019,"file_id":"5537","relation":"main_file","date_created":"2018-12-12T11:54:15Z","date_updated":"2020-07-14T12:46:51Z","checksum":"730c0a8e97cf2712a884b2cc423f3919"}],"oa_version":"Published Version","_id":"5426","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2014","ddc":["005"],"title":"Qualitative analysis of POMDPs with temporal logic specifications for robotics applications","publication_status":"published","status":"public","department":[{"_id":"KrCh"}],"publisher":"IST Austria","file_date_updated":"2020-07-14T12:46:51Z","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"}],"type":"technical_report","alternative_title":["IST Austria Technical Report"]},{"oa":1,"citation":{"ieee":"K. Chatterjee, A. Kössler, A. Pavlogiannis, and U. Schmid, A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks. IST Austria, 2014.","apa":"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. https://doi.org/10.15479/AT:IST-2014-300-v1-1","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.","ama":"Chatterjee K, Kössler A, Pavlogiannis A, Schmid U. A Framework for Automated Competitive Analysis of On-Line Scheduling of Firm-Deadline Tasks. IST Austria; 2014. doi:10.15479/AT:IST-2014-300-v1-1","chicago":"Chatterjee, Krishnendu, Alexander Kössler, Andreas Pavlogiannis, and Ulrich Schmid. A Framework for Automated Competitive Analysis of On-Line Scheduling of Firm-Deadline Tasks. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-300-v1-1.","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.","mla":"Chatterjee, Krishnendu, et al. A Framework for Automated Competitive Analysis of On-Line Scheduling of Firm-Deadline Tasks. IST Austria, 2014, doi:10.15479/AT:IST-2014-300-v1-1."},"page":"14","date_published":"2014-07-29T00:00:00Z","doi":"10.15479/AT:IST-2014-300-v1-1","language":[{"iso":"eng"}],"publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1","day":"29","month":"07","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"5423","year":"2014","department":[{"_id":"KrCh"}],"publisher":"IST Austria","status":"public","title":"A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks","ddc":["005"],"publication_status":"published","pubrep_id":"300","related_material":{"record":[{"id":"1714","status":"public","relation":"later_version"}]},"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"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","first_name":"Andreas","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas"},{"full_name":"Schmid, Ulrich","first_name":"Ulrich","last_name":"Schmid"}],"file":[{"access_level":"open_access","file_name":"IST-2014-300-v1+1_main.pdf","content_type":"application/pdf","file_size":1270021,"creator":"system","relation":"main_file","file_id":"5514","checksum":"4b8fde4d9ef6653837f6803921d83032","date_updated":"2020-07-14T12:46:50Z","date_created":"2018-12-12T11:53:53Z"}],"oa_version":"Published Version","date_created":"2018-12-12T11:39:15Z","date_updated":"2023-02-23T10:11:15Z","type":"technical_report","alternative_title":["IST Austria Technical Report"],"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. "}],"file_date_updated":"2020-07-14T12:46:50Z"},{"abstract":[{"lang":"eng","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."}],"file_date_updated":"2020-07-14T12:46:52Z","alternative_title":["IST Austria Technical Report"],"type":"technical_report","file":[{"relation":"main_file","file_id":"5471","checksum":"9d3b90bf4fff74664f182f2d95ef727a","date_updated":"2020-07-14T12:46:52Z","date_created":"2018-12-12T11:53:10Z","access_level":"open_access","file_name":"IST-2014-314-v1+1_long.pdf","content_type":"application/pdf","file_size":405561,"creator":"system"}],"oa_version":"Published Version","date_updated":"2021-01-12T08:02:09Z","date_created":"2018-12-12T11:39:16Z","pubrep_id":"314","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","last_name":"Ibsen-Jensen","id":"3B699956-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-4783-0389"},{"full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87","last_name":"Pavlogiannis","first_name":"Andreas"}],"publisher":"IST Austria","department":[{"_id":"KrCh"}],"status":"public","title":"Optimal tree-decomposition balancing and reachability on low treewidth graphs","publication_status":"published","ddc":["000"],"year":"2014","_id":"5427","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"month":"11","day":"05","language":[{"iso":"eng"}],"doi":"10.15479/AT:IST-2014-314-v1-1","date_published":"2014-11-05T00:00:00Z","page":"24","citation":{"ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2014. Optimal tree-decomposition balancing and reachability on low treewidth graphs, IST Austria, 24p.","apa":"Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2014). Optimal tree-decomposition balancing and reachability on low treewidth graphs. IST Austria. https://doi.org/10.15479/AT:IST-2014-314-v1-1","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, Optimal tree-decomposition balancing and reachability on low treewidth graphs. IST Austria, 2014.","ama":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Optimal Tree-Decomposition Balancing and Reachability on Low Treewidth Graphs. IST Austria; 2014. doi:10.15479/AT:IST-2014-314-v1-1","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. Optimal Tree-Decomposition Balancing and Reachability on Low Treewidth Graphs. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-314-v1-1.","mla":"Chatterjee, Krishnendu, et al. Optimal Tree-Decomposition Balancing and Reachability on Low Treewidth Graphs. IST Austria, 2014, doi:10.15479/AT:IST-2014-314-v1-1.","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Optimal Tree-Decomposition Balancing and Reachability on Low Treewidth Graphs, IST Austria, 2014."},"oa":1},{"has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"day":"19","month":"02","page":"27","citation":{"short":"K. Chatterjee, T.A. Henzinger, J. Otop, Nested Weighted Automata, IST Austria, 2014.","mla":"Chatterjee, Krishnendu, et al. Nested Weighted Automata. IST Austria, 2014, doi:10.15479/AT:IST-2014-170-v1-1.","chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. Nested Weighted Automata. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-170-v1-1.","ama":"Chatterjee K, Henzinger TA, Otop J. Nested Weighted Automata. IST Austria; 2014. doi:10.15479/AT:IST-2014-170-v1-1","apa":"Chatterjee, K., Henzinger, T. A., & Otop, J. (2014). Nested weighted automata. IST Austria. https://doi.org/10.15479/AT:IST-2014-170-v1-1","ieee":"K. Chatterjee, T. A. Henzinger, and J. Otop, Nested weighted automata. IST Austria, 2014.","ista":"Chatterjee K, Henzinger TA, Otop J. 2014. Nested weighted automata, IST Austria, 27p."},"oa":1,"language":[{"iso":"eng"}],"doi":"10.15479/AT:IST-2014-170-v1-1","date_published":"2014-02-19T00:00:00Z","alternative_title":["IST Austria Technical Report"],"type":"technical_report","abstract":[{"lang":"eng","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. "}],"file_date_updated":"2020-07-14T12:46:48Z","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"IST Austria","ddc":["004"],"title":"Nested weighted automata","status":"public","publication_status":"published","_id":"5415","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2014","oa_version":"Published Version","file":[{"creator":"system","content_type":"application/pdf","file_size":573457,"access_level":"open_access","file_name":"IST-2014-170-v1+1_main.pdf","checksum":"31f90dcf2cf899c3f8c6427cfcc2b3c7","date_created":"2018-12-12T11:53:36Z","date_updated":"2020-07-14T12:46:48Z","file_id":"5497","relation":"main_file"}],"date_created":"2018-12-12T11:39:12Z","date_updated":"2023-02-23T12:26:19Z","related_material":{"record":[{"id":"1656","relation":"later_version","status":"public"},{"status":"public","relation":"later_version","id":"467"},{"id":"5436","status":"public","relation":"later_version"}]},"pubrep_id":"170","author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","first_name":"Jan","last_name":"Otop"}]},{"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 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."}],"file_date_updated":"2020-07-14T12:46:50Z","type":"technical_report","alternative_title":["IST Austria Technical Report"],"author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Ibsen-Jensen","first_name":"Rasmus","orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus"},{"full_name":"Nowak, Martin","last_name":"Nowak","first_name":"Martin"}],"pubrep_id":"190","related_material":{"record":[{"relation":"later_version","status":"public","id":"5432"},{"id":"5440","relation":"later_version","status":"public"}]},"date_updated":"2023-02-23T12:26:33Z","date_created":"2018-12-12T11:39:14Z","file":[{"file_id":"5538","relation":"main_file","date_created":"2018-12-12T11:54:16Z","date_updated":"2020-07-14T12:46:50Z","checksum":"42f3d8b563286eb0d903832bd9a848d3","file_name":"IST-2014-190-v2+2_main_full.pdf","access_level":"open_access","creator":"system","file_size":443529,"content_type":"application/pdf"},{"creator":"kschuh","file_size":440911,"content_type":"application/pdf","access_level":"open_access","file_name":"IST-2014-190-v1+1_main_full.pdf","checksum":"0c9a2fd822309719634495a35957e34d","date_created":"2019-09-06T07:30:20Z","date_updated":"2020-07-14T12:46:50Z","file_id":"6852","relation":"main_file"}],"oa_version":"Published Version","_id":"5421","year":"2014","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","publication_status":"published","status":"public","ddc":["000","005"],"title":"The complexity of evolution on graphs","publisher":"IST Austria","department":[{"_id":"KrCh"}],"day":"18","month":"04","has_accepted_license":"1","publication_identifier":{"issn":["2664-1690"]},"date_published":"2014-04-18T00:00:00Z","doi":"10.15479/AT:IST-2014-190-v2-2","language":[{"iso":"eng"}],"citation":{"apa":"Chatterjee, K., Ibsen-Jensen, R., & Nowak, M. (2014). The complexity of evolution on graphs. IST Austria. https://doi.org/10.15479/AT:IST-2014-190-v2-2","ieee":"K. Chatterjee, R. Ibsen-Jensen, and M. Nowak, The complexity of evolution on graphs. IST Austria, 2014.","ista":"Chatterjee K, Ibsen-Jensen R, Nowak M. 2014. The complexity of evolution on graphs, IST Austria, 27p.","ama":"Chatterjee K, Ibsen-Jensen R, Nowak M. The Complexity of Evolution on Graphs. IST Austria; 2014. doi:10.15479/AT:IST-2014-190-v2-2","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Martin Nowak. The Complexity of Evolution on Graphs. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-190-v2-2.","short":"K. Chatterjee, R. Ibsen-Jensen, M. Nowak, The Complexity of Evolution on Graphs, IST Austria, 2014.","mla":"Chatterjee, Krishnendu, et al. The Complexity of Evolution on Graphs. IST Austria, 2014, doi:10.15479/AT:IST-2014-190-v2-2."},"oa":1,"page":"27"},{"ec_funded":1,"acknowledgement":" Supported by Austrian Science Fund (FWF) Grant No P23499-N23, FWF NFN Grant No\r\nS11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.","year":"2014","publisher":"Springer Nature","department":[{"_id":"KrCh"}],"publication_status":"published","related_material":{"record":[{"status":"public","relation":"later_version","id":"681"}]},"author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Doyen, Laurent","last_name":"Doyen","first_name":"Laurent"},{"full_name":"Filiot, Emmanuel","last_name":"Filiot","first_name":"Emmanuel"},{"full_name":"Raskin, Jean-François","last_name":"Raskin","first_name":"Jean-François"}],"volume":8318,"date_created":"2022-03-18T13:03:15Z","date_updated":"2023-02-23T12:52:24Z","publication_identifier":{"eissn":["1611-3349"],"isbn":["9783642540127"],"eisbn":["9783642540134"],"issn":["0302-9743"]},"month":"01","external_id":{"arxiv":["1311.3238"]},"project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"quality_controlled":"1","doi":"10.1007/978-3-642-54013-4_5","conference":{"end_date":"2014-01-21","location":"San Diego, CA, United States","start_date":"2014-01-19","name":"VMCAI: Verifcation, Model Checking, and Abstract Interpretation"},"language":[{"iso":"eng"}],"type":"conference","alternative_title":["LNCS"],"abstract":[{"text":"Two-player games on graphs provide the theoretical framework for many important problems such as reactive synthesis. While the traditional study of two-player zero-sum games has been extended to multi-player games with several notions of equilibria, they are decidable only for perfect-information games, whereas several applications require imperfect-information games.\r\nIn this paper we propose a new notion of equilibria, called doomsday equilibria, which is a strategy profile such that all players satisfy their own objective, and if any coalition of players deviates and violates even one of the players objective, then the objective of every player is violated.\r\nWe present algorithms and complexity results for deciding the existence of doomsday equilibria for various classes of ω-regular objectives, both for imperfect-information games, and for perfect-information games.We provide optimal complexity bounds for imperfect-information games, and in most cases for perfect-information games.","lang":"eng"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"10885","intvolume":" 8318","status":"public","title":"Doomsday equilibria for omega-regular games","oa_version":"Preprint","scopus_import":"1","article_processing_charge":"No","day":"30","citation":{"chicago":"Chatterjee, Krishnendu, Laurent Doyen, Emmanuel Filiot, and Jean-François Raskin. “Doomsday Equilibria for Omega-Regular Games.” In VMCAI 2014: Verification, Model Checking, and Abstract Interpretation, 8318:78–97. Springer Nature, 2014. https://doi.org/10.1007/978-3-642-54013-4_5.","short":"K. Chatterjee, L. Doyen, E. Filiot, J.-F. Raskin, in:, VMCAI 2014: Verification, Model Checking, and Abstract Interpretation, Springer Nature, 2014, pp. 78–97.","mla":"Chatterjee, Krishnendu, et al. “Doomsday Equilibria for Omega-Regular Games.” VMCAI 2014: Verification, Model Checking, and Abstract Interpretation, vol. 8318, Springer Nature, 2014, pp. 78–97, doi:10.1007/978-3-642-54013-4_5.","ieee":"K. Chatterjee, L. Doyen, E. Filiot, and J.-F. Raskin, “Doomsday equilibria for omega-regular games,” in VMCAI 2014: Verification, Model Checking, and Abstract Interpretation, San Diego, CA, United States, 2014, vol. 8318, pp. 78–97.","apa":"Chatterjee, K., Doyen, L., Filiot, E., & Raskin, J.-F. (2014). Doomsday equilibria for omega-regular games. In VMCAI 2014: Verification, Model Checking, and Abstract Interpretation (Vol. 8318, pp. 78–97). San Diego, CA, United States: Springer Nature. https://doi.org/10.1007/978-3-642-54013-4_5","ista":"Chatterjee K, Doyen L, Filiot E, Raskin J-F. 2014. Doomsday equilibria for omega-regular games. VMCAI 2014: Verification, Model Checking, and Abstract Interpretation. VMCAI: Verifcation, Model Checking, and Abstract Interpretation, LNCS, vol. 8318, 78–97.","ama":"Chatterjee K, Doyen L, Filiot E, Raskin J-F. Doomsday equilibria for omega-regular games. In: VMCAI 2014: Verification, Model Checking, and Abstract Interpretation. Vol 8318. Springer Nature; 2014:78-97. doi:10.1007/978-3-642-54013-4_5"},"publication":"VMCAI 2014: Verification, Model Checking, and Abstract Interpretation","page":"78-97","date_published":"2014-01-30T00:00:00Z"},{"file":[{"file_id":"4890","relation":"main_file","checksum":"712d4c5787ddf97809cfc962507f0738","date_updated":"2020-07-14T12:45:26Z","date_created":"2018-12-12T10:11:35Z","access_level":"open_access","file_name":"IST-2016-440-v1+1_journal.pcbi.1003818.pdf","creator":"system","file_size":1399093,"content_type":"application/pdf"}],"oa_version":"Published Version","pubrep_id":"440","status":"public","title":"The time scale of evolutionary innovation","ddc":["510"],"intvolume":" 10","user_id":"4435EBFC-F248-11E8-B48F-1D18A9856A87","_id":"2039","abstract":[{"lang":"eng","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."}],"issue":"9","type":"journal_article","date_published":"2014-09-11T00:00:00Z","publication":"PLoS Computational Biology","citation":{"ama":"Chatterjee K, Pavlogiannis A, Adlam B, Nowak M. The time scale of evolutionary innovation. PLoS Computational Biology. 2014;10(9). doi:10.1371/journal.pcbi.1003818","ista":"Chatterjee K, Pavlogiannis A, Adlam B, Nowak M. 2014. The time scale of evolutionary innovation. PLoS Computational Biology. 10(9), 7p.","ieee":"K. Chatterjee, A. Pavlogiannis, B. Adlam, and M. Nowak, “The time scale of evolutionary innovation,” PLoS Computational Biology, vol. 10, no. 9. Public Library of Science, 2014.","apa":"Chatterjee, K., Pavlogiannis, A., Adlam, B., & Nowak, M. (2014). The time scale of evolutionary innovation. PLoS Computational Biology. Public Library of Science. https://doi.org/10.1371/journal.pcbi.1003818","mla":"Chatterjee, Krishnendu, et al. “The Time Scale of Evolutionary Innovation.” PLoS Computational Biology, vol. 10, no. 9, 7p, Public Library of Science, 2014, doi:10.1371/journal.pcbi.1003818.","short":"K. Chatterjee, A. Pavlogiannis, B. Adlam, M. Nowak, PLoS Computational Biology 10 (2014).","chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, Ben Adlam, and Martin Nowak. “The Time Scale of Evolutionary Innovation.” PLoS Computational Biology. Public Library of Science, 2014. https://doi.org/10.1371/journal.pcbi.1003818."},"day":"11","has_accepted_license":"1","scopus_import":1,"date_created":"2018-12-11T11:55:22Z","date_updated":"2023-02-23T14:06:36Z","volume":10,"author":[{"full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Pavlogiannis, Andreas","last_name":"Pavlogiannis","first_name":"Andreas","orcid":"0000-0002-8943-0722","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Ben","last_name":"Adlam","full_name":"Adlam, Ben"},{"full_name":"Nowak, Martin","first_name":"Martin","last_name":"Nowak"}],"related_material":{"record":[{"relation":"research_data","status":"public","id":"9739"}]},"publication_status":"published","publisher":"Public Library of Science","department":[{"_id":"KrCh"}],"year":"2014","file_date_updated":"2020-07-14T12:45:26Z","publist_id":"5012","ec_funded":1,"article_number":"7p","language":[{"iso":"eng"}],"doi":"10.1371/journal.pcbi.1003818","quality_controlled":"1","project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","call_identifier":"FWF","name":"Game Theory"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"oa":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"month":"09"},{"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","first_name":"Andreas","last_name":"Pavlogiannis","full_name":"Pavlogiannis, Andreas"},{"last_name":"Adlam","first_name":"Ben","full_name":"Adlam, Ben"},{"full_name":"Novak, Martin","last_name":"Novak","first_name":"Martin"}],"related_material":{"record":[{"status":"public","relation":"used_in_publication","id":"2039"}]},"date_updated":"2023-02-23T10:25:37Z","date_created":"2021-07-28T08:13:57Z","oa_version":"Published Version","_id":"9739","year":"2014","user_id":"6785fbc1-c503-11eb-8a32-93094b40e1cf","status":"public","title":"Detailed proofs for “The time scale of evolutionary innovation”","department":[{"_id":"KrCh"}],"publisher":"Public Library of Science","type":"research_data_reference","doi":"10.1371/journal.pcbi.1003818.s001","date_published":"2014-09-11T00:00:00Z","citation":{"short":"K. Chatterjee, A. Pavlogiannis, B. Adlam, M. Novak, (2014).","mla":"Chatterjee, Krishnendu, et al. Detailed Proofs for “The Time Scale of Evolutionary Innovation.” Public Library of Science, 2014, doi:10.1371/journal.pcbi.1003818.s001.","chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, Ben Adlam, and Martin Novak. “Detailed Proofs for ‘The Time Scale of Evolutionary Innovation.’” Public Library of Science, 2014. https://doi.org/10.1371/journal.pcbi.1003818.s001.","ama":"Chatterjee K, Pavlogiannis A, Adlam B, Novak M. Detailed proofs for “The time scale of evolutionary innovation.” 2014. doi:10.1371/journal.pcbi.1003818.s001","ieee":"K. Chatterjee, A. Pavlogiannis, B. Adlam, and M. Novak, “Detailed proofs for ‘The time scale of evolutionary innovation.’” Public Library of Science, 2014.","apa":"Chatterjee, K., Pavlogiannis, A., Adlam, B., & Novak, M. (2014). Detailed proofs for “The time scale of evolutionary innovation.” Public Library of Science. https://doi.org/10.1371/journal.pcbi.1003818.s001","ista":"Chatterjee K, Pavlogiannis A, Adlam B, Novak M. 2014. Detailed proofs for “The time scale of evolutionary innovation”, Public Library of Science, 10.1371/journal.pcbi.1003818.s001."},"month":"09","day":"11","article_processing_charge":"No"},{"language":[{"iso":"eng"}],"doi":"10.1007/s00453-013-9843-7","project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23"},{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory"},{"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"}],"quality_controlled":"1","oa":1,"external_id":{"arxiv":["1604.08234"]},"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1604.08234"}],"month":"11","volume":70,"date_updated":"2023-09-05T14:09:29Z","date_created":"2018-12-11T11:47:01Z","related_material":{"record":[{"id":"10905","status":"public","relation":"earlier_version"}]},"author":[{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"full_name":"Henzinger, Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","orcid":"0000-0002-5008-6530","first_name":"Monika H","last_name":"Henzinger"},{"last_name":"Krinninger","first_name":"Sebastian","full_name":"Krinninger, Sebastian"},{"last_name":"Nanongkai","first_name":"Danupon","full_name":"Nanongkai, Danupon"}],"publisher":"Springer","department":[{"_id":"KrCh"}],"publication_status":"published","year":"2014","ec_funded":1,"publist_id":"7282","date_published":"2014-11-01T00:00:00Z","page":"457 - 492","article_type":"original","citation":{"ama":"Chatterjee K, Henzinger MH, Krinninger S, Nanongkai D. Polynomial-time algorithms for energy games with special weight structures. Algorithmica. 2014;70(3):457-492. doi:10.1007/s00453-013-9843-7","apa":"Chatterjee, K., Henzinger, M. H., Krinninger, S., & Nanongkai, D. (2014). Polynomial-time algorithms for energy games with special weight structures. Algorithmica. Springer. https://doi.org/10.1007/s00453-013-9843-7","ieee":"K. Chatterjee, M. H. Henzinger, S. Krinninger, and D. Nanongkai, “Polynomial-time algorithms for energy games with special weight structures,” Algorithmica, vol. 70, no. 3. Springer, pp. 457–492, 2014.","ista":"Chatterjee K, Henzinger MH, Krinninger S, Nanongkai D. 2014. Polynomial-time algorithms for energy games with special weight structures. Algorithmica. 70(3), 457–492.","short":"K. Chatterjee, M.H. Henzinger, S. Krinninger, D. Nanongkai, Algorithmica 70 (2014) 457–492.","mla":"Chatterjee, Krishnendu, et al. “Polynomial-Time Algorithms for Energy Games with Special Weight Structures.” Algorithmica, vol. 70, no. 3, Springer, 2014, pp. 457–92, doi:10.1007/s00453-013-9843-7.","chicago":"Chatterjee, Krishnendu, Monika H Henzinger, Sebastian Krinninger, and Danupon Nanongkai. “Polynomial-Time Algorithms for Energy Games with Special Weight Structures.” Algorithmica. Springer, 2014. https://doi.org/10.1007/s00453-013-9843-7."},"publication":"Algorithmica","article_processing_charge":"No","day":"01","scopus_import":"1","oa_version":"Preprint","intvolume":" 70","title":"Polynomial-time algorithms for energy games with special weight structures","status":"public","user_id":"72615eeb-f1f3-11ec-aa25-d4573ddc34fd","_id":"535","issue":"3","abstract":[{"lang":"eng","text":"Energy games belong to a class of turn-based two-player infinite-duration games played on a weighted directed graph. It is one of the rare and intriguing combinatorial problems that lie in NP∩co-NP, but are not known to be in P. The existence of polynomial-time algorithms has been a major open problem for decades and apart from pseudopolynomial algorithms there is no algorithm that solves any non-trivial subclass in polynomial time. In this paper, we give several results based on the weight structures of the graph. First, we identify a notion of penalty and present a polynomial-time algorithm when the penalty is large. Our algorithm is the first polynomial-time algorithm on a large class of weighted graphs. It includes several worst-case instances on which previous algorithms, such as value iteration and random facet algorithms, require at least sub-exponential time. Our main technique is developing the first non-trivial approximation algorithm and showing how to convert it to an exact algorithm. Moreover, we show that in a practical case in verification where weights are clustered around a constant number of values, the energy game problem can be solved in polynomial time. We also show that the problem is still as hard as in general when the clique-width is bounded or the graph is strongly ergodic, suggesting that restricting the graph structure does not necessarily help."}],"type":"journal_article"},{"day":"01","month":"07","conference":{"name":"CAV: Computer Aided Verification","end_date":"2014-07-22","start_date":"2014-07-18","location":"Vienna, Austria"},"doi":"10.1007/978-3-319-08867-9_31","date_published":"2014-07-01T00:00:00Z","language":[{"iso":"eng"}],"citation":{"ista":"Chatterjee K, Chmelik M, Daca P. 2014. CEGAR for qualitative analysis of probabilistic systems. CAV: Computer Aided Verification, LNCS, vol. 8559, 473–490.","apa":"Chatterjee, K., Chmelik, M., & Daca, P. (2014). CEGAR for qualitative analysis of probabilistic systems (Vol. 8559, pp. 473–490). Presented at the CAV: Computer Aided Verification, Vienna, Austria: Springer. https://doi.org/10.1007/978-3-319-08867-9_31","ieee":"K. Chatterjee, M. Chmelik, and P. Daca, “CEGAR for qualitative analysis of probabilistic systems,” presented at the CAV: Computer Aided Verification, Vienna, Austria, 2014, vol. 8559, pp. 473–490.","ama":"Chatterjee K, Chmelik M, Daca P. CEGAR for qualitative analysis of probabilistic systems. In: Vol 8559. Springer; 2014:473-490. doi:10.1007/978-3-319-08867-9_31","chicago":"Chatterjee, Krishnendu, Martin Chmelik, and Przemyslaw Daca. “CEGAR for Qualitative Analysis of Probabilistic Systems,” 8559:473–90. Springer, 2014. https://doi.org/10.1007/978-3-319-08867-9_31.","mla":"Chatterjee, Krishnendu, et al. CEGAR for Qualitative Analysis of Probabilistic Systems. Vol. 8559, Springer, 2014, pp. 473–90, doi:10.1007/978-3-319-08867-9_31.","short":"K. Chatterjee, M. Chmelik, P. Daca, in:, Springer, 2014, pp. 473–490."},"quality_controlled":"1","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF"},{"call_identifier":"FWF","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"name":"Moderne Concurrency Paradigms","call_identifier":"FWF","grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"},{"grant_number":"267989","_id":"25EE3708-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Reactive Modeling"}],"page":"473 - 490","abstract":[{"text":"We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems.We focus on qualitative properties forMDPs that can express that desired behaviors of the system arise almost-surely (with probability 1) or with positive probability. We introduce a new simulation relation to capture the refinement relation ofMDPs with respect to qualitative properties, and present discrete graph theoretic algorithms with quadratic complexity to compute the simulation relation.We present an automated technique for assume-guarantee style reasoning for compositional analysis ofMDPs with qualitative properties by giving a counterexample guided abstraction-refinement approach to compute our new simulation relation. We have implemented our algorithms and show that the compositional analysis leads to significant improvements.","lang":"eng"}],"publist_id":"4978","ec_funded":1,"type":"conference","alternative_title":["LNCS"],"author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Chmelik, Martin","last_name":"Chmelik","first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Daca, Przemyslaw","last_name":"Daca","first_name":"Przemyslaw","id":"49351290-F248-11E8-B48F-1D18A9856A87"}],"related_material":{"record":[{"id":"5412","relation":"earlier_version","status":"public"},{"relation":"earlier_version","status":"public","id":"5413"},{"id":"5414","status":"public","relation":"earlier_version"},{"relation":"dissertation_contains","status":"public","id":"1155"}]},"date_updated":"2023-09-07T11:58:33Z","date_created":"2018-12-11T11:55:30Z","oa_version":"None","volume":8559,"_id":"2063","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2014","status":"public","title":"CEGAR for qualitative analysis of probabilistic systems","publication_status":"published","intvolume":" 8559","publisher":"Springer","department":[{"_id":"KrCh"},{"_id":"ToHe"}]},{"alternative_title":["IST Austria Technical Report"],"type":"technical_report","abstract":[{"lang":"eng","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."}],"file_date_updated":"2020-07-14T12:46:52Z","publication_status":"published","ddc":["004"],"status":"public","title":"Quantitative fair simulation games","publisher":"IST Austria","department":[{"_id":"ToHe"},{"_id":"KrCh"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"5428","year":"2014","date_created":"2018-12-12T11:39:16Z","date_updated":"2023-09-20T12:07:48Z","file":[{"access_level":"open_access","file_name":"IST-2014-315-v1+1_report.pdf","content_type":"application/pdf","file_size":531046,"creator":"system","relation":"main_file","file_id":"5521","checksum":"b1d573bc04365625ff9974880c0aa807","date_created":"2018-12-12T11:53:59Z","date_updated":"2020-07-14T12:46:52Z"}],"oa_version":"Published Version","author":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"full_name":"Otop, Jan","id":"2FC5DA74-F248-11E8-B48F-1D18A9856A87","last_name":"Otop","first_name":"Jan"},{"last_name":"Velner","first_name":"Yaron","full_name":"Velner, Yaron"}],"pubrep_id":"315","related_material":{"record":[{"status":"public","relation":"later_version","id":"1066"}]},"day":"05","month":"12","publication_identifier":{"issn":["2664-1690"]},"has_accepted_license":"1","page":"26","citation":{"chicago":"Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Yaron Velner. Quantitative Fair Simulation Games. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-315-v1-1.","short":"K. Chatterjee, T.A. Henzinger, J. Otop, Y. Velner, Quantitative Fair Simulation Games, IST Austria, 2014.","mla":"Chatterjee, Krishnendu, et al. Quantitative Fair Simulation Games. IST Austria, 2014, doi:10.15479/AT:IST-2014-315-v1-1.","ieee":"K. Chatterjee, T. A. Henzinger, J. Otop, and Y. Velner, Quantitative fair simulation games. IST Austria, 2014.","apa":"Chatterjee, K., Henzinger, T. A., Otop, J., & Velner, Y. (2014). Quantitative fair simulation games. IST Austria. https://doi.org/10.15479/AT:IST-2014-315-v1-1","ista":"Chatterjee K, Henzinger TA, Otop J, Velner Y. 2014. Quantitative fair simulation games, IST Austria, 26p.","ama":"Chatterjee K, Henzinger TA, Otop J, Velner Y. Quantitative Fair Simulation Games. IST Austria; 2014. doi:10.15479/AT:IST-2014-315-v1-1"},"oa":1,"language":[{"iso":"eng"}],"doi":"10.15479/AT:IST-2014-315-v1-1","date_published":"2014-12-05T00:00:00Z"},{"abstract":[{"lang":"eng","text":"We study two-player zero-sum games over infinite-state graphs equipped with ωB and finitary conditions. Our first contribution is about the strategy complexity, i.e the memory required for winning strategies: we prove that over general infinite-state graphs, memoryless strategies are sufficient for finitary Büchi, and finite-memory suffices for finitary parity games. We then study pushdown games with boundedness conditions, with two contributions. First we prove a collapse result for pushdown games with ωB-conditions, implying the decidability of solving these games. Second we consider pushdown games with finitary parity along with stack boundedness conditions, and show that solving these games is EXPTIME-complete."}],"alternative_title":["LIPIcs"],"type":"conference","file":[{"file_size":547296,"content_type":"application/pdf","creator":"system","access_level":"open_access","file_name":"IST-2016-624-v1+1_ChKr_Infinite-state_games_2013_17.pdf","checksum":"b7091a3866db573c0db5ec486952255e","date_updated":"2020-07-14T12:44:47Z","date_created":"2018-12-12T10:13:38Z","relation":"main_file","file_id":"5023"}],"oa_version":"Published Version","pubrep_id":"624","intvolume":" 23","title":"Infinite-state games with finitary conditions","ddc":["000"],"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"1374","has_accepted_license":"1","day":"01","series_title":"Leibniz International Proceedings in Informatics","scopus_import":1,"date_published":"2013-09-01T00:00:00Z","page":"181 - 196","citation":{"short":"K. Chatterjee, N. Fijalkow, in:, 22nd EACSL Annual Conference on Computer Science Logic, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013, pp. 181–196.","mla":"Chatterjee, Krishnendu, and Nathanaël Fijalkow. “Infinite-State Games with Finitary Conditions.” 22nd EACSL Annual Conference on Computer Science Logic, vol. 23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013, pp. 181–96, doi:10.4230/LIPIcs.CSL.2013.181.","chicago":"Chatterjee, Krishnendu, and Nathanaël Fijalkow. “Infinite-State Games with Finitary Conditions.” In 22nd EACSL Annual Conference on Computer Science Logic, 23:181–96. Leibniz International Proceedings in Informatics. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013. https://doi.org/10.4230/LIPIcs.CSL.2013.181.","ama":"Chatterjee K, Fijalkow N. Infinite-state games with finitary conditions. In: 22nd EACSL Annual Conference on Computer Science Logic. Vol 23. Leibniz International Proceedings in Informatics. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2013:181-196. doi:10.4230/LIPIcs.CSL.2013.181","ieee":"K. Chatterjee and N. Fijalkow, “Infinite-state games with finitary conditions,” in 22nd EACSL Annual Conference on Computer Science Logic, Torino, Italy, 2013, vol. 23, pp. 181–196.","apa":"Chatterjee, K., & Fijalkow, N. (2013). Infinite-state games with finitary conditions. In 22nd EACSL Annual Conference on Computer Science Logic (Vol. 23, pp. 181–196). Torino, Italy: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CSL.2013.181","ista":"Chatterjee K, Fijalkow N. 2013. Infinite-state games with finitary conditions. 22nd EACSL Annual Conference on Computer Science Logic. CSL: Computer Science LogicLeibniz International Proceedings in Informatics, LIPIcs, vol. 23, 181–196."},"publication":"22nd EACSL Annual Conference on Computer Science Logic","publist_id":"5837","ec_funded":1,"file_date_updated":"2020-07-14T12:44:47Z","volume":23,"date_created":"2018-12-11T11:51:39Z","date_updated":"2021-01-12T06:50:14Z","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"last_name":"Fijalkow","first_name":"Nathanaël","full_name":"Fijalkow, Nathanaël"}],"department":[{"_id":"KrCh"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","publication_status":"published","year":"2013","month":"09","language":[{"iso":"eng"}],"doi":"10.4230/LIPIcs.CSL.2013.181","conference":{"name":"CSL: Computer Science Logic","location":"Torino, Italy","start_date":"203-09-02","end_date":"2013-09-05"},"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","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"quality_controlled":"1","oa":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"}},{"publist_id":"4723","ec_funded":1,"volume":8312,"date_updated":"2020-08-11T10:09:42Z","date_created":"2018-12-11T11:56:30Z","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu"},{"full_name":"Forejt, Vojtěch","last_name":"Forejt","first_name":"Vojtěch"},{"full_name":"Wojtczak, Dominik","last_name":"Wojtczak","first_name":"Dominik"}],"department":[{"_id":"KrCh"}],"publisher":"Springer","publication_status":"published","year":"2013","month":"12","language":[{"iso":"eng"}],"doi":"10.1007/978-3-642-45221-5_17","conference":{"name":"LPAR: Logic for Programming, Artificial Intelligence, and Reasoning","end_date":"2013-12-19","start_date":"2013-12-14","location":"Stellenbosch, South Africa"},"project":[{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"quality_controlled":"1","abstract":[{"lang":"eng","text":"We study the problem of achieving a given value in Markov decision processes (MDPs) with several independent discounted reward objectives. We consider a generalised version of discounted reward objectives, in which the amount of discounting depends on the states visited and on the objective. This definition extends the usual definition of discounted reward, and allows to capture the systems in which the value of different commodities diminish at different and variable rates.\r\n\r\nWe establish results for two prominent subclasses of the problem, namely state-discount models where the discount factors are only dependent on the state of the MDP (and independent of the objective), and reward-discount models where they are only dependent on the objective (but not on the state of the MDP). For the state-discount models we use a straightforward reduction to expected total reward and show that the problem whether a value is achievable can be solved in polynomial time. For the reward-discount model we show that memory and randomisation of the strategies are required, but nevertheless that the problem is decidable and it is sufficient to consider strategies which after a certain number of steps behave in a memoryless way.\r\n\r\nFor the general case, we show that when restricted to graphs (i.e. MDPs with no randomisation), pure strategies and discount factors of the form 1/n where n is an integer, the problem is in PSPACE and finite memory suffices for achieving a given value. We also show that when the discount factors are not of the form 1/n, the memory required by a strategy can be infinite.\r\n"}],"alternative_title":["LNCS"],"type":"conference","oa_version":"None","intvolume":" 8312","status":"public","title":"Multi-objective discounted reward verification in graphs and MDPs","_id":"2238","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"01","series_title":"Lecture Notes in Computer Science","scopus_import":1,"date_published":"2013-12-01T00:00:00Z","page":"228 - 242","citation":{"mla":"Chatterjee, Krishnendu, et al. Multi-Objective Discounted Reward Verification in Graphs and MDPs. Vol. 8312, Springer, 2013, pp. 228–42, doi:10.1007/978-3-642-45221-5_17.","short":"K. Chatterjee, V. Forejt, D. Wojtczak, 8312 (2013) 228–242.","chicago":"Chatterjee, Krishnendu, Vojtěch Forejt, and Dominik Wojtczak. “Multi-Objective Discounted Reward Verification in Graphs and MDPs.” Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-45221-5_17.","ama":"Chatterjee K, Forejt V, Wojtczak D. Multi-objective discounted reward verification in graphs and MDPs. 2013;8312:228-242. doi:10.1007/978-3-642-45221-5_17","ista":"Chatterjee K, Forejt V, Wojtczak D. 2013. Multi-objective discounted reward verification in graphs and MDPs. 8312, 228–242.","apa":"Chatterjee, K., Forejt, V., & Wojtczak, D. (2013). Multi-objective discounted reward verification in graphs and MDPs. Presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Stellenbosch, South Africa: Springer. https://doi.org/10.1007/978-3-642-45221-5_17","ieee":"K. Chatterjee, V. Forejt, and D. Wojtczak, “Multi-objective discounted reward verification in graphs and MDPs,” vol. 8312. Springer, pp. 228–242, 2013."}},{"_id":"2292","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2013","status":"public","title":"Mathematical Foundations of Computer Science 2013","publication_status":"published","department":[{"_id":"KrCh"}],"editor":[{"full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee"},{"last_name":"Sgall","first_name":"Jiri","full_name":"Sgall, Jiri"}],"intvolume":" 8087","publisher":"Springer","date_created":"2018-12-11T11:56:48Z","date_updated":"2020-08-11T10:09:45Z","volume":8087,"oa_version":"None","type":"conference_editor","alternative_title":["LNCS"],"abstract":[{"lang":"eng","text":"This book constitutes the thoroughly refereed conference proceedings of the 38th International Symposium on Mathematical Foundations of Computer Science, MFCS 2013, held in Klosterneuburg, Austria, in August 2013. The 67 revised full papers presented together with six invited talks were carefully selected from 191 submissions. Topics covered include algorithmic game theory, algorithmic learning theory, algorithms and data structures, automata, formal languages, bioinformatics, complexity, computational geometry, computer-assisted reasoning, concurrency theory, databases and knowledge-based systems, foundations of computing, logic in computer science, models of computation, semantics and verification of programs, and theoretical issues in artificial intelligence."}],"publist_id":"4636","citation":{"apa":"Chatterjee, K., & Sgall, J. (Eds.). (2013). Mathematical Foundations of Computer Science 2013 (Vol. 8087, p. VI-854). Presented at the MFCS: Mathematical Foundations of Computer Science, Klosterneuburg, Austria: Springer. https://doi.org/10.1007/978-3-642-40313-2","ieee":"K. Chatterjee and J. Sgall, Eds., Mathematical Foundations of Computer Science 2013, vol. 8087. Springer, 2013, p. VI-854.","ista":"Chatterjee K, Sgall J eds. 2013. Mathematical Foundations of Computer Science 2013, Springer,p.","ama":"Chatterjee K, Sgall J, eds. Mathematical Foundations of Computer Science 2013. Vol 8087. Springer; 2013:VI-854. doi:10.1007/978-3-642-40313-2","chicago":"Chatterjee, Krishnendu, and Jiri Sgall, eds. Mathematical Foundations of Computer Science 2013. Vol. 8087. Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-40313-2.","short":"K. Chatterjee, J. Sgall, eds., Mathematical Foundations of Computer Science 2013, Springer, 2013.","mla":"Chatterjee, Krishnendu, and Jiri Sgall, editors. Mathematical Foundations of Computer Science 2013. Vol. 8087, Springer, 2013, p. VI-854, doi:10.1007/978-3-642-40313-2."},"quality_controlled":"1","page":"VI - 854","conference":{"name":"MFCS: Mathematical Foundations of Computer Science","end_date":"2013-08-30","start_date":"2013-08-26","location":"Klosterneuburg, Austria"},"doi":"10.1007/978-3-642-40313-2","date_published":"2013-08-08T00:00:00Z","language":[{"iso":"eng"}],"scopus_import":1,"series_title":"Lecture Notes in Computer Science","day":"08","month":"08","publication_identifier":{"isbn":["978-3-642-40312-5"]}},{"date_published":"2013-10-01T00:00:00Z","page":"585 - 601","publication":"International Journal on Software Tools for Technology Transfer","citation":{"ista":"Godhal Y, Chatterjee K, Henzinger TA. 2013. Synthesis of AMBA AHB from formal specification: A case study. International Journal on Software Tools for Technology Transfer. 15(5–6), 585–601.","apa":"Godhal, Y., Chatterjee, K., & Henzinger, T. A. (2013). Synthesis of AMBA AHB from formal specification: A case study. International Journal on Software Tools for Technology Transfer. Springer. https://doi.org/10.1007/s10009-011-0207-9","ieee":"Y. Godhal, K. Chatterjee, and T. A. Henzinger, “Synthesis of AMBA AHB from formal specification: A case study,” International Journal on Software Tools for Technology Transfer, vol. 15, no. 5–6. Springer, pp. 585–601, 2013.","ama":"Godhal Y, Chatterjee K, Henzinger TA. Synthesis of AMBA AHB from formal specification: A case study. International Journal on Software Tools for Technology Transfer. 2013;15(5-6):585-601. doi:10.1007/s10009-011-0207-9","chicago":"Godhal, Yashdeep, Krishnendu Chatterjee, and Thomas A Henzinger. “Synthesis of AMBA AHB from Formal Specification: A Case Study.” International Journal on Software Tools for Technology Transfer. Springer, 2013. https://doi.org/10.1007/s10009-011-0207-9.","mla":"Godhal, Yashdeep, et al. “Synthesis of AMBA AHB from Formal Specification: A Case Study.” International Journal on Software Tools for Technology Transfer, vol. 15, no. 5–6, Springer, 2013, pp. 585–601, doi:10.1007/s10009-011-0207-9.","short":"Y. Godhal, K. Chatterjee, T.A. Henzinger, International Journal on Software Tools for Technology Transfer 15 (2013) 585–601."},"day":"01","has_accepted_license":"1","scopus_import":1,"oa_version":"Submitted Version","file":[{"creator":"system","content_type":"application/pdf","file_size":277372,"access_level":"open_access","file_name":"IST-2012-87-v1+1_Synthesis_of_AMBA_AHB_from_formal_specifications-_A_case_study.pdf","checksum":"57b06a732dd8d6349190dba6b5b0d33b","date_updated":"2020-07-14T12:45:37Z","date_created":"2018-12-12T10:11:53Z","file_id":"4910","relation":"main_file"}],"pubrep_id":"87","title":"Synthesis of AMBA AHB from formal specification: A case study","ddc":["000"],"status":"public","intvolume":" 15","_id":"2299","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","abstract":[{"text":"The standard hardware design flow involves: (a) design of an integrated circuit using a hardware description language, (b) extensive functional and formal verification, and (c) logical synthesis. However, the above-mentioned processes consume significant effort and time. An alternative approach is to use a formal specification language as a high-level hardware description language and synthesize hardware from formal specifications. Our work is a case study of the synthesis of the widely and industrially used AMBA AHB protocol from formal specifications. Bloem et al. presented the first formal specifications for the AMBA AHB Arbiter and synthesized the AHB Arbiter circuit. However, in the first formal specification some important assumptions were missing. Our contributions are as follows: (a) We present detailed formal specifications for the AHB Arbiter incorporating the missing details, and obtain significant improvements in the synthesis results (both with respect to the number of gates in the synthesized circuit and with respect to the time taken to synthesize the circuit), and (b) we present formal specifications to generate compact circuits for the remaining two main components of AMBA AHB, namely, AHB Master and AHB Slave. Thus with systematic description we are able to automatically and completely synthesize an important and widely used industrial protocol.","lang":"eng"}],"issue":"5-6","type":"journal_article","language":[{"iso":"eng"}],"doi":"10.1007/s10009-011-0207-9","quality_controlled":"1","project":[{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"oa":1,"month":"10","date_created":"2018-12-11T11:56:51Z","date_updated":"2021-01-12T06:56:37Z","volume":15,"author":[{"first_name":"Yashdeep","last_name":"Godhal","id":"5B547124-EB61-11E9-8887-89D9C04DBDF5","full_name":"Godhal, Yashdeep"},{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"publication_status":"published","publisher":"Springer","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"year":"2013","file_date_updated":"2020-07-14T12:45:37Z","publist_id":"4629"},{"month":"07","conference":{"name":"CAV: Computer Aided Verification","end_date":"2013-07-19","location":"St. Petersburg, Russia","start_date":"2013-07-13"},"doi":"10.1007/978-3-642-39799-8_37","language":[{"iso":"eng"}],"main_file_link":[{"url":"http://arxiv.org/abs/1304.5281","open_access":"1"}],"oa":1,"external_id":{"arxiv":["1304.5281"]},"quality_controlled":"1","project":[{"grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425","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"},{"_id":"2587B514-B435-11E9-9278-68D0E5697425","name":"Microsoft Research Faculty Fellowship"}],"ec_funded":1,"publist_id":"4457","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"full_name":"Gaiser, Andreas","last_name":"Gaiser","first_name":"Andreas"},{"full_name":"Kretinsky, Jan","last_name":"Kretinsky","first_name":"Jan","orcid":"0000-0002-8122-2881","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"}],"date_created":"2018-12-11T11:57:42Z","date_updated":"2020-08-11T10:09:47Z","volume":8044,"year":"2013","publication_status":"published","publisher":"Springer","department":[{"_id":"KrCh"}],"day":"01","scopus_import":1,"series_title":"Lecture Notes in Computer Science","date_published":"2013-07-01T00:00:00Z","citation":{"ama":"Chatterjee K, Gaiser A, Kretinsky J. Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. 2013;8044:559-575. doi:10.1007/978-3-642-39799-8_37","ista":"Chatterjee K, Gaiser A, Kretinsky J. 2013. Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. 8044, 559–575.","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.","apa":"Chatterjee, K., Gaiser, A., & 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. https://doi.org/10.1007/978-3-642-39799-8_37","mla":"Chatterjee, Krishnendu, et al. Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis. Vol. 8044, Springer, 2013, pp. 559–75, doi:10.1007/978-3-642-39799-8_37.","short":"K. Chatterjee, A. Gaiser, J. Kretinsky, 8044 (2013) 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. https://doi.org/10.1007/978-3-642-39799-8_37."},"page":"559 - 575","abstract":[{"lang":"eng","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."}],"type":"conference","alternative_title":["LNCS"],"oa_version":"Preprint","_id":"2446","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis","status":"public","intvolume":" 8044"}]