Synthesis of Reactive Systems

Synthesis of reactive systems is a research direction inspired by Church's realisability problem. It focuses on systems that receive a constant stream of inputs from an environment, and must, for each input, produce some output. Specifically, we are given a logical specification that dictates how the system must react to the inputs, and we must construct a system that satisfies the specification for all possible inputs that the environment could provide. While the verification problem (the validation or refutation of the correctness of such a system) has gained many algorithmic solutions and various successful tools, the synthesis problem has had fewer results. We focus on the classical approach by Pnueli and Rosner, which links synthesis to emptiness games of automata and the treatment of incomplete information. We will discuss why these approaches require determinisation and how the resulting automata can be simplified with respect to their acceptance mechanism. For pleasure, we might look into a connection between complexity classes and the existence of succinct control strategies.

Oh, and we'll look for a PostDoc on a parity games project soon -- pure pleasure! If your PhD is nearing an end or your time as a PDRA is coming to a close, there is no better way to spend 3 years!