Gal Amram: Multi-Process Systems, Synchronization and Synthesis

The design of correct and efficient multi-process systems, in which processes are executed in parallel, and influence each other, is a significant challenge for software engineers. In this talk, I will survey two of my research projects, that tackle this aim from different aspects. The first part concerns process-synchronization. I will present the signaling problem, proposed by Marcus Aguilera, Eli Gafni, and Leslie Lamport. Then, I will provide a solution to that problem by presenting an efficient signaling algorithm, as well as applications thereof. The second part concerns reactive synthesis. GR(1) is a fragment of linear temporal logic for which a feasible synthesis algorithm exists. I will present GR(1)*, an augmentation of GR(1) with existential guarantees. GR(1)* strictly extends the expressive power of GR(1), yet the time complexity of our GR(1)*-synthesis technique is asymptotically the same as of the known GR(1)-synthesis technique. Finally, I will suggest some future research directions that integrate the two discussed aspects.
The results I will survey are part of joint works with Uri Abraham, Shahar Maoz, and Or Pistiner.