Synthesis Of Asynchronous Reactive Programs From Temporal Specifications

Asynchronous interactions are ubiquitous in computing systems and complicate design and programming. Automatic construction ("synthesis") of asynchronous programs from specifications could help ease this difficulty, but known methods are intractable in practice. This work develops substantially simpler methods for synthesis. An exponentially more compact automaton construction is developed for the reduction of asynchronous to synchronous synthesis. Furthermore, it is shown that for several useful classes of temporal properties, automaton-based methods can be avoided altogether and replaced with simpler Boolean constraint solving. Experiments with a prototype implementation of the new methods demonstrate practical feasibility.