Translating Asynchronous Games for Distributed Synthesis
Raven Beutner
Synthesis is the ambitious task of automatically generating an implementation fulfilling a given specification against all possible inputs or proving the unrealizability of the specification, i.e, the absence of a fulfilling implementation. As the user does not need to come up with an implementation herself but gets presented with a, by default, correct one, synthesis offers maximal convenience. In distributed systems, individual processes act both locally and communicate with one another without having full information about the global state of the system. For distributed synthesis we hence try to generate a family of individual implementations, that governs the processes such that the system as a whole satisfies a given objective, independent of received inputs. We explicitly consider systems where the processes share no information when acting concurrently but exchange their entire causal past, i.e., all information known to them, upon communication.
So far the synthesis problem for this class of systems has been studied in terms of either Petri games or control games. In both the overall system is modelled as either a Petri net or an asynchronous automaton and the synthesis problem consists of finding a restriction on the global behavior that accomplishes a given objective. Petri games partition the places of a net as either system or environment and allow only tokens on system places to forbid transitions, while tokens on environment places are regarded as adversary players that cannot be controlled. By contrast, control games split the actions of an asynchronous automaton as either controllable or uncontrollable. Individual processes can refuse controllable actions and thereby restrict the executions of the automaton, while uncontrollable ones cannot be thwarted and have to be accounted for in any execution.
In both frameworks it is an open question whether the existence of a correct implementation for the system is decidable. There are, however, interesting classes for which decision procedures exist. The precise connection between both games and therefore the question whether existing results can be transferred to the other type was, so far, unknown.
In this thesis we establish the first formal connection of Petri games and control games by providing exponential translations in both directions. We show that our translations yield structurally equivalent games, in the sense that they admit weak bisimilar implementations. In addition to our upper bound we provide lower bounds in both directions showing an intrinsic trade off between the two frameworks. Our translation allow for the transfer of existing decidability results to the respective other game type. We exemplary outline the newly identified decidable classes of control games where at most one process comprises controllable behavior as well as Petri games with acyclic communication architectures.
Bachelor Thesis.