Write a Blog >>
Thu 23 Jan 2020 10:30 - 10:51 at Ile de France III (IDF III) - Synthesis Chair(s): Mohsen Lesani

This paper focuses on coordination problems, and presents a method for synthesizing a reactive program which coordinates the actions of a group of other programs, so that the combined system satisfies a temporal specification of its desired long-term behavior. Traditionally, reactive synthesis has been applied to the construction of stateful hardware circuits. This work is motivated by applications to other domains, such as the control of a network of sensors and devices, and the management of a heterogeneous team of robots. These applications require coordination between the individual sensors, devices, or robots. The mathematical model represents such entities in Hoare’s CSP model, as a network of interacting processes called the environment. Given a temporal specification, the synthesis method constructs a coordinator process (if one exists) that guides the actions of the environment processes so that the combined system is deadlock-free and satisfies the given specification. The main technical challenge is that the coordinator may have only partial knowledge of the environment state, due to non-determinism at the environment interface, and internal environment actions that are hidden from a coordinator. This is the first method to handle both sources of partial knowledge for arbitrary linear temporal logic specifications. It is also shown that this synthesis problem is PSPACE-hard in the size of the environment. A prototype implementation is able to synthesize compact solutions for a number of coordination specifications.

Coordination synthesis (AsynchSynth.pdf)861KiB

Thu 23 Jan

Displayed time zone: Saskatchewan, Central America change

10:30 - 11:35
SynthesisResearch Papers at Ile de France III (IDF III)
Chair(s): Mohsen Lesani University of California, Riverside
10:30
21m
Talk
Synthesis of Coordination Programs from Linear Temporal Specifications
Research Papers
Suguman Bansal Rice University, USA, Kedar Namjoshi Bell Labs, Nokia, Yaniv Sa'ar Nokia Bell Labs, Kfar Saba, Israel
Link to publication DOI Media Attached File Attached
10:51
21m
Talk
Augmented Example-based Synthesis using Relational Perturbation Properties
Research Papers
Shengwei An Purdue University, Rishabh Singh Google Brain, Sasa Misailovic University of Illinois at Urbana-Champaign, Roopsha Samanta Purdue University
Link to publication DOI Media Attached File Attached
11:13
21m
Talk
Provenance-Guided Synthesis of Datalog Programs
Research Papers
Mukund Raghothaman University of Southern California, Jonathan Mendelson University of Pennsylvania, David Zhao The University of Sydney, Mayur Naik University of Pennsylvania, Bernhard Scholz University of Sydney, Australia
Link to publication DOI Media Attached File Attached