分布式优先级综合

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