iBet uBet web content aggregator. Adding the entire web to your favor.
iBet uBet web content aggregator. Adding the entire web to your favor.



Link to original content: http://hal.inria.fr/hal-03641392v1/dcterms
hal-03641392 https://hal.science/hal-03641392 arxiv:2107.04081 doi:10.4230/LIPIcs.FSTTCS.2021.41 [CNRS] CNRS - Centre national de la recherche scientifique [INRIA] INRIA - Institut National de Recherche en Informatique et en Automatique [ENS-CACHAN] Ecole Normale Supérieure de Cachan [CENTRALESUPELEC] Ecole CentraleSupélec [UNIV-PARIS-SACLAY] Université Paris-Saclay [INRIA-AUT] Inria autres [UNIVERSITE-PARIS-SACLAY] Université Paris-Saclay [ENS-PARIS-SACLAY] Ecole Normale Supérieure paris-Saclay [ENS-PSACLAY] Ecole Normale Supérieure Paris-Saclay [GS-COMPUTER-SCIENCE] Graduate School Computer Science [LMF] Laboratoire Méthodes Formelles [LMF-MCS] Model-checking et synthèse From Local to Global Determinacy in Concurrent Graph Games Bordais, Benjamin Bouyer, Patricia Le Roux, Stéphane [INFO] Computer Science [cs] [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO] [INFO.INFO-GT] Computer Science [cs]/Computer Science and Game Theory [cs.GT] COMM Concurrent games Game forms Local interaction In general, finite concurrent two-player reachability games are only determined in a weak sense: the supremum probability to win can be approached via stochastic strategies, but cannot be realized.We introduce a class of concurrent games that are determined in a much stronger sense, and in a way, it is the largest class with this property. To this end, we introduce the notion of local interaction at a state of a graph game: it is a game form whose outcomes (i.e. a table whose entries) are the next states, which depend on the concurrent actions of the players. By definition, a game form is determined iff it always yields games that are determined via deterministic strategies when used as a local interaction in a Nature-free, one-shot reachability game. We show that if all the local interactions of a graph game with Borel objective are determined game forms, the game itself is determined: if Nature does not play, one player has a winning strategy; if Nature plays, both players have deterministic strategies that maximize the probability to win. This constitutes a clear-cut separation: either a game form behaves poorly already when used alone with basic objectives, or it behaves well even when used together with other well-behaved game forms and complex objectives.Existing results for positional and finite-memory determinacy in turn-based games are extended this way to concurrent games with determined local interactions (CG-DLI). 2021-12-15 en FSTTCS'21 on line, India