天使与恶魔：动态模型的战略（去）构建

近年来，越来越多的人关注形式化战略推理的逻辑，这些逻辑能够推理关于能够修改给定模型结构的代理人。这种研究线索的动力来自于应用场景，其中建模系统随时间演化，例如通信网络、安全协议和多代理计划。在本文中，我们引入了三个逻辑来推理修改加权图拓扑结构的战略。在战略解构逻辑中，破坏性代理人（恶魔）可在一定成本内删除边缘。在战略构建逻辑中，构造性代理人（天使）可在成本限制内添加边缘。最后，战略更新逻辑结合了两个代理人，他们可以合作或竞争。我们研究了这些逻辑的表达力量以及其模型检查问题的复杂性。