Parameterized Synthesis with Safety Properties

Oliver Markgraf*, Chih-Duo Hong, Anthony W. Lin, Muhammad Najib, Daniel Neider

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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). 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 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-PSynth and have demonstrated its performance on a range of benchmarks, including robotic motion planning and distributed protocols. Despite the simplicity of L-PSynth it competes well against (and in many cases even outperforms) the state-of-the-art tools for synthesizing parameterized systems.

Original languageEnglish
Title of host publicationProgramming Languages and Systems. APLAS 2020
EditorsBruno C. Oliveira
PublisherSpringer
Pages273-292
Number of pages20
ISBN (Electronic)9783030644376
ISBN (Print)9783030644369
DOIs
Publication statusPublished - 2020
Event18th Asian Symposium on Programming Languages and Systems 2020 - Fukuoka, Japan
Duration: 30 Nov 20202 Dec 2020

Publication series

NameLecture Notes in Computer Science
Volume12470
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference18th Asian Symposium on Programming Languages and Systems 2020
Abbreviated titleAPLAS 2020
Country/TerritoryJapan
CityFukuoka
Period30/11/202/12/20

Keywords

  • Angluin’s algorithm
  • Machine learning
  • Parameterized systems
  • Reactive synthesis
  • Regular model checking

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Parameterized Synthesis with Safety Properties'. Together they form a unique fingerprint.

Cite this