Authors: Uri Klein, Nir Piterman, and Amir Pnueli

Title: Effective Synthesis of Asynchronous Systems from GR(1) Specifications

Abstract:
We consider automatic synthesis from linear temporal logic
specifications for asynchronous systems. We aim the produced reactive
systems to be used as software in a multi-threaded environment. We ex-
tend previous reduction of asynchronous synthesis to synchronous syn-
thesis to the setting of multiple input and multiple output variables.
Much like synthesis for synchronous designs, this solution is not practical
as it requires determinization of automata on infinite words and solution
of complicated games. We follow advances in synthesis of synchronous
designs, which restrict the handled specifications but achieve scalabil-
ity and efficiency. We propose a heuristic that, in some cases, maintains
scalability for asynchronous synthesis. Our heuristic can prove that spec-
ifications are realizable and extract designs. This is done by a reduction
to synchronous synthesis that is inspired by the theoretical reduction.