Parameterized Synthesis with Safety Properties

TL;DR

This paper introduces a learning-based method for synthesizing correct controllers for parameterized systems with safety properties, leveraging regular model checking and the L* algorithm, demonstrating competitive performance on benchmarks.

Contribution

It presents a novel, simpler synthesis approach using L* algorithm within regular model checking for parameterized systems with safety specifications, with proven completeness.

Findings

The approach guarantees correctness when a regular winning strategy exists.

The tool L*-PSynth performs well on benchmarks, often outperforming existing methods.

The method simplifies the synthesis process while maintaining completeness.

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.