On Angels and Demons: Strategic (De)Construction of Dynamic Models

TL;DR

This paper introduces three logics for reasoning about agents that can modify the structure of weighted graphs, modeling strategic actions like adding or removing edges, with analysis of their expressive power and computational complexity.

Contribution

It presents new logical frameworks for modeling strategic structural modifications in dynamic systems, including both destructive and constructive agents, and analyzes their properties.

Findings

The logics can express complex strategic modifications.

Model checking problems are characterized in terms of complexity.

The frameworks unify destructive and constructive strategic reasoning.

Abstract

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.