Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Davide Catta, Rustam Galimullin, Munyque Mittelmann

TL;DR

This work addresses the verification of dynamic systems where agents permanently modify a graph’s topology through edge deletions, additions, or both. It introduces three logics—SDL, SCL, and SUL—to reason about such strategic, permanent changes on weighted graphs, with SDL and SCL handling single-agent moves and SUL capturing concurrent, coalition-based interactions. The authors establish expressivity relations (CTL is a fragment of all three; SUL strictly dominates SDL and SCL; SDL and SCL are incomparable) and determine model-checking complexities (PSPACE-complete for SDL/SCL; EXPSPACE for full SUL; PSPACE for the next-time fragment). The results advance the formal tooling for verifying dynamic access control and defensive mechanisms that operate during execution, with potential extensions to coalitions, perfect recall strategies, and fixed-point logics. The work connects dynamic, graph-modification reasoning to broader strands in sabotage logics, DEL, and normative MAS analysis, offering a foundation for practical verification of evolving multi-agent systems.

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.

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

TL;DR

This work addresses the verification of dynamic systems where agents permanently modify a graph’s topology through edge deletions, additions, or both. It introduces three logics—SDL, SCL, and SUL—to reason about such strategic, permanent changes on weighted graphs, with SDL and SCL handling single-agent moves and SUL capturing concurrent, coalition-based interactions. The authors establish expressivity relations (CTL is a fragment of all three; SUL strictly dominates SDL and SCL; SDL and SCL are incomparable) and determine model-checking complexities (PSPACE-complete for SDL/SCL; EXPSPACE for full SUL; PSPACE for the next-time fragment). The results advance the formal tooling for verifying dynamic access control and defensive mechanisms that operate during execution, with potential extensions to coalitions, perfect recall strategies, and fixed-point logics. The work connects dynamic, graph-modification reasoning to broader strands in sabotage logics, DEL, and normative MAS analysis, offering a foundation for practical verification of evolving multi-agent systems.

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.
Paper Structure (10 sections, 11 theorems, 1 equation, 3 figures)

This paper contains 10 sections, 11 theorems, 1 equation, 3 figures.

Table of Contents

  1. Introduction
  2. Logics of Angels and Demons
  3. Models
  4. Strategic Deconstruction Logic
  5. Strategic Construction Logic
  6. Strategic Update Logic
  7. Expressivity
  8. Model Checking
  9. Related Work
  10. Discussion

Key Result

Theorem 1

CTL $\prec$ SDL, CTL $\prec$ SCL, and CTL $\prec$ SUL.

Figures (3)

  • Figure 1: Models $\mathfrak{M}_{1}$ (left) and $\mathfrak{M}_{2}$ (right). Arrows with solid lines represent live transitions in the system, whereas dotted lines depict possible new transitions within cost 3.
  • Figure 2: Model $\mathfrak{M}_3$ (left) and $\mathfrak{M}_4$ (right), obtained from changing $\mathfrak{M}_1$ and $\mathfrak{M}_2$ (Figure \ref{['fig:example']}), respectively.
  • Figure 5: The expressivity results. An arrow from $\mathcal{L}_1$ to $\mathcal{L}_2$ means $\mathcal{L}_1 \prec\mathcal{L}_2$. A strike-out arrow from $\mathcal{L}_1$ to $\mathcal{L}_2$ depicts $\mathcal{L}_1 \not \preccurlyeq \mathcal{L}_2$. Open problems are denoted with question marks.

Theorems & Definitions (28)

  • Definition 1: Model
  • Remark 1
  • Definition 2: (De)Construction and Updates
  • Definition 3: Demonic Strategy
  • Definition 4: Strategic Deconstruction Logic
  • Definition 5: SDL Semantics
  • Example 1
  • Definition 6: Angelic Strategy
  • Definition 7: Strategic Construction Logic
  • Definition 8: SCL Semantics
  • ...and 18 more