In the modelling and analysis of large, real systems, the main problem in their eficient 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 diferent 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.
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 [
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 [
There are many methods that address the issue of both memory and time complexity for the
analysis of MAS. The methods reducing state space range from partial order reductions [
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 [
Another branch of the literature study shows a number of approaches using Petri nets to
coordinate, organize or plan MAS behaviors. In [
Finally, an approach that seems to be very close to ours uses Nested Unit Petri Nets (NUPN)[
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 [
As already noticed in [
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, ).
Note, however, that local events of diferent 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.
Petri nets were introduced by Carl Adam Petri in his PhD thesis [
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 marking produced from the occurrence of in . A marking is reachable in a net system
relation .
: ( × ) ∪ ( × ) → N instead of flow Σ = ( , , , 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⟩, ∈ , [⟩′}.
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 [
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 ( )
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 diferent label. This
generates a set of diferent 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 diferent 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 [
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 [
In this section we recall from [
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.
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 if 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. 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 diferent 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 removed. 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 diferent 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 if, 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 compositions.
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 [
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.
Unfortunately, this is only a necessary condition to identify transitions that cannot fire, but it is not suficient. 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 ifgure, 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 ifrst 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 ifrst 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 diferent 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 if is 1-live in Σ . 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 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 ifring 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( )11( )... ( ) the sequence of states and ( ), since +1 can fire after transitions obtained by firing the sequence 1... in Σ ( ); ∈ 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 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 afect the reduced systems.
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, 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 suficient 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 [
In this paper we provided a 1-safe Petri net framework to support the reasoning about multiagent 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 efectiveness of proposed
algorithm comparing with the liveness checks in the existing tools for analysing NUPNs like
EVALUATOR [
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 [
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).