Parameterized Synthesis with Safety Properties
Parameterized Synthesis with Safety Properties
复制标题
具有安全特性的参数化合成
DOI：
10.1007/978-3-030-64437-6_14
复制
发表时间：
2020
影响因子：
--
通讯作者：
D. Neider
中科院分区：
文献类型：
--
作者：
Oliver Markgraf;Chih;A. Lin;Muhammad Najib;D. Neider
参数化综合为参数化系统构造正确的、可验证的控制器提供了一种解决方法。这种系统在实践中自然发生（例如，以分布式协议的形式，其中进程的数量在设计时通常是未知的，并且协议必须工作而不管进程的数量）。在本文中，我们提出了一种新的学习为基础的方法来综合反应控制器的参数化系统的安全规格。我们使用定期模型检查的框架来模拟合成问题作为一个无限持续时间的两个玩家的游戏，并显示如何可以利用Angluin的著名的L* 算法来学习正确的设计控制器。这种方法的结果是在一个合成过程中，概念上比现有的合成方法更简单的完整性保证，只要一个获胜的策略可以表示为一个正规的集合。我们已经在一个名为L*-PSynth的工具中实现了我们的算法，并在一系列基准测试中证明了其性能，包括机器人运动规划和分布式协议。尽管L*-PSynth很简单，但它与用于合成参数化系统的最先进的工具竞争得很好（在许多情况下甚至优于）。
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.