--- _id: '466' abstract: - lang: eng text: 'We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. There exist two different views: (i) the expectation semantics, where the goal is to optimize the expected mean-payoff objective, and (ii) the satisfaction semantics, where the goal is to maximize the probability of runs such that the mean-payoff value stays above a given vector. We consider optimization with respect to both objectives at once, thus unifying the existing semantics. Precisely, the goal is to optimize the expectation while ensuring the satisfaction constraint. Our problem captures the notion of optimization with respect to strategies that are risk-averse (i.e., ensure certain probabilistic guarantee). Our main results are as follows: First, we present algorithms for the decision problems which are always polynomial in the size of the MDP. We also show that an approximation of the Pareto-curve can be computed in time polynomial in the size of the MDP, and the approximation factor, but exponential in the number of dimensions. Second, we present a complete characterization of the strategy complexity (in terms of memory bounds and randomization) required to solve our problem. ' article_number: '15' author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Zuzana full_name: Křetínská, Zuzana last_name: Křetínská - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 citation: ama: Chatterjee K, Křetínská Z, Kretinsky J. Unifying two views on multiple mean-payoff objectives in Markov decision processes. Logical Methods in Computer Science. 2017;13(2). doi:10.23638/LMCS-13(2:15)2017 apa: Chatterjee, K., Křetínská, Z., & Kretinsky, J. (2017). Unifying two views on multiple mean-payoff objectives in Markov decision processes. Logical Methods in Computer Science. International Federation of Computational Logic. https://doi.org/10.23638/LMCS-13(2:15)2017 chicago: Chatterjee, Krishnendu, Zuzana Křetínská, and Jan Kretinsky. “Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.” Logical Methods in Computer Science. International Federation of Computational Logic, 2017. https://doi.org/10.23638/LMCS-13(2:15)2017. ieee: K. Chatterjee, Z. Křetínská, and J. Kretinsky, “Unifying two views on multiple mean-payoff objectives in Markov decision processes,” Logical Methods in Computer Science, vol. 13, no. 2. International Federation of Computational Logic, 2017. ista: Chatterjee K, Křetínská Z, Kretinsky J. 2017. Unifying two views on multiple mean-payoff objectives in Markov decision processes. Logical Methods in Computer Science. 13(2), 15. mla: Chatterjee, Krishnendu, et al. “Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.” Logical Methods in Computer Science, vol. 13, no. 2, 15, International Federation of Computational Logic, 2017, doi:10.23638/LMCS-13(2:15)2017. short: K. Chatterjee, Z. Křetínská, J. Kretinsky, Logical Methods in Computer Science 13 (2017). date_created: 2018-12-11T11:46:38Z date_published: 2017-07-03T00:00:00Z date_updated: 2023-02-23T12:26:16Z day: '03' ddc: - '004' department: - _id: KrCh doi: 10.23638/LMCS-13(2:15)2017 ec_funded: 1 file: - access_level: open_access checksum: bfa405385ec6229ad5ead89ab5751639 content_type: application/pdf creator: system date_created: 2018-12-12T10:18:32Z date_updated: 2020-07-14T12:46:33Z file_id: '5354' file_name: IST-2018-957-v1+1_2017_Chatterjee_Unifying_two.pdf file_size: 511832 relation: main_file file_date_updated: 2020-07-14T12:46:33Z has_accepted_license: '1' intvolume: ' 13' issue: '2' language: - iso: eng license: https://creativecommons.org/licenses/by-nd/4.0/ month: '07' oa: 1 oa_version: Published Version project: - _id: 25681D80-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '291734' name: International IST Postdoc Fellowship Programme - _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: 2590DB08-B435-11E9-9278-68D0E5697425 call_identifier: H2020 grant_number: '701309' name: Atomic-Resolution Structures of Mitochondrial Respiratory Chain Supercomplexes (H2020) publication: Logical Methods in Computer Science publication_identifier: issn: - '18605974' publication_status: published publisher: International Federation of Computational Logic publist_id: '7355' pubrep_id: '957' quality_controlled: '1' related_material: record: - id: '1657' relation: earlier_version status: public - id: '5429' relation: earlier_version status: public - id: '5435' relation: earlier_version status: public scopus_import: 1 status: public title: Unifying two views on multiple mean-payoff objectives in Markov decision processes 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: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 13 year: '2017' ... --- _id: '465' abstract: - lang: eng text: 'The edit distance between two words w 1 , w 2 is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform w 1 to w 2 . The edit distance generalizes to languages L 1 , L 2 , where the edit distance from L 1 to L 2 is the minimal number k such that for every word from L 1 there exists a word in L 2 with edit distance at most k . We study the edit distance computation problem between pushdown automata and their subclasses. The problem of computing edit distance to a pushdown automaton is undecidable, and in practice, the interesting question is to compute the edit distance from a pushdown automaton (the implementation, a standard model for programs with recursion) to a regular language (the specification). In this work, we present a complete picture of decidability and complexity for the following problems: (1) deciding whether, for a given threshold k , the edit distance from a pushdown automaton to a finite automaton is at most k , and (2) deciding whether the edit distance from a pushdown automaton to a finite automaton is finite. ' author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Rasmus full_name: Ibsen-Jensen, Rasmus id: 3B699956-F248-11E8-B48F-1D18A9856A87 last_name: Ibsen-Jensen orcid: 0000-0003-4783-0389 - first_name: Jan full_name: Otop, Jan last_name: Otop citation: ama: Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. Edit distance for pushdown automata. Logical Methods in Computer Science. 2017;13(3). doi:10.23638/LMCS-13(3:23)2017 apa: Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., & Otop, J. (2017). Edit distance for pushdown automata. Logical Methods in Computer Science. International Federation of Computational Logic. https://doi.org/10.23638/LMCS-13(3:23)2017 chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan Otop. “Edit Distance for Pushdown Automata.” Logical Methods in Computer Science. International Federation of Computational Logic, 2017. https://doi.org/10.23638/LMCS-13(3:23)2017. ieee: K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, “Edit distance for pushdown automata,” Logical Methods in Computer Science, vol. 13, no. 3. International Federation of Computational Logic, 2017. ista: Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2017. Edit distance for pushdown automata. Logical Methods in Computer Science. 13(3). mla: Chatterjee, Krishnendu, et al. “Edit Distance for Pushdown Automata.” Logical Methods in Computer Science, vol. 13, no. 3, International Federation of Computational Logic, 2017, doi:10.23638/LMCS-13(3:23)2017. short: K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, Logical Methods in Computer Science 13 (2017). date_created: 2018-12-11T11:46:37Z date_published: 2017-09-13T00:00:00Z date_updated: 2023-02-23T12:26:25Z day: '13' ddc: - '004' department: - _id: KrCh - _id: ToHe doi: 10.23638/LMCS-13(3:23)2017 ec_funded: 1 file: - access_level: open_access checksum: 08041379ba408d40664f449eb5907a8f content_type: application/pdf creator: system date_created: 2018-12-12T10:14:37Z date_updated: 2020-07-14T12:46:33Z file_id: '5090' file_name: IST-2015-321-v1+1_main.pdf file_size: 279071 relation: main_file - access_level: open_access checksum: 08041379ba408d40664f449eb5907a8f content_type: application/pdf creator: system date_created: 2018-12-12T10:14:38Z date_updated: 2020-07-14T12:46:33Z file_id: '5091' file_name: IST-2018-955-v1+1_2017_Chatterjee_Edit_distance.pdf file_size: 279071 relation: main_file file_date_updated: 2020-07-14T12:46:33Z has_accepted_license: '1' intvolume: ' 13' issue: '3' language: - iso: eng month: '09' oa: 1 oa_version: Published Version project: - _id: 25F5A88A-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Moderne Concurrency Paradigms - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25F42A32-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: Z211 name: The Wittgenstein Prize - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory publication: Logical Methods in Computer Science publication_identifier: issn: - '18605974' publication_status: published publisher: International Federation of Computational Logic publist_id: '7356' pubrep_id: '955' quality_controlled: '1' related_material: record: - id: '1610' relation: earlier_version status: public - id: '5438' relation: earlier_version status: public scopus_import: 1 status: public title: Edit distance for pushdown automata 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: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 13 year: '2017' ... --- _id: '2233' abstract: - lang: eng text: ' A discounted-sum automaton (NDA) is a nondeterministic finite automaton with edge weights, valuing a run by the discounted sum of visited edge weights. More precisely, the weight in the i-th position of the run is divided by λi, where the discount factor λ is a fixed rational number greater than 1. The value of a word is the minimal value of the automaton runs on it. Discounted summation is a common and useful measuring scheme, especially for infinite sequences, reflecting the assumption that earlier weights are more important than later weights. Unfortunately, determinization of NDAs, which is often essential in formal verification, is, in general, not possible. We provide positive news, showing that every NDA with an integral discount factor is determinizable. We complete the picture by proving that the integers characterize exactly the discount factors that guarantee determinizability: for every nonintegral rational discount factor λ, there is a nondeterminizable λ-NDA. We also prove that the class of NDAs with integral discount factors enjoys closure under the algebraic operations min, max, addition, and subtraction, which is not the case for general NDAs nor for deterministic NDAs. For general NDAs, we look into approximate determinization, which is always possible as the influence of a word''s suffix decays. We show that the naive approach, of unfolding the automaton computations up to a sufficient level, is doubly exponential in the discount factor. We provide an alternative construction for approximate determinization, which is singly exponential in the discount factor, in the precision, and in the number of states. We also prove matching lower bounds, showing that the exponential dependency on each of these three parameters cannot be avoided. All our results hold equally for automata over finite words and for automata over infinite words. ' author: - first_name: Udi full_name: Boker, Udi last_name: Boker - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 citation: ama: Boker U, Henzinger TA. Exact and approximate determinization of discounted-sum automata. Logical Methods in Computer Science. 2014;10(1). doi:10.2168/LMCS-10(1:10)2014 apa: Boker, U., & Henzinger, T. A. (2014). Exact and approximate determinization of discounted-sum automata. Logical Methods in Computer Science. International Federation of Computational Logic. https://doi.org/10.2168/LMCS-10(1:10)2014 chicago: Boker, Udi, and Thomas A Henzinger. “Exact and Approximate Determinization of Discounted-Sum Automata.” Logical Methods in Computer Science. International Federation of Computational Logic, 2014. https://doi.org/10.2168/LMCS-10(1:10)2014. ieee: U. Boker and T. A. Henzinger, “Exact and approximate determinization of discounted-sum automata,” Logical Methods in Computer Science, vol. 10, no. 1. International Federation of Computational Logic, 2014. ista: Boker U, Henzinger TA. 2014. Exact and approximate determinization of discounted-sum automata. Logical Methods in Computer Science. 10(1). mla: Boker, Udi, and Thomas A. Henzinger. “Exact and Approximate Determinization of Discounted-Sum Automata.” Logical Methods in Computer Science, vol. 10, no. 1, International Federation of Computational Logic, 2014, doi:10.2168/LMCS-10(1:10)2014. short: U. Boker, T.A. Henzinger, Logical Methods in Computer Science 10 (2014). date_created: 2018-12-11T11:56:28Z date_published: 2014-02-13T00:00:00Z date_updated: 2021-01-12T06:56:11Z day: '13' ddc: - '000' department: - _id: ToHe doi: 10.2168/LMCS-10(1:10)2014 ec_funded: 1 file: - access_level: open_access checksum: 9f6ea2e2d8d4a32ff0becc29d835bbf8 content_type: application/pdf creator: system date_created: 2018-12-12T10:07:45Z date_updated: 2020-07-14T12:45:34Z file_id: '4643' file_name: IST-2015-389-v1+1_1401.3957.pdf file_size: 550936 relation: main_file file_date_updated: 2020-07-14T12:45:34Z has_accepted_license: '1' intvolume: ' 10' issue: '1' language: - iso: eng month: '02' oa: 1 oa_version: Published Version project: - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling publication: Logical Methods in Computer Science publication_identifier: issn: - '18605974' publication_status: published publisher: International Federation of Computational Logic publist_id: '4728' pubrep_id: '389' quality_controlled: '1' scopus_import: 1 status: public title: Exact and approximate determinization of discounted-sum automata tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 10 year: '2014' ... --- _id: '2234' 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 κ limit-average 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 case of one limit-average function, both randomization and memory are necessary for strategies even for ε-approximation, and that finite-memory randomized strategies are sufficient for achieving Pareto optimal values. Under the satisfaction objective, in contrast to the case of one limit-average function, infinite memory is necessary for strategies achieving a specific value (i.e. randomized finite-memory strategies are not sufficient), whereas memoryless randomized strategies are sufficient for ε-approximation, for all ε > 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 ε-approximated in time polynomial in the size of the MDP and 1/ε, and exponential in the number of limit-average functions, for all ε > 0. Our analysis also reveals flaws in previous work for MDPs with multiple mean-payoff functions under the expectation objective, corrects the flaws, and allows us to obtain improved results. 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. Markov decision processes with multiple long-run average objectives. Logical Methods in Computer Science. 2014;10(1). doi:10.2168/LMCS-10(1:13)2014 apa: Brázdil, T., Brožek, V., Chatterjee, K., Forejt, V., & Kučera, A. (2014). Markov decision processes with multiple long-run average objectives. Logical Methods in Computer Science. International Federation of Computational Logic. https://doi.org/10.2168/LMCS-10(1:13)2014 chicago: Brázdil, Tomáš, Václav Brožek, Krishnendu Chatterjee, Vojtěch Forejt, and Antonín Kučera. “Markov Decision Processes with Multiple Long-Run Average Objectives.” Logical Methods in Computer Science. International Federation of Computational Logic, 2014. https://doi.org/10.2168/LMCS-10(1:13)2014. ieee: T. Brázdil, V. Brožek, K. Chatterjee, V. Forejt, and A. Kučera, “Markov decision processes with multiple long-run average objectives,” Logical Methods in Computer Science, vol. 10, no. 1. International Federation of Computational Logic, 2014. ista: Brázdil T, Brožek V, Chatterjee K, Forejt V, Kučera A. 2014. Markov decision processes with multiple long-run average objectives. Logical Methods in Computer Science. 10(1). mla: Brázdil, Tomáš, et al. “Markov Decision Processes with Multiple Long-Run Average Objectives.” Logical Methods in Computer Science, vol. 10, no. 1, International Federation of Computational Logic, 2014, doi:10.2168/LMCS-10(1:13)2014. short: T. Brázdil, V. Brožek, K. Chatterjee, V. Forejt, A. Kučera, Logical Methods in Computer Science 10 (2014). date_created: 2018-12-11T11:56:29Z date_published: 2014-02-14T00:00:00Z date_updated: 2021-01-12T06:56:11Z day: '14' ddc: - '000' department: - _id: KrCh doi: 10.2168/LMCS-10(1:13)2014 ec_funded: 1 file: - access_level: open_access checksum: 803edcc2d8c1acfba44a9ec43a5eb9f0 content_type: application/pdf creator: system date_created: 2018-12-12T10:07:57Z date_updated: 2020-07-14T12:45:34Z file_id: '4656' file_name: IST-2016-428-v1+1_1104.3489.pdf file_size: 375388 relation: main_file file_date_updated: 2020-07-14T12:45:34Z has_accepted_license: '1' intvolume: ' 10' issue: '1' language: - iso: eng main_file_link: - open_access: '1' url: http://repository.ist.ac.at/id/eprint/428 month: '02' oa: 1 oa_version: Published Version project: - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: Logical Methods in Computer Science publication_identifier: issn: - '18605974' publication_status: published publisher: International Federation of Computational Logic publist_id: '4727' pubrep_id: '428' quality_controlled: '1' scopus_import: 1 status: public title: Markov decision processes with multiple long-run average objectives tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 10 year: '2014' ...