---
_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'
...