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
Times are displayed in time zone: Saskatchewan, Central America change

10:30 - 11:35: SynthesisResearch Papers at Ile de France III (IDF III)
Chair(s): Mohsen LesaniUniversity of California, Riverside
10:30 - 10:51
Talk
Synthesis of Coordination Programs from Linear Temporal Specifications
Research Papers
Suguman BansalRice University, USA, Kedar NamjoshiBell Labs, Nokia, Yaniv Sa'arNokia Bell Labs, Kfar Saba, Israel
Link to publication DOI Media Attached File Attached
10:51 - 11:13
Talk
Augmented Example-based Synthesis using Relational Perturbation Properties
Research Papers
Shengwei AnPurdue University, Rishabh SinghGoogle Brain, Sasa MisailovicUniversity of Illinois at Urbana-Champaign, Roopsha SamantaPurdue University
Link to publication DOI Media Attached File Attached
11:13 - 11:35
Talk
Provenance-Guided Synthesis of Datalog Programs
Research Papers
Mukund RaghothamanUniversity of Southern California, Jonathan MendelsonUniversity of Pennsylvania, David ZhaoThe University of Sydney, Mayur NaikUniversity of Pennsylvania, Bernhard ScholzUniversity of Sydney, Australia
Link to publication DOI Media Attached File Attached