zbMATH — the first resource for mathematics

Alternating reachability games with behavioral and revenue objectives. (English) Zbl 1415.68150
Barthe, Gilles (ed.) et al., LPAR-22. 22nd international conference on logic for programming, artificial intelligence and reasoning, Awassa, Ethiopia, November 17–21, 2018. Selected papers. Manchester: EasyChair. EPiC Ser. Comput. 57, 498-514 (2018).
Summary: We introduce and study alternating reachability games with tolls (ARGTs). An ARGT is a multi-player game played on a directed graph. Each player has a source vertex and a set of target vertices. The vertices of the graph are partitioned among the players. Thus, each player owns a subset of the vertices. In the beginning of the game, each player places a token on her source vertex. Whenever a token reaches a vertex \(v\), the owner of the token pays a toll to the owner of vertex \(v\), who directs the token to one of the successors of \(v\). The objective of each player combines a reachability objective with a minimal-cost maximal-profit objective. For the first, the token of the player needs to reach one of her target vertices. For the second, the player aims at decreasing the toll she pays to other players and increasing the toll paid to her due to visits in vertices she owns. ARGTs model settings in which the vertices are owned by entities who also use the network; for example, communication networks in which service providers own the routers and send messages. ARGTs also offer an extension of rational synthesis with rewards to actions. To the best of our knowledge, this model is the first to combine behavioral and revenue objectives.
We study different instances of the game, distinguishing between various network topologies and various levels of overlap among the reachability objectives of the players. We analyze the stability of ARGTs, characterizing instances for which a Nash equilibrium is guaranteed to exist, and studying its inefficiency. We also analyze the problems of finding optimal strategies for the players and for the society as a whole.
For the entire collection see [Zbl 1407.68021].
68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
91A80 Applications of game theory
Full Text: DOI