---
_id: '2162'
abstract:
- lang: eng
text: 'We study two-player (zero-sum) concurrent mean-payoff games played on a finite-state
graph. We focus on the important sub-class of ergodic games where all states are
visited infinitely often with probability 1. The algorithmic study of ergodic
games was initiated in a seminal work of Hoffman and Karp in 1966, but all basic
complexity questions have remained unresolved. Our main results for ergodic games
are as follows: We establish (1) an optimal exponential bound on the patience
of stationary strategies (where patience of a distribution is the inverse of the
smallest positive probability and represents a complexity measure of a stationary
strategy); (2) the approximation problem lies in FNP; (3) the approximation problem
is at least as hard as the decision problem for simple stochastic games (for which
NP ∩ coNP is the long-standing best known bound). We present a variant of the
strategy-iteration algorithm by Hoffman and Karp; show that both our algorithm
and the classical value-iteration algorithm can approximate the value in exponential
time; and identify a subclass where the value-iteration algorithm is a FPTAS.
We also show that the exact value can be expressed in the existential theory of
the reals, and establish square-root sum hardness for a related class of 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: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
citation:
ama: 'Chatterjee K, Ibsen-Jensen R. The complexity of ergodic mean payoff games.
In: Vol 8573. Springer; 2014:122-133. doi:10.1007/978-3-662-43951-7_11'
apa: 'Chatterjee, K., & Ibsen-Jensen, R. (2014). The complexity of ergodic mean
payoff games (Vol. 8573, pp. 122–133). Presented at the ICST: International Conference
on Software Testing, Verification and Validation, Copenhagen, Denmark: Springer.
https://doi.org/10.1007/978-3-662-43951-7_11'
chicago: Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. “The Complexity of Ergodic
Mean Payoff Games,” 8573:122–33. Springer, 2014. https://doi.org/10.1007/978-3-662-43951-7_11.
ieee: 'K. Chatterjee and R. Ibsen-Jensen, “The complexity of ergodic mean payoff
games,” presented at the ICST: International Conference on Software Testing, Verification
and Validation, Copenhagen, Denmark, 2014, vol. 8573, no. Part 2, pp. 122–133.'
ista: 'Chatterjee K, Ibsen-Jensen R. 2014. The complexity of ergodic mean payoff
games. ICST: International Conference on Software Testing, Verification and Validation,
LNCS, vol. 8573, 122–133.'
mla: Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. The Complexity of Ergodic
Mean Payoff Games. Vol. 8573, no. Part 2, Springer, 2014, pp. 122–33, doi:10.1007/978-3-662-43951-7_11.
short: K. Chatterjee, R. Ibsen-Jensen, in:, Springer, 2014, pp. 122–133.
conference:
end_date: 2014-07-11
location: Copenhagen, Denmark
name: 'ICST: International Conference on Software Testing, Verification and Validation'
start_date: 2014-07-08
date_created: 2018-12-11T11:56:04Z
date_published: 2014-01-01T00:00:00Z
date_updated: 2023-02-23T12:24:48Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-662-43951-7_11
ec_funded: 1
external_id:
arxiv:
- '1404.5734'
intvolume: ' 8573'
issue: Part 2
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1404.5734
month: '01'
oa: 1
oa_version: Preprint
page: 122 - 133
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_status: published
publisher: Springer
publist_id: '4822'
quality_controlled: '1'
related_material:
record:
- id: '5404'
relation: earlier_version
status: public
status: public
title: The complexity of ergodic mean payoff games
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8573
year: '2014'
...
---
_id: '2213'
abstract:
- lang: eng
text: We consider two-player partial-observation stochastic games on finitestate
graphs where player 1 has partial observation and player 2 has perfect observation.
The winning condition we study are ε-regular conditions specified as parity objectives.
The qualitative-analysis problem given a partial-observation stochastic game and
a parity objective asks whether there is a strategy to ensure that the objective
is satisfied with probability 1 (resp. positive probability). These qualitative-analysis
problems are known to be undecidable. However in many applications the relevant
question is the existence of finite-memory strategies, and the qualitative-analysis
problems under finite-memory strategies was recently shown to be decidable in
2EXPTIME.We improve the complexity and show that the qualitative-analysis problems
for partial-observation stochastic parity games under finite-memory strategies
are EXPTIME-complete; and also establish optimal (exponential) memory bounds for
finite-memory strategies required for qualitative analysis.
acknowledgement: 'This research was supported by European project Cassting (FP7-601148),
NSF grants CNS 1049862 and CCF-1139011, by NSF Expe ditions in Computing project
“ExCAPE: Expeditions in Computer Augmented Program Engineering”, by BSF grant 9800096,
and by gift from Intel.'
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: Sumit
full_name: Nain, Sumit
last_name: Nain
- first_name: Moshe
full_name: Vardi, Moshe
last_name: Vardi
citation:
ama: 'Chatterjee K, Doyen L, Nain S, Vardi M. The complexity of partial-observation
stochastic parity games with finite-memory strategies. In: Vol 8412. Springer;
2014:242-257. doi:10.1007/978-3-642-54830-7_16'
apa: 'Chatterjee, K., Doyen, L., Nain, S., & Vardi, M. (2014). The complexity
of partial-observation stochastic parity games with finite-memory strategies (Vol.
8412, pp. 242–257). Presented at the FoSSaCS: Foundations of Software Science
and Computation Structures, Grenoble, France: Springer. https://doi.org/10.1007/978-3-642-54830-7_16'
chicago: Chatterjee, Krishnendu, Laurent Doyen, Sumit Nain, and Moshe Vardi. “The
Complexity of Partial-Observation Stochastic Parity Games with Finite-Memory Strategies,”
8412:242–57. Springer, 2014. https://doi.org/10.1007/978-3-642-54830-7_16.
ieee: 'K. Chatterjee, L. Doyen, S. Nain, and M. Vardi, “The complexity of partial-observation
stochastic parity games with finite-memory strategies,” presented at the FoSSaCS:
Foundations of Software Science and Computation Structures, Grenoble, France,
2014, vol. 8412, pp. 242–257.'
ista: 'Chatterjee K, Doyen L, Nain S, Vardi M. 2014. The complexity of partial-observation
stochastic parity games with finite-memory strategies. FoSSaCS: Foundations of
Software Science and Computation Structures, LNCS, vol. 8412, 242–257.'
mla: Chatterjee, Krishnendu, et al. The Complexity of Partial-Observation Stochastic
Parity Games with Finite-Memory Strategies. Vol. 8412, Springer, 2014, pp.
242–57, doi:10.1007/978-3-642-54830-7_16.
short: K. Chatterjee, L. Doyen, S. Nain, M. Vardi, in:, Springer, 2014, pp. 242–257.
conference:
end_date: 2014-04-13
location: Grenoble, France
name: 'FoSSaCS: Foundations of Software Science and Computation Structures'
start_date: 2014-04-05
date_created: 2018-12-11T11:56:21Z
date_published: 2014-04-01T00:00:00Z
date_updated: 2023-02-23T12:24:58Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-642-54830-7_16
ec_funded: 1
external_id:
arxiv:
- '1401.3289'
intvolume: ' 8412'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1401.3289
month: '04'
oa: 1
oa_version: Preprint
page: 242 - 257
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_status: published
publisher: Springer
publist_id: '4757'
quality_controlled: '1'
related_material:
record:
- id: '5408'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: The complexity of partial-observation stochastic parity games with finite-memory
strategies
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8412
year: '2014'
...
---
_id: '2212'
abstract:
- lang: eng
text: 'The theory of graph games is the foundation for modeling and synthesizing
reactive processes. In the synthesis of stochastic processes, we use 2 1/2-player
games where some transitions of the game graph are controlled by two adversarial
players, the System and the Environment, and the other transitions are determined
probabilistically. We consider 2 1/2-player games where the objective of the System
is the conjunction of a qualitative objective (specified as a parity condition)
and a quantitative objective (specified as a mean-payoff condition). We establish
that the problem of deciding whether the System can ensure that the probability
to satisfy the mean-payoff parity objective is at least a given threshold is in
NP ∩ coNP, matching the best known bound in the special case of 2-player games
(where all transitions are deterministic). We present an algorithm running in
time O(d·n2d·MeanGame) to compute the set of almost-sure winning states from which
the objective can be ensured with probability 1, where n is the number of states
of the game, d the number of priorities of the parity objective, and MeanGame
is the complexity to compute the set of almost-sure winning states in 2 1/2-player
mean-payoff games. Our results are useful in the synthesis of stochastic reactive
systems with both functional requirement (given as a qualitative objective) and
performance requirement (given as a quantitative objective). '
acknowledgement: "This research was supported by European project Cassting (FP7-601148).\r\nA
Technical Report of this paper is available at: \r\nhttps://repository.ist.ac.at/id/eprint/128."
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: Youssouf
full_name: Oualhadj, Youssouf
last_name: Oualhadj
citation:
ama: 'Chatterjee K, Doyen L, Gimbert H, Oualhadj Y. Perfect-information stochastic
mean-payoff parity games. In: Vol 8412. Springer; 2014:210-225. doi:10.1007/978-3-642-54830-7_14'
apa: 'Chatterjee, K., Doyen, L., Gimbert, H., & Oualhadj, Y. (2014). Perfect-information
stochastic mean-payoff parity games (Vol. 8412, pp. 210–225). Presented at the
FoSSaCS: Foundations of Software Science and Computation Structures, Grenoble,
France: Springer. https://doi.org/10.1007/978-3-642-54830-7_14'
chicago: Chatterjee, Krishnendu, Laurent Doyen, Hugo Gimbert, and Youssouf Oualhadj.
“Perfect-Information Stochastic Mean-Payoff Parity Games,” 8412:210–25. Springer,
2014. https://doi.org/10.1007/978-3-642-54830-7_14.
ieee: 'K. Chatterjee, L. Doyen, H. Gimbert, and Y. Oualhadj, “Perfect-information
stochastic mean-payoff parity games,” presented at the FoSSaCS: Foundations of
Software Science and Computation Structures, Grenoble, France, 2014, vol. 8412,
pp. 210–225.'
ista: 'Chatterjee K, Doyen L, Gimbert H, Oualhadj Y. 2014. Perfect-information stochastic
mean-payoff parity games. FoSSaCS: Foundations of Software Science and Computation
Structures, LNCS, vol. 8412, 210–225.'
mla: Chatterjee, Krishnendu, et al. Perfect-Information Stochastic Mean-Payoff
Parity Games. Vol. 8412, Springer, 2014, pp. 210–25, doi:10.1007/978-3-642-54830-7_14.
short: K. Chatterjee, L. Doyen, H. Gimbert, Y. Oualhadj, in:, Springer, 2014, pp.
210–225.
conference:
end_date: 2014-04-13
location: Grenoble, France
name: 'FoSSaCS: Foundations of Software Science and Computation Structures'
start_date: 2014-04-05
date_created: 2018-12-11T11:56:21Z
date_published: 2014-04-01T00:00:00Z
date_updated: 2023-02-23T12:24:50Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-642-54830-7_14
ec_funded: 1
intvolume: ' 8412'
language:
- iso: eng
month: '04'
oa_version: None
page: 210 - 225
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_status: published
publisher: Springer
publist_id: '4758'
quality_controlled: '1'
related_material:
record:
- id: '5405'
relation: earlier_version
status: public
scopus_import: 1
status: public
title: Perfect-information stochastic mean-payoff parity games
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8412
year: '2014'
...
---
_id: '2216'
abstract:
- lang: eng
text: The edit distance between two (untimed) traces is the minimum cost of a sequence
of edit operations (insertion, deletion, or substitution) needed to transform
one trace to the other. Edit distances have been extensively studied in the untimed
setting, and form the basis for approximate matching of sequences in different
domains such as coding theory, parsing, and speech recognition. In this paper,
we lift the study of edit distances from untimed languages to the timed setting.
We define an edit distance between timed words which incorporates both the edit
distance between the untimed words and the absolute difference in time stamps.
Our edit distance between two timed words is computable in polynomial time. Further,
we show that the edit distance between a timed word and a timed language generated
by a timed automaton, defined as the edit distance between the word and the closest
word in the language, is PSPACE-complete. While computing the edit distance between
two timed automata is undecidable, we show that the approximate version, where
we decide if the edit distance between two timed automata is either less than
a given parameter or more than δ away from the parameter, for δ > 0, can be
solved in exponential space and is EXPSPACE-hard. Our definitions and techniques
can be generalized to the setting of hybrid systems, and analogous decidability
results hold for rectangular automata.
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
- first_name: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
citation:
ama: 'Chatterjee K, Ibsen-Jensen R, Majumdar R. Edit distance for timed automata.
In: Springer; 2014:303-312. doi:10.1145/2562059.2562141'
apa: 'Chatterjee, K., Ibsen-Jensen, R., & Majumdar, R. (2014). Edit distance
for timed automata (pp. 303–312). Presented at the HSCC: Hybrid Systems - Computation
and Control, Berlin, Germany: Springer. https://doi.org/10.1145/2562059.2562141'
chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Ritankar Majumdar. “Edit
Distance for Timed Automata,” 303–12. Springer, 2014. https://doi.org/10.1145/2562059.2562141.
ieee: 'K. Chatterjee, R. Ibsen-Jensen, and R. Majumdar, “Edit distance for timed
automata,” presented at the HSCC: Hybrid Systems - Computation and Control, Berlin,
Germany, 2014, pp. 303–312.'
ista: 'Chatterjee K, Ibsen-Jensen R, Majumdar R. 2014. Edit distance for timed automata.
HSCC: Hybrid Systems - Computation and Control, 303–312.'
mla: Chatterjee, Krishnendu, et al. Edit Distance for Timed Automata. Springer,
2014, pp. 303–12, doi:10.1145/2562059.2562141.
short: K. Chatterjee, R. Ibsen-Jensen, R. Majumdar, in:, Springer, 2014, pp. 303–312.
conference:
end_date: 2017-04-17
location: Berlin, Germany
name: 'HSCC: Hybrid Systems - Computation and Control'
start_date: 2017-04-15
date_created: 2018-12-11T11:56:22Z
date_published: 2014-01-01T00:00:00Z
date_updated: 2023-02-23T12:25:01Z
day: '01'
department:
- _id: KrCh
doi: 10.1145/2562059.2562141
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://dl.acm.org/citation.cfm?doid=2562059.2562141
month: '01'
oa: 1
oa_version: Submitted Version
page: 303 - 312
publication_status: published
publisher: Springer
publist_id: '4752'
quality_controlled: '1'
related_material:
record:
- id: '5409'
relation: earlier_version
status: public
status: public
title: Edit distance for timed automata
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
year: '2014'
...
---
_id: '5411'
abstract:
- lang: eng
text: "Model-based testing is a promising technology for black-box software and
hardware testing, in which test cases are generated automatically from high-level
specifications. Nowadays, systems typically consist of multiple interacting components
and, due to their complexity, testing presents a considerable portion of the effort
and cost in the design process. Exploiting the compositional structure of system
specifications can considerably reduce the effort in model-based testing. Moreover,
inferring properties about the system from testing its individual components allows
the designer to reduce the amount of integration testing.\r\nIn this paper, we
study compositional properties of the IOCO-testing theory. We propose a new approach
to composition and hiding operations, inspired by contract-based design and interface
theories. These operations preserve behaviors that are compatible under composition
and hiding, and prune away incompatible ones. The resulting specification characterizes
the input sequences for which the unit testing of components is sufficient to
infer the correctness of component integration without the need for further tests.
We provide a methodology that uses these results to minimize integration testing
effort, but also to detect potential weaknesses in specifications. While we focus
on asynchronous models and the IOCO conformance relation, the resulting methodology
can be applied to a broader class of systems."
alternative_title:
- IST Austria Technical Report
author:
- first_name: Przemyslaw
full_name: Daca, Przemyslaw
id: 49351290-F248-11E8-B48F-1D18A9856A87
last_name: Daca
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Willibald
full_name: Krenn, Willibald
last_name: Krenn
- first_name: Dejan
full_name: Nickovic, Dejan
id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
last_name: Nickovic
citation:
ama: Daca P, Henzinger TA, Krenn W, Nickovic D. Compositional Specifications
for IOCO Testing. IST Austria; 2014. doi:10.15479/AT:IST-2014-148-v2-1
apa: Daca, P., Henzinger, T. A., Krenn, W., & Nickovic, D. (2014). Compositional
specifications for IOCO testing. IST Austria. https://doi.org/10.15479/AT:IST-2014-148-v2-1
chicago: Daca, Przemyslaw, Thomas A Henzinger, Willibald Krenn, and Dejan Nickovic.
Compositional Specifications for IOCO Testing. IST Austria, 2014. https://doi.org/10.15479/AT:IST-2014-148-v2-1.
ieee: P. Daca, T. A. Henzinger, W. Krenn, and D. Nickovic, Compositional specifications
for IOCO testing. IST Austria, 2014.
ista: Daca P, Henzinger TA, Krenn W, Nickovic D. 2014. Compositional specifications
for IOCO testing, IST Austria, 20p.
mla: Daca, Przemyslaw, et al. Compositional Specifications for IOCO Testing.
IST Austria, 2014, doi:10.15479/AT:IST-2014-148-v2-1.
short: P. Daca, T.A. Henzinger, W. Krenn, D. Nickovic, Compositional Specifications
for IOCO Testing, IST Austria, 2014.
date_created: 2018-12-12T11:39:11Z
date_published: 2014-01-28T00:00:00Z
date_updated: 2023-02-23T10:31:07Z
day: '28'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.15479/AT:IST-2014-148-v2-1
file:
- access_level: open_access
checksum: 0e03aba625cc334141a3148432aa5760
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:54:21Z
date_updated: 2020-07-14T12:46:46Z
file_id: '5543'
file_name: IST-2014-148-v2+1_main_tr.pdf
file_size: 534732
relation: main_file
file_date_updated: 2020-07-14T12:46:46Z
has_accepted_license: '1'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: '20'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '152'
related_material:
record:
- id: '2167'
relation: later_version
status: public
status: public
title: Compositional specifications for IOCO testing
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2014'
...