In the construction of reactive systems, like communication protocols or control systems, a central aim is to put the synthesis and the verification of hardware and software on a mathematical basis which is both firm and practical. A characteristic feature of such systems is their perpetual interaction with the environment as well as their non-terminating behaviour. The theory of infinite duration games offers many appealing results under this prospect [see e.g. Automata, Logics and Infinite Games: a Guide to Current Research. Gradel, Thomas, Wilke (2004)].
For instance, consider the following communication network problem. Suppose we have data stored on each node of a network and we want to continuously update all nodes with consistent data: often one requirement is to share key information between all nodes of a network; this can be done by having a data packet of current information continuously going through all nodes. Unfortunately not all routing choices are always under our control, some of them may be controlled by the network environment, which could play against us. This is essentially an infinite 2-player pebble game played on an arena, i.e. a finite directed simple graph in which the vertices are divided into two classes, and , where Player wants to visit all vertices infinitely often by moving the pebble on them, while Player works against. This is called Update Game (UG) in [Dinneen and Khoussainov (1999)].
In this work, we introduce and study a refined notion of reachability for arenas, named trap-reachability, where Player attempts to reach vertices without leaving a prescribed subset , while Player works against. It is shown that every arena decomposes into strongly-trap-connected components (STCCs).
Our main result is a linear time algorithm for computing this unique decomposition.
Both the graph structures and the algorithm generalize the classical decomposition of a directed graph into its strongly-connected components (SCCs). The algorithm builds on a generalization of the depth-first search (DFS), taking inspiration from Tarjan’s SCCs classical algorithm. The structures of palm-trees and jungles described in Tarjan’s original paper need to be revisited and generalized (i.e. tr-palm-trees and tr-jungles) in order to handle the 2-player infinite pebble game’s setting.
This theory has direct applications in solving Update Games (UGs) faster. Dinneen and Khoussainov showed in 1999 that deciding who’s the winner in a given UG costs time, where is the number of vertices and is that of arcs. We solve that problem in linear time. The result is obtained by observing that the UG is a win for Player if and only if the arena comprises one single STCC. It is also observed that the tr-palm-tree returned by the algorithm encodes routing information that an -space agent can consult to win the UG in time per move. With this, the polynomial-time complexity for deciding Explicit McNaughton-Muller Games is also improved, from cubic to quadratic.
Download: manuscript, presentation.