---
_id: '6752'
abstract:
- lang: eng
text: 'Two-player games on graphs are widely studied in formal methods, as they
model the interaction between a system and its environment. The game is played
by moving a token throughout a graph to produce an infinite path. There are several
common modes to determine how the players move the token through the graph; e.g.,
in turn-based games the players alternate turns in moving the token. We study
the bidding mode of moving the token, which, to the best of our knowledge, has
never been studied in infinite-duration games. The following bidding rule was
previously defined and called Richman bidding. Both players have separate budgets,
which sum up to 1. In each turn, a bidding takes place: Both players submit bids
simultaneously, where a bid is legal if it does not exceed the available budget,
and the higher bidder pays his bid to the other player and moves the token. The
central question studied in bidding games is a necessary and sufficient initial
budget for winning the game: a threshold budget in a vertex is a value t ∈ [0,
1] such that if Player 1’s budget exceeds t, he can win the game; and if Player
2’s budget exceeds 1 − t, he can win the game. Threshold budgets were previously
shown to exist in every vertex of a reachability game, which have an interesting
connection with random-turn games—a sub-class of simple stochastic games in which
the player who moves is chosen randomly. We show the existence of threshold budgets
for a qualitative class of infinite-duration games, namely parity games, and a
quantitative class, namely mean-payoff games. The key component of the proof is
a quantitative solution to strongly connected mean-payoff bidding games in which
we extend the connection with random-turn games to these games, and construct
explicit optimal strategies for both players.'
article_number: '31'
article_processing_charge: No
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- 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: Ventsislav K
full_name: Chonev, Ventsislav K
id: 36CBE2E6-F248-11E8-B48F-1D18A9856A87
last_name: Chonev
citation:
ama: Avni G, Henzinger TA, Chonev VK. Infinite-duration bidding games. Journal
of the ACM. 2019;66(4). doi:10.1145/3340295
apa: Avni, G., Henzinger, T. A., & Chonev, V. K. (2019). Infinite-duration bidding
games. Journal of the ACM. ACM. https://doi.org/10.1145/3340295
chicago: Avni, Guy, Thomas A Henzinger, and Ventsislav K Chonev. “Infinite-Duration
Bidding Games.” Journal of the ACM. ACM, 2019. https://doi.org/10.1145/3340295.
ieee: G. Avni, T. A. Henzinger, and V. K. Chonev, “Infinite-duration bidding games,”
Journal of the ACM, vol. 66, no. 4. ACM, 2019.
ista: Avni G, Henzinger TA, Chonev VK. 2019. Infinite-duration bidding games. Journal
of the ACM. 66(4), 31.
mla: Avni, Guy, et al. “Infinite-Duration Bidding Games.” Journal of the ACM,
vol. 66, no. 4, 31, ACM, 2019, doi:10.1145/3340295.
short: G. Avni, T.A. Henzinger, V.K. Chonev, Journal of the ACM 66 (2019).
date_created: 2019-08-04T21:59:16Z
date_published: 2019-07-16T00:00:00Z
date_updated: 2023-08-29T07:02:13Z
day: '16'
department:
- _id: ToHe
doi: 10.1145/3340295
external_id:
arxiv:
- '1705.01433'
isi:
- '000487714900008'
intvolume: ' 66'
isi: 1
issue: '4'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1705.01433
month: '07'
oa: 1
oa_version: Preprint
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
- _id: 25F2ACDE-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Rigorous Systems Engineering
- _id: 264B3912-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: M02369
name: Formal Methods meets Algorithmic Game Theory
publication: Journal of the ACM
publication_identifier:
eissn:
- 1557735X
issn:
- '00045411'
publication_status: published
publisher: ACM
quality_controlled: '1'
related_material:
record:
- id: '950'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Infinite-duration bidding games
type: journal_article
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 66
year: '2019'
...
---
_id: '950'
abstract:
- lang: eng
text: "Two-player games on graphs are widely studied in formal methods as they model
the interaction between a system and its environment. The game is played by moving
a token throughout a graph to produce an infinite path. There are several common
modes to determine how the players move the token through the graph; e.g., in
turn-based games the players alternate turns in moving the token. We study the
bidding mode of moving the token, which, to the best of our knowledge, has never
been studied in infinite-duration games. Both players have separate budgets, which
sum up to $1$. In each turn, a bidding takes place. Both players submit bids simultaneously,
and a bid is legal if it does not exceed the available budget. The winner of the
bidding pays his bid to the other player and moves the token. For reachability
objectives, repeated bidding games have been studied and are called Richman games.
There, a central question is the existence and computation of threshold budgets;
namely, a value t\\in [0,1] such that if\\PO's budget exceeds $t$, he can win
the game, and if\\PT's budget exceeds 1-t, he can win the game. We focus on parity
games and mean-payoff games. We show the existence of threshold budgets in these
games, and reduce the problem of finding them to Richman games. We also determine
the strategy-complexity of an optimal strategy. Our most interesting result shows
that memoryless strategies suffice for mean-payoff bidding games. \r\n"
alternative_title:
- LIPIcs
article_number: '17'
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- 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: Ventsislav K
full_name: Chonev, Ventsislav K
id: 36CBE2E6-F248-11E8-B48F-1D18A9856A87
last_name: Chonev
citation:
ama: 'Avni G, Henzinger TA, Chonev VK. Infinite-duration bidding games. In: Vol
85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:10.4230/LIPIcs.CONCUR.2017.21'
apa: 'Avni, G., Henzinger, T. A., & Chonev, V. K. (2017). Infinite-duration
bidding games (Vol. 85). Presented at the CONCUR: Concurrency Theory, Berlin,
Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2017.21'
chicago: Avni, Guy, Thomas A Henzinger, and Ventsislav K Chonev. “Infinite-Duration
Bidding Games,” Vol. 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.
https://doi.org/10.4230/LIPIcs.CONCUR.2017.21.
ieee: 'G. Avni, T. A. Henzinger, and V. K. Chonev, “Infinite-duration bidding games,”
presented at the CONCUR: Concurrency Theory, Berlin, Germany, 2017, vol. 85.'
ista: 'Avni G, Henzinger TA, Chonev VK. 2017. Infinite-duration bidding games. CONCUR:
Concurrency Theory, LIPIcs, vol. 85, 17.'
mla: Avni, Guy, et al. Infinite-Duration Bidding Games. Vol. 85, 17, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:10.4230/LIPIcs.CONCUR.2017.21.
short: G. Avni, T.A. Henzinger, V.K. Chonev, in:, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2017.
conference:
end_date: 2017-09-07
location: Berlin, Germany
name: 'CONCUR: Concurrency Theory'
start_date: 2017-09-05
date_created: 2018-12-11T11:49:22Z
date_published: 2017-09-01T00:00:00Z
date_updated: 2023-08-29T07:02:13Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
- _id: KrCh
doi: 10.4230/LIPIcs.CONCUR.2017.21
external_id:
arxiv:
- '1705.01433'
file:
- access_level: open_access
checksum: 6d5cccf755207b91ccbef95d8275b013
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:18:00Z
date_updated: 2020-07-14T12:48:16Z
file_id: '5318'
file_name: IST-2017-844-v1+1_concur-cr.pdf
file_size: 335170
relation: main_file
file_date_updated: 2020-07-14T12:48:16Z
has_accepted_license: '1'
intvolume: ' 85'
language:
- iso: eng
month: '09'
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: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication_identifier:
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '6466'
pubrep_id: '844'
quality_controlled: '1'
related_material:
record:
- id: '6752'
relation: later_version
status: public
scopus_import: 1
status: public
title: Infinite-duration bidding games
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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 85
year: '2017'
...
---
_id: '1069'
abstract:
- lang: eng
text: "The Continuous Skolem Problem asks whether a real-valued function satisfying
a linear differen-\r\ntial equation has a zero in a given interval of real numbers.
This is a fundamental reachability\r\nproblem for continuous linear dynamical
systems, such as linear hybrid automata and continuous-\r\ntime Markov chains.
Decidability of the problem is currently open – indeed decidability is open\r\neven
for the sub-problem in which a zero is sought in a bounded interval. In this paper
we show\r\ndecidability of the bounded problem subject to Schanuel’s Conjecture,
a unifying conjecture in\r\ntranscendental number theory. We furthermore analyse
the unbounded problem in terms of the\r\nfrequencies of the differential equation,
that is, the imaginary parts of the characteristic roots.\r\nWe show that the
unbounded problem can be reduced to the bounded problem if there is at most\r\none
rationally linearly independent frequency, or if there are two rationally linearly
independent\r\nfrequencies and all characteristic roots are simple. We complete
the picture by showing that de-\r\ncidability of the unbounded problem in the
case of two (or more) rationally linearly independent\r\nfrequencies would entail
a major new effectiveness result in Diophantine approximation, namely\r\ncomputability
of the Diophantine-approximation types of all real algebraic numbers."
acknowledgement: 'Ventsislav Chonev is supported by Austrian Science Fund (FWF) NFN
Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant (279307: Graph Games), and ERC
Advanced Grant (267989: QUAREM).'
alternative_title:
- LIPIcs
article_number: '100'
author:
- first_name: Ventsislav K
full_name: Chonev, Ventsislav K
id: 36CBE2E6-F248-11E8-B48F-1D18A9856A87
last_name: Chonev
- first_name: Joël
full_name: Ouaknine, Joël
last_name: Ouaknine
- first_name: James
full_name: Worrell, James
last_name: Worrell
citation:
ama: 'Chonev VK, Ouaknine J, Worrell J. On the skolem problem for continuous linear
dynamical systems. In: Vol 55. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik;
2016. doi:10.4230/LIPIcs.ICALP.2016.100'
apa: 'Chonev, V. K., Ouaknine, J., & Worrell, J. (2016). On the skolem problem
for continuous linear dynamical systems (Vol. 55). Presented at the ICALP: Automata,
Languages and Programming, Rome, Italy: Schloss Dagstuhl- Leibniz-Zentrum fur
Informatik. https://doi.org/10.4230/LIPIcs.ICALP.2016.100'
chicago: Chonev, Ventsislav K, Joël Ouaknine, and James Worrell. “On the Skolem
Problem for Continuous Linear Dynamical Systems,” Vol. 55. Schloss Dagstuhl- Leibniz-Zentrum
fur Informatik, 2016. https://doi.org/10.4230/LIPIcs.ICALP.2016.100.
ieee: 'V. K. Chonev, J. Ouaknine, and J. Worrell, “On the skolem problem for continuous
linear dynamical systems,” presented at the ICALP: Automata, Languages and Programming,
Rome, Italy, 2016, vol. 55.'
ista: 'Chonev VK, Ouaknine J, Worrell J. 2016. On the skolem problem for continuous
linear dynamical systems. ICALP: Automata, Languages and Programming, LIPIcs,
vol. 55, 100.'
mla: Chonev, Ventsislav K., et al. On the Skolem Problem for Continuous Linear
Dynamical Systems. Vol. 55, 100, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik,
2016, doi:10.4230/LIPIcs.ICALP.2016.100.
short: V.K. Chonev, J. Ouaknine, J. Worrell, in:, Schloss Dagstuhl- Leibniz-Zentrum
fur Informatik, 2016.
conference:
end_date: 2016-07-15
location: Rome, Italy
name: 'ICALP: Automata, Languages and Programming'
start_date: 2016-07-12
date_created: 2018-12-11T11:49:59Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2021-01-12T06:48:03Z
day: '01'
ddc:
- '004'
- '006'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.ICALP.2016.100
ec_funded: 1
file:
- access_level: open_access
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:16:26Z
date_updated: 2018-12-12T10:16:26Z
file_id: '5213'
file_name: IST-2017-778-v1+1_LIPIcs-ICALP-2016-100.pdf
file_size: 521415
relation: main_file
file_date_updated: 2018-12-12T10:16:26Z
has_accepted_license: '1'
intvolume: ' 55'
language:
- iso: eng
month: '08'
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: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication_status: published
publisher: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik
publist_id: '6314'
pubrep_id: '778'
quality_controlled: '1'
scopus_import: 1
status: public
title: On the skolem problem for continuous linear dynamical systems
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: 55
year: '2016'
...
---
_id: '1380'
abstract:
- lang: eng
text: We consider higher-dimensional versions of Kannan and Lipton's Orbit Problem
- determining whether a target vector space V may be reached from a starting point
x under repeated applications of a linear transformation A. Answering two questions
posed by Kannan and Lipton in the 1980s, we show that when V has dimension one,
this problem is solvable in polynomial time, and when V has dimension two or three,
the problem is in NPRP.
article_number: '23'
author:
- first_name: Ventsislav K
full_name: Chonev, Ventsislav K
id: 36CBE2E6-F248-11E8-B48F-1D18A9856A87
last_name: Chonev
- first_name: Joël
full_name: Ouaknine, Joël
last_name: Ouaknine
- first_name: James
full_name: Worrell, James
last_name: Worrell
citation:
ama: Chonev VK, Ouaknine J, Worrell J. On the complexity of the orbit problem. Journal
of the ACM. 2016;63(3). doi:10.1145/2857050
apa: Chonev, V. K., Ouaknine, J., & Worrell, J. (2016). On the complexity of
the orbit problem. Journal of the ACM. ACM. https://doi.org/10.1145/2857050
chicago: Chonev, Ventsislav K, Joël Ouaknine, and James Worrell. “On the Complexity
of the Orbit Problem.” Journal of the ACM. ACM, 2016. https://doi.org/10.1145/2857050.
ieee: V. K. Chonev, J. Ouaknine, and J. Worrell, “On the complexity of the orbit
problem,” Journal of the ACM, vol. 63, no. 3. ACM, 2016.
ista: Chonev VK, Ouaknine J, Worrell J. 2016. On the complexity of the orbit problem.
Journal of the ACM. 63(3), 23.
mla: Chonev, Ventsislav K., et al. “On the Complexity of the Orbit Problem.” Journal
of the ACM, vol. 63, no. 3, 23, ACM, 2016, doi:10.1145/2857050.
short: V.K. Chonev, J. Ouaknine, J. Worrell, Journal of the ACM 63 (2016).
date_created: 2018-12-11T11:51:41Z
date_published: 2016-06-01T00:00:00Z
date_updated: 2021-01-12T06:50:17Z
day: '01'
department:
- _id: KrCh
doi: 10.1145/2857050
intvolume: ' 63'
issue: '3'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/1303.2981
month: '06'
oa: 1
oa_version: Preprint
publication: Journal of the ACM
publication_status: published
publisher: ACM
publist_id: '5831'
quality_controlled: '1'
scopus_import: 1
status: public
title: On the complexity of the orbit problem
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 63
year: '2016'
...
---
_id: '1389'
abstract:
- lang: eng
text: "The continuous evolution of a wide variety of systems, including continous-time
Markov chains and linear hybrid automata, can be\r\ndescribed in terms of linear
differential equations. In this paper we study the decision problem of whether
the solution x(t) of a system of linear differential equations dx/dt = Ax reaches
a target halfspace infinitely often. This recurrent reachability problem can\r\nequivalently
be formulated as the following Infinite Zeros Problem: does a real-valued function
f:R≥0 --> R satisfying a given linear\r\ndifferential equation have infinitely
many zeros? Our main decidability result is that if the differential equation
has order at most 7, then the Infinite Zeros Problem is decidable. On the other
hand, we show that a decision procedure for the Infinite Zeros Problem at order
9 (and above) would entail a major breakthrough in Diophantine Approximation,
specifically an algorithm for computing the Lagrange constants of arbitrary real
algebraic numbers to arbitrary precision."
author:
- first_name: Ventsislav K
full_name: Chonev, Ventsislav K
id: 36CBE2E6-F248-11E8-B48F-1D18A9856A87
last_name: Chonev
- first_name: Joël
full_name: Ouaknine, Joël
last_name: Ouaknine
- first_name: James
full_name: Worrell, James
last_name: Worrell
citation:
ama: 'Chonev VK, Ouaknine J, Worrell J. On recurrent reachability for continuous
linear dynamical systems. In: LICS ’16. IEEE; 2016:515-524. doi:10.1145/2933575.2934548'
apa: 'Chonev, V. K., Ouaknine, J., & Worrell, J. (2016). On recurrent reachability
for continuous linear dynamical systems. In LICS ’16 (pp. 515–524). New
York, NY, USA: IEEE. https://doi.org/10.1145/2933575.2934548'
chicago: Chonev, Ventsislav K, Joël Ouaknine, and James Worrell. “On Recurrent Reachability
for Continuous Linear Dynamical Systems.” In LICS ’16, 515–24. IEEE, 2016.
https://doi.org/10.1145/2933575.2934548.
ieee: V. K. Chonev, J. Ouaknine, and J. Worrell, “On recurrent reachability for
continuous linear dynamical systems,” in LICS ’16, New York, NY, USA, 2016,
pp. 515–524.
ista: 'Chonev VK, Ouaknine J, Worrell J. 2016. On recurrent reachability for continuous
linear dynamical systems. LICS ’16. LICS: Logic in Computer Science, 515–524.'
mla: Chonev, Ventsislav K., et al. “On Recurrent Reachability for Continuous Linear
Dynamical Systems.” LICS ’16, IEEE, 2016, pp. 515–24, doi:10.1145/2933575.2934548.
short: V.K. Chonev, J. Ouaknine, J. Worrell, in:, LICS ’16, IEEE, 2016, pp. 515–524.
conference:
end_date: 2018-07-08
location: New York, NY, USA
name: 'LICS: Logic in Computer Science'
start_date: 2018-07-05
date_created: 2018-12-11T11:51:44Z
date_published: 2016-07-05T00:00:00Z
date_updated: 2021-01-12T06:50:20Z
day: '05'
department:
- _id: KrCh
doi: 10.1145/2933575.2934548
ec_funded: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1507.03632
month: '07'
oa: 1
oa_version: Preprint
page: 515 - 524
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: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
publication: LICS '16
publication_status: published
publisher: IEEE
publist_id: '5820'
quality_controlled: '1'
scopus_import: 1
status: public
title: On recurrent reachability for continuous linear dynamical systems
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2016'
...