Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Asynchronous Multi-Agent Systems with Petri nets

Federica Adobbati, Łukasz Mikulski

TL;DR

The paper develops a framework for asynchronous multi-agent systems using $1$-safe Petri nets with read arcs to model concurrency. It defines two semantics—synchronization on transitions and synchronization on data—and provides Petri-net constructions and fusion operators that preserve the global behavior of the corresponding transition-system models. It proves equivalence results: the Petri-net MAS under either semantics can reproduce the IIS or data-based closures, and it establishes transformations (including weak bisimulation and reachability equivalence) between the two semantics to enable model switching. The approach enables flexible modeling and verification, with practical relevance to assume-guarantee reasoning and scalable composition, and it outlines directions for improving decomposition and efficiency in model checking.

Abstract

Modeling the interaction between components is crucial for many applications and serves as a fundamental step in analyzing and verifying properties in multi-agent systems. In this paper, we propose a method based on 1-safe Petri nets to model Asynchronous Multi-Agent Systems (AMAS), starting from two semantics defined on AMAS represented as transition systems. Specifically, we focus on two types of synchronization: synchronization on transitions and synchronization on data. For both, we define an operator that composes 1-safe Petri nets and demonstrate the relationships between the composed Petri net and the global transition systems as defined in theliterature. Additionally, we analyze the relationships between the two semantics on Petri nets, proposing two constructions that enable switching between them. These transformations are particularly useful for system analysis, as they allow the selection of the most suitable model based on the property that needs to be verified.

Asynchronous Multi-Agent Systems with Petri nets

TL;DR

The paper develops a framework for asynchronous multi-agent systems using -safe Petri nets with read arcs to model concurrency. It defines two semantics—synchronization on transitions and synchronization on data—and provides Petri-net constructions and fusion operators that preserve the global behavior of the corresponding transition-system models. It proves equivalence results: the Petri-net MAS under either semantics can reproduce the IIS or data-based closures, and it establishes transformations (including weak bisimulation and reachability equivalence) between the two semantics to enable model switching. The approach enables flexible modeling and verification, with practical relevance to assume-guarantee reasoning and scalable composition, and it outlines directions for improving decomposition and efficiency in model checking.

Abstract

Modeling the interaction between components is crucial for many applications and serves as a fundamental step in analyzing and verifying properties in multi-agent systems. In this paper, we propose a method based on 1-safe Petri nets to model Asynchronous Multi-Agent Systems (AMAS), starting from two semantics defined on AMAS represented as transition systems. Specifically, we focus on two types of synchronization: synchronization on transitions and synchronization on data. For both, we define an operator that composes 1-safe Petri nets and demonstrate the relationships between the composed Petri net and the global transition systems as defined in theliterature. Additionally, we analyze the relationships between the two semantics on Petri nets, proposing two constructions that enable switching between them. These transformations are particularly useful for system analysis, as they allow the selection of the most suitable model based on the property that needs to be verified.

Paper Structure

This paper contains 19 sections, 6 theorems, 2 equations, 17 figures.

Table of Contents

  1. Introduction
  2. MAS as transition systems: two semantics
  3. Synchronization on transitions
  4. Composition of agents
  5. Synchronization on data
  6. Composition of agents
  7. 1-safe Petri nets with read and inhibitor arcs
  8. Fusion of transitions
  9. Fusion of places
  10. Fusion of sequential components
  11. Synthesis of Petri nets from transition systems
  12. Synthesis of multi-agent systems
  13. Composition with Petri nets in the two semantics
  14. Synchronization on common actions
  15. Synchronization based on sequential components
  16. ...and 4 more sections

Key Result

proposition 1

Let $S = (A_1,...,A_n)$ be an $\mathrm{AMAS}$, $\Sigma_1,...,\Sigma_n$ be a set of Petri net agents such that for each $i\in\{1,...,n\}$, $\Sigma_i$ is a 1-safe system, possibly labeled, obtained through the synthesis of $A_i$, $\Sigma = (P, T, F, m_0, \ell)$ be global Petri net constructed as descr

Figures (17)

  • Figure 1: Schema of involved models.
  • Figure 2: Train-Gate-Controller benchmark with two trains, adapted from JPSDM20.
  • Figure 3: Global model of the $\mathrm{AMAS}$ in Fig. \ref{['fig:tramas']} with synchronizations on transitions
  • Figure 4: Global model of the TGC MAS with two trains and synchronizations on data. Since the transitions are local, but some have the same label, the owner is specified before their label.
  • Figure 5: Example of $1$-safe labeled net system with read arcs.
  • ...and 12 more figures

Theorems & Definitions (27)

  • definition 1
  • definition 2
  • definition 3
  • definition 4
  • definition 5
  • remark 1
  • remark 2
  • definition 6
  • definition 7
  • remark 3
  • ...and 17 more