Write a Blog >>
APLAS 2020
Mon 30 November - Wed 2 December 2020
Wed 2 Dec 2020 16:00 - 16:30 at online - Synthesis and Program Transformation Chair(s): Cristina David

Parameterized synthesis offers a solution to the problem of constructing correct and verified controllers for parameterized systems. Such systems occur naturally in practice (e.g., in the form of distributed protocols where the amount of processes is often unknown at design time and the protocol must work regardless of the number of processes participating). In this paper, we present a novel learning-based approach to the synthesis of reactive controllers for parameterized systems from safety specifications. We use the framework of regular model checking to model the synthesis problem as an infinite-duration two-player game and show how one can utilize Angluin’s well-known $L^{\ast}$ algorithm to learn correct-by-design controllers. This approach results in a synthesis procedure that is conceptually simpler than existing synthesis methods with a completeness guarantee,
whenever a winning strategy can be expressed by a regular set. We have implemented our algorithm in a tool called $L^{\ast}-PSynth$ and have demonstrated its performance on a range of benchmarks, including robotic motion planning and distributed protocols. Despite the simplicity of $L^{\ast}-PSynth$, it competes well against (and in many cases even outperforms) the state-of-the-art tools for synthesizing parameterized systems.

Wed 2 Dec

Displayed time zone: Osaka, Sapporo, Tokyo change

15:30 - 17:00
Synthesis and Program TransformationResearch Papers at online
Chair(s): Cristina David University of Oxford
15:30
30m
Talk
Relational Synthesis for Pattern Matching
Research Papers
Dmitrii Kosarev , Dmitri Boulytchev Saint Petersburg State University / JetBrains Research
16:00
30m
Talk
Parameterized Synthesis with Safety Properties
Research Papers
Oliver Markgraf Technische Universität Kaiserslautern, Anthony Widjaja Lin Technische Universität Kaiserslautern, Daniel Neider Max Planck Institute for Software Systems, Muhammad Najib Technische Universität Kaiserslautern, Chih-Duo Hong University of Oxford
16:30
30m
Talk
REFINITY to Model and Prove Program Transformation Rules
Research Papers
Dominic Steinhöfel Technical University of Darmstadt