具有随机行为的无限状态系统的综合

给定系统所展现行为的多样性在多种应用情境下是一种期望特性。一致性实现的综合通常通过发现见证Skolem函数来进行，这些函数传统上是确定性的。在本文中，我们提出一种新颖的Skolem提取算法，以实现具有随机行为的见证的综合，并展示其在反应式系统背景下的适用性。所综合的解在设计上保证满足给定规约，同时在对外部刺激的反应中展现出高度的多样性。案例研究展示了我们提出的框架如何在基于模型的模糊测试中揭示综合的新应用，以生成相对于通用替代方案具有竞争力的模糊器，以及所综合的控制器在机器人运动规划问题中的实际效用。