--- _id: '495' abstract: - lang: eng text: An automaton with advice is a finite state automaton which has access to an additional fixed infinite string called an advice tape. We refine the Myhill-Nerode theorem to characterize the languages of finite strings that are accepted by automata with advice. We do the same for tree automata with advice. alternative_title: - EPTCS author: - first_name: Alex full_name: Kruckman, Alex last_name: Kruckman - first_name: Sasha full_name: Rubin, Sasha id: 2EC51194-F248-11E8-B48F-1D18A9856A87 last_name: Rubin - first_name: John full_name: Sheridan, John last_name: Sheridan - first_name: Ben full_name: Zax, Ben last_name: Zax citation: ama: 'Kruckman A, Rubin S, Sheridan J, Zax B. A Myhill Nerode theorem for automata with advice. In: Proceedings GandALF 2012. Vol 96. Open Publishing Association; 2012:238-246. doi:10.4204/EPTCS.96.18' apa: 'Kruckman, A., Rubin, S., Sheridan, J., & Zax, B. (2012). A Myhill Nerode theorem for automata with advice. In Proceedings GandALF 2012 (Vol. 96, pp. 238–246). Napoli, Italy: Open Publishing Association. https://doi.org/10.4204/EPTCS.96.18' chicago: Kruckman, Alex, Sasha Rubin, John Sheridan, and Ben Zax. “A Myhill Nerode Theorem for Automata with Advice.” In Proceedings GandALF 2012, 96:238–46. Open Publishing Association, 2012. https://doi.org/10.4204/EPTCS.96.18. ieee: A. Kruckman, S. Rubin, J. Sheridan, and B. Zax, “A Myhill Nerode theorem for automata with advice,” in Proceedings GandALF 2012, Napoli, Italy, 2012, vol. 96, pp. 238–246. ista: 'Kruckman A, Rubin S, Sheridan J, Zax B. 2012. A Myhill Nerode theorem for automata with advice. Proceedings GandALF 2012. GandALF: Games, Automata, Logics and Formal Verification, EPTCS, vol. 96, 238–246.' mla: Kruckman, Alex, et al. “A Myhill Nerode Theorem for Automata with Advice.” Proceedings GandALF 2012, vol. 96, Open Publishing Association, 2012, pp. 238–46, doi:10.4204/EPTCS.96.18. short: A. Kruckman, S. Rubin, J. Sheridan, B. Zax, in:, Proceedings GandALF 2012, Open Publishing Association, 2012, pp. 238–246. conference: end_date: 2012-09-08 location: Napoli, Italy name: 'GandALF: Games, Automata, Logics and Formal Verification' start_date: 2012-09-06 date_created: 2018-12-11T11:46:47Z date_published: 2012-10-07T00:00:00Z date_updated: 2021-01-12T08:01:04Z day: '07' ddc: - '004' department: - _id: KrCh doi: 10.4204/EPTCS.96.18 ec_funded: 1 file: - access_level: open_access checksum: 56277f95edc9d531fa3bdc5f9579fda8 content_type: application/pdf creator: system date_created: 2018-12-12T10:15:31Z date_updated: 2020-07-14T12:46:35Z file_id: '5152' file_name: IST-2018-944-v1+1_2012_Rubin_A_Myhill.pdf file_size: 97736 relation: main_file file_date_updated: 2020-07-14T12:46:35Z has_accepted_license: '1' intvolume: ' 96' language: - iso: eng month: '10' oa: 1 oa_version: Published Version page: 238 - 246 project: - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' publication: Proceedings GandALF 2012 publication_status: published publisher: Open Publishing Association publist_id: '7325' pubrep_id: '944' quality_controlled: '1' scopus_import: 1 status: public title: A Myhill Nerode theorem for automata with advice tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 96 year: '2012' ... --- _id: '496' abstract: - lang: eng text: 'We study the expressive power of logical interpretations on the class of scattered trees, namely those with countably many infinite branches. Scattered trees can be thought of as the tree analogue of scattered linear orders. Every scattered tree has an ordinal rank that reflects the structure of its infinite branches. We prove, roughly, that trees and orders of large rank cannot be interpreted in scattered trees of small rank. We consider a quite general notion of interpretation: each element of the interpreted structure is represented by a set of tuples of subsets of the interpreting tree. Our trees are countable, not necessarily finitely branching, and may have finitely many unary predicates as labellings. We also show how to replace injective set-interpretations in (not necessarily scattered) trees by ''finitary'' set-interpretations.' alternative_title: - LICS article_number: '6280474' author: - first_name: Alexander full_name: Rabinovich, Alexander last_name: Rabinovich - first_name: Sasha full_name: Rubin, Sasha id: 2EC51194-F248-11E8-B48F-1D18A9856A87 last_name: Rubin citation: ama: 'Rabinovich A, Rubin S. Interpretations in trees with countably many branches. In: IEEE; 2012. doi:10.1109/LICS.2012.65' apa: 'Rabinovich, A., & Rubin, S. (2012). Interpretations in trees with countably many branches. Presented at the LICS: Symposium on Logic in Computer Science, Dubrovnik, Croatia: IEEE. https://doi.org/10.1109/LICS.2012.65' chicago: Rabinovich, Alexander, and Sasha Rubin. “Interpretations in Trees with Countably Many Branches.” IEEE, 2012. https://doi.org/10.1109/LICS.2012.65. ieee: 'A. Rabinovich and S. Rubin, “Interpretations in trees with countably many branches,” presented at the LICS: Symposium on Logic in Computer Science, Dubrovnik, Croatia, 2012.' ista: 'Rabinovich A, Rubin S. 2012. Interpretations in trees with countably many branches. LICS: Symposium on Logic in Computer Science, LICS, , 6280474.' mla: Rabinovich, Alexander, and Sasha Rubin. Interpretations in Trees with Countably Many Branches. 6280474, IEEE, 2012, doi:10.1109/LICS.2012.65. short: A. Rabinovich, S. Rubin, in:, IEEE, 2012. conference: end_date: 2012-06-28 location: Dubrovnik, Croatia name: 'LICS: Symposium on Logic in Computer Science' start_date: 2012-06-25 date_created: 2018-12-11T11:46:47Z date_published: 2012-01-01T00:00:00Z date_updated: 2021-01-12T08:01:05Z day: '01' department: - _id: KrCh doi: 10.1109/LICS.2012.65 ec_funded: 1 language: - iso: eng main_file_link: - open_access: '1' url: https://arise.or.at/pubpdf/Interpretations_in_Trees_with_Countably_Many_Branches.pdf month: '01' oa: 1 oa_version: Preprint project: - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering publication_status: published publisher: IEEE publist_id: '7324' quality_controlled: '1' scopus_import: 1 status: public title: Interpretations in trees with countably many branches type: conference user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 year: '2012' ... --- _id: '497' 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(n 3·m) time as compared to the previous known O(n 6)-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. © Krishnendu Chatterjee, Siddhesh Chaubal, and Pritish Kamath.' alternative_title: - LIPIcs author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: 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. In: Vol 16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2012:167-182. doi:10.4230/LIPIcs.CSL.2012.167' apa: 'Chatterjee, K., Chaubal, S., & Kamath, P. (2012). Faster algorithms for alternating refinement relations (Vol. 16, pp. 167–182). Presented at the EACSL: European Association for Computer Science Logic, Fontainebleau, France: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CSL.2012.167' chicago: Chatterjee, Krishnendu, Siddhesh Chaubal, and Pritish Kamath. “Faster Algorithms for Alternating Refinement Relations,” 16:167–82. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. https://doi.org/10.4230/LIPIcs.CSL.2012.167. ieee: 'K. Chatterjee, S. Chaubal, and P. Kamath, “Faster algorithms for alternating refinement relations,” presented at the EACSL: European Association for Computer Science Logic, Fontainebleau, France, 2012, vol. 16, pp. 167–182.' ista: 'Chatterjee K, Chaubal S, Kamath P. 2012. Faster algorithms for alternating refinement relations. EACSL: European Association for Computer Science Logic, LIPIcs, vol. 16, 167–182.' mla: Chatterjee, Krishnendu, et al. Faster Algorithms for Alternating Refinement Relations. Vol. 16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012, pp. 167–82, doi:10.4230/LIPIcs.CSL.2012.167. short: K. Chatterjee, S. Chaubal, P. Kamath, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012, pp. 167–182. conference: end_date: 2012-09-06 location: Fontainebleau, France name: 'EACSL: European Association for Computer Science Logic' start_date: 2012-09-03 date_created: 2018-12-11T11:46:48Z date_published: 2012-09-01T00:00:00Z date_updated: 2023-02-23T12:23:32Z day: '01' ddc: - '004' department: - _id: KrCh doi: 10.4230/LIPIcs.CSL.2012.167 ec_funded: 1 file: - access_level: open_access checksum: f1b0dd99240800db2d7dbf9b5131fe5e content_type: application/pdf creator: system date_created: 2018-12-12T10:08:50Z date_updated: 2020-07-14T12:46:35Z file_id: '4712' file_name: IST-2018-943-v1+1_2012_Chatterjee_Faster_Algorithms.pdf file_size: 471236 relation: main_file file_date_updated: 2020-07-14T12:46:35Z has_accepted_license: '1' intvolume: ' 16' language: - iso: eng license: https://creativecommons.org/licenses/by-nc-nd/4.0/ month: '09' oa: 1 oa_version: Published Version page: 167 - 182 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik publist_id: '7323' pubrep_id: '943' quality_controlled: '1' related_material: record: - id: '5378' relation: earlier_version status: public scopus_import: 1 status: public title: Faster algorithms for alternating refinement relations tmp: image: /images/cc_by_nc_nd.png legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0) short: CC BY-NC-ND (4.0) type: conference user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 16 year: '2012' ... --- _id: '3165' abstract: - lang: eng text: Computing the winning set for Büchi objectives in alternating games on graphs is a central problem in computer aided verification with a large number of applications. The long standing best known upper bound for solving the problem is Õ(n·m), where n is the number of vertices and m is the number of edges in the graph. We are the first to break the Õ(n·m) boundary by presenting a new technique that reduces the running time to O(n 2). This bound also leads to O(n 2) time algorithms for computing the set of almost-sure winning vertices for Büchi objectives (1) in alternating games with probabilistic transitions (improving an earlier bound of Õ(n·m)), (2) in concurrent graph games with constant actions (improving an earlier bound of O(n 3)), and (3) in Markov decision processes (improving for m > n 4/3 an earlier bound of O(min(m 1.5, m·n 2/3)). We also show that the same technique can be used to compute the maximal end-component decomposition of a graph in time O(n 2), which is an improvement over earlier bounds for m > n 4/3. Finally, we show how to maintain the winning set for Büchi objectives in alternating games under a sequence of edge insertions or a sequence of edge deletions in O(n) amortized time per operation. This is the first dynamic algorithm for this problem. acknowledgement: 'The research was supported by Austrian Science Fund (FWF) Grant No P 23499-N23 on Modern Graph Algorithmic Techniques in Formal Verification, Vienna Science and Technology Fund (WWTF) Grant ICT10-002, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.' article_processing_charge: No author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Monika H full_name: Henzinger, Monika H id: 540c9bbd-f2de-11ec-812d-d04a5be85630 last_name: Henzinger orcid: 0000-0002-5008-6530 citation: ama: 'Chatterjee K, Henzinger MH. An O(n2) time algorithm for alternating Büchi games. In: Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms. SIAM; 2012:1386-1399. doi:10.1137/1.9781611973099.109' apa: 'Chatterjee, K., & Henzinger, M. H. (2012). An O(n2) time algorithm for alternating Büchi games. In Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms (pp. 1386–1399). Kyoto, Japan: SIAM. https://doi.org/10.1137/1.9781611973099.109' chicago: Chatterjee, Krishnendu, and Monika H Henzinger. “An O(N2) Time Algorithm for Alternating Büchi Games.” In Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms, 1386–99. SIAM, 2012. https://doi.org/10.1137/1.9781611973099.109. ieee: K. Chatterjee and M. H. Henzinger, “An O(n2) time algorithm for alternating Büchi games,” in Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms, Kyoto, Japan, 2012, pp. 1386–1399. ista: 'Chatterjee K, Henzinger MH. 2012. An O(n2) time algorithm for alternating Büchi games. Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms. SODA: Symposium on Discrete Algorithms, 1386–1399.' mla: Chatterjee, Krishnendu, and Monika H. Henzinger. “An O(N2) Time Algorithm for Alternating Büchi Games.” Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms, SIAM, 2012, pp. 1386–99, doi:10.1137/1.9781611973099.109. short: K. Chatterjee, M.H. Henzinger, in:, Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms, SIAM, 2012, pp. 1386–1399. conference: end_date: 2012-01-19 location: Kyoto, Japan name: 'SODA: Symposium on Discrete Algorithms' start_date: 2012-01-17 date_created: 2018-12-11T12:01:46Z date_published: 2012-01-01T00:00:00Z date_updated: 2023-02-23T12:23:35Z day: '01' department: - _id: KrCh doi: 10.1137/1.9781611973099.109 ec_funded: 1 external_id: arxiv: - '1109.5018' language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/1109.5018 month: '01' oa: 1 oa_version: None page: 1386 - 1399 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms publication_status: published publisher: SIAM publist_id: '3519' pubrep_id: '15' quality_controlled: '1' related_material: record: - id: '2141' relation: later_version status: public - id: '5379' relation: earlier_version status: public status: public title: An O(n2) time algorithm for alternating Büchi games type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2012' ... --- _id: '2956' 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 parity 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 computational 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.' acknowledgement: "The research was supported by Austrian Science Fund (FWF) Grant No P 23499-N23, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), Microsoft faculty fellows award, the Israeli Centers of Research Excellence (ICORE) program, (Center No. 4/11), the RICH Model Toolkit (ICT COST Action IC0901), and was carried out in partial fulfillment of the requirements for the Ph.D. degree of the second author.\r\nA Technical Report of this paper is available via internal link." article_number: '6280438' 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. In: Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE; 2012. doi:10.1109/LICS.2012.30' apa: 'Chatterjee, K., & Velner, Y. (2012). Mean payoff pushdown games. In Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science. Dubrovnik, Croatia : IEEE. https://doi.org/10.1109/LICS.2012.30' chicago: Chatterjee, Krishnendu, and Yaron Velner. “Mean Payoff Pushdown Games.” In Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE, 2012. https://doi.org/10.1109/LICS.2012.30. ieee: K. Chatterjee and Y. Velner, “Mean payoff pushdown games,” in Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, Dubrovnik, Croatia , 2012. ista: 'Chatterjee K, Velner Y. 2012. Mean payoff pushdown games. Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 6280438.' mla: Chatterjee, Krishnendu, and Yaron Velner. “Mean Payoff Pushdown Games.” Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, 6280438, IEEE, 2012, doi:10.1109/LICS.2012.30. short: K. Chatterjee, Y. Velner, in:, Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2012. conference: end_date: 2012-06-28 location: 'Dubrovnik, Croatia ' name: 'LICS: Logic in Computer Science' start_date: 2012-06-25 date_created: 2018-12-11T12:00:32Z date_published: 2012-08-23T00:00:00Z date_updated: 2023-02-23T12:23:30Z day: '23' department: - _id: KrCh doi: 10.1109/LICS.2012.30 ec_funded: 1 language: - iso: eng month: '08' oa_version: None project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science publication_status: published publisher: IEEE publist_id: '3770' quality_controlled: '1' related_material: record: - id: '5377' relation: earlier_version status: public scopus_import: 1 status: public title: Mean payoff pushdown games type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2012' ... --- _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: '2955' abstract: - lang: eng text: 'We consider two-player stochastic games played on finite graphs with reachability objectives where the first player tries to ensure a target state to be visited almost-surely (i.e., with probability 1), or positively (i.e., with positive probability), no matter the strategy of the second player. We classify such games according to the information and the power of randomization available to the players. On the basis of information, the game can be one-sided with either (a) player 1, or (b) player 2 having partial observation (and the other player has perfect observation), or two-sided with (c) both players having partial observation. On the basis of randomization, the players (a) may not be allowed to use randomization (pure strategies), or (b) may choose a probability distribution over actions but the actual random choice is external and not visible to the player (actions invisible), or (c) may use full randomization. Our main results for pure strategies are as follows. (1) For one-sided games with player 1 having partial observation we show that (in contrast to full randomized strategies) belief-based (subset-construction based) strategies are not sufficient, and we present an exponential upper bound on memory both for almostsure and positive winning strategies; we show that the problem of deciding the existence of almost-sure and positive winning strategies for player 1 is EXPTIME-complete. (2) For one-sided games with player 2 having partial observation we show that non-elementary memory is both necessary and sufficient for both almost-sure and positive winning strategies. (3) We show that for the general (two-sided) case finite-memory strategies are sufficient for both positive and almost-sure winning, and at least non-elementary memory is required. We establish the equivalence of the almost-sure winning problems for pure strategies and for randomized strategies with actions invisible. Our equivalence result exhibits serious flaws in previous results of the literature: we show a non-elementary memory lower bound for almost-sure winning whereas an exponential upper bound was previously claimed.' acknowledgement: 'This work was partially supported by FWF Grant No P 23499-N23, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty fellows award.' article_number: '6280436' 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. Partial-observation stochastic games: How to win when belief fails. In: Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE; 2012. doi:10.1109/LICS.2012.28' apa: 'Chatterjee, K., & Doyen, L. (2012). Partial-observation stochastic games: How to win when belief fails. In Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science. Dubrovnik, Croatia: IEEE. https://doi.org/10.1109/LICS.2012.28' chicago: 'Chatterjee, Krishnendu, and Laurent Doyen. “Partial-Observation Stochastic Games: How to Win When Belief Fails.” In Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE, 2012. https://doi.org/10.1109/LICS.2012.28.' ieee: 'K. Chatterjee and L. Doyen, “Partial-observation stochastic games: How to win when belief fails,” in Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, Dubrovnik, Croatia, 2012.' ista: 'Chatterjee K, Doyen L. 2012. Partial-observation stochastic games: How to win when belief fails. Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 6280436.' mla: 'Chatterjee, Krishnendu, and Laurent Doyen. “Partial-Observation Stochastic Games: How to Win When Belief Fails.” Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, 6280436, IEEE, 2012, doi:10.1109/LICS.2012.28.' short: K. Chatterjee, L. Doyen, in:, Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2012. conference: end_date: 2012-06-28 location: Dubrovnik, Croatia name: 'LICS: Logic in Computer Science' start_date: 2012-06-25 date_created: 2018-12-11T12:00:32Z date_published: 2012-08-23T00:00:00Z date_updated: 2023-02-23T12:23:43Z day: '23' department: - _id: KrCh doi: 10.1109/LICS.2012.28 ec_funded: 1 external_id: arxiv: - '1107.2141' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1107.2141 month: '08' oa: 1 oa_version: Preprint project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science publication_status: published publisher: IEEE publist_id: '3771' quality_controlled: '1' related_material: record: - id: '2211' relation: later_version status: public - id: '5381' relation: earlier_version status: public scopus_import: 1 status: public title: 'Partial-observation stochastic games: How to win when belief fails' type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2012' ... --- _id: '3341' abstract: - lang: eng text: 'We consider two-player stochastic games played on a finite state space for an infinite number of rounds. The games are concurrent: in each round, the two players (player 1 and player 2) choose their moves independently and simultaneously; the current state and the two moves determine a probability distribution over the successor states. We also consider the important special case of turn-based stochastic games where players make moves in turns, rather than concurrently. We study concurrent games with \omega-regular winning conditions specified as parity objectives. The value for player 1 for a parity objective is the maximal probability with which the player can guarantee the satisfaction of the objective against all strategies of the opponent. We study the problem of continuity and robustness of the value function in concurrent and turn-based stochastic parity gameswith respect to imprecision in the transition probabilities. We present quantitative bounds on the difference of the value function (in terms of the imprecision of the transition probabilities) and show the value continuity for structurally equivalent concurrent games (two games are structurally equivalent if the support of the transition function is same and the probabilities differ). We also show robustness of optimal strategies for structurally equivalent turn-based stochastic parity games. Finally we show that the value continuity property breaks without the structurally equivalent assumption (even for Markov chains) and show that our quantitative bound is asymptotically optimal. Hence our results are tight (the assumption is both necessary and sufficient) and optimal (our quantitative bound is asymptotically optimal).' alternative_title: - LNCS author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X citation: ama: 'Chatterjee K. Robustness of structurally equivalent concurrent parity games. In: Vol 7213. Springer; 2012:270-285. doi:10.1007/978-3-642-28729-9_18' apa: 'Chatterjee, K. (2012). Robustness of structurally equivalent concurrent parity games (Vol. 7213, pp. 270–285). Presented at the FoSSaCS: Foundations of Software Science and Computation Structures, Tallinn, Estonia: Springer. https://doi.org/10.1007/978-3-642-28729-9_18' chicago: Chatterjee, Krishnendu. “Robustness of Structurally Equivalent Concurrent Parity Games,” 7213:270–85. Springer, 2012. https://doi.org/10.1007/978-3-642-28729-9_18. ieee: 'K. Chatterjee, “Robustness of structurally equivalent concurrent parity games,” presented at the FoSSaCS: Foundations of Software Science and Computation Structures, Tallinn, Estonia, 2012, vol. 7213, pp. 270–285.' ista: 'Chatterjee K. 2012. Robustness of structurally equivalent concurrent parity games. FoSSaCS: Foundations of Software Science and Computation Structures, LNCS, vol. 7213, 270–285.' mla: Chatterjee, Krishnendu. Robustness of Structurally Equivalent Concurrent Parity Games. Vol. 7213, Springer, 2012, pp. 270–85, doi:10.1007/978-3-642-28729-9_18. short: K. Chatterjee, in:, Springer, 2012, pp. 270–285. conference: end_date: 2012-04-01 location: Tallinn, Estonia name: 'FoSSaCS: Foundations of Software Science and Computation Structures' start_date: 2012-03-24 date_created: 2018-12-11T12:02:46Z date_published: 2012-03-22T00:00:00Z date_updated: 2023-02-23T12:23:46Z day: '22' department: - _id: KrCh doi: 10.1007/978-3-642-28729-9_18 ec_funded: 1 external_id: arxiv: - '1107.2009' intvolume: ' 7213' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1107.2009 month: '03' oa: 1 oa_version: Preprint page: 270 - 285 project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication_status: published publisher: Springer publist_id: '3284' quality_controlled: '1' related_material: record: - id: '5382' relation: earlier_version status: public scopus_import: 1 status: public title: Robustness of structurally equivalent concurrent parity games type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 7213 year: '2012' ... --- _id: '2957' abstract: - lang: eng text: 'We consider probabilistic automata on infinite words with acceptance defined by parity conditions. We consider three qualitative decision problems: (i) the positive decision problem asks whether there is a word that is accepted with positive probability; (ii) the almost decision problem asks whether there is a word that is accepted with probability 1; and (iii) the limit decision problem asks whether words are accepted with probability arbitrarily close to 1. We unify and generalize several decidability results for probabilistic automata over infinite words, and identify a robust (closed under union and intersection) subclass of probabilistic automata for which all the qualitative decision problems are decidable for parity conditions. We also show that if the input words are restricted to lasso shape (regular) words, then the positive and almost problems are decidable for all probabilistic automata with parity conditions. For most decidable problems we show an optimal PSPACE-complete complexity bound.' article_number: '6280437' author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Mathieu full_name: Tracol, Mathieu id: 3F54FA38-F248-11E8-B48F-1D18A9856A87 last_name: Tracol citation: ama: 'Chatterjee K, Tracol M. Decidable problems for probabilistic automata on infinite words. In: Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE; 2012. doi:10.1109/LICS.2012.29' apa: 'Chatterjee, K., & Tracol, M. (2012). Decidable problems for probabilistic automata on infinite words. In Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science. Dubrovnik, Croatia : IEEE. https://doi.org/10.1109/LICS.2012.29' chicago: Chatterjee, Krishnendu, and Mathieu Tracol. “Decidable Problems for Probabilistic Automata on Infinite Words.” In Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE, 2012. https://doi.org/10.1109/LICS.2012.29. ieee: K. Chatterjee and M. Tracol, “Decidable problems for probabilistic automata on infinite words,” in Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, Dubrovnik, Croatia , 2012. ista: 'Chatterjee K, Tracol M. 2012. Decidable problems for probabilistic automata on infinite words. Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 6280437.' mla: Chatterjee, Krishnendu, and Mathieu Tracol. “Decidable Problems for Probabilistic Automata on Infinite Words.” Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, 6280437, IEEE, 2012, doi:10.1109/LICS.2012.29. short: K. Chatterjee, M. Tracol, in:, Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2012. conference: end_date: 2012-06-28 location: 'Dubrovnik, Croatia ' name: 'LICS: Logic in Computer Science' start_date: 2012-06-25 date_created: 2018-12-11T12:00:33Z date_published: 2012-08-23T00:00:00Z date_updated: 2023-02-23T12:23:51Z day: '23' department: - _id: KrCh doi: 10.1109/LICS.2012.29 ec_funded: 1 external_id: arxiv: - '1107.2091' language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/1107.2091 month: '08' oa: 1 oa_version: Preprint project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science publication_status: published publisher: IEEE publist_id: '3769' quality_controlled: '1' related_material: record: - id: '5384' relation: earlier_version status: public scopus_import: 1 status: public title: Decidable problems for probabilistic automata on infinite words type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2012' ... --- _id: '10905' abstract: - lang: eng text: "Energy games belong to a class of turn-based two-player infinite-duration games played on a weighted directed graph. It is one of the rare and intriguing combinatorial problems that lie in NP ∩ co−NP, but are not known to be in P. While the existence of polynomial-time algorithms has been a major open problem for decades, there is no algorithm that solves any non-trivial subclass in polynomial time.\r\nIn this paper, we give several results based on the weight structures of the graph. First, we identify a notion of penalty and present a polynomial-time algorithm when the penalty is large. Our algorithm is the first polynomial-time algorithm on a large class of weighted graphs. It includes several counter examples that show that many previous algorithms, such as value iteration and random facet algorithms, require at least sub-exponential time. Our main technique is developing the first non-trivial approximation algorithm and showing how to convert it to an exact algorithm. Moreover, we show that in a practical case in verification where weights are clustered around a constant number of values, the energy game problem can be solved in polynomial time. We also show that the problem is still as hard as in general when the clique-width is bounded or the graph is strongly ergodic, suggesting that restricting graph structures need not help." acknowledgement: 'Supported by the Austrian Science Fund (FWF): P23499-N23, the Austrian Science Fund (FWF): S11407-N23 (RiSE), an ERC Start Grant (279307: Graph Games), and a Microsoft Faculty Fellows Award' alternative_title: - LNCS article_processing_charge: No author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Monika H full_name: Henzinger, Monika H id: 540c9bbd-f2de-11ec-812d-d04a5be85630 last_name: Henzinger orcid: 0000-0002-5008-6530 - first_name: Sebastian full_name: Krinninger, Sebastian last_name: Krinninger - first_name: Danupon full_name: Nanongkai, Danupon last_name: Nanongkai citation: ama: 'Chatterjee K, Henzinger MH, Krinninger S, Nanongkai D. Polynomial-time algorithms for energy games with special weight structures. In: Algorithms – ESA 2012. Vol 7501. Springer; 2012:301-312. doi:10.1007/978-3-642-33090-2_27' apa: 'Chatterjee, K., Henzinger, M. H., Krinninger, S., & Nanongkai, D. (2012). Polynomial-time algorithms for energy games with special weight structures. In Algorithms – ESA 2012 (Vol. 7501, pp. 301–312). Ljubljana, Slovenia: Springer. https://doi.org/10.1007/978-3-642-33090-2_27' chicago: Chatterjee, Krishnendu, Monika H Henzinger, Sebastian Krinninger, and Danupon Nanongkai. “Polynomial-Time Algorithms for Energy Games with Special Weight Structures.” In Algorithms – ESA 2012, 7501:301–12. Springer, 2012. https://doi.org/10.1007/978-3-642-33090-2_27. ieee: K. Chatterjee, M. H. Henzinger, S. Krinninger, and D. Nanongkai, “Polynomial-time algorithms for energy games with special weight structures,” in Algorithms – ESA 2012, Ljubljana, Slovenia, 2012, vol. 7501, pp. 301–312. ista: 'Chatterjee K, Henzinger MH, Krinninger S, Nanongkai D. 2012. Polynomial-time algorithms for energy games with special weight structures. Algorithms – ESA 2012. ESA: European Symposium on Algorithms, LNCS, vol. 7501, 301–312.' mla: Chatterjee, Krishnendu, et al. “Polynomial-Time Algorithms for Energy Games with Special Weight Structures.” Algorithms – ESA 2012, vol. 7501, Springer, 2012, pp. 301–12, doi:10.1007/978-3-642-33090-2_27. short: K. Chatterjee, M.H. Henzinger, S. Krinninger, D. Nanongkai, in:, Algorithms – ESA 2012, Springer, 2012, pp. 301–312. conference: end_date: 2012-09-12 location: Ljubljana, Slovenia name: 'ESA: European Symposium on Algorithms' start_date: 2012-09-10 date_created: 2022-03-21T08:01:45Z date_published: 2012-10-01T00:00:00Z date_updated: 2023-09-05T14:09:30Z day: '01' department: - _id: KrCh doi: 10.1007/978-3-642-33090-2_27 ec_funded: 1 external_id: arxiv: - '1604.08234' intvolume: ' 7501' language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/1604.08234 month: '10' oa: 1 oa_version: Preprint page: 301-312 project: - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: Algorithms – ESA 2012 publication_identifier: eisbn: - '9783642330902' eissn: - 1611-3349 isbn: - '9783642330896' issn: - 0302-9743 publication_status: published publisher: Springer quality_controlled: '1' related_material: record: - id: '535' relation: later_version status: public scopus_import: '1' status: public title: Polynomial-time algorithms for energy games with special weight structures type: conference user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1 volume: 7501 year: '2012' ... --- _id: '3157' abstract: - lang: eng text: Colorectal tumours that are wild type for KRAS are often sensitive to EGFR blockade, but almost always develop resistance within several months of initiating therapy. The mechanisms underlying this acquired resistance to anti-EGFR antibodies are largely unknown. This situation is in marked contrast to that of small-molecule targeted agents, such as inhibitors of ABL, EGFR, BRAF and MEK, in which mutations in the genes encoding the protein targets render the tumours resistant to the effects of the drugs. The simplest hypothesis to account for the development of resistance to EGFR blockade is that rare cells with KRAS mutations pre-exist at low levels in tumours with ostensibly wild-type KRAS genes. Although this hypothesis would seem readily testable, there is no evidence in pre-clinical models to support it, nor is there data from patients. To test this hypothesis, we determined whether mutant KRAS DNA could be detected in the circulation of 28 patients receiving monotherapy with panitumumab, a therapeutic anti-EGFR antibody. We found that 9 out of 24 (38%) patients whose tumours were initially KRAS wild type developed detectable mutations in KRAS in their sera, three of which developed multiple different KRAS mutations. The appearance of these mutations was very consistent, generally occurring between 5 and 6months following treatment. Mathematical modelling indicated that the mutations were present in expanded subclones before the initiation of panitumumab treatment. These results suggest that the emergence of KRAS mutations is a mediator of acquired resistance to EGFR blockade and that these mutations can be detected in a non-invasive manner. They explain why solid tumours develop resistance to targeted therapies in a highly reproducible fashion. author: - first_name: Luis full_name: Diaz Jr, Luis last_name: Diaz Jr - first_name: Richard full_name: Williams, Richard last_name: Williams - first_name: Jian full_name: Wu, Jian last_name: Wu - first_name: Isaac full_name: Kinde, Isaac last_name: Kinde - first_name: Joel full_name: Hecht, Joel last_name: Hecht - first_name: Jordan full_name: Berlin, Jordan last_name: Berlin - first_name: Benjamin full_name: Allen, Benjamin last_name: Allen - first_name: Ivana full_name: Božić, Ivana last_name: Božić - first_name: Johannes full_name: Reiter, Johannes id: 4A918E98-F248-11E8-B48F-1D18A9856A87 last_name: Reiter orcid: 0000-0002-0170-7353 - first_name: Martin full_name: Nowak, Martin last_name: Nowak - first_name: Kenneth full_name: Kinzler, Kenneth last_name: Kinzler - first_name: Kelly full_name: Oliner, Kelly last_name: Oliner - first_name: Bert full_name: Vogelstein, Bert last_name: Vogelstein citation: ama: Diaz Jr L, Williams R, Wu J, et al. The molecular evolution of acquired resistance to targeted EGFR blockade in colorectal cancers. Nature. 2012;486(7404):537-540. doi:10.1038/nature11219 apa: Diaz Jr, L., Williams, R., Wu, J., Kinde, I., Hecht, J., Berlin, J., … Vogelstein, B. (2012). The molecular evolution of acquired resistance to targeted EGFR blockade in colorectal cancers. Nature. Nature Publishing Group. https://doi.org/10.1038/nature11219 chicago: Diaz Jr, Luis, Richard Williams, Jian Wu, Isaac Kinde, Joel Hecht, Jordan Berlin, Benjamin Allen, et al. “The Molecular Evolution of Acquired Resistance to Targeted EGFR Blockade in Colorectal Cancers.” Nature. Nature Publishing Group, 2012. https://doi.org/10.1038/nature11219. ieee: L. Diaz Jr et al., “The molecular evolution of acquired resistance to targeted EGFR blockade in colorectal cancers,” Nature, vol. 486, no. 7404. Nature Publishing Group, pp. 537–540, 2012. ista: Diaz Jr L, Williams R, Wu J, Kinde I, Hecht J, Berlin J, Allen B, Božić I, Reiter J, Nowak M, Kinzler K, Oliner K, Vogelstein B. 2012. The molecular evolution of acquired resistance to targeted EGFR blockade in colorectal cancers. Nature. 486(7404), 537–540. mla: Diaz Jr, Luis, et al. “The Molecular Evolution of Acquired Resistance to Targeted EGFR Blockade in Colorectal Cancers.” Nature, vol. 486, no. 7404, Nature Publishing Group, 2012, pp. 537–40, doi:10.1038/nature11219. short: L. Diaz Jr, R. Williams, J. Wu, I. Kinde, J. Hecht, J. Berlin, B. Allen, I. Božić, J. Reiter, M. Nowak, K. Kinzler, K. Oliner, B. Vogelstein, Nature 486 (2012) 537–540. date_created: 2018-12-11T12:01:43Z date_published: 2012-06-28T00:00:00Z date_updated: 2023-09-07T11:40:43Z day: '28' department: - _id: KrCh doi: 10.1038/nature11219 ec_funded: 1 external_id: pmid: - '22722843' intvolume: ' 486' issue: '7404' language: - iso: eng main_file_link: - open_access: '1' url: http://www.ncbi.nlm.nih.gov/pmc/articles/PMC3436069/ month: '06' oa: 1 oa_version: Submitted Version page: 537 - 540 pmid: 1 project: - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering publication: Nature publication_status: published publisher: Nature Publishing Group publist_id: '3537' quality_controlled: '1' related_material: record: - id: '1400' relation: dissertation_contains status: public scopus_import: 1 status: public title: The molecular evolution of acquired resistance to targeted EGFR blockade in colorectal cancers type: journal_article user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 486 year: '2012' ... --- _id: '3260' abstract: - lang: eng text: "Many scenarios in the living world, where individual organisms compete for winning positions (or resources), have properties of auctions. Here we study the evolution of bids in biological auctions. For each auction, n individuals are drawn at random from a population of size N. Each individual makes a bid which entails a cost. The winner obtains a benefit of a certain value. Costs and benefits are translated into reproductive success (fitness). Therefore, successful bidding strategies spread in the population. We compare two types of auctions. In “biological all-pay auctions”, the costs are the bid for every participating individual. In “biological second price all-pay auctions”, the cost for everyone other than the winner is the bid, but the cost for the winner is the second highest bid. Second price all-pay auctions are generalizations of the “war of attrition” introduced by Maynard Smith. We study evolutionary dynamics in both types of auctions. We calculate pairwise invasion plots and evolutionarily stable distributions over the continuous strategy space. We find that the average bid in second price all-pay auctions is higher than in all-pay auctions, but the average cost for the winner is similar in both auctions. In both cases, the average bid is a declining function of the number of participants, n. The more individuals participate in an auction the smaller is the chance of winning, and thus expensive bids must be avoided.\r\n" author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Johannes full_name: Reiter, Johannes id: 4A918E98-F248-11E8-B48F-1D18A9856A87 last_name: Reiter orcid: 0000-0002-0170-7353 - first_name: Martin full_name: Nowak, Martin last_name: Nowak citation: ama: Chatterjee K, Reiter J, Nowak M. Evolutionary dynamics of biological auctions. Theoretical Population Biology. 2012;81(1):69-80. doi:10.1016/j.tpb.2011.11.003 apa: Chatterjee, K., Reiter, J., & Nowak, M. (2012). Evolutionary dynamics of biological auctions. Theoretical Population Biology. Academic Press. https://doi.org/10.1016/j.tpb.2011.11.003 chicago: Chatterjee, Krishnendu, Johannes Reiter, and Martin Nowak. “Evolutionary Dynamics of Biological Auctions.” Theoretical Population Biology. Academic Press, 2012. https://doi.org/10.1016/j.tpb.2011.11.003. ieee: K. Chatterjee, J. Reiter, and M. Nowak, “Evolutionary dynamics of biological auctions,” Theoretical Population Biology, vol. 81, no. 1. Academic Press, pp. 69–80, 2012. ista: Chatterjee K, Reiter J, Nowak M. 2012. Evolutionary dynamics of biological auctions. Theoretical Population Biology. 81(1), 69–80. mla: Chatterjee, Krishnendu, et al. “Evolutionary Dynamics of Biological Auctions.” Theoretical Population Biology, vol. 81, no. 1, Academic Press, 2012, pp. 69–80, doi:10.1016/j.tpb.2011.11.003. short: K. Chatterjee, J. Reiter, M. Nowak, Theoretical Population Biology 81 (2012) 69–80. date_created: 2018-12-11T12:02:19Z date_published: 2012-02-01T00:00:00Z date_updated: 2023-09-07T11:40:43Z day: '01' department: - _id: KrCh doi: 10.1016/j.tpb.2011.11.003 ec_funded: 1 external_id: pmid: - '22120126' intvolume: ' 81' issue: '1' language: - iso: eng main_file_link: - open_access: '1' url: 'http://www.ncbi.nlm.nih.gov/pmc/articles/PMC3279759/ ' month: '02' oa: 1 oa_version: Submitted Version page: 69 - 80 pmid: 1 project: - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: Theoretical Population Biology publication_status: published publisher: Academic Press publist_id: '3388' quality_controlled: '1' related_material: record: - id: '1400' relation: dissertation_contains status: public scopus_import: 1 status: public title: Evolutionary dynamics of biological auctions type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 81 year: '2012' ... --- _id: '3316' abstract: - lang: eng text: In addition to being correct, a system should be robust, that is, it should behave reasonably even after receiving unexpected inputs. In this paper, we summarize two formal notions of robustness that we have introduced previously for reactive systems. One of the notions is based on assigning costs for failures on a user-provided notion of incorrect transitions in a specification. Here, we define a system to be robust if a finite number of incorrect inputs does not lead to an infinite number of incorrect outputs. We also give a more refined notion of robustness that aims to minimize the ratio of output failures to input failures. The second notion is aimed at liveness. In contrast to the previous notion, it has no concept of recovery from an error. Instead, it compares the ratio of the number of liveness constraints that the system violates to the number of liveness constraints that the environment violates. article_processing_charge: No author: - first_name: Roderick full_name: Bloem, Roderick last_name: Bloem - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Karin full_name: Greimel, Karin last_name: Greimel - 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: Barbara full_name: Jobstmann, Barbara last_name: Jobstmann citation: ama: 'Bloem R, Chatterjee K, Greimel K, Henzinger TA, Jobstmann B. Specification-centered robustness. In: 6th IEEE International Symposium on Industrial and Embedded Systems. IEEE; 2011:176-185. doi:10.1109/SIES.2011.5953660' apa: 'Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T. A., & Jobstmann, B. (2011). Specification-centered robustness. In 6th IEEE International Symposium on Industrial and Embedded Systems (pp. 176–185). Vasteras, Sweden: IEEE. https://doi.org/10.1109/SIES.2011.5953660' chicago: Bloem, Roderick, Krishnendu Chatterjee, Karin Greimel, Thomas A Henzinger, and Barbara Jobstmann. “Specification-Centered Robustness.” In 6th IEEE International Symposium on Industrial and Embedded Systems, 176–85. IEEE, 2011. https://doi.org/10.1109/SIES.2011.5953660. ieee: R. Bloem, K. Chatterjee, K. Greimel, T. A. Henzinger, and B. Jobstmann, “Specification-centered robustness,” in 6th IEEE International Symposium on Industrial and Embedded Systems, Vasteras, Sweden, 2011, pp. 176–185. ista: 'Bloem R, Chatterjee K, Greimel K, Henzinger TA, Jobstmann B. 2011. Specification-centered robustness. 6th IEEE International Symposium on Industrial and Embedded Systems. SIES: International Symposium on Industrial Embedded Systems, 176–185.' mla: Bloem, Roderick, et al. “Specification-Centered Robustness.” 6th IEEE International Symposium on Industrial and Embedded Systems, IEEE, 2011, pp. 176–85, doi:10.1109/SIES.2011.5953660. short: R. Bloem, K. Chatterjee, K. Greimel, T.A. Henzinger, B. Jobstmann, in:, 6th IEEE International Symposium on Industrial and Embedded Systems, IEEE, 2011, pp. 176–185. conference: end_date: 2011-06-17 location: Vasteras, Sweden name: ' SIES: International Symposium on Industrial Embedded Systems' start_date: 2011-06-15 date_created: 2018-12-11T12:02:38Z date_published: 2011-07-14T00:00:00Z date_updated: 2021-01-12T07:42:36Z day: '14' department: - _id: KrCh - _id: ToHe doi: 10.1109/SIES.2011.5953660 ec_funded: 1 language: - iso: eng main_file_link: - open_access: '1' url: https://openlib.tugraz.at/download.php?id=5cb57c8a49344&location=browse month: '07' oa: 1 oa_version: Published Version page: 176 - 185 project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25F2ACDE-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Rigorous Systems Engineering - _id: 25F1337C-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '214373' name: Design for Embedded Systems - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: 6th IEEE International Symposium on Industrial and Embedded Systems publication_status: published publisher: IEEE publist_id: '3323' quality_controlled: '1' scopus_import: 1 status: public title: Specification-centered robustness type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2011' ... --- _id: '3350' abstract: - lang: eng text: A controller for a discrete game with ω-regular objectives requires attention if, intuitively, it requires measuring the state and switching from the current control action. Minimum attention controllers are preferable in modern shared implementations of cyber-physical systems because they produce the least burden on system resources such as processor time or communication bandwidth. We give algorithms to compute minimum attention controllers for ω-regular objectives in imperfect information discrete two-player games. We show a polynomial-time reduction from minimum attention controller synthesis to synthesis of controllers for mean-payoff parity objectives in games of incomplete information. This gives an optimal EXPTIME-complete synthesis algorithm. We show that the minimum attention controller problem is decidable for infinite state systems with finite bisimulation quotients. In particular, the problem is decidable for timed and rectangular automata. alternative_title: - LNCS author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Ritankar full_name: Majumdar, Ritankar last_name: Majumdar citation: ama: 'Chatterjee K, Majumdar R. Minimum attention controller synthesis for omega regular objectives. In: Fahrenberg U, Tripakis S, eds. Vol 6919. Springer; 2011:145-159. doi:10.1007/978-3-642-24310-3_11' apa: 'Chatterjee, K., & Majumdar, R. (2011). Minimum attention controller synthesis for omega regular objectives. In U. Fahrenberg & S. Tripakis (Eds.) (Vol. 6919, pp. 145–159). Presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Aalborg, Denmark: Springer. https://doi.org/10.1007/978-3-642-24310-3_11' chicago: Chatterjee, Krishnendu, and Ritankar Majumdar. “Minimum Attention Controller Synthesis for Omega Regular Objectives.” edited by Uli Fahrenberg and Stavros Tripakis, 6919:145–59. Springer, 2011. https://doi.org/10.1007/978-3-642-24310-3_11. ieee: 'K. Chatterjee and R. Majumdar, “Minimum attention controller synthesis for omega regular objectives,” presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Aalborg, Denmark, 2011, vol. 6919, pp. 145–159.' ista: 'Chatterjee K, Majumdar R. 2011. Minimum attention controller synthesis for omega regular objectives. FORMATS: Formal Modeling and Analysis of Timed Systems, LNCS, vol. 6919, 145–159.' mla: Chatterjee, Krishnendu, and Ritankar Majumdar. Minimum Attention Controller Synthesis for Omega Regular Objectives. Edited by Uli Fahrenberg and Stavros Tripakis, vol. 6919, Springer, 2011, pp. 145–59, doi:10.1007/978-3-642-24310-3_11. short: K. Chatterjee, R. Majumdar, in:, U. Fahrenberg, S. Tripakis (Eds.), Springer, 2011, pp. 145–159. conference: end_date: 2011-09-23 location: Aalborg, Denmark name: 'FORMATS: Formal Modeling and Analysis of Timed Systems' start_date: 2011-09-21 date_created: 2018-12-11T12:02:49Z date_published: 2011-01-01T00:00:00Z date_updated: 2021-01-12T07:42:51Z day: '01' department: - _id: KrCh doi: 10.1007/978-3-642-24310-3_11 editor: - first_name: Uli full_name: Fahrenberg, Uli last_name: Fahrenberg - first_name: Stavros full_name: Tripakis, Stavros last_name: Tripakis intvolume: ' 6919' language: - iso: eng month: '01' oa_version: None page: 145 - 159 project: - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication_status: published publisher: Springer publist_id: '3271' quality_controlled: '1' scopus_import: 1 status: public title: Minimum attention controller synthesis for omega regular objectives type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 6919 year: '2011' ... --- _id: '3351' abstract: - lang: eng text: In two-player games on graph, the players construct an infinite path through the game graph and get a reward computed by a payoff function over infinite paths. Over weighted graphs, the typical and most studied payoff functions compute the limit-average or the discounted sum of the rewards along the path. Besides their simple definition, these two payoff functions enjoy the property that memoryless optimal strategies always exist. In an attempt to construct other simple payoff functions, we define a class of payoff functions which compute an (infinite) weighted average of the rewards. This new class contains both the limit-average and the discounted sum functions, and we show that they are the only members of this class which induce memoryless optimal strategies, showing that there is essentially no other simple payoff functions. alternative_title: - LNCS author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Laurent full_name: Doyen, Laurent last_name: Doyen - first_name: Rohit full_name: Singh, Rohit last_name: Singh citation: ama: 'Chatterjee K, Doyen L, Singh R. On memoryless quantitative objectives. In: Owe O, Steffen M, Telle JA, eds. Vol 6914. Springer; 2011:148-159. doi:10.1007/978-3-642-22953-4_13' apa: 'Chatterjee, K., Doyen, L., & Singh, R. (2011). On memoryless quantitative objectives. In O. Owe, M. Steffen, & J. A. Telle (Eds.) (Vol. 6914, pp. 148–159). Presented at the FCT: Fundamentals of Computation Theory, Oslo, Norway: Springer. https://doi.org/10.1007/978-3-642-22953-4_13' chicago: Chatterjee, Krishnendu, Laurent Doyen, and Rohit Singh. “On Memoryless Quantitative Objectives.” edited by Olaf Owe, Martin Steffen, and Jan Arne Telle, 6914:148–59. Springer, 2011. https://doi.org/10.1007/978-3-642-22953-4_13. ieee: 'K. Chatterjee, L. Doyen, and R. Singh, “On memoryless quantitative objectives,” presented at the FCT: Fundamentals of Computation Theory, Oslo, Norway, 2011, vol. 6914, pp. 148–159.' ista: 'Chatterjee K, Doyen L, Singh R. 2011. On memoryless quantitative objectives. FCT: Fundamentals of Computation Theory, LNCS, vol. 6914, 148–159.' mla: Chatterjee, Krishnendu, et al. On Memoryless Quantitative Objectives. Edited by Olaf Owe et al., vol. 6914, Springer, 2011, pp. 148–59, doi:10.1007/978-3-642-22953-4_13. short: K. Chatterjee, L. Doyen, R. Singh, in:, O. Owe, M. Steffen, J.A. Telle (Eds.), Springer, 2011, pp. 148–159. conference: end_date: 2011-08-25 location: Oslo, Norway name: 'FCT: Fundamentals of Computation Theory' start_date: 2011-08-22 date_created: 2018-12-11T12:02:50Z date_published: 2011-04-16T00:00:00Z date_updated: 2021-01-12T07:42:52Z day: '16' department: - _id: KrCh doi: 10.1007/978-3-642-22953-4_13 editor: - first_name: Olaf full_name: Owe, Olaf last_name: Owe - first_name: Martin full_name: Steffen, Martin last_name: Steffen - first_name: Jan Arne full_name: Telle, Jan Arne last_name: Telle intvolume: ' 6914' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1104.3211 month: '04' oa: 1 oa_version: Submitted Version page: 148 - 159 project: - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication_status: published publisher: Springer publist_id: '3270' quality_controlled: '1' scopus_import: 1 status: public title: On memoryless quantitative objectives type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 6914 year: '2011' ... --- _id: '3354' abstract: - lang: eng text: 'We consider two-player games played on a finite state space for an infinite number of rounds. The games are concurrent: in each round, the two players (player 1 and player 2) choose their moves independently and simultaneously; the current state and the two moves determine the successor state. We consider ω-regular winning conditions specified as parity objectives. Both players are allowed to use randomization when choosing their moves. We study the computation of the limit-winning set of states, consisting of the states where the sup-inf value of the game for player 1 is 1: in other words, a state is limit-winning if player 1 can ensure a probability of winning arbitrarily close to 1. We show that the limit-winning set can be computed in O(n2d+2) time, where n is the size of the game structure and 2d is the number of priorities (or colors). The membership problem of whether a state belongs to the limit-winning set can be decided in NP ∩ coNP. While this complexity is the same as for the simpler class of turn-based parity games, where in each state only one of the two players has a choice of moves, our algorithms are considerably more involved than those for turn-based games. This is because concurrent games do not satisfy two of the most fundamental properties of turn-based parity games. First, in concurrent games limit-winning strategies require randomization; and second, they require infinite memory.' article_number: '28' author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Luca full_name: De Alfaro, Luca last_name: De Alfaro - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 citation: ama: Chatterjee K, De Alfaro L, Henzinger TA. Qualitative concurrent parity games. ACM Transactions on Computational Logic (TOCL). 2011;12(4). doi:10.1145/1970398.1970404 apa: Chatterjee, K., De Alfaro, L., & Henzinger, T. A. (2011). Qualitative concurrent parity games. ACM Transactions on Computational Logic (TOCL). ACM. https://doi.org/10.1145/1970398.1970404 chicago: Chatterjee, Krishnendu, Luca De Alfaro, and Thomas A Henzinger. “Qualitative Concurrent Parity Games.” ACM Transactions on Computational Logic (TOCL). ACM, 2011. https://doi.org/10.1145/1970398.1970404. ieee: K. Chatterjee, L. De Alfaro, and T. A. Henzinger, “Qualitative concurrent parity games,” ACM Transactions on Computational Logic (TOCL), vol. 12, no. 4. ACM, 2011. ista: Chatterjee K, De Alfaro L, Henzinger TA. 2011. Qualitative concurrent parity games. ACM Transactions on Computational Logic (TOCL). 12(4), 28. mla: Chatterjee, Krishnendu, et al. “Qualitative Concurrent Parity Games.” ACM Transactions on Computational Logic (TOCL), vol. 12, no. 4, 28, ACM, 2011, doi:10.1145/1970398.1970404. short: K. Chatterjee, L. De Alfaro, T.A. Henzinger, ACM Transactions on Computational Logic (TOCL) 12 (2011). date_created: 2018-12-11T12:02:51Z date_published: 2011-07-04T00:00:00Z date_updated: 2023-02-23T10:26:18Z day: '04' department: - _id: KrCh - _id: ToHe doi: 10.1145/1970398.1970404 intvolume: ' 12' issue: '4' language: - iso: eng month: '07' oa_version: None project: - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: ACM Transactions on Computational Logic (TOCL) publication_status: published publisher: ACM publist_id: '3262' quality_controlled: '1' related_material: record: - id: '2054' relation: later_version status: public scopus_import: 1 status: public title: Qualitative concurrent parity games type: journal_article user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 12 year: '2011' ... --- _id: '3349' abstract: - lang: eng text: 'Games on graphs provide a natural model for reactive non-terminating systems. In such games, the interaction of two players on an arena results in an infinite path that describes a run of the system. Different settings are used to model various open systems in computer science, as for instance turn-based or concurrent moves, and deterministic or stochastic transitions. In this paper, we are interested in turn-based games, and specifically in deterministic parity games and stochastic reachability games (also known as simple stochastic games). We present a simple, direct and efficient reduction from deterministic parity games to simple stochastic games: it yields an arena whose size is linear up to a logarithmic factor in size of the original arena.' alternative_title: - EPTCS author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Nathanaël full_name: Fijalkow, Nathanaël last_name: Fijalkow citation: ama: 'Chatterjee K, Fijalkow N. A reduction from parity games to simple stochastic games. In: Vol 54. EPTCS; 2011:74-86. doi:10.4204/EPTCS.54.6' apa: 'Chatterjee, K., & Fijalkow, N. (2011). A reduction from parity games to simple stochastic games (Vol. 54, pp. 74–86). Presented at the GandALF: Games, Automata, Logic, and Formal Verification, Minori, Italy: EPTCS. https://doi.org/10.4204/EPTCS.54.6' chicago: Chatterjee, Krishnendu, and Nathanaël Fijalkow. “A Reduction from Parity Games to Simple Stochastic Games,” 54:74–86. EPTCS, 2011. https://doi.org/10.4204/EPTCS.54.6. ieee: 'K. Chatterjee and N. Fijalkow, “A reduction from parity games to simple stochastic games,” presented at the GandALF: Games, Automata, Logic, and Formal Verification, Minori, Italy, 2011, vol. 54, pp. 74–86.' ista: 'Chatterjee K, Fijalkow N. 2011. A reduction from parity games to simple stochastic games. GandALF: Games, Automata, Logic, and Formal Verification, EPTCS, vol. 54, 74–86.' mla: Chatterjee, Krishnendu, and Nathanaël Fijalkow. A Reduction from Parity Games to Simple Stochastic Games. Vol. 54, EPTCS, 2011, pp. 74–86, doi:10.4204/EPTCS.54.6. short: K. Chatterjee, N. Fijalkow, in:, EPTCS, 2011, pp. 74–86. conference: end_date: 2011-06-17 location: Minori, Italy name: 'GandALF: Games, Automata, Logic, and Formal Verification' start_date: 2011-06-15 date_created: 2018-12-11T12:02:49Z date_published: 2011-06-04T00:00:00Z date_updated: 2021-01-12T07:42:51Z day: '04' department: - _id: KrCh doi: 10.4204/EPTCS.54.6 intvolume: ' 54' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1106.1232 month: '06' oa: 1 oa_version: Submitted Version page: 74 - 86 project: - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering publication_status: published publisher: EPTCS publist_id: '3272' scopus_import: 1 status: public title: A reduction from parity games to simple stochastic games type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 54 year: '2011' ... --- _id: '3365' abstract: - lang: eng text: We present the tool Quasy, a quantitative synthesis tool. Quasy takes qualitative and quantitative specifications and automatically constructs a system that satisfies the qualitative specification and optimizes the quantitative specification, if such a system exists. The user can choose between a system that satisfies and optimizes the specifications (a) under all possible environment behaviors or (b) under the most-likely environment behaviors given as a probability distribution on the possible input sequences. Quasy solves these two quantitative synthesis problems by reduction to instances of 2-player games and Markov Decision Processes (MDPs) with quantitative winning objectives. Quasy can also be seen as a game solver for quantitative games. Most notable, it can solve lexicographic mean-payoff games with 2 players, MDPs with mean-payoff objectives, and ergodic MDPs with mean-payoff parity objectives. alternative_title: - LNCS author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Barbara full_name: Jobstmann, Barbara last_name: Jobstmann - first_name: Rohit full_name: Singh, Rohit last_name: Singh citation: ama: 'Chatterjee K, Henzinger TA, Jobstmann B, Singh R. QUASY: quantitative synthesis tool. In: Vol 6605. Springer; 2011:267-271. doi:10.1007/978-3-642-19835-9_24' apa: 'Chatterjee, K., Henzinger, T. A., Jobstmann, B., & Singh, R. (2011). QUASY: quantitative synthesis tool (Vol. 6605, pp. 267–271). Presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Saarbrucken, Germany: Springer. https://doi.org/10.1007/978-3-642-19835-9_24' chicago: 'Chatterjee, Krishnendu, Thomas A Henzinger, Barbara Jobstmann, and Rohit Singh. “QUASY: Quantitative Synthesis Tool,” 6605:267–71. Springer, 2011. https://doi.org/10.1007/978-3-642-19835-9_24.' ieee: 'K. Chatterjee, T. A. Henzinger, B. Jobstmann, and R. Singh, “QUASY: quantitative synthesis tool,” presented at the TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Saarbrucken, Germany, 2011, vol. 6605, pp. 267–271.' ista: 'Chatterjee K, Henzinger TA, Jobstmann B, Singh R. 2011. QUASY: quantitative synthesis tool. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 6605, 267–271.' mla: 'Chatterjee, Krishnendu, et al. QUASY: Quantitative Synthesis Tool. Vol. 6605, Springer, 2011, pp. 267–71, doi:10.1007/978-3-642-19835-9_24.' short: K. Chatterjee, T.A. Henzinger, B. Jobstmann, R. Singh, in:, Springer, 2011, pp. 267–271. conference: end_date: 2011-04-03 location: Saarbrucken, Germany name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems' start_date: 2011-03-26 date_created: 2018-12-11T12:02:55Z date_published: 2011-09-29T00:00:00Z date_updated: 2021-01-12T07:42:58Z day: '29' ddc: - '000' - '005' department: - _id: KrCh - _id: ToHe doi: 10.1007/978-3-642-19835-9_24 file: - access_level: open_access checksum: 762e52eb296f6dbfbf2a75d98b8ebaee content_type: application/pdf creator: system date_created: 2018-12-12T10:13:37Z date_updated: 2020-07-14T12:46:10Z file_id: '5022' file_name: IST-2012-77-v1+1_QUASY-_quantitative_synthesis_tool.pdf file_size: 475661 relation: main_file file_date_updated: 2020-07-14T12:46:10Z has_accepted_license: '1' intvolume: ' 6605' language: - iso: eng month: '09' oa: 1 oa_version: Submitted Version page: 267 - 271 publication_status: published publisher: Springer publist_id: '3248' pubrep_id: '77' quality_controlled: '1' scopus_import: 1 status: public title: 'QUASY: quantitative synthesis tool' type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 6605 year: '2011' ... --- _id: '3363' abstract: - lang: eng text: We consider probabilistic automata on infinite words with acceptance defined by safety, reachability, Büchi, coBüchi, and limit-average conditions. We consider quantitative and qualitative decision problems. We present extensions and adaptations of proofs for probabilistic finite automata and present a complete characterization of the decidability and undecidability frontier of the quantitative and qualitative decision problems for probabilistic automata on infinite words. 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: Mathieu full_name: Tracol, Mathieu id: 3F54FA38-F248-11E8-B48F-1D18A9856A87 last_name: Tracol citation: ama: Chatterjee K, Henzinger TA, Tracol M. The decidability frontier for probabilistic automata on infinite words. apa: Chatterjee, K., Henzinger, T. A., & Tracol, M. (n.d.). The decidability frontier for probabilistic automata on infinite words. ArXiv. chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Mathieu Tracol. “The Decidability Frontier for Probabilistic Automata on Infinite Words.” ArXiv, n.d. ieee: K. Chatterjee, T. A. Henzinger, and M. Tracol, “The decidability frontier for probabilistic automata on infinite words.” ArXiv. ista: Chatterjee K, Henzinger TA, Tracol M. The decidability frontier for probabilistic automata on infinite words. mla: Chatterjee, Krishnendu, et al. The Decidability Frontier for Probabilistic Automata on Infinite Words. ArXiv. short: K. Chatterjee, T.A. Henzinger, M. Tracol, (n.d.). date_created: 2018-12-11T12:02:54Z date_published: 2011-04-01T00:00:00Z date_updated: 2020-01-21T13:20:24Z day: '01' department: - _id: KrCh - _id: ToHe ec_funded: 1 external_id: arxiv: - '1104.0127' language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/1104.0127 month: '04' oa: 1 oa_version: Preprint page: '19' project: - _id: 25EFB36C-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '215543' name: COMponent-Based Embedded Systems design Techniques - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship - _id: 25F1337C-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '214373' name: Design for Embedded Systems publication_status: submitted publisher: ArXiv publist_id: '3251' status: public title: The decidability frontier for probabilistic automata on infinite words type: preprint user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2011' ... --- _id: '3315' abstract: - lang: eng text: We consider two-player games played in real time on game structures with clocks where the objectives of players are described using parity conditions. The games are concurrent in that at each turn, both players independently propose a time delay and an action, and the action with the shorter delay is chosen. To prevent a player from winning by blocking time, we restrict each player to play strategies that ensure that the player cannot be responsible for causing a zeno run. First, we present an efficient reduction of these games to turn-based (i.e., not concurrent) finite-state (i.e., untimed) parity games. Our reduction improves the best known complexity for solving timed parity games. Moreover, the rich class of algorithms for classical parity games can now be applied to timed parity games. The states of the resulting game are based on clock regions of the original game, and the state space of the finite game is linear in the size of the region graph. Second, we consider two restricted classes of strategies for the player that represents the controller in a real-time synthesis problem, namely, limit-robust and bounded-robust winning strategies. Using a limit-robust winning strategy, the controller cannot choose an exact real-valued time delay but must allow for some nonzero jitter in each of its actions. If there is a given lower bound on the jitter, then the strategy is bounded-robust winning. We show that exact strategies are more powerful than limit-robust strategies, which are more powerful than bounded-robust winning strategies for any bound. For both kinds of robust strategies, we present efficient reductions to standard timed automaton games. These reductions provide algorithms for the synthesis of robust real-time controllers. 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: Vinayak full_name: Prabhu, Vinayak last_name: Prabhu citation: ama: 'Chatterjee K, Henzinger TA, Prabhu V. Timed parity games: Complexity and robustness. Logical Methods in Computer Science. 2011;7(4). doi:10.2168/LMCS-7(4:8)2011' apa: 'Chatterjee, K., Henzinger, T. A., & Prabhu, V. (2011). Timed parity games: Complexity and robustness. Logical Methods in Computer Science. International Federation of Computational Logic. https://doi.org/10.2168/LMCS-7(4:8)2011' chicago: 'Chatterjee, Krishnendu, Thomas A Henzinger, and Vinayak Prabhu. “Timed Parity Games: Complexity and Robustness.” Logical Methods in Computer Science. International Federation of Computational Logic, 2011. https://doi.org/10.2168/LMCS-7(4:8)2011.' ieee: 'K. Chatterjee, T. A. Henzinger, and V. Prabhu, “Timed parity games: Complexity and robustness,” Logical Methods in Computer Science, vol. 7, no. 4. International Federation of Computational Logic, 2011.' ista: 'Chatterjee K, Henzinger TA, Prabhu V. 2011. Timed parity games: Complexity and robustness. Logical Methods in Computer Science. 7(4).' mla: 'Chatterjee, Krishnendu, et al. “Timed Parity Games: Complexity and Robustness.” Logical Methods in Computer Science, vol. 7, no. 4, International Federation of Computational Logic, 2011, doi:10.2168/LMCS-7(4:8)2011.' short: K. Chatterjee, T.A. Henzinger, V. Prabhu, Logical Methods in Computer Science 7 (2011). date_created: 2018-12-11T12:02:37Z date_published: 2011-12-14T00:00:00Z date_updated: 2023-02-23T11:46:35Z day: '14' ddc: - '000' - '005' department: - _id: KrCh - _id: ToHe doi: 10.2168/LMCS-7(4:8)2011 ec_funded: 1 file: - access_level: open_access checksum: 3480e1594bbef25ff7462fa93a8a814e content_type: application/pdf creator: system date_created: 2018-12-12T10:16:42Z date_updated: 2020-07-14T12:46:07Z file_id: '5231' file_name: IST-2016-86-v2+1_1011.0688_3_.pdf file_size: 588863 relation: main_file file_date_updated: 2020-07-14T12:46:07Z has_accepted_license: '1' intvolume: ' 7' issue: '4' language: - iso: eng license: https://creativecommons.org/licenses/by-nd/4.0/ month: '12' oa: 1 oa_version: Published Version project: - _id: 25EFB36C-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '215543' name: COMponent-Based Embedded Systems design Techniques publication: Logical Methods in Computer Science publication_status: published publisher: International Federation of Computational Logic publist_id: '3324' pubrep_id: '506' quality_controlled: '1' related_material: record: - id: '3876' relation: earlier_version status: public scopus_import: 1 status: public title: 'Timed parity games: Complexity and robustness' tmp: image: /image/cc_by_nd.png legal_code_url: https://creativecommons.org/licenses/by-nd/4.0/legalcode name: Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0) short: CC BY-ND (4.0) type: journal_article user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 7 year: '2011' ... --- _id: '3339' abstract: - lang: eng text: 'Turn-based stochastic games and its important subclass Markov decision processes (MDPs) provide models for systems with both probabilistic and nondeterministic behaviors. We consider turn-based stochastic games with two classical quantitative objectives: discounted-sum and long-run average objectives. The game models and the quantitative objectives are widely used in probabilistic verification, planning, optimal inventory control, network protocol and performance analysis. Games and MDPs that model realistic systems often have very large state spaces, and probabilistic abstraction techniques are necessary to handle the state-space explosion. The commonly used full-abstraction techniques do not yield space-savings for systems that have many states with similar value, but does not necessarily have similar transition structure. A semi-abstraction technique, namely Magnifying-lens abstractions (MLA), that clusters states based on value only, disregarding differences in their transition relation was proposed for qualitative objectives (reachability and safety objectives). In this paper we extend the MLA technique to solve stochastic games with discounted-sum and long-run average objectives. We present the MLA technique based abstraction-refinement algorithm for stochastic games and MDPs with discounted-sum objectives. For long-run average objectives, our solution works for all MDPs and a sub-class of stochastic games where every state has the same value. ' author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Luca full_name: De Alfaro, Luca last_name: De Alfaro - first_name: Roy full_name: Pritam, Roy last_name: Pritam citation: ama: Chatterjee K, De Alfaro L, Pritam R. Magnifying lens abstraction for stochastic games with discounted and long-run average objectives. arXiv. 2011. apa: Chatterjee, K., De Alfaro, L., & Pritam, R. (2011). Magnifying lens abstraction for stochastic games with discounted and long-run average objectives. arXiv. ArXiv. chicago: Chatterjee, Krishnendu, Luca De Alfaro, and Roy Pritam. “Magnifying Lens Abstraction for Stochastic Games with Discounted and Long-Run Average Objectives.” ArXiv. ArXiv, 2011. ieee: K. Chatterjee, L. De Alfaro, and R. Pritam, “Magnifying lens abstraction for stochastic games with discounted and long-run average objectives,” arXiv. ArXiv, 2011. ista: Chatterjee K, De Alfaro L, Pritam R. 2011. Magnifying lens abstraction for stochastic games with discounted and long-run average objectives. arXiv, . mla: Chatterjee, Krishnendu, et al. “Magnifying Lens Abstraction for Stochastic Games with Discounted and Long-Run Average Objectives.” ArXiv, ArXiv, 2011. short: K. Chatterjee, L. De Alfaro, R. Pritam, ArXiv (2011). date_created: 2018-12-11T12:02:46Z date_published: 2011-07-11T00:00:00Z date_updated: 2021-01-12T07:42:46Z day: '11' department: - _id: KrCh external_id: arxiv: - '1107.2132' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1107.2132 month: '07' oa: 1 oa_version: Preprint page: '17' publication: arXiv publication_status: published publisher: ArXiv publist_id: '3286' status: public title: Magnifying lens abstraction for stochastic games with discounted and long-run average objectives type: preprint user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2011' ... --- _id: '3342' abstract: - lang: eng text: 'We consider Markov decision processes (MDPs) with ω-regular specifications given as parity objectives. We consider the problem of computing the set of almost-sure winning states from where the objective can be ensured with probability 1. The algorithms for the computation of the almost-sure winning set for parity objectives iteratively use the solutions for the almost-sure winning set for Büchi objectives (a special case of parity objectives). Our contributions are as follows: First, we present the first subquadratic symbolic algorithm to compute the almost-sure winning set for MDPs with Büchi objectives; our algorithm takes O(nm) symbolic steps as compared to the previous known algorithm that takes O(n 2) symbolic steps, where n is the number of states and m is the number of edges of the MDP. In practice MDPs often have constant out-degree, and then our symbolic algorithm takes O(nn) symbolic steps, as compared to the previous known O(n 2) symbolic steps algorithm. Second, we present a new algorithm, namely win-lose algorithm, with the following two properties: (a) the algorithm iteratively computes subsets of the almost-sure winning set and its complement, as compared to all previous algorithms that discover the almost-sure winning set upon termination; and (b) requires O(nK) symbolic steps, where K is the maximal number of edges of strongly connected components (scc’s) of the MDP. The win-lose algorithm requires symbolic computation of scc’s. Third, we improve the algorithm for symbolic scc computation; the previous known algorithm takes linear symbolic steps, and our new algorithm improves the constants associated with the linear number of steps. In the worst case the previous known algorithm takes 5·n symbolic steps, whereas our new algorithm takes 4 ·n symbolic steps.' alternative_title: - LNCS article_processing_charge: No author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Monika H full_name: Henzinger, Monika H id: 540c9bbd-f2de-11ec-812d-d04a5be85630 last_name: Henzinger orcid: 0000-0002-5008-6530 - first_name: Manas full_name: Joglekar, Manas last_name: Joglekar - first_name: Shah full_name: Nisarg, Shah last_name: Nisarg citation: ama: 'Chatterjee K, Henzinger MH, Joglekar M, Nisarg S. Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives. In: Gopalakrishnan G, Qadeer S, eds. Vol 6806. Springer; 2011:260-276. doi:10.1007/978-3-642-22110-1_21' apa: 'Chatterjee, K., Henzinger, M. H., Joglekar, M., & Nisarg, S. (2011). Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives. In G. Gopalakrishnan & S. Qadeer (Eds.) (Vol. 6806, pp. 260–276). Presented at the CAV: Computer Aided Verification, Snowbird, USA: Springer. https://doi.org/10.1007/978-3-642-22110-1_21' chicago: Chatterjee, Krishnendu, Monika H Henzinger, Manas Joglekar, and Shah Nisarg. “Symbolic Algorithms for Qualitative Analysis of Markov Decision Processes with Büchi Objectives.” edited by Ganesh Gopalakrishnan and Shaz Qadeer, 6806:260–76. Springer, 2011. https://doi.org/10.1007/978-3-642-22110-1_21. ieee: 'K. Chatterjee, M. H. Henzinger, M. Joglekar, and S. Nisarg, “Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives,” presented at the CAV: Computer Aided Verification, Snowbird, USA, 2011, vol. 6806, pp. 260–276.' ista: 'Chatterjee K, Henzinger MH, Joglekar M, Nisarg S. 2011. Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives. CAV: Computer Aided Verification, LNCS, vol. 6806, 260–276.' mla: Chatterjee, Krishnendu, et al. Symbolic Algorithms for Qualitative Analysis of Markov Decision Processes with Büchi Objectives. Edited by Ganesh Gopalakrishnan and Shaz Qadeer, vol. 6806, Springer, 2011, pp. 260–76, doi:10.1007/978-3-642-22110-1_21. short: K. Chatterjee, M.H. Henzinger, M. Joglekar, S. Nisarg, in:, G. Gopalakrishnan, S. Qadeer (Eds.), Springer, 2011, pp. 260–276. conference: end_date: 2011-07-20 location: Snowbird, USA name: 'CAV: Computer Aided Verification' start_date: 2011-07-14 date_created: 2018-12-11T12:02:47Z date_published: 2011-08-11T00:00:00Z date_updated: 2023-02-23T11:00:13Z day: '11' department: - _id: KrCh doi: 10.1007/978-3-642-22110-1_21 editor: - first_name: Ganesh full_name: Gopalakrishnan, Ganesh last_name: Gopalakrishnan - first_name: Shaz full_name: Qadeer, Shaz last_name: Qadeer external_id: arxiv: - '1104.3348' intvolume: ' 6806' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1104.3348 month: '08' oa: 1 oa_version: Preprint page: 260 - 276 project: - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering publication_status: published publisher: Springer publist_id: '3282' quality_controlled: '1' related_material: record: - id: '2831' relation: later_version status: public status: public title: Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives type: conference user_id: 72615eeb-f1f3-11ec-aa25-d4573ddc34fd volume: 6806 year: '2011' ... --- _id: '3347' abstract: - lang: eng text: 'The class of omega-regular languages provides a robust specification language in verification. Every omega-regular condition can be decomposed into a safety part and a liveness part. The liveness part ensures that something good happens "eventually". Finitary liveness was proposed by Alur and Henzinger as a stronger formulation of liveness. It requires that there exists an unknown, fixed bound b such that something good happens within b transitions. In this work we consider automata with finitary acceptance conditions defined by finitary Buchi, parity and Streett languages. We study languages expressible by such automata: we give their topological complexity and present a regular-expression characterization. We compare the expressive power of finitary automata and give optimal algorithms for classical decisions questions. We show that the finitary languages are Sigma 2-complete; we present a complete picture of the expressive power of various classes of automata with finitary and infinitary acceptance conditions; we show that the languages defined by finitary parity automata exactly characterize the star-free fragment of omega B-regular languages; and we show that emptiness is NLOGSPACE-complete and universality as well as language inclusion are PSPACE-complete for finitary parity and Streett automata.' alternative_title: - LNCS author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Nathanaël full_name: Fijalkow, Nathanaël id: A1B5DD72-E997-11E9-8398-E808B6C6ADC0 last_name: Fijalkow citation: ama: 'Chatterjee K, Fijalkow N. Finitary languages. In: Vol 6638. Springer; 2011:216-226. doi:10.1007/978-3-642-21254-3_16' apa: 'Chatterjee, K., & Fijalkow, N. (2011). Finitary languages (Vol. 6638, pp. 216–226). Presented at the LATA: Language and Automata Theory and Applications, Tarragona, Spain: Springer. https://doi.org/10.1007/978-3-642-21254-3_16' chicago: Chatterjee, Krishnendu, and Nathanaël Fijalkow. “Finitary Languages,” 6638:216–26. Springer, 2011. https://doi.org/10.1007/978-3-642-21254-3_16. ieee: 'K. Chatterjee and N. Fijalkow, “Finitary languages,” presented at the LATA: Language and Automata Theory and Applications, Tarragona, Spain, 2011, vol. 6638, pp. 216–226.' ista: 'Chatterjee K, Fijalkow N. 2011. Finitary languages. LATA: Language and Automata Theory and Applications, LNCS, vol. 6638, 216–226.' mla: Chatterjee, Krishnendu, and Nathanaël Fijalkow. Finitary Languages. Vol. 6638, Springer, 2011, pp. 216–26, doi:10.1007/978-3-642-21254-3_16. short: K. Chatterjee, N. Fijalkow, in:, Springer, 2011, pp. 216–226. conference: end_date: 2011-05-31 location: Tarragona, Spain name: 'LATA: Language and Automata Theory and Applications' start_date: 2011-05-26 date_created: 2018-12-11T12:02:48Z date_published: 2011-06-16T00:00:00Z date_updated: 2021-01-12T07:42:50Z day: '16' department: - _id: KrCh doi: 10.1007/978-3-642-21254-3_16 external_id: arxiv: - '1101.1727' intvolume: ' 6638' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1101.1727 month: '06' oa: 1 oa_version: Preprint page: 216 - 226 project: - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering publication_status: published publisher: Springer publist_id: '3274' quality_controlled: '1' scopus_import: 1 status: public title: Finitary languages type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 6638 year: '2011' ... --- _id: '3346' abstract: - lang: eng text: We study Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) functions. We consider two different objectives, namely, expectation and satisfaction objectives. Given an MDP with k reward functions, in the expectation objective the goal is to maximize the expected limit-average value, and in the satisfaction objective the goal is to maximize the probability of runs such that the limit-average value stays above a given vector. We show that under the expectation objective, in contrast to the single-objective case, both randomization and memory are necessary for strategies, and that finite-memory randomized strategies are sufficient. Under the satisfaction objective, in contrast to the single-objective case, infinite memory is necessary for strategies, and that randomized memoryless strategies are sufficient for epsilon-approximation, for all epsilon>;0. We further prove that the decision problems for both expectation and satisfaction objectives can be solved in polynomial time and the trade-off curve (Pareto curve) can be epsilon-approximated in time polynomial in the size of the MDP and 1/epsilon, and exponential in the number of reward functions, for all epsilon>;0. Our results also reveal flaws in previous work for MDPs with multiple mean-payoff functions under the expectation objective, correct the flaws and obtain improved results. article_number: '5970225' author: - first_name: Tomáš full_name: Brázdil, Tomáš last_name: Brázdil - first_name: Václav full_name: Brožek, Václav last_name: Brožek - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Vojtěch full_name: Forejt, Vojtěch last_name: Forejt - first_name: Antonín full_name: Kučera, Antonín last_name: Kučera citation: ama: 'Brázdil T, Brožek V, Chatterjee K, Forejt V, Kučera A. Two views on multiple mean payoff objectives in Markov Decision Processes. In: IEEE; 2011. doi:10.1109/LICS.2011.10' apa: 'Brázdil, T., Brožek, V., Chatterjee, K., Forejt, V., & Kučera, A. (2011). Two views on multiple mean payoff objectives in Markov Decision Processes. Presented at the LICS: Logic in Computer Science, Toronto, Canada: IEEE. https://doi.org/10.1109/LICS.2011.10' chicago: Brázdil, Tomáš, Václav Brožek, Krishnendu Chatterjee, Vojtěch Forejt, and Antonín Kučera. “Two Views on Multiple Mean Payoff Objectives in Markov Decision Processes.” IEEE, 2011. https://doi.org/10.1109/LICS.2011.10. ieee: 'T. Brázdil, V. Brožek, K. Chatterjee, V. Forejt, and A. Kučera, “Two views on multiple mean payoff objectives in Markov Decision Processes,” presented at the LICS: Logic in Computer Science, Toronto, Canada, 2011.' ista: 'Brázdil T, Brožek V, Chatterjee K, Forejt V, Kučera A. 2011. Two views on multiple mean payoff objectives in Markov Decision Processes. LICS: Logic in Computer Science, 5970225.' mla: Brázdil, Tomáš, et al. Two Views on Multiple Mean Payoff Objectives in Markov Decision Processes. 5970225, IEEE, 2011, doi:10.1109/LICS.2011.10. short: T. Brázdil, V. Brožek, K. Chatterjee, V. Forejt, A. Kučera, in:, IEEE, 2011. conference: end_date: 2011-06-24 location: Toronto, Canada name: 'LICS: Logic in Computer Science' start_date: 2011-06-21 date_created: 2018-12-11T12:02:48Z date_published: 2011-06-21T00:00:00Z date_updated: 2021-01-12T07:42:49Z day: '21' department: - _id: KrCh doi: 10.1109/LICS.2011.10 ec_funded: 1 language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1104.3489 month: '06' oa: 1 oa_version: Submitted Version project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication_status: published publisher: IEEE publist_id: '3275' quality_controlled: '1' scopus_import: 1 status: public title: Two views on multiple mean payoff objectives in Markov Decision Processes type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 year: '2011' ... --- _id: '3348' abstract: - lang: eng text: We study synthesis of controllers for real-time systems, where the objective is to stay in a given safe set. The problem is solved by obtaining winning strategies in the setting of concurrent two-player timed automaton games with safety objectives. To prevent a player from winning by blocking time, we restrict each player to strategies that ensure that the player cannot be responsible for causing a zeno run. We construct winning strategies for the controller which require access only to (1) the system clocks (thus, controllers which require their own internal infinitely precise clocks are not necessary), and (2) a linear (in the number of clocks) number of memory bits. Precisely, we show that for safety objectives, a memory of size (3 · |C|+lg(|C|+1)) bits suffices for winning controller strategies, where C is the set of clocks of the timed automaton game, significantly improving the previous known exponential bound. We also settle the open question of whether winning region controller strategies require memory for safety objectives by showing with an example the necessity of memory for region strategies to win for safety objectives. author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Vinayak full_name: Prabhu, Vinayak last_name: Prabhu citation: ama: 'Chatterjee K, Prabhu V. Synthesis of memory efficient real time controllers for safety objectives. In: Springer; 2011:221-230. doi:10.1145/1967701.1967734' apa: 'Chatterjee, K., & Prabhu, V. (2011). Synthesis of memory efficient real time controllers for safety objectives (pp. 221–230). Presented at the HSCC: Hybrid Systems - Computation and Control, Chicago, USA: Springer. https://doi.org/10.1145/1967701.1967734' chicago: Chatterjee, Krishnendu, and Vinayak Prabhu. “Synthesis of Memory Efficient Real Time Controllers for Safety Objectives,” 221–30. Springer, 2011. https://doi.org/10.1145/1967701.1967734. ieee: 'K. Chatterjee and V. Prabhu, “Synthesis of memory efficient real time controllers for safety objectives,” presented at the HSCC: Hybrid Systems - Computation and Control, Chicago, USA, 2011, pp. 221–230.' ista: 'Chatterjee K, Prabhu V. 2011. Synthesis of memory efficient real time controllers for safety objectives. HSCC: Hybrid Systems - Computation and Control, 221–230.' mla: Chatterjee, Krishnendu, and Vinayak Prabhu. Synthesis of Memory Efficient Real Time Controllers for Safety Objectives. Springer, 2011, pp. 221–30, doi:10.1145/1967701.1967734. short: K. Chatterjee, V. Prabhu, in:, Springer, 2011, pp. 221–230. conference: end_date: 2011-04-14 location: Chicago, USA name: 'HSCC: Hybrid Systems - Computation and Control' start_date: 2011-04-12 date_created: 2018-12-11T12:02:49Z date_published: 2011-01-31T00:00:00Z date_updated: 2021-01-12T07:42:50Z day: '31' department: - _id: KrCh doi: 10.1145/1967701.1967734 language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1101.5842 month: '01' oa: 1 oa_version: Submitted Version page: 221 - 230 project: - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering publication_status: published publisher: Springer publist_id: '3273' quality_controlled: '1' scopus_import: 1 status: public title: Synthesis of memory efficient real time controllers for safety objectives type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 year: '2011' ... --- _id: '3344' abstract: - lang: eng text: 'Games played on graphs provide the mathematical framework to analyze several important problems in computer science as well as mathematics, such as the synthesis problem of Church, model checking of open reactive systems and many others. On the basis of mode of interaction of the players these games can be classified as follows: (a) turn-based (players make moves in turns); and (b) concurrent (players make moves simultaneously). On the basis of the information available to the players these games can be classified as follows: (a) perfect-information (players have perfect view of the game); and (b) partial-information (players have partial view of the game). In this talk we will consider all these classes of games with reachability objectives, where the goal of one player is to reach a set of target vertices of the graph, and the goal of the opponent player is to prevent the player from reaching the target. We will survey the results for various classes of games, and the results range from linear time decision algorithms to EXPTIME-complete problems to undecidable problems.' alternative_title: - LNCS author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X citation: ama: 'Chatterjee K. Graph games with reachability objectives. In: Delzanno G, Potapov I, eds. Vol 6945. Springer; 2011:1-1. doi:10.1007/978-3-642-24288-5_1' apa: 'Chatterjee, K. (2011). Graph games with reachability objectives. In G. Delzanno & I. Potapov (Eds.) (Vol. 6945, pp. 1–1). Presented at the RP: Reachability Problems, Genoa, Italy: Springer. https://doi.org/10.1007/978-3-642-24288-5_1' chicago: Chatterjee, Krishnendu. “Graph Games with Reachability Objectives.” edited by Giorgo Delzanno and Igor Potapov, 6945:1–1. Springer, 2011. https://doi.org/10.1007/978-3-642-24288-5_1. ieee: 'K. Chatterjee, “Graph games with reachability objectives,” presented at the RP: Reachability Problems, Genoa, Italy, 2011, vol. 6945, pp. 1–1.' ista: 'Chatterjee K. 2011. Graph games with reachability objectives. RP: Reachability Problems, LNCS, vol. 6945, 1–1.' mla: Chatterjee, Krishnendu. Graph Games with Reachability Objectives. Edited by Giorgo Delzanno and Igor Potapov, vol. 6945, Springer, 2011, pp. 1–1, doi:10.1007/978-3-642-24288-5_1. short: K. Chatterjee, in:, G. Delzanno, I. Potapov (Eds.), Springer, 2011, pp. 1–1. conference: end_date: 2011-09-30 location: Genoa, Italy name: 'RP: Reachability Problems' start_date: 2011-09-28 date_created: 2018-12-11T12:02:47Z date_published: 2011-10-15T00:00:00Z date_updated: 2021-01-12T07:42:48Z day: '15' department: - _id: KrCh doi: 10.1007/978-3-642-24288-5_1 editor: - first_name: Giorgo full_name: Delzanno, Giorgo last_name: Delzanno - first_name: Igor full_name: Potapov, Igor last_name: Potapov intvolume: ' 6945' language: - iso: eng month: '10' oa_version: None page: 1 - 1 publication_status: published publisher: Springer publist_id: '3277' quality_controlled: '1' status: public title: Graph games with reachability objectives type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 6945 year: '2011' ... --- _id: '3343' abstract: - lang: eng text: 'We present faster and dynamic algorithms for the following problems arising in probabilistic verification: Computation of the maximal end-component (mec) decomposition of Markov decision processes (MDPs), and of the almost sure winning set for reachability and parity objectives in MDPs. We achieve the following running time for static algorithms in MDPs with graphs of n vertices and m edges: (1) O(m · min{ √m, n2/3 }) for the mec decomposition, improving the longstanding O(m·n) bound; (2) O(m·n2/3) for reachability objectives, improving the previous O(m · √m) bound for m > n4/3; and (3) O(m · min{ √m, n2/3 } · log(d)) for parity objectives with d priorities, improving the previous O(m · √m · d) bound. We also give incremental and decremental algorithms in linear time for mec decomposition and reachability objectives and O(m · log d) time for parity ob jectives.' article_processing_charge: No author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Monika H full_name: Henzinger, Monika H id: 540c9bbd-f2de-11ec-812d-d04a5be85630 last_name: Henzinger orcid: 0000-0002-5008-6530 citation: ama: 'Chatterjee K, Henzinger MH. Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification. In: SIAM; 2011:1318-1336. doi:10.1137/1.9781611973082.101' apa: 'Chatterjee, K., & Henzinger, M. H. (2011). Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification (pp. 1318–1336). Presented at the SODA: Symposium on Discrete Algorithms, San Francisco, SA, United States: SIAM. https://doi.org/10.1137/1.9781611973082.101' chicago: Chatterjee, Krishnendu, and Monika H Henzinger. “Faster and Dynamic Algorithms for Maximal End-Component Decomposition and Related Graph Problems in Probabilistic Verification,” 1318–36. SIAM, 2011. https://doi.org/10.1137/1.9781611973082.101. ieee: 'K. Chatterjee and M. H. Henzinger, “Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification,” presented at the SODA: Symposium on Discrete Algorithms, San Francisco, SA, United States, 2011, pp. 1318–1336.' ista: 'Chatterjee K, Henzinger MH. 2011. Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification. SODA: Symposium on Discrete Algorithms, 1318–1336.' mla: Chatterjee, Krishnendu, and Monika H. Henzinger. Faster and Dynamic Algorithms for Maximal End-Component Decomposition and Related Graph Problems in Probabilistic Verification. SIAM, 2011, pp. 1318–36, doi:10.1137/1.9781611973082.101. short: K. Chatterjee, M.H. Henzinger, in:, SIAM, 2011, pp. 1318–1336. conference: end_date: 2011-01-25 location: San Francisco, SA, United States name: 'SODA: Symposium on Discrete Algorithms' start_date: 2011-01-23 date_created: 2018-12-11T12:02:47Z date_published: 2011-01-01T00:00:00Z date_updated: 2023-02-14T10:36:10Z day: '01' department: - _id: KrCh doi: 10.1137/1.9781611973082.101 language: - iso: eng main_file_link: - open_access: '1' url: https://eprints.cs.univie.ac.at/21/ month: '01' oa: 1 oa_version: Submitted Version page: 1318 - 1336 publication_status: published publisher: SIAM publist_id: '3278' quality_controlled: '1' scopus_import: '1' status: public title: Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2011' ... --- _id: '3361' abstract: - lang: eng text: In this paper, we investigate the computational complexity of quantitative information flow (QIF) problems. Information-theoretic quantitative relaxations of noninterference (based on Shannon entropy)have been introduced to enable more fine-grained reasoning about programs in situations where limited information flow is acceptable. The QIF bounding problem asks whether the information flow in a given program is bounded by a constant $d$. Our first result is that the QIF bounding problem is PSPACE-complete. The QIF memoryless synthesis problem asks whether it is possible to resolve nondeterministic choices in a given partial program in such a way that in the resulting deterministic program, the quantitative information flow is bounded by a given constant $d$. Our second result is that the QIF memoryless synthesis problem is also EXPTIME-complete. The QIF memoryless synthesis problem generalizes to QIF general synthesis problem which does not impose the memoryless requirement (that is, by allowing the synthesized program to have more variables then the original partial program). Our third result is that the QIF general synthesis problem is EXPTIME-hard. author: - first_name: Pavol full_name: Cerny, Pavol id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87 last_name: Cerny - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 citation: ama: 'Cerny P, Chatterjee K, Henzinger TA. The complexity of quantitative information flow problems. In: IEEE; 2011:205-217. doi:10.1109/CSF.2011.21' apa: 'Cerny, P., Chatterjee, K., & Henzinger, T. A. (2011). The complexity of quantitative information flow problems (pp. 205–217). Presented at the CSF: Computer Security Foundations, Cernay-la-Ville, France: IEEE. https://doi.org/10.1109/CSF.2011.21' chicago: Cerny, Pavol, Krishnendu Chatterjee, and Thomas A Henzinger. “The Complexity of Quantitative Information Flow Problems,” 205–17. IEEE, 2011. https://doi.org/10.1109/CSF.2011.21. ieee: 'P. Cerny, K. Chatterjee, and T. A. Henzinger, “The complexity of quantitative information flow problems,” presented at the CSF: Computer Security Foundations, Cernay-la-Ville, France, 2011, pp. 205–217.' ista: 'Cerny P, Chatterjee K, Henzinger TA. 2011. The complexity of quantitative information flow problems. CSF: Computer Security Foundations, 205–217.' mla: Cerny, Pavol, et al. The Complexity of Quantitative Information Flow Problems. IEEE, 2011, pp. 205–17, doi:10.1109/CSF.2011.21. short: P. Cerny, K. Chatterjee, T.A. Henzinger, in:, IEEE, 2011, pp. 205–217. conference: end_date: 2011-06-29 location: Cernay-la-Ville, France name: 'CSF: Computer Security Foundations' start_date: 2011-06-27 date_created: 2018-12-11T12:02:54Z date_published: 2011-06-27T00:00:00Z date_updated: 2021-01-12T07:42:56Z day: '27' ddc: - '000' - '005' department: - _id: ToHe - _id: KrCh doi: 10.1109/CSF.2011.21 ec_funded: 1 file: - access_level: open_access checksum: 1a25be0c62459fc7640db88af08ff63a content_type: application/pdf creator: system date_created: 2018-12-12T10:10:07Z date_updated: 2020-07-14T12:46:10Z file_id: '4792' file_name: IST-2012-81-v1+1_The_complexity_of_quantitative_information_flow_problems.pdf file_size: 299069 relation: main_file file_date_updated: 2020-07-14T12:46:10Z has_accepted_license: '1' language: - iso: eng month: '06' oa: 1 oa_version: Submitted Version page: 205 - 217 project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25F5A88A-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Moderne Concurrency Paradigms - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication_status: published publisher: IEEE publist_id: '3254' pubrep_id: '81' quality_controlled: '1' scopus_import: 1 status: public title: The complexity of quantitative information flow problems type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 year: '2011' ... --- _id: '3357' abstract: - lang: eng text: We consider two-player graph games whose objectives are request-response condition, i.e conjunctions of conditions of the form "if a state with property Rq is visited, then later a state with property Rp is visited". The winner of such games can be decided in EXPTIME and the problem is known to be NP-hard. In this paper, we close this gap by showing that this problem is, in fact, EXPTIME-complete. We show that the problem becomes PSPACE-complete if we only consider games played on DAGs, and NP-complete or PTIME-complete if there is only one player (depending on whether he wants to enforce or spoil the request-response condition). We also present near-optimal bounds on the memory needed to design winning strategies for each player, in each case. alternative_title: - LNCS author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Florian full_name: Horn, Florian id: 37327ACE-F248-11E8-B48F-1D18A9856A87 last_name: Horn citation: ama: 'Chatterjee K, Henzinger TA, Horn F. The complexity of request-response games. In: Dediu A-H, Inenaga S, Martín-Vide C, eds. Vol 6638. Springer; 2011:227-237. doi:10.1007/978-3-642-21254-3_17' apa: 'Chatterjee, K., Henzinger, T. A., & Horn, F. (2011). The complexity of request-response games. In A.-H. Dediu, S. Inenaga, & C. Martín-Vide (Eds.) (Vol. 6638, pp. 227–237). Presented at the LATA: Language and Automata Theory and Applications, Tarragona, Spain: Springer. https://doi.org/10.1007/978-3-642-21254-3_17' chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Florian Horn. “The Complexity of Request-Response Games.” edited by Adrian-Horia Dediu, Shunsuke Inenaga, and Carlos Martín-Vide, 6638:227–37. Springer, 2011. https://doi.org/10.1007/978-3-642-21254-3_17. ieee: 'K. Chatterjee, T. A. Henzinger, and F. Horn, “The complexity of request-response games,” presented at the LATA: Language and Automata Theory and Applications, Tarragona, Spain, 2011, vol. 6638, pp. 227–237.' ista: 'Chatterjee K, Henzinger TA, Horn F. 2011. The complexity of request-response games. LATA: Language and Automata Theory and Applications, LNCS, vol. 6638, 227–237.' mla: Chatterjee, Krishnendu, et al. The Complexity of Request-Response Games. Edited by Adrian-Horia Dediu et al., vol. 6638, Springer, 2011, pp. 227–37, doi:10.1007/978-3-642-21254-3_17. short: K. Chatterjee, T.A. Henzinger, F. Horn, in:, A.-H. Dediu, S. Inenaga, C. Martín-Vide (Eds.), Springer, 2011, pp. 227–237. conference: end_date: 2011-05-31 location: Tarragona, Spain name: 'LATA: Language and Automata Theory and Applications' start_date: 2011-05-26 date_created: 2018-12-11T12:02:52Z date_published: 2011-01-01T00:00:00Z date_updated: 2021-01-12T07:42:54Z day: '01' department: - _id: KrCh - _id: ToHe doi: 10.1007/978-3-642-21254-3_17 editor: - first_name: Adrian-Horia full_name: Dediu, Adrian-Horia last_name: Dediu - first_name: Shunsuke full_name: Inenaga, Shunsuke last_name: Inenaga - first_name: Carlos full_name: Martín-Vide, Carlos last_name: Martín-Vide intvolume: ' 6638' language: - iso: eng month: '01' oa_version: None page: 227 - 237 publication_status: published publisher: Springer publist_id: '3258' quality_controlled: '1' scopus_import: 1 status: public title: The complexity of request-response games type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 6638 year: '2011' ... --- _id: '5379' abstract: - lang: eng text: Computing the winning set for Büchi objectives in alternating games on graphs is a central problem in computer aided verification with a large number of applications. The long standing best known upper bound for solving the problem is ̃O(n·m), where n is the number of vertices and m is the number of edges in the graph. We are the first to break the ̃O(n·m) boundary by presenting a new technique that reduces the running time to O(n2). This bound also leads to O(n2) time algorithms for computing the set of almost-sure winning vertices for Büchi objectives (1) in alternating games with probabilistic transitions (improving an earlier bound of O(n·m)), (2) in concurrent graph games with constant actions (improving an earlier bound of O(n3)), and (3) in Markov decision processes (improving for m > n4/3 an earlier bound of O(min(m1.5, m·n2/3)). We also show that the same technique can be used to compute the maximal end-component decomposition of a graph in time O(n2), which is an improvement over earlier bounds for m > n4/3. Finally, we show how to maintain the winning set for Büchi objectives in alternating games under a sequence of edge insertions or a sequence of edge deletions in O(n) amortized time per operation. This is the first dynamic algorithm for this problem. alternative_title: - IST Austria Technical Report article_processing_charge: No author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Monika H full_name: Henzinger, Monika H id: 540c9bbd-f2de-11ec-812d-d04a5be85630 last_name: Henzinger orcid: 0000-0002-5008-6530 citation: ama: Chatterjee K, Henzinger MH. An O(N2) Time Algorithm for Alternating Büchi Games. IST Austria; 2011. doi:10.15479/AT:IST-2011-0009 apa: Chatterjee, K., & Henzinger, M. H. (2011). An O(n2) time algorithm for alternating Büchi games. IST Austria. https://doi.org/10.15479/AT:IST-2011-0009 chicago: Chatterjee, Krishnendu, and Monika H Henzinger. An O(N2) Time Algorithm for Alternating Büchi Games. IST Austria, 2011. https://doi.org/10.15479/AT:IST-2011-0009. ieee: K. Chatterjee and M. H. Henzinger, An O(n2) time algorithm for alternating Büchi games. IST Austria, 2011. ista: Chatterjee K, Henzinger MH. 2011. An O(n2) time algorithm for alternating Büchi games, IST Austria, 20p. mla: Chatterjee, Krishnendu, and Monika H. Henzinger. An O(N2) Time Algorithm for Alternating Büchi Games. IST Austria, 2011, doi:10.15479/AT:IST-2011-0009. short: K. Chatterjee, M.H. Henzinger, An O(N2) Time Algorithm for Alternating Büchi Games, IST Austria, 2011. date_created: 2018-12-12T11:38:59Z date_published: 2011-07-11T00:00:00Z date_updated: 2023-02-23T11:15:12Z day: '11' ddc: - '000' - '004' department: - _id: KrCh doi: 10.15479/AT:IST-2011-0009 file: - access_level: open_access checksum: 0b354264229045d982332fd2cb5b9a26 content_type: application/pdf creator: system date_created: 2018-12-12T11:53:43Z date_updated: 2020-07-14T12:46:39Z file_id: '5504' file_name: IST-2011-0009_IST-2011-0009.pdf file_size: 388665 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: '20' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '15' related_material: record: - id: '3165' relation: later_version status: public status: public title: An O(n2) time algorithm for alternating Büchi games type: technical_report user_id: 6785fbc1-c503-11eb-8a32-93094b40e1cf year: '2011' ... --- _id: '5381' abstract: - lang: eng text: "In two-player finite-state stochastic games of partial obser- vation on graphs, in every state of the graph, the players simultaneously choose an action, and their joint actions determine a probability distri- bution over the successor states. The game is played for infinitely many rounds and thus the players construct an infinite path in the graph. We consider reachability objectives where the first player tries to ensure a target state to be visited almost-surely (i.e., with probability 1) or pos- itively (i.e., with positive probability), no matter the strategy of the second player.\r\n\r\nWe classify such games according to the information and to the power of randomization available to the players. On the basis of information, the game can be one-sided with either (a) player 1, or (b) player 2 having partial observation (and the other player has perfect observation), or two- sided with (c) both players having partial observation. On the basis of randomization, (a) the players may not be allowed to use randomization (pure strategies), or (b) they may choose a probability distribution over actions but the actual random choice is external and not visible to the player (actions invisible), or (c) they may use full randomization.\r\n\r\nOur main results for pure strategies are as follows: (1) For one-sided games with player 2 perfect observation we show that (in contrast to full randomized strategies) belief-based (subset-construction based) strate- gies are not sufficient, and present an exponential upper bound on mem- ory both for almost-sure and positive winning strategies; we show that the problem of deciding the existence of almost-sure and positive winning strategies for player 1 is EXPTIME-complete and present symbolic algo- rithms that avoid the explicit exponential construction. (2) For one-sided games with player 1 perfect observation we show that non-elementary memory is both necessary and sufficient for both almost-sure and posi- tive winning strategies. (3) We show that for the general (two-sided) case finite-memory strategies are sufficient for both positive and almost-sure winning, and at least non-elementary memory is required. We establish the equivalence of the almost-sure winning problems for pure strategies and for randomized strategies with actions invisible. Our equivalence re- sult exhibit serious flaws in previous results in the literature: we show a non-elementary memory lower bound for almost-sure winning whereas an exponential upper bound was previously claimed." 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. Partial-Observation Stochastic Games: How to Win When Belief Fails. IST Austria; 2011. doi:10.15479/AT:IST-2011-0007' apa: 'Chatterjee, K., & Doyen, L. (2011). Partial-observation stochastic games: How to win when belief fails. IST Austria. https://doi.org/10.15479/AT:IST-2011-0007' chicago: 'Chatterjee, Krishnendu, and Laurent Doyen. Partial-Observation Stochastic Games: How to Win When Belief Fails. IST Austria, 2011. https://doi.org/10.15479/AT:IST-2011-0007.' ieee: 'K. Chatterjee and L. Doyen, Partial-observation stochastic games: How to win when belief fails. IST Austria, 2011.' ista: 'Chatterjee K, Doyen L. 2011. Partial-observation stochastic games: How to win when belief fails, IST Austria, 43p.' mla: 'Chatterjee, Krishnendu, and Laurent Doyen. Partial-Observation Stochastic Games: How to Win When Belief Fails. IST Austria, 2011, doi:10.15479/AT:IST-2011-0007.' short: 'K. Chatterjee, L. Doyen, Partial-Observation Stochastic Games: How to Win When Belief Fails, IST Austria, 2011.' date_created: 2018-12-12T11:39:00Z date_published: 2011-07-05T00:00:00Z date_updated: 2023-02-23T11:05:48Z day: '05' ddc: - '000' - '005' department: - _id: KrCh doi: 10.15479/AT:IST-2011-0007 file: - access_level: open_access checksum: 06bf6dfc97f6006e3fd0e9a3f31bc961 content_type: application/pdf creator: system date_created: 2018-12-12T11:53:27Z date_updated: 2020-07-14T12:46:39Z file_id: '5488' file_name: IST-2011-0007_IST-2011-0007.pdf file_size: 574055 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: '43' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '17' related_material: record: - id: '1903' relation: later_version status: public - id: '2211' relation: later_version status: public - id: '2955' relation: later_version status: public status: public title: 'Partial-observation stochastic games: How to win when belief fails' type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2011' ... --- _id: '5380' abstract: - lang: eng text: 'We consider 2-player games played on a finite state space for an infinite number of rounds. The games are concurrent: in each round, the two players (player 1 and player 2) choose their moves independently and simultaneously; the current state and the two moves determine the successor state. We study concurrent games with ω-regular winning conditions specified as parity objectives. We consider the qualitative analysis problems: the computation of the almost-sure and limit-sure winning set of states, where player 1 can ensure to win with probability 1 and with probability arbitrarily close to 1, respectively. In general the almost-sure and limit-sure winning strategies require both infinite-memory as well as infinite-precision (to describe probabilities). We study the bounded-rationality problem for qualitative analysis of concurrent parity games, where the strategy set for player 1 is restricted to bounded-resource strategies. In terms of precision, strategies can be deterministic, uniform, finite-precision or infinite-precision; and in terms of memory, strategies can be memoryless, finite-memory or infinite-memory. We present a precise and complete characterization of the qualitative winning sets for all combinations of classes of strategies. In particular, we show that uniform memoryless strategies are as powerful as finite-precision infinite-memory strategies, and infinite-precision memoryless strategies are as powerful as infinite-precision finite-memory strategies. We show that the winning sets can be computed in O(n2d+3) time, where n is the size of the game structure and 2d is the number of priorities (or colors), and our algorithms are symbolic. The membership problem of whether a state belongs to a winning set can be decided in NP ∩ coNP. While this complexity is the same as for the simpler class of turn-based parity games, where in each state only one of the two players has a choice of moves, our algorithms,that are obtained by characterization of the winning sets as μ-calculus formulas, are considerably more involved than those for turn-based 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 citation: ama: Chatterjee K. Bounded Rationality in Concurrent Parity Games. IST Austria; 2011. doi:10.15479/AT:IST-2011-0008 apa: Chatterjee, K. (2011). Bounded rationality in concurrent parity games. IST Austria. https://doi.org/10.15479/AT:IST-2011-0008 chicago: Chatterjee, Krishnendu. Bounded Rationality in Concurrent Parity Games. IST Austria, 2011. https://doi.org/10.15479/AT:IST-2011-0008. ieee: K. Chatterjee, Bounded rationality in concurrent parity games. IST Austria, 2011. ista: Chatterjee K. 2011. Bounded rationality in concurrent parity games, IST Austria, 53p. mla: Chatterjee, Krishnendu. Bounded Rationality in Concurrent Parity Games. IST Austria, 2011, doi:10.15479/AT:IST-2011-0008. short: K. Chatterjee, Bounded Rationality in Concurrent Parity Games, IST Austria, 2011. date_created: 2018-12-12T11:39:00Z date_published: 2011-07-11T00:00:00Z date_updated: 2023-02-23T11:22:53Z day: '11' ddc: - '000' department: - _id: KrCh doi: 10.15479/AT:IST-2011-0008 file: - access_level: open_access checksum: 0fd38186409be819a911c4990fa79d1f content_type: application/pdf creator: system date_created: 2018-12-12T11:54:22Z date_updated: 2020-07-14T12:46:39Z file_id: '5544' file_name: IST-2011-0008_IST-2011-0008.pdf file_size: 500399 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: '53' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '16' related_material: record: - id: '3338' relation: later_version status: public status: public title: Bounded rationality in concurrent parity games type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2011' ... --- _id: '5382' abstract: - lang: eng text: 'We consider two-player stochastic games played on a finite state space for an infinite num- ber of rounds. The games are concurrent: in each round, the two players (player 1 and player 2) choose their moves independently and simultaneously; the current state and the two moves determine a probability distribution over the successor states. We also consider the important special case of turn-based stochastic games where players make moves in turns, rather than concurrently. We study concurrent games with ω-regular winning conditions specified as parity objectives. The value for player 1 for a parity objective is the maximal probability with which the player can guarantee the satisfaction of the objective against all strategies of the opponent. We study the problem of continuity and robustness of the value function in concurrent and turn-based stochastic parity games with respect to imprecision in the transition probabilities. We present quantitative bounds on the difference of the value function (in terms of the imprecision of the transition probabilities) and show the value continuity for structurally equivalent concurrent games (two games are structurally equivalent if the support of the transition func- tion is same and the probabilities differ). We also show robustness of optimal strategies for structurally equivalent turn-based stochastic parity games. Finally we show that the value continuity property breaks without the structurally equivalent assumption (even for Markov chains) and show that our quantitative bound is asymptotically optimal. Hence our results are tight (the assumption is both necessary and sufficient) and optimal (our quantitative bound is asymptotically optimal).' 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 citation: ama: Chatterjee K. Robustness of Structurally Equivalent Concurrent Parity Games. IST Austria; 2011. doi:10.15479/AT:IST-2011-0006 apa: Chatterjee, K. (2011). Robustness of structurally equivalent concurrent parity games. IST Austria. https://doi.org/10.15479/AT:IST-2011-0006 chicago: Chatterjee, Krishnendu. Robustness of Structurally Equivalent Concurrent Parity Games. IST Austria, 2011. https://doi.org/10.15479/AT:IST-2011-0006. ieee: K. Chatterjee, Robustness of structurally equivalent concurrent parity games. IST Austria, 2011. ista: Chatterjee K. 2011. Robustness of structurally equivalent concurrent parity games, IST Austria, 18p. mla: Chatterjee, Krishnendu. Robustness of Structurally Equivalent Concurrent Parity Games. IST Austria, 2011, doi:10.15479/AT:IST-2011-0006. short: K. Chatterjee, Robustness of Structurally Equivalent Concurrent Parity Games, IST Austria, 2011. date_created: 2018-12-12T11:39:00Z date_published: 2011-06-27T00:00:00Z date_updated: 2023-02-23T11:23:01Z day: '27' ddc: - '000' - '005' department: - _id: KrCh doi: 10.15479/AT:IST-2011-0006 file: - access_level: open_access checksum: 1322b652d6ab07eb5248298a3f91c1cf content_type: application/pdf creator: system date_created: 2018-12-12T11:54:24Z date_updated: 2020-07-14T12:46:40Z file_id: '5546' file_name: IST-2011-0006_IST-2011-0006.pdf file_size: 335997 relation: main_file file_date_updated: 2020-07-14T12:46:40Z 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: '18' related_material: record: - id: '3341' relation: later_version status: public status: public title: Robustness of structurally equivalent concurrent parity games type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2011' ... --- _id: '3338' abstract: - lang: eng text: 'We consider 2-player games played on a finite state space for an infinite number of rounds. The games are concurrent: in each round, the two players (player 1 and player 2) choose their moves inde- pendently and simultaneously; the current state and the two moves determine the successor state. We study concurrent games with ω-regular winning conditions specified as parity objectives. We consider the qualitative analysis problems: the computation of the almost-sure and limit-sure winning set of states, where player 1 can ensure to win with probability 1 and with probability arbitrarily close to 1, respec- tively. In general the almost-sure and limit-sure winning strategies require both infinite-memory as well as infinite-precision (to describe probabilities). We study the bounded-rationality problem for qualitative analysis of concurrent parity games, where the strategy set for player 1 is restricted to bounded-resource strategies. In terms of precision, strategies can be deterministic, uniform, finite-precision or infinite- precision; and in terms of memory, strategies can be memoryless, finite-memory or infinite-memory. We present a precise and complete characterization of the qualitative winning sets for all combinations of classes of strategies. In particular, we show that uniform memoryless strategies are as powerful as finite-precision infinite-memory strategies, and infinite-precision memoryless strategies are as power- ful as infinite-precision finite-memory strategies. We show that the winning sets can be computed in O(n2d+3) time, where n is the size of the game structure and 2d is the number of priorities (or colors), and our algorithms are symbolic. The membership problem of whether a state belongs to a winning set can be decided in NP ∩ coNP. While this complexity is the same as for the simpler class of turn-based parity games, where in each state only one of the two players has a choice of moves, our algorithms, that are obtained by characterization of the winning sets as μ-calculus formulas, are considerably more involved than those for turn-based games.' author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X citation: ama: Chatterjee K. Bounded rationality in concurrent parity games. arXiv. 2011:1-51. apa: Chatterjee, K. (2011). Bounded rationality in concurrent parity games. arXiv. ArXiv. chicago: Chatterjee, Krishnendu. “Bounded Rationality in Concurrent Parity Games.” ArXiv. ArXiv, 2011. ieee: K. Chatterjee, “Bounded rationality in concurrent parity games,” arXiv. ArXiv, pp. 1–51, 2011. ista: Chatterjee K. 2011. Bounded rationality in concurrent parity games. arXiv, 1–51, . mla: Chatterjee, Krishnendu. “Bounded Rationality in Concurrent Parity Games.” ArXiv, ArXiv, 2011, pp. 1–51. short: K. Chatterjee, ArXiv (2011) 1–51. date_created: 2018-12-11T12:02:45Z date_published: 2011-07-11T00:00:00Z date_updated: 2023-02-23T12:23:40Z day: '11' department: - _id: KrCh external_id: arxiv: - '1107.2146' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1107.2146 month: '07' oa: 1 oa_version: Preprint page: 1 - 51 publication: arXiv publication_status: published publisher: ArXiv publist_id: '3287' related_material: record: - id: '5380' relation: earlier_version status: public status: public title: Bounded rationality in concurrent parity games type: preprint user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2011' ... --- _id: '3356' abstract: - lang: eng text: There is recently a significant effort to add quantitative objectives to formal verification and synthesis. We introduce and investigate the extension of temporal logics with quantitative atomic assertions, aiming for a general and flexible framework for quantitative-oriented specifications. In the heart of quantitative objectives lies the accumulation of values along a computation. It is either the accumulated summation, as with the energy objectives, or the accumulated average, as with the mean-payoff objectives. We investigate the extension of temporal logics with the prefix-accumulation assertions Sum(v) ≥ c and Avg(v) ≥ c, where v is a numeric variable of the system, c is a constant rational number, and Sum(v) and Avg(v) denote the accumulated sum and average of the values of v from the beginning of the computation up to the current point of time. We also allow the path-accumulation assertions LimInfAvg(v) ≥ c and LimSupAvg(v) ≥ c, referring to the average value along an entire computation. We study the border of decidability for extensions of various temporal logics. In particular, we show that extending the fragment of CTL that has only the EX, EF, AX, and AG temporal modalities by prefix-accumulation assertions and extending LTL with path-accumulation assertions, result in temporal logics whose model-checking problem is decidable. The extended logics allow to significantly extend the currently known energy and mean-payoff objectives. Moreover, the prefix-accumulation assertions may be refined with "controlled-accumulation", allowing, for example, to specify constraints on the average waiting time between a request and a grant. On the negative side, we show that the fragment we point to is, in a sense, the maximal logic whose extension with prefix-accumulation assertions permits a decidable model-checking procedure. Extending a temporal logic that has the EG or EU modalities, and in particular CTL and LTL, makes the problem undecidable. article_number: '5970226' author: - first_name: Udi full_name: Boker, Udi id: 31E297B6-F248-11E8-B48F-1D18A9856A87 last_name: Boker - 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: Orna full_name: Kupferman, Orna last_name: Kupferman citation: ama: 'Boker U, Chatterjee K, Henzinger TA, Kupferman O. Temporal specifications with accumulative values. In: IEEE; 2011. doi:10.1109/LICS.2011.33' apa: 'Boker, U., Chatterjee, K., Henzinger, T. A., & Kupferman, O. (2011). Temporal specifications with accumulative values. Presented at the LICS: Logic in Computer Science, Toronto, Canada: IEEE. https://doi.org/10.1109/LICS.2011.33' chicago: Boker, Udi, Krishnendu Chatterjee, Thomas A Henzinger, and Orna Kupferman. “Temporal Specifications with Accumulative Values.” IEEE, 2011. https://doi.org/10.1109/LICS.2011.33. ieee: 'U. Boker, K. Chatterjee, T. A. Henzinger, and O. Kupferman, “Temporal specifications with accumulative values,” presented at the LICS: Logic in Computer Science, Toronto, Canada, 2011.' ista: 'Boker U, Chatterjee K, Henzinger TA, Kupferman O. 2011. Temporal specifications with accumulative values. LICS: Logic in Computer Science, 5970226.' mla: Boker, Udi, et al. Temporal Specifications with Accumulative Values. 5970226, IEEE, 2011, doi:10.1109/LICS.2011.33. short: U. Boker, K. Chatterjee, T.A. Henzinger, O. Kupferman, in:, IEEE, 2011. conference: end_date: 2011-06-24 location: Toronto, Canada name: 'LICS: Logic in Computer Science' start_date: 2011-06-21 date_created: 2018-12-11T12:02:52Z date_published: 2011-06-21T00:00:00Z date_updated: 2023-02-23T12:23:54Z day: '21' ddc: - '000' - '004' department: - _id: ToHe - _id: KrCh doi: 10.1109/LICS.2011.33 ec_funded: 1 file: - access_level: open_access checksum: 792128f5455f0f40f1105f0398e05fa9 content_type: application/pdf creator: system date_created: 2018-12-12T10:12:42Z date_updated: 2020-07-14T12:46:09Z file_id: '4960' file_name: IST-2012-83-v1+1_Temporal_specifications_with_accumulative_values.pdf file_size: 225426 relation: main_file file_date_updated: 2020-07-14T12:46:09Z has_accepted_license: '1' language: - iso: eng month: '06' oa: 1 oa_version: Submitted Version project: - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 25EFB36C-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '215543' name: COMponent-Based Embedded Systems design Techniques - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25F1337C-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '214373' name: Design for Embedded Systems - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication_status: published publisher: IEEE publist_id: '3259' pubrep_id: '83' related_material: record: - id: '2038' relation: later_version status: public - id: '5385' relation: earlier_version status: public scopus_import: 1 status: public title: Temporal specifications with accumulative values type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 year: '2011' ... --- _id: '5385' abstract: - lang: eng text: There is recently a significant effort to add quantitative objectives to formal verification and synthesis. We introduce and investigate the extension of temporal logics with quantitative atomic assertions, aiming for a general and flexible framework for quantitative-oriented specifications. In the heart of quantitative objectives lies the accumulation of values along a computation. It is either the accumulated summation, as with the energy objectives, or the accumulated average, as with the mean-payoff objectives. We investigate the extension of temporal logics with the prefix-accumulation assertions Sum(v) ≥ c and Avg(v) ≥ c, where v is a numeric variable of the system, c is a constant rational number, and Sum(v) and Avg(v) denote the accumulated sum and average of the values of v from the beginning of the computation up to the current point of time. We also allow the path-accumulation assertions LimInfAvg(v) ≥ c and LimSupAvg(v) ≥ c, referring to the average value along an entire computation. We study the border of decidability for extensions of various temporal logics. In particular, we show that extending the fragment of CTL that has only the EX, EF, AX, and AG temporal modalities by prefix-accumulation assertions and extending LTL with path-accumulation assertions, result in temporal logics whose model-checking problem is decidable. The extended logics allow to significantly extend the currently known energy and mean-payoff objectives. Moreover, the prefix-accumulation assertions may be refined with “controlled-accumulation”, allowing, for example, to specify constraints on the average waiting time between a request and a grant. On the negative side, we show that the fragment we point to is, in a sense, the maximal logic whose extension with prefix-accumulation assertions permits a decidable model-checking procedure. Extending a temporal logic that has the EG or EU modalities, and in particular CTL and LTL, makes the problem undecidable. 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: 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: Orna full_name: Kupferman, Orna last_name: Kupferman citation: ama: Boker U, Chatterjee K, Henzinger TA, Kupferman O. Temporal Specifications with Accumulative Values. IST Austria; 2011. doi:10.15479/AT:IST-2011-0003 apa: Boker, U., Chatterjee, K., Henzinger, T. A., & Kupferman, O. (2011). Temporal specifications with accumulative values. IST Austria. https://doi.org/10.15479/AT:IST-2011-0003 chicago: Boker, Udi, Krishnendu Chatterjee, Thomas A Henzinger, and Orna Kupferman. Temporal Specifications with Accumulative Values. IST Austria, 2011. https://doi.org/10.15479/AT:IST-2011-0003. ieee: U. Boker, K. Chatterjee, T. A. Henzinger, and O. Kupferman, Temporal specifications with accumulative values. IST Austria, 2011. ista: Boker U, Chatterjee K, Henzinger TA, Kupferman O. 2011. Temporal specifications with accumulative values, IST Austria, 14p. mla: Boker, Udi, et al. Temporal Specifications with Accumulative Values. IST Austria, 2011, doi:10.15479/AT:IST-2011-0003. short: U. Boker, K. Chatterjee, T.A. Henzinger, O. Kupferman, Temporal Specifications with Accumulative Values, IST Austria, 2011. date_created: 2018-12-12T11:39:02Z date_published: 2011-04-04T00:00:00Z date_updated: 2023-02-23T11:23:41Z day: '04' ddc: - '000' - '004' department: - _id: ToHe - _id: KrCh doi: 10.15479/AT:IST-2011-0003 ec_funded: 1 file: - access_level: open_access checksum: 8491d0d48c4911620ecd5350b413c11e content_type: application/pdf creator: system date_created: 2018-12-12T11:53:00Z date_updated: 2020-07-14T12:46:41Z file_id: '5461' file_name: IST-2011-0003_IST-2011-0003.pdf file_size: 366281 relation: main_file file_date_updated: 2020-07-14T12:46:41Z has_accepted_license: '1' language: - iso: eng month: '04' oa: 1 oa_version: Published Version page: '14' project: - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 25EFB36C-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '215543' name: COMponent-Based Embedded Systems design Techniques - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25F1337C-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '214373' name: Design for Embedded Systems - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '21' related_material: record: - id: '2038' relation: later_version status: public - id: '3356' relation: later_version status: public status: public title: Temporal specifications with accumulative values type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2011' ... --- _id: '5384' abstract: - lang: eng text: 'We consider probabilistic automata on infinite words with acceptance defined by parity conditions. We consider three qualitative decision problems: (i) the positive decision problem asks whether there is a word that is accepted with positive probability; (ii) the almost decision problem asks whether there is a word that is accepted with probability 1; and (iii) the limit decision problem asks whether for every ε > 0 there is a word that is accepted with probability at least 1 − ε. We unify and generalize several decidability results for probabilistic automata over infinite words, and identify a robust (closed under union and intersection) subclass of probabilistic automata for which all the qualitative decision problems are decidable for parity conditions. We also show that if the input words are restricted to lasso shape words, then the positive and almost problems are decidable for all probabilistic automata with parity conditions.' 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: Mathieu full_name: Tracol, Mathieu id: 3F54FA38-F248-11E8-B48F-1D18A9856A87 last_name: Tracol citation: ama: Chatterjee K, Tracol M. Decidable Problems for Probabilistic Automata on Infinite Words. IST Austria; 2011. doi:10.15479/AT:IST-2011-0004 apa: Chatterjee, K., & Tracol, M. (2011). Decidable problems for probabilistic automata on infinite words. IST Austria. https://doi.org/10.15479/AT:IST-2011-0004 chicago: Chatterjee, Krishnendu, and Mathieu Tracol. Decidable Problems for Probabilistic Automata on Infinite Words. IST Austria, 2011. https://doi.org/10.15479/AT:IST-2011-0004. ieee: K. Chatterjee and M. Tracol, Decidable problems for probabilistic automata on infinite words. IST Austria, 2011. ista: Chatterjee K, Tracol M. 2011. Decidable problems for probabilistic automata on infinite words, IST Austria, 30p. mla: Chatterjee, Krishnendu, and Mathieu Tracol. Decidable Problems for Probabilistic Automata on Infinite Words. IST Austria, 2011, doi:10.15479/AT:IST-2011-0004. short: K. Chatterjee, M. Tracol, Decidable Problems for Probabilistic Automata on Infinite Words, IST Austria, 2011. date_created: 2018-12-12T11:39:01Z date_published: 2011-04-11T00:00:00Z date_updated: 2023-02-23T11:05:53Z day: '11' ddc: - '000' - '005' department: - _id: KrCh doi: 10.15479/AT:IST-2011-0004 file: - access_level: open_access checksum: f5a0f664fadc335990f5fcf138df19f1 content_type: application/pdf creator: system date_created: 2018-12-12T11:54:23Z date_updated: 2020-07-14T12:46:40Z file_id: '5545' file_name: IST-2011-004_IST-2011-0004.pdf file_size: 570827 relation: main_file file_date_updated: 2020-07-14T12:46:40Z has_accepted_license: '1' language: - iso: eng month: '04' oa: 1 oa_version: Published Version page: '30' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '20' related_material: record: - id: '2957' relation: later_version status: public status: public title: Decidable problems for probabilistic automata on infinite words type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2011' ... --- _id: '3366' abstract: - lang: eng text: 'We present an algorithmic method for the quantitative, performance-aware synthesis of concurrent programs. The input consists of a nondeterministic partial program and of a parametric performance model. The nondeterminism allows the programmer to omit which (if any) synchronization construct is used at a particular program location. The performance model, specified as a weighted automaton, can capture system architectures by assigning different costs to actions such as locking, context switching, and memory and cache accesses. The quantitative synthesis problem is to automatically resolve the nondeterminism of the partial program so that both correctness is guaranteed and performance is optimal. As is standard for shared memory concurrency, correctness is formalized "specification free", in particular as race freedom or deadlock freedom. For worst-case (average-case) performance, we show that the problem can be reduced to 2-player graph games (with probabilistic transitions) with quantitative objectives. While we show, using game-theoretic methods, that the synthesis problem is Nexp-complete, we present an algorithmic method and an implementation that works efficiently for concurrent programs and performance models of practical interest. We have implemented a prototype tool and used it to synthesize finite-state concurrent programs that exhibit different programming patterns, for several performance models representing different architectures. ' alternative_title: - LNCS article_processing_charge: No author: - first_name: Pavol full_name: Cerny, Pavol id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87 last_name: Cerny - 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: Arjun full_name: Radhakrishna, Arjun id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87 last_name: Radhakrishna - first_name: Rohit full_name: Singh, Rohit last_name: Singh citation: ama: 'Cerny P, Chatterjee K, Henzinger TA, Radhakrishna A, Singh R. Quantitative synthesis for concurrent programs. In: Gopalakrishnan G, Qadeer S, eds. Vol 6806. Springer; 2011:243-259. doi:10.1007/978-3-642-22110-1_20' apa: 'Cerny, P., Chatterjee, K., Henzinger, T. A., Radhakrishna, A., & Singh, R. (2011). Quantitative synthesis for concurrent programs. In G. Gopalakrishnan & S. Qadeer (Eds.) (Vol. 6806, pp. 243–259). Presented at the CAV: Computer Aided Verification, Snowbird, USA: Springer. https://doi.org/10.1007/978-3-642-22110-1_20' chicago: Cerny, Pavol, Krishnendu Chatterjee, Thomas A Henzinger, Arjun Radhakrishna, and Rohit Singh. “Quantitative Synthesis for Concurrent Programs.” edited by Ganesh Gopalakrishnan and Shaz Qadeer, 6806:243–59. Springer, 2011. https://doi.org/10.1007/978-3-642-22110-1_20. ieee: 'P. Cerny, K. Chatterjee, T. A. Henzinger, A. Radhakrishna, and R. Singh, “Quantitative synthesis for concurrent programs,” presented at the CAV: Computer Aided Verification, Snowbird, USA, 2011, vol. 6806, pp. 243–259.' ista: 'Cerny P, Chatterjee K, Henzinger TA, Radhakrishna A, Singh R. 2011. Quantitative synthesis for concurrent programs. CAV: Computer Aided Verification, LNCS, vol. 6806, 243–259.' mla: Cerny, Pavol, et al. Quantitative Synthesis for Concurrent Programs. Edited by Ganesh Gopalakrishnan and Shaz Qadeer, vol. 6806, Springer, 2011, pp. 243–59, doi:10.1007/978-3-642-22110-1_20. short: P. Cerny, K. Chatterjee, T.A. Henzinger, A. Radhakrishna, R. Singh, in:, G. Gopalakrishnan, S. Qadeer (Eds.), Springer, 2011, pp. 243–259. conference: end_date: 2011-07-20 location: Snowbird, USA name: 'CAV: Computer Aided Verification' start_date: 2011-07-14 date_created: 2018-12-11T12:02:55Z date_published: 2011-04-21T00:00:00Z date_updated: 2023-02-23T12:24:01Z day: '21' ddc: - '000' - '004' department: - _id: ToHe - _id: KrCh doi: 10.1007/978-3-642-22110-1_20 ec_funded: 1 editor: - first_name: Ganesh full_name: Gopalakrishnan, Ganesh last_name: Gopalakrishnan - first_name: Shaz full_name: Qadeer, Shaz last_name: Qadeer file: - access_level: open_access checksum: c033689355f45742dc7c99b5af13ce7a content_type: application/pdf creator: system date_created: 2018-12-12T10:15:51Z date_updated: 2020-07-14T12:46:10Z file_id: '5174' file_name: IST-2012-76-v1+1_Quantitative_synthesis_for_concurrent_programs.pdf file_size: 508946 relation: main_file file_date_updated: 2020-07-14T12:46:10Z has_accepted_license: '1' intvolume: ' 6806' language: - iso: eng month: '04' oa: 1 oa_version: Submitted Version page: 243 - 259 project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25F5A88A-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Moderne Concurrency Paradigms - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship - _id: 25F1337C-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '214373' name: Design for Embedded Systems publication_status: published publisher: Springer publist_id: '3247' pubrep_id: '76' quality_controlled: '1' related_material: record: - id: '5388' relation: earlier_version status: public status: public title: Quantitative synthesis for concurrent programs type: conference user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 6806 year: '2011' ... --- _id: '3345' abstract: - lang: eng text: We consider Markov Decision Processes (MDPs) with mean-payoff parity and energy parity objectives. In system design, the parity objective is used to encode ω-regular specifications, and the mean-payoff and energy objectives can be used to model quantitative resource constraints. The energy condition re- quires that the resource level never drops below 0, and the mean-payoff condi- tion requires that the limit-average value of the resource consumption is within a threshold. While these two (energy and mean-payoff) classical conditions are equivalent for two-player games, we show that they differ for MDPs. We show that the problem of deciding whether a state is almost-sure winning (i.e., winning with probability 1) in energy parity MDPs is in NP ∩ coNP, while for mean- payoff parity MDPs, the problem is solvable in polynomial time, improving a recent PSPACE bound. alternative_title: - LNCS author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Laurent full_name: Doyen, Laurent last_name: Doyen citation: ama: 'Chatterjee K, Doyen L. Energy and mean-payoff parity Markov Decision Processes. In: Vol 6907. Springer; 2011:206-218. doi:10.1007/978-3-642-22993-0_21' apa: 'Chatterjee, K., & Doyen, L. (2011). Energy and mean-payoff parity Markov Decision Processes (Vol. 6907, pp. 206–218). Presented at the MFCS: Mathematical Foundations of Computer Science, Warsaw, Poland: Springer. https://doi.org/10.1007/978-3-642-22993-0_21' chicago: Chatterjee, Krishnendu, and Laurent Doyen. “Energy and Mean-Payoff Parity Markov Decision Processes,” 6907:206–18. Springer, 2011. https://doi.org/10.1007/978-3-642-22993-0_21. ieee: 'K. Chatterjee and L. Doyen, “Energy and mean-payoff parity Markov Decision Processes,” presented at the MFCS: Mathematical Foundations of Computer Science, Warsaw, Poland, 2011, vol. 6907, pp. 206–218.' ista: 'Chatterjee K, Doyen L. 2011. Energy and mean-payoff parity Markov Decision Processes. MFCS: Mathematical Foundations of Computer Science, LNCS, vol. 6907, 206–218.' mla: Chatterjee, Krishnendu, and Laurent Doyen. Energy and Mean-Payoff Parity Markov Decision Processes. Vol. 6907, Springer, 2011, pp. 206–18, doi:10.1007/978-3-642-22993-0_21. short: K. Chatterjee, L. Doyen, in:, Springer, 2011, pp. 206–218. conference: end_date: 2011-08-26 location: Warsaw, Poland name: 'MFCS: Mathematical Foundations of Computer Science' start_date: 2011-08-22 date_created: 2018-12-11T12:02:48Z date_published: 2011-09-28T00:00:00Z date_updated: 2023-02-23T12:23:59Z day: '28' department: - _id: KrCh doi: 10.1007/978-3-642-22993-0_21 external_id: arxiv: - '1104.2909' intvolume: ' 6907' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1104.2909 month: '09' oa: 1 oa_version: Preprint page: 206 - 218 project: - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication_status: published publisher: Springer publist_id: '3276' quality_controlled: '1' related_material: record: - id: '5387' relation: earlier_version status: public scopus_import: 1 status: public title: Energy and mean-payoff parity Markov Decision Processes type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 6907 year: '2011' ... --- _id: '5387' abstract: - lang: eng text: We consider Markov Decision Processes (MDPs) with mean-payoff parity and energy parity objectives. In system design, the parity objective is used to encode ω-regular specifications, and the mean-payoff and energy objectives can be used to model quantitative resource constraints. The energy condition re- quires that the resource level never drops below 0, and the mean-payoff condi- tion requires that the limit-average value of the resource consumption is within a threshold. While these two (energy and mean-payoff) classical conditions are equivalent for two-player games, we show that they differ for MDPs. We show that the problem of deciding whether a state is almost-sure winning (i.e., winning with probability 1) in energy parity MDPs is in NP ∩ coNP, while for mean- payoff parity MDPs, the problem is solvable in polynomial time, improving a recent PSPACE bound. 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. Energy and Mean-Payoff Parity Markov Decision Processes. IST Austria; 2011. doi:10.15479/AT:IST-2011-0001 apa: Chatterjee, K., & Doyen, L. (2011). Energy and mean-payoff parity Markov decision processes. IST Austria. https://doi.org/10.15479/AT:IST-2011-0001 chicago: Chatterjee, Krishnendu, and Laurent Doyen. Energy and Mean-Payoff Parity Markov Decision Processes. IST Austria, 2011. https://doi.org/10.15479/AT:IST-2011-0001. ieee: K. Chatterjee and L. Doyen, Energy and mean-payoff parity Markov decision processes. IST Austria, 2011. ista: Chatterjee K, Doyen L. 2011. Energy and mean-payoff parity Markov decision processes, IST Austria, 20p. mla: Chatterjee, Krishnendu, and Laurent Doyen. Energy and Mean-Payoff Parity Markov Decision Processes. IST Austria, 2011, doi:10.15479/AT:IST-2011-0001. short: K. Chatterjee, L. Doyen, Energy and Mean-Payoff Parity Markov Decision Processes, IST Austria, 2011. date_created: 2018-12-12T11:39:02Z date_published: 2011-02-16T00:00:00Z date_updated: 2023-02-23T11:23:11Z day: '16' ddc: - '000' - '005' department: - _id: KrCh doi: 10.15479/AT:IST-2011-0001 file: - access_level: open_access checksum: 824d6c70e6d3feb3e836b009e0b3cf73 content_type: application/pdf creator: system date_created: 2018-12-12T11:52:57Z date_updated: 2020-07-14T12:46:41Z file_id: '5458' file_name: IST-2011-0001_IST-2011-0001.pdf file_size: 329976 relation: main_file file_date_updated: 2020-07-14T12:46:41Z has_accepted_license: '1' language: - iso: eng month: '02' oa: 1 oa_version: Published Version page: '20' publication_identifier: issn: - 2664-1690 publication_status: published publisher: IST Austria pubrep_id: '23' related_material: record: - id: '3345' relation: later_version status: public status: public title: Energy and mean-payoff parity Markov decision processes type: technical_report user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2011' ... --- _id: '3858' abstract: - lang: eng text: 'We consider two-player zero-sum games on graphs. On the basis of the information available to the players these games can be classified as follows: (a) partial-observation (both players have partial view of the game); (b) one-sided partial-observation (one player has partial-observation and the other player has complete-observation); and (c) complete-observation (both players have com- plete view of the game). We survey the complexity results for the problem of de- ciding the winner in various classes of partial-observation games with ω-regular winning conditions specified as parity objectives. We present a reduction from the class of parity objectives that depend on sequence of states of the game to the sub-class of parity objectives that only depend on the sequence of observations. We also establish that partial-observation acyclic games are PSPACE-complete.' alternative_title: - LNCS article_processing_charge: No author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Laurent full_name: Doyen, Laurent last_name: Doyen citation: ama: 'Chatterjee K, Doyen L. The complexity of partial-observation parity games. In: Vol 6397. Springer; 2010:1-14. doi:10.1007/978-3-642-16242-8_1' apa: 'Chatterjee, K., & Doyen, L. (2010). The complexity of partial-observation parity games (Vol. 6397, pp. 1–14). Presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Yogyakarta, Indonesia: Springer. https://doi.org/10.1007/978-3-642-16242-8_1' chicago: Chatterjee, Krishnendu, and Laurent Doyen. “The Complexity of Partial-Observation Parity Games,” 6397:1–14. Springer, 2010. https://doi.org/10.1007/978-3-642-16242-8_1. ieee: 'K. Chatterjee and L. Doyen, “The complexity of partial-observation parity games,” presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Yogyakarta, Indonesia, 2010, vol. 6397, pp. 1–14.' ista: 'Chatterjee K, Doyen L. 2010. The complexity of partial-observation parity games. LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, LNCS, vol. 6397, 1–14.' mla: Chatterjee, Krishnendu, and Laurent Doyen. The Complexity of Partial-Observation Parity Games. Vol. 6397, Springer, 2010, pp. 1–14, doi:10.1007/978-3-642-16242-8_1. short: K. Chatterjee, L. Doyen, in:, Springer, 2010, pp. 1–14. conference: end_date: 2010-10-15 location: Yogyakarta, Indonesia name: 'LPAR: Logic for Programming, Artificial Intelligence, and Reasoning' start_date: 2010-10-10 date_created: 2018-12-11T12:05:33Z date_published: 2010-12-09T00:00:00Z date_updated: 2021-01-12T07:52:43Z day: '09' ddc: - '000' department: - _id: KrCh doi: 10.1007/978-3-642-16242-8_1 file: - access_level: open_access checksum: 770e86e5d78c56fddb4786a8da7ef126 content_type: application/pdf creator: dernst date_created: 2020-05-19T16:29:04Z date_updated: 2020-07-14T12:46:18Z file_id: '7872' file_name: 2010_LPAR_Chatterjee.pdf file_size: 142836 relation: main_file file_date_updated: 2020-07-14T12:46:18Z has_accepted_license: '1' intvolume: ' 6397' language: - iso: eng month: '12' oa: 1 oa_version: Submitted Version page: 1 - 14 publication_status: published publisher: Springer publist_id: '2323' quality_controlled: '1' scopus_import: 1 status: public title: The complexity of partial-observation parity games type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 6397 year: '2010' ... --- _id: '3856' abstract: - lang: eng text: 'We consider two-player zero-sum games on graphs. These games can be classified on the basis of the information of the players and on the mode of interaction between them. On the basis of information the classification is as follows: (a) partial-observation (both players have partial view of the game); (b) one-sided complete-observation (one player has complete observation); and (c) complete-observation (both players have complete view of the game). On the basis of mode of interaction we have the following classification: (a) concurrent (players interact simultaneously); and (b) turn-based (players interact in turn). The two sources of randomness in these games are randomness in transition function and randomness in strategies. In general, randomized strategies are more powerful than deterministic strategies, and randomness in transitions gives more general classes of games. We present a complete characterization for the classes of games where randomness is not helpful in: (a) the transition function (probabilistic transition can be simulated by deterministic transition); and (b) strategies (pure strategies are as powerful as randomized strategies). As consequence of our characterization we obtain new undecidability results for these games. ' acknowledgement: This research was supported by the European Union project COMBEST and the European Network of Excellence ArtistDesign. alternative_title: - LNCS author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Laurent full_name: Doyen, Laurent last_name: Doyen - first_name: Hugo full_name: Gimbert, Hugo last_name: Gimbert - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 citation: ama: 'Chatterjee K, Doyen L, Gimbert H, Henzinger TA. Randomness for free. In: Vol 6281. Springer; 2010:246-257. doi:10.1007/978-3-642-15155-2_23' apa: 'Chatterjee, K., Doyen, L., Gimbert, H., & Henzinger, T. A. (2010). Randomness for free (Vol. 6281, pp. 246–257). Presented at the MFCS: Mathematical Foundations of Computer Science, Brno, Czech Republic: Springer. https://doi.org/10.1007/978-3-642-15155-2_23' chicago: Chatterjee, Krishnendu, Laurent Doyen, Hugo Gimbert, and Thomas A Henzinger. “Randomness for Free,” 6281:246–57. Springer, 2010. https://doi.org/10.1007/978-3-642-15155-2_23. ieee: 'K. Chatterjee, L. Doyen, H. Gimbert, and T. A. Henzinger, “Randomness for free,” presented at the MFCS: Mathematical Foundations of Computer Science, Brno, Czech Republic, 2010, vol. 6281, pp. 246–257.' ista: 'Chatterjee K, Doyen L, Gimbert H, Henzinger TA. 2010. Randomness for free. MFCS: Mathematical Foundations of Computer Science, LNCS, vol. 6281, 246–257.' mla: Chatterjee, Krishnendu, et al. Randomness for Free. Vol. 6281, Springer, 2010, pp. 246–57, doi:10.1007/978-3-642-15155-2_23. short: K. Chatterjee, L. Doyen, H. Gimbert, T.A. Henzinger, in:, Springer, 2010, pp. 246–257. conference: end_date: 2010-08-27 location: Brno, Czech Republic name: 'MFCS: Mathematical Foundations of Computer Science' start_date: 2010-08-23 date_created: 2018-12-11T12:05:32Z date_published: 2010-09-06T00:00:00Z date_updated: 2023-02-23T10:12:00Z day: '06' department: - _id: KrCh - _id: ToHe doi: 10.1007/978-3-642-15155-2_23 ec_funded: 1 intvolume: ' 6281' language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/1006.0673v1 month: '09' oa: 1 oa_version: Preprint page: 246 - 257 project: - _id: 25EFB36C-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '215543' name: COMponent-Based Embedded Systems design Techniques - _id: 25F1337C-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '214373' name: Design for Embedded Systems publication_status: published publisher: Springer publist_id: '2325' pubrep_id: '60' quality_controlled: '1' related_material: record: - id: '1731' relation: later_version status: public scopus_import: 1 status: public title: Randomness for free type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 6281 year: '2010' ... --- _id: '3859' abstract: - lang: eng text: This book constitutes the proceedings of the 8th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2010, held in Klosterneuburg, Austria in September 2010. The 14 papers presented were carefully reviewed and selected from 31 submissions. In addition, the volume contains 3 invited talks and 2 invited tutorials.The aim of FORMATS is to promote the study of fundamental and practical aspects of timed systems, and to bring together researchers from different disciplines that share an interest in the modeling and analysis of timed systems. Typical topics include foundations and semantics, methods and tools, and applications. alternative_title: - LNCS citation: ama: Chatterjee K, Henzinger TA, eds. Formal Modeling and Analysis of Timed Systems. Vol 6246. Springer; 2010. doi:10.1007/978-3-642-15297-9 apa: 'Chatterjee, K., & Henzinger, T. A. (Eds.). (2010). Formal modeling and analysis of timed systems (Vol. 6246). Presented at the FORMATS: Formal Modeling and Analysis of Timed Systems, Klosterneuburg, Austria: Springer. https://doi.org/10.1007/978-3-642-15297-9' chicago: Chatterjee, Krishnendu, and Thomas A Henzinger, eds. Formal Modeling and Analysis of Timed Systems. Vol. 6246. Springer, 2010. https://doi.org/10.1007/978-3-642-15297-9. ieee: K. Chatterjee and T. A. Henzinger, Eds., Formal modeling and analysis of timed systems, vol. 6246. Springer, 2010. ista: Chatterjee K, Henzinger TA eds. 2010. Formal modeling and analysis of timed systems, Springer,p. mla: Chatterjee, Krishnendu, and Thomas A. Henzinger, editors. Formal Modeling and Analysis of Timed Systems. Vol. 6246, Springer, 2010, doi:10.1007/978-3-642-15297-9. short: K. Chatterjee, T.A. Henzinger, eds., Formal Modeling and Analysis of Timed Systems, Springer, 2010. conference: end_date: 2010-09-10 location: Klosterneuburg, Austria name: 'FORMATS: Formal Modeling and Analysis of Timed Systems' start_date: 2010-09-08 date_created: 2018-12-11T12:05:33Z date_published: 2010-09-20T00:00:00Z date_updated: 2019-11-14T08:42:42Z day: '20' department: - _id: KrCh - _id: ToHe doi: 10.1007/978-3-642-15297-9 editor: - 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 intvolume: ' 6246' language: - iso: eng month: '09' oa_version: None publication_status: published publisher: Springer publist_id: '2322' quality_controlled: '1' related_material: link: - description: eBook available via IST BookList relation: other url: https://koha.app.ist.ac.at/cgi-bin/koha/opac-detail.pl?biblionumber=12721 status: public title: Formal modeling and analysis of timed systems type: conference_editor user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 6246 year: '2010' ... --- _id: '3866' abstract: - lang: eng text: Systems ought to behave reasonably even in circumstances that are not anticipated in their specifications. We propose a definition of robustness for liveness specifications which prescribes, for any number of environment assumptions that are violated, a minimal number of system guarantees that must still be fulfilled. This notion of robustness can be formulated and realized using a Generalized Reactivity formula. We present an algorithm for synthesizing robust systems from such formulas. For the important special case of Generalized Reactivity formulas of rank 1, our algorithm improves the complexity of [PPS06] for large specifications with a small number of assumptions and guarantees. alternative_title: - LNCS author: - first_name: Roderick full_name: Bloem, Roderick last_name: Bloem - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Karin full_name: Greimel, Karin last_name: Greimel - 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: Barbara full_name: Jobstmann, Barbara last_name: Jobstmann citation: ama: 'Bloem R, Chatterjee K, Greimel K, Henzinger TA, Jobstmann B. Robustness in the presence of liveness. In: Touili T, Cook B, Jackson P, eds. Vol 6174. Springer; 2010:410-424. doi:10.1007/978-3-642-14295-6_36' apa: 'Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T. A., & Jobstmann, B. (2010). Robustness in the presence of liveness. In T. Touili, B. Cook, & P. Jackson (Eds.) (Vol. 6174, pp. 410–424). Presented at the CAV: Computer Aided Verification, Edinburgh, UK: Springer. https://doi.org/10.1007/978-3-642-14295-6_36' chicago: Bloem, Roderick, Krishnendu Chatterjee, Karin Greimel, Thomas A Henzinger, and Barbara Jobstmann. “Robustness in the Presence of Liveness.” edited by Tayssir Touili, Byron Cook, and Paul Jackson, 6174:410–24. Springer, 2010. https://doi.org/10.1007/978-3-642-14295-6_36. ieee: 'R. Bloem, K. Chatterjee, K. Greimel, T. A. Henzinger, and B. Jobstmann, “Robustness in the presence of liveness,” presented at the CAV: Computer Aided Verification, Edinburgh, UK, 2010, vol. 6174, pp. 410–424.' ista: 'Bloem R, Chatterjee K, Greimel K, Henzinger TA, Jobstmann B. 2010. Robustness in the presence of liveness. CAV: Computer Aided Verification, LNCS, vol. 6174, 410–424.' mla: Bloem, Roderick, et al. Robustness in the Presence of Liveness. Edited by Tayssir Touili et al., vol. 6174, Springer, 2010, pp. 410–24, doi:10.1007/978-3-642-14295-6_36. short: R. Bloem, K. Chatterjee, K. Greimel, T.A. Henzinger, B. Jobstmann, in:, T. Touili, B. Cook, P. Jackson (Eds.), Springer, 2010, pp. 410–424. conference: end_date: 2010-07-19 location: Edinburgh, UK name: 'CAV: Computer Aided Verification' start_date: 2010-07-15 date_created: 2018-12-11T12:05:36Z date_published: 2010-07-01T00:00:00Z date_updated: 2021-01-12T07:52:47Z day: '01' ddc: - '004' department: - _id: KrCh - _id: ToHe doi: 10.1007/978-3-642-14295-6_36 ec_funded: 1 editor: - first_name: Tayssir full_name: Touili, Tayssir last_name: Touili - first_name: Byron full_name: Cook, Byron last_name: Cook - first_name: Paul full_name: Jackson, Paul last_name: Jackson file: - access_level: open_access checksum: 9d204611c8d7855bed8134f8708a0010 content_type: application/pdf creator: system date_created: 2018-12-12T10:16:52Z date_updated: 2020-07-14T12:46:19Z file_id: '5243' file_name: IST-2012-54-v1+1_Robustness_in_the_presence_of_liveness.pdf file_size: 213083 relation: main_file file_date_updated: 2020-07-14T12:46:19Z has_accepted_license: '1' intvolume: ' 6174' language: - iso: eng month: '07' oa: 1 oa_version: Submitted Version page: 410 - 424 project: - _id: 25EFB36C-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '215543' name: COMponent-Based Embedded Systems design Techniques - _id: 25F1337C-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '214373' name: Design for Embedded Systems publication_status: published publisher: Springer publist_id: '2310' pubrep_id: '54' quality_controlled: '1' scopus_import: 1 status: public title: Robustness in the presence of liveness type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 6174 year: '2010' ... --- _id: '3868' abstract: - lang: eng text: Simulation and bisimulation metrics for stochastic systems provide a quantitative generalization of the classical simulation and bisimulation relations. These metrics capture the similarity of states with respect to quantitative specifications written in the quantitative mu-calculus and related probabilistic logics. We first show that the metrics provide a bound for the difference in long-run average and discounted average behavior across states, indicating that the metrics can be used both in system verification, and in performance evaluation. For turn-based games and MDPs, we provide a polynomial-time algorithm for the computation of the one-step metric distance between states. The algorithm is based on linear programming; it improves on the previous known exponential-time algorithm based on a reduction to the theory of reals. We then present PSPACE algorithms for both the decision problem and the problem of approximating the metric distance between two states, matching the best known algorithms for Markov chains. For the bisimulation kernel of the metric our algorithm works in time O(n(4)) for both turn-based games and MDPs; improving the previously best known O(n(9).log(n)) time algorithm for MDPs. For a concurrent game G, we show that computing the exact distance be tween states is at least as hard as computing the value of concurrent reachability games and the square-root-sum problem in computational geometry. We show that checking whether the metric distance is bounded by a rational r, can be done via a reduction to the theory of real closed fields, involving a formula with three quantifier alternations, yielding O(vertical bar G vertical bar(O(vertical bar G vertical bar 5))) time complexity, improving the previously known reduction, which yielded O(vertical bar G vertical bar(O(vertical bar G vertical bar 7))) time complexity. These algorithms can be iterated to approximate the metrics using binary search author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Luca full_name: De Alfaro, Luca last_name: De Alfaro - first_name: Ritankar full_name: Majumdar, Ritankar last_name: Majumdar - first_name: Vishwanath full_name: Raman, Vishwanath last_name: Raman citation: ama: Chatterjee K, De Alfaro L, Majumdar R, Raman V. Algorithms for game metrics. Logical Methods in Computer Science. 2010;6(3):1-27. doi:10.2168/LMCS-6(3:13)2010 apa: Chatterjee, K., De Alfaro, L., Majumdar, R., & Raman, V. (2010). Algorithms for game metrics. Logical Methods in Computer Science. International Federation of Computational Logic. https://doi.org/10.2168/LMCS-6(3:13)2010 chicago: Chatterjee, Krishnendu, Luca De Alfaro, Ritankar Majumdar, and Vishwanath Raman. “Algorithms for Game Metrics.” Logical Methods in Computer Science. International Federation of Computational Logic, 2010. https://doi.org/10.2168/LMCS-6(3:13)2010. ieee: K. Chatterjee, L. De Alfaro, R. Majumdar, and V. Raman, “Algorithms for game metrics,” Logical Methods in Computer Science, vol. 6, no. 3. International Federation of Computational Logic, pp. 1–27, 2010. ista: Chatterjee K, De Alfaro L, Majumdar R, Raman V. 2010. Algorithms for game metrics. Logical Methods in Computer Science. 6(3), 1–27. mla: Chatterjee, Krishnendu, et al. “Algorithms for Game Metrics.” Logical Methods in Computer Science, vol. 6, no. 3, International Federation of Computational Logic, 2010, pp. 1–27, doi:10.2168/LMCS-6(3:13)2010. short: K. Chatterjee, L. De Alfaro, R. Majumdar, V. Raman, Logical Methods in Computer Science 6 (2010) 1–27. date_created: 2018-12-11T12:05:36Z date_published: 2010-09-01T00:00:00Z date_updated: 2023-02-23T11:30:18Z day: '01' ddc: - '000' department: - _id: KrCh doi: 10.2168/LMCS-6(3:13)2010 file: - access_level: open_access checksum: a18988135fef3016c93808ecb15b55f5 content_type: application/pdf creator: system date_created: 2018-12-12T10:08:11Z date_updated: 2020-07-14T12:46:19Z file_id: '4671' file_name: IST-2015-370-v1+1_0809.4326.pdf file_size: 346527 relation: main_file file_date_updated: 2020-07-14T12:46:19Z has_accepted_license: '1' intvolume: ' 6' issue: '3' language: - iso: eng month: '09' oa: 1 oa_version: Published Version page: 1 - 27 publication: Logical Methods in Computer Science publication_status: published publisher: International Federation of Computational Logic publist_id: '2312' pubrep_id: '370' quality_controlled: '1' related_material: record: - id: '3504' relation: earlier_version status: public scopus_import: 1 status: public title: Algorithms for game metrics tmp: image: /image/cc_by_nd.png legal_code_url: https://creativecommons.org/licenses/by-nd/4.0/legalcode name: Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0) short: CC BY-ND (4.0) type: journal_article user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 6 year: '2010' ... --- _id: '3853' abstract: - lang: eng text: 'Quantitative languages are an extension of boolean languages that assign to each word a real number. Mean-payoff automata are finite automata with numerical weights on transitions that assign to each infinite path the long-run average of the transition weights. When the mode of branching of the automaton is deterministic, nondeterministic, or alternating, the corresponding class of quantitative languages is not robust as it is not closed under the pointwise operations of max, min, sum, and numerical complement. Nondeterministic and alternating mean-payoff automata are not decidable either, as the quantitative generalization of the problems of universality and language inclusion is undecidable. We introduce a new class of quantitative languages, defined by mean-payoff automaton expressions, which is robust and decidable: it is closed under the four pointwise operations, and we show that all decision problems are decidable for this class. Mean-payoff automaton expressions subsume deterministic meanpayoff automata, and we show that they have expressive power incomparable to nondeterministic and alternating mean-payoff automata. We also present for the first time an algorithm to compute distance between two quantitative languages, and in our case the quantitative languages are given as mean-payoff automaton expressions.' alternative_title: - LNCS author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Laurent full_name: Doyen, Laurent last_name: Doyen - first_name: Herbert full_name: Edelsbrunner, Herbert id: 3FB178DA-F248-11E8-B48F-1D18A9856A87 last_name: Edelsbrunner orcid: 0000-0002-9823-6833 - 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: Philippe full_name: Rannou, Philippe last_name: Rannou citation: ama: 'Chatterjee K, Doyen L, Edelsbrunner H, Henzinger TA, Rannou P. Mean-payoff automaton expressions. In: Vol 6269. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2010:269-283. doi:10.1007/978-3-642-15375-4_19' apa: 'Chatterjee, K., Doyen, L., Edelsbrunner, H., Henzinger, T. A., & Rannou, P. (2010). Mean-payoff automaton expressions (Vol. 6269, pp. 269–283). Presented at the CONCUR: Concurrency Theory, Paris, France: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/978-3-642-15375-4_19' chicago: Chatterjee, Krishnendu, Laurent Doyen, Herbert Edelsbrunner, Thomas A Henzinger, and Philippe Rannou. “Mean-Payoff Automaton Expressions,” 6269:269–83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010. https://doi.org/10.1007/978-3-642-15375-4_19. ieee: 'K. Chatterjee, L. Doyen, H. Edelsbrunner, T. A. Henzinger, and P. Rannou, “Mean-payoff automaton expressions,” presented at the CONCUR: Concurrency Theory, Paris, France, 2010, vol. 6269, pp. 269–283.' ista: 'Chatterjee K, Doyen L, Edelsbrunner H, Henzinger TA, Rannou P. 2010. Mean-payoff automaton expressions. CONCUR: Concurrency Theory, LNCS, vol. 6269, 269–283.' mla: Chatterjee, Krishnendu, et al. Mean-Payoff Automaton Expressions. Vol. 6269, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010, pp. 269–83, doi:10.1007/978-3-642-15375-4_19. short: K. Chatterjee, L. Doyen, H. Edelsbrunner, T.A. Henzinger, P. Rannou, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010, pp. 269–283. conference: end_date: 2010-09-03 location: Paris, France name: 'CONCUR: Concurrency Theory' start_date: 2010-08-31 date_created: 2018-12-11T12:05:31Z date_published: 2010-11-18T00:00:00Z date_updated: 2021-01-12T07:52:40Z day: '18' ddc: - '000' - '005' department: - _id: KrCh - _id: HeEd - _id: ToHe doi: 10.1007/978-3-642-15375-4_19 ec_funded: 1 file: - access_level: open_access checksum: 4f753ae99d076553fb8733e2c8b390e2 content_type: application/pdf creator: system date_created: 2018-12-12T10:15:41Z date_updated: 2020-07-14T12:46:17Z file_id: '5163' file_name: IST-2012-62-v1+1_Mean-payoff_automaton_expressions.pdf file_size: 233260 relation: main_file file_date_updated: 2020-07-14T12:46:17Z has_accepted_license: '1' intvolume: ' 6269' language: - iso: eng month: '11' oa: 1 oa_version: Submitted Version page: 269 - 283 project: - _id: 25EFB36C-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '215543' name: COMponent-Based Embedded Systems design Techniques - _id: 25F1337C-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '214373' name: Design for Embedded Systems publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik publist_id: '2328' pubrep_id: '62' quality_controlled: '1' scopus_import: 1 status: public title: Mean-payoff automaton expressions type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 6269 year: '2010' ... --- _id: '3854' abstract: - lang: eng text: 'Graph games of infinite length provide a natural model for open reactive systems: one player (Eve) represents the controller and the other player (Adam) represents the environment. The evolution of the system depends on the decisions of both players. The specification for the system is usually given as an ω-regular language L over paths and Eve’s goal is to ensure that the play belongs to L irrespective of Adam’s behaviour. The classical notion of winning strategies fails to capture several interesting scenarios. For example, strong fairness (Streett) conditions are specified by a number of request-grant pairs and require every pair that is requested infinitely often to be granted infinitely often: Eve might win just by preventing Adam from making any new request, but a “better” strategy would allow Adam to make as many requests as possible and still ensure fairness. To address such questions, we introduce the notion of obliging games, where Eve has to ensure a strong condition Φ, while always allowing Adam to satisfy a weak condition Ψ. We present a linear time reduction of obliging games with two Muller conditions Φ and Ψ to classical Muller games. We consider obliging Streett games and show they are co-NP complete, and show a natural quantitative optimisation problem for obliging Streett games is in FNP. We also show how obliging games can provide new and interesting semantics for multi-player games.' alternative_title: - LNCS author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Florian full_name: Horn, Florian id: 37327ACE-F248-11E8-B48F-1D18A9856A87 last_name: Horn - first_name: Christof full_name: Löding, Christof last_name: Löding citation: ama: 'Chatterjee K, Horn F, Löding C. Obliging games. In: Vol 6269. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2010:284-296. doi:10.1007/978-3-642-15375-4_20' apa: 'Chatterjee, K., Horn, F., & Löding, C. (2010). Obliging games (Vol. 6269, pp. 284–296). Presented at the CONCUR: Concurrency Theory, Paris, France: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/978-3-642-15375-4_20' chicago: Chatterjee, Krishnendu, Florian Horn, and Christof Löding. “Obliging Games,” 6269:284–96. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010. https://doi.org/10.1007/978-3-642-15375-4_20. ieee: 'K. Chatterjee, F. Horn, and C. Löding, “Obliging games,” presented at the CONCUR: Concurrency Theory, Paris, France, 2010, vol. 6269, pp. 284–296.' ista: 'Chatterjee K, Horn F, Löding C. 2010. Obliging games. CONCUR: Concurrency Theory, LNCS, vol. 6269, 284–296.' mla: Chatterjee, Krishnendu, et al. Obliging Games. Vol. 6269, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010, pp. 284–96, doi:10.1007/978-3-642-15375-4_20. short: K. Chatterjee, F. Horn, C. Löding, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010, pp. 284–296. conference: end_date: 2010-09-03 location: Paris, France name: 'CONCUR: Concurrency Theory' start_date: 2010-08-31 date_created: 2018-12-11T12:05:32Z date_published: 2010-09-08T00:00:00Z date_updated: 2021-01-12T07:52:41Z day: '08' department: - _id: KrCh doi: 10.1007/978-3-642-15375-4_20 intvolume: ' 6269' language: - iso: eng month: '09' oa_version: None page: 284 - 296 publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik publist_id: '2327' quality_controlled: '1' scopus_import: 1 status: public title: Obliging games type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 6269 year: '2010' ... --- _id: '3851' abstract: - lang: eng text: 'Energy parity games are infinite two-player turn-based games played on weighted graphs. The objective of the game combines a (qualitative) parity condition with the (quantitative) requirement that the sum of the weights (i.e., the level of energy in the game) must remain positive. Beside their own interest in the design and synthesis of resource-constrained omega-regular specifications, energy parity games provide one of the simplest model of games with combined qualitative and quantitative objective. Our main results are as follows: (a) exponential memory is sufficient and may be necessary for winning strategies in energy parity games; (b) the problem of deciding the winner in energy parity games can be solved in NP ∩ coNP; and (c) we give an algorithm to solve energy parity by reduction to energy games. We also show that the problem of deciding the winner in energy parity games is polynomially equivalent to the problem of deciding the winner in mean-payoff parity games, which can thus be solved in NP ∩ coNP. As a consequence we also obtain a conceptually simple algorithm to solve mean-payoff parity games.' alternative_title: - LNCS author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Laurent full_name: Doyen, Laurent last_name: Doyen citation: ama: 'Chatterjee K, Doyen L. Energy parity games. In: Vol 6199. Springer; 2010:599-610. doi:10.1007/978-3-642-14162-1_50' apa: 'Chatterjee, K., & Doyen, L. (2010). Energy parity games (Vol. 6199, pp. 599–610). Presented at the ICALP: Automata, Languages and Programming, 37th International Colloquium, Bordeaux, France: Springer. https://doi.org/10.1007/978-3-642-14162-1_50' chicago: Chatterjee, Krishnendu, and Laurent Doyen. “Energy Parity Games,” 6199:599–610. Springer, 2010. https://doi.org/10.1007/978-3-642-14162-1_50. ieee: 'K. Chatterjee and L. Doyen, “Energy parity games,” presented at the ICALP: Automata, Languages and Programming, 37th International Colloquium, Bordeaux, France, 2010, vol. 6199, pp. 599–610.' ista: 'Chatterjee K, Doyen L. 2010. Energy parity games. ICALP: Automata, Languages and Programming, 37th International Colloquium, LNCS, vol. 6199, 599–610.' mla: Chatterjee, Krishnendu, and Laurent Doyen. Energy Parity Games. Vol. 6199, Springer, 2010, pp. 599–610, doi:10.1007/978-3-642-14162-1_50. short: K. Chatterjee, L. Doyen, in:, Springer, 2010, pp. 599–610. conference: end_date: 2010-07-10 location: Bordeaux, France name: ' ICALP: Automata, Languages and Programming, 37th International Colloquium' start_date: 2010-07-06 date_created: 2018-12-11T12:05:31Z date_published: 2010-09-10T00:00:00Z date_updated: 2023-02-23T11:06:35Z day: '10' department: - _id: KrCh doi: 10.1007/978-3-642-14162-1_50 external_id: arxiv: - '1001.5183' intvolume: ' 6199' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1001.5183 month: '09' oa: 1 oa_version: Preprint page: 599 - 610 publication_status: published publisher: Springer publist_id: '2330' quality_controlled: '1' related_material: record: - id: '2972' relation: later_version status: public scopus_import: 1 status: public title: Energy parity games type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 6199 year: '2010' ... --- _id: '3860' abstract: - lang: eng text: 'In mean-payoff games, the objective of the protagonist is to ensure that the limit average of an infinite sequence of numeric weights is nonnegative. In energy games, the objective is to ensure that the running sum of weights is always nonnegative. Generalized mean-payoff and energy games replace individual weights by tuples, and the limit average (resp. running sum) of each coordinate must be (resp. remain) nonnegative. These games have applications in the synthesis of resource-bounded processes with multiple resources. We prove the finite-memory determinacy of generalized energy games and show the inter- reducibility of generalized mean-payoff and energy games for finite-memory strategies. We also improve the computational complexity for solving both classes of games with finite-memory strategies: while the previously best known upper bound was EXPSPACE, and no lower bound was known, we give an optimal coNP-complete bound. For memoryless strategies, we show that the problem of deciding the existence of a winning strategy for the protagonist is NP-complete.' alternative_title: - LIPIcs article_processing_charge: No author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Laurent full_name: Doyen, Laurent last_name: Doyen - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Jean full_name: Raskin, Jean last_name: Raskin citation: ama: 'Chatterjee K, Doyen L, Henzinger TA, Raskin J. Generalized mean-payoff and energy games. In: Vol 8. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2010:505-516. doi:10.4230/LIPIcs.FSTTCS.2010.505' apa: 'Chatterjee, K., Doyen, L., Henzinger, T. A., & Raskin, J. (2010). Generalized mean-payoff and energy games (Vol. 8, pp. 505–516). Presented at the FSTTCS: Foundations of Software Technology and Theoretical Computer Science, Chennai, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.FSTTCS.2010.505' chicago: Chatterjee, Krishnendu, Laurent Doyen, Thomas A Henzinger, and Jean Raskin. “Generalized Mean-Payoff and Energy Games,” 8:505–16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010. https://doi.org/10.4230/LIPIcs.FSTTCS.2010.505. ieee: 'K. Chatterjee, L. Doyen, T. A. Henzinger, and J. Raskin, “Generalized mean-payoff and energy games,” presented at the FSTTCS: Foundations of Software Technology and Theoretical Computer Science, Chennai, India, 2010, vol. 8, pp. 505–516.' ista: 'Chatterjee K, Doyen L, Henzinger TA, Raskin J. 2010. Generalized mean-payoff and energy games. FSTTCS: Foundations of Software Technology and Theoretical Computer Science, LIPIcs, vol. 8, 505–516.' mla: Chatterjee, Krishnendu, et al. Generalized Mean-Payoff and Energy Games. Vol. 8, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010, pp. 505–16, doi:10.4230/LIPIcs.FSTTCS.2010.505. short: K. Chatterjee, L. Doyen, T.A. Henzinger, J. Raskin, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010, pp. 505–516. conference: end_date: 2010-12-18 location: Chennai, India name: 'FSTTCS: Foundations of Software Technology and Theoretical Computer Science' start_date: 2010-12-15 date_created: 2018-12-11T12:05:34Z date_published: 2010-12-13T00:00:00Z date_updated: 2021-01-12T07:52:44Z day: '13' ddc: - '005' department: - _id: KrCh - _id: ToHe doi: 10.4230/LIPIcs.FSTTCS.2010.505 file: - access_level: open_access checksum: 1caabd6319b979927208117a41192637 content_type: application/pdf creator: system date_created: 2018-12-12T10:15:27Z date_updated: 2020-07-14T12:46:18Z file_id: '5147' file_name: IST-2012-59-v1+1_Generalized_mean-payoff_and_energy_games.pdf file_size: 178278 relation: main_file - access_level: open_access checksum: 3a59759ceeacdb5b578f3803d5e6769b content_type: application/pdf creator: system date_created: 2018-12-12T10:15:28Z date_updated: 2020-07-14T12:46:18Z file_id: '5148' file_name: IST-2016-59-v2+1_2_1_.pdf file_size: 477976 relation: main_file file_date_updated: 2020-07-14T12:46:18Z has_accepted_license: '1' intvolume: ' 8' language: - iso: eng month: '12' oa: 1 oa_version: Submitted Version page: 505 - 516 publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik publist_id: '2321' pubrep_id: '59' quality_controlled: '1' scopus_import: 1 status: public title: Generalized mean-payoff and energy games tmp: image: /images/cc_by_nc_nd.png legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0) short: CC BY-NC-ND (4.0) type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 8 year: '2010' ...