--- _id: '2187' abstract: - lang: eng text: 'Systems should not only be correct but also robust in the sense that they behave reasonably in unexpected situations. This article addresses synthesis of robust reactive systems from temporal specifications. Existing methods allow arbitrary behavior if assumptions in the specification are violated. To overcome this, we define two robustness notions, combine them, and show how to enforce them in synthesis. The first notion applies to safety properties: If safety assumptions are violated temporarily, we require that the system recovers to normal operation with as few errors as possible. The second notion requires that, if liveness assumptions are violated, as many guarantees as possible should be fulfilled nevertheless. We present a synthesis procedure achieving this for the important class of GR(1) specifications, and establish complexity bounds. We also present an implementation of a special case of robustness, and show experimental results.' article_processing_charge: No article_type: original 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: Georg full_name: Hofferek, Georg last_name: Hofferek - first_name: Barbara full_name: Jobstmann, Barbara last_name: Jobstmann - first_name: Bettina full_name: Könighofer, Bettina last_name: Könighofer - first_name: Robert full_name: Könighofer, Robert last_name: Könighofer citation: ama: Bloem R, Chatterjee K, Greimel K, et al. Synthesizing robust systems. Acta Informatica. 2014;51(3-4):193-220. doi:10.1007/s00236-013-0191-5 apa: Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T. A., Hofferek, G., Jobstmann, B., … Könighofer, R. (2014). Synthesizing robust systems. Acta Informatica. Springer. https://doi.org/10.1007/s00236-013-0191-5 chicago: Bloem, Roderick, Krishnendu Chatterjee, Karin Greimel, Thomas A Henzinger, Georg Hofferek, Barbara Jobstmann, Bettina Könighofer, and Robert Könighofer. “Synthesizing Robust Systems.” Acta Informatica. Springer, 2014. https://doi.org/10.1007/s00236-013-0191-5. ieee: R. Bloem et al., “Synthesizing robust systems,” Acta Informatica, vol. 51, no. 3–4. Springer, pp. 193–220, 2014. ista: Bloem R, Chatterjee K, Greimel K, Henzinger TA, Hofferek G, Jobstmann B, Könighofer B, Könighofer R. 2014. Synthesizing robust systems. Acta Informatica. 51(3–4), 193–220. mla: Bloem, Roderick, et al. “Synthesizing Robust Systems.” Acta Informatica, vol. 51, no. 3–4, Springer, 2014, pp. 193–220, doi:10.1007/s00236-013-0191-5. short: R. Bloem, K. Chatterjee, K. Greimel, T.A. Henzinger, G. Hofferek, B. Jobstmann, B. Könighofer, R. Könighofer, Acta Informatica 51 (2014) 193–220. date_created: 2018-12-11T11:56:13Z date_published: 2014-06-01T00:00:00Z date_updated: 2021-01-12T06:55:51Z day: '01' ddc: - '621' department: - _id: KrCh - _id: ToHe doi: 10.1007/s00236-013-0191-5 ec_funded: 1 file: - access_level: open_access checksum: d7f560f3d923f0f00aa10a0652f83273 content_type: application/pdf creator: system date_created: 2018-12-12T10:16:44Z date_updated: 2020-07-14T12:45:31Z file_id: '5234' file_name: IST-2012-71-v1+1_Synthesizing_robust_systems.pdf file_size: 169523 relation: main_file file_date_updated: 2020-07-14T12:45:31Z has_accepted_license: '1' intvolume: ' 51' issue: 3-4 language: - iso: eng month: '06' oa: 1 oa_version: Submitted Version page: 193 - 220 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: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling publication: Acta Informatica publication_status: published publisher: Springer publist_id: '4787' pubrep_id: '71' quality_controlled: '1' scopus_import: 1 status: public title: Synthesizing robust systems type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 51 year: '2014' ... --- _id: '2190' abstract: - lang: eng text: We present a new algorithm to construct a (generalized) deterministic Rabin automaton for an LTL formula φ. The automaton is the product of a master automaton and an array of slave automata, one for each G-subformula of φ. The slave automaton for G ψ is in charge of recognizing whether FG ψ holds. As opposed to standard determinization procedures, the states of all our automata have a clear logical structure, which allows for various optimizations. Our construction subsumes former algorithms for fragments of LTL. Experimental results show improvement in the sizes of the resulting automata compared to existing methods. acknowledgement: The author is on leave from Faculty of Informatics, Masaryk University, Czech Republic, and partially supported by the Czech Science Foundation, grant No. P202/12/G061. alternative_title: - LNCS author: - first_name: Javier full_name: Esparza, Javier last_name: Esparza - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 citation: ama: 'Esparza J, Kretinsky J. From LTL to deterministic automata: A safraless compositional approach. In: Vol 8559. Springer; 2014:192-208. doi:10.1007/978-3-319-08867-9_13' apa: 'Esparza, J., & Kretinsky, J. (2014). From LTL to deterministic automata: A safraless compositional approach (Vol. 8559, pp. 192–208). Presented at the CAV: Computer Aided Verification, Springer. https://doi.org/10.1007/978-3-319-08867-9_13' chicago: 'Esparza, Javier, and Jan Kretinsky. “From LTL to Deterministic Automata: A Safraless Compositional Approach,” 8559:192–208. Springer, 2014. https://doi.org/10.1007/978-3-319-08867-9_13.' ieee: 'J. Esparza and J. Kretinsky, “From LTL to deterministic automata: A safraless compositional approach,” presented at the CAV: Computer Aided Verification, 2014, vol. 8559, pp. 192–208.' ista: 'Esparza J, Kretinsky J. 2014. From LTL to deterministic automata: A safraless compositional approach. CAV: Computer Aided Verification, LNCS, vol. 8559, 192–208.' mla: 'Esparza, Javier, and Jan Kretinsky. From LTL to Deterministic Automata: A Safraless Compositional Approach. Vol. 8559, Springer, 2014, pp. 192–208, doi:10.1007/978-3-319-08867-9_13.' short: J. Esparza, J. Kretinsky, in:, Springer, 2014, pp. 192–208. conference: name: 'CAV: Computer Aided Verification' date_created: 2018-12-11T11:56:14Z date_published: 2014-01-01T00:00:00Z date_updated: 2021-01-12T06:55:53Z day: '01' department: - _id: ToHe - _id: KrCh doi: 10.1007/978-3-319-08867-9_13 ec_funded: 1 intvolume: ' 8559' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1402.3388 month: '01' oa: 1 oa_version: Submitted Version page: 192 - 208 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 publication_status: published publisher: Springer publist_id: '4784' quality_controlled: '1' status: public title: 'From LTL to deterministic automata: A safraless compositional approach' type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 8559 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 license: https://creativecommons.org/licenses/by/4.0/ 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' ... --- _id: '2246' abstract: - lang: eng text: 'Muller games are played by two players moving a token along a graph; the winner is determined by the set of vertices that occur infinitely often. The central algorithmic problem is to compute the winning regions for the players. Different classes and representations of Muller games lead to problems of varying computational complexity. One such class are parity games; these are of particular significance in computational complexity, as they remain one of the few combinatorial problems known to be in NP ∩ co-NP but not known to be in P. We show that winning regions for a Muller game can be determined from the alternating structure of its traps. To every Muller game we then associate a natural number that we call its trap depth; this parameter measures how complicated the trap structure is. We present algorithms for parity games that run in polynomial time for graphs of bounded trap depth, and in general run in time exponential in the trap depth. ' author: - first_name: Andrey full_name: Grinshpun, Andrey last_name: Grinshpun - first_name: Pakawat full_name: Phalitnonkiat, Pakawat last_name: Phalitnonkiat - first_name: Sasha full_name: Rubin, Sasha id: 2EC51194-F248-11E8-B48F-1D18A9856A87 last_name: Rubin - first_name: Andrei full_name: Tarfulea, Andrei last_name: Tarfulea citation: ama: Grinshpun A, Phalitnonkiat P, Rubin S, Tarfulea A. Alternating traps in Muller and parity games. Theoretical Computer Science. 2014;521:73-91. doi:10.1016/j.tcs.2013.11.032 apa: Grinshpun, A., Phalitnonkiat, P., Rubin, S., & Tarfulea, A. (2014). Alternating traps in Muller and parity games. Theoretical Computer Science. Elsevier. https://doi.org/10.1016/j.tcs.2013.11.032 chicago: Grinshpun, Andrey, Pakawat Phalitnonkiat, Sasha Rubin, and Andrei Tarfulea. “Alternating Traps in Muller and Parity Games.” Theoretical Computer Science. Elsevier, 2014. https://doi.org/10.1016/j.tcs.2013.11.032. ieee: A. Grinshpun, P. Phalitnonkiat, S. Rubin, and A. Tarfulea, “Alternating traps in Muller and parity games,” Theoretical Computer Science, vol. 521. Elsevier, pp. 73–91, 2014. ista: Grinshpun A, Phalitnonkiat P, Rubin S, Tarfulea A. 2014. Alternating traps in Muller and parity games. Theoretical Computer Science. 521, 73–91. mla: Grinshpun, Andrey, et al. “Alternating Traps in Muller and Parity Games.” Theoretical Computer Science, vol. 521, Elsevier, 2014, pp. 73–91, doi:10.1016/j.tcs.2013.11.032. short: A. Grinshpun, P. Phalitnonkiat, S. Rubin, A. Tarfulea, Theoretical Computer Science 521 (2014) 73–91. date_created: 2018-12-11T11:56:33Z date_published: 2014-02-13T00:00:00Z date_updated: 2021-01-12T06:56:16Z day: '13' department: - _id: KrCh doi: 10.1016/j.tcs.2013.11.032 intvolume: ' 521' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1303.3777 month: '02' oa: 1 oa_version: Submitted Version page: 73 - 91 publication: Theoretical Computer Science publication_identifier: issn: - '03043975' publication_status: published publisher: Elsevier publist_id: '4703' quality_controlled: '1' scopus_import: 1 status: public title: Alternating traps in Muller and parity games type: journal_article user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 521 year: '2014' ... --- _id: '2716' abstract: - lang: eng text: Multi-dimensional mean-payoff and energy games provide the mathematical foundation for the quantitative study of reactive systems, and play a central role in the emerging quantitative theory of verification and synthesis. In this work, we study the strategy synthesis problem for games with such multi-dimensional objectives along with a parity condition, a canonical way to express ω ω -regular conditions. While in general, the winning strategies in such games may require infinite memory, for synthesis the most relevant problem is the construction of a finite-memory winning strategy (if one exists). Our main contributions are as follows. First, we show a tight exponential bound (matching upper and lower bounds) on the memory required for finite-memory winning strategies in both multi-dimensional mean-payoff and energy games along with parity objectives. This significantly improves the triple exponential upper bound for multi energy games (without parity) that could be derived from results in literature for games on vector addition systems with states. Second, we present an optimal symbolic and incremental algorithm to compute a finite-memory winning strategy (if one exists) in such games. Finally, we give a complete characterization of when finite memory of strategies can be traded off for randomness. In particular, we show that for one-dimension mean-payoff parity games, randomized memoryless strategies are as powerful as their pure finite-memory counterparts. acknowledgement: "Krishnendu Chatterjee is supported by Austrian Science Fund (FWF) Grant No P 23499-N23, FWF NFN Grant No S11407 (RiSE), ERC Starting Grant (279307: Graph Games) and Microsoft faculty fellowship. Mickael Randour is supported by F.R.S.-FNRS. fellowship. \r\nJean-François Raskin is supported by ERC Starting Grant (279499: inVEST).Thanks to D. Sbabo for useful pointers, V. Bruyère for comments on a preliminary draft, and A. Bohy for fruitful discussions about the Acacia+ tool. We are grateful to the anonymous reviewers for their insightful comments. " article_processing_charge: No article_type: original author: - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Mickael full_name: Randour, Mickael last_name: Randour - first_name: Jean full_name: Raskin, Jean last_name: Raskin citation: ama: Chatterjee K, Randour M, Raskin J. Strategy synthesis for multi-dimensional quantitative objectives. Acta Informatica. 2014;51(3-4):129-163. doi:10.1007/s00236-013-0182-6 apa: Chatterjee, K., Randour, M., & Raskin, J. (2014). Strategy synthesis for multi-dimensional quantitative objectives. Acta Informatica. Springer. https://doi.org/10.1007/s00236-013-0182-6 chicago: Chatterjee, Krishnendu, Mickael Randour, and Jean Raskin. “Strategy Synthesis for Multi-Dimensional Quantitative Objectives.” Acta Informatica. Springer, 2014. https://doi.org/10.1007/s00236-013-0182-6. ieee: K. Chatterjee, M. Randour, and J. Raskin, “Strategy synthesis for multi-dimensional quantitative objectives,” Acta Informatica, vol. 51, no. 3–4. Springer, pp. 129–163, 2014. ista: Chatterjee K, Randour M, Raskin J. 2014. Strategy synthesis for multi-dimensional quantitative objectives. Acta Informatica. 51(3–4), 129–163. mla: Chatterjee, Krishnendu, et al. “Strategy Synthesis for Multi-Dimensional Quantitative Objectives.” Acta Informatica, vol. 51, no. 3–4, Springer, 2014, pp. 129–63, doi:10.1007/s00236-013-0182-6. short: K. Chatterjee, M. Randour, J. Raskin, Acta Informatica 51 (2014) 129–163. date_created: 2018-12-11T11:59:14Z date_published: 2014-06-01T00:00:00Z date_updated: 2023-02-21T16:06:56Z day: '01' department: - _id: KrCh doi: 10.1007/s00236-013-0182-6 external_id: arxiv: - '1201.5073' intvolume: ' 51' issue: 3-4 language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1201.5073 month: '06' oa: 1 oa_version: Preprint page: 129 - 163 project: - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory publication: Acta Informatica publication_status: published publisher: Springer publist_id: '4176' quality_controlled: '1' related_material: record: - id: '10904' relation: earlier_version status: public scopus_import: '1' status: public title: Strategy synthesis for multi-dimensional quantitative objectives type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 51 year: '2014' ...