Abstract
Reactive Synthesis has traditionally been applied to the construction of a stateful hardware circuit. This talk is motivated by future applications to other domains, such as the IoT (the Internet of Things) and robotics, where it is necessary to coordinate the actions of multiple sensors, devices, and robots to carry out a task. Given a network of interacting agents, called an environment, and a temporal specification of long-term behavior, the synthesis problem is to construct a coordinator process (if one exists) that guides the actions of the environment agents so that the combined system is deadlock-free and satisfies the given specification. The main technical challenge is that a coordinator may have only partial information of the environment state, due to non-determinism within the environment and internal environment actions that are hidden from the coordinator. In this talk, I will present a method to handle both sources of partial information and to do so for arbitrary linear temporal logic specifications.