Automatic generating algorithm of rewriting logic specification for multi-agent system models based on Petri nets

Abstract

On one hand, Petri nets are widely used as a modeling formalism to assess both structural and behavioral properties of the multi-agent system bacause of their mathematical foundations and the rich underlying analysis tools has developed around them. On the other hand, Maude is a very powerful formal specification language based on rewriting logic that is known as a unifying framework for different types of Petri nets and offers a wide range of analysis techniques.

In this paper, we will present a new algorithm allowing the automatic generation of Maude specifications from Petri nets models in order to help designers to effectively obtain the rewriting logic based specification of their multi-agent systems and then facilitate their analysis, pick up time and stay away from human related errors occurred during the manual preparation of such specification.

Keywords

Automatic code generation multi-agent systems Petri nets rewriting logic

1. Introduction

It is very evident that the paradigm of Multi-Agent System (MAS) has emerged as one of the cutting-edge approaches that led to the study of a wide range of problems in different fields [61, 48, 42, 32]. However, due to the complex nature and heterogeneity of multi-agent based system components, designers need to simulate the system behavior and for that they often use formal modeling notations and approaches to assess key properties of multi-agent systems. Such approach could be used to provide a formal description of agent’s behavior and/or system functions, provide guidelines for the design of MAS, facilitate their preliminary analysis, ensure that the system will comply with a set of required properties and then make decision about its feasibility [24, 47, 63].

In this context, Petri nets are the most popular modeling language that have proven to be very reliable in practice for both MAS simulation and analysis [16, 51]. This success of Petri nets is principally due to their graphical notation, simple semantics, and the rich underlying mathematical theory that has developed around them for analyzing their models. For instance, Petri nets have been used to describe both the internal and external behavior of agents [1, 37, 38], conversation and interaction protocols [15, 8, 50] and developing cooperation for multi-agent systems [39, 31]. However, their potentiality of modeling should not hide the increasing need for automatic techniques, methods and tools facilitating the formal analysis of large scale Petri net models.

On the other hand, Maude [23] is a very powerful formal specification language based on rewriting logic [44] that is a unifying framework for Petri nets [33, 7, 9, 55, 35]. In addition, Maude offers a wide range of analysis techniques and it has been used in different works to specify and analyze multi-agent systems [57, 59, 4]. However, the transcription of Petri net models into Maude specifications is prepared manually. There lacked a bridge to directly link Petri net models and the Maude system. Such operation is turned out to be difficult, time consuming and error-prone especially in the case of large scale and complex models.

The main goal of this paper is to bridge the gap between Petri net models and Maude system and for that we present a new algorithm to automatically generate Maude specifications from Petri Net models of multi-agent based systems, to palliate the above mentioned difficulties, and their consequently related risks; especially in the case of safety-critical systems. In addition, it is worthy to note that the advantages of this algorithm will not be limited to those designing multi-agent systems, but all practitioners building models with Petri nets can benefit from this algorithm and then exploit the Maude analysis tools for their models.

The following Section 2 gives a short literature review on the use of Petri nets and rewriting logic in the context of multi-agent systems. Section 3 introduces the required concepts of rewriting logic and Petri nets and we alternatively refer to [45, 53] for background. In Section 4, we present the process to generate Maude specifications from Petri nets models. Then, a case study and results are presented in Section 5. Section 6 presents the most related work to this paper. Finally, Section 7 concludes the paper with perspectives for the future work.

2. Literature review

In fact, various modeling techniques have been proposed and used in order to go from the informal or less formal system description to its formal specification and then, the individual agents with their relationships are described in terms of activities by means Petri nets, automata, state machine, logic rules or conditional statements (if-then) … etc. [29, 58, 49, 36, 2]. In this section, and because it is out of the scope of this paper, we will not compare Petri nets and Maude with other formalisms and specification languages since our interest is focused on the automatic generation of Maude specification from Petri net. However, we will present some previous works to show the advantages, effectiveness and then motivate our choice of Petri nets and rewriting logic.

2.1 Petri nets based works

Petri-net is still known as one of the most popular used formalism to assist designers in the early stages of multi-agent-based simulation of models development [3, 21]. For instance, Petri nets have been widely used to describe both the internal, external and social behavior of agents [1, 46, 37, 38], conversation and interaction protocols [15, 8, 50] and developing cooperation for multi-agent systems [39, 31]. In addition, a lot of extensions have been also proposed for Petri nets in order to describe intentional agents and other aspects in MAS [37, 17, 30, 18, 43, 19] and maintain significant properties (mathematical foundation) of ordinary Petri nets.

Moreover, Petri nets have been widely favored for analyzing multi-agent systems because of their exact mathematical definition of their execution semantics with the well-developed theory for process analysis. Hence, the corresponding Petri net models of multi-agent systems will be assessed by using the existing analysis methodologies and simulation techniques for Petri nets [41, 6, 52, 20, 14]. In [5], Petri net models are generated from the multi-agent UML diagrams to simulate the behavior of an agent. Thereafter, Petri net analysis techniques are applied to automatic agent behavioral testing.

2.2 Rewriting logic based works

The Maude term rewriting language has been advocated in several works for the specification and verification of multi-agent systems. The Maude system is mainly characterized by its expressive strength, as well as the large number of formal analysis tools. For instance, the paper [60] presents a Maude based implementation of (a simplified version of) the cognitive agent programming language 3APL. In such implementation, the 3APL configurations are represented as terms, and the transition rules are mapped into rewrite rules. In the enhanced version [59], Maude is used for prototyping agent programming language BUpL (Belief Update programming Language) and executing agent programs. Thereafter, the LTL-model checker and Maude analysis tools are also used for verification and testing. Authors in [40] used Maude to gain a formal description for Agent-Group-Role-based-organization models and, they are simulated and verified by means of its associated tools.

Finally, the Maude language is used for behavior formalization of DIMA model’s agents [13]. In this work, the inherent aspects of a DIMA models are captured and then, the corresponding Maude descriptions have been validated using the analysis tools of Maude. Such work has been extended to support both formal description and verification of DIMA multi-agent models [12]. However, the common main disadvantage of all these works is that the translation of multi-agent models into Maude specification is prepared manually in ad hoc manner. Hence, it may be very difficult to ensure that such specification is a faithful description of the studied multi-agent system.

2.3 Synthesis

According to what we have exhibited, it turns out to be evident that the use of Petri nets and Maude in MAS context is very advantageous and helpful. On one hand, the Petri nets formalism permits to normally visualize the parallelism, the synchronization, the sharing of resources and conflicts in distributed systems. What’s more, it allows to model the behavior (internal and external) of the agents, interaction protocols and the social aspect (organization). Nevertheless, Petri nets practitioners need to use a formal verification techniques that identifies and mitigates risks in their proposed models. On the other hand, Maude is also used directly for the development of MAS or indirectly as a formal unifying framework for a wide range of Petri nets. In addition, Maude offers some advanced analysis tools allowing the automatic verification of Petri nets based models properties. In particular, the Maude LTL model checker is a powerful tool that combines a very expressive and general-purpose system specification language with on-the-fly explicit-state model checking techniques, which is one of the most commonly used approaches to model checking. Moreover, Maude allows using another complementary technique, i.e., a reachability tool that can explicitly check the existence of critical states in the studied system from a pre-defined initial state and then offers a very quick verification time if the best initial state is used.

Therefore, even if the Petri net models are attentively prepared, Maude specification defects can be introduced during the manual preparation of such specification for Petri net based models of multi-agent system. These defects may be introduced by designers because of the large size and/or complexity of described behaviour of multi-agent systems. Consequently, the best solution to cater this problem is the automatic generation of Maude specifications from the Petri net models. In addition, automatic generation provide considerable saving of time and reproducible quality of the generated code.

Finally, we will focus on the presentation of a straightforward algorithm for the automatic translation from Petri nets based models to Maude specifications.

3. Preliminaries

Firstly, rewriting logic [44] is a formal specification language built upon the membership equational logic by adding “rewrite rules” to deal with change, dynamic and concurrency. In such logic, the rewrite theory $\mathcal{T}=$ ( $\Sigma$ , E, L, R) is the key structure to represent concurrent systems. The signature ( $\Sigma$ , E) describes its static structure, whereas its dynamic behavior is described by the set of labelled conditional rewrite rules (L, R) that will operate on equivalence classes of terms modulo the equations E.

Secondly, Maude [23, 22] is a rewriting logic based language in which a system specification can be written in two modules. While functional modules are used to define the signature (basic elements) of the system such as, sorts, operations, terms and equations, system modules are very general rewrite theories that may have equations in addition to rewrite rules to define the dynamic part (behavior) of the system.

Thirdly, a Petri net consists of a set of places, transitions and a set of arcs connecting places with transitions. In fact, a Petri net is defined as a 5-tuple $\mathcal{PN}=(P,T,\textit{Pre},\textit{Post},M_{0})$ where:

•
$P$ : a finite set of places connected with;
•
$T$ : a finite set of transitions where $P\cap T=\emptyset$ ;
•
Pre: $P\times T\longrightarrow\mathds{N}^{+}$ is the pre-incidence function, where: $\textit{Pre}(P_{i},T_{j})$ is the weight of the arc from place $P_{i}$ to transition $T_{j}$ ;
•
Post: $T\times P\longrightarrow\mathds{N}^{+}$ is the post-incidence function, where: $\textit{Post}(P_{i},T_{j})$ is the weight of the arc from place $T_{j}$ to transition $P_{i}$ ;
•
$M_{0}$ : $P\rightarrow\mathds{N}$ is the initial marking.

According, a place (which may contain different number of tokens) with an arc starts from itself to a transition is an input place, and a place with an arc starts from a transition to itself is an output place. An arc has a weight “ $k$ ” attributed by Pre or Post function. An Ordinary Petri net is one where all arcs are unity-weighted ( $k=1$ and hence unlabeled).

A transition $T_{j}$ is enabled if all its input places $P_{i}$ are marked with at least $\textit{Pre}(P_{i},T_{j})$ tokens. Such enabled transition may be unconditionally fired. Thereafter, the fired transition $T_{j}$ consumes $\textit{Pre}(P_{i},T_{j})$ tokens from each input place $P_{i}$ and adds $\textit{Post}(P^{\prime}_{i},T_{j})$ tokens to each output place $P^{\prime}_{i}$ .

The global state of a Petri net (marking), designs in fact the distribution of tokens over places. This distribution is defined via the function $M:P\rightarrow\mathds{N}$ that assigns to each place the number of tokens reside in. A Petri net marking M can be changed when one or more transitions are fired. In order to illustrate some concepts of Petri nets related to our paper, we give the following example.

Figure 1.
Example of Petri net.

In the Fig. 1, P1, P2, P3 and P4 represent the set of places and T1, T2, T3 and T4 represent the set of transitions. All arcs in this Petri net have implicitly weights equal to “1” except the one connecting P1 with T2. In addition, the transition T1 is called source transition since it hasn’t any input place and the transition T4 is called sink transition because it hasn’t any output place. Moreover, the place P3 is at the same time an input and an output to the transition T4 which represent a self-loop. Therefore, the present Petri net is not a pure Petri net since it has a self-loop.

Finally, Petri nets have been well-studied in the context of rewriting logic and in order to facilitate their description in Maude, we give the following example (see Fig. 2) that describes the behavior of the famous dining philosophers problem. In such well-known problem, we consider four philosophers (simple agents) eating at the same round table, sharing four forks. For sake of simplicity, we consider that each philosopher agent alternates between thinking with eating states.

The corresponding Maude specification of such Petri net is given in Listing 1.
Listing 1
Maude specification modules of dining philosophers behaviour.

fmod PETRI_NET is mod DINING_PHILOSOPHERS is

sorts Place Marking . including PETRI_NET .

subsorts Place < Marking . rl [takes-forks0] : T0 F3 F0 => E0 .

op empty : -> Marking . rl [releases-forks0] : E0 => T0 F3 F0 .

op Initial : -> Marking . rl [takes-forks1] : T1 F0 F1 => E1 .

ops E0 T0 E1 T1 E2 T2 E3 T3 : -> State . rl [releases-forks1] : E1 => T1 F0 F1 .

ops F0 F1 F2 F3 : -> Fork . rl [takes-forks2] : T2 F1 F2 => E2 .

op __ : Marking Marking -> Marking rl [releases-forks2] : E2 => T2 F1 F2 .

[assoc comm id: empty] . rl [takes-forks3] : T3 F2 F3 => E3 .

eq Initial = F0 F1 F2 F3 T0 T1 T2 T3 . rl [releases-forks3] : E3 => T3 F2 F3 .

endfm endm

In this specification, the static part (components or signature) of the system is given in a functional module PETRI_NET. This module is then imported in the system module DINING_PHILOSOPHERS in which we add a rule for each transition to complete describing each state and/or action in the behavior of each philosopher.
4. Automatic generation algorithm

Our algorithm is principally based on the translation mechanism proposed in [56] and its general description is illustrated in Fig. 3.

Figure 2.

Petri net describing the dining philosophers behaviour.

Figure 3.

Generating algorithm description.

4.1 Algorithm entries

The proposed algorithm is principally based on the use of the incidence matrix and modules templates for both functional and system modules.

4.1.1 Incidence matrix

The algebraic representation of a Petri net $\mathcal{PN}$ is defined by the incidence matrix, which is composed of Pre-incidence PRE and Post-incidence POST matrices that are defined by $N$ rows (number of places) and $M$ columns (number of transitions). Such two matrices can be obtained from the Petri net according to the pre-incidence and the post-incidence functions. Therefore, the PRE matrix could be filled from the Petri net $\mathcal{PN}$ as given in Algorithm 1.

Algorithm 1
Fill the pre-incidence matrix (PRE)
1:
Petri Net : N places, M transitions
2:
procedure Fill_PRE_Matrix(PRE : Matrix of N $\times$ M of integer)
3:
Ouput : PRE Matrix of N $\times$ M of integer
4:
for $i\leftarrow 1∼{}∼{}to∼{}∼{}N$ do
5:
for $j\leftarrow 1∼{}∼{}to∼{}∼{}M$ do
6:
if (an arc leads from place $i$ to transition $j$ ) then
7:
$\textbf{PRE[\emph{i},\,\,\emph{j}]}\leftarrow\textit{Pre}(P_{i},T_{j})$
8:
else
9:
$\textbf{PRE[\emph{i},\,\,\emph{j}]}\leftarrow 0$
10:
end if
11:
end for
12:
end for
13:
end procedure

Similarly, we present the procedure Fill_POST_Matrix in Algorithm 2.
Algorithm 2
Fill the post-incidence matrix (POST)
1:
Petri Net : N places, M transitions
2:
procedure Fill_POST_Matrix(POST : Matrix of N $\times$ M of integer)
3:
Ouput : POST Matrix of N $\times$ M of integer
4:
for $i\leftarrow 1∼{}∼{}to∼{}∼{}N$ do
5:
for $j\leftarrow 1∼{}∼{}to∼{}∼{}M$ do
6:
if (an arc leads from transition $j$ to place $i$ ) then
7:
$\textbf{POST[\emph{i},\,\,\emph{j}]}\leftarrow\textit{Post}(P_{i},T_{j})$
8:
else
9:
$\textbf{POST[\emph{i},\,\,\emph{j}]}\leftarrow 0$
10:
end if
11:
end for
12:
end for
13:
end procedure
4.1.2 Modules templates

As one can see in Listing 1, some parts are not changeable in both functional and system modules. Therefore, the use of a specification template file that contains the constant specification parts will be very useful. Such specification templates FTemplate (func_petrinet) and STemplate (system_petrinet) are given in Listing 2.

Listing 2
Maude specification templates for functional and system modules.

1. fmod FUNC_PETRINET is 1. mod SYSTEM_PETRINET is

2. sorts Place Marking . 2. including FUNC_PETRINET .

3. subsorts Place < Marking . 3. rl [Trans-Name] : lhs => rhs .

4. op empty : -> Marking . … Other Rules …

5. ops PLACES_NAMES : -> Place . 4. endm

6. op __ : Marking Marking -> Marking

[assoc comm id: empty] .

7. endfm
4.2 Algorithm elements

The proposed algorithm consists of two parts. The first one concerns the generation of the functional module, whereas the second concerns the generation of the system module. Such two modules are complementary to describe the whole system.

4.2.1 Specification modules creation

The following procedure (see Algorithm 3) describes the process of creation of the specification modules by using the templates files (Listing 2). In fact, this procedure will copy the template file in the specification module to be created.

Algorithm 3
Creation of specification files
1:
Template file
2:
procedure Create_specification_file(Specificationfilename : String, Templatefilename : String)
3:
Ouput : Specification file : Maude file
4:
$\textit{Open}(\textit{Templatefilename})$
5:
$\textit{Createemptyfile}(\textit{Specificationfilename})$
6:
$\textit{Copyfile}(\textit{Templatefilename},\textit{Specificationfilename})$ $\lx@algorithmicx@hfill\triangleright$ copy “Template file” to “Specification file”
7:
$\textit{Close}(\textit{Specificationfilename})$
8:
$\textit{Close}(\textit{Templatefilename})$
9:
end procedure
4.2.2 The generation of specification modules

In order to facilitate the generation process of the Maude specification, we assume that places are labeled as: P1, P2, … P $n$ and, transitions as: T1, T2, … T $m$ . In addition, we will principally use two procedures that are place_names and rewrite_rules.

The first procedure extracts the number of places from the incidence matrix IM in order to generate the corresponding specification line in a string variable “placenames” which will be inserted in the appropriate place in the functional module as given in Algorithm 4.

Algorithm 4
Generation of the place names for the functional module
1:
N: rows number of IM Matrix
2:
procedure Place_Names(placenames: String)
3:
Ouput : placenames : String $\triangleright$ this will replace line 5 in functional module template
4:
placenames $\leftarrow$ “ops” $+$ “ ”
5:
for $i\leftarrow 1∼{}∼{}to∼{}∼{}N$ do
6:
placenames $\leftarrow$ placenames $+$ “P” $+$ Asstring(i) $+$ “ ” $\triangleright$ Asstring(i): converts $i$ into string
7:
end for
8:
placenames $\leftarrow$ placenames $+$ “: $->$ Place .”
9:
end procedure

The following function Is_Source (resp, Is_Sink) is an intermediate function that determines the source (resp, sink) transitions in the Petri net and it is given in Algorithm 5 (resp, Algorithm 6). In fact, such two functions are necessary since their corresponding rewrite rules will be prepared with special treatment.

Similarly, the next function Is_Sink is given as follow.

The second procedure generates a new rewrite rule for each transition in the incidence matrix IM then save result in a string variable “RewriteRule”. These strings will be inserted in the system module. This procedure is illustrated in Algorithm 7.
Algorithm 5
Verification of source transitions
1:
PRE Matrix
2:
function Is_Source(x: integer) $\lx@algorithmicx@hfill\triangleright$ $x$ : order of transition in PRE
3:
Ouput : result : boolean
4:
result $\leftarrow$ True
5:
i $\leftarrow$ 1
6:
while $(i<=N)\textit{and}(\textit{result})$ do
7:
if (PRE[i,x] $>$ 0) then
8:
$\textbf{result}\leftarrow\textit{False}$ $\lx@algorithmicx@hfill\triangleright$ The transition $x$ : is not a source
9:
end if
10:
i $\leftarrow$ i $+$ 1
11:
end while
12:
Is_Source $\leftarrow$ result
13:
end function
Algorithm 6
Verification of sink transitions
1:
POST Matrix
2:
function Is_Sink(x: integer) $\lx@algorithmicx@hfill\triangleright$ $x$ : order of transition in POST
3:
Ouput : result : boolean
4:
result $\leftarrow$ True
5:
i $\leftarrow$ 1
6:
while $(i<=N)\textit{and}(\textit{result})$ do
7:
if (POST[i,x] $>$ 0) then
8:
$\textbf{result}\leftarrow\textit{False}$ $\lx@algorithmicx@hfill\triangleright$ t The transition $x$ : is not sink
9:
end if
10:
i $\leftarrow$ i $+$ 1
11:
end while
12:
Is_Sink $\leftarrow$ result
13:
end function
Algorithm 7
Generation of the corresponding rewrite rule for a transition
1:
Matrix IM (PRE and POST matrices)
2:
procedure Rewrite_Rule(x : integer, RewriteRule : String) $\triangleright$ x : represents row/transition number
3:
Ouput : RewriteRule : String
4:
Variables: $\textit{Label},\textit{lhs},\textit{rhs},\textit{arrow}$ : String
5:
$\textit{arrow}\leftarrow$ “ $=>$ ” $+$ “ ”
6:
$\textit{Label}\leftarrow$ “T” $+$ Asstring(x) $\triangleright$ to generate label for each transition
7:
$\textbf{RewriteRule}\leftarrow$ “rl” $+$ “ ” $+$ “[“ $+$ label $+$ ”]” $+$ “ ” $+$ “:” $+$ “ ” $\triangleright$ prepare the rewrite rule
8:
$\textit{lhs}\leftarrow$ “ ” $\triangleright$ at the beginning, lhs of each rule is empty
9:
$\textit{rhs}\leftarrow$ “ ” $\triangleright$ rhs is also empty at the beginning
10:
for $i\leftarrow 1∼{}∼{}to∼{}∼{}N$ do
11:
for $j\leftarrow 1∼{}∼{}to∼{}∼{}\textit{PRE}[i,x]$ do
12:
$\textit{lhs}\leftarrow\textit{lhs}$ $+$ “P” $+$ Asstring(i) $+$ “ ” $\triangleright$ preparing lhs
13:
end for
14:
for $j\leftarrow 1∼{}∼{}to∼{}∼{}(\textit{POST}[i,x])$ do
15:
$\textit{rhs}\leftarrow rhs$ $+$ “P” $+$ Asstring(i) $+$ “ ” $\triangleright$ preparing rhs
16:
end for
17:
end for
18:
$\textbf{RewriteRule}\leftarrow\textbf{RewriteRule}+\textit{lhs}+\textit{arrow}% +\textit{rhs}+$ “.”
19:
$\triangleright$ each generated RewriteRule will be written at line 3 of system_module
20:
end procedure

In order to write placenames and RewriteRule in the specification files, we need another procedure (see Algorithm 8) for which we need the specification file name and the line number where we have to write the strings placenames or RewriteRule.
Algorithm 8
Insertion of generated code in the specification file
1:
Specification file
2:
procedure Insert(Specificationfilename: String, Linetoinsert : String, linenumber : integer)
3:
$\textit{Open}(\textit{Specificationfilename})$
4:
$\textit{writenewline}(\textit{Specificationfilename},\textit{Linetoinsert},% \textit{linenumber})$
5:
$\triangleright$ write “Linetoinsert” at the line : (linenumber) of Specificationfilename
6:
$\textit{Close}(\textit{Specificationfilename})$
7:
end procedure
4.3 Full algorithm

The full proposed algorithm for the automatic generation of Maude specifications from Petri nets is given in Algorithm 9 as follows.

Algorithm 9
Automatic generation of Maude specification
1:
Petri Net : N places, M transitions
2:
$\ \ \ \ \ \ \textbf{FTemplate}$ : Functional template file
3:
$\ \ \ \ \ \ \textbf{STemplate}$ : System template file
4:
Specification Files : Functional module, System Module
5:
Begin
6:
$S$ : integer
7:
$S\leftarrow$ 0 $\lx@algorithmicx@hfill\triangleright$ M : is equal 0 when there is (are) not sink or source transition(s)
8:
Sink_or_Source : boolean
9:
Sink_or_Source $\leftarrow$ False
10:
Fill_PRE_Matrix(PRE)
11:
Fill_POST_Matrix(POST)
12:
Create_specification_file(functional_module, FTemplate)
13:
Place_Names(placenames)
14:
Insert(functional_module, placenames, 5)
15:
Create_specification_file(system_module, STemplate)
16:
j $\leftarrow$ 1
17:
while $(j<=M)\textit{and}$ not(Sink_or_Source) do $\lx@algorithmicx@hfill\triangleright$ Test the existence of source or sink transitions
18:
if (Is_Sink(j) or (Is_Source(j)) then
19:
Sink_or_Source $\leftarrow$ True
20:
end if
21:
j $\leftarrow$ j + 1
22:
end while
23:
if (Sink_or_Source) then
24:
Insert(system_module, “op M :- $>$ Marking .”, 3 $+$ S) $\lx@algorithmicx@hfill\triangleright$ Add the variable M declaration to the specification
25:
$S\leftarrow S+1$ $\lx@algorithmicx@hfill\triangleright$ Incrementing S to insert the next rule in the following line
26:
end if
27:
for $j\leftarrow 1∼{}∼{}to∼{}∼{}M$ do
28:
Rewrite_Rule(j, RewriteRule)
29:
Insert(system_module, RewriteRule, 3 $+$ S)
30:
$S\leftarrow S+1$ $\lx@algorithmicx@hfill\triangleright$ Incrementing S to insert the next rule in the following line
31:
end for
32:
End
5. Case study with implementation results

In order to test the correctness of the proposed algorithm, we have implemented a prototype1 of such algorithm by using the Delphi programming language, as we have used the same Petri net (Fig. 2) as entry to ensure the correctness of the automatic generation of Maude specification process.

To do so, we have followed the propositions cited in Subsection 4.2 to rename places and transitions. The resulted equivalent Petri Net is given in Fig. 4.

On the other hand, by using the procedure fill_matrix, the corresponding incidence matrix of such Petri net is given in the following Table 1.

Table 1
Incidence matrices

	T1	T2	T3	T4	T5	T6	T7	T8		T1	T2	T3	T4	T5	T6	T7	T8
P1	1								P1		1
P2		1							P2	1
P3			1						P3				1
P4				1					P4			1
P5					1				P5						1
P6						1			P6					1
P7							1		P7								1
P8								1	P8							1
P9	1		1						P9		1		1
P10			1		1				P10				1		1
P11					1		1		P11						1		1
P12	1						1		P12		1						1
			(a) PRE Matrix									(b) POST Matrix

Figure 4.

Equivalent Petri net describing the dining philosophers behaviour.

After executing the prototype implementing our algorithm, we have exactly obtained the following specification modules.

Listing 3

The generated specification modules.

fmod FUNC_PETRINET is mod SYSTEM_PETRINET is

sorts Place Marking . including FUNC_PETRINET .

subsorts Place < Marking . rl [ T1] : P1 P9 P12 => P2 .

op empty : -> Marking . rl [ T2] : P2 => P1 P9 P12 .

ops P1 P2 P3 P4 P5 P6 P7 P8 P9 P10 P11 rl [ T3] : P3 P9 P10 => P4 .

P12 : -> Place . rl [ T4] : P4 => P3 P9 P10 .

op __ : Marking Marking -> Marking [assoc rl [ T5] : P5 P10 P11 => P6 .

comm id: empty] . rl [ T6] : P6 => P5 P10 P11 .

endfm rl [ T7] : P7 P11 P12 => P8 .

rl [ T8] : P8 => P7 P11 P12 .

endm

In order to confirm the syntax correctness of the generated specification, we have compiled the specification files with Maude system by using the Maude command “load” and everything is gone ok and Maude compiler gave us a positive result.

5.1 Algorithm time complexity

Let’s now analyze the time complexity of the proposed algorithm. This complexity will be given as a function of the size of an incidence matrix $IM:(N,M)$ that reflect the size of the modeled system. The proposed algorithm fills first the incidence matrices and then creates the functional and system specification files. So the time complexity of the complete algorithm corresponds to the total cost of the matrix filling process and of the generation of the two specification files, that is:

$\displaystyle\textit{Cost}(N,M)=\textit{Cost}_{\textit{Fill}\_\textit{Matrix}}% (N,M)+\textit{Cost}_{\textit{Gen}\_\textit{Fun}\_\textit{Mod}}(N,M)+\textit{% Cost}_{\textit{Gen}\_\textit{Sys}\_\textit{Mod}}(N,M),$

where $\textit{Cost}_{\textit{Fill}\_\textit{Matrix}}(N,M)$ is the cost of the matrices filling, $\textit{Cost}_{\textit{Gen}\_\textit{Fun}\_\textit{Mod}}(N,M)$ and $\textit{Cost}_{\textit{Gen}\_\textit{Sys}\_\textit{Mod}}$ $(N,M)$ correspond to the costs of the generation of the functional and system files respectively.

So, the time of the matrix filling process is a linear function of the number of elements in the matrix $I M$ , that is $\textit{Cost}_{\textit{Fill}\_\textit{Matrix}}(N,M)\in O(NM)$ .

As to the time of the generation of the functional template file, this process need a linear time of the number of places, that is $\textit{Cost}_{\textit{Gen}\_\textit{Fun}\_\textit{Mod}}(N,M)\in O(N)$ .

The generation of system template file is done in lines 22–26 of Algorithm 9 in Listing 3. This process generate a rule of each transition $j=1,...,M$ . Let $\beta$ denote the value of the element ( $i, j$ ) in the incidence matrix: $\beta=(IM[i,j])$ . The generation of each rule does $\beta N$ computational steps. In the general case, the maximum value of $W$ is bounded by an independent value of $N$ and $M$ , and thus the time of writing a rule is a linear function of the number of places. In this case, the running time of the generation of the system template file will be $\textit{Cost}_{\textit{Gen}\_\textit{Sys}\_\textit{Mod}(N,M)}\in O(NM)$ .

The total cost is therefore $\textit{Cost}(N,M)\in O(NM)$ for the complete proposed algorithm to automatically generate Maude specification of MAS from the corresponding Petri net model.

6. Related works

Quite number of works and tools have been proposed and realized for automatic code generation from Petri nets into many other languages such as to C [27], C++ [25], Java [28, 62], VHDL [26] and PROMELA [54]. However, we cannot compare our work with the most of them because the description languages are radically different and then, we will discuss only those related to the Maude language.

Although, the formal specification of Petri nets based on rewriting logic dates to a couple of decades ago [56], only a little number of works for the automatic generation have been published. For instance, the first rewriting logic based tool is the one presented in [10] for editing, simulating, and analyzing Extended Concurrent Algebraic Terms Nets (ECATNets) via a quasi-complete collection of formal analysis tools. The second one is the approach presented in [34] that combines meta-modeling and graph grammars to automatically generate the Maude specification in order to simulate and analyse ECATNets Models by means A Tool for Multi-formalism and Meta-Modelling (ATOM3). In that work, a Unified Modeling Language (UML) class diagram is used to define a meta-model of ECATNets. Then, a graph grammar is proposed to generate the Maude specification of the specified ECATNets models to perform the simulation.

Finally, to the best to our knowledge, perhaps the most closely related effort to our present work is that presented in [11], where authors have proposed a graphical tool allowing bidirectional translation from colored Petri Nets to Maude and vice versa. At the same time, we should note that all the pre-cited works present their tools as black box, and none of them neither presents a straightforward algorithm to generate the Maude specification nor makes available of such tool. In addition, still the major advantage and thus, contribution of our work is that it is fully automatic and based on a well-defined algorithm.

7. Conclusion and future work

In this paper, we have presented a well-defined algorithm for the automatic generation of Maude specifications from Petri net models representing multi-agent based systems architecture. This algorithm (prototype) will be helpful for all Petri nets practitioners and designers building large models and even who don’t have too much experience with rewriting logic. It will permit them to save time, avoid human related errors during the usually manual translation process as it will give them the opportunity to exploit all Maude advanced analysis tools for their models. Our future work is to create a complete tool or an Eclipse plug-in implementing this algorithm and providing a convenient GUI (Graphical User Interface) interface for end users to edit the Petri net and then generate the incidence matrix and the Maude specification from the Petri net model. In addition, we also aim to generalize the proposed algorithm for other Petri net categories by using the appropriate data structures.

Footnotes

Available at: https://drive.google.com/open?id=12PmlZHrJfhniEseM-uBRuFU3PGisgxPm.

Acknowledgments

This work is financially supported by a grant No: 034/PNE/ENS/Spain/13-14 from the Algerian ministry of higher education and scientific research. In addition, our special thanks goes to my friend BENALI Abdel kamel for his help and guidance in preparing the algorithm time complexity subsection.

Author’s Bios

	Ammar Boucherit received Magister (master’s degree) in software engineering from University of Oum El-Bouaghi, Algeria in 2005. He is currently an assistant teacher of computer science at the Department of Computer Science, University of Echahid Hamma Lakhdhar, El-Oued, Algeria. His research focused on three areas: formal design of computer systems, software architecture and multi-agents systems.
	Abdallah Khababa is currently a full professor at the university of Ferhat abbas Setif, Algeria. He holds a Ph.D. in computer science from the University of Ferhat abbas Setif. His main areas of interest include cognitive science and artificial intelligence, knowledge representation with ontologies and human-machine interface and its usability.
	Laura M. Castro is an associate professor at the University of A Coruña, Spain. She is a member of the MADS (Models and Applications of Distributed Systems) research group. She gives lectures on Software Architecture, and Software Verification and Validation. Her research focuses on software testing (automated, model and property-based testing), applied to software in general, and distributed, concurrent, functional systems in particular.

References

Adameit

Betz

Cabac

Hars

Hewelt

Köhler-Bußmeier

Moldt

Popov

Quenum

Theilmann

et al., Modelling distributed network security in a petri net-and agent-based approach, in: German Conference on Multiagent System Technologies, Springer, 2010, pp. 209–220.

Ali

Khan

Zafar

N.A.

and Ahmad

, Formal modeling towards a dynamic organization of multi-agent systems using communicating x-machine and z-notation, Indian Journal of Science and Technology 5(7) (2012), 2972–2977.

Allan

R.J.

, Survey of agent based modelling and simulation tools. Science & Technology Facilities Council, 2010.

Ammar

and Abdallah

, Towards the formal specification and verification of multi-agent based systems, International Journal of Computer Science Issues (IJCSI) 8(4) (2011), 200–210.

Athamena

and Houhamdi

, A petri net based agent behavioral testing, in: American Journal of Applied Sciences, Vol. 12, 2011, pp. 1876–1883.

Bai

Zhang

and Zhang

, A colored petri net based strategy for multi-agent scheduling, In: Rational, Robust, and Secure Negotiation Mechanisms in Multi-Agent Systems, 2005, IEEE, 2005, pp. 3–10.

Barbosa

P.E.

Costa

de Figueiredo

J.C.

Ramalho

Gomes

et al., Modeling complex Petri nets operations in the model-driven architecture, in: Industrial Electronics, 2009. IECON’09, IEEE, 2009, pp. 4359–4364.

Benmerzoug

Kordon

and Boufaida

, A petri-net based formalisation of interaction protocols applied to business process integration, in: Advances in Enterprise Engineering I, Springer, 2008, pp. 78–92.

Boudiaf

and Bensaber

, Adapting and implementing a reduction rule to ECATNets by using rewriting logic, Engineering Letters 20(2) (2012), 116–127.

10.

Boudiaf

Chaoui

and Bakha

, A rewriting logic based tool for ECATNet’s analysis: Edition and simulation steps description, European Journal of Scientific Research 6(2) (2005), 16–27.

11.

Boudiaf

and Djebbar

, Towards an automatic translation of colored petri nets to maude language, International Journal of Computer Science & Engineering 3(1) (2009), 1078–1083.

12.

Boudiaf

Mokhati

and Badri

, Supporting formal verification of dima multi-agents models: Towards a framework based on maude model checking, International Journal of Software Engineering and Knowledge Engineering 18(7) (2008), 853–875.

13.

Boudiaf

Mokhati

Badri

and Badri

, Specifying dima multi-agents models using maude, in: Pacific Rim International Workshop on Multi-Agents, Springer, 2004, pp. 29–42.

14.

Brahimi

Maamri

and Sahnoun

, Dynamic verification of hierarchical multi-agent plans, Multiagent and Grid Systems 13(2) (2017), 113–142.

15.

Cabac

Moldt

and Rölke

, A proposal for structuring petri net-based agent interaction protocols, in: International Conference on Application and Theory of Petri Nets, Springer, 2003, pp. 102–120.

16.

Celaya

J.R.

Desrochers

A.A.

and Graves

R.J.

, Modeling and analysis of multi-agent systems using petri nets, in: Systems, Man and Cybernetics, 2007. ISIC. IEEE International Conference on, IEEE, 2007, pp. 1439–1444.

17.

Chainbi

, Multi-agent systems: a petri net with objects based approach, in: Intelligent Agent Technology, 2004. (IAT 2004). Proceedings. IEEE/WIC/ACM International Conference on, IEEE, 2004, pp. 429–432.

18.

Chang

Lian

and Shatz

, Applying a nested petri net modeling paradigm to coordination of sensor networks with mobile agents, in: Proc. of Workshop on Petri Nets and Distributed Systems, Xian, China, 2008, pp. 132–145.

19.

Chatterjee

R.K.

Neha

and Sarkar

, Behavioral modeling of multi agent system: high level petri net based approach, International Journal of Agent Technologies and Systems (IJATS) 7(1) (2015), 55–78.

20.

Chatterjee

R.K.

Sarkar

and Bhattacharya

, Modeling and analysis of agent oriented system: Petri net based approach, in: Proceedings of the International Conference on Software Engineering Research and Practice (SERP’11), 2011, pp. 17–23.

21.

Clancey

W.J.

Sierhuis

Seah

Buckley

Reynolds

Hall

and Scott

, Multi-agent simulation to implementation: a practical engineering methodology for designing space flight operations, in: International Workshop on Engineering Societies in the Agents World, Springer, 2007, pp. 108–123.

22.

Clavel

Durán

Eker

Lincoln

Martí-Oliet

Meseguer

and Quesada

, A maude tutorial, Computer Science Laboratory, SRI International, 2000.

23.

Clavel

Durán

Eker

Lincoln

Martí-Oliet

Meseguer

and Talcott

, All about maude – a high-performance logical framework: how to specify, program and verify systems in rewriting logic. Springer-Verlag, 2007.

24.

Filatova

Verburg

P.H.

Parker

D.C.

and Stannard

C.A.

, Spatial agent-based models for socio-ecological systems: Challenges and prospects, Environmental Modelling & Software 45 (2013), 1–7.

25.

Golenkov

Sokolov

Tarasov

and Kharitonov

, Experimental version of parallel programs translator from petri nets to c++, in: International Conference on Parallel Computing Technologies, Springer, 2001, pp. 226–231.

26.

Gomes

Costa

Barros

J.P.

and Lima

, From petri net models to vhdl implementation of digital controllers, in: Industrial Electronics Society, 2007. IECON 2007. 33rd Annual Conference of the IEEE, IEEE, 2007, pp. 94–99.

27.

Gomes

Rebelo

Barros

J.P.

Costa

and Pais

, From petri net models to c implementation of digital controllers, in: 2010 IEEE International Symposium on Industrial Electronics, IEEE, 2010, pp. 3057–3062.

28.

Hagge

and Wagner

, Java code patterns for petri net based behavioral models, in: Industrial Informatics, 2005. INDIN’05. 2005 3rd IEEE International Conference on, IEEE, 2005, pp. 450–455.

29.

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(11) (2001), 2829–2837.

30.

Hoffmann

Ehrig

and Mossakowski

, High-level nets with nets and rules as tokens, in: International Conference on Application and Theory of Petri Nets, Springer, 2005, pp. 268–288.

31.

Hsieh

F.-S.

, Developing cooperation mechanism for multi-agent systems with petri nets, Engineering Applications of Artificial Intelligence 22(4-5) (2009), 616–627.

32.

Jennings

N.R.

and Bussmann

, Agent-based control systems: Why are they suited to engineering complex systems? IEEE Control Systems 23(3) (2003), 61–73.

33.

Kahloul

and Chaoui

, LRN/R-Maude based approach for modeling and simulation of mobile code systems, Ubiquitous Computing and Communication Journal (UbiCC journal) 3(6) (2008), 1–10.

34.

Kerkouche

and Chaou

, A graphical tool support to process and simulate ecatnets models based on meta-modelling and graph grammars, INFOCOMP 8(4) (2009), 37–44.

35.

Kheldoun

Barkaoui

and Ioualalen

, Formal verification of complex business processes based on high-level petri nets, Information Sciences 385 (2017), 39–54.

36.

Köhler

, A formal model of multi-agent organisations, Fundamenta Informaticae 79(3-4) (2007), 415–430.

37.

Köhler

Martens

and Rölke

, Modelling social behaviour with petri net based multi-agent systems, in: Proceedings of the Workshop MASHO, Vol. 3, 2003.

38.

Köhler

Moldt

and Rölke

, Modelling the structure and behaviour of petri net agents, in: International Conference on Application and Theory of Petri Nets, Springer, 2001, pp. 224–241.

39.

Kotb

Y.T.

Beauchemin

S.S.

and Barron

J.L.

, Petri net-based cooperation in multi-agent systems, in: Computer and Robot Vision, 2007. CRV’07. Fourth Canadian Conference on, IEEE, 2007, pp. 123–130.

40.

Laouadi

M.A.

Mokhati

and Seridi-Bouchelaghem

, A formal framework for organization-centered multi-agent system specification: A rewriting logic based approach, Multiagent and Grid Systems 13(4) (2017), 395–419.

41.

Lehmann

and Moldt

, Modelling and analysis of agent protocols with petri nets, in: German Conference on Multiagent System Technologies, Springer, 2004, pp. 85–98.

42.

Marik

and McFarlane

, Industrial adoption of agent-based technologies, IEEE Intelligent Systems 20(1) (2005), 27–35.

43.

Marzougui

Hassine

and Barkaoui

, A new formalism for modeling a multi agent systems: Agent petri nets, Journal of Software Engineering and Applications 3(12) (2010), 1118–1124.

44.

Meseguer

, Conditional rewriting logic as a unified model of concurrency, Theoretical Computer Science 96(1) (1992), 73–155.

45.

Meseguer

, Twenty years of rewriting logic, The Journal of Logic and Algebraic Programming 81(7-8) (2012), 721–781.

46.

Michael

Langer

von Lüde

Moldt

Heiko

Valk

et al., Socionic multi-agent systems based on reflexive petri nets and theories of social self-organisation, Journal of Artificial Societies and Social Simulation 10(1) (2007), 1–3.

47.

Midgley

Marks

and Kunchamwar

, Building and assurance of agent-based models: An example and challenge to the field, Journal of Business Research 60(8) (2007), 884–893.

48.

Monostori

Váncza

and Kumara

S.R.

, Agent-based systems for manufacturing, CIRP Annals-Manufacturing Technology 55(2) (2006), 697–720.

49.

Nowé

Verbeeck

and Peeters

, Learning automata as a basis for multi agent reinforcement learning, in: Learning and Adaption in Multi-agent Systems, Springer, 2006, pp. 71–85.

50.

Nowostawski

Purvis

and Cranefield

, A layered approach for modelling agent conversations, in: The 2nd International Workshop on Infrastructure for Agents, MAS, and Scalable MAS, 2001, pp. 163–170.

51.

Ou-Yang

and Winarjo

, Petri-net integration – an approach to support multi-agent process mining, Expert Systems with Applications 38(4) (2011), 4039–4051.

52.

Perše

Kristan

Perš

Mušič

Vučkovič

and Kovačič

, Analysis of multi-agent activity using petri nets, Pattern Recognition 43(4) (2010), 1491–1501.

53.

Reisig

, A primer in Petri net design. Springer Science & Business Media, 2012.

54.

Ribeiro

O.R.

and Fernandes

J.M.

, Translating synchronous petri nets into promela for verifying behavioural properties, in: Industrial Embedded Systems, 2007. SIES’07. International Symposium on, IEEE, 2007, pp. 266–273.

55.

Schulz

, Model checking of reconfigurable Petri nets. Master’s thesis, University of Applied Sciences, Hamburg, Germany, 2015.

56.

Stehr

M.-O.

Meseguer

and Ölveczky

P.C.

, Rewriting logic as a unifying framework for petri nets, in: Unifying Petri Nets, Springer, 2001, pp. 250–303.

57.

Van Baalen

Caldwell

J.L.

and Mishra

, Specifying and checking fault-tolerant agent-based protocols using maude, in: International Workshop on Formal Approaches to Agent-Based Systems, Springer, 2000, pp. 180–193.

58.

Van der Hoek

and Wooldridge

, Towards a logic of rational agency, Logic Journal of IGPL 11(2) (2003), 135–159.

59.

van Riemsdijk

M.B.

Aştefănoaei

and de Boer

F.S.

, Using the maude term rewriting language for agent development with formal foundations, in: Specification and Verification of Multi-agent Systems, Springer, 2010, pp. 255–287.

60.

Van Riemsdijk

M.B.

De Boer

F.S.

Dastani

and Meyer

J.-J.C.

, Prototyping 3apl in the maude term rewriting language, in: International Workshop on Computational Logic in Multi-Agent Systems, Springer, 2006, pp. 95–114.

61.

Wilensky

and Rand

, An introduction to agent-based modeling: modeling natural, social, and engineered complex systems with NetLogo. MIT Press, 2015.

62.

Willrich

De Saqui-Sannes

Sénac

and Diaz

, Multimedia authoring with hierarchical timed stream petri nets and java, Multimedia Tools and Applications 16(1-2) (2002), 7–27.

63.

Zambonelli

and Omicini

, Challenges and research directions in agent-oriented software engineering, Autonomous Agents and Multi-agent Systems 9(3) (2004), 253–283.

Automatic generating algorithm of rewriting logic specification for multi-agent system models based on Petri nets

Abstract

Keywords

1. Introduction

2. Literature review

2.1 Petri nets based works

2.2 Rewriting logic based works

2.3 Synthesis

3. Preliminaries

4.1.1 Incidence matrix

4.2.1 Specification modules creation

Table 1 Incidence matrices

6. Related works

7. Conclusion and future work

Footnotes

Acknowledgments

Author’s Bios

References

Table 1
Incidence matrices