Paper

Paper
edit
description
id	Vol-3170/paper8
wikidataid	→Q117351467
title	Analysing Multi-Agent Systems using 1-safe Petri Nets
pdfUrl	https://ceur-ws.org/Vol-3170/paper8.pdf
dblpUrl	https://dblp.org/rec/conf/apn/AdobbatiM22
volume	Vol-3170→Vol-3170
session	→

Analysing Multi-Agent Systems using 1-safe Petri Nets

Analysing Multi-Agent Systems using 1-safe Petri
Nets
Federica Adobbati1 , Łukasz Mikulski2,3
1
DISCo Università degli Studi di Milano-Bicocca
2
Faculty of Mathematics and Computer Science, Nicolaus Copernicus University
3
Institute of Computer Science, Polish Academy of Sciences

Abstract
In the modelling and analysis of large, real systems, the main problem in their efficient processing is the
size of the global model. One of the popular approaches that address this issue is the decomposition of
such global model into much smaller submodels and interaction between them. In this paper we discuss
the translation of multi-agent systems with the common-action-based synchronization to 1-safe Petri
nets. We prove that the composition in terms of transition systems is equivalent to the transition-based
fusion of nets modelling different agents. We also address the issue of permanent disabling of some
parts of the system by constraints implied by the synchronization and discuss the methods of solving it
without the computation of the entire global model.

Keywords
1-safe, Petri nets, multi-agent systems, composition

1. Introduction
A multi-agent system (MAS) is composed of multiple decision-making agents interacting inside
some environment. They are highly distributed and concurrent systems. Each agent performs
actions aimed at reaching one’s goal, making decisions according to own strategy. Thus, when
the goal is common or beneficial for many agents, they cooperate to achieve it. On the other hand,
they compete when their goals are in conflict. Multi-agent systems originate from distributed
artificial intelligence field [1], and are also studied by the formal methods and model-checking
community.
The main challenge related to the analysis of real-live MAS is the complexity. On one hand,
the global model of such system is usually very large. A simple voting model with four voters
and one coercer discussed in [2] consists of almost 300 000 states and 7 000 000 transitions. On
the other hand, the price for expressiveness, which allows to express properties like Stackelberg
or Nash equilibria, is high computational complexity of model checking: from 2EXPTIME-
complete in the case of ATL*, to non-elementary for SL [3]. It is worth to note that ATL, being
less expressive, allows to model check strategic properties in polynomial time.
There are many methods that address the issue of both memory and time complexity for the

PNSE’22: International Workshop on Petri Nets and Software Engineering, Bergen, Norway, 2022
" f.adobbati@campus.unimib.it (F. Adobbati); lukasz.mikulski@mat.umk.pl (Ł. Mikulski)
� 0000-0002-6356-7026 (F. Adobbati); 0000-0002-6711-557X (Ł. Mikulski)
© 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
Proceedings
http://ceur-ws.org
ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org)

139
�Federica Adobbati et al. CEUR Workshop Proceedings 139–155

analysis of MAS. The methods reducing state space range from partial order reductions [4],
where the analysed model is much smaller, through on-the-fly techniques [5], hoping that the
small part of the model is sufficient to verify the considered formula, ending with decomposition
methods and assume-guarantee techniques, where the local specification is checked on a small
part of the system immersed in the abstraction of the global model [6]. In order to speed up
the computation, one can try to reason about the base of approximations related with less
expressive but more desirable models [7], or reduce the space of checked strategies by their
internal structure [8]. The research reported in this paper fits in the decomposition methods
approach.

Related work Synthesis and analysis of multi-agent systems is a well known topic in the
literature, also in the context of Petri nets. Pujari and Mukhopadhyay in [9] discuss MAS
as a discrete-event dynamic system (DEDS), and use Petri nets as a modeling tool to assess
the structural properties of the system. Similarily, following DEDS concept, Lukomski and
Wilkosz [10] show rules of modeling and analyzing the considered multi-agent system with
use of Petri nets. Everdij et.al. [11] propose to use compositional specification power of Petri
nets in application to a multi-agent system. Highly distributed air traffic operations system
is considered and modelled using Stochastically and Dynamically Coloured Petri Nets. The
approach of Galan and Baker [12] focuses on specifying and analyzing the conversations in
a multi-agent system. Conversations are specified using an automata model and converted
into a Petri net representation. Using a Petri net analyzer, the conversations are checked for
consistency and coherency by testing liveness and safety of the resulting net. Hiraishi in [13]
proposes 𝑃 𝑁 2 model, an extension of P/T nets, for the design and the analysis of multi-agent
systems.
Another branch of the literature study shows a number of approaches using Petri nets to
coordinate, organize or plan MAS behaviors. In [14] a representation and execution framework
for high level multirobot plan design, called Petri Net Plans (PNP), is proposed. PNP is based
on Petri nets with a domain specific interpretation. Places and transitions are partitioned into
several classes of different interpretations. A special case is a Petri net that has at most one
token per place and edges of weight one. As a central feature, PNPs allow for a formal analysis
of plans based on standard Petri net tools. Scheduling by hierarchical structuring of the tasks
performed by agents is one of key ideas in [15]. They propose a multi-agent system that allows
the user to define a hierarchical structuring of the tasks that these agents perform, to plan
a schedule involving parallel and sequential calling of the agents. The agents are atomic or
complex. Atomic agents are simple Petri nets performing a task, while complex agents are used
to gather atomic (and/or other complex agents) to conglomerate their individual behaviour,
and arrange their working order. The authors of [16] propose a framework for specifying
multi-agent systems based on Synchronized Petri Nets. It is an extension of Recursive Petri
nets, facilitating multi-agent system specifications by concepts like: typed places, transitions
and tokens, synchronization points, synchronization conditions, synchronization relations and
binding functions.
Finally, an approach that seems to be very close to ours uses Nested Unit Petri Nets (NUPN)[17].
One can see multi-agent systems as safe NUPNs of height 1 (taking every agent as a leaf unit

140
�Federica Adobbati et al. CEUR Workshop Proceedings 139–155

and the whole system as the root unit). The nets used in the examples and constructed with the
use of a naive solution (taking a single place for every state of considered transition system) are
even unit-safe. The considered problem of transitions disabled by synchronizations corresponds
to the usual weak-liveness check for such nets.

Contribution The main contribution of this paper is the proof of the operational equivalence
between multi-agent systems and labelled 1-safe Petri nets. First we discuss how one can
synthesize a Petri net of desired behaviour (see [18] for comprehensive description) and utilize
it to prepare a model for each agent separately. Following the idea of splitting transitions in the
case of behaviour which cannot be covered by a 1-safe Petri net utilized in Petrify [19], we first
provide a naive solution. Then we prove that the composition of the set of agents defined in [4]
is equivalent to classical Petri net transition fusion [20].
As already noticed in [21], asynchronous multi-agent systems with the composition based
on the synchronization on actions are prone to all sorts of unwanted side effects. Some actions
designed in the model of composed agents may be permanently disabled in the global model
of the system. Such an artifact can surely be seen as an unwanted side effect of building the
multi-agent system by the composition. As our second contribution, we address this issue
and provide a procedure to check whether a particular action is permanently disabled without
computing the entire global model of a considered multi-agent system. Although the proposed
procedure does not reduce the complexity of the considered problem, it allows to perform
calculations on a fragment of the considered model (which might be much smaller then the
global model).

2. The model
2.1. Asynchronous multi-agent systems
In this section we recall an asynchronous multi-agent system defined in [4].

Definition 1. An asynchronous multi-agent system (AMAS) consists of n agents 𝐴 = {1, . . . , 𝑛}.
Each agent is associated with a tuple 𝐴𝑖 = (𝐿𝑖 , 𝜄𝑖 , 𝐸𝑣𝑡𝑖 , PR 𝑖 , TR 𝑖 , 𝒫𝒱 𝑖 , 𝑉𝑖 ), where

• 𝐿𝑖 = {𝑙𝑖1 , . . . , 𝑙𝑖𝑛𝑖 } is a set of local states;
• 𝜄𝑖 ∈ 𝐿𝑖 is an initial state;
• 𝐸𝑣𝑡𝑖 = {𝛼𝑖1 , . . . , 𝛼𝑖𝑚𝑖 } is a set of events in which agent 𝐴𝑖 can choose to participate;
• PR 𝑖 : 𝐿𝑖 → 2𝐸𝑣𝑡𝑖 is a local protocol, which assigns events to states in which they are
available;
• TR 𝑖 : 𝐿𝑖 × 𝐸𝑣𝑡𝑖 → 𝐿𝑖 is a local transition function, such that TR 𝑖 (𝑙𝑖 , 𝛼) is defined
whenever 𝛼 ∈ PR 𝑖 (𝑙𝑖 );
• 𝒫𝒱 𝑖 is a set of local propositions;
• 𝑉𝑖 : 𝐿𝑖 → 2𝒫𝒱 𝑖 is the valuation of local propositions in local states.

Since the model checking of AMAS is not in the scope of this paper, we are interested only in
transition systems which define the behaviour of AMAS, namely the tuples (𝐿𝑖 , 𝐸𝑣𝑡𝑖 , TR 𝑖 , 𝜄𝑖 ).

141
�Federica Adobbati et al. CEUR Workshop Proceedings 139–155

Figure 1: Example of three local models for agents related to Train-Gate-Controller benchmark from
[4].

Note, however, that local events of different agents may not be disjoint. Events which are
present in more than one event set 𝐸𝑣𝑡 require participation of more than one agent, namely
those agents synchronize on such events.
Example 1. Fig. 1 represents an AMAS with three agents. The events 𝑛1, 𝑚1, 𝑛2, 𝑚2 are shared
by two agents, and require the participation of both of them to occur, whereas the events 𝑛3 and
𝑚3 are local, and depends on a single agent.

2.2. 1-safe Petri nets
Petri nets were introduced by Carl Adam Petri in his PhD thesis [22] as a formal graphical model
to represent and analyse concurrent systems. In this section we provide some basic definitions
that will be useful in the rest of the paper, for an extensive overview about Petri nets and their
applications we refer to [23, 24].
A plain net is characterized by a set of places or conditions 𝑃 , represented as circles, by a set of
transitions 𝑇 , represented as squares, and by a flow relation between them 𝐹 ⊆ (𝑃 ×𝑇 )∪(𝑇 ×𝑃 ),
represented with arcs1 .
For each element 𝑥 ∈ 𝑃 ∪ 𝑇 , its preset is ∙ 𝑥 = {𝑦 ∈ 𝑃 ∪ 𝑇 : (𝑦, 𝑥) ∈ 𝐹 }, and its postset is
𝑥 = {𝑦 ∈ 𝑃 ∪ 𝑇 : (𝑥, 𝑦) ∈ 𝐹 }. For each transition 𝑡 ∈ 𝑇 , we assume that its preset and its
∙

postset are non-empty, i.e. ∙ 𝑡 ̸= ∅ and 𝑡∙ ̸= ∅. The elements in ∙ 𝑡 are also called preconditions
of 𝑡, and the elements in 𝑡∙ are also called postconditions.
A net system is a quadruple Σ = (𝑃, 𝑇, 𝐹, 𝑚0 ), where 𝑃, 𝑇, 𝐹 are the elements of the net,
and 𝑚0 : 𝑃 → N is the initial marking. A transition 𝑡 ∈ 𝑇 is enabled in a marking 𝑚 if for each
𝑝 ∈ ∙ 𝑡, 𝑚(𝑝) ≥ 0. If a transition is enabled, it can occur or fire, and its occurrence generates a
new marking 𝑚′ defined as follows.

⎨𝑚(𝑝) − 1 for all 𝑝 ∈ 𝑡 ∖ 𝑡
⎧
⎪ ∙ ∙

𝑚′ (𝑝) = 𝑚(𝑝) + 1 for all 𝑝 ∈ 𝑡∙ ∖ ∙ 𝑡
in all other cases.
⎪
𝑚(𝑝)
⎩

In symbols, 𝑚[𝑡⟩ denotes that 𝑡 is enabled in 𝑚, while 𝑚[𝑡⟩𝑚′ denotes that 𝑚′ is the mark-
ing produced from the occurrence of 𝑡 in 𝑚. A marking 𝑚 is reachable in a net system
1
In more general definition one can define a weight function 𝑊 : (𝑃 × 𝑇 ) ∪ (𝑇 × 𝑃 ) → N instead of flow
relation 𝐹 .

142
�Federica Adobbati et al. CEUR Workshop Proceedings 139–155

Σ = (𝑃, 𝑇, 𝐹, 𝑚0 ) if there is a sequence of transitions (called a firing sequence) 𝑡1 ...𝑡𝑛 such
that 𝑚0 [𝑡1 ⟩𝑚1 ...𝑚𝑛−1 [𝑡𝑛 ⟩𝑚. The set of all the reachable markings is denoted with [𝑚0 ⟩. A
transition 𝑡 ∈ 𝑇 is 1-live if there is a marking 𝑚 ∈ [𝑚0 ⟩ such that 𝑚[𝑡⟩.
Let 𝑚 be a reachable marking, and 𝑡1 , 𝑡2 ∈ 𝑇 be two transitions enabled in 𝑚: 𝑡1 and 𝑡2 are
in conflict in 𝑚 if ∙ 𝑡1 ∩ ∙ 𝑡2 ̸= ∅; 𝑡1 and 𝑡2 are concurrent in 𝑚 if ∙ 𝑡1 ∩ ∙ 𝑡2 = ∅ and 𝑡∙1 ∩ 𝑡∙2 = ∅.
In this paper we work with the class of 1-safe net systems. A net system is 1-safe if, for each
𝑚 ∈ [𝑚0 ⟩ and for each 𝑝 ∈ 𝑃 , 𝑚(𝑝) ≤ 1. In a 1-safe system, each marking can (and will) be
considered as a set of places, and each place can be interpreted as a proposition, that is true if
the place belongs to the marking, and false otherwise.
A labelled Petri net Σ𝜆 = (Σ, 𝜆) is a 1-safe net system with a function 𝜆 : 𝑇 → Λ, where
Λ is a set of labels. Abusing the notation, for each 𝑇 ′ ⊆ 𝑇 subset of 𝑇 , we will denote with
𝜆(𝑇 ′ ) = {𝛼 ∈ Λ : ∃𝑡 ∈ 𝑇 ′ : 𝜆(𝑡) = 𝛼} the set of labels of the elements in 𝑇 ′ . The set 𝜆(𝑇 ) is
the alphabet of Σ𝜆 .
The sequential behaviour of a labelled Petri net can be described by an initialized labelled
transition system, where each state corresponds to a reachable marking, and each arc is labelled
by the label of the transition leading from the source marking to the target one.

Definition 2. Let Σ = (𝑃, 𝑇, 𝐹, 𝑚0 , 𝜆) be a labelled Petri net, its marking graph is a quadruple
𝑀 𝐺(Σ) = ([𝑚0 ⟩, 𝜆(𝑇 ), 𝐴𝑟, 𝑚0 ) where 𝐴𝑟 = {(𝑚, 𝜆(𝑡), 𝑚′ ) | 𝑚, 𝑚′ ∈ [𝑚0 ⟩, 𝑡 ∈ 𝑇, 𝑚[𝑡⟩𝑚′ }.

2.3. Synthesis of 1-safe Petri nets from AMAS
For each agent in an AMAS, we can always obtain a 1-safe labelled Petri net: the agent in the
AMAS can be considered as the marking graph of the net, therefore the net can be found through
a synthesis procedure. The classical techniques for the synthesis of 1-safe net systems are based
on the research of regions [18]. Let 𝐴𝑖 = (𝐿𝑖 , 𝐸𝑣𝑡𝑖 , TR 𝑖 , 𝜄𝑖 ) be a labelled transition system. A
region is a subset of states 𝑟 ⊆ 𝐿𝑖 such that, for each 𝑒 ∈ 𝐸𝑣𝑡𝑖 , one of the following conditions
holds: (1) 𝑒 enters the region, i.e. for each arc labelled with 𝑒 from 𝑠1 to 𝑠2 , 𝑠1 ̸∈ 𝑟 ∧ 𝑠2 ∈ 𝑟; (2)
𝑒 leaves the region, i.e. for each arc labelled with 𝑒 from 𝑠1 to 𝑠2 , 𝑠1 ∈ 𝑟 ∧ 𝑠2 ̸∈ 𝑟; (3) 𝑒 does not
cross the border of the region, i.e. for each arc labelled with 𝑒 from 𝑠1 to 𝑠2 , 𝑠1 ∈ 𝑟 ∧ 𝑠2 ∈ 𝑟, or
𝑠1 ̸∈ 𝑟 ∧ 𝑠2 ̸∈ 𝑟. In order to synthesize a 1-safe net system, every label in 𝐸𝑣𝑡𝑖 is translated into
a transition of the net system, and every region into a place. The flow relation is determined
as follows: for each transition 𝑒, for each place 𝑟, 𝑟 is a precondition of 𝑒 if 𝑒 leaves 𝑟 in 𝐴𝑖 , 𝑟
is a post-condition of 𝑒 if 𝑒 enters 𝑟 in 𝐴𝑖 . If 𝑒 does not cross the border of 𝑟, and for each arc
labelled with 𝑒 from 𝑠1 to 𝑠2 , we have 𝑠1 , 𝑠2 ∈ 𝑟, then we can see 𝑟 as both a precondition and
a postcondition of 𝑒, and add a self loop to the net. Otherwise, there is no flow relation between
𝑟 and 𝑒 in the net.
Not every transition system can be synthesized into a 1-safe net. In particular, we can
synthesize a 1-safe net system from a transition system if, and only if, the set of regions of the
transition system satisfies the so called state separation property (SSP) and event-state separation
property (ESSP):

∀𝑠, 𝑠′ ∈ 𝐿𝑖 𝑠 ̸= 𝑠′ → ∃𝑟 ∈ 𝑅 : (𝑠 ∈ 𝑟 ∧ 𝑠′ ̸∈ 𝑟) ∨ (𝑠 ̸∈ 𝑟 ∧ 𝑠 ∈ 𝑟) (𝑆𝑆𝑃 )
∀𝑒 ∈ 𝐸, ∀𝑠 ∈ 𝑆 : 𝑒 is not outgoing from 𝑠, → ∃𝑟 : 𝑠 ̸∈ 𝑟 ∧ 𝑒 leaves 𝑟 (𝐸𝑆𝑆𝑃 )

143
�Federica Adobbati et al. CEUR Workshop Proceedings 139–155

Figure 2: 1-safe Petri nets for transition systems depicted in Fig. 1.

Example 2. Consider the central transition system on the upper part of Fig. 4. Since there is an
outgoing transition labelled as 3 from all the states, the only regions in this system are trivial:
the empty set, and the set of all the states. These regions do not allow to separate any pair of
states, therefore SSP is not satisfied, and the transition system is not synthesizable with a 1-safe
net without labels.

However, it is always possible to obtain a labelled 1-safe system, by allowing the net to have
more transitions with the same label. In this case, we can split the transitions of 𝐴𝑖 with the
same label into subgroups, and look for regions as if each group had a different label. This
generates a set of different transitions in the net sharing the same label. To obtain such a net
is always possible, since we could consider subsets formed by single arcs: if each arc of the
transition system is considered as if it had different labels from the others, it is easy to verify
that the set of regions satisfies the separation properties SSP and ESSP. Furthermore, each state
of 𝐴𝑖 is a region and therefore can be translated into a place of the synthesized net. As showed
in [18], the minimal regions with respect to inclusion are sufficient for the synthesis, therefore
we can consider the states of 𝐴𝑖 as all and only the places of the net. In what follows we will
transform each agent of the AMAS in this way.
For each 𝑖, we can represent each agent as a labelled Petri net. In particular, for each agent
𝐴𝑖 = (𝐿𝑖 , 𝐸𝑣𝑡𝑖 , TR 𝑖 , 𝜄𝑖 ), the associated Petri net is defined as Σ𝑖 = (𝐿𝑖 , 𝑇𝑖 , 𝐹𝑖 , 𝜄𝑖 , 𝜆), where:

• 𝐿𝑖 is the set of places that coincides with the set of local states in 𝐴𝑖 ;
• 𝑇𝑖 is the set of transitions, and there is one for each element in TR 𝑖 ;
• 𝐹𝑖 is the flow relation, fully determined by TR 𝑖 ;
• 𝜄𝑖 is the initial marking, that coincides with the initial state of 𝐴𝑖 ;
• 𝜆 : 𝑇𝑖 → 𝐸𝑣𝑡𝑖 is the labelling function, associating every transition of the net with the
label of the corresponding arc on the agent.

Example 3. Consider the AMAS in Figure 1, described also in [4]. In Figure 2 the agents of the
AMAS are represented as Petri nets.

144
�Federica Adobbati et al. CEUR Workshop Proceedings 139–155

3. Composition
3.1. Composition of AMAS
In this section we recall from [4] the definition of canonical interleaved interpreted system,
which is a composition of agents being parts of an asynchronous multi-agent system with
synchronizations on common events. Note that since we are not interested in model checking,
we would concentrate only on the behaviour of the multi-agent system (putting apart the
propositional variables).

Definition 3. A canonical interleaved interpreted system (canonical IIS) is an AMAS extended
with a tuple (𝑆𝑡, 𝐸𝑣𝑡, TR, 𝜄) where:

• 𝑆𝑡 ⊆ 𝐿1 × . . . × 𝐿𝑛 is a set of global states;
• 𝐸𝑣𝑡 = 𝑖∈{1,...,𝑛} 𝐸𝑣𝑡𝑖 is a set of events;
⋃︀

• TR : 𝑆𝑡×𝐸𝑣𝑡 → 𝑆𝑡 is a (partial) global transition function, where TR((𝑙1 , . . . , 𝑙𝑛 ), 𝛼) =
(𝑙1′ , . . . , 𝑙𝑛′ ) if TR 𝑖 (𝑙𝑖 , 𝛼) = 𝑙𝑖′ for all 𝑖 where 𝛼 ∈ 𝐸𝑣𝑡𝑖 and TR 𝑖 (𝑙𝑖 , 𝛼) = 𝑙𝑖 otherwise;
• 𝜄 = (𝜄1 , . . . , 𝜄𝑛 ) is an initial state.

Given a canonical IIS 𝐼, some of its states may not be reachable through any execution, due
to the restrictions given by the synchronizations, and therefore also the transitions outgoing
from these states can never be executed. We will denote with 𝐼𝑟 the canonical system where
these unreachable states and transitions have been pruned.
By definition, the number of states in the IIS grows exponentially with the number of agents,
therefore limiting the number of compositions when studying the properties of the system may
help in the analysis.

3.2. Composition of 1-safe Petri nets
Let Σ1 = (𝐿1 , 𝑇1 , 𝐹1 , 𝜄1 , 𝜆), ..., Σ𝑛 = (𝐿𝑛 , 𝑇𝑛 , 𝐹𝑛 , 𝜄𝑛 , 𝜆) be the set of Petri net agents. We then
construct a global net Σ = (𝑃, 𝑇, 𝐹, 𝑚0 , 𝜆), showing the interaction of the agents. The set of
places 𝑃 of Σ is the union of the sets of places 𝐿𝑖 . For each label 𝛼 ∈ 𝜆(𝑇𝑖 ), for each agent Σ𝑖 ,
let 𝑇𝑖𝛼 = {𝑡 ∈ 𝑇𝑖 : 𝜆(𝑡)⋃︀= 𝛼} be⨂︀ the set of transitions labelled with 𝛼. The set of transition
of Σ is defined as 𝑇 = 𝛼∈𝜆(𝑇𝑖 ) 𝑖∈{1,...,𝑛} 𝑇𝑖𝛼 . The flow relation is determined in this way:
for each transition 𝑡 ∈ 𝑇 , and each place 𝑝 ∈ 𝑃 there is an arc from 𝑝 to 𝑡 iff there is a Σ𝑖 and
𝑡𝑗 ∈ 𝑇𝑖 such that 𝑝 ∈ 𝐿𝑖 , 𝑡𝑗 is a component in 𝑡, and (𝑝, 𝑡𝑗 ) ∈ 𝐹𝑖 ; analogously for the arcs from
𝑡 ∈ 𝑇 to 𝑝 ∈ 𝑃 . The initial marking 𝑚0 is the union of all the elements 𝜄𝑖 , with 𝑖 ∈ {1, ..., 𝑛}.
The labelling function 𝜆 associates every transition 𝑡 ∈ 𝑇 to the label of all its component, that
is unique by construction. We denote the alphabet of Σ with 𝜆(𝑇 ).
By construction, each place in Σ belongs at most to one agent, whereas the transitions can be
shared. Note that some of the transitions may be enabled in no reachable marking, and therefore
are not 1-live. As we discussed in the previous section, the same problem happens when we
consider the composition of AMAS, because some states may not be reachable from the initial
state 𝜄, due to the synchronization constraints. The problem of finding these transitions is
discussed in detail in Sec. 4.

145
�Federica Adobbati et al. CEUR Workshop Proceedings 139–155

Figure 3: Global Petri net model resulting from the composition of the nets depicted in Fig. 2.

Example 4. Fig. 3 represents the composition of the three agents from Fig. 2. In this model, for
each agent, each label appears only in one transitions, therefore in the global net in Fig. 3 each
transition has a different label.
This is in general not the case, as we can see in Fig.4. In the latter case both the Petri net agents
and the global model have the same label shared between more transitions.

Let 𝐼𝑟 be the canonical IIS where all the unreachable states and transitions have been re-
moved. The following proposition shows that synthesis and composition are commutative,
i.e synthesizing Petri net agents from the AMAS and then composing them is equivalent to
construct the composition of AMAS and then synthesizing a Petri net.

Proposition 1. Let 𝑆 be an AMAS, Σ = (𝑃, 𝑇, 𝐹, 𝑚0 , 𝜆) be global Petri net constructed as
described above, and 𝐼 the canonical IIS of 𝑆. The transition system of Σ is isomorphic to 𝐼𝑟 .

Proof. The initial marking of Σ is the initial state of 𝐼 by the construction. Let 𝑚 be any
reachable marking in Σ. By the construction, 𝑚 is a set of 𝑛 places, each of them from a
different set 𝐿𝑖 , with 𝑖 ∈ {1, ..., 𝑛}. For each 𝑖 ∈ {1, ..., 𝑛} we denote as 𝑙𝑖 the element of 𝑚
in the set 𝐿𝑖 . Let 𝑡 ∈ 𝑇 be a transition such that 𝜆(𝑡) = 𝛼. By construction, 𝑡 is enabled in 𝑚
iff, for each agent Σ𝑖 , 𝑖 ∈ {1, ..., 𝑛} such that 𝛼 ∈ 𝜆(𝑇𝑖 ), there is a transition 𝑡𝑖 ∈ 𝑇𝑖 such that
𝜆(𝑡𝑖 ) = 𝛼 and 𝑡𝑖 enabled in 𝑙𝑖 . This condition is equivalent to the one of the global transition
function defined for 𝐼𝑟 , therefore for each marking, the set of outgoing transitions and states
reachable in one step is the same. Hence the two models are isomorphic.

Note that, for simplicity, in the above proposition we consider the specific 1-safe labelled
systems. One can easily repeat similar reasoning for any 1-safe labelled systems which are
synthesized from transition systems describing behaviours of particular agents and their com-
positions.

146
�Federica Adobbati et al. CEUR Workshop Proceedings 139–155

Figure 4: Three agents described as automata, the same agents represented with Petri nets, and the
global Petri net.

4. 1-liveness of transitions
In this section we discuss how to find transitions that are not 1-live on the global net. This
is known to be a PSPACE-complete problem [25, 26]. We propose an algorithm that, in some
cases, does not need to construct the global net in order to verify whether a transition is 1-live,
but uses a smaller subnet. If this is possible, some computation is saved, since the complexity of

147
�Federica Adobbati et al. CEUR Workshop Proceedings 139–155

Figure 5: Composition of the first and third transition system depicted in Fig. 4.

the problem depends on the dimension of the net. In the worse case, the algorithm reconstructs
the global system, and checks 1-liveness on it.
Consider the net in Fig. 4. All the transitions labelled with 0 will never be enabled. A simple
way to find these transitions consists in computing the marking graph of the net and check its
labels. The transitions that do not appear in the marking graph will never be enabled. However,
this can be computationally very expensive, since having all the agents may increase the level
of concurrency, and therefore the size of the transition system.
A first alternative idea could be to find some of the transitions that will never be enabled by
composing for each label all the agents sharing it. For example, the labels 1 and 0 are shared
by the first and third agent in Fig. 4. Fig. 5 shows the composition of the two agents, and the
marking graph of this reduced net. The part coloured in red shows the transitions that cannot
be enabled. If a transition cannot occur in the net obtained composing only the agents sharing
its label, then it cannot occur in the global net, since adding new components can only add the
number of constraints, due to the synchronization requirements.

148
�Federica Adobbati et al. CEUR Workshop Proceedings 139–155

Unfortunately, this is only a necessary condition to identify transitions that cannot fire, but it
is not sufficient. To see an example, consider the agents represented in Fig. 6. In the upper part
of the figure, we see three agents sharing some of their labels. Below it, there is the global net,
where the unreachable parts are coloured in red, and its transition system. At the bottom of the
figure, we find the composition of the second and third agent, and its transition system. The
label 𝑑 is shared only by the second and third agent, and by composing only them, it seems to
be possible to fire it. However, this is not true, as we can see in the global transition system.
This happens because in the reduced composition for label 𝑑, 𝑏 is considered as a label of the
third agent only, whereas in the global system, it must synchronize with the transition of the
first agent. We can see from the reduced transition system that 𝑑 must occur after 𝑐 and 𝑏, but
since 𝑏 cannot fire in the global net, also 𝑑 cannot be reached.
This suggests us another element to check whether a transition can be enabled without
constructing the transition system of the global net, consisting in composing all the agents
sharing a certain label, and all the labels in a minimal path leading to it from the initial state.

Definition 4. Let 𝑀 𝐺(Σ) be the marking graph of Σ. The firing sequence 𝑡1 ...𝑡𝑛 is minimal if
for each 𝑖, 𝑗 < 𝑛, 𝑚𝑖 ̸= 𝑚𝑗 , where 𝑚𝑖−1 [𝑡𝑖 ⟩𝑚𝑖 .

Let Λ ⊆ 𝜆(𝑇 ) be any subset of labels in the global net Σ. We will denote with ΣΛ the net
obtained by composing all the agents with at least an element of Λ in their alphabet.
Let 𝛼 be any label on the system, and 𝑇𝛼 = {𝑡𝑗 ∈ 𝑇 : 𝜆(𝑡𝑗 ) = 𝛼}. Algorithm 1 shows how
to check that 𝑡𝑗 ∈ 𝑇𝛼 is 1-live in Σ, without computing the entire system. By applying the
algorithm to each 𝑡𝑗 ∈ 𝑇𝛼 , we can discover which transitions of Σ are not 1-live, and therefore
can be removed without changing the behaviour of the net.
The algorithm takes as input 𝑡𝑗 , the set of all the agents in the system, and a set of labels Λ,
and returns true if there is a firing sequence of transitions that enable 𝑡𝑗 , false otherwise. In
addition, if one exists, the algorithm returns the sequence 𝜋 of transitions leading to 𝑡𝑗 . In the
first call Λ = {𝛼}.
The algorithm has a recursive structure. The first step consists in computing the minimal
paths from the initial state of ΣΛ to 𝑡𝑗 (this is done by the function comp_min_paths). If there
are no minimal paths in 𝑀 𝐺(ΣΛ ), then it returns false, since ΣΛ does not need to be further
explored. Otherwise, it selects a minimal path 𝜋, through the function select_path. Let 𝜆(𝜋) be
the set of labels of the transitions in 𝜋. If Σ𝜆(𝜋) = ΣΛ , then the algorithm returns true, since
we found a path that can be executed on Σ and enables 𝑡𝑗 . When this happens, there is no need
to look for alternative paths, and the computation can stop and return true. This is not the case
if a recursive call returns false, since the unreachability of 𝑡𝑗 may be due to a wrong choice of
the path in one of the previous steps. Then, we need to check if, in previous calls, other paths
could have been chosen, leading to different subsystems, and check if 𝑡𝑗 is reachable in them. If
𝑡𝑗 is not reachable from any path, then we can conclude that 𝑡𝑗 is not 1-live.
By construction, for each transition 𝑡𝑖 in the sequence 𝜋 returned by Algorithm 1, the set of
preconditions and the set of postconditions are the same in Σ and in Σ𝜆(𝜋) .

Theorem 1. Algorithm 1 is correct, i.e. for each transition 𝑡𝑗 ∈ 𝑇 , the algorithm returns true iff
𝑡𝑗 is 1-live in Σ.

149
�Federica Adobbati et al. CEUR Workshop Proceedings 139–155

Figure 6: Example of a transition that from the reduced composition falsely seems to be 1-live.

Proof. As the first step, we show that if the algorithm returns true, then 𝑡𝑗 is executable in
Σ, and in particular the path 𝜋 = 𝑡1 ...𝑡𝑗 returned by the algorithm is a firing sequence of Σ.
We proceed by induction, starting to show that 𝑡1 is enabled in 𝑚0 . By contradiction, let us
suppose that 𝑡1 is not enabled in 𝑚0 . Then, there must be a precondition 𝑝 ∈ ∙ 𝑡1 , such that
𝑝 ̸∈ 𝑚0 . By the construction, all the elements in ∙ 𝑡1 come from agents that have transitions
labelled with 𝜆(𝑡1 ), and all these agents are included in Σ𝜆(𝜋) ; hence, if 𝑡1 is enabled in the
initial state of Σ𝜆(𝜋) , it must be enabled also in 𝑚0 . Let 𝜋𝑖 = 𝑡1 ...𝑡𝑖 , 𝑖 < 𝑗, be a prefix of the

150
�Federica Adobbati et al. CEUR Workshop Proceedings 139–155

Algorithm 1 Check if 𝑡𝑗 is 1-live
procedure check_1liveness(𝑡𝑗 , {Σ𝑖 : 𝑖 ∈ {1, ..., 𝑛}}, Λ) ∈ {true, false } × Π
Π =comp_min_paths(𝑀 𝐺(ΣΛ ), 𝑡𝑗 )
if Π == ∅
return false, ∅
end if
while Π ̸= ∅
𝜋 =select_path(Π)
Π = Π ∖ {𝜋}
if ΣΛ == Σ𝜆(𝜋)
𝜋′ = 𝜋
return true, 𝜋
end if
𝑟, 𝜋 ′ = check_1liveness(𝑡𝑗 , {Σ𝑖 : 𝑖 ∈ {1, ..., 𝑛}}, 𝜆(𝜋))
if 𝑟 == true
return true, 𝜋 ′
end if
end while
return false, ∅
end procedure

firing sequence 𝜋 and 𝑚𝑖 the state reached in Σ after executing 𝜋𝑖 . We show that 𝑡𝑖+1 is enabled
in 𝑚𝑖 . By contradiction, let us suppose that 𝑡𝑖+1 is not enabled in 𝑚𝑖 . Then there must be a place
𝑝 ̸∈ 𝑚𝑖 and such that 𝑝 ∈ ∙ 𝑡𝑖+1 . This place must be also in Σ𝜆(𝜋) , since, by the construction,
Σ𝜆(𝜋) includes all the agents with transitions labelled 𝜆(𝑡𝑖+1 ), and the preconditions of 𝑡𝑖+1
𝜆(𝜋) 𝜆(𝜋) 𝜆(𝜋)
on Σ cannot belong to any other agent. Let 𝑚0 𝑡1 𝑚1 ...𝑡𝑖 𝑚𝑖 the sequence of states and
𝜆(𝜋)
transitions obtained by firing the sequence 𝑡1 ...𝑡𝑖 in Σ 𝜆(𝜋) ; 𝑝 ∈ 𝑚𝑖 , since 𝑡𝑖+1 can fire after
𝜋𝑖 in Σ𝜆(𝜋) , and there must be an index 𝑘 ≤ 𝑖 such that 𝑝 ∈ 𝑚𝛼𝑟 for each 𝑟 ≥ 𝑘. If 𝑘 = 0, then
𝜆(𝜋)
𝑝 ∈ 𝑚0 , since 𝑚0 ⊆ 𝑚0 , by the construction. If 𝑘 > 0, then 𝑝 ∈ 𝑡∙𝑘 , and 𝑝 ∈ 𝑚𝑘 . Since the
𝜆(𝜋)
set of preconditions and postconditions of 𝑡𝑘+1 ...𝑡𝑖 is the same in Σ and Σ𝜆(𝜋) , if 𝑝 ∈ 𝑚𝑖
after the execution of 𝑡𝑘+1 ...𝑡𝑖 , then 𝑝 ∈ 𝑚𝑖 after firing the same sequence.
As the second step, we need to prove that if the algorithm returns false, then 𝑡𝑗 is not 1-live
in Σ. This follows from the observation that adding agents to the system can only restrict the
possibility of the transitions in Σ𝛼 to occur by adding synchronizations constraints. Therefore,
if 𝑡𝑗 is a transition in ΣΛ , but there is no sequence in ΣΛ enabling 𝑡𝑗 , a fortiori there cannot be
any sequence in Σ.

Proposition 2. Algorithm 1 terminates after a finite number of steps.

Proof. The thesis follows from the finiteness of the number of agents in the system, and of the
number of minimal paths.

Algorithm 1 does not guarantee that the system Σ𝜆(𝜋) to check will be smaller than Σ, since

151
�Federica Adobbati et al. CEUR Workshop Proceedings 139–155

Figure 7: Example of the system where each agent interact with a small subset of other agents.

the two systems may coincide (for example in the systems in Fig. 4 and Fig. 6). However, in
distributed systems in which each agent interacts with a small subset of other agents of the
entire system, it may become a convenient technique. An example of such a system could be
represented by a social network, where the number of users is huge, but each of them has a
limited number of connections. A toy example is represented in Fig. 7. In this case concurrency
enlarges the size of the global transition system, while does not affect the reduced systems.

Figure 8: Net with two possible paths to reach 𝑑 and the alternatives compositions.

The required computation can also be reduced by choosing proper heuristics for the function
select_path, so that the more convenient paths are selected to be analysed first. A possible
criterion could be to select first the paths requiring to add the minor number of new agents,

152
�Federica Adobbati et al. CEUR Workshop Proceedings 139–155

even when they are longer and with more labels than others. Consider for example the system
of agents in Fig. 8. The four agents are represented at the top of the figure, and two of their
compositions at the bottom. Transition 𝑑 belongs only to agent 1 (the second from the left), and
there are two minimal sequences reaching it: 𝑎𝑑, and 𝑏𝑐𝑑. Although 𝑎𝑑 is shorter, the label 𝑎 is
shared by two more agents: agent 0 and agent 2, whereas 𝑐 belongs only to agent 1, and 𝑏 is
shared with agent 3 only. The two compositions of agents represented in Fig. 8 shows Σ{𝑎,𝑑}
(on the left), and Σ{𝑏,𝑐,𝑑} (on the right). It is easy to see that Σ{𝑏,𝑐,𝑑} has less reachable states
than Σ{𝑎,𝑑} , and it is sufficient to decide the 1-liveness of the transition labelled with 𝑑.
Note that, for simplicity, once more we have considered only the specific 1-safe labelled
systems. If we restrict ourselves to such situation, most of the reasoning can be repeated without
using Petri nets. However, the real performance improvement is revealed when we utilize more
sophisticated synthesis algorithms based on region theory. One can expect that in such cases the
number of transitions with the same label appearing in a single local model would be smaller.
Moreover, such approach gives a chance to decompose local models into sequential components
(see [27]) and use them instead of entire modules.

5. Summary
In this paper we provided a 1-safe Petri net framework to support the reasoning about multi-
agent systems. We have shown that it faithfully reflects the transition-based composition of the
agents and illustrates the usage in the case of checking 1-liveness of transitions. Continuing this
thread of research we plan to take a closer look to the ideas highlighted at the end of Section 4.
The mentioned semi-automatic decomposition of the agents’ behaviour into smaller subsystems
has a large potential not only in the case of checking 1-liveness, but also in preparing the
environment (formal assumption subsystem) for the assume-guarantee reasoning.
Taking into account the similarity of labelled 1-safe Petri net models of AMAS described
in paper with Nested Unit Petri Nets, we would like to examine the effectiveness of proposed
algorithm comparing with the liveness checks in the existing tools for analysing NUPNs like
EVALUATOR [28].
However, in the future we would like to consider systems that are k-safe. The reason is
twofold, there are synthesis methods which work fine without the restriction of 1-safeness.
The resulting nets usually require less use of transition splitting, hence are smaller. Moreover,
such approach is much more natural in planned by us analysis of asynchronous systems, where
the synchronization is data-oriented (not action-oriented as in the approach presented in this
paper).
Recently, an approach to automated synthesis of MAS based on satisfiability and model
checking tools, has been presented in [29]. After specifying the constraints and the strategic
properties to be met, the tool, exploiting monotonic theory for ATL [30], looks for the model
satisfying all requirements. To reason about strategic abilities of MASs variants of ATL* and SL
logic are considered [3, 31]. As a future work, we plan to utilize the described framework both
in direct model checking using 1-safe Petri nets, and in the synthesis of MAS satisfying desired
ATL formulas.

153
�Federica Adobbati et al. CEUR Workshop Proceedings 139–155

Acknowledgments
The first author was supported by the Italian MUR. The second author was supported by
the National Centre for Research and Development, Poland (NCBR), and by the Luxembourg
National Research Fund (FNR), under the PolLux/FNR-CORE project STV (POLLUX-VII/1/2019).

References
[1] J. Ferber, G. Weiss, Multi-agent systems: an introduction to distributed artificial intelligence,
volume 1, Addison-Wesley Reading, 1999.
[2] D. Kurpiewski, Ł. Mikulski, W. Jamroga, STV+AGR: towards practical verification
of strategic ability using assume-guarantee reasoning, CoRR abs/2203.01033 (2022).
doi:10.48550/arXiv.2203.01033.
[3] F. Belardinelli, W. Jamroga, V. Malvone, A. Murano, Strategy logic with simple goals:
Tractable reasoning about strategies, in: 28th International Joint Conference on Artificial
Intelligence (IJCAI 2019), 2019, pp. 88–94.
[4] W. Jamroga, W. Penczek, T. Sidoruk, P. Dembinski, A. W. Mazurkiewicz, Towards partial
order reductions for strategic ability, J. Artif. Intell. Res. 68 (2020) 817–850. URL: https:
//doi.org/10.1613/jair.1.11936. doi:10.1613/jair.1.11936.
[5] F. Raimondi, A. Lomuscio, Model Checking ATL and its epistemic extensions, Technical
Report, Technical Report RN/05/01, University College London, 2005.
[6] A. Lomuscio, B. Strulo, N. Walker, P. Wu, Assume-guarantee reasoning with local specifi-
cations, International Journal of Foundations of Computer Science 24 (2013) 419–444.
[7] W. Jamroga, M. Knapik, D. Kurpiewski, Ł. Mikulski, Approximate verification of
strategic abilities under imperfect information, Artif. Intell. 277 (2019). doi:10.1016/
j.artint.2019.103172.
[8] D. Kurpiewski, M. Knapik, W. Jamroga, On domination and control in strategic ability,
in: Proceedings of AAMAS’19, International Foundation for Autonomous Agents and
Multiagent Systems, 2019, pp. 197–205.
[9] S. Pujari, S. Mukhopadhyay, Petri net: A tool for modeling and analyze multi-agent
oriented systems, International Journal of Intelligent Systems and Applications 4 (2012)
103.
[10] R. Lukomski, K. Wilkosz, Modeling of multi-agent system for power system topology
verification with use of Petri nets, in: 2010 Modern Electric Power Systems, IEEE, 2010,
pp. 1–6.
[11] M. H. Everdij, M. B. Klompstra, H. A. Blom, B. Klein Obbink, Compositional specification of
a multi-agent system by stochastically and dynamically coloured Petri nets, in: Stochastic
hybrid systems, Springer, 2006, pp. 325–350.
[12] A. K. Galan, A. D. Baker, Multi-agent communication in JAFMAS, Trans: Propose to Q3 5
(1999) S7.
[13] K. Hiraishi, A Petri-net-based model for the mathematical analysis of multi-agent systems,
IEICE Transactions on Fundamentals of Electronics, Communications and Computer
Sciences 84 (2001) 2829–2837.

154
�Federica Adobbati et al. CEUR Workshop Proceedings 139–155

[14] V. A. Ziparo, L. Iocchi, P. U. Lima, D. Nardi, P. F. Palamara, Petri net plans, Autonomous
Agents and Multi-Agent Systems 23 (2011) 344–383.
[15] C. Molinero, M. Núñez, Planning of work schedules through the use of a hierarchical
multi-agent system, Automation in Construction 20 (2011) 1227–1241. URL: https://
www.sciencedirect.com/science/article/pii/S0926580511000793. doi:https://doi.org/
10.1016/j.autcon.2011.05.006.
[16] S. Kouah, D.-E. Saïdouni, J.-M. Ilié, Synchronized Petri net: A formal specification model
for multi agent systems., J. Softw. 8 (2013) 587–602.
[17] H. Garavel, Nested-unit Petri nets, Journal of Logical and Algebraic Methods in Program-
ming 104 (2019) 60–85.
[18] E. Badouel, L. Bernardinello, P. Darondeau, Petri net synthesis, Springer, 2015.
[19] J. Cortadella, M. Kishinevsky, A. Kondratyev, L. Lavagno, A. Yakovlev, Petrify: a tool for
manipulating concurrent specifications and synthesis of asynchronous controllers, IEICE
Transactions on information and Systems 80 (1997) 315–325.
[20] L. Gomes, J. P. Barros, Structuring and composability issues in Petri nets modeling, IEEE
Transactions on Industrial Informatics 1 (2005) 112–123.
[21] W. Jamroga, W. Penczek, T. Sidoruk, Strategic abilities of asynchronous agents: Semantic
side effects, Proceedings of AAMAS 2021 (2021) 1545–1547.
[22] C. A. Petri, Kommunikation mit Automaten, Ph.D. thesis, Hamburg Univ., Germany, 1962.
[23] T. Murata, Petri nets: Properties, analysis and applications, Proceedings of the IEEE 77
(1989) 541–580.
[24] J. L. Peterson, Petri nets, ACM Computing Surveys (CSUR) 9 (1977) 223–252.
[25] N. D. Jones, L. H. Landweber, Y. E. Lien, Complexity of some problems in Petri nets,
Theoretical Computer Science 4 (1977) 277–299.
[26] J. Esparza, Decidability and complexity of Petri net problems—an introduction, in:
Advanced Course on Petri Nets, Springer, 1996, pp. 374–428.
[27] G. Rozenberg, J. Engelfriet, Elementary net systems, in: Advanced Course on Petri Nets,
Springer, 1996, pp. 12–121.
[28] R. Mateescu, Specification and analysis of asynchronous systems using CADP, 2008.
[29] A. Niewiadomski, M. Kacprzak, D. Kurpiewski, M. Knapik, W. Penczek, W. Jamroga, MsATL:
A tool for SAT-based ATL satisfiability checking, in: Proceedings of 19th International
Conference on Autonomous Agents and Multiagent Systems AAMAS 2020, 2020.
[30] M. Kacprzak, A. Niewiadomski, W. Penczek, SAT-Based ATL Satisfiability Checking,
in: Proceedings of the 17th International Conference on Principles of Knowledge Rep-
resentation and Reasoning, 2020, pp. 539–549. URL: https://doi.org/10.24963/kr.2020/54.
doi:10.24963/kr.2020/54.
[31] M. Kacprzak, A. Niewiadomski, W. Penczek, Satisfiability Checking of Strategy Logic
with Simple Goals, in: Proceedings of the 18th International Conference on Principles
of Knowledge Representation and Reasoning, 2021, pp. 400–410. URL: https://doi.org/
10.24963/kr.2021/38. doi:10.24963/kr.2021/38.

155
�

Vol-3170/paper8

Paper

Analysing Multi-Agent Systems using 1-safe Petri Nets

Navigation menu

Search