In recent years, there has been growing interest in logics that formalise strategic reasoning about agents capable of modifying the structure of a given model. This line of research has been motivated by applications where a modelled system evolves over time, such as communication networks, security protocols, and multi-agent planning. In this paper, we introduce three logics for reasoning about strategies that modify the topology of weighted graphs. In Strategic Deconstruction Logic, a destructive agent (the demon) removes edges up to a certain cost. In Strategic Construction Logic, a constructive agent (the angel) adds edges within a cost bound. Finally, Strategic Update Logic combines both agents, who may cooperate or compete. We study the expressive power of these logics and the complexity of their model checking problems.
翻译:近年来,对于形式化描述智能体在修改给定模型结构时进行战略推理的逻辑体系,学界关注日益增长。这一研究方向受到通信网络、安全协议与多智能体规划等随时间演化的建模系统应用的推动。本文提出三种用于推理加权图拓扑修改策略的逻辑体系:在战略解构逻辑中,破坏性智能体(恶魔)以特定成本为上限移除边;在战略建构逻辑中,建设性智能体(天使)在成本约束范围内添加边;最终,战略更新逻辑融合了既可协作又可对抗的两种智能体。我们研究了这些逻辑的表达能力及其模型检测问题的计算复杂度。