Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Agentive Permissions in Multiagent Systems

Qi Shi

TL;DR

This paper develops a four-form, agentive permission framework for multiagent systems, distinguishing permissions to admit and to ensure, each in weak and strong variants. It provides a formal semantics on multiagent transition systems, exact model-checking complexity, and reductions to STIT and ATL to connect with established logics. The authors prove semantic undefinability among the four modalities and furnish a sound and complete axiom system, supported by a canonical model construction and a strong completeness theorem. The work advances principled reasoning about agentive permissions and their interplay, with potential applications to normative planning and deontic reasoning in multiagent environments.

Abstract

This paper proposes to distinguish four forms of agentive permissions in multiagent settings. The main technical results are the complexity analysis of model checking, the semantic undefinability of modalities that capture these forms of permissions through each other, and a complete logical system capturing the interplay between these modalities.

Agentive Permissions in Multiagent Systems

TL;DR

This paper develops a four-form, agentive permission framework for multiagent systems, distinguishing permissions to admit and to ensure, each in weak and strong variants. It provides a formal semantics on multiagent transition systems, exact model-checking complexity, and reductions to STIT and ATL to connect with established logics. The authors prove semantic undefinability among the four modalities and furnish a sound and complete axiom system, supported by a canonical model construction and a strong completeness theorem. The work advances principled reasoning about agentive permissions and their interplay, with potential applications to normative planning and deontic reasoning in multiagent environments.

Abstract

This paper proposes to distinguish four forms of agentive permissions in multiagent settings. The main technical results are the complexity analysis of model checking, the semantic undefinability of modalities that capture these forms of permissions through each other, and a complete logical system capturing the interplay between these modalities.
Paper Structure (30 sections, 33 theorems, 39 equations, 5 figures, 4 algorithms)

This paper contains 30 sections, 33 theorems, 39 equations, 5 figures, 4 algorithms.

Table of Contents

  1. Introduction
  2. Literature Review and Notion Discussion
  3. Syntax and Semantics
  4. Model Checking
  5. Reduction to Other Logics
  6. Reduction to STIT
  7. Reduction to ATL
  8. Mutual Undefinability
  9. Axioms
  10. Completeness
  11. Canonical Transition System
  12. Strong Completeness Theorem
  13. Conclusion and Future Research
  14. Model Checking
  15. Proofs of the Undefinability Results
  16. ...and 15 more sections

Key Result

Lemma 1

If set $\mathcal{A}$ contains only agent $a$, then for any formula $\varphi\in\Phi$ and state $s$ of a deterministic transition system,

Figures (5)

  • Figure 1: Toward undefinability of $\text{\upshape WA}$ through $\text{\upshape WE}$, $\text{\upshape SA}$, and $\text{\upshape SE}$.
  • Figure 2: Toward undefinability of $\text{\upshape WE}$ through $\text{\upshape WA}$, $\text{\upshape SA}$, and $\text{\upshape SE}$.
  • Figure 3: Toward undefinability of $\text{\upshape SE}$ through $\text{\upshape WA}$, $\text{\upshape WE}$, and $\text{\upshape SA}$.
  • Figure 4: Toward undefinability of $\text{\upshape SA}$ through $\text{\upshape WA}$, $\text{\upshape WE}$, and $\text{\upshape SE}$.
  • Figure 5: Toward mutual undefinability of $\text{\upshape WA}$ (top) and $\text{\upshape SA}$ (bottom) in single-agent deterministic settings.

Theorems & Definitions (71)

  • Definition 1
  • Definition 2
  • Lemma 1
  • Definition 3
  • Theorem 1: time complexity
  • Definition 4
  • Theorem 2: undefinability of $\text{\upshape WA}$
  • Lemma 2: deduction
  • Lemma 3: Lindenbaum
  • Lemma 4
  • ...and 61 more