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: (GMT-06:00) Saskatchewan, Central America change

POPL-2020-Research-Papers
10:30 - 11:35: Research Papers - Synthesis at Ile de France III (IDF III)
Chair(s): Mohsen LesaniUniversity of California, Riverside
POPL-2020-Research-Papers10:30 - 10:51
Talk
Suguman BansalRice University, USA, Kedar NamjoshiBell Labs, Nokia, Yaniv Sa'arNokia Bell Labs, Kfar Saba, Israel
Link to publication DOI Media Attached File Attached
POPL-2020-Research-Papers10:51 - 11:13
Talk
Shengwei AnPurdue University, Rishabh SinghGoogle Brain, Sasa MisailovicUniversity of Illinois at Urbana-Champaign, Roopsha SamantaPurdue University
Link to publication DOI Media Attached File Attached
POPL-2020-Research-Papers11:13 - 11:35
Talk
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