--- _id: '5453' alternative_title: - IST Austria Technical Report author: - first_name: Andreas full_name: Pavlogiannis, Andreas id: 49704004-F248-11E8-B48F-1D18A9856A87 last_name: Pavlogiannis orcid: 0000-0002-8943-0722 - first_name: Josef full_name: Tkadlec, Josef id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87 last_name: Tkadlec orcid: 0000-0002-1097-9684 - 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: Nowak, Martin last_name: Nowak citation: ama: Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. Arbitrarily Strong Amplifiers of Natural Selection. IST Austria; 2016. doi:10.15479/AT:IST-2017-749-v3-1 apa: Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. (2016). Arbitrarily strong amplifiers of natural selection. IST Austria. https://doi.org/10.15479/AT:IST-2017-749-v3-1 chicago: Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak. Arbitrarily Strong Amplifiers of Natural Selection. IST Austria, 2016. https://doi.org/10.15479/AT:IST-2017-749-v3-1. ieee: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, Arbitrarily strong amplifiers of natural selection. IST Austria, 2016. ista: Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Arbitrarily strong amplifiers of natural selection, IST Austria, 34p. mla: Pavlogiannis, Andreas, et al. Arbitrarily Strong Amplifiers of Natural Selection. IST Austria, 2016, doi:10.15479/AT:IST-2017-749-v3-1. short: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Arbitrarily Strong Amplifiers of Natural Selection, IST Austria, 2016. date_created: 2018-12-12T11:39:25Z date_published: 2016-12-30T00:00:00Z date_updated: 2023-02-23T12:27:07Z day: '30' ddc: - '000' department: - _id: KrCh doi: 10.15479/AT:IST-2017-749-v3-1 file: - access_level: open_access checksum: 83b0313dab3bff4bdb6ac38695026fda content_type: application/pdf creator: system date_created: 2018-12-12T11:53:13Z date_updated: 2020-07-14T12:46:59Z file_id: '5474' file_name: IST-2017-749-v3+1_main.pdf file_size: 1015647 relation: main_file file_date_updated: 2020-07-14T12:46:59Z has_accepted_license: '1' language: - iso: eng month: '12' oa: 1 oa_version: Published Version page: '34' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '755' related_material: record: - id: '5452' relation: earlier_version status: public status: public title: Arbitrarily strong amplifiers of natural selection type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2016' ... --- _id: '5451' alternative_title: - IST Austria Technical Report author: - first_name: Andreas full_name: Pavlogiannis, Andreas id: 49704004-F248-11E8-B48F-1D18A9856A87 last_name: Pavlogiannis orcid: 0000-0002-8943-0722 - first_name: Josef full_name: Tkadlec, Josef id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87 last_name: Tkadlec orcid: 0000-0002-1097-9684 - 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: Nowak, Martin last_name: Nowak citation: ama: Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. Strong Amplifiers of Natural Selection. IST Austria; 2016. doi:10.15479/AT:IST-2016-728-v1-1 apa: Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. (2016). Strong amplifiers of natural selection. IST Austria. https://doi.org/10.15479/AT:IST-2016-728-v1-1 chicago: Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak. Strong Amplifiers of Natural Selection. IST Austria, 2016. https://doi.org/10.15479/AT:IST-2016-728-v1-1. ieee: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, Strong amplifiers of natural selection. IST Austria, 2016. ista: Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Strong amplifiers of natural selection, IST Austria, 34p. mla: Pavlogiannis, Andreas, et al. Strong Amplifiers of Natural Selection. IST Austria, 2016, doi:10.15479/AT:IST-2016-728-v1-1. short: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Strong Amplifiers of Natural Selection, IST Austria, 2016. date_created: 2018-12-12T11:39:24Z date_published: 2016-12-30T00:00:00Z date_updated: 2023-02-23T12:27:05Z day: '30' ddc: - '000' department: - _id: KrCh doi: 10.15479/AT:IST-2016-728-v1-1 file: - access_level: open_access checksum: 7b8bb17c322c0556acba6ac169fa71c1 content_type: application/pdf creator: system date_created: 2018-12-12T11:53:04Z date_updated: 2020-07-14T12:46:59Z file_id: '5465' file_name: IST-2016-728-v1+1_main.pdf file_size: 1014732 relation: main_file file_date_updated: 2020-07-14T12:46:59Z has_accepted_license: '1' language: - iso: eng month: '12' oa: 1 oa_version: Published Version page: '34' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '728' status: public title: Strong amplifiers of natural selection type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2016' ... --- _id: '5448' abstract: - lang: eng text: "We present a new dynamic partial-order reduction method for stateless model checking of concurrent programs. A common approach for exploring program behaviors relies on enumerating the traces of the program, without storing the visited states (aka stateless exploration). As the number of distinct traces grows exponentially, dynamic partial-order reduction (DPOR) techniques have been successfully used to partition the space of traces into equivalence classes (Mazurkiewicz partitioning), with the goal of exploring only few representative traces from each class.\r\nWe introduce a new equivalence on traces under sequential consistency semantics, which we call the observation equivalence. Two traces are observationally equivalent if every read event observes the same write event in both traces. While the traditional Mazurkiewicz equivalence is control-centric, our new definition is data-centric. We show that our observation equivalence is coarser than the Mazurkiewicz equivalence, and in many cases even exponentially coarser. We devise a DPOR exploration of the trace space, called data-centric DPOR, based on the observation equivalence.\r\n1. For acyclic architectures, our algorithm is guaranteed to explore exactly one representative trace from each observation class, while spending polynomial time per class. Hence, our algorithm is optimal wrt the observation equivalence, and in several cases explores exponentially fewer traces than any enumerative method based on the Mazurkiewicz equivalence.\r\n2. For cyclic architectures, we consider an equivalence between traces which is finer than the observation equivalence; but coarser than the Mazurkiewicz equivalence, and in some cases is exponentially coarser. Our data-centric DPOR algorithm remains optimal under this trace equivalence. \r\nFinally, we perform a basic experimental comparison between the existing Mazurkiewicz-based DPOR and our data-centric DPOR on a set of academic benchmarks. Our results show a significant reduction in both running time and the number of explored equivalence classes." alternative_title: - IST Austria Technical Report author: - first_name: '1' full_name: Anonymous, 1 last_name: Anonymous - first_name: '2' full_name: Anonymous, 2 last_name: Anonymous - first_name: '3' full_name: Anonymous, 3 last_name: Anonymous - first_name: '4' full_name: Anonymous, 4 last_name: Anonymous citation: ama: Anonymous 1, Anonymous 2, Anonymous 3, Anonymous 4. Data-Centric Dynamic Partial Order Reduction. IST Austria; 2016. apa: Anonymous, 1, Anonymous, 2, Anonymous, 3, & Anonymous, 4. (2016). Data-centric dynamic partial order reduction. IST Austria. chicago: Anonymous, 1, 2 Anonymous, 3 Anonymous, and 4 Anonymous. Data-Centric Dynamic Partial Order Reduction. IST Austria, 2016. ieee: 1 Anonymous, 2 Anonymous, 3 Anonymous, and 4 Anonymous, Data-centric dynamic partial order reduction. IST Austria, 2016. ista: Anonymous 1, Anonymous 2, Anonymous 3, Anonymous 4. 2016. Data-centric dynamic partial order reduction, IST Austria, 20p. mla: Anonymous, 1, et al. Data-Centric Dynamic Partial Order Reduction. IST Austria, 2016. short: 1 Anonymous, 2 Anonymous, 3 Anonymous, 4 Anonymous, Data-Centric Dynamic Partial Order Reduction, IST Austria, 2016. date_created: 2018-12-12T11:39:23Z date_published: 2016-07-15T00:00:00Z date_updated: 2023-02-23T12:27:16Z day: '15' ddc: - '000' external_id: arxiv: - '1610.01188' file: - access_level: open_access checksum: 1d69252d66bcdf782615ddfb911d2957 content_type: application/pdf creator: system date_created: 2018-12-12T11:53:45Z date_updated: 2020-07-14T12:46:58Z file_id: '5506' file_name: IST-2016-620-v1+1_main.pdf file_size: 538881 relation: main_file - access_level: closed checksum: deabb0eb8f237cae4f9542b28b0b6eb2 content_type: text/plain creator: dernst date_created: 2019-05-10T13:30:40Z date_updated: 2020-07-14T12:46:58Z file_id: '6405' file_name: authornames.txt file_size: 121 relation: main_file file_date_updated: 2020-07-14T12:46:58Z has_accepted_license: '1' language: - iso: eng month: '07' oa: 1 oa_version: Published Version page: '20' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '620' related_material: record: - id: '10417' relation: later_version status: public - id: '5456' relation: later_version status: public status: public title: Data-centric dynamic partial order reduction type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2016' ... --- _id: '5452' alternative_title: - IST Austria Technical Report article_processing_charge: No author: - first_name: Andreas full_name: Pavlogiannis, Andreas id: 49704004-F248-11E8-B48F-1D18A9856A87 last_name: Pavlogiannis orcid: 0000-0002-8943-0722 - first_name: Josef full_name: Tkadlec, Josef id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87 last_name: Tkadlec orcid: 0000-0002-1097-9684 - 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: Nowak, Martin last_name: Nowak citation: ama: Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. Arbitrarily Strong Amplifiers of Natural Selection. IST Austria; 2016. doi:10.15479/AT:IST-2017-728-v2-1 apa: Pavlogiannis, A., Tkadlec, J., Chatterjee, K., & Nowak, M. (2016). Arbitrarily strong amplifiers of natural selection. IST Austria. https://doi.org/10.15479/AT:IST-2017-728-v2-1 chicago: Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin Nowak. Arbitrarily Strong Amplifiers of Natural Selection. IST Austria, 2016. https://doi.org/10.15479/AT:IST-2017-728-v2-1. ieee: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, Arbitrarily strong amplifiers of natural selection. IST Austria, 2016. ista: Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Arbitrarily strong amplifiers of natural selection, IST Austria, 32p. mla: Pavlogiannis, Andreas, et al. Arbitrarily Strong Amplifiers of Natural Selection. IST Austria, 2016, doi:10.15479/AT:IST-2017-728-v2-1. short: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Arbitrarily Strong Amplifiers of Natural Selection, IST Austria, 2016. date_created: 2018-12-12T11:39:25Z date_published: 2016-12-30T00:00:00Z date_updated: 2024-02-21T13:48:42Z day: '30' ddc: - '000' department: - _id: KrCh doi: 10.15479/AT:IST-2017-728-v2-1 ec_funded: 1 file: - access_level: open_access checksum: 58e895f26c82f560c0f0989bf8b08599 content_type: application/pdf creator: system date_created: 2018-12-12T11:52:59Z date_updated: 2020-07-14T12:46:59Z file_id: '5460' file_name: IST-2017-728-v2+1_main.pdf file_size: 811558 relation: main_file file_date_updated: 2020-07-14T12:46:59Z has_accepted_license: '1' language: - iso: eng month: '12' oa: 1 oa_version: Published Version page: '32' project: - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '750' related_material: record: - id: '5453' relation: later_version status: public - id: '5559' relation: popular_science status: public status: public title: Arbitrarily strong amplifiers of natural selection type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2016' ... --- _id: '5431' abstract: - lang: eng text: "We consider finite-state concurrent stochastic games, played by k>=2 players for an infinite number of rounds, where in every round, each player simultaneously and independently of the other players chooses an action, whereafter the successor state is determined by a probability distribution given by the current state and the chosen actions. We consider reachability objectives that given a target set of states require that some state in the target set is visited, and the dual safety objectives that given a target set require that only states in the target set are visited. We are interested in the complexity of stationary strategies measured by their patience, which is defined as the inverse of the smallest non-zero probability employed.\r\n\r\n Our main results are as follows: We show that in two-player zero-sum concurrent stochastic games (with reachability objective for one player and the complementary safety objective for the other player): (i) the optimal bound on the patience of optimal and epsilon-optimal strategies, for both players is doubly exponential; and (ii) even in games with a single non-absorbing state exponential (in the number of actions) patience is necessary. In general we study the class of non-zero-sum games admitting epsilon-Nash equilibria. We show that if there is at least one player with reachability objective, then doubly-exponential patience is needed in general for epsilon-Nash equilibrium strategies, whereas in contrast if all players have safety objectives, then the optimal bound on patience for epsilon-Nash equilibrium strategies is only exponential." 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: Kristoffer full_name: Hansen, Kristoffer last_name: Hansen citation: ama: Chatterjee K, Ibsen-Jensen R, Hansen K. The Patience of Concurrent Stochastic Games with Safety and Reachability Objectives. IST Austria; 2015. doi:10.15479/AT:IST-2015-322-v1-1 apa: Chatterjee, K., Ibsen-Jensen, R., & Hansen, K. (2015). The patience of concurrent stochastic games with safety and reachability objectives. IST Austria. https://doi.org/10.15479/AT:IST-2015-322-v1-1 chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Kristoffer Hansen. The Patience of Concurrent Stochastic Games with Safety and Reachability Objectives. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-322-v1-1. ieee: K. Chatterjee, R. Ibsen-Jensen, and K. Hansen, The patience of concurrent stochastic games with safety and reachability objectives. IST Austria, 2015. ista: Chatterjee K, Ibsen-Jensen R, Hansen K. 2015. The patience of concurrent stochastic games with safety and reachability objectives, IST Austria, 25p. mla: Chatterjee, Krishnendu, et al. The Patience of Concurrent Stochastic Games with Safety and Reachability Objectives. IST Austria, 2015, doi:10.15479/AT:IST-2015-322-v1-1. short: K. Chatterjee, R. Ibsen-Jensen, K. Hansen, The Patience of Concurrent Stochastic Games with Safety and Reachability Objectives, IST Austria, 2015. date_created: 2018-12-12T11:39:17Z date_published: 2015-02-19T00:00:00Z date_updated: 2021-01-12T08:02:13Z day: '19' ddc: - '005' - '519' department: - _id: KrCh doi: 10.15479/AT:IST-2015-322-v1-1 file: - access_level: open_access checksum: bfb858262c30445b8e472c40069178a2 content_type: application/pdf creator: system date_created: 2018-12-12T11:53:31Z date_updated: 2020-07-14T12:46:53Z file_id: '5491' file_name: IST-2015-322-v1+1_safetygames.pdf file_size: 661015 relation: main_file file_date_updated: 2020-07-14T12:46:53Z has_accepted_license: '1' language: - iso: eng month: '02' oa: 1 oa_version: Published Version page: '25' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '322' status: public title: The patience of concurrent stochastic games with safety and reachability objectives type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2015' ... --- _id: '5434' abstract: - lang: eng text: DEC-POMDPs extend POMDPs to a multi-agent setting, where several agents operate in an uncertain environment independently to achieve a joint objective. DEC-POMDPs have been studied with finite-horizon and infinite-horizon discounted-sum objectives, and there exist solvers both for exact and approximate solutions. In this work we consider Goal-DEC-POMDPs, where given a set of target states, the objective is to ensure that the target set is reached with minimal cost. We consider the indefinite-horizon (infinite-horizon with either discounted-sum, or undiscounted-sum, where absorbing goal states have zero-cost) problem. We present a new method to solve the problem that extends methods for finite-horizon DEC- POMDPs and the RTDP-Bel approach for POMDPs. We present experimental results on several examples, and show our approach presents promising results. alternative_title: - IST Austria Technical Report author: - first_name: '1' full_name: Anonymous, 1 last_name: Anonymous - first_name: '2' full_name: Anonymous, 2 last_name: Anonymous citation: ama: Anonymous 1, Anonymous 2. Optimal Cost Indefinite-Horizon Reachability in Goal DEC-POMDPs. IST Austria; 2015. apa: Anonymous, 1, & Anonymous, 2. (2015). Optimal cost indefinite-horizon reachability in goal DEC-POMDPs. IST Austria. chicago: Anonymous, 1, and 2 Anonymous. Optimal Cost Indefinite-Horizon Reachability in Goal DEC-POMDPs. IST Austria, 2015. ieee: 1 Anonymous and 2 Anonymous, Optimal cost indefinite-horizon reachability in goal DEC-POMDPs. IST Austria, 2015. ista: Anonymous 1, Anonymous 2. 2015. Optimal cost indefinite-horizon reachability in goal DEC-POMDPs, IST Austria, 16p. mla: Anonymous, 1, and 2 Anonymous. Optimal Cost Indefinite-Horizon Reachability in Goal DEC-POMDPs. IST Austria, 2015. short: 1 Anonymous, 2 Anonymous, Optimal Cost Indefinite-Horizon Reachability in Goal DEC-POMDPs, IST Austria, 2015. date_created: 2018-12-12T11:39:18Z date_published: 2015-02-19T00:00:00Z date_updated: 2020-07-14T23:04:59Z day: '19' ddc: - '000' file: - access_level: open_access checksum: 8542fd0b10aed7811cd41077b8ccb632 content_type: application/pdf creator: system date_created: 2018-12-12T11:53:14Z date_updated: 2020-07-14T12:46:53Z file_id: '5475' file_name: IST-2015-326-v1+1_main.pdf file_size: 378162 relation: main_file - access_level: closed checksum: 84c31c537bdaf7a91909f18d25d640ab content_type: text/plain creator: dernst date_created: 2019-04-16T13:00:33Z date_updated: 2020-07-14T12:46:53Z file_id: '6317' file_name: IST-2015-326-v1+2_authors.txt file_size: 64 relation: main_file file_date_updated: 2020-07-14T12:46:53Z has_accepted_license: '1' language: - iso: eng month: '02' oa: 1 oa_version: Published Version page: '16' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '326' status: public title: Optimal cost indefinite-horizon reachability in goal DEC-POMDPs type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2015' ... --- _id: '5429' abstract: - lang: eng text: "We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. \r\nThere have been two different views: (i) the expectation semantics, where the goal is to optimize the expected mean-payoff objective, and (ii) the satisfaction semantics, where the goal is to maximize the probability of runs such that the mean-payoff value stays above a given vector. \ \r\nWe consider the problem where the goal is to optimize the expectation under the constraint that the satisfaction semantics is ensured, and thus consider a generalization that unifies the existing semantics.\r\nOur problem captures the notion of optimization with respect to strategies that are risk-averse (i.e., ensures certain probabilistic guarantee).\r\nOur main results are algorithms for the decision problem which are always polynomial in the size of the MDP. We also show that an approximation of the Pareto-curve can be computed in time polynomial in the size of the MDP, and the approximation factor, but exponential in the number of dimensions.\r\nFinally, we present a complete characterization of the strategy complexity (in terms of memory bounds and randomization) required to solve our problem." 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: Zuzana full_name: Komarkova, Zuzana last_name: Komarkova - 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, Komarkova Z, Kretinsky J. Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. IST Austria; 2015. doi:10.15479/AT:IST-2015-318-v1-1 apa: Chatterjee, K., Komarkova, Z., & Kretinsky, J. (2015). Unifying two views on multiple mean-payoff objectives in Markov decision processes. IST Austria. https://doi.org/10.15479/AT:IST-2015-318-v1-1 chicago: Chatterjee, Krishnendu, Zuzana Komarkova, and Jan Kretinsky. Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-318-v1-1. ieee: K. Chatterjee, Z. Komarkova, and J. Kretinsky, Unifying two views on multiple mean-payoff objectives in Markov decision processes. IST Austria, 2015. ista: Chatterjee K, Komarkova Z, Kretinsky J. 2015. Unifying two views on multiple mean-payoff objectives in Markov decision processes, IST Austria, 41p. mla: Chatterjee, Krishnendu, et al. Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. IST Austria, 2015, doi:10.15479/AT:IST-2015-318-v1-1. short: K. Chatterjee, Z. Komarkova, J. Kretinsky, Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes, IST Austria, 2015. date_created: 2018-12-12T11:39:17Z date_published: 2015-01-12T00:00:00Z date_updated: 2023-02-23T12:26:16Z day: '12' ddc: - '004' department: - _id: KrCh doi: 10.15479/AT:IST-2015-318-v1-1 file: - access_level: open_access checksum: e4869a584567c506349abda9c8ec7db3 content_type: application/pdf creator: system date_created: 2018-12-12T11:54:11Z date_updated: 2020-07-14T12:46:52Z file_id: '5533' file_name: IST-2015-318-v1+1_main.pdf file_size: 689863 relation: main_file file_date_updated: 2020-07-14T12:46:52Z has_accepted_license: '1' language: - iso: eng month: '01' oa: 1 oa_version: Published Version page: '41' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '318' related_material: record: - id: '1657' relation: later_version status: public - id: '466' relation: later_version status: public - id: '5435' relation: later_version status: public status: public title: Unifying two views on multiple mean-payoff objectives in Markov decision processes type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2015' ... --- _id: '5435' abstract: - lang: eng text: "We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. \r\nThere have been two different views: (i) the expectation semantics, where the goal is to optimize the expected mean-payoff objective, and (ii) the satisfaction semantics, where the goal is to maximize the probability of runs such that the mean-payoff value stays above a given vector. \ \r\nWe consider the problem where the goal is to optimize the expectation under the constraint that the satisfaction semantics is ensured, and thus consider a generalization that unifies the existing semantics. Our problem captures the notion of optimization with respect to strategies that are risk-averse (i.e., ensures certain probabilistic guarantee).\r\nOur main results are algorithms for the decision problem which are always polynomial in the size of the MDP.\r\nWe also show that an approximation of the Pareto-curve can be computed in time polynomial in the size of the MDP, and the approximation factor, but exponential in the number of dimensions. Finally, we present a complete characterization of the strategy complexity (in terms of memory bounds and randomization) required to solve our problem." 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: Zuzana full_name: Komarkova, Zuzana last_name: Komarkova - 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, Komarkova Z, Kretinsky J. Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. IST Austria; 2015. doi:10.15479/AT:IST-2015-318-v2-1 apa: Chatterjee, K., Komarkova, Z., & Kretinsky, J. (2015). Unifying two views on multiple mean-payoff objectives in Markov decision processes. IST Austria. https://doi.org/10.15479/AT:IST-2015-318-v2-1 chicago: Chatterjee, Krishnendu, Zuzana Komarkova, and Jan Kretinsky. Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-318-v2-1. ieee: K. Chatterjee, Z. Komarkova, and J. Kretinsky, Unifying two views on multiple mean-payoff objectives in Markov decision processes. IST Austria, 2015. ista: Chatterjee K, Komarkova Z, Kretinsky J. 2015. Unifying two views on multiple mean-payoff objectives in Markov decision processes, IST Austria, 51p. mla: Chatterjee, Krishnendu, et al. Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. IST Austria, 2015, doi:10.15479/AT:IST-2015-318-v2-1. short: K. Chatterjee, Z. Komarkova, J. Kretinsky, Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes, IST Austria, 2015. date_created: 2018-12-12T11:39:19Z date_published: 2015-02-23T00:00:00Z date_updated: 2023-02-23T12:26:00Z day: '23' ddc: - '004' department: - _id: KrCh doi: 10.15479/AT:IST-2015-318-v2-1 file: - access_level: open_access checksum: 75284adec80baabdfe71ff9ebbc27445 content_type: application/pdf creator: system date_created: 2018-12-12T11:54:03Z date_updated: 2020-07-14T12:46:53Z file_id: '5525' file_name: IST-2015-318-v2+1_main.pdf file_size: 717630 relation: main_file file_date_updated: 2020-07-14T12:46:53Z has_accepted_license: '1' language: - iso: eng month: '02' oa: 1 oa_version: Published Version page: '51' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '327' related_material: record: - id: '1657' relation: later_version status: public - id: '466' relation: later_version status: public - id: '5429' relation: earlier_version status: public status: public title: Unifying two views on multiple mean-payoff objectives in Markov decision processes type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2015' ... --- _id: '5436' abstract: - lang: eng text: "Recently there has been a significant effort to handle quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, perhaps surprisingly, some basic system properties such as average response time cannot be expressed using weighted automata, nor in any other know decidable formalism. In this work, we introduce nested weighted automata as a natural extension of weighted automata which makes it possible to express important quantitative properties such as average response time.\r\nIn nested weighted automata, a master automaton spins off and collects results from weighted slave automata, each of which computes a quantity along a finite portion of an infinite word. Nested weighted automata can be viewed as the quantitative analogue of monitor automata, which are used in run-time verification. We establish an almost complete decidability picture for the basic decision problems about nested weighted automata, and illustrate their applicability in several domains. In particular, nested weighted automata can be used to decide average response time properties." 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; 2015. doi:10.15479/AT:IST-2015-170-v2-2 apa: Chatterjee, K., Henzinger, T. A., & Otop, J. (2015). Nested weighted automata. IST Austria. https://doi.org/10.15479/AT:IST-2015-170-v2-2 chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. Nested Weighted Automata. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-170-v2-2. ieee: K. Chatterjee, T. A. Henzinger, and J. Otop, Nested weighted automata. IST Austria, 2015. ista: Chatterjee K, Henzinger TA, Otop J. 2015. Nested weighted automata, IST Austria, 29p. mla: Chatterjee, Krishnendu, et al. Nested Weighted Automata. IST Austria, 2015, doi:10.15479/AT:IST-2015-170-v2-2. short: K. Chatterjee, T.A. Henzinger, J. Otop, Nested Weighted Automata, IST Austria, 2015. date_created: 2018-12-12T11:39:19Z date_published: 2015-04-24T00:00:00Z date_updated: 2023-02-23T12:25:21Z day: '24' ddc: - '000' department: - _id: KrCh - _id: ToHe doi: 10.15479/AT:IST-2015-170-v2-2 file: - access_level: open_access checksum: 3c402f47d3669c28d04d1af405a08e3f content_type: application/pdf creator: system date_created: 2018-12-12T11:54:19Z date_updated: 2020-07-14T12:46:54Z file_id: '5541' file_name: IST-2015-170-v2+2_report.pdf file_size: 569991 relation: main_file file_date_updated: 2020-07-14T12:46:54Z has_accepted_license: '1' language: - iso: eng month: '04' oa: 1 oa_version: Published Version page: '29' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '331' related_material: record: - id: '1656' relation: later_version status: public - id: '467' relation: later_version status: public - id: '5415' relation: earlier_version status: public status: public title: Nested weighted automata type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2015' ... --- _id: '5437' abstract: - lang: eng text: "We consider the core algorithmic problems related to verification of systems with respect to three classical quantitative properties, namely, the mean-payoff property, the ratio property, and the minimum initial credit for energy property. \r\nThe algorithmic problem given a graph and a quantitative property asks to compute the optimal value (the infimum value over all traces) from every node of the graph. We consider graphs with constant treewidth, and it is well-known that the control-flow graphs of most programs have constant treewidth. Let $n$ denote the number of nodes of a graph, $m$ the number of edges (for constant treewidth graphs $m=O(n)$) and $W$ the largest absolute value of the weights.\r\nOur main theoretical results are as follows.\r\nFirst, for constant treewidth graphs we present an algorithm that approximates the mean-payoff value within a multiplicative factor of $\\epsilon$ in time $O(n \\cdot \\log (n/\\epsilon))$ and linear space, as compared to the classical algorithms that require quadratic time. Second, for the ratio property we present an algorithm that for constant treewidth graphs works in time $O(n \\cdot \\log (|a\\cdot b|))=O(n\\cdot\\log (n\\cdot W))$, when the output is $\\frac{a}{b}$, as compared to the previously best known algorithm with running time $O(n^2 \\cdot \\log (n\\cdot W))$. Third, for the minimum initial credit problem we show that (i)~for general graphs the problem can be solved in $O(n^2\\cdot m)$ time and the associated decision problem can be solved in $O(n\\cdot m)$ time, improving the previous known $O(n^3\\cdot m\\cdot \\log (n\\cdot W))$ and $O(n^2 \\cdot m)$ bounds, respectively; and (ii)~for constant treewidth graphs we present an algorithm that requires $O(n\\cdot \\log n)$ time, improving the previous known $O(n^4 \\cdot \\log (n \\cdot W))$ bound.\r\nWe have implemented some of our algorithms and show that they present a significant speedup on standard benchmarks. " 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. Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs. IST Austria; 2015. doi:10.15479/AT:IST-2015-330-v2-1 apa: Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2015). Faster algorithms for quantitative verification in constant treewidth graphs. IST Austria. https://doi.org/10.15479/AT:IST-2015-330-v2-1 chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-330-v2-1. ieee: K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, Faster algorithms for quantitative verification in constant treewidth graphs. IST Austria, 2015. ista: Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2015. Faster algorithms for quantitative verification in constant treewidth graphs, IST Austria, 27p. mla: Chatterjee, Krishnendu, et al. Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs. IST Austria, 2015, doi:10.15479/AT:IST-2015-330-v2-1. short: K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs, IST Austria, 2015. date_created: 2018-12-12T11:39:19Z date_published: 2015-04-27T00:00:00Z date_updated: 2023-02-23T12:26:05Z day: '27' ddc: - '000' department: - _id: KrCh doi: 10.15479/AT:IST-2015-330-v2-1 file: - access_level: open_access checksum: f5917c20f84018b362d385c000a2e123 content_type: application/pdf creator: system date_created: 2018-12-12T11:53:12Z date_updated: 2020-07-14T12:46:54Z file_id: '5473' file_name: IST-2015-330-v2+1_main.pdf file_size: 1072137 relation: main_file file_date_updated: 2020-07-14T12:46:54Z 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: '333' related_material: record: - id: '1607' relation: later_version status: public - id: '5430' relation: earlier_version status: public status: public title: Faster algorithms for quantitative verification in constant treewidth graphs type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2015' ... --- _id: '5430' abstract: - lang: eng text: We consider the core algorithmic problems related to verification of systems with respect to three classical quantitative properties, namely, the mean- payoff property, the ratio property, and the minimum initial credit for energy property. The algorithmic problem given a graph and a quantitative property asks to compute the optimal value (the infimum value over all traces) from every node of the graph. We consider graphs with constant treewidth, and it is well-known that the control-flow graphs of most programs have constant treewidth. Let n denote the number of nodes of a graph, m the number of edges (for constant treewidth graphs m = O ( n ) ) and W the largest absolute value of the weights. Our main theoretical results are as follows. First, for constant treewidth graphs we present an algorithm that approximates the mean-payoff value within a mul- tiplicative factor of ∊ in time O ( n · log( n/∊ )) and linear space, as compared to the classical algorithms that require quadratic time. Second, for the ratio property we present an algorithm that for constant treewidth graphs works in time O ( n · log( | a · b · n | )) = O ( n · log( n · W )) , when the output is a b , as compared to the previously best known algorithm with running time O ( n 2 · log( n · W )) . Third, for the minimum initial credit problem we show that (i) for general graphs the problem can be solved in O ( n 2 · m ) time and the associated decision problem can be solved in O ( n · m ) time, improving the previous known O ( n 3 · m · log( n · W )) and O ( n 2 · m ) bounds, respectively; and (ii) for constant treewidth graphs we present an algorithm that requires O ( n · log n ) time, improving the previous known O ( n 4 · log( n · W )) bound. We have implemented some of our algorithms and show that they present a significant speedup on standard benchmarks. 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. Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs. IST Austria; 2015. doi:10.15479/AT:IST-2015-319-v1-1 apa: Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2015). Faster algorithms for quantitative verification in constant treewidth graphs. IST Austria. https://doi.org/10.15479/AT:IST-2015-319-v1-1 chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-319-v1-1. ieee: K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, Faster algorithms for quantitative verification in constant treewidth graphs. IST Austria, 2015. ista: Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2015. Faster algorithms for quantitative verification in constant treewidth graphs, IST Austria, 31p. mla: Chatterjee, Krishnendu, et al. Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs. IST Austria, 2015, doi:10.15479/AT:IST-2015-319-v1-1. short: K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs, IST Austria, 2015. date_created: 2018-12-12T11:39:17Z date_published: 2015-02-10T00:00:00Z date_updated: 2023-02-23T12:26:22Z day: '10' ddc: - '000' department: - _id: KrCh doi: 10.15479/AT:IST-2015-319-v1-1 file: - access_level: open_access checksum: 62c6ea01e342553dcafb88a070fb1ad5 content_type: application/pdf creator: system date_created: 2018-12-12T11:53:21Z date_updated: 2020-07-14T12:46:52Z file_id: '5482' file_name: IST-2015-319-v1+1_long.pdf file_size: 1089651 relation: main_file file_date_updated: 2020-07-14T12:46:52Z has_accepted_license: '1' language: - iso: eng month: '02' oa: 1 oa_version: Published Version page: '31' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '319' related_material: record: - id: '1607' relation: later_version status: public - id: '5437' relation: later_version status: public status: public title: Faster algorithms for quantitative verification in constant treewidth graphs type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2015' ... --- _id: '5439' abstract: - lang: eng text: 'The target discounted-sum problem is the following: Given a rational discount factor 0 < λ < 1 and three rational values a, b, and t, does there exist a finite or an infinite sequence w ε(a, b)∗ or w ε(a, b)w, such that Σ|w| i=0 w(i)λi equals t? The problem turns out to relate to many fields of mathematics and computer science, and its decidability question is surprisingly hard to solve. We solve the finite version of the problem, and show the hardness of the infinite version, linking it to various areas and open problems in mathematics and computer science: β-expansions, discounted-sum automata, piecewise affine maps, and generalizations of the Cantor set. We provide some partial results to the infinite version, among which are solutions to its restriction to eventually-periodic sequences and to the cases that λ λ 1/2 or λ = 1/n, for every n ε N. We use our results for solving some open problems on discounted-sum automata, among which are the exact-value problem for nondeterministic automata over finite words and the universality and inclusion problems for functional automata. ' alternative_title: - IST Austria Technical Report author: - first_name: Udi full_name: Boker, Udi id: 31E297B6-F248-11E8-B48F-1D18A9856A87 last_name: Boker - 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: Boker U, Henzinger TA, Otop J. The Target Discounted-Sum Problem. IST Austria; 2015. doi:10.15479/AT:IST-2015-335-v1-1 apa: Boker, U., Henzinger, T. A., & Otop, J. (2015). The target discounted-sum problem. IST Austria. https://doi.org/10.15479/AT:IST-2015-335-v1-1 chicago: Boker, Udi, Thomas A Henzinger, and Jan Otop. The Target Discounted-Sum Problem. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-335-v1-1. ieee: U. Boker, T. A. Henzinger, and J. Otop, The target discounted-sum problem. IST Austria, 2015. ista: Boker U, Henzinger TA, Otop J. 2015. The target discounted-sum problem, IST Austria, 20p. mla: Boker, Udi, et al. The Target Discounted-Sum Problem. IST Austria, 2015, doi:10.15479/AT:IST-2015-335-v1-1. short: U. Boker, T.A. Henzinger, J. Otop, The Target Discounted-Sum Problem, IST Austria, 2015. date_created: 2018-12-12T11:39:20Z date_published: 2015-05-18T00:00:00Z date_updated: 2023-02-23T10:08:48Z day: '18' ddc: - '004' - '512' - '513' department: - _id: ToHe doi: 10.15479/AT:IST-2015-335-v1-1 file: - access_level: open_access checksum: 40405907aa012acece1bc26cf0be554d content_type: application/pdf creator: system date_created: 2018-12-12T11:53:55Z date_updated: 2020-07-14T12:46:55Z file_id: '5517' file_name: IST-2015-335-v1+1_report.pdf file_size: 589619 relation: main_file file_date_updated: 2020-07-14T12:46:55Z has_accepted_license: '1' language: - iso: eng month: '05' oa: 1 oa_version: Published Version page: '20' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '335' related_material: record: - id: '1659' relation: later_version status: public status: public title: The target discounted-sum problem type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2015' ... --- _id: '5438' abstract: - lang: eng text: "The edit distance between two words w1, w2 is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform w1 to w2. The edit distance generalizes to languages L1, L2, where the edit distance is the minimal number k such that for every word from L1 there exists a word in L2 with edit distance at most k. We study the edit distance computation problem between pushdown automata and their subclasses.\r\nThe problem of computing edit distance to a pushdown automaton is undecidable, and in practice, the interesting question is to compute the edit distance from a pushdown automaton (the implementation, a standard model for programs with recursion) to a regular language (the specification). In this work, we present a complete picture of decidability and complexity for deciding whether, for a given threshold k, the edit distance from a pushdown automaton to a finite automaton is at most k. " 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: Rasmus full_name: Ibsen-Jensen, Rasmus id: 3B699956-F248-11E8-B48F-1D18A9856A87 last_name: Ibsen-Jensen orcid: 0000-0003-4783-0389 - first_name: Jan full_name: Otop, Jan id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87 last_name: Otop citation: ama: Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. Edit Distance for Pushdown Automata. IST Austria; 2015. doi:10.15479/AT:IST-2015-334-v1-1 apa: Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., & Otop, J. (2015). Edit distance for pushdown automata. IST Austria. https://doi.org/10.15479/AT:IST-2015-334-v1-1 chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan Otop. Edit Distance for Pushdown Automata. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-334-v1-1. ieee: K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, Edit distance for pushdown automata. IST Austria, 2015. ista: Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2015. Edit distance for pushdown automata, IST Austria, 15p. mla: Chatterjee, Krishnendu, et al. Edit Distance for Pushdown Automata. IST Austria, 2015, doi:10.15479/AT:IST-2015-334-v1-1. short: K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, Edit Distance for Pushdown Automata, IST Austria, 2015. date_created: 2018-12-12T11:39:20Z date_published: 2015-05-05T00:00:00Z date_updated: 2023-02-23T12:20:08Z day: '05' ddc: - '004' department: - _id: KrCh doi: 10.15479/AT:IST-2015-334-v1-1 file: - access_level: open_access checksum: 8a5f2d77560e552af87eb1982437a43b content_type: application/pdf creator: system date_created: 2018-12-12T11:53:56Z date_updated: 2020-07-14T12:46:55Z file_id: '5518' file_name: IST-2015-334-v1+1_report.pdf file_size: 422573 relation: main_file file_date_updated: 2020-07-14T12:46:55Z has_accepted_license: '1' language: - iso: eng month: '05' oa: 1 oa_version: Published Version page: '15' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '334' related_material: record: - id: '1610' relation: later_version status: public - id: '465' relation: later_version status: public status: public title: Edit distance for pushdown automata type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2015' ... --- _id: '5440' abstract: - lang: eng text: 'Evolution occurs in populations of reproducing individuals. The structure of the population affects the outcome of the evolutionary process. Evolutionary graph theory is a powerful approach to study this phenomenon. There are two graphs. The interaction graph specifies who interacts with whom for payoff in the context of evolution. The replacement graph specifies who competes with whom for reproduction. The vertices of the two graphs are the same, and each vertex corresponds to an individual of the population. The fitness (or the reproductive rate) is a non-negative number, and depends on the payoff. A key quantity is the fixation probability of a new mutant. It is defined as the probability that a newly introduced mutant (on a single vertex) generates a lineage of offspring which eventually takes over the entire population of resident individuals. The basic computational questions are as follows: (i) the qualitative question asks whether the fixation probability is positive; and (ii) the quantitative approximation question asks for an approximation of the fixation probability. Our main results are as follows: First, we consider a special case of the general problem, where the residents do not reproduce. We show that the qualitative question is NP-complete, and the quantitative approximation question is #P-complete, and the hardness results hold even in the special case where the interaction and the replacement graphs coincide. Second, we show that in general both the qualitative and the quantitative approximation questions are PSPACE-complete. The PSPACE-hardness result for quantitative approximation holds even when the fitness is always positive.' 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 Evolutionary Games on Graphs. IST Austria; 2015. doi:10.15479/AT:IST-2015-323-v2-2 apa: Chatterjee, K., Ibsen-Jensen, R., & Nowak, M. (2015). The complexity of evolutionary games on graphs. IST Austria. https://doi.org/10.15479/AT:IST-2015-323-v2-2 chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Martin Nowak. The Complexity of Evolutionary Games on Graphs. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-323-v2-2. ieee: K. Chatterjee, R. Ibsen-Jensen, and M. Nowak, The complexity of evolutionary games on graphs. IST Austria, 2015. ista: Chatterjee K, Ibsen-Jensen R, Nowak M. 2015. The complexity of evolutionary games on graphs, IST Austria, 18p. mla: Chatterjee, Krishnendu, et al. The Complexity of Evolutionary Games on Graphs. IST Austria, 2015, doi:10.15479/AT:IST-2015-323-v2-2. short: K. Chatterjee, R. Ibsen-Jensen, M. Nowak, The Complexity of Evolutionary Games on Graphs, IST Austria, 2015. date_created: 2018-12-12T11:39:21Z date_published: 2015-06-16T00:00:00Z date_updated: 2023-02-23T12:26:10Z day: '16' ddc: - '005' - '576' department: - _id: KrCh doi: 10.15479/AT:IST-2015-323-v2-2 file: - access_level: open_access checksum: 66aace7d367032af97c15e35c9be9636 content_type: application/pdf creator: system date_created: 2018-12-12T11:53:23Z date_updated: 2020-07-14T12:46:56Z file_id: '5484' file_name: IST-2015-323-v2+2_main.pdf file_size: 466161 relation: main_file file_date_updated: 2020-07-14T12:46:56Z has_accepted_license: '1' language: - iso: eng month: '06' oa: 1 oa_version: Published Version page: '18' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '338' related_material: record: - id: '5421' relation: earlier_version status: public - id: '5432' relation: earlier_version status: public status: public title: The complexity of evolutionary games on graphs type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2015' ... --- _id: '5432' 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. \r\nThe vertices of the two graphs are the same, and each vertex corresponds to an individual of the population. 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. \r\nOur main results are:\r\n(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).\r\n(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.\r\n" 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 Evolutionary Games on Graphs. IST Austria; 2015. doi:10.15479/AT:IST-2015-323-v1-1 apa: Chatterjee, K., Ibsen-Jensen, R., & Nowak, M. (2015). The complexity of evolutionary games on graphs. IST Austria. https://doi.org/10.15479/AT:IST-2015-323-v1-1 chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Martin Nowak. The Complexity of Evolutionary Games on Graphs. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-323-v1-1. ieee: K. Chatterjee, R. Ibsen-Jensen, and M. Nowak, The complexity of evolutionary games on graphs. IST Austria, 2015. ista: Chatterjee K, Ibsen-Jensen R, Nowak M. 2015. The complexity of evolutionary games on graphs, IST Austria, 29p. mla: Chatterjee, Krishnendu, et al. The Complexity of Evolutionary Games on Graphs. IST Austria, 2015, doi:10.15479/AT:IST-2015-323-v1-1. short: K. Chatterjee, R. Ibsen-Jensen, M. Nowak, The Complexity of Evolutionary Games on Graphs, IST Austria, 2015. date_created: 2018-12-12T11:39:18Z date_published: 2015-02-19T00:00:00Z date_updated: 2023-02-23T12:26:33Z day: '19' ddc: - '005' - '576' department: - _id: KrCh doi: 10.15479/AT:IST-2015-323-v1-1 file: - access_level: open_access checksum: 546c1b291d545e7b24aaaf4199dac671 content_type: application/pdf creator: system date_created: 2018-12-12T11:53:57Z date_updated: 2020-07-14T12:46:53Z file_id: '5519' file_name: IST-2015-323-v1+1_main.pdf file_size: 576347 relation: main_file file_date_updated: 2020-07-14T12:46:53Z has_accepted_license: '1' language: - iso: eng month: '02' oa: 1 oa_version: Published Version page: '29' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '323' related_material: record: - id: '5421' relation: earlier_version status: public - id: '5440' relation: later_version status: public status: public title: The complexity of evolutionary games on graphs type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2015' ... --- _id: '5444' abstract: - lang: eng text: A comprehensive understanding of the clonal evolution of cancer is critical for understanding neoplasia. Genome-wide sequencing data enables evolutionary studies at unprecedented depth. However, classical phylogenetic methods often struggle with noisy sequencing data of impure DNA samples and fail to detect subclones that have different evolutionary trajectories. We have developed a tool, called Treeomics, that allows us to reconstruct the phylogeny of a cancer with commonly available sequencing technologies. Using Bayesian inference and Integer Linear Programming, robust phylogenies consistent with the biological processes underlying cancer evolution were obtained for pancreatic, ovarian, and prostate cancers. Furthermore, Treeomics correctly identified sequencing artifacts such as those resulting from low statistical power; nearly 7% of variants were misclassified by conventional statistical methods. These artifacts can skew phylogenies by creating illusory tumor heterogeneity among distinct samples. Importantly, we show that the evolutionary trees generated with Treeomics are mathematically optimal. alternative_title: - IST Austria Technical Report author: - first_name: Johannes full_name: Reiter, Johannes id: 4A918E98-F248-11E8-B48F-1D18A9856A87 last_name: Reiter orcid: 0000-0002-0170-7353 - first_name: Alvin full_name: Makohon-Moore, Alvin last_name: Makohon-Moore - first_name: Jeffrey full_name: Gerold, Jeffrey last_name: Gerold - first_name: Ivana full_name: Bozic, Ivana last_name: Bozic - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Christine full_name: Iacobuzio-Donahue, Christine last_name: Iacobuzio-Donahue - first_name: Bert full_name: Vogelstein, Bert last_name: Vogelstein - first_name: Martin full_name: Nowak, Martin last_name: Nowak citation: ama: Reiter J, Makohon-Moore A, Gerold J, et al. Reconstructing Robust Phylogenies of Metastatic Cancers. IST Austria; 2015. doi:10.15479/AT:IST-2015-399-v1-1 apa: Reiter, J., Makohon-Moore, A., Gerold, J., Bozic, I., Chatterjee, K., Iacobuzio-Donahue, C., … Nowak, M. (2015). Reconstructing robust phylogenies of metastatic cancers. IST Austria. https://doi.org/10.15479/AT:IST-2015-399-v1-1 chicago: Reiter, Johannes, Alvin Makohon-Moore, Jeffrey Gerold, Ivana Bozic, Krishnendu Chatterjee, Christine Iacobuzio-Donahue, Bert Vogelstein, and Martin Nowak. Reconstructing Robust Phylogenies of Metastatic Cancers. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-399-v1-1. ieee: J. Reiter et al., Reconstructing robust phylogenies of metastatic cancers. IST Austria, 2015. ista: Reiter J, Makohon-Moore A, Gerold J, Bozic I, Chatterjee K, Iacobuzio-Donahue C, Vogelstein B, Nowak M. 2015. Reconstructing robust phylogenies of metastatic cancers, IST Austria, 25p. mla: Reiter, Johannes, et al. Reconstructing Robust Phylogenies of Metastatic Cancers. IST Austria, 2015, doi:10.15479/AT:IST-2015-399-v1-1. short: J. Reiter, A. Makohon-Moore, J. Gerold, I. Bozic, K. Chatterjee, C. Iacobuzio-Donahue, B. Vogelstein, M. Nowak, Reconstructing Robust Phylogenies of Metastatic Cancers, IST Austria, 2015. date_created: 2018-12-12T11:39:22Z date_published: 2015-12-30T00:00:00Z date_updated: 2020-07-14T23:05:07Z day: '30' ddc: - '000' - '576' department: - _id: KrCh doi: 10.15479/AT:IST-2015-399-v1-1 file: - access_level: open_access checksum: c47d33bdda06181753c0af36f16e7b5d content_type: application/pdf creator: system date_created: 2018-12-12T11:53:24Z date_updated: 2020-07-14T12:46:58Z file_id: '5485' file_name: IST-2015-399-v1+1_treeomics.pdf file_size: 3533200 relation: main_file file_date_updated: 2020-07-14T12:46:58Z has_accepted_license: '1' language: - iso: eng month: '12' oa: 1 oa_version: Published Version page: '25' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '399' status: public title: Reconstructing robust phylogenies of metastatic cancers type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2015' ... --- _id: '5443' abstract: - lang: eng text: POMDPs are standard models for probabilistic planning problems, where an agent interacts with an uncertain environment. We study the problem of almost-sure reachability, where given a set of target states, the question is to decide whether there is a policy to ensure that the target set is reached with probability 1 (almost-surely). While in general the problem is EXPTIME-complete, in many practical cases policies with a small amount of memory suffice. Moreover, the existing solution to the problem is explicit, which first requires to construct explicitly an exponential reduction to a belief-support MDP. In this work, we first study the existence of observation-stationary strategies, which is NP-complete, and then small-memory strategies. We present a symbolic algorithm by an efficient encoding to SAT and using a SAT solver for the problem. We report experimental results demonstrating the scalability of our symbolic (SAT-based) approach. 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: Jessica full_name: Davies, Jessica id: 378E0060-F248-11E8-B48F-1D18A9856A87 last_name: Davies citation: ama: Chatterjee K, Chmelik M, Davies J. A Symbolic SAT-Based Algorithm for Almost-Sure Reachability with Small Strategies in POMDPs. IST Austria; 2015. doi:10.15479/AT:IST-2015-325-v2-1 apa: Chatterjee, K., Chmelik, M., & Davies, J. (2015). A symbolic SAT-based algorithm for almost-sure reachability with small strategies in POMDPs. IST Austria. https://doi.org/10.15479/AT:IST-2015-325-v2-1 chicago: Chatterjee, Krishnendu, Martin Chmelik, and Jessica Davies. A Symbolic SAT-Based Algorithm for Almost-Sure Reachability with Small Strategies in POMDPs. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-325-v2-1. ieee: K. Chatterjee, M. Chmelik, and J. Davies, A symbolic SAT-based algorithm for almost-sure reachability with small strategies in POMDPs. IST Austria, 2015. ista: Chatterjee K, Chmelik M, Davies J. 2015. A symbolic SAT-based algorithm for almost-sure reachability with small strategies in POMDPs, IST Austria, 23p. mla: Chatterjee, Krishnendu, et al. A Symbolic SAT-Based Algorithm for Almost-Sure Reachability with Small Strategies in POMDPs. IST Austria, 2015, doi:10.15479/AT:IST-2015-325-v2-1. short: K. Chatterjee, M. Chmelik, J. Davies, A Symbolic SAT-Based Algorithm for Almost-Sure Reachability with Small Strategies in POMDPs, IST Austria, 2015. date_created: 2018-12-12T11:39:22Z date_published: 2015-11-06T00:00:00Z date_updated: 2023-02-21T16:24:05Z day: '06' ddc: - '000' department: - _id: KrCh doi: 10.15479/AT:IST-2015-325-v2-1 file: - access_level: open_access checksum: f0fa31ad8161ed655137e94012123ef9 content_type: application/pdf creator: system date_created: 2018-12-12T11:53:05Z date_updated: 2020-07-14T12:46:57Z file_id: '5466' file_name: IST-2015-325-v2+1_main.pdf file_size: 412379 relation: main_file file_date_updated: 2020-07-14T12:46:57Z has_accepted_license: '1' language: - iso: eng month: '11' oa: 1 oa_version: Published Version page: '23' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '362' related_material: record: - id: '1166' relation: later_version status: public status: public title: A symbolic SAT-based algorithm for almost-sure reachability with small strategies in POMDPs type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2015' ... --- _id: '5441' abstract: - lang: eng text: We study algorithmic questions for concurrent systems where the transitions are labeled from a complete, closed semiring, and path properties are algebraic with semiring operations. The algebraic path properties can model dataflow analysis problems, the shortest path problem, and many other natural problems that arise in program analysis. We consider that each component of the concurrent system is a graph with constant treewidth, a property satisfied by the controlflow graphs of most programs. We allow for multiple possible queries, which arise naturally in demand driven dataflow analysis. The study of multiple queries allows us to consider the tradeoff between the resource usage of the one-time preprocessing and for each individual query. The traditional approach constructs the product graph of all components and applies the best-known graph algorithm on the product. In this approach, even the answer to a single query requires the transitive closure (i.e., the results of all possible queries), which provides no room for tradeoff between preprocessing and query time. Our main contributions are algorithms that significantly improve the worst-case running time of the traditional approach, and provide various tradeoffs depending on the number of queries. For example, in a concurrent system of two components, the traditional approach requires hexic time in the worst case for answering one query as well as computing the transitive closure, whereas we show that with one-time preprocessing in almost cubic time, each subsequent query can be answered in at most linear time, and even the transitive closure can be computed in almost quartic time. Furthermore, we establish conditional optimality results showing that the worst-case running time of our algorithms cannot be improved without achieving major breakthroughs in graph algorithms (i.e., improving the worst-case bound for the shortest path problem in general graphs). Preliminary experimental results show that our algorithms perform favorably on several benchmarks. 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: Amir full_name: Goharshady, Amir id: 391365CE-F248-11E8-B48F-1D18A9856A87 last_name: Goharshady orcid: 0000-0003-1702-6584 - 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, Goharshady AK, Pavlogiannis A. Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components. IST Austria; 2015. doi:10.15479/AT:IST-2015-340-v1-1 apa: Chatterjee, K., Ibsen-Jensen, R., Goharshady, A. K., & Pavlogiannis, A. (2015). Algorithms for algebraic path properties in concurrent systems of constant treewidth components. IST Austria. https://doi.org/10.15479/AT:IST-2015-340-v1-1 chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Amir Kafshdar Goharshady, and Andreas Pavlogiannis. Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-340-v1-1. ieee: K. Chatterjee, R. Ibsen-Jensen, A. K. Goharshady, and A. Pavlogiannis, Algorithms for algebraic path properties in concurrent systems of constant treewidth components. IST Austria, 2015. ista: Chatterjee K, Ibsen-Jensen R, Goharshady AK, Pavlogiannis A. 2015. Algorithms for algebraic path properties in concurrent systems of constant treewidth components, IST Austria, 24p. mla: Chatterjee, Krishnendu, et al. Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components. IST Austria, 2015, doi:10.15479/AT:IST-2015-340-v1-1. short: K. Chatterjee, R. Ibsen-Jensen, A.K. Goharshady, A. Pavlogiannis, Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components, IST Austria, 2015. date_created: 2018-12-12T11:39:21Z date_published: 2015-07-11T00:00:00Z date_updated: 2023-09-19T14:36:19Z day: '11' ddc: - '000' department: - _id: KrCh doi: 10.15479/AT:IST-2015-340-v1-1 file: - access_level: open_access checksum: df383dc62c94d7b2ea639aba088a76c6 content_type: application/pdf creator: system date_created: 2018-12-12T11:54:09Z date_updated: 2020-07-14T12:46:56Z file_id: '5531' file_name: IST-2015-340-v1+1_main.pdf file_size: 861396 relation: main_file file_date_updated: 2020-07-14T12:46:56Z has_accepted_license: '1' language: - iso: eng month: '07' oa: 1 oa_version: Published Version page: '24' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '340' related_material: record: - id: '1437' relation: later_version status: public - id: '5442' relation: earlier_version status: public - id: '6009' relation: later_version status: public status: public title: Algorithms for algebraic path properties in concurrent systems of constant treewidth components type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2015' ... --- _id: '5442' abstract: - lang: eng text: "We study algorithmic questions for concurrent systems where the transitions are labeled from a complete, closed semiring, and path properties are algebraic with semiring operations. The algebraic path properties can model dataflow analysis problems, the shortest path problem, and many other natural properties that arise in program analysis.\r\nWe consider that each component of the concurrent system is a graph with constant treewidth, and it is known that the controlflow graphs of most programs have constant treewidth. We allow for multiple possible queries, which arise naturally in demand driven dataflow analysis problems (e.g., alias analysis). The study of multiple queries allows us to consider the tradeoff between the resource usage of the \\emph{one-time} preprocessing and for \\emph{each individual} query. The traditional approaches construct the product graph of all components and apply the best-known graph algorithm on the product. In the traditional approach, even the answer to a single query requires the transitive closure computation (i.e., the results of all possible queries), which provides no room for tradeoff between preprocessing and query time.\r\n\r\nOur main contributions are algorithms that significantly improve the worst-case running time of the traditional approach, and provide various tradeoffs depending on the number of queries. For example, in a concurrent system of two components, the traditional approach requires hexic time in the worst case for answering one query as well as computing the transitive closure, whereas we show that with one-time preprocessing in almost cubic time, \r\neach subsequent query can be answered in at most linear time, and even the transitive closure can be computed in almost quartic time. Furthermore, we establish conditional optimality results that show that the worst-case running times of our algorithms cannot be improved without achieving major breakthroughs in graph algorithms (such as improving \r\nthe worst-case bounds for the shortest path problem in general graphs whose current best-known bound has not been improved in five decades). Finally, we provide a prototype implementation of our algorithms which significantly outperforms the existing algorithmic methods on several benchmarks." alternative_title: - IST Austria Technical Report author: - first_name: '1' full_name: Anonymous, 1 last_name: Anonymous - first_name: '2' full_name: Anonymous, 2 last_name: Anonymous - first_name: '3' full_name: Anonymous, 3 last_name: Anonymous - first_name: '4' full_name: Anonymous, 4 last_name: Anonymous citation: ama: Anonymous 1, Anonymous 2, Anonymous 3, Anonymous 4. Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components. IST Austria; 2015. apa: Anonymous, 1, Anonymous, 2, Anonymous, 3, & Anonymous, 4. (2015). Algorithms for algebraic path properties in concurrent systems of constant treewidth components. IST Austria. chicago: Anonymous, 1, 2 Anonymous, 3 Anonymous, and 4 Anonymous. Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components. IST Austria, 2015. ieee: 1 Anonymous, 2 Anonymous, 3 Anonymous, and 4 Anonymous, Algorithms for algebraic path properties in concurrent systems of constant treewidth components. IST Austria, 2015. ista: Anonymous 1, Anonymous 2, Anonymous 3, Anonymous 4. 2015. Algorithms for algebraic path properties in concurrent systems of constant treewidth components, IST Austria, 22p. mla: Anonymous, 1, et al. Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components. IST Austria, 2015. short: 1 Anonymous, 2 Anonymous, 3 Anonymous, 4 Anonymous, Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components, IST Austria, 2015. date_created: 2018-12-12T11:39:21Z date_published: 2015-07-14T00:00:00Z date_updated: 2023-09-19T14:36:19Z day: '14' ddc: - '000' file: - access_level: open_access checksum: 98fd936102f3e057fc321ef6d316001d content_type: application/pdf creator: system date_created: 2018-12-12T11:53:37Z date_updated: 2020-07-14T12:46:57Z file_id: '5498' file_name: IST-2015-343-v2+1_main.pdf file_size: 658747 relation: main_file - access_level: closed checksum: b31d09b1241b59c75e1f42dadf09d258 content_type: text/plain creator: dernst date_created: 2019-04-16T12:36:08Z date_updated: 2020-07-14T12:46:57Z file_id: '6316' file_name: IST-2015-343-v2+2_anonymous.txt file_size: 139 relation: main_file file_date_updated: 2020-07-14T12:46:57Z has_accepted_license: '1' language: - iso: eng month: '07' oa: 1 oa_version: Published Version page: '22' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '344' related_material: record: - id: '1437' relation: later_version status: public - id: '5441' relation: later_version status: public - id: '6009' relation: later_version status: public scopus_import: 1 status: public title: Algorithms for algebraic path properties in concurrent systems of constant treewidth components type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2015' ... --- _id: '5411' abstract: - lang: eng text: "Model-based testing is a promising technology for black-box software and hardware testing, in which test cases are generated automatically from high-level specifications. Nowadays, systems typically consist of multiple interacting components and, due to their complexity, testing presents a considerable portion of the effort and cost in the design process. Exploiting the compositional structure of system specifications can considerably reduce the effort in model-based testing. Moreover, inferring properties about the system from testing its individual components allows the designer to reduce the amount of integration testing.\r\nIn this paper, we study compositional properties of the IOCO-testing theory. We propose a new approach to composition and hiding operations, inspired by contract-based design and interface theories. These operations preserve behaviors that are compatible under composition and hiding, and prune away incompatible ones. The resulting specification characterizes the input sequences for which the unit testing of components is sufficient to infer the correctness of component integration without the need for further tests. We provide a methodology that uses these results to minimize integration testing effort, but also to detect potential weaknesses in specifications. While we focus on asynchronous models and the IOCO conformance relation, the resulting methodology can be applied to a broader class of systems." alternative_title: - IST Austria Technical Report author: - first_name: Przemyslaw full_name: Daca, Przemyslaw id: 49351290-F248-11E8-B48F-1D18A9856A87 last_name: Daca - 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: Willibald full_name: Krenn, Willibald last_name: Krenn - first_name: Dejan full_name: Nickovic, Dejan id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87 last_name: Nickovic citation: ama: Daca P, Henzinger TA, Krenn W, Nickovic D. Compositional Specifications for IOCO Testing. IST Austria; 2014. doi:10.15479/AT:IST-2014-148-v2-1 apa: Daca, P., Henzinger, T. A., Krenn, W., & Nickovic, D. (2014). Compositional specifications for IOCO testing. IST Austria. https://doi.org/10.15479/AT:IST-2014-148-v2-1 chicago: Daca, Przemyslaw, Thomas A Henzinger, Willibald Krenn, and Dejan Nickovic. Compositional Specifications for IOCO Testing. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-148-v2-1. ieee: P. Daca, T. A. Henzinger, W. Krenn, and D. Nickovic, Compositional specifications for IOCO testing. IST Austria, 2014. ista: Daca P, Henzinger TA, Krenn W, Nickovic D. 2014. Compositional specifications for IOCO testing, IST Austria, 20p. mla: Daca, Przemyslaw, et al. Compositional Specifications for IOCO Testing. IST Austria, 2014, doi:10.15479/AT:IST-2014-148-v2-1. short: P. Daca, T.A. Henzinger, W. Krenn, D. Nickovic, Compositional Specifications for IOCO Testing, IST Austria, 2014. date_created: 2018-12-12T11:39:11Z date_published: 2014-01-28T00:00:00Z date_updated: 2023-02-23T10:31:07Z day: '28' ddc: - '000' department: - _id: ToHe doi: 10.15479/AT:IST-2014-148-v2-1 file: - access_level: open_access checksum: 0e03aba625cc334141a3148432aa5760 content_type: application/pdf creator: system date_created: 2018-12-12T11:54:21Z date_updated: 2020-07-14T12:46:46Z file_id: '5543' file_name: IST-2014-148-v2+1_main_tr.pdf file_size: 534732 relation: main_file file_date_updated: 2020-07-14T12:46:46Z has_accepted_license: '1' language: - iso: eng month: '01' oa: 1 oa_version: Published Version page: '20' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '152' related_material: record: - id: '2167' relation: later_version status: public status: public title: Compositional specifications for IOCO testing type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2014' ... --- _id: '5413' abstract: - lang: eng text: "We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems. We focus on qualitative properties for MDPs that can express that desired behaviors of the system arise almost-surely (with probability 1) or with positive probability.\r\nWe introduce a new simulation relation to capture the refinement relation of MDPs with respect to qualitative properties, and present discrete graph theoretic algorithms with quadratic complexity to compute the simulation relation.\r\nWe present an automated technique for assume-guarantee style reasoning for compositional analysis of MDPs with qualitative properties by giving a counter-example 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: - 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: Przemyslaw full_name: Daca, Przemyslaw id: 49351290-F248-11E8-B48F-1D18A9856A87 last_name: Daca - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik citation: ama: Chatterjee K, Daca P, Chmelik M. CEGAR for Qualitative Analysis of Probabilistic Systems. IST Austria; 2014. doi:10.15479/AT:IST-2014-153-v2-2 apa: Chatterjee, K., Daca, P., & Chmelik, M. (2014). CEGAR for qualitative analysis of probabilistic systems. IST Austria. https://doi.org/10.15479/AT:IST-2014-153-v2-2 chicago: Chatterjee, Krishnendu, Przemyslaw Daca, and Martin Chmelik. CEGAR for Qualitative Analysis of Probabilistic Systems. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-153-v2-2. ieee: K. Chatterjee, P. Daca, and M. Chmelik, CEGAR for qualitative analysis of probabilistic systems. IST Austria, 2014. ista: Chatterjee K, Daca P, Chmelik M. 2014. CEGAR for qualitative analysis of probabilistic systems, IST Austria, 33p. mla: Chatterjee, Krishnendu, et al. CEGAR for Qualitative Analysis of Probabilistic Systems. IST Austria, 2014, doi:10.15479/AT:IST-2014-153-v2-2. short: K. Chatterjee, P. Daca, M. Chmelik, CEGAR for Qualitative Analysis of Probabilistic Systems, IST Austria, 2014. date_created: 2018-12-12T11:39:11Z date_published: 2014-02-06T00:00:00Z date_updated: 2023-02-23T12:25:18Z day: '06' ddc: - '000' department: - _id: KrCh doi: 10.15479/AT:IST-2014-153-v2-2 file: - access_level: open_access checksum: ce4967a184d84863eec76c66cbac1614 content_type: application/pdf creator: system date_created: 2018-12-12T11:54:17Z date_updated: 2020-07-14T12:46:47Z file_id: '5539' file_name: IST-2014-153-v2+2_main.pdf file_size: 606049 relation: main_file file_date_updated: 2020-07-14T12:46:47Z has_accepted_license: '1' language: - iso: eng month: '02' oa: 1 oa_version: Published Version page: '33' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '164' related_material: record: - id: '2063' relation: later_version status: public - id: '5412' relation: earlier_version status: public - id: '5414' relation: later_version status: public status: public title: CEGAR for qualitative analysis of probabilistic systems type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2014' ... --- _id: '5414' abstract: - lang: eng text: "We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems. We focus on qualitative properties for MDPs that can express that desired behaviors of the system arise almost-surely (with probability 1) or with positive probability.\r\nWe introduce a new simulation relation to capture the refinement relation of MDPs with respect to qualitative properties, and present discrete graph theoretic algorithms with quadratic complexity to compute the simulation relation.\r\nWe present an automated technique for assume-guarantee style reasoning for compositional analysis of MDPs with qualitative properties by giving a counter-example guided abstraction-refinement approach to compute our new simulation relation. \r\nWe have implemented our algorithms and show that the compositional analysis leads to significant improvements. " 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: Przemyslaw full_name: Daca, Przemyslaw id: 49351290-F248-11E8-B48F-1D18A9856A87 last_name: Daca - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik citation: ama: Chatterjee K, Daca P, Chmelik M. CEGAR for Qualitative Analysis of Probabilistic Systems. IST Austria; 2014. doi:10.15479/AT:IST-2014-153-v3-1 apa: Chatterjee, K., Daca, P., & Chmelik, M. (2014). CEGAR for qualitative analysis of probabilistic systems. IST Austria. https://doi.org/10.15479/AT:IST-2014-153-v3-1 chicago: Chatterjee, Krishnendu, Przemyslaw Daca, and Martin Chmelik. CEGAR for Qualitative Analysis of Probabilistic Systems. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-153-v3-1. ieee: K. Chatterjee, P. Daca, and M. Chmelik, CEGAR for qualitative analysis of probabilistic systems. IST Austria, 2014. ista: Chatterjee K, Daca P, Chmelik M. 2014. CEGAR for qualitative analysis of probabilistic systems, IST Austria, 33p. mla: Chatterjee, Krishnendu, et al. CEGAR for Qualitative Analysis of Probabilistic Systems. IST Austria, 2014, doi:10.15479/AT:IST-2014-153-v3-1. short: K. Chatterjee, P. Daca, M. Chmelik, CEGAR for Qualitative Analysis of Probabilistic Systems, IST Austria, 2014. date_created: 2018-12-12T11:39:12Z date_published: 2014-02-07T00:00:00Z date_updated: 2023-02-23T12:25:15Z day: '07' ddc: - '000' department: - _id: KrCh doi: 10.15479/AT:IST-2014-153-v3-1 file: - access_level: open_access checksum: 87b93fe9af71fc5c94b0eb6151537e11 content_type: application/pdf creator: system date_created: 2018-12-12T11:53:03Z date_updated: 2020-07-14T12:46:48Z file_id: '5464' file_name: IST-2014-153-v3+1_main.pdf file_size: 606227 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: '33' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '165' related_material: record: - id: '2063' relation: later_version status: public - id: '5412' relation: earlier_version status: public - id: '5413' relation: earlier_version status: public status: public title: CEGAR for qualitative analysis of probabilistic systems type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2014' ... --- _id: '5412' abstract: - lang: eng text: "We consider Markov decision processes (MDPs) which are a standard model for probabilistic systems. We focus on qualitative properties for MDPs that can express that desired behaviors of the system arise almost-surely (with probability 1) or with positive probability.\r\nWe introduce a new simulation relation to capture the refinement relation of MDPs with respect to qualitative properties, and present discrete graph theoretic algorithms with quadratic complexity to compute the simulation relation.\r\nWe present an automated technique for assume-guarantee style reasoning for compositional analysis of MDPs with qualitative properties by giving a counter-example 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: - 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: Przemyslaw full_name: Daca, Przemyslaw id: 49351290-F248-11E8-B48F-1D18A9856A87 last_name: Daca - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik citation: ama: Chatterjee K, Daca P, Chmelik M. CEGAR for Qualitative Analysis of Probabilistic Systems. IST Austria; 2014. doi:10.15479/AT:IST-2014-153-v1-1 apa: Chatterjee, K., Daca, P., & Chmelik, M. (2014). CEGAR for qualitative analysis of probabilistic systems. IST Austria. https://doi.org/10.15479/AT:IST-2014-153-v1-1 chicago: Chatterjee, Krishnendu, Przemyslaw Daca, and Martin Chmelik. CEGAR for Qualitative Analysis of Probabilistic Systems. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-153-v1-1. ieee: K. Chatterjee, P. Daca, and M. Chmelik, CEGAR for qualitative analysis of probabilistic systems. IST Austria, 2014. ista: Chatterjee K, Daca P, Chmelik M. 2014. CEGAR for qualitative analysis of probabilistic systems, IST Austria, 31p. mla: Chatterjee, Krishnendu, et al. CEGAR for Qualitative Analysis of Probabilistic Systems. IST Austria, 2014, doi:10.15479/AT:IST-2014-153-v1-1. short: K. Chatterjee, P. Daca, M. Chmelik, CEGAR for Qualitative Analysis of Probabilistic Systems, IST Austria, 2014. date_created: 2018-12-12T11:39:11Z date_published: 2014-01-29T00:00:00Z date_updated: 2023-02-23T12:25:18Z day: '29' ddc: - '000' department: - _id: KrCh doi: 10.15479/AT:IST-2014-153-v1-1 file: - access_level: open_access checksum: 4d6cda4bebed970926403ad6ad8c745f content_type: application/pdf creator: system date_created: 2018-12-12T11:53:39Z date_updated: 2020-07-14T12:46:47Z file_id: '5500' file_name: IST-2014-153-v1+1_main.pdf file_size: 423322 relation: main_file file_date_updated: 2020-07-14T12:46:47Z has_accepted_license: '1' language: - iso: eng month: '01' oa: 1 oa_version: Published Version page: '31' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '153' related_material: record: - id: '2063' relation: later_version status: public - id: '5413' relation: later_version status: public - id: '5414' relation: later_version status: public status: public title: CEGAR for qualitative analysis of probabilistic systems type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2014' ... --- _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: '5417' abstract: - lang: eng text: "We define the model-measuring problem: given a model M and specification φ, what is the maximal distance ρ such that all models M'within distance ρ from M satisfy (or violate)φ. The model measuring problem presupposes a distance function on models. We concentrate on automatic distance functions, which are defined by weighted automata.\r\nThe model-measuring problem subsumes several generalizations of the classical model-checking problem, in particular, quantitative model-checking problems that measure the degree of satisfaction of a specification, and robustness problems that measure how much a model can be perturbed without violating the specification.\r\nWe show that for automatic distance functions, and ω-regular linear-time and branching-time specifications, the model-measuring problem can be solved.\r\nWe use automata-theoretic model-checking methods for model measuring, replacing the emptiness question for standard word and tree automata by the optimal-weight question for the weighted versions of these automata. We consider weighted automata that accumulate weights by maximizing, summing, discounting, and limit averaging. \r\nWe give several examples of using the model-measuring problem to compute various notions of robustness and quantitative satisfaction for temporal specifications." alternative_title: - IST Austria Technical Report author: - 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: Henzinger TA, Otop J. From Model Checking to Model Measuring. IST Austria; 2014. doi:10.15479/AT:IST-2014-172-v1-1 apa: Henzinger, T. A., & Otop, J. (2014). From model checking to model measuring. IST Austria. https://doi.org/10.15479/AT:IST-2014-172-v1-1 chicago: Henzinger, Thomas A, and Jan Otop. From Model Checking to Model Measuring. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-172-v1-1. ieee: T. A. Henzinger and J. Otop, From model checking to model measuring. IST Austria, 2014. ista: Henzinger TA, Otop J. 2014. From model checking to model measuring, IST Austria, 14p. mla: Henzinger, Thomas A., and Jan Otop. From Model Checking to Model Measuring. IST Austria, 2014, doi:10.15479/AT:IST-2014-172-v1-1. short: T.A. Henzinger, J. Otop, From Model Checking to Model Measuring, IST Austria, 2014. date_created: 2018-12-12T11:39:13Z date_published: 2014-02-19T00:00:00Z date_updated: 2023-02-23T10:38:10Z day: '19' ddc: - '000' department: - _id: ToHe doi: 10.15479/AT:IST-2014-172-v1-1 file: - access_level: open_access checksum: fcc3eab903cfcd3778b338d2d0d44d18 content_type: application/pdf creator: system date_created: 2018-12-12T11:53:20Z date_updated: 2020-07-14T12:46:49Z file_id: '5481' file_name: IST-2014-172-v1+1_report.pdf file_size: 383052 relation: main_file file_date_updated: 2020-07-14T12:46:49Z has_accepted_license: '1' language: - iso: eng month: '02' oa: 1 oa_version: Published Version page: '14' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '175' related_material: record: - id: '2327' relation: later_version status: public status: public title: From model checking to model measuring type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2014' ... --- _id: '5416' abstract: - lang: eng text: As hybrid systems involve continuous behaviors, they should be evaluated by quantitative methods, rather than qualitative methods. In this paper we adapt a quantitative framework, called model measuring, to the hybrid systems domain. The model-measuring problem asks, given a model M and a specification, what is the maximal distance such that all models within that distance from M satisfy (or violate) the specification. A distance function on models is given as part of the input of the problem. Distances, especially related to continuous behaviors are more natural in the hybrid case than the discrete case. We are interested in distances represented by monotonic hybrid automata, a hybrid counterpart of (discrete) weighted automata, whose recognized timed languages are monotone (w.r.t. inclusion) in the values of parameters.The contributions of this paper are twofold. First, we give sufficient conditions under which the model-measuring problem can be solved. Second, we discuss the modeling of distances and applications of the model-measuring problem. alternative_title: - IST Austria Technical Report author: - 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: Henzinger TA, Otop J. Model Measuring for Hybrid Systems. IST Austria; 2014. doi:10.15479/AT:IST-2014-171-v1-1 apa: Henzinger, T. A., & Otop, J. (2014). Model measuring for hybrid systems. IST Austria. https://doi.org/10.15479/AT:IST-2014-171-v1-1 chicago: Henzinger, Thomas A, and Jan Otop. Model Measuring for Hybrid Systems. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-171-v1-1. ieee: T. A. Henzinger and J. Otop, Model measuring for hybrid systems. IST Austria, 2014. ista: Henzinger TA, Otop J. 2014. Model measuring for hybrid systems, IST Austria, 22p. mla: Henzinger, Thomas A., and Jan Otop. Model Measuring for Hybrid Systems. IST Austria, 2014, doi:10.15479/AT:IST-2014-171-v1-1. short: T.A. Henzinger, J. Otop, Model Measuring for Hybrid Systems, IST Austria, 2014. date_created: 2018-12-12T11:39:12Z date_published: 2014-02-19T00:00:00Z date_updated: 2023-02-23T10:33:21Z day: '19' ddc: - '005' department: - _id: ToHe doi: 10.15479/AT:IST-2014-171-v1-1 file: - access_level: open_access checksum: 445456d22371e4e49aad2b9a0c13bf80 content_type: application/pdf creator: system date_created: 2018-12-12T11:53:32Z date_updated: 2020-07-14T12:46:49Z file_id: '5492' file_name: IST-2014-171-v1+1_report.pdf file_size: 712077 relation: main_file file_date_updated: 2020-07-14T12:46:49Z has_accepted_license: '1' language: - iso: eng month: '02' oa: 1 oa_version: Published Version page: '22' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '171' related_material: record: - id: '2217' relation: later_version status: public status: public title: Model measuring for hybrid systems 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: '5425' abstract: - lang: eng text: ' We consider partially observable Markov decision processes (POMDPs) with a set of target states and every transition is associated with an integer cost. The optimization objective we study asks to minimize the expected total cost till the target set is reached, while ensuring that the target set is reached almost-surely (with probability 1). We show that for integer costs approximating the optimal cost is undecidable. For positive costs, our results are as follows: (i) we establish matching lower and upper bounds for the optimal cost and the bound is double exponential; (ii) we show that the problem of approximating the optimal cost is decidable and present approximation algorithms developing on the existing algorithms for POMDPs with finite-horizon objectives. While the worst-case running time of our algorithm is double exponential, we also present efficient stopping criteria for the algorithm and show experimentally that it performs well in many examples of interest.' alternative_title: - IST Austria Technical Report author: - first_name: '1' full_name: Anonymous, 1 last_name: Anonymous - first_name: '2' full_name: Anonymous, 2 last_name: Anonymous - first_name: '3' full_name: Anonymous, 3 last_name: Anonymous - first_name: '4' full_name: Anonymous, 4 last_name: Anonymous citation: ama: Anonymous 1, Anonymous 2, Anonymous 3, Anonymous 4. Optimal Cost Almost-Sure Reachability in POMDPs. IST Austria; 2014. apa: Anonymous, 1, Anonymous, 2, Anonymous, 3, & Anonymous, 4. (2014). Optimal cost almost-sure reachability in POMDPs. IST Austria. chicago: Anonymous, 1, 2 Anonymous, 3 Anonymous, and 4 Anonymous. Optimal Cost Almost-Sure Reachability in POMDPs. IST Austria, 2014. ieee: 1 Anonymous, 2 Anonymous, 3 Anonymous, and 4 Anonymous, Optimal cost almost-sure reachability in POMDPs. IST Austria, 2014. ista: Anonymous 1, Anonymous 2, Anonymous 3, Anonymous 4. 2014. Optimal cost almost-sure reachability in POMDPs, IST Austria, 22p. mla: Anonymous, 1, et al. Optimal Cost Almost-Sure Reachability in POMDPs. IST Austria, 2014. short: 1 Anonymous, 2 Anonymous, 3 Anonymous, 4 Anonymous, Optimal Cost Almost-Sure Reachability in POMDPs, IST Austria, 2014. date_created: 2018-12-12T11:39:15Z date_published: 2014-09-09T00:00:00Z date_updated: 2023-02-23T10:02:57Z day: '09' ddc: - '000' file: - access_level: open_access checksum: b9668a70d53c550b3cd64f0c77451c3d content_type: application/pdf creator: system date_created: 2018-12-12T11:53:17Z date_updated: 2020-07-14T12:46:51Z file_id: '5478' file_name: IST-2014-307-v1+1_main.pdf file_size: 2725429 relation: main_file - access_level: closed checksum: 808ada1dddecc48ca041526fcc6a9efd content_type: text/plain creator: dernst date_created: 2019-04-16T14:16:12Z date_updated: 2020-07-14T12:46:51Z file_id: '6322' file_name: IST-2014-307-v1+2_authors.txt file_size: 117 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: '22' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '307' related_material: record: - id: '1529' relation: later_version status: public scopus_import: 1 status: public title: Optimal cost almost-sure reachability in POMDPs 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: '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: '5399' abstract: - lang: eng text: In this work we present a flexible tool for tumor progression, which simulates the evolutionary dynamics of cancer. Tumor progression implements a multi-type branching process where the key parameters are the fitness landscape, the mutation rate, and the average time of cell division. The fitness of a cancer cell depends on the mutations it has accumulated. The input to our tool could be any fitness landscape, mutation rate, and cell division time, and the tool produces the growth dynamics and all relevant statistics. alternative_title: - IST Austria Technical Report author: - first_name: Johannes full_name: Reiter, Johannes id: 4A918E98-F248-11E8-B48F-1D18A9856A87 last_name: Reiter orcid: 0000-0002-0170-7353 - first_name: Ivana full_name: Bozic, Ivana last_name: Bozic - 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: Nowak, Martin last_name: Nowak citation: ama: 'Reiter J, Bozic I, Chatterjee K, Nowak M. TTP: Tool for Tumor Progression. IST Austria; 2013. doi:10.15479/AT:IST-2013-104-v1-1' apa: 'Reiter, J., Bozic, I., Chatterjee, K., & Nowak, M. (2013). TTP: Tool for Tumor Progression. IST Austria. https://doi.org/10.15479/AT:IST-2013-104-v1-1' chicago: 'Reiter, Johannes, Ivana Bozic, Krishnendu Chatterjee, and Martin Nowak. TTP: Tool for Tumor Progression. IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-104-v1-1.' ieee: 'J. Reiter, I. Bozic, K. Chatterjee, and M. Nowak, TTP: Tool for Tumor Progression. IST Austria, 2013.' ista: 'Reiter J, Bozic I, Chatterjee K, Nowak M. 2013. TTP: Tool for Tumor Progression, IST Austria, 17p.' mla: 'Reiter, Johannes, et al. TTP: Tool for Tumor Progression. IST Austria, 2013, doi:10.15479/AT:IST-2013-104-v1-1.' short: 'J. Reiter, I. Bozic, K. Chatterjee, M. Nowak, TTP: Tool for Tumor Progression, IST Austria, 2013.' date_created: 2018-12-12T11:39:07Z date_published: 2013-01-11T00:00:00Z date_updated: 2023-02-23T10:23:57Z day: '11' ddc: - '000' department: - _id: KrCh doi: 10.15479/AT:IST-2013-104-v1-1 file: - access_level: open_access checksum: 2cc8c6e157eca1271128db80bb3dec80 content_type: application/pdf creator: system date_created: 2018-12-12T11:54:20Z date_updated: 2020-07-14T12:46:44Z file_id: '5542' file_name: IST-2013-104-v1+1_tumortool.pdf file_size: 1471954 relation: main_file file_date_updated: 2020-07-14T12:46:44Z has_accepted_license: '1' language: - iso: eng month: '01' oa: 1 oa_version: Published Version page: '17' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '104' related_material: record: - id: '2000' relation: later_version status: public status: public title: 'TTP: Tool for Tumor Progression' type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2013' ... --- _id: '5403' abstract: - lang: eng text: 'We consider concurrent games played by two-players on a finite state graph, where in every round the players simultaneously choose a move, and the current state along with the joint moves determine the successor state. We study the most fundamental objective for concurrent games, namely, mean-payoff or limit-average objective, where a reward is associated to every transition, and the goal of player 1 is to maximize the long-run average of the rewards, and the objective of player 2 is strictly the opposite (i.e., the games are zero-sum). The path constraint for player 1 could be qualitative, i.e., the mean-payoff is the maximal reward, or arbitrarily close to it; or quantitative, i.e., a given threshold between the minimal and maximal reward. We consider the computation of the almost-sure (resp. positive) winning sets, where player 1 can ensure that the path constraint is satisfied with probability 1 (resp. positive probability). Almost-sure winning with qualitative constraint exactly corresponds to the question whether there exists a strategy to ensure that the payoff is the maximal reward of the game. Our main results for qualitative path constraints are as follows: (1) we establish qualitative determinacy results that show for every state either player 1 has a strategy to ensure almost-sure (resp. positive) winning against all player-2 strategies or player 2 has a spoiling strategy to falsify almost-sure (resp. positive) winning against all player-1 strategies; (2) we present optimal strategy complexity results that precisely characterize the classes of strategies required for almost-sure and positive winning for both players; and (3) we present quadratic time algorithms to compute the almost-sure and the positive winning sets, matching the best known bound of the algorithms for much simpler problems (such as reachability objectives). For quantitative constraints we show that a polynomial time solution for the almost-sure or the positive winning set would imply a solution to a long-standing open problem (of solving the value problem of mean-payoff games) that is not known to be in polynomial 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 citation: ama: Chatterjee K, Ibsen-Jensen R. Qualitative Analysis of Concurrent Mean-Payoff Games. IST Austria; 2013. doi:10.15479/AT:IST-2013-126-v1-1 apa: Chatterjee, K., & Ibsen-Jensen, R. (2013). Qualitative analysis of concurrent mean-payoff games. IST Austria. https://doi.org/10.15479/AT:IST-2013-126-v1-1 chicago: Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. Qualitative Analysis of Concurrent Mean-Payoff Games. IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-126-v1-1. ieee: K. Chatterjee and R. Ibsen-Jensen, Qualitative analysis of concurrent mean-payoff games. IST Austria, 2013. ista: Chatterjee K, Ibsen-Jensen R. 2013. Qualitative analysis of concurrent mean-payoff games, IST Austria, 33p. mla: Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. Qualitative Analysis of Concurrent Mean-Payoff Games. IST Austria, 2013, doi:10.15479/AT:IST-2013-126-v1-1. short: K. Chatterjee, R. Ibsen-Jensen, Qualitative Analysis of Concurrent Mean-Payoff Games, IST Austria, 2013. date_created: 2018-12-12T11:39:08Z date_published: 2013-07-03T00:00:00Z date_updated: 2023-02-23T12:22:53Z day: '03' ddc: - '000' - '005' department: - _id: KrCh doi: 10.15479/AT:IST-2013-126-v1-1 file: - access_level: open_access checksum: 063868c665beec37bf28160e2a695746 content_type: application/pdf creator: system date_created: 2018-12-12T11:53:49Z date_updated: 2020-07-14T12:46:45Z file_id: '5510' file_name: IST-2013-126-v1+1_soda_full.pdf file_size: 434523 relation: main_file file_date_updated: 2020-07-14T12:46:45Z has_accepted_license: '1' language: - iso: eng month: '07' oa: 1 oa_version: Published Version page: '33' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '126' related_material: record: - id: '524' relation: later_version status: public status: public title: Qualitative analysis of concurrent mean-payoff games type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2013' ... --- _id: '5402' abstract: - lang: eng text: "Linearizability requires that the outcome of calls by competing threads to a concurrent data structure is the same as some sequential execution where each thread has exclusive access to the data structure. In an ordered data structure, such as a queue or a stack, linearizability is ensured by requiring threads commit in the order dictated by the sequential semantics of the data structure; e.g., in a concurrent queue implementation a dequeue can only remove the oldest element. \r\nIn this paper, we investigate the impact of this strict ordering, by comparing what linearizability allows to what existing implementations do. We first give an operational definition for linearizability which allows us to build the most general linearizable implementation as a transition system for any given sequential specification. We then use this operational definition to categorize linearizable implementations based on whether they are bound or free. In a bound implementation, whenever all threads observe the same logical state, the updates to the logical state and the temporal order of commits coincide. All existing queue implementations we know of are bound. We then proceed to present, to the best of our knowledge, the first ever free queue implementation. Our experiments show that free implementations have the potential for better performance by suffering less from contention." alternative_title: - IST Austria Technical Report author: - 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: Ali full_name: Sezgin, Ali id: 4C7638DA-F248-11E8-B48F-1D18A9856A87 last_name: Sezgin citation: ama: Henzinger TA, Sezgin A. How Free Is Your Linearizable Concurrent Data Structure? IST Austria; 2013. doi:10.15479/AT:IST-2013-123-v1-1 apa: Henzinger, T. A., & Sezgin, A. (2013). How free is your linearizable concurrent data structure? IST Austria. https://doi.org/10.15479/AT:IST-2013-123-v1-1 chicago: Henzinger, Thomas A, and Ali Sezgin. How Free Is Your Linearizable Concurrent Data Structure? IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-123-v1-1. ieee: T. A. Henzinger and A. Sezgin, How free is your linearizable concurrent data structure? IST Austria, 2013. ista: Henzinger TA, Sezgin A. 2013. How free is your linearizable concurrent data structure?, IST Austria, 16p. mla: Henzinger, Thomas A., and Ali Sezgin. How Free Is Your Linearizable Concurrent Data Structure? IST Austria, 2013, doi:10.15479/AT:IST-2013-123-v1-1. short: T.A. Henzinger, A. Sezgin, How Free Is Your Linearizable Concurrent Data Structure?, IST Austria, 2013. date_created: 2018-12-12T11:39:07Z date_published: 2013-06-12T00:00:00Z date_updated: 2020-07-14T23:04:47Z day: '12' ddc: - '000' - '004' department: - _id: ToHe doi: 10.15479/AT:IST-2013-123-v1-1 file: - access_level: open_access checksum: ce580605ae9756a8c99d7b403ebb8eed content_type: application/pdf creator: system date_created: 2018-12-12T11:53:19Z date_updated: 2020-07-14T12:46:45Z file_id: '5480' file_name: IST-2013-123-v1+1_main-concur2013.pdf file_size: 249790 relation: main_file file_date_updated: 2020-07-14T12:46:45Z has_accepted_license: '1' language: - iso: eng month: '06' oa: 1 oa_version: Published Version page: '16' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '123' status: public title: How free is your linearizable concurrent data structure? type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2013' ... --- _id: '5400' abstract: - lang: eng text: We consider partially observable Markov decision processes (POMDPs) with ω-regular conditions specified as parity objectives. The class of ω-regular languages extends regular languages to infinite strings and provides a robust specification language to express all properties used in verification, and parity objectives are canonical forms to express ω-regular conditions. The qualitative analysis problem given a POMDP and a parity objective asks whether there is a strategy to ensure that the objective is satis- fied with probability 1 (resp. positive probability). While the qualitative analysis problems are known to be undecidable even for very special cases of parity objectives, we establish decidability (with optimal complexity) of the qualitative analysis problems for POMDPs with all parity objectives under finite- memory strategies. We establish asymptotically optimal (exponential) memory bounds and EXPTIME- completeness of the qualitative analysis problems under finite-memory strategies for POMDPs with parity objectives. 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: Mathieu full_name: Tracol, Mathieu id: 3F54FA38-F248-11E8-B48F-1D18A9856A87 last_name: Tracol citation: ama: Chatterjee K, Chmelik M, Tracol M. What Is Decidable about Partially Observable Markov Decision Processes with ω-Regular Objectives. IST Austria; 2013. doi:10.15479/AT:IST-2013-109-v1-1 apa: Chatterjee, K., Chmelik, M., & Tracol, M. (2013). What is decidable about partially observable Markov decision processes with ω-regular objectives. IST Austria. https://doi.org/10.15479/AT:IST-2013-109-v1-1 chicago: Chatterjee, Krishnendu, Martin Chmelik, and Mathieu Tracol. What Is Decidable about Partially Observable Markov Decision Processes with ω-Regular Objectives. IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-109-v1-1. ieee: K. Chatterjee, M. Chmelik, and M. Tracol, What is decidable about partially observable Markov decision processes with ω-regular objectives. IST Austria, 2013. ista: Chatterjee K, Chmelik M, Tracol M. 2013. What is decidable about partially observable Markov decision processes with ω-regular objectives, IST Austria, 41p. mla: Chatterjee, Krishnendu, et al. What Is Decidable about Partially Observable Markov Decision Processes with ω-Regular Objectives. IST Austria, 2013, doi:10.15479/AT:IST-2013-109-v1-1. short: K. Chatterjee, M. Chmelik, M. Tracol, What Is Decidable about Partially Observable Markov Decision Processes with ω-Regular Objectives, IST Austria, 2013. date_created: 2018-12-12T11:39:07Z date_published: 2013-02-20T00:00:00Z date_updated: 2023-02-23T10:36:45Z day: '20' ddc: - '000' - '005' department: - _id: KrCh doi: 10.15479/AT:IST-2013-109-v1-1 file: - access_level: open_access checksum: cbba40210788a1b22c6cf06433b5ed6f content_type: application/pdf creator: system date_created: 2018-12-12T11:53:06Z date_updated: 2020-07-14T12:46:44Z file_id: '5467' file_name: IST-2013-109-v1+1_What_is_Decidable_about_Partially_Observable_Markov_Decision_Processes_with_ω-Regular_Objectives.pdf file_size: 483407 relation: main_file file_date_updated: 2020-07-14T12:46:44Z has_accepted_license: '1' language: - iso: eng month: '02' oa: 1 oa_version: Published Version page: '41' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '109' related_material: record: - id: '1477' relation: later_version status: public - id: '2295' relation: later_version status: public status: public title: What is decidable about partially observable Markov decision processes with ω-regular objectives type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2013' ... --- _id: '5404' abstract: - lang: eng text: 'We study finite-state two-player (zero-sum) concurrent mean-payoff games played on a graph. We focus on the important sub-class of ergodic games where all states are visited infinitely often with probability 1. The algorithmic study of ergodic games was initiated in a seminal work of Hoffman and Karp in 1966, but all basic complexity questions have remained unresolved. Our main results for ergodic games are as follows: We establish (1) an optimal exponential bound 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); (2) the approximation problem lie in FNP; (3) the approximation problem is at least as hard as the decision problem for simple stochastic games (for which NP and coNP is the long-standing best known bound). We show that the exact value can be expressed in the existential theory of the reals, and also establish square-root sum hardness for a related class of games.' 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 Complexity of Ergodic Games. IST Austria; 2013. doi:10.15479/AT:IST-2013-127-v1-1 apa: Chatterjee, K., & Ibsen-Jensen, R. (2013). The complexity of ergodic games. IST Austria. https://doi.org/10.15479/AT:IST-2013-127-v1-1 chicago: Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. The Complexity of Ergodic Games. IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-127-v1-1. ieee: K. Chatterjee and R. Ibsen-Jensen, The complexity of ergodic games. IST Austria, 2013. ista: Chatterjee K, Ibsen-Jensen R. 2013. The complexity of ergodic games, IST Austria, 29p. mla: Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. The Complexity of Ergodic Games. IST Austria, 2013, doi:10.15479/AT:IST-2013-127-v1-1. short: K. Chatterjee, R. Ibsen-Jensen, The Complexity of Ergodic Games, IST Austria, 2013. date_created: 2018-12-12T11:39:08Z date_published: 2013-07-03T00:00:00Z date_updated: 2023-02-23T10:30:55Z day: '03' ddc: - '000' - '005' department: - _id: KrCh doi: 10.15479/AT:IST-2013-127-v1-1 file: - access_level: open_access checksum: 79ee5e677a82611ce06e0360c69d494a content_type: application/pdf creator: system date_created: 2018-12-12T11:53:35Z date_updated: 2020-07-14T12:46:45Z file_id: '5496' file_name: IST-2013-127-v1+1_ergodic.pdf file_size: 517275 relation: main_file file_date_updated: 2020-07-14T12:46:45Z has_accepted_license: '1' language: - iso: eng month: '07' oa: 1 oa_version: Published Version page: '29' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '127' related_material: record: - id: '2162' relation: later_version status: public status: public title: The complexity of ergodic games type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2013' ... --- _id: '5405' abstract: - lang: eng text: "The theory of graph games is the foundation for modeling and synthesizing reactive processes. In the synthesis of stochastic processes, we use 2-1/2-player games where some transitions of the game graph are controlled by two adversarial players, the System and the Environment, and the other transitions are determined probabilistically. We consider 2-1/2-player games where the objective of the System is the conjunction of a qualitative objective (specified as a parity condition) and a quantitative objective (specified as a mean-payoff condition). We establish that the problem of deciding whether the System can ensure that the probability to satisfy the mean-payoff parity objective is at least a given threshold is in NP ∩ coNP, matching the best known bound in the special case of 2-player games (where all transitions are deterministic) with only parity objectives, or with only mean-payoff objectives. We present an algorithm running\r\nin time O(d · n^{2d}·MeanGame) to compute the set of almost-sure winning states from which the objective\r\ncan be ensured with probability 1, where n is the number of states of the game, d the number of priorities\r\nof the parity objective, and MeanGame is the complexity to compute the set of almost-sure winning states\r\nin 2-1/2-player mean-payoff games. Our results are useful in the synthesis of stochastic reactive systems\r\nwith both functional requirement (given as a qualitative objective) and performance requirement (given\r\nas a quantitative objective)." 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 - first_name: Hugo full_name: Gimbert, Hugo last_name: Gimbert - first_name: Youssouf full_name: Oualhadj, Youssouf last_name: Oualhadj citation: ama: Chatterjee K, Doyen L, Gimbert H, Oualhadj Y. Perfect-Information Stochastic Mean-Payoff Parity Games. IST Austria; 2013. doi:10.15479/AT:IST-2013-128-v1-1 apa: Chatterjee, K., Doyen, L., Gimbert, H., & Oualhadj, Y. (2013). Perfect-information stochastic mean-payoff parity games. IST Austria. https://doi.org/10.15479/AT:IST-2013-128-v1-1 chicago: Chatterjee, Krishnendu, Laurent Doyen, Hugo Gimbert, and Youssouf Oualhadj. Perfect-Information Stochastic Mean-Payoff Parity Games. IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-128-v1-1. ieee: K. Chatterjee, L. Doyen, H. Gimbert, and Y. Oualhadj, Perfect-information stochastic mean-payoff parity games. IST Austria, 2013. ista: Chatterjee K, Doyen L, Gimbert H, Oualhadj Y. 2013. Perfect-information stochastic mean-payoff parity games, IST Austria, 22p. mla: Chatterjee, Krishnendu, et al. Perfect-Information Stochastic Mean-Payoff Parity Games. IST Austria, 2013, doi:10.15479/AT:IST-2013-128-v1-1. short: K. Chatterjee, L. Doyen, H. Gimbert, Y. Oualhadj, Perfect-Information Stochastic Mean-Payoff Parity Games, IST Austria, 2013. date_created: 2018-12-12T11:39:09Z date_published: 2013-07-08T00:00:00Z date_updated: 2023-02-23T10:33:08Z day: '08' ddc: - '000' - '005' - '510' department: - _id: KrCh doi: 10.15479/AT:IST-2013-128-v1-1 file: - access_level: open_access checksum: ede787a10e74e4f7db302fab8f12f3ca content_type: application/pdf creator: system date_created: 2018-12-12T11:53:54Z date_updated: 2020-07-14T12:46:45Z file_id: '5516' file_name: IST-2013-128-v1+1_full_stoch_mpp.pdf file_size: 387467 relation: main_file file_date_updated: 2020-07-14T12:46:45Z has_accepted_license: '1' language: - iso: eng month: '07' oa: 1 oa_version: Published Version page: '22' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '128' related_material: record: - id: '2212' relation: later_version status: public status: public title: Perfect-information stochastic mean-payoff parity games type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2013' ... --- _id: '5409' abstract: - lang: eng text: "The edit distance between two (untimed) traces is the minimum cost of a sequence of edit operations (insertion, deletion, or substitution) needed to transform one trace to the other. Edit distances have been extensively studied in the untimed setting, and form the basis for approximate matching of sequences in different domains such as coding theory, parsing, and speech recognition. \r\nIn this paper, we lift the study of edit distances from untimed languages to the timed setting. We define an edit distance between timed words which incorporates both the edit distance between the untimed words and the absolute difference in timestamps. Our edit distance between two timed words is computable in polynomial time. Further, we show that the edit distance between a timed word and a timed language generated by a timed automaton, defined as the edit distance between the word and the closest word in the language, is PSPACE-complete. While computing the edit distance between two timed automata is undecidable, we show that the approximate version, where we decide if the edit distance between two timed automata is either less than a given parameter or more than delta away from the parameter, for delta>0, can be solved in exponential space and is EXPSPACE-hard. Our definitions and techniques can be generalized to the setting of hybrid systems, and we show analogous decidability results for rectangular 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: Rasmus full_name: Ibsen-Jensen, Rasmus id: 3B699956-F248-11E8-B48F-1D18A9856A87 last_name: Ibsen-Jensen orcid: 0000-0003-4783-0389 - first_name: Rupak full_name: Majumdar, Rupak last_name: Majumdar citation: ama: Chatterjee K, Ibsen-Jensen R, Majumdar R. Edit Distance for Timed Automata. IST Austria; 2013. doi:10.15479/AT:IST-2013-144-v1-1 apa: Chatterjee, K., Ibsen-Jensen, R., & Majumdar, R. (2013). Edit distance for timed automata. IST Austria. https://doi.org/10.15479/AT:IST-2013-144-v1-1 chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Rupak Majumdar. Edit Distance for Timed Automata. IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-144-v1-1. ieee: K. Chatterjee, R. Ibsen-Jensen, and R. Majumdar, Edit distance for timed automata. IST Austria, 2013. ista: Chatterjee K, Ibsen-Jensen R, Majumdar R. 2013. Edit distance for timed automata, IST Austria, 12p. mla: Chatterjee, Krishnendu, et al. Edit Distance for Timed Automata. IST Austria, 2013, doi:10.15479/AT:IST-2013-144-v1-1. short: K. Chatterjee, R. Ibsen-Jensen, R. Majumdar, Edit Distance for Timed Automata, IST Austria, 2013. date_created: 2018-12-12T11:39:10Z date_published: 2013-10-30T00:00:00Z date_updated: 2023-02-23T10:33:18Z day: '30' ddc: - '000' department: - _id: KrCh doi: 10.15479/AT:IST-2013-144-v1-1 file: - access_level: open_access checksum: 0f7633081ba8299c543322f0ad08571f content_type: application/pdf creator: system date_created: 2018-12-12T11:53:08Z date_updated: 2020-07-14T12:46:46Z file_id: '5469' file_name: IST-2013-144-v1+1_main.pdf file_size: 336377 relation: main_file file_date_updated: 2020-07-14T12:46:46Z has_accepted_license: '1' language: - iso: eng month: '10' oa: 1 oa_version: Published Version page: '12' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '144' related_material: record: - id: '2216' relation: later_version status: public status: public title: Edit distance for timed automata type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2013' ... --- _id: '5406' abstract: - lang: eng text: 'We consider the distributed synthesis problem fortemporal logic specifications. Traditionally, the problem has been studied for LTL, and the previous results show that the problem is decidable iff there is no information fork in the architecture. We consider the problem for fragments of LTLand our main results are as follows: (1) We show that the problem is undecidable for architectures with information forks even for the fragment of LTL with temporal operators restricted to next and eventually. (2) For specifications restricted to globally along with non-nested next operators, we establish decidability (in EXPSPACE) for star architectures where the processes receive disjoint inputs, whereas we establish undecidability for architectures containing an information fork-meet structure. (3)Finally, we consider LTL without the next operator, and establish decidability (NEXPTIME-complete) for all architectures for a fragment that consists of a set of safety assumptions, and a set of guarantees where each guarantee is a safety, reachability, or liveness condition.' 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: Andreas full_name: Pavlogiannis, Andreas id: 49704004-F248-11E8-B48F-1D18A9856A87 last_name: Pavlogiannis orcid: 0000-0002-8943-0722 citation: ama: Chatterjee K, Henzinger TA, Otop J, Pavlogiannis A. Distributed Synthesis for LTL Fragments. IST Austria; 2013. doi:10.15479/AT:IST-2013-130-v1-1 apa: Chatterjee, K., Henzinger, T. A., Otop, J., & Pavlogiannis, A. (2013). Distributed synthesis for LTL Fragments. IST Austria. https://doi.org/10.15479/AT:IST-2013-130-v1-1 chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Andreas Pavlogiannis. Distributed Synthesis for LTL Fragments. IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-130-v1-1. ieee: K. Chatterjee, T. A. Henzinger, J. Otop, and A. Pavlogiannis, Distributed synthesis for LTL Fragments. IST Austria, 2013. ista: Chatterjee K, Henzinger TA, Otop J, Pavlogiannis A. 2013. Distributed synthesis for LTL Fragments, IST Austria, 11p. mla: Chatterjee, Krishnendu, et al. Distributed Synthesis for LTL Fragments. IST Austria, 2013, doi:10.15479/AT:IST-2013-130-v1-1. short: K. Chatterjee, T.A. Henzinger, J. Otop, A. Pavlogiannis, Distributed Synthesis for LTL Fragments, IST Austria, 2013. date_created: 2018-12-12T11:39:09Z date_published: 2013-07-08T00:00:00Z date_updated: 2023-02-21T17:01:26Z day: '08' ddc: - '005' department: - _id: KrCh - _id: ToHe doi: 10.15479/AT:IST-2013-130-v1-1 file: - access_level: open_access checksum: 855513ebaf6f72228800c5fdb522f93c content_type: application/pdf creator: system date_created: 2018-12-12T11:54:18Z date_updated: 2020-07-14T12:46:45Z file_id: '5540' file_name: IST-2013-130-v1+1_Distributed_Synthesis.pdf file_size: 467895 relation: main_file file_date_updated: 2020-07-14T12:46:45Z has_accepted_license: '1' language: - iso: eng month: '07' oa: 1 oa_version: Published Version page: '11' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '130' related_material: record: - id: '1376' relation: later_version status: public status: public title: Distributed synthesis for LTL Fragments type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2013' ... --- _id: '5408' abstract: - lang: eng text: "We consider two-player partial-observation stochastic games where player 1 has partial observation and player 2 has perfect observation. The winning condition we study are omega-regular conditions specified as parity objectives. The qualitative analysis problem given a partial-observation stochastic game and a parity objective asks whether there is a strategy to ensure that the objective is satisfied with probability 1 (resp. positive probability). While the qualitative analysis problems are known to be undecidable even for very special cases of parity objectives, they were shown to be decidable in 2EXPTIME under finite-memory strategies. We improve the complexity and show that the qualitative analysis problems for partial-observation stochastic parity games under finite-memory strategies are \r\nEXPTIME-complete; and also establish optimal (exponential) memory bounds for finite-memory strategies required for qualitative analysis. " 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 - first_name: Sumit full_name: Nain, Sumit last_name: Nain - first_name: Moshe full_name: Vardi, Moshe last_name: Vardi citation: ama: Chatterjee K, Doyen L, Nain S, Vardi M. The Complexity of Partial-Observation Stochastic Parity Games with Finite-Memory Strategies. IST Austria; 2013. doi:10.15479/AT:IST-2013-141-v1-1 apa: Chatterjee, K., Doyen, L., Nain, S., & Vardi, M. (2013). The complexity of partial-observation stochastic parity games with finite-memory strategies. IST Austria. https://doi.org/10.15479/AT:IST-2013-141-v1-1 chicago: Chatterjee, Krishnendu, Laurent Doyen, Sumit Nain, and Moshe Vardi. The Complexity of Partial-Observation Stochastic Parity Games with Finite-Memory Strategies. IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-141-v1-1. ieee: K. Chatterjee, L. Doyen, S. Nain, and M. Vardi, The complexity of partial-observation stochastic parity games with finite-memory strategies. IST Austria, 2013. ista: Chatterjee K, Doyen L, Nain S, Vardi M. 2013. The complexity of partial-observation stochastic parity games with finite-memory strategies, IST Austria, 17p. mla: Chatterjee, Krishnendu, et al. The Complexity of Partial-Observation Stochastic Parity Games with Finite-Memory Strategies. IST Austria, 2013, doi:10.15479/AT:IST-2013-141-v1-1. short: K. Chatterjee, L. Doyen, S. Nain, M. Vardi, The Complexity of Partial-Observation Stochastic Parity Games with Finite-Memory Strategies, IST Austria, 2013. date_created: 2018-12-12T11:39:10Z date_published: 2013-09-12T00:00:00Z date_updated: 2023-02-23T10:33:11Z day: '12' ddc: - '000' - '005' department: - _id: KrCh doi: 10.15479/AT:IST-2013-141-v1-1 file: - access_level: open_access checksum: 226bc791124f8d3138379778ce834e86 content_type: application/pdf creator: system date_created: 2018-12-12T11:53:16Z date_updated: 2020-07-14T12:46:46Z file_id: '5477' file_name: IST-2013-141-v1+1_main-tech-rpt.pdf file_size: 300481 relation: main_file file_date_updated: 2020-07-14T12:46:46Z has_accepted_license: '1' language: - iso: eng month: '09' oa: 1 oa_version: Published Version page: '17' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '141' related_material: record: - id: '2213' relation: later_version status: public status: public title: The complexity of partial-observation stochastic parity games with finite-memory strategies type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2013' ... --- _id: '5410' abstract: - lang: eng text: "Board games, like Tic-Tac-Toe and CONNECT-4, play an important role not only in development of mathematical and logical skills, but also in emotional and social development. In this paper, we address the problem of generating targeted starting positions for such games. This can facilitate new approaches for bringing novice players to mastery, and also leads to discovery of interesting game variants. \r\nOur approach generates starting states of varying hardness levels for player 1 in a two-player board game, given rules of the board game, the desired number of steps required for player 1 to win, and the expertise levels of the two players. Our approach leverages symbolic methods and iterative simulation to efficiently search the extremely large state space. We present experimental results that include discovery of states of varying hardness levels for several simple grid-based board games. Also, the presence of such states for standard game variants like Tic-Tac-Toe on board size 4x4 opens up new games to be played that have not been played for ages since the default start state is heavily biased. " alternative_title: - IST Austria Technical Report author: - first_name: Umair full_name: Ahmed, Umair last_name: Ahmed - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Sumit full_name: Gulwani, Sumit last_name: Gulwani citation: ama: Ahmed U, Chatterjee K, Gulwani S. Automatic Generation of Alternative Starting Positions for Traditional Board Games. IST Austria; 2013. doi:10.15479/AT:IST-2013-146-v1-1 apa: Ahmed, U., Chatterjee, K., & Gulwani, S. (2013). Automatic generation of alternative starting positions for traditional board games. IST Austria. https://doi.org/10.15479/AT:IST-2013-146-v1-1 chicago: Ahmed, Umair, Krishnendu Chatterjee, and Sumit Gulwani. Automatic Generation of Alternative Starting Positions for Traditional Board Games. IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-146-v1-1. ieee: U. Ahmed, K. Chatterjee, and S. Gulwani, Automatic generation of alternative starting positions for traditional board games. IST Austria, 2013. ista: Ahmed U, Chatterjee K, Gulwani S. 2013. Automatic generation of alternative starting positions for traditional board games, IST Austria, 13p. mla: Ahmed, Umair, et al. Automatic Generation of Alternative Starting Positions for Traditional Board Games. IST Austria, 2013, doi:10.15479/AT:IST-2013-146-v1-1. short: U. Ahmed, K. Chatterjee, S. Gulwani, Automatic Generation of Alternative Starting Positions for Traditional Board Games, IST Austria, 2013. date_created: 2018-12-12T11:39:10Z date_published: 2013-12-03T00:00:00Z date_updated: 2023-02-23T10:00:50Z day: '03' ddc: - '000' - '005' department: - _id: KrCh doi: 10.15479/AT:IST-2013-146-v1-1 file: - access_level: open_access checksum: 409f3aaaf1184e4057b89cbb449dac80 content_type: application/pdf creator: system date_created: 2018-12-12T11:54:06Z date_updated: 2020-07-14T12:46:46Z file_id: '5528' file_name: IST-2013-146-v1+1_main.pdf file_size: 818189 relation: main_file file_date_updated: 2020-07-14T12:46:46Z has_accepted_license: '1' language: - iso: eng month: '12' oa: 1 oa_version: Published Version page: '13' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '146' related_material: record: - id: '1481' relation: later_version status: public status: public title: Automatic generation of alternative starting positions for traditional board games type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2013' ... --- _id: '6440' abstract: - lang: eng text: In order to guarantee that each method of a data structure updates the logical state exactly once, al-most all non-blocking implementations employ Compare-And-Swap (CAS) based synchronization. For FIFO queue implementations this translates into concurrent enqueue or dequeue methods competing among themselves to update the same variable, the tail or the head, respectively, leading to high contention and poor scalability. Recent non-blocking queue implementations try to alleviate high contentionby increasing the number of contention points, all the while using CAS-based synchronization. Furthermore, obtaining a wait-free implementation with competition is achieved by additional synchronization which leads to further degradation of performance.In this paper we formalize the notion of competitiveness of a synchronizing statement which can beused as a measure for the scalability of concurrent implementations. We present a new queue implementation, the Speculative Pairing (SP) queue, which, as we show, decreases competitiveness by using Fetch-And-Increment (FAI) instead of CAS. We prove that the SP queue is linearizable and lock-free.We also show that replacing CAS with FAI leads to wait-freedom for dequeue methods without an adverse effect on performance. In fact, our experiments suggest that the SP queue can perform and scale better than the state-of-the-art queue implementations. alternative_title: - IST Austria Technical Report author: - 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: Hannes full_name: Payer, Hannes last_name: Payer - first_name: Ali full_name: Sezgin, Ali id: 4C7638DA-F248-11E8-B48F-1D18A9856A87 last_name: Sezgin citation: ama: Henzinger TA, Payer H, Sezgin A. Replacing Competition with Cooperation to Achieve Scalable Lock-Free FIFO Queues . IST Austria; 2013. doi:10.15479/AT:IST-2013-124-v1-1 apa: Henzinger, T. A., Payer, H., & Sezgin, A. (2013). Replacing competition with cooperation to achieve scalable lock-free FIFO queues . IST Austria. https://doi.org/10.15479/AT:IST-2013-124-v1-1 chicago: Henzinger, Thomas A, Hannes Payer, and Ali Sezgin. Replacing Competition with Cooperation to Achieve Scalable Lock-Free FIFO Queues . IST Austria, 2013. https://doi.org/10.15479/AT:IST-2013-124-v1-1. ieee: T. A. Henzinger, H. Payer, and A. Sezgin, Replacing competition with cooperation to achieve scalable lock-free FIFO queues . IST Austria, 2013. ista: Henzinger TA, Payer H, Sezgin A. 2013. Replacing competition with cooperation to achieve scalable lock-free FIFO queues , IST Austria, 23p. mla: Henzinger, Thomas A., et al. Replacing Competition with Cooperation to Achieve Scalable Lock-Free FIFO Queues . IST Austria, 2013, doi:10.15479/AT:IST-2013-124-v1-1. short: T.A. Henzinger, H. Payer, A. Sezgin, Replacing Competition with Cooperation to Achieve Scalable Lock-Free FIFO Queues , IST Austria, 2013. date_created: 2019-05-13T14:13:27Z date_published: 2013-06-13T00:00:00Z date_updated: 2020-07-14T23:06:19Z day: '13' ddc: - '000' - '005' department: - _id: ToHe doi: 10.15479/AT:IST-2013-124-v1-1 file: - access_level: open_access checksum: a219ba4eada6cd62befed52262ee15d4 content_type: application/pdf creator: dernst date_created: 2019-05-13T14:11:39Z date_updated: 2020-07-14T12:47:30Z file_id: '6441' file_name: 2013_TechRep_Henzinger.pdf file_size: 549684 relation: main_file file_date_updated: 2020-07-14T12:47:30Z has_accepted_license: '1' language: - iso: eng month: '06' oa: 1 oa_version: Published Version page: '23' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '124' status: public title: 'Replacing competition with cooperation to achieve scalable lock-free FIFO queues ' type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2013' ... --- _id: '5377' abstract: - lang: eng text: 'Two-player games on graphs are central in many problems in formal verification and program analysis such as synthesis and verification of open systems. In this work we consider solving recursive game graphs (or pushdown game graphs) that can model the control flow of sequential programs with recursion. While pushdown games have been studied before with qualitative objectives, such as reachability and ω-regular objectives, in this work we study for the first time such games with the most well-studied quantitative objective, namely, mean-payoff objectives. In pushdown games two types of strategies are relevant: (1) global strategies, that depend on the entire global history; and (2) modular strategies, that have only local memory and thus do not depend on the context of invocation, but only on the history of the current invocation of the module. Our main results are as follows: (1) One-player pushdown games with mean-payoff objectives under global strategies are decidable in polynomial time. (2) Two- player pushdown games with mean-payoff objectives under global strategies are undecidable. (3) One-player pushdown games with mean-payoff objectives under modular strategies are NP- hard. (4) Two-player pushdown games with mean-payoff objectives under modular strategies can be solved in NP (i.e., both one-player and two-player pushdown games with mean-payoff objectives under modular strategies are NP-complete). We also establish the optimal strategy complexity showing that global strategies for mean-payoff objectives require infinite memory even in one-player pushdown games; and memoryless modular strategies are sufficient in two- player pushdown games. Finally we also show that all the problems have the same complexity if the stack boundedness condition is added, where along with the mean-payoff objective the player must also ensure that the stack height is bounded.' 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: Yaron full_name: Velner, Yaron last_name: Velner citation: ama: Chatterjee K, Velner Y. Mean-Payoff Pushdown Games. IST Austria; 2012. doi:10.15479/AT:IST-2012-0002 apa: Chatterjee, K., & Velner, Y. (2012). Mean-payoff pushdown games. IST Austria. https://doi.org/10.15479/AT:IST-2012-0002 chicago: Chatterjee, Krishnendu, and Yaron Velner. Mean-Payoff Pushdown Games. IST Austria, 2012. https://doi.org/10.15479/AT:IST-2012-0002. ieee: K. Chatterjee and Y. Velner, Mean-payoff pushdown games. IST Austria, 2012. ista: Chatterjee K, Velner Y. 2012. Mean-payoff pushdown games, IST Austria, 33p. mla: Chatterjee, Krishnendu, and Yaron Velner. Mean-Payoff Pushdown Games. IST Austria, 2012, doi:10.15479/AT:IST-2012-0002. short: K. Chatterjee, Y. Velner, Mean-Payoff Pushdown Games, IST Austria, 2012. date_created: 2018-12-12T11:38:59Z date_published: 2012-07-02T00:00:00Z date_updated: 2023-02-23T11:05:50Z day: '02' ddc: - '000' - '005' department: - _id: KrCh doi: 10.15479/AT:IST-2012-0002 file: - access_level: open_access checksum: a03c08c1589dbb0c96183a8bcf3ab240 content_type: application/pdf creator: system date_created: 2018-12-12T11:54:00Z date_updated: 2020-07-14T12:46:38Z file_id: '5522' file_name: IST-2012-002_IST-2012-0002.pdf file_size: 592098 relation: main_file file_date_updated: 2020-07-14T12:46:38Z has_accepted_license: '1' language: - iso: eng month: '07' oa: 1 oa_version: Published Version page: '33' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '10' related_material: record: - id: '2956' relation: later_version status: public status: public title: Mean-payoff pushdown games type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2012' ... --- _id: '5378' abstract: - lang: eng text: 'One central issue in the formal design and analysis of reactive systems is the notion of refinement that asks whether all behaviors of the implementation is allowed by the specification. The local interpretation of behavior leads to the notion of simulation. Alternating transition systems (ATSs) provide a general model for composite reactive systems, and the simulation relation for ATSs is known as alternating simulation. The simulation relation for fair transition systems is called fair simulation. In this work our main contributions are as follows: (1) We present an improved algorithm for fair simulation with Büchi fairness constraints; our algorithm requires O(n3 · m) time as compared to the previous known O(n6)-time algorithm, where n is the number of states and m is the number of transitions. (2) We present a game based algorithm for alternating simulation that requires O(m2)-time as compared to the previous known O((n · m)2)-time algorithm, where n is the number of states and m is the size of transition relation. (3) We present an iterative algorithm for alternating simulation that matches the time complexity of the game based algorithm, but is more space efficient than the game based algorithm.' 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: Siddhesh full_name: Chaubal, Siddhesh last_name: Chaubal - first_name: Pritish full_name: Kamath, Pritish last_name: Kamath citation: ama: Chatterjee K, Chaubal S, Kamath P. Faster Algorithms for Alternating Refinement Relations. IST Austria; 2012. doi:10.15479/AT:IST-2012-0001 apa: Chatterjee, K., Chaubal, S., & Kamath, P. (2012). Faster algorithms for alternating refinement relations. IST Austria. https://doi.org/10.15479/AT:IST-2012-0001 chicago: Chatterjee, Krishnendu, Siddhesh Chaubal, and Pritish Kamath. Faster Algorithms for Alternating Refinement Relations. IST Austria, 2012. https://doi.org/10.15479/AT:IST-2012-0001. ieee: K. Chatterjee, S. Chaubal, and P. Kamath, Faster algorithms for alternating refinement relations. IST Austria, 2012. ista: Chatterjee K, Chaubal S, Kamath P. 2012. Faster algorithms for alternating refinement relations, IST Austria, 21p. mla: Chatterjee, Krishnendu, et al. Faster Algorithms for Alternating Refinement Relations. IST Austria, 2012, doi:10.15479/AT:IST-2012-0001. short: K. Chatterjee, S. Chaubal, P. Kamath, Faster Algorithms for Alternating Refinement Relations, IST Austria, 2012. date_created: 2018-12-12T11:38:59Z date_published: 2012-07-04T00:00:00Z date_updated: 2023-02-23T12:21:38Z day: '04' ddc: - '000' - '005' department: - _id: KrCh doi: 10.15479/AT:IST-2012-0001 file: - access_level: open_access checksum: ec8d1857cc7095d3de5107a0162ced37 content_type: application/pdf creator: system date_created: 2018-12-12T11:53:28Z date_updated: 2020-07-14T12:46:39Z file_id: '5489' file_name: IST-2012-0001_IST-2012-0001.pdf file_size: 394256 relation: main_file file_date_updated: 2020-07-14T12:46:39Z has_accepted_license: '1' language: - iso: eng month: '07' oa: 1 oa_version: Published Version page: '21' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '14' related_material: record: - id: '497' relation: later_version status: public status: public title: Faster algorithms for alternating refinement relations type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2012' ... --- _id: '5396' abstract: - lang: eng text: We consider the problem of inference in agraphical model with binary variables. While in theory it is arguably preferable to compute marginal probabilities, in practice researchers often use MAP inference due to the availability of efficient discrete optimization algorithms. We bridge the gap between the two approaches by introducing the Discrete Marginals technique in which approximate marginals are obtained by minimizing an objective function with unary and pair-wise terms over a discretized domain. This allows the use of techniques originally devel-oped for MAP-MRF inference and learning. We explore two ways to set up the objective function - by discretizing the Bethe free energy and by learning it from training data. Experimental results show that for certain types of graphs a learned function can out-perform the Bethe approximation. We also establish a link between the Bethe free energy and submodular functions. alternative_title: - IST Austria Technical Report author: - first_name: Filip full_name: Korc, Filip id: 476A2FD6-F248-11E8-B48F-1D18A9856A87 last_name: Korc - first_name: Vladimir full_name: Kolmogorov, Vladimir id: 3D50B0BA-F248-11E8-B48F-1D18A9856A87 last_name: Kolmogorov - first_name: Christoph full_name: Lampert, Christoph id: 40C20FD2-F248-11E8-B48F-1D18A9856A87 last_name: Lampert orcid: 0000-0001-8622-7887 citation: ama: Korc F, Kolmogorov V, Lampert C. Approximating Marginals Using Discrete Energy Minimization. IST Austria; 2012. doi:10.15479/AT:IST-2012-0003 apa: Korc, F., Kolmogorov, V., & Lampert, C. (2012). Approximating marginals using discrete energy minimization. IST Austria. https://doi.org/10.15479/AT:IST-2012-0003 chicago: Korc, Filip, Vladimir Kolmogorov, and Christoph Lampert. Approximating Marginals Using Discrete Energy Minimization. IST Austria, 2012. https://doi.org/10.15479/AT:IST-2012-0003. ieee: F. Korc, V. Kolmogorov, and C. Lampert, Approximating marginals using discrete energy minimization. IST Austria, 2012. ista: Korc F, Kolmogorov V, Lampert C. 2012. Approximating marginals using discrete energy minimization, IST Austria, 13p. mla: Korc, Filip, et al. Approximating Marginals Using Discrete Energy Minimization. IST Austria, 2012, doi:10.15479/AT:IST-2012-0003. short: F. Korc, V. Kolmogorov, C. Lampert, Approximating Marginals Using Discrete Energy Minimization, IST Austria, 2012. date_created: 2018-12-12T11:39:06Z date_published: 2012-07-23T00:00:00Z date_updated: 2023-02-23T11:13:22Z day: '23' ddc: - '000' department: - _id: VlKo - _id: ChLa doi: 10.15479/AT:IST-2012-0003 file: - access_level: open_access checksum: 7e0ba85ad123b13223aaf6cdde2d288c content_type: application/pdf creator: system date_created: 2018-12-12T11:53:29Z date_updated: 2020-07-14T12:46:44Z file_id: '5490' file_name: IST-2012-0003_IST-2012-0003.pdf file_size: 618744 relation: main_file file_date_updated: 2020-07-14T12:46:44Z has_accepted_license: '1' language: - iso: eng month: '07' oa: 1 oa_version: Published Version page: '13' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '36' related_material: record: - id: '3124' relation: earlier_version status: public status: public title: Approximating marginals using discrete energy minimization type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2012' ...