Parameterized synthesis with safety properties

DOI10.1007/978-3-030-64437-6_14MaRDI QIDQ2038085zbMATH OpenOpenAlexFDO

Authors Oliver Markgraf, Chih-Duo Hong, Muhammad Najib, Daniel Neider, Anthony Widjaja Lin

Publication date 8 July 2021

Full work available at URL https://arxiv.org/abs/2009.13459

zbMATH Keywords

Angluin's algorithmmachine learningparameterized systemsreactive synthesisregular model checking

Mathematics Subject Classification ID

Computational learning theory (68Q32) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Artificial intelligence for robotics (68T40) Applications of game theory (91A80)

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.

Recommendations

• Parameterized synthesis
• Parameterized Synthesis
• Compositional synthesis with parametric reactive controllers
• Towards efficient parameterized synthesis
• Parametric systems: verification and synthesis

Cited in

(12)

• An automaton learning approach to solving safety games over infinite graphs
• Automated formal synthesis of provably safe digital controllers for continuous plants
• Parameterized synthesis
• Towards efficient parameterized synthesis
• SAT-Based Synthesis Methods for Safety Specs
• Compositional synthesis with parametric reactive controllers
• An Improved Safety Solver in Go Using Partial Regions
• Parametric systems: verification and synthesis
• Parameterized Synthesis
• Verification-guided programmatic controller synthesis
• Synthesis of distributed agreement-based systems with efficiently-decidable verification
• Learning union of integer hypercubes with queries (with applications to monadic decomposition)

This page was built for publication: Parameterized synthesis with safety properties

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2038085)