Synthesis of Coordination Programs from Linear Temporal Specifications
This paper focuses on coordination problems, and presents a method for synthesizing a reactive program which coordinates the actions of a group of other programs, so that the combined system satisfies a temporal specification of its desired long-term behavior. Traditionally, reactive synthesis has been applied to the construction of stateful hardware circuits. This work is motivated by applications to other domains, such as the control of a network of sensors and devices, and the management of a heterogeneous team of robots. These applications require coordination between the individual sensors, devices, or robots. The mathematical model represents such entities in Hoare’s CSP model, as a network of interacting processes called the environment. Given a temporal specification, the synthesis method constructs a coordinator process (if one exists) that guides the actions of the environment processes so that the combined system is deadlock-free and satisfies the given specification. The main technical challenge is that the coordinator may have only partial knowledge of the environment state, due to non-determinism at the environment interface, and internal environment actions that are hidden from a coordinator. This is the first method to handle both sources of partial knowledge for arbitrary linear temporal logic specifications. It is also shown that this synthesis problem is PSPACE-hard in the size of the environment. A prototype implementation is able to synthesize compact solutions for a number of coordination specifications.
Coordination synthesis (AsynchSynth.pdf) | 861KiB |