分布式优先级合成及其应用

给定一组具有非确定性变量更新且需满足安全性要求的交互组件，优先级合成的目标是通过引入优先级来限制可能的交互集合，从而保证所有可能运行均满足给定的安全条件。在分布式优先级合成中，我们致力于获取局部优先级集合，这些集合以局部组件控制器的形式部署，仅在局部邻域内的组件间共享预期的下一步动作。这些局部控制器之间可能的通信路径由通信架构指定。我们将分布式优先级合成问题形式化为多玩家安全博弈：一方玩家（天使性地）选择组件的下一个转换，另一方环境（恶魔性地）更新不可控变量；该问题是 NP 完全的。我们提出了若干优化方案，包括基于诊断方法的解空间探索，该方法利用博弈中吸引子计算的嵌套扩展，并将其归约到相应的 SAT 问题。当诊断失败时，该方法提出潜在候选解以引导探索。这些用于求解分布式优先级合成问题的优化算法已集成到我们的 VissBIP 框架中。利用包括多核处理器调度和模块化机器人在内的多个案例研究，对该实现进行了实验验证。