Network-Formation Games with Regular Objectives
===============================================

Classical network-formation games are played on a directed
graph. Players have reachability objectives, and each player has to
select a path satisfying his objective. Edges are associated with
costs, and when several players use the same edge, they evenly share
its cost. The theoretical and practical aspects of network-formation
games have been extensively studied and are well understood. We
introduce and study {\em network-formation games with regular
objectives}. In our setting, the edges are labeled by alphabet letters
and the objective of each player is a regular language over the
alphabet of labels, given by means of an automaton or a temporal-logic
formula. Thus, beyond reachability properties, a player may restrict
attention to paths that satisfy certain properties, referring, for
example, to the providers of the traversed edges, the actions
associated with them, their quality of service, security, etc.

Unlike the case of network-formation games with reachability
objectives, here the paths selected by the players need not be simple,
thus a player may traverse some transitions several times. Edge costs
are shared by the players with the share being proportional to the
number of times the transition is traversed. We study the existence of
a pure Nash equilibrium (NE), convergence of best-response-dynamics,
the complexity of finding the social optimum, and the inefficiency of
a NE compared to a social-optimum solution. We examine several classes
of networks (for example, networks with uniform edge costs, or
alphabet of size $1$) and several classes of regular objectives. We
show that many properties of classical network-formation games are no
longer valid in our game. In particular, a pure NE might not exist and
the Price of Stability equals the number of players (as opposed to
logarithmic in the number of players in the classic setting, where a
pure NE always exists). In light of these results, we also present
special cases for which the resulting game is more stable.