FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Synthesis Of Asynchronous Reactive Programs From Temporal Specifications

Authors: Suguman Bansal, Kedar Namjoshi and Yaniv Sa'Ar

Paper Information

Title:Synthesis Of Asynchronous Reactive Programs From Temporal Specifications
Authors:Suguman Bansal, Kedar Namjoshi and Yaniv Sa'Ar
Proceedings:CAV All Papers
Editors: Georg Weissenbacher, Hana Chockler and Igor Konnov
Keywords:synthesis, asynchronous, temporal logic, QBF
Abstract:

ABSTRACT. Asynchronous interactions are ubiquitous in computing systems and complicate design and programming. Automatic construction (``synthesis'') of asynchronous programs from specifications could ease the difficulty, but known methods are intractable in practice. This work develops substantially simpler methods for asynchronous synthesis. An exponentially more compact automaton construction is developed for the reduction of asynchronous to synchronous synthesis. Experiments with a prototype implementation of the new method demonstrate practical feasibility. 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.

Pages:19
Talk:Jul 14 17:30 (Session 99A: Synthesis)
Paper: