--- _id: '5419' 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." alternative_title: - IST Austria Technical Report author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Rasmus full_name: Ibsen-Jensen, Rasmus id: 3B699956-F248-11E8-B48F-1D18A9856A87 last_name: Ibsen-Jensen orcid: 0000-0003-4783-0389 - first_name: Andreas full_name: Pavlogiannis, Andreas id: 49704004-F248-11E8-B48F-1D18A9856A87 last_name: Pavlogiannis orcid: 0000-0002-8943-0722 citation: 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 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 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. 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. 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. short: K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Improved Algorithms for Reachability and Shortest Path on Low Tree-Width Graphs, IST Austria, 2014. date_created: 2018-12-12T11:39:13Z date_published: 2014-04-14T00:00:00Z date_updated: 2021-01-12T08:02:03Z day: '14' ddc: - '000' department: - _id: KrCh doi: 10.15479/AT:IST-2014-187-v1-1 file: - access_level: open_access checksum: c608e66030a4bf51d2d99b451f539b99 content_type: application/pdf creator: system date_created: 2018-12-12T11:54:25Z date_updated: 2020-07-14T12:46:50Z file_id: '5548' file_name: IST-2014-187-v1+1_main_full_tech.pdf file_size: 670031 relation: main_file file_date_updated: 2020-07-14T12:46:50Z has_accepted_license: '1' language: - iso: eng month: '04' oa: 1 oa_version: Published Version page: '34' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '187' status: public title: Improved algorithms for reachability and shortest path on low tree-width graphs type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2014' ... --- _id: '5418' abstract: - lang: eng 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. alternative_title: - IST Austria Technical Report author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Laurent full_name: Doyen, Laurent last_name: Doyen citation: ama: Chatterjee K, Doyen L. Games with a Weak Adversary. IST Austria; 2014. doi:10.15479/AT:IST-2014-176-v1-1 apa: Chatterjee, K., & Doyen, L. (2014). Games with a weak adversary. IST Austria. https://doi.org/10.15479/AT:IST-2014-176-v1-1 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. ieee: K. Chatterjee and L. Doyen, Games with a weak adversary. IST Austria, 2014. ista: Chatterjee K, Doyen L. 2014. Games with a weak adversary, IST Austria, 18p. 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. date_created: 2018-12-12T11:39:13Z date_published: 2014-03-22T00:00:00Z date_updated: 2023-02-23T10:30:58Z day: '22' ddc: - '000' - '005' department: - _id: KrCh doi: 10.15479/AT:IST-2014-176-v1-1 file: - access_level: open_access checksum: 1d6958aa60050e1c3e932c6e5f34c39f content_type: application/pdf creator: system date_created: 2018-12-12T11:53:07Z date_updated: 2020-07-14T12:46:49Z file_id: '5468' file_name: IST-2014-176-v1+1_icalp_14.pdf file_size: 328253 relation: main_file file_date_updated: 2020-07-14T12:46:49Z has_accepted_license: '1' language: - iso: eng month: '03' oa: 1 oa_version: Published Version page: '18' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '176' related_material: record: - id: '2163' relation: later_version status: public status: public title: Games with a weak adversary type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2014' ... --- _id: '5420' abstract: - lang: eng text: 'We consider concurrent mean-payoff games, a very well-studied class of two-player (player 1 vs player 2) zero-sum games on finite-state graphs where every transition is assigned a reward between 0 and 1, and the payoff function is the long-run average of the rewards. The value is the maximal expected payoff that player 1 can guarantee against all strategies of player 2. We consider the computation of the set of states with value 1 under finite-memory strategies for player 1, and our main results for the problem are as follows: (1) we present a polynomial-time algorithm; (2) we show that whenever there is a finite-memory strategy, there is a stationary strategy that does not need memory at all; and (3) we present an optimal bound (which is double exponential) on the patience of stationary strategies (where patience of a distribution is the inverse of the smallest positive probability and represents a complexity measure of a stationary strategy).' alternative_title: - IST Austria Technical Report author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Rasmus full_name: Ibsen-Jensen, Rasmus id: 3B699956-F248-11E8-B48F-1D18A9856A87 last_name: Ibsen-Jensen orcid: 0000-0003-4783-0389 citation: 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 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 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. ieee: K. Chatterjee and R. Ibsen-Jensen, The value 1 problem for concurrent mean-payoff games. IST Austria, 2014. ista: Chatterjee K, Ibsen-Jensen R. 2014. The value 1 problem for concurrent mean-payoff games, IST Austria, 49p. 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. date_created: 2018-12-12T11:39:14Z date_published: 2014-04-14T00:00:00Z date_updated: 2021-01-12T08:02:05Z day: '14' ddc: - '000' - '005' department: - _id: KrCh doi: 10.15479/AT:IST-2014-191-v1-1 file: - access_level: open_access checksum: 49e0fd3e62650346daf7dc04604f7a0a content_type: application/pdf creator: system date_created: 2018-12-12T11:53:58Z date_updated: 2020-07-14T12:46:50Z file_id: '5520' file_name: IST-2014-191-v1+1_main_full.pdf file_size: 584368 relation: main_file file_date_updated: 2020-07-14T12:46:50Z has_accepted_license: '1' language: - iso: eng month: '04' oa: 1 oa_version: Published Version page: '49' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '191' status: public title: The value 1 problem for concurrent mean-payoff games type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2014' ... --- _id: '5424' 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. alternative_title: - IST Austria Technical Report author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Raghav full_name: Gupta, Raghav last_name: Gupta - first_name: Ayush full_name: Kanodia, Ayush last_name: Kanodia citation: 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 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 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. ieee: K. Chatterjee, M. Chmelik, R. Gupta, and 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. 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. date_created: 2018-12-12T11:39:15Z date_published: 2014-09-09T00:00:00Z date_updated: 2023-02-23T12:25:52Z day: '09' ddc: - '005' department: - _id: KrCh doi: 10.15479/AT:IST-2014-305-v1-1 file: - access_level: open_access checksum: 35009d5fad01198341e6c1a3353481b7 content_type: application/pdf creator: system date_created: 2018-12-12T11:53:51Z date_updated: 2020-07-14T12:46:51Z file_id: '5512' file_name: IST-2014-305-v1+1_main.pdf file_size: 655774 relation: main_file file_date_updated: 2020-07-14T12:46:51Z has_accepted_license: '1' language: - iso: eng month: '09' oa: 1 oa_version: Published Version page: '12' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '305' related_material: record: - id: '1732' relation: later_version status: public - id: '5426' relation: later_version status: public status: public title: Qualitative analysis of POMDPs with temporal logic specifications for robotics applications type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2014' ... --- _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. alternative_title: - IST Austria Technical Report author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Raghav full_name: Gupta, Raghav last_name: Gupta - first_name: Ayush full_name: Kanodia, Ayush last_name: Kanodia citation: 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 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 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. ieee: K. Chatterjee, M. Chmelik, R. Gupta, and 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, 10p. 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. short: K. Chatterjee, M. Chmelik, R. Gupta, A. Kanodia, Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications, IST Austria, 2014. date_created: 2018-12-12T11:39:16Z date_published: 2014-09-29T00:00:00Z date_updated: 2023-02-23T12:25:47Z day: '29' ddc: - '005' department: - _id: KrCh doi: 10.15479/AT:IST-2014-305-v2-1 file: - access_level: open_access checksum: 730c0a8e97cf2712a884b2cc423f3919 content_type: application/pdf creator: system date_created: 2018-12-12T11:54:15Z date_updated: 2020-07-14T12:46:51Z file_id: '5537' file_name: IST-2014-305-v2+1_main2.pdf file_size: 656019 relation: main_file file_date_updated: 2020-07-14T12:46:51Z has_accepted_license: '1' language: - iso: eng month: '09' oa: 1 oa_version: Published Version page: '10' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '311' related_material: record: - id: '1732' relation: later_version status: public - id: '5424' relation: earlier_version status: public status: public title: Qualitative analysis of POMDPs with temporal logic specifications for robotics applications type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2014' ... --- _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. ' alternative_title: - IST Austria Technical Report author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Alexander full_name: Kössler, Alexander last_name: Kössler - first_name: Andreas full_name: Pavlogiannis, Andreas id: 49704004-F248-11E8-B48F-1D18A9856A87 last_name: Pavlogiannis orcid: 0000-0002-8943-0722 - first_name: Ulrich full_name: Schmid, Ulrich last_name: Schmid citation: 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 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 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. 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. 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. 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. 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. date_created: 2018-12-12T11:39:15Z date_published: 2014-07-29T00:00:00Z date_updated: 2023-02-23T10:11:15Z day: '29' ddc: - '005' department: - _id: KrCh doi: 10.15479/AT:IST-2014-300-v1-1 file: - access_level: open_access checksum: 4b8fde4d9ef6653837f6803921d83032 content_type: application/pdf creator: system date_created: 2018-12-12T11:53:53Z date_updated: 2020-07-14T12:46:50Z file_id: '5514' file_name: IST-2014-300-v1+1_main.pdf file_size: 1270021 relation: main_file file_date_updated: 2020-07-14T12:46:50Z has_accepted_license: '1' language: - iso: eng month: '07' oa: 1 oa_version: Published Version page: '14' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '300' related_material: record: - id: '1714' relation: later_version status: public status: public title: A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2014' ... --- _id: '5427' 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.' alternative_title: - IST Austria Technical Report author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Rasmus full_name: Ibsen-Jensen, Rasmus id: 3B699956-F248-11E8-B48F-1D18A9856A87 last_name: Ibsen-Jensen orcid: 0000-0003-4783-0389 - first_name: Andreas full_name: Pavlogiannis, Andreas id: 49704004-F248-11E8-B48F-1D18A9856A87 last_name: Pavlogiannis orcid: 0000-0002-8943-0722 citation: 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 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 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. ieee: K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, Optimal tree-decomposition balancing and reachability on low treewidth graphs. IST Austria, 2014. ista: Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2014. Optimal tree-decomposition balancing and reachability on low treewidth graphs, IST Austria, 24p. 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. date_created: 2018-12-12T11:39:16Z date_published: 2014-11-05T00:00:00Z date_updated: 2021-01-12T08:02:09Z day: '05' ddc: - '000' department: - _id: KrCh doi: 10.15479/AT:IST-2014-314-v1-1 file: - access_level: open_access checksum: 9d3b90bf4fff74664f182f2d95ef727a content_type: application/pdf creator: system date_created: 2018-12-12T11:53:10Z date_updated: 2020-07-14T12:46:52Z file_id: '5471' file_name: IST-2014-314-v1+1_long.pdf file_size: 405561 relation: main_file file_date_updated: 2020-07-14T12:46:52Z has_accepted_license: '1' language: - iso: eng month: '11' oa: 1 oa_version: Published Version page: '24' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '314' status: public title: Optimal tree-decomposition balancing and reachability on low treewidth graphs type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2014' ... --- _id: '5415' 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. ' alternative_title: - IST Austria Technical Report author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Jan full_name: Otop, Jan id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87 last_name: Otop citation: 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 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. 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. mla: Chatterjee, Krishnendu, et al. Nested Weighted Automata. IST Austria, 2014, doi:10.15479/AT:IST-2014-170-v1-1. short: K. Chatterjee, T.A. Henzinger, J. Otop, Nested Weighted Automata, IST Austria, 2014. date_created: 2018-12-12T11:39:12Z date_published: 2014-02-19T00:00:00Z date_updated: 2023-02-23T12:26:19Z day: '19' ddc: - '004' department: - _id: KrCh - _id: ToHe doi: 10.15479/AT:IST-2014-170-v1-1 file: - access_level: open_access checksum: 31f90dcf2cf899c3f8c6427cfcc2b3c7 content_type: application/pdf creator: system date_created: 2018-12-12T11:53:36Z date_updated: 2020-07-14T12:46:48Z file_id: '5497' file_name: IST-2014-170-v1+1_main.pdf file_size: 573457 relation: main_file file_date_updated: 2020-07-14T12:46:48Z has_accepted_license: '1' language: - iso: eng month: '02' oa: 1 oa_version: Published Version page: '27' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '170' related_material: record: - id: '1656' relation: later_version status: public - id: '467' relation: later_version status: public - id: '5436' relation: later_version status: public status: public title: Nested weighted automata type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2014' ... --- _id: '5421' 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.' alternative_title: - IST Austria Technical Report author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Rasmus full_name: Ibsen-Jensen, Rasmus id: 3B699956-F248-11E8-B48F-1D18A9856A87 last_name: Ibsen-Jensen orcid: 0000-0003-4783-0389 - first_name: Martin full_name: Nowak, Martin last_name: Nowak citation: 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 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 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. 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. mla: Chatterjee, Krishnendu, et al. The Complexity of Evolution on Graphs. IST Austria, 2014, doi: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. date_created: 2018-12-12T11:39:14Z date_published: 2014-04-18T00:00:00Z date_updated: 2023-02-23T12:26:33Z day: '18' ddc: - '000' - '005' department: - _id: KrCh doi: 10.15479/AT:IST-2014-190-v2-2 file: - access_level: open_access checksum: 42f3d8b563286eb0d903832bd9a848d3 content_type: application/pdf creator: system date_created: 2018-12-12T11:54:16Z date_updated: 2020-07-14T12:46:50Z file_id: '5538' file_name: IST-2014-190-v2+2_main_full.pdf file_size: 443529 relation: main_file - access_level: open_access checksum: 0c9a2fd822309719634495a35957e34d content_type: application/pdf creator: kschuh date_created: 2019-09-06T07:30:20Z date_updated: 2020-07-14T12:46:50Z file_id: '6852' file_name: IST-2014-190-v1+1_main_full.pdf file_size: 440911 relation: main_file file_date_updated: 2020-07-14T12:46:50Z has_accepted_license: '1' language: - iso: eng month: '04' oa: 1 oa_version: Published Version page: '27' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '190' related_material: record: - id: '5432' relation: later_version status: public - id: '5440' relation: later_version status: public status: public title: The complexity of evolution on graphs type: technical_report user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 year: '2014' ... --- _id: '10885' abstract: - lang: eng 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." 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." alternative_title: - LNCS article_processing_charge: No author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Laurent full_name: Doyen, Laurent last_name: Doyen - first_name: Emmanuel full_name: Filiot, Emmanuel last_name: Filiot - first_name: Jean-François full_name: Raskin, Jean-François last_name: Raskin citation: 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' 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' 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.' 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.' 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.' 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.' 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.' conference: end_date: 2014-01-21 location: San Diego, CA, United States name: 'VMCAI: Verifcation, Model Checking, and Abstract Interpretation' start_date: 2014-01-19 date_created: 2022-03-18T13:03:15Z date_published: 2014-01-30T00:00:00Z date_updated: 2023-02-23T12:52:24Z day: '30' department: - _id: KrCh doi: 10.1007/978-3-642-54013-4_5 ec_funded: 1 external_id: arxiv: - '1311.3238' intvolume: ' 8318' language: - iso: eng month: '01' oa_version: Preprint page: 78-97 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: 'VMCAI 2014: Verification, Model Checking, and Abstract Interpretation' publication_identifier: eisbn: - '9783642540134' eissn: - 1611-3349 isbn: - '9783642540127' issn: - 0302-9743 publication_status: published publisher: Springer Nature quality_controlled: '1' related_material: record: - id: '681' relation: later_version status: public scopus_import: '1' status: public title: Doomsday equilibria for omega-regular games type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 8318 year: '2014' ... --- _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.' article_number: 7p author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Andreas full_name: Pavlogiannis, Andreas id: 49704004-F248-11E8-B48F-1D18A9856A87 last_name: Pavlogiannis orcid: 0000-0002-8943-0722 - first_name: Ben full_name: Adlam, Ben last_name: Adlam - first_name: Martin full_name: Nowak, Martin last_name: Nowak 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 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 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. 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. ista: Chatterjee K, Pavlogiannis A, Adlam B, Nowak M. 2014. The time scale of evolutionary innovation. PLoS Computational Biology. 10(9), 7p. 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). date_created: 2018-12-11T11:55:22Z date_published: 2014-09-11T00:00:00Z date_updated: 2023-02-23T14:06:36Z day: '11' ddc: - '510' department: - _id: KrCh doi: 10.1371/journal.pcbi.1003818 ec_funded: 1 file: - access_level: open_access checksum: 712d4c5787ddf97809cfc962507f0738 content_type: application/pdf creator: system date_created: 2018-12-12T10:11:35Z date_updated: 2020-07-14T12:45:26Z file_id: '4890' file_name: IST-2016-440-v1+1_journal.pcbi.1003818.pdf file_size: 1399093 relation: main_file file_date_updated: 2020-07-14T12:45:26Z has_accepted_license: '1' intvolume: ' 10' issue: '9' language: - iso: eng month: '09' oa: 1 oa_version: Published Version project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: PLoS Computational Biology publication_status: published publisher: Public Library of Science publist_id: '5012' pubrep_id: '440' quality_controlled: '1' related_material: record: - id: '9739' relation: research_data status: public scopus_import: 1 status: public title: The time scale of evolutionary innovation tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 10 year: '2014' ... --- _id: '9739' article_processing_charge: No author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Andreas full_name: Pavlogiannis, Andreas id: 49704004-F248-11E8-B48F-1D18A9856A87 last_name: Pavlogiannis orcid: 0000-0002-8943-0722 - first_name: Ben full_name: Adlam, Ben last_name: Adlam - first_name: Martin full_name: Novak, Martin last_name: Novak citation: 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 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 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. 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, 10.1371/journal.pcbi.1003818.s001. 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. short: K. Chatterjee, A. Pavlogiannis, B. Adlam, M. Novak, (2014). date_created: 2021-07-28T08:13:57Z date_published: 2014-09-11T00:00:00Z date_updated: 2023-02-23T10:25:37Z day: '11' department: - _id: KrCh doi: 10.1371/journal.pcbi.1003818.s001 month: '09' oa_version: Published Version publisher: Public Library of Science related_material: record: - id: '2039' relation: used_in_publication status: public status: public title: Detailed proofs for “The time scale of evolutionary innovation” type: research_data_reference user_id: 6785fbc1-c503-11eb-8a32-93094b40e1cf year: '2014' ... --- _id: '535' 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. article_processing_charge: No article_type: original author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Monika H full_name: Henzinger, Monika H id: 540c9bbd-f2de-11ec-812d-d04a5be85630 last_name: Henzinger orcid: 0000-0002-5008-6530 - first_name: Sebastian full_name: Krinninger, Sebastian last_name: Krinninger - first_name: Danupon full_name: Nanongkai, Danupon last_name: Nanongkai 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 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. 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. 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. short: K. Chatterjee, M.H. Henzinger, S. Krinninger, D. Nanongkai, Algorithmica 70 (2014) 457–492. date_created: 2018-12-11T11:47:01Z date_published: 2014-11-01T00:00:00Z date_updated: 2023-09-05T14:09:29Z day: '01' department: - _id: KrCh doi: 10.1007/s00453-013-9843-7 ec_funded: 1 external_id: arxiv: - '1604.08234' intvolume: ' 70' issue: '3' language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/1604.08234 month: '11' oa: 1 oa_version: Preprint page: 457 - 492 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: Algorithmica publication_status: published publisher: Springer publist_id: '7282' quality_controlled: '1' related_material: record: - id: '10905' relation: earlier_version status: public scopus_import: '1' status: public title: Polynomial-time algorithms for energy games with special weight structures type: journal_article user_id: 72615eeb-f1f3-11ec-aa25-d4573ddc34fd volume: 70 year: '2014' ... --- _id: '2063' abstract: - lang: eng 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. alternative_title: - LNCS author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Przemyslaw full_name: Daca, Przemyslaw id: 49351290-F248-11E8-B48F-1D18A9856A87 last_name: Daca citation: 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' 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' 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. 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.' ista: 'Chatterjee K, Chmelik M, Daca P. 2014. CEGAR for qualitative analysis of probabilistic systems. CAV: Computer Aided Verification, LNCS, vol. 8559, 473–490.' 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. conference: end_date: 2014-07-22 location: Vienna, Austria name: 'CAV: Computer Aided Verification' start_date: 2014-07-18 date_created: 2018-12-11T11:55:30Z date_published: 2014-07-01T00:00:00Z date_updated: 2023-09-07T11:58:33Z day: '01' department: - _id: KrCh - _id: ToHe doi: 10.1007/978-3-319-08867-9_31 ec_funded: 1 intvolume: ' 8559' language: - iso: eng month: '07' oa_version: None page: 473 - 490 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _id: 25F5A88A-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Moderne Concurrency Paradigms - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling publication_status: published publisher: Springer publist_id: '4978' quality_controlled: '1' related_material: record: - id: '5412' relation: earlier_version status: public - id: '5413' relation: earlier_version status: public - id: '5414' relation: earlier_version status: public - id: '1155' relation: dissertation_contains status: public status: public title: CEGAR for qualitative analysis of probabilistic systems type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 8559 year: '2014' ... --- _id: '5428' 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." alternative_title: - IST Austria Technical Report author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Jan full_name: Otop, Jan id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87 last_name: Otop - first_name: Yaron full_name: Velner, Yaron last_name: Velner citation: 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 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 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. ieee: K. Chatterjee, T. A. Henzinger, J. Otop, and Y. Velner, Quantitative fair simulation games. IST Austria, 2014. ista: Chatterjee K, Henzinger TA, Otop J, Velner Y. 2014. Quantitative fair simulation games, IST Austria, 26p. mla: Chatterjee, Krishnendu, et al. Quantitative Fair Simulation Games. IST Austria, 2014, doi: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. date_created: 2018-12-12T11:39:16Z date_published: 2014-12-05T00:00:00Z date_updated: 2023-09-20T12:07:48Z day: '05' ddc: - '004' department: - _id: ToHe - _id: KrCh doi: 10.15479/AT:IST-2014-315-v1-1 file: - access_level: open_access checksum: b1d573bc04365625ff9974880c0aa807 content_type: application/pdf creator: system date_created: 2018-12-12T11:53:59Z date_updated: 2020-07-14T12:46:52Z file_id: '5521' file_name: IST-2014-315-v1+1_report.pdf file_size: 531046 relation: main_file file_date_updated: 2020-07-14T12:46:52Z has_accepted_license: '1' language: - iso: eng month: '12' oa: 1 oa_version: Published Version page: '26' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '315' related_material: record: - id: '1066' relation: later_version status: public status: public title: Quantitative fair simulation games type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2014' ... --- _id: '1374' 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 author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Nathanaël full_name: Fijalkow, Nathanaël last_name: Fijalkow citation: 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' 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' 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. 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. 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.' 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. 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. conference: end_date: 2013-09-05 location: Torino, Italy name: 'CSL: Computer Science Logic' start_date: 203-09-02 date_created: 2018-12-11T11:51:39Z date_published: 2013-09-01T00:00:00Z date_updated: 2021-01-12T06:50:14Z day: '01' ddc: - '000' department: - _id: KrCh doi: 10.4230/LIPIcs.CSL.2013.181 ec_funded: 1 file: - access_level: open_access checksum: b7091a3866db573c0db5ec486952255e content_type: application/pdf creator: system date_created: 2018-12-12T10:13:38Z date_updated: 2020-07-14T12:44:47Z file_id: '5023' file_name: IST-2016-624-v1+1_ChKr_Infinite-state_games_2013_17.pdf file_size: 547296 relation: main_file file_date_updated: 2020-07-14T12:44:47Z has_accepted_license: '1' intvolume: ' 23' language: - iso: eng month: '09' oa: 1 oa_version: Published Version page: 181 - 196 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: 22nd EACSL Annual Conference on Computer Science Logic publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik publist_id: '5837' pubrep_id: '624' quality_controlled: '1' scopus_import: 1 series_title: Leibniz International Proceedings in Informatics status: public title: Infinite-state games with finitary conditions tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 23 year: '2013' ... --- _id: '2238' 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 author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Vojtěch full_name: Forejt, Vojtěch last_name: Forejt - first_name: Dominik full_name: Wojtczak, Dominik last_name: Wojtczak citation: 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 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' 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. ieee: K. Chatterjee, V. Forejt, and D. Wojtczak, “Multi-objective discounted reward verification in graphs and MDPs,” vol. 8312. Springer, pp. 228–242, 2013. ista: Chatterjee K, Forejt V, Wojtczak D. 2013. Multi-objective discounted reward verification in graphs and MDPs. 8312, 228–242. 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. conference: end_date: 2013-12-19 location: Stellenbosch, South Africa name: 'LPAR: Logic for Programming, Artificial Intelligence, and Reasoning' start_date: 2013-12-14 date_created: 2018-12-11T11:56:30Z date_published: 2013-12-01T00:00:00Z date_updated: 2020-08-11T10:09:42Z day: '01' department: - _id: KrCh doi: 10.1007/978-3-642-45221-5_17 ec_funded: 1 intvolume: ' 8312' language: - iso: eng month: '12' oa_version: None page: 228 - 242 project: - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' publication_status: published publisher: Springer publist_id: '4723' quality_controlled: '1' scopus_import: 1 series_title: Lecture Notes in Computer Science status: public title: Multi-objective discounted reward verification in graphs and MDPs type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 8312 year: '2013' ... --- _id: '2292' 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. alternative_title: - LNCS citation: 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 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' 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. 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. 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. short: K. Chatterjee, J. Sgall, eds., Mathematical Foundations of Computer Science 2013, Springer, 2013. conference: end_date: 2013-08-30 location: Klosterneuburg, Austria name: 'MFCS: Mathematical Foundations of Computer Science' start_date: 2013-08-26 date_created: 2018-12-11T11:56:48Z date_published: 2013-08-08T00:00:00Z date_updated: 2020-08-11T10:09:45Z day: '08' department: - _id: KrCh doi: 10.1007/978-3-642-40313-2 editor: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Jiri full_name: Sgall, Jiri last_name: Sgall intvolume: ' 8087' language: - iso: eng month: '08' oa_version: None page: VI - 854 publication_identifier: isbn: - 978-3-642-40312-5 publication_status: published publisher: Springer publist_id: '4636' quality_controlled: '1' scopus_import: 1 series_title: Lecture Notes in Computer Science status: public title: Mathematical Foundations of Computer Science 2013 type: conference_editor user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 8087 year: '2013' ... --- _id: '2299' abstract: - lang: eng 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.' author: - first_name: Yashdeep full_name: Godhal, Yashdeep id: 5B547124-EB61-11E9-8887-89D9C04DBDF5 last_name: Godhal - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 citation: 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' 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' 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.' 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.' 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.' 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. date_created: 2018-12-11T11:56:51Z date_published: 2013-10-01T00:00:00Z date_updated: 2021-01-12T06:56:37Z day: '01' ddc: - '000' department: - _id: KrCh - _id: ToHe doi: 10.1007/s10009-011-0207-9 file: - access_level: open_access checksum: 57b06a732dd8d6349190dba6b5b0d33b content_type: application/pdf creator: system date_created: 2018-12-12T10:11:53Z date_updated: 2020-07-14T12:45:37Z file_id: '4910' file_name: IST-2012-87-v1+1_Synthesis_of_AMBA_AHB_from_formal_specifications-_A_case_study.pdf file_size: 277372 relation: main_file file_date_updated: 2020-07-14T12:45:37Z has_accepted_license: '1' intvolume: ' 15' issue: 5-6 language: - iso: eng month: '10' oa: 1 oa_version: Submitted Version page: 585 - 601 project: - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: International Journal on Software Tools for Technology Transfer publication_status: published publisher: Springer publist_id: '4629' pubrep_id: '87' quality_controlled: '1' scopus_import: 1 status: public title: 'Synthesis of AMBA AHB from formal specification: A case study' type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 15 year: '2013' ... --- _id: '2446' 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. alternative_title: - LNCS author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Andreas full_name: Gaiser, Andreas last_name: Gaiser - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 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 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' 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. 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. 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. conference: end_date: 2013-07-19 location: St. Petersburg, Russia name: 'CAV: Computer Aided Verification' start_date: 2013-07-13 date_created: 2018-12-11T11:57:42Z date_published: 2013-07-01T00:00:00Z date_updated: 2020-08-11T10:09:47Z day: '01' department: - _id: KrCh doi: 10.1007/978-3-642-39799-8_37 ec_funded: 1 external_id: arxiv: - '1304.5281' intvolume: ' 8044' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1304.5281 month: '07' oa: 1 oa_version: Preprint page: 559 - 575 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication_status: published publisher: Springer publist_id: '4457' quality_controlled: '1' scopus_import: 1 series_title: Lecture Notes in Computer Science status: public title: Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 8044 year: '2013' ...