---
_id: '10674'
abstract:
- lang: eng
text: 'In two-player games on graphs, the players move a token through a graph to
produce an infinite path, which determines the winner of the game. Such games
are central in formal methods since they model the interaction between a non-terminating
system and its environment. In bidding games the players bid for the right to
move the token: in each round, the players simultaneously submit bids, and the
higher bidder moves the token and pays the other player. Bidding games are known
to have a clean and elegant mathematical structure that relies on the ability
of the players to submit arbitrarily small bids. Many applications, however, require
a fixed granularity for the bids, which can represent, for example, the monetary
value expressed in cents. We study, for the first time, the combination of discrete-bidding
and infinite-duration games. Our most important result proves that these games
form a large determined subclass of concurrent games, where determinacy is the
strong property that there always exists exactly one player who can guarantee
winning the game. In particular, we show that, in contrast to non-discrete bidding
games, the mechanism with which tied bids are resolved plays an important role
in discrete-bidding games. We study several natural tie-breaking mechanisms and
show that, while some do not admit determinacy, most natural mechanisms imply
determinacy for every pair of initial budgets.'
acknowledgement: "This research was supported in part by the Austrian Science Fund
(FWF) under grants S11402-N23 (RiSE/SHiNE), Z211-N23 (Wittgenstein Award), and M
2369-N33 (Meitner fellowship).\r\n"
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Milad
full_name: Aghajohari, Milad
last_name: Aghajohari
- 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
citation:
ama: Aghajohari M, Avni G, Henzinger TA. Determinacy in discrete-bidding infinite-duration
games. Logical Methods in Computer Science. 2021;17(1):10:1-10:23. doi:10.23638/LMCS-17(1:10)2021
apa: Aghajohari, M., Avni, G., & Henzinger, T. A. (2021). Determinacy in discrete-bidding
infinite-duration games. Logical Methods in Computer Science. International
Federation for Computational Logic. https://doi.org/10.23638/LMCS-17(1:10)2021
chicago: Aghajohari, Milad, Guy Avni, and Thomas A Henzinger. “Determinacy in Discrete-Bidding
Infinite-Duration Games.” Logical Methods in Computer Science. International
Federation for Computational Logic, 2021. https://doi.org/10.23638/LMCS-17(1:10)2021.
ieee: M. Aghajohari, G. Avni, and T. A. Henzinger, “Determinacy in discrete-bidding
infinite-duration games,” Logical Methods in Computer Science, vol. 17,
no. 1. International Federation for Computational Logic, p. 10:1-10:23, 2021.
ista: Aghajohari M, Avni G, Henzinger TA. 2021. Determinacy in discrete-bidding
infinite-duration games. Logical Methods in Computer Science. 17(1), 10:1-10:23.
mla: Aghajohari, Milad, et al. “Determinacy in Discrete-Bidding Infinite-Duration
Games.” Logical Methods in Computer Science, vol. 17, no. 1, International
Federation for Computational Logic, 2021, p. 10:1-10:23, doi:10.23638/LMCS-17(1:10)2021.
short: M. Aghajohari, G. Avni, T.A. Henzinger, Logical Methods in Computer Science
17 (2021) 10:1-10:23.
corr_author: '1'
date_created: 2022-01-25T16:32:13Z
date_published: 2021-02-03T00:00:00Z
date_updated: 2025-04-15T06:25:56Z
day: '03'
ddc:
- '510'
department:
- _id: ToHe
doi: 10.23638/LMCS-17(1:10)2021
external_id:
arxiv:
- '1905.03588'
isi:
- '000658724600010'
file:
- access_level: open_access
checksum: b35586a50ed1ca8f44767de116d18d81
content_type: application/pdf
creator: alisjak
date_created: 2022-01-26T08:04:50Z
date_updated: 2022-01-26T08:04:50Z
file_id: '10690'
file_name: 2021_LMCS_AGHAJOHAR.pdf
file_size: 819878
relation: main_file
success: 1
file_date_updated: 2022-01-26T08:04:50Z
has_accepted_license: '1'
intvolume: ' 17'
isi: 1
issue: '1'
keyword:
- computer science
- computer science and game theory
- logic in computer science
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: 10:1-10:23
project:
- _id: 264B3912-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: M02369
name: Formal Methods meets Algorithmic Game Theory
- _id: 25F2ACDE-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
publication: Logical Methods in Computer Science
publication_identifier:
eissn:
- 1860-5974
publication_status: published
publisher: International Federation for Computational Logic
quality_controlled: '1'
scopus_import: '1'
status: public
title: Determinacy in discrete-bidding infinite-duration 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: journal_article
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 17
year: '2021'
...
---
OA_place: repository
OA_type: green
_id: '9197'
abstract:
- lang: eng
text: In this paper we introduce and study all-pay bidding games, a class of two
player, zero-sum games on graphs. The game proceeds as follows. We place a token
on some vertex in the graph and assign budgets to the two players. Each turn,
each player submits a sealed legal bid (non-negative and below their remaining
budget), which is deducted from their budget and the highest bidder moves the
token onto an adjacent vertex. The game ends once a sink is reached, and Player
1 pays Player 2 the outcome that is associated with the sink. The players attempt
to maximize their expected outcome. Our games model settings where effort (of
no inherent value) needs to be invested in an ongoing and stateful manner. On
the negative side, we show that even in simple games on DAGs, optimal strategies
may require a distribution over bids with infinite support. A central quantity
in bidding games is the ratio of the players budgets. On the positive side, we
show a simple FPTAS for DAGs, that, for each budget ratio, outputs an approximation
for the optimal strategy for that ratio. We also implement it, show that it performs
well, and suggests interesting properties of these games. Then, given an outcome
c, we show an algorithm for finding the necessary and sufficient initial ratio
for guaranteeing outcome c with probability 1 and a strategy ensuring such. Finally,
while the general case has not previously been studied, solving the specific game
in which Player 1 wins iff he wins the first two auctions, has been long stated
as an open question, which we solve.
acknowledgement: This research was supported by the Austrian Science Fund (FWF) under
grants S11402-N23 (RiSE/SHiNE), Z211-N23 (Wittgenstein Award), and M 2369-N33 (Meitner
fellowship).
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- 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: Josef
full_name: Tkadlec, Josef
id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87
last_name: Tkadlec
orcid: 0000-0002-1097-9684
citation:
ama: Avni G, Ibsen-Jensen R, Tkadlec J. All-pay bidding games on graphs. Proceedings
of the AAAI Conference on Artificial Intelligence. 2020;34(02):1798-1805.
doi:10.1609/aaai.v34i02.5546
apa: 'Avni, G., Ibsen-Jensen, R., & Tkadlec, J. (2020). All-pay bidding games
on graphs. Proceedings of the AAAI Conference on Artificial Intelligence.
New York, NY, United States: Association for the Advancement of Artificial Intelligence.
https://doi.org/10.1609/aaai.v34i02.5546'
chicago: Avni, Guy, Rasmus Ibsen-Jensen, and Josef Tkadlec. “All-Pay Bidding Games
on Graphs.” Proceedings of the AAAI Conference on Artificial Intelligence.
Association for the Advancement of Artificial Intelligence, 2020. https://doi.org/10.1609/aaai.v34i02.5546.
ieee: G. Avni, R. Ibsen-Jensen, and J. Tkadlec, “All-pay bidding games on graphs,”
Proceedings of the AAAI Conference on Artificial Intelligence, vol. 34,
no. 02. Association for the Advancement of Artificial Intelligence, pp. 1798–1805,
2020.
ista: Avni G, Ibsen-Jensen R, Tkadlec J. 2020. All-pay bidding games on graphs.
Proceedings of the AAAI Conference on Artificial Intelligence. 34(02), 1798–1805.
mla: Avni, Guy, et al. “All-Pay Bidding Games on Graphs.” Proceedings of the
AAAI Conference on Artificial Intelligence, vol. 34, no. 02, Association for
the Advancement of Artificial Intelligence, 2020, pp. 1798–805, doi:10.1609/aaai.v34i02.5546.
short: G. Avni, R. Ibsen-Jensen, J. Tkadlec, Proceedings of the AAAI Conference
on Artificial Intelligence 34 (2020) 1798–1805.
conference:
end_date: 2020-02-12
location: New York, NY, United States
name: 'AAAI: Conference on Artificial Intelligence'
start_date: 2020-02-07
date_created: 2021-02-25T09:05:18Z
date_published: 2020-04-03T00:00:00Z
date_updated: 2025-07-03T11:44:58Z
day: '03'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1609/aaai.v34i02.5546
external_id:
arxiv:
- '1911.08360'
intvolume: ' 34'
issue: '02'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1911.08360
month: '04'
oa: 1
oa_version: Preprint
page: 1798-1805
project:
- _id: 25F2ACDE-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
- _id: 264B3912-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: M02369
name: Formal Methods meets Algorithmic Game Theory
publication: Proceedings of the AAAI Conference on Artificial Intelligence
publication_identifier:
eissn:
- 2374-3468
isbn:
- '9781577358350'
issn:
- 2159-5399
publication_status: published
publisher: Association for the Advancement of Artificial Intelligence
quality_controlled: '1'
scopus_import: '1'
status: public
title: All-pay bidding games on graphs
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 34
year: '2020'
...
---
_id: '6761'
abstract:
- lang: eng
text: In resource allocation games, selfish players share resources that are needed
in order to fulfill their objectives. The cost of using a resource depends on
the load on it. In the traditional setting, the players make their choices concurrently
and in one-shot. That is, a strategy for a player is a subset of the resources.
We introduce and study dynamic resource allocation games. In this setting, the
game proceeds in phases. In each phase each player chooses one resource. A scheduler
dictates the order in which the players proceed in a phase, possibly scheduling
several players to proceed concurrently. The game ends when each player has collected
a set of resources that fulfills his objective. The cost for each player then
depends on this set as well as on the load on the resources in it – we consider
both congestion and cost-sharing games. We argue that the dynamic setting is the
suitable setting for many applications in practice. We study the stability of
dynamic resource allocation games, where the appropriate notion of stability is
that of subgame perfect equilibrium, study the inefficiency incurred due to selfish
behavior, and also study problems that are particular to the dynamic setting,
like constraints on the order in which resources can be chosen or the problem
of finding a scheduler that achieves stability.
article_processing_charge: No
article_type: original
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: Orna
full_name: Kupferman, Orna
last_name: Kupferman
citation:
ama: Avni G, Henzinger TA, Kupferman O. Dynamic resource allocation games. Theoretical
Computer Science. 2020;807:42-55. doi:10.1016/j.tcs.2019.06.031
apa: Avni, G., Henzinger, T. A., & Kupferman, O. (2020). Dynamic resource allocation
games. Theoretical Computer Science. Elsevier. https://doi.org/10.1016/j.tcs.2019.06.031
chicago: Avni, Guy, Thomas A Henzinger, and Orna Kupferman. “Dynamic Resource Allocation
Games.” Theoretical Computer Science. Elsevier, 2020. https://doi.org/10.1016/j.tcs.2019.06.031.
ieee: G. Avni, T. A. Henzinger, and O. Kupferman, “Dynamic resource allocation games,”
Theoretical Computer Science, vol. 807. Elsevier, pp. 42–55, 2020.
ista: Avni G, Henzinger TA, Kupferman O. 2020. Dynamic resource allocation games.
Theoretical Computer Science. 807, 42–55.
mla: Avni, Guy, et al. “Dynamic Resource Allocation Games.” Theoretical Computer
Science, vol. 807, Elsevier, 2020, pp. 42–55, doi:10.1016/j.tcs.2019.06.031.
short: G. Avni, T.A. Henzinger, O. Kupferman, Theoretical Computer Science 807 (2020)
42–55.
date_created: 2019-08-04T21:59:20Z
date_published: 2020-02-06T00:00:00Z
date_updated: 2026-04-16T09:35:15Z
day: '06'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1016/j.tcs.2019.06.031
external_id:
isi:
- '000512219400004'
file:
- access_level: open_access
checksum: e86635417f45eb2cd75778f91382f737
content_type: application/pdf
creator: dernst
date_created: 2020-10-09T06:31:22Z
date_updated: 2020-10-09T06:31:22Z
file_id: '8639'
file_name: 2020_TheoreticalCS_Avni.pdf
file_size: 1413001
relation: main_file
success: 1
file_date_updated: 2020-10-09T06:31:22Z
has_accepted_license: '1'
intvolume: ' 807'
isi: 1
language:
- iso: eng
month: '02'
oa: 1
oa_version: Submitted Version
page: 42-55
project:
- _id: 25F2ACDE-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
- _id: 264B3912-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: M02369
name: Formal Methods meets Algorithmic Game Theory
publication: Theoretical Computer Science
publication_identifier:
issn:
- 0304-3975
publication_status: published
publisher: Elsevier
quality_controlled: '1'
related_material:
record:
- id: '1341'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Dynamic resource allocation games
type: journal_article
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
volume: 807
year: '2020'
...
---
_id: '6462'
abstract:
- lang: eng
text: A controller is a device that interacts with a plant. At each time point,it
reads the plant’s state and issues commands with the goal that the plant oper-ates
optimally. Constructing optimal controllers is a fundamental and challengingproblem.
Machine learning techniques have recently been successfully applied totrain controllers,
yet they have limitations. Learned controllers are monolithic andhard to reason
about. In particular, it is difficult to add features without retraining,to guarantee
any level of performance, and to achieve acceptable performancewhen encountering
untrained scenarios. These limitations can be addressed bydeploying quantitative
run-timeshieldsthat serve as a proxy for the controller.At each time point, the
shield reads the command issued by the controller andmay choose to alter it before
passing it on to the plant. We show how optimalshields that interfere as little
as possible while guaranteeing a desired level ofcontroller performance, can be
generated systematically and automatically usingreactive synthesis. First, we abstract the plant by building a stochastic model.Second,
we consider the learned controller to be a black box. Third, we mea-surecontroller
performanceandshield interferenceby two quantitative run-timemeasures that are
formally defined using weighted automata. Then, the problemof constructing a shield
that guarantees maximal performance with minimal inter-ference is the problem
of finding an optimal strategy in a stochastic2-player game“controller versus
shield” played on the abstract state space of the plant with aquantitative objective
obtained from combining the performance and interferencemeasures. We illustrate
the effectiveness of our approach by automatically con-structing lightweight shields
for learned traffic-light controllers in various roadnetworks. The shields we
generate avoid liveness bugs, improve controller per-formance in untrained and
changing traffic situations, and add features to learnedcontrollers, such as giving
priority to emergency vehicles.
alternative_title:
- LNCS
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: 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: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Bettina
full_name: Konighofer, Bettina
last_name: Konighofer
- first_name: Stefan
full_name: Pranger, Stefan
last_name: Pranger
citation:
ama: 'Avni G, Bloem R, Chatterjee K, Henzinger TA, Konighofer B, Pranger S. Run-time
optimization for learned controllers through quantitative games. In: 31st International
Conference on Computer-Aided Verification. Vol 11561. Springer; 2019:630-649.
doi:10.1007/978-3-030-25540-4_36'
apa: 'Avni, G., Bloem, R., Chatterjee, K., Henzinger, T. A., Konighofer, B., &
Pranger, S. (2019). Run-time optimization for learned controllers through quantitative
games. In 31st International Conference on Computer-Aided Verification
(Vol. 11561, pp. 630–649). New York, NY, United States: Springer. https://doi.org/10.1007/978-3-030-25540-4_36'
chicago: Avni, Guy, Roderick Bloem, Krishnendu Chatterjee, Thomas A Henzinger, Bettina
Konighofer, and Stefan Pranger. “Run-Time Optimization for Learned Controllers
through Quantitative Games.” In 31st International Conference on Computer-Aided
Verification, 11561:630–49. Springer, 2019. https://doi.org/10.1007/978-3-030-25540-4_36.
ieee: G. Avni, R. Bloem, K. Chatterjee, T. A. Henzinger, B. Konighofer, and S. Pranger,
“Run-time optimization for learned controllers through quantitative games,” in
31st International Conference on Computer-Aided Verification, New York,
NY, United States, 2019, vol. 11561, pp. 630–649.
ista: 'Avni G, Bloem R, Chatterjee K, Henzinger TA, Konighofer B, Pranger S. 2019.
Run-time optimization for learned controllers through quantitative games. 31st
International Conference on Computer-Aided Verification. CAV: Computer Aided Verification,
LNCS, vol. 11561, 630–649.'
mla: Avni, Guy, et al. “Run-Time Optimization for Learned Controllers through Quantitative
Games.” 31st International Conference on Computer-Aided Verification, vol.
11561, Springer, 2019, pp. 630–49, doi:10.1007/978-3-030-25540-4_36.
short: G. Avni, R. Bloem, K. Chatterjee, T.A. Henzinger, B. Konighofer, S. Pranger,
in:, 31st International Conference on Computer-Aided Verification, Springer, 2019,
pp. 630–649.
conference:
end_date: 2019-07-18
location: New York, NY, United States
name: 'CAV: Computer Aided Verification'
start_date: 2019-07-13
corr_author: '1'
date_created: 2019-05-16T11:22:30Z
date_published: 2019-07-12T00:00:00Z
date_updated: 2025-04-15T06:26:05Z
day: '12'
ddc:
- '000'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/978-3-030-25540-4_36
external_id:
isi:
- '000491468000036'
file:
- access_level: open_access
checksum: c231579f2485c6fd4df17c9443a4d80b
content_type: application/pdf
creator: dernst
date_created: 2019-08-14T09:35:24Z
date_updated: 2020-07-14T12:47:31Z
file_id: '6816'
file_name: 2019_CAV_Avni.pdf
file_size: 659766
relation: main_file
file_date_updated: 2020-07-14T12:47:31Z
has_accepted_license: '1'
intvolume: ' 11561'
isi: 1
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 630-649
project:
- _id: 264B3912-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: M02369
name: Formal Methods meets Algorithmic Game Theory
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
publication: 31st International Conference on Computer-Aided Verification
publication_identifier:
isbn:
- '9783030255398'
issn:
- 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
scopus_import: '1'
status: public
title: Run-time optimization for learned controllers through quantitative 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: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 11561
year: '2019'
...
---
_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
arxiv: 1
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: 2025-07-10T11:53:47Z
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: Formal methods for the design and analysis of complex systems
- _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:
- 1557-735X
issn:
- 0004-5411
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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 66
year: '2019'
...
---
_id: '6822'
abstract:
- lang: eng
text: "In two-player games on graphs, the players move a token through a graph to
produce an infinite path, which determines the qualitative winner or quantitative
payoff of the game. In bidding games, in each turn, we hold an auction between
the two players to determine which player moves the token. Bidding games have
largely been studied with concrete bidding mechanisms that are variants of a first-price
auction: in each turn both players simultaneously submit bids, the higher\r\nbidder
moves the token, and pays his bid to the lower bidder in Richman bidding, to the
bank in poorman bidding, and in taxman bidding, the bid is split between the other
player and the bank according to a predefined constant factor. Bidding games are
deterministic games. They have an intriguing connection with a fragment of stochastic
games called \r\n randomturn games. We study, for the first time, a combination
of bidding games with probabilistic behavior; namely, we study bidding games that
are played on Markov decision processes, where the players bid for the right to
choose the next action, which determines the probability distribution according
to which the next vertex is chosen. We study parity and meanpayoff bidding games
on MDPs and extend results from the deterministic bidding setting to the probabilistic
one."
alternative_title:
- LNCS
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: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
- first_name: Petr
full_name: Novotny, Petr
last_name: Novotny
citation:
ama: 'Avni G, Henzinger TA, Ibsen-Jensen R, Novotny P. Bidding games on Markov decision
processes. In: Proceedings of the 13th International Conference of Reachability
Problems. Vol 11674. Springer; 2019:1-12. doi:10.1007/978-3-030-30806-3_1'
apa: 'Avni, G., Henzinger, T. A., Ibsen-Jensen, R., & Novotny, P. (2019). Bidding
games on Markov decision processes. In Proceedings of the 13th International
Conference of Reachability Problems (Vol. 11674, pp. 1–12). Brussels, Belgium:
Springer. https://doi.org/10.1007/978-3-030-30806-3_1'
chicago: Avni, Guy, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Petr Novotny. “Bidding
Games on Markov Decision Processes.” In Proceedings of the 13th International
Conference of Reachability Problems, 11674:1–12. Springer, 2019. https://doi.org/10.1007/978-3-030-30806-3_1.
ieee: G. Avni, T. A. Henzinger, R. Ibsen-Jensen, and P. Novotny, “Bidding games
on Markov decision processes,” in Proceedings of the 13th International Conference
of Reachability Problems, Brussels, Belgium, 2019, vol. 11674, pp. 1–12.
ista: 'Avni G, Henzinger TA, Ibsen-Jensen R, Novotny P. 2019. Bidding games on Markov
decision processes. Proceedings of the 13th International Conference of Reachability
Problems. RP: Reachability Problems, LNCS, vol. 11674, 1–12.'
mla: Avni, Guy, et al. “Bidding Games on Markov Decision Processes.” Proceedings
of the 13th International Conference of Reachability Problems, vol. 11674,
Springer, 2019, pp. 1–12, doi:10.1007/978-3-030-30806-3_1.
short: G. Avni, T.A. Henzinger, R. Ibsen-Jensen, P. Novotny, in:, Proceedings of
the 13th International Conference of Reachability Problems, Springer, 2019, pp.
1–12.
conference:
end_date: 2019-09-13
location: Brussels, Belgium
name: 'RP: Reachability Problems'
start_date: 2019-09-11
date_created: 2019-08-19T07:58:10Z
date_published: 2019-09-06T00:00:00Z
date_updated: 2025-09-10T10:39:56Z
day: '06'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-030-30806-3_1
external_id:
isi:
- '001333747500001'
file:
- access_level: open_access
checksum: 45ebbc709af2b247d28c7c293c01504b
content_type: application/pdf
creator: gavni
date_created: 2019-08-19T07:56:40Z
date_updated: 2020-07-14T12:47:41Z
file_id: '6823'
file_name: prob.pdf
file_size: 436635
relation: main_file
file_date_updated: 2020-07-14T12:47:41Z
has_accepted_license: '1'
intvolume: ' 11674'
isi: 1
language:
- iso: eng
month: '09'
oa: 1
oa_version: Submitted Version
page: 1-12
project:
- _id: 264B3912-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: M02369
name: Formal Methods meets Algorithmic Game Theory
- _id: 25F2ACDE-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
publication: ' Proceedings of the 13th International Conference of Reachability Problems'
publication_identifier:
isbn:
- 978-303030805-6
issn:
- 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
scopus_import: '1'
status: public
title: Bidding games on Markov decision processes
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 11674
year: '2019'
...
---
_id: '6884'
abstract:
- lang: eng
text: 'In two-player games on graphs, the players move a token through a graph to
produce a finite or infinite path, which determines the qualitative winner or
quantitative payoff of the game. We study bidding games in which the players bid
for the right to move the token. Several bidding rules were studied previously.
In Richman bidding, in each round, the players simultaneously submit bids, and
the higher bidder moves the token and pays the other player. Poorman bidding is
similar except that the winner of the bidding pays the "bank" rather than the
other player. Taxman bidding spans the spectrum between Richman and poorman bidding.
They are parameterized by a constant tau in [0,1]: portion tau of the winning
bid is paid to the other player, and portion 1-tau to the bank. While finite-duration
(reachability) taxman games have been studied before, we present, for the first
time, results on infinite-duration taxman games. It was previously shown that
both Richman and poorman infinite-duration games with qualitative objectives reduce
to reachability games, and we show a similar result here. Our most interesting
results concern quantitative taxman games, namely mean-payoff games, where poorman
and Richman bidding differ significantly. A central quantity in these games is
the ratio between the two players'' initial budgets. While in poorman mean-payoff
games, the optimal payoff of a player depends on the initial ratio, in Richman
bidding, the payoff depends only on the structure of the game. In both games the
optimal payoffs can be found using (different) probabilistic connections with
random-turn games in which in each turn, instead of bidding, a coin is tossed
to determine which player moves. While the value with Richman bidding equals the
value of a random-turn game with an un-biased coin, with poorman bidding, the
bias in the coin is the initial ratio of the budgets. We give a complete classification
of mean-payoff taxman games that is based on a probabilistic connection: the value
of a taxman bidding game with parameter tau and initial ratio r, equals the value
of a random-turn game that uses a coin with bias F(tau, r) = (r+tau * (1-r))/(1+tau).
Thus, we show that Richman bidding is the exception; namely, for every tau <1,
the value of the game depends on the initial ratio. Our proof technique simplifies
and unifies the previous proof techniques for both Richman and poorman bidding. '
alternative_title:
- LIPIcs
article_number: '11'
article_processing_charge: No
arxiv: 1
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: Dorde
full_name: Zikelic, Dorde
id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
last_name: Zikelic
orcid: 0000-0002-4681-1699
citation:
ama: 'Avni G, Henzinger TA, Zikelic D. Bidding mechanisms in graph games. In: Vol
138. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2019. doi:10.4230/LIPICS.MFCS.2019.11'
apa: 'Avni, G., Henzinger, T. A., & Zikelic, D. (2019). Bidding mechanisms in
graph games (Vol. 138). Presented at the MFCS: Mathematical Foundations of Computer
Science, Aachen, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.MFCS.2019.11'
chicago: Avni, Guy, Thomas A Henzinger, and Dorde Zikelic. “Bidding Mechanisms in
Graph Games,” Vol. 138. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.
https://doi.org/10.4230/LIPICS.MFCS.2019.11.
ieee: 'G. Avni, T. A. Henzinger, and D. Zikelic, “Bidding mechanisms in graph games,”
presented at the MFCS: Mathematical Foundations of Computer Science, Aachen, Germany,
2019, vol. 138.'
ista: 'Avni G, Henzinger TA, Zikelic D. 2019. Bidding mechanisms in graph games.
MFCS: Mathematical Foundations of Computer Science, LIPIcs, vol. 138, 11.'
mla: Avni, Guy, et al. Bidding Mechanisms in Graph Games. Vol. 138, 11, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2019, doi:10.4230/LIPICS.MFCS.2019.11.
short: G. Avni, T.A. Henzinger, D. Zikelic, in:, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2019.
conference:
end_date: 2019-08-30
location: Aachen, Germany
name: 'MFCS: Mathematical Foundations of Computer Science'
start_date: 2019-08-26
corr_author: '1'
date_created: 2019-09-18T08:04:26Z
date_published: 2019-08-01T00:00:00Z
date_updated: 2025-07-10T11:53:57Z
day: '01'
ddc:
- '004'
department:
- _id: ToHe
- _id: KrCh
doi: 10.4230/LIPICS.MFCS.2019.11
ec_funded: 1
external_id:
arxiv:
- '1905.03835'
file:
- access_level: open_access
checksum: 6346e116a4f4ed1414174d96d2c4fbd7
content_type: application/pdf
creator: kschuh
date_created: 2019-09-27T11:45:15Z
date_updated: 2020-07-14T12:47:42Z
file_id: '6913'
file_name: 2019_LIPIcs_Avni.pdf
file_size: 554457
relation: main_file
file_date_updated: 2020-07-14T12:47:42Z
has_accepted_license: '1'
intvolume: ' 138'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
call_identifier: H2020
grant_number: '665385'
name: International IST Doctoral Program
- _id: 264B3912-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: M02369
name: Formal Methods meets Algorithmic Game Theory
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
- _id: 25F2ACDE-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Rigorous Systems Engineering
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
related_material:
record:
- id: '9239'
relation: later_version
status: public
scopus_import: '1'
status: public
title: Bidding mechanisms in graph 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: 138
year: '2019'
...
---
_id: '6886'
abstract:
- lang: eng
text: 'In two-player games on graphs, the players move a token through a graph to
produce an infinite path, which determines the winner of the game. Such games
are central in formal methods since they model the interaction between a non-terminating
system and its environment. In bidding games the players bid for the right to
move the token: in each round, the players simultaneously submit bids, and the
higher bidder moves the token and pays the other player. Bidding games are known
to have a clean and elegant mathematical structure that relies on the ability
of the players to submit arbitrarily small bids. Many applications, however, require
a fixed granularity for the bids, which can represent, for example, the monetary
value expressed in cents. We study, for the first time, the combination of discrete-bidding
and infinite-duration games. Our most important result proves that these games
form a large determined subclass of concurrent games, where determinacy is the
strong property that there always exists exactly one player who can guarantee
winning the game. In particular, we show that, in contrast to non-discrete bidding
games, the mechanism with which tied bids are resolved plays an important role
in discrete-bidding games. We study several natural tie-breaking mechanisms and
show that, while some do not admit determinacy, most natural mechanisms imply
determinacy for every pair of initial budgets. '
alternative_title:
- LIPIcs
article_number: '20'
article_processing_charge: No
arxiv: 1
author:
- first_name: Milad
full_name: Aghajohari, Milad
last_name: Aghajohari
- 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
citation:
ama: 'Aghajohari M, Avni G, Henzinger TA. Determinacy in discrete-bidding infinite-duration
games. In: Vol 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2019. doi:10.4230/LIPICS.CONCUR.2019.20'
apa: 'Aghajohari, M., Avni, G., & Henzinger, T. A. (2019). Determinacy in discrete-bidding
infinite-duration games (Vol. 140). Presented at the CONCUR: Conference on Concurrency
Theory, Amsterdam, Netherlands: Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
https://doi.org/10.4230/LIPICS.CONCUR.2019.20'
chicago: Aghajohari, Milad, Guy Avni, and Thomas A Henzinger. “Determinacy in Discrete-Bidding
Infinite-Duration Games,” Vol. 140. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2019. https://doi.org/10.4230/LIPICS.CONCUR.2019.20.
ieee: 'M. Aghajohari, G. Avni, and T. A. Henzinger, “Determinacy in discrete-bidding
infinite-duration games,” presented at the CONCUR: Conference on Concurrency Theory,
Amsterdam, Netherlands, 2019, vol. 140.'
ista: 'Aghajohari M, Avni G, Henzinger TA. 2019. Determinacy in discrete-bidding
infinite-duration games. CONCUR: Conference on Concurrency Theory, LIPIcs, vol.
140, 20.'
mla: Aghajohari, Milad, et al. Determinacy in Discrete-Bidding Infinite-Duration
Games. Vol. 140, 20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019,
doi:10.4230/LIPICS.CONCUR.2019.20.
short: M. Aghajohari, G. Avni, T.A. Henzinger, in:, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2019.
conference:
end_date: 2019-08-30
location: Amsterdam, Netherlands
name: 'CONCUR: Conference on Concurrency Theory'
start_date: 2019-08-27
corr_author: '1'
date_created: 2019-09-18T08:06:58Z
date_published: 2019-08-01T00:00:00Z
date_updated: 2025-07-10T11:53:58Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPICS.CONCUR.2019.20
external_id:
arxiv:
- '1905.03588'
file:
- access_level: open_access
checksum: 4df6d3575c506edb17215adada03cc8e
content_type: application/pdf
creator: kschuh
date_created: 2019-09-27T12:21:38Z
date_updated: 2020-07-14T12:47:43Z
file_id: '6915'
file_name: 2019_LIPIcs_Aghajohari.pdf
file_size: 741425
relation: main_file
file_date_updated: 2020-07-14T12:47:43Z
has_accepted_license: '1'
intvolume: ' 140'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _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_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: Determinacy in discrete-bidding infinite-duration games
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/3.0/legalcode
name: Creative Commons Attribution 3.0 Unported (CC BY 3.0)
short: CC BY (3.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 140
year: '2019'
...
---
_id: '6005'
abstract:
- lang: eng
text: Network games are widely used as a model for selfish resource-allocation problems.
In the classicalmodel, each player selects a path connecting her source and target
vertices. The cost of traversingan edge depends on theload; namely, number of
players that traverse it. Thus, it abstracts the factthat different users may
use a resource at different times and for different durations, which playsan important
role in determining the costs of the users in reality. For example, when transmittingpackets
in a communication network, routing traffic in a road network, or processing a
task in aproduction system, actual sharing and congestion of resources crucially
depends on time.In [13], we introducedtimed network games, which add a time component
to network games.Each vertexvin the network is associated with a cost function,
mapping the load onvto theprice that a player pays for staying invfor one time
unit with this load. Each edge in thenetwork is guarded by the time intervals
in which it can be traversed, which forces the players tospend time in the vertices.
In this work we significantly extend the way time can be referred toin timed network
games. In the model we study, the network is equipped withclocks, and, as intimed
automata, edges are guarded by constraints on the values of the clocks, and their
traversalmay involve a reset of some clocks. We argue that the stronger model
captures many realisticnetworks. The addition of clocks breaks the techniques
we developed in [13] and we developnew techniques in order to show that positive
results on classic network games carry over to thestronger timed setting.
alternative_title:
- LIPIcs
article_number: '23'
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: Shibashis
full_name: Guha, Shibashis
last_name: Guha
- first_name: Orna
full_name: Kupferman, Orna
last_name: Kupferman
citation:
ama: 'Avni G, Guha S, Kupferman O. Timed network games with clocks. In: Vol 117.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2018. doi:10.4230/LIPICS.MFCS.2018.23'
apa: 'Avni, G., Guha, S., & Kupferman, O. (2018). Timed network games with clocks
(Vol. 117). Presented at the MFCS: Mathematical Foundations of Computer Science,
Liverpool, United Kingdom: Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
https://doi.org/10.4230/LIPICS.MFCS.2018.23'
chicago: Avni, Guy, Shibashis Guha, and Orna Kupferman. “Timed Network Games with
Clocks,” Vol. 117. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. https://doi.org/10.4230/LIPICS.MFCS.2018.23.
ieee: 'G. Avni, S. Guha, and O. Kupferman, “Timed network games with clocks,” presented
at the MFCS: Mathematical Foundations of Computer Science, Liverpool, United Kingdom,
2018, vol. 117.'
ista: 'Avni G, Guha S, Kupferman O. 2018. Timed network games with clocks. MFCS:
Mathematical Foundations of Computer Science, LIPIcs, vol. 117, 23.'
mla: Avni, Guy, et al. Timed Network Games with Clocks. Vol. 117, 23, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2018, doi:10.4230/LIPICS.MFCS.2018.23.
short: G. Avni, S. Guha, O. Kupferman, in:, Schloss Dagstuhl - Leibniz-Zentrum für
Informatik, 2018.
conference:
end_date: 2018-08-31
location: Liverpool, United Kingdom
name: 'MFCS: Mathematical Foundations of Computer Science'
start_date: 2018-08-27
date_created: 2019-02-14T14:12:09Z
date_published: 2018-08-01T00:00:00Z
date_updated: 2025-07-10T12:01:59Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.4230/LIPICS.MFCS.2018.23
file:
- access_level: open_access
checksum: 41ab2ae9b63f5eb49fa995250c0ba128
content_type: application/pdf
creator: dernst
date_created: 2019-02-14T14:22:04Z
date_updated: 2020-07-14T12:47:15Z
file_id: '6007'
file_name: 2018_LIPIcs_Avni.pdf
file_size: 542889
relation: main_file
file_date_updated: 2020-07-14T12:47:15Z
has_accepted_license: '1'
intvolume: ' 117'
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: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
- _id: 264B3912-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: M02369
name: Formal Methods meets Algorithmic Game Theory
publication_identifier:
issn:
- 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
related_material:
record:
- id: '963'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Timed network games with clocks
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: 117
year: '2018'
...
---
_id: '6006'
abstract:
- lang: eng
text: 'Network games (NGs) are played on directed graphs and are extensively used
in network design and analysis. Search problems for NGs include finding special
strategy profiles such as a Nash equilibrium and a globally-optimal solution.
The networks modeled by NGs may be huge. In formal verification, abstraction has
proven to be an extremely effective technique for reasoning about systems with
big and even infinite state spaces. We describe an abstraction-refinement methodology
for reasoning about NGs. Our methodology is based on an abstraction function that
maps the state space of an NG to a much smaller state space. We search for a global
optimum and a Nash equilibrium by reasoning on an under- and an over-approximation
defined on top of this smaller state space. When the approximations are too coarse
to find such profiles, we refine the abstraction function. We extend the abstraction-refinement
methodology to labeled networks, where the objectives of the players are regular
languages. Our experimental results demonstrate the effectiveness of the methodology. '
article_number: '39'
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: Shibashis
full_name: Guha, Shibashis
last_name: Guha
- first_name: Orna
full_name: Kupferman, Orna
last_name: Kupferman
citation:
ama: Avni G, Guha S, Kupferman O. An abstraction-refinement methodology for reasoning
about network games. Games. 2018;9(3). doi:10.3390/g9030039
apa: Avni, G., Guha, S., & Kupferman, O. (2018). An abstraction-refinement methodology
for reasoning about network games. Games. MDPI. https://doi.org/10.3390/g9030039
chicago: Avni, Guy, Shibashis Guha, and Orna Kupferman. “An Abstraction-Refinement
Methodology for Reasoning about Network Games.” Games. MDPI, 2018. https://doi.org/10.3390/g9030039.
ieee: G. Avni, S. Guha, and O. Kupferman, “An abstraction-refinement methodology
for reasoning about network games,” Games, vol. 9, no. 3. MDPI, 2018.
ista: Avni G, Guha S, Kupferman O. 2018. An abstraction-refinement methodology for
reasoning about network games. Games. 9(3), 39.
mla: Avni, Guy, et al. “An Abstraction-Refinement Methodology for Reasoning about
Network Games.” Games, vol. 9, no. 3, 39, MDPI, 2018, doi:10.3390/g9030039.
short: G. Avni, S. Guha, O. Kupferman, Games 9 (2018).
date_created: 2019-02-14T14:17:54Z
date_published: 2018-09-01T00:00:00Z
date_updated: 2025-07-10T11:49:38Z
day: '01'
ddc:
- '004'
department:
- _id: ToHe
doi: 10.3390/g9030039
file:
- access_level: open_access
checksum: 749d65ca4ce74256a029d9644a1b1cb0
content_type: application/pdf
creator: kschuh
date_created: 2019-02-14T14:20:31Z
date_updated: 2020-07-14T12:47:16Z
file_id: '6008'
file_name: 2018_MDPI_Avni.pdf
file_size: 505155
relation: main_file
file_date_updated: 2020-07-14T12:47:16Z
has_accepted_license: '1'
intvolume: ' 9'
issue: '3'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
project:
- _id: 264B3912-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: M02369
name: Formal Methods meets Algorithmic Game Theory
- _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: Formal methods for the design and analysis of complex systems
publication: Games
publication_identifier:
issn:
- 2073-4336
publication_status: published
publisher: MDPI
quality_controlled: '1'
related_material:
record:
- id: '1003'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: An abstraction-refinement methodology for reasoning about network 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: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9
year: '2018'
...
---
_id: '5788'
abstract:
- lang: eng
text: In two-player games on graphs, the players move a token through a graph to
produce an infinite path, which determines the winner or payoff of the game. Such
games are central in formal verification since they model the interaction between
a non-terminating system and its environment. We study bidding games in which
the players bid for the right to move the token. Two bidding rules have been defined.
In Richman bidding, in each round, the players simultaneously submit bids, and
the higher bidder moves the token and pays the other player. Poorman bidding is
similar except that the winner of the bidding pays the “bank” rather than the
other player. While poorman reachability games have been studied before, we present,
for the first time, results on infinite-duration poorman games. A central quantity
in these games is the ratio between the two players’ initial budgets. The questions
we study concern a necessary and sufficient ratio with which a player can achieve
a goal. For reachability objectives, such threshold ratios are known to exist
for both bidding rules. We show that the properties of poorman reachability games
extend to complex qualitative objectives such as parity, similarly to the Richman
case. Our most interesting results concern quantitative poorman games, namely
poorman mean-payoff games, where we construct optimal strategies depending on
the initial ratio, by showing a connection with random-turn based games. The connection
in itself is interesting, because it does not hold for reachability poorman games.
We also solve the complexity problems that arise in poorman bidding games.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
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: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
citation:
ama: 'Avni G, Henzinger TA, Ibsen-Jensen R. Infinite-duration poorman-bidding games.
In: Vol 11316. Springer; 2018:21-36. doi:10.1007/978-3-030-04612-5_2'
apa: 'Avni, G., Henzinger, T. A., & Ibsen-Jensen, R. (2018). Infinite-duration
poorman-bidding games (Vol. 11316, pp. 21–36). Presented at the 14th International
Conference on Web and Internet Economics, WINE, Oxford, UK: Springer. https://doi.org/10.1007/978-3-030-04612-5_2'
chicago: Avni, Guy, Thomas A Henzinger, and Rasmus Ibsen-Jensen. “Infinite-Duration
Poorman-Bidding Games,” 11316:21–36. Springer, 2018. https://doi.org/10.1007/978-3-030-04612-5_2.
ieee: G. Avni, T. A. Henzinger, and R. Ibsen-Jensen, “Infinite-duration poorman-bidding
games,” presented at the 14th International Conference on Web and Internet Economics,
WINE, Oxford, UK, 2018, vol. 11316, pp. 21–36.
ista: Avni G, Henzinger TA, Ibsen-Jensen R. 2018. Infinite-duration poorman-bidding
games. 14th International Conference on Web and Internet Economics, WINE, LNCS,
vol. 11316, 21–36.
mla: Avni, Guy, et al. Infinite-Duration Poorman-Bidding Games. Vol. 11316,
Springer, 2018, pp. 21–36, doi:10.1007/978-3-030-04612-5_2.
short: G. Avni, T.A. Henzinger, R. Ibsen-Jensen, in:, Springer, 2018, pp. 21–36.
conference:
end_date: 2018-12-17
location: Oxford, UK
name: 14th International Conference on Web and Internet Economics, WINE
start_date: 2018-12-15
date_created: 2018-12-30T22:59:14Z
date_published: 2018-11-21T00:00:00Z
date_updated: 2026-04-16T09:54:39Z
day: '21'
department:
- _id: ToHe
doi: 10.1007/978-3-030-04612-5_2
external_id:
arxiv:
- '1804.04372'
isi:
- '000865933000002'
intvolume: ' 11316'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1804.04372
month: '11'
oa: 1
oa_version: Preprint
page: 21-36
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: Formal methods for the design and analysis of complex systems
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_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_identifier:
isbn:
- '9783030046118'
issn:
- 0302-9743
publisher: Springer
quality_controlled: '1'
scopus_import: '1'
status: public
title: Infinite-duration poorman-bidding games
type: conference
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
volume: 11316
year: '2018'
...