Synthesis of Coordination Programs from Linear Temporal Specifications

In several settings, it is necessary to coordinate the actions of a group of concurrently executing actors in order to fulfill a task. This work proposes a new algorithm for fully automatic construction (i.e., ``synthesis'') of a coordination program, in a setting where the actors are represented by finite-state, reactive processes and the task is specified as a propositional linear temporal property. If the task specification is realizable, the algorithm produces a finite-state coordinator program that guides the actors so that every joint behavior has the required property. The algorithm significantly extends prior work to resolve both partial information and asynchrony, while handling arbitrary linear temporal logic specifications. Partial information arises when actors change state with interactions that are invisible to a coordinator; asynchrony arises when the specification depends on these hidden interactions. The solution uses automata-theoretic methods, implemented symbolically in a prototype tool.