Converting Reconfigurable Petri Nets to Maude

Model checking is an important aim of the theoretical computer science. It enables the verification of a model with a set of properties such as liveness, deadlock or safety. One of the typical modelling techniques are Petri nets they are well understood and can be used for a model checking. Reconfigurable Petri nets are based on a Petri nets with a set of rules. These rules can be used dynamically to change the net. Missing is the possibility to verify a reconfigurable net and properties such as deadlocks or liveness. This paper introduces a conversion from reconfigurable Petri net to Maude, that allows us to fill the gap. It presents a net transformation approach which is based on Maude's equation- and rewrite logic as well as the LTLR model checker.


Motivation
The first approach to convert reconfigurable Petri net to Maude (see [Schulz, 2014]) is designed as extension for ReConNet. It uses the implementation of ReConNet to get all possible matches for a set of rules and a given Petri net. This approach results in a dependency of the current net state and the algorithm of ReConNet. Hence, that the model-checking process has only one-step application of a rule may be wrong if a rule is used twice, because an error may occur after the second usage.
The new approach is based on the algebraic structure of reconfigurable Petri nets. The main task was to create a structure which can be read similar to the mathematical notation of a reconfigurable Petri net. It includes the possibility to simulate the net. This implies a solution for a transition that defines the activation and firing. Maude has been chosen as the appropriate language to implement this definition.
Moreover, the rules need to be implemented within the new structure. In contrast to the first approach it should be able to detect a match itself.
The following sections contain an overview of all relevant parts of this approach. The first section gives a short overview of the background for this work. The next section focuses the new modules, which contain the data-types for the resulting Maude specification of a converted reconfigurable Petri net. Finally, an evaluation shows the performance of the current implementation based on a test net.

Background
First we introduce reconfigurable Petri nets. They extend Petri nets with a set of rules, that can modify the net at runtime. Moreover, Maude is introduced since it is the result the conversion aims at. Finally, a short survey of related works is presented.

Reconfigurable Petri nets
One of the most important models for concurrent systems and some software engineering parts are the Petri nets, based on Carl Adam Petri's dissertation [Petri, 1962].
A marked Petri net can be formally described as a tuple N = (P, T, pre, post, M 0 ) where P is a set of places and T is a set of transitions. pre is used for all pre-conditions of transitions, which describes how many token are required for firing. On the other hand, post holds all information of the post-conditions for all transitions. Finally, M 0 shows all initial tokens on the places for this net N [Meseguer a. Montanari, 1990;Juhas et al., 2007].
Further, based on a Petri net are reconfigurable Petri nets important because they can modify themselves with a set of rules [Ehrig et al., 2007;Kahloul et al., 2010]. A reconfigurable Petri net can be describe a tuple of a reconfigurable Petri net RN = (N, R). This definition uses the Petri net tuple and a set R of rules, which are given by rule r = (L ← K → R) [Padberg, 2012;Ehrig et al., 2009]. L is the left-hand side (LHS), which needs a morphism to be mapped to a net N . K is an interface between L and R. R is the part which is inserted into the original net. To realise this replacement a matching algorithm needs to be defined that finds L within the source net N . This match includes a mapping between the elements in the Petri net and the left side of the rule (L). Basically, this algorithm finds the same structure (form L) within the Petri nets [Blumreiter, 2013].
Reconfigurable Petri nets are also comprises capacities and labels for transitions/places [Padberg, 2012]. A limitation for place is realised via a capacity, that contains a value which describes how much token can be stored on a place. The function cap : P → N w + assigns for each place a natural number as capacity. Further, two label function (pname and tname) refer for each place or transition a name from a name space (pname : P → A P and tname : R → A T ).
ReConNet is shown in Figure 1 with an example net N 1 and rule R 1 . The configurations such as node names or markings as well as the control elements for firing and transformation are presented in the upper region of the graphical interface. A graphical illustration of reconfigurable Petri nets is in the remaining interface. First, a net which models a cycle is composed of three places and transitions as well as one token. Wider, a rule which changes the arc direction of a transition is displayed under the net. In both editors are activated transitions marked as black transitions instead of grey normal transitions. Colours for places in rules are used to ensure the common bond.

Maude
Maude has been developed at the Stanford Research Institute International (SRI International) for the last two decades. The equation and rewriting logic, which supports a powerful algebraic language, is used as a base [Escobar et al., 2009;Clavel et al., 2002]. Based on these two kinds of logics Maude models a concurrent state systems that used for semantic analysis such as deadlock discovery via LTL-model-checking-module [Katoen a . Baier, 2008;Eker et al., 2004].
Maude consists of a core which is named " Maude Core". On top of its core every other part is written in Maude itself. Actually, Maude is distributed in version 2.6 form the website 1 [Clavel et al., 2011].
A program in Maude is based on one or many modules where every part of the system looks like a clear to read abstract data type (ADT). A module contains a set of types, which are used with the " sort"-keyword. It is also possible to define more than one type with the plural form " sorts". Each type describes a property for the module. For example types for a Petri net can be described with: sort P laces T ransitions M arkings .
If this operator has to be associative (in Maude with a short version: " assoc") and commutative (short with: " comm") properties, Maude defines this in the end of this line. Hence, we obtain a multiset of markings by this operator. The notation allows these properties in box brackets, so that it can be written as: Maude uses the equation logic to define the validity for an operator (axioms). This can be exemplified with the initial marking from a Petri net. This marking is a representation of the initial state of the Petri net. Based on this information we can define an operator that describes the initial state of a Petri net. After that, the validity with an equation can added.
If we have a Petri net with only one marking with an " A" label we obtain these two lines: eq initial = A .
Types are defined as " sort", operators as functors and equations as the validity of operators.
The rewrite rules can be used to replace one multiset with another multiset. So all terms are immutable as in many functional languages. A replacement rule consists of two multisets, where the first set is replaced with the second one. These two termsets are separated with a double arrow, as shown in the following example, where a term A is replaced with a new term B: Based on this example an implementation of the token game of Petri nets can be realised.
The two multisets can be seen as pre-and post-set of a transition. Hence, a rule can be used to describe a firing step with this two sets. This replacement rule can be modelled with the following graphical representation:

Related Work
The basic example for a Petri net to Maude conversion uses a shop system, where a user can buy an apple or candies. The mapping into Maude uses the term replacement system to model the firing steps of this net. Based on this Maude-structure it is possible to add a model-checking possibility, which can be used to verify a deadlock or safety properties [Clavel et al., 2011].

Figure 3: Shop example with apple and candy
A more complex example of this modelling (see Figure 3) is shown with high level nets in [Stehr et al., 2001]. It presents a conversion of the banker problem where two credits are handled by the net structure. The focus of the work lays on the soundness and correctness for this conversion approach. A formal definition of the model and the operators as well as the firing of a transition is given. Further, the paper presents an approach for a coloured Petri net (CPN). It extends the previous approach with more complex operators for the firing replacement rules. The conversion of transitions is realised via Maudes replacement rules and operators which contain the coloured tokens.
Automatic mapping for UML-models to a Maude-specification (see [Chama et al., 2013]) is similar to this paper's idea of converting reconfigurable Petri nets. In [Chama et al., 2013] the authors present three steps modeling, analysing and converting to Maude modules.
The first step focuses on subject-specific modeling within UMLs class, state or components diagrams. After that step, the tool AtoM is used to convert the model into a Pythoncode representation. This code will be used to solve some constrains inside the UML-model components and some diagram specific parts. Lastly, the final step transfers all data into a Maude-specification, which can be used to verify some properties for example deadlocks.
In [Barbosa et al., 2011] Petri nets are also converted into Maude-modules. As a base an Input-Output Place/Transition net (IOPT net) is used and saved in a PNML-file. These files are the origin for the conversion process. Further, PNML is used as a well-known markup-language for Petri nets. This process divides all components of a Petri net in special Maude-modules (net, semantic and initial markings) which can be used to verify in a same way as in [Chama et al., 2013].
A use case for the resulting Maude structure is presented in [Bjørk, 2006] [Stehr et al., 2001]) which are simulations with one step commands. After one step the tool is capable to present the results.

Data type
A reconfigurable Petri net N 1 consists of a tuple which is separated in a Petri net N and a set of rules R. It can be written with N 1 = (N, R). Furthermore, a Petri net can be formally described as a tuple N = (P, T, pre, post, M, cap). Where P is a set of places, T is a set of transitions, pre and post are functions which maps T → P ⊕ and finally M is the initial marking. Additionally, a function cap : P → N ω can be used to model a capacity of a place P with a value N ω [Padberg, 2012].
An example of a Petri net is shown in Figure 4. Each blue circle is a place and each rectangle is a transition. The arrows between these elements describe the arcs, which can connect a place with a transition and vice versa. The two black points are tokens which can be consumed by a transition. The example in Figure 5 shows a rule which changes the direction of an arc for a transition T . The change is realised by two steps. At first, the match of the left-hand side ensures that the rules can be applied. And finally, the right-hand side contains the information to be used.
This example contains a transition which connects the places in reverse order (arc colour black). However, the mapping net contains both transitions. The arc inversion is realised by a deleting one transition and adding a new transition with reversed arcs. The aim of this work is to create Maude modules, which provides the possibility to create a formal writing of a reconfigurable Petri net. The example net in Figure 4 can be formally indicated as: First, all sorts are defined. A sort can be understand as a type which contains the semantic.    which are a mapping between a transition and a multi-set of places. Finally, the markingoperator contains a multi-set of Places. The content is separated with an additional symbol as the linear sum in the mathematics definition in Figure 6.
The example in Figure 6 can be written in Maude as in Listing 2. It separates all operators and the included multi-sets with commas. Each multi-set is wrapped with curved brackets.
A place is modelled as tuple with p(<label> | <identifier> | <capacity>). Labels are defined as a string, identifier and capacity as numbers. Transitions are based on the tuple t(<label> | <identifier>). Each type has the same type as for the place.
Listing 2: Maude module for a Petri net

Activation and Firing
A transition t is activated, written by m[t , when the following two conditions are satisfied.
The first condition consists of the pre-set of this transition. The net marking has to contain at least as many tokens, as described it in the pre-set (see Equation 7). Furthermore, all post places have to satisfy the capacity condition. Adding more tokens than a place can store is not possible (see Equation 8).
If both conditions are satisfied, the transition t can fire. One firing step is written with where m is the current marking and m is the following marking. The calculation of m is described in Equation 9. First, the pre-set is deducted from the current marking.
Now the post-set of t can be added to the result. The source code consists of the helper method leeqth with . This operator tests the capacity of a place multi-set and a single place. The third parameter is used to count the occurrence of a token in the multi-set. In case that the counter is bigger than the capacity it returns false. All other cases results with true. Listing 4: Capacity proof of each place in the post-set

LTL Properties
The aim of this work is to verify properties such as deadlocks, liveness or reachability for a reconfigurable Petri net. To realise this Maude's LTLR implementation is used. It is based on an implementation of the linear temporal logic (LTL). The implementation itself uses a Kripke structure, which is realised on the basis of the equation and rewriting logic, basically a finite transition system [Eker et al., 2004].
The following examples in Listing 15 ff. are using the operators defined in Listing 5. It contains an operator for the reachability of a marking. The enabled-operator includes the activation of a transition as well as the ability to apply a rule. Finally, the last three lines in Listing 5 include a standard equation, which is used when no other equation can be used.
The implementation starts with a sub sorting of the Configuration-type. This is necessary because the Kripke structure is based on these informations. It means that all Configurationobjects are relevant for the construction of the states of the Kripke structure. In terms of this work a Configuration-object contains a snapshot of a reconfigurable Petri net. At the beginning it includes the initial marking and the primal state of the net without any transformation with rules. All other following conditions include the further interactions of the net (in this case the Configuration with firing steps and rule treatments).

Matching of Rules
A reconfigurable Petri net consists of a net and a set of rules R. Each rule contains three sub-nets, which contain a net L for matching, a net R for the replacement and a net K that maps between the two nets.
The first project [Schulz, 2014] is based on ReConNet. This tool provides the capability to find non-deterministic matches for a net and a set of rules [Blumreiter, 2013]. The aim of the first project is an extension that enables ReConNet to verify a net with a given set of rules. The verification process is realised by a conversion to a Maude specification. In order to realise this process, an interface is designed for using ReConNet to find a match. Due to this constellation, only the initial state of a net and all rules can be verified with the LTL-process.
The new aim is to ensure that the Maude specification finds the matching itself. This implies a possibility to define a rule in this specification as well as the dangling-condition (see section 3.4). Further, the meta-data configuration (such as current highest identifier) should adapt a net and a set of rules.
The definition of a rule and the meta configuration can be found in Listing 6. First, the sorts Rule, LeftHandSide and RightHandSide are defined. This models the two sides of a rule. The mapping net K is not included, because it is not relevant for matching of a rule.
Further, the Configuration consists of a net, a multi-set of rules and a global ID-count. The net contains all information as places, transitions, markings and pre-as well as post-sets.
Each rule multi-set entry contains a left and right side. At last the ID-count is used for each insertion step, where a new transition or a place will be added. The whole rule is written as a condition replacement. If the conditions satisfied with the current net, the rule can be applied. Due to the replacement, the left-hand side of the rule is replaced with the right-hand side. Furthermore, a rule is working with a configuration object. It uses a net, a multi-set of rules as well as an ID-count.
The example in Listing 7 shows the left side of the rule in Figure 5. The net which should be found, consists of two places with the label A. Further, it contains a transition T which connects the two places. A description of the arcs can be found in the pre-and post-set. At last it contains a marking on the place A. All these elements are part of the net in the rule.
It only differs in the ID, which are not given as concrete numbers. Each Irule<number> is a variable that is used for finding a structural match. If the net has the same structure, but other ID's for the places and transitions, this rule is also activated. This is possible because Maude maps the ID's internal with each variable. Moreover, each set contains a variable for possible residual elements. For example, in this net the set places contains more than two places. The remaining place's are mapped into the variable P Rest, so this rule is still activated. If a multiset has no more elements the identities (id) is used (for a definition see Listing 1). Each id itself is the empty-set constant operator (such as emptyPlace, emptyTransition, emptyMappingTuple or emptyMarking).
It calculates the new identifier which is detailed described in subsection 3.5.

Dangling-Condition
A special part of a rule matching is the gluing condition. This condition is separated into the identification and dangling condition. The identification condition requires that no place or transition is specified to be simultaneously added and deleted. Further, the dangling condition defines that a place can only be deleted if there are only arcs to transitions, that are deleted as well. Transitions are not relevant for dangling condition.
The example net N 2 in Figure 7 shows a short example, where a place A (the red place) should be deleted with rule r 3 in Figure 8. The rule has only one match because the bottom part of the net differs in an addition transition. This transition injured the dangling condition and the rule cannot be used at this point.

A T A
A T A T

Multi-Set for used Identifiers
One problem of Maude is the missing garbage collection 2 . This can result in an overflow if a rule inserts a node (place or transition), because each new node gets an identifier.
To solve this problem a multi-set of unique identifiers is used. It requires a modification of the Configuration definition which is introduced in Listing 6. Now it contains an integer for the maxID and for the defined step size. Further, it has two sets for the place and transition identifiers. The implementation can be found in Listing 11.

Transformation
This section includes the architecture of the conversion process as well as the results of some model checking formula.

Architecture
The output base of ReConNet consists an extension of PNML 3 . PNML is a XML-based standard for the Petri net export. The graphical editor ReConNet uses this standard for the persistence of developed nets. In addition to the pure PNML-standard, a rule is stored with its three net in a PNML file.
Based on PNML, this work uses XSL to realise the conversion. The result uses the Maude modules which are defined before the conversion.The sorts for Places, Transitions and the net itself are previously defined. And further it contains the logic of firing or the identification of the dangling condition (see also the definition of all modules in the listings above).
The XSL process is designed with the separation of the global types as places, transitions, pre or post. Further, it has the specific sub xsl-templates for the conversions as in the net, rules, prop or rpn. The structure is summarized in Figure 9. The global types are defined above the specific modules that are grouped together in separate packages. The difference to the first project is that this approach is independent of ReConNets implementation. The first project uses the persistence-module of ReConNets to load PNML-files (net or rule) [Schulz, 2014]. This approach is superior because it is built up directly on the PNML data. The conversion process is written with XSL, which provides a well known language. The interface between this approach and ReConNet is realised through an export to the PNML files that can be used with a net or few rules.

Results
Based on the result of the conversion process it is possible to use Maude's LTL implementation. The prop.maude-module includes all the necessary code for the LTL process (see Listing 14). It subsorts the Configuration-typ under state, which is required (for the Configuration-typ see Listing 6).

Listing 14: Sub sorting of Configuration with State
In the first example, the deadlock freedom of example Figure 4 will be shown. The formula is based on the box-and diamond-operator. In total it describes the semantic of liveness.
It means that a property is globally (box) repeatedly (diamond) true. To write the liveness property for the reconfigurable Petri net modules, the following line can be used: marking{p("A" | 17 | 2147483647)}))) 26 28 10 aidPlace{26, (27,(28,(29,(30,(31,(32,(33,(34,(35,( 30 36))))))))))} aidTransition{26, (27,(28,(29,(30,(31,(32,(33,(34,(35,(36))))))))))} 32 ,deadlock}) Listing 15: Counterexample of a deadlock The meaning of this counterexample is that the rule consists of this marking. It is possible that all tokens are on one place. Furthermore, this place has only incoming arcs which results in a deadlock. The net-state with this deadlock is modelled in Figure 10. Figure 10: State of N 1 with a deadlock (r 1 can not be applied) In assumption that the markings were changed on the places within the rule (see Figure 11) the result is varied, shown in Listing 16. It shows, that the net N1 and rule r2 are deadlock free. The new rule prevents the situation in Figure 10, where the marking can be located on one place which has only incoming arcs. Hence, two situations are possible. First, the rule is not enabled when a marking is at a place, where all arcs are starting. The net itself can fire. On the other hand, a marking will be placed on a place where one or more arcs are incoming. For this case, the rule can be used. The result is that a transition is enabled now and will also continue to be used for the token game. In either situation, an operator of Listing 5 is enabled since the enabled-operator is defined for the firing and transformation step. The reachable-operator is designed to find a given marking. The formal definition of this operator is: Therefore, it is possible to test one or many tokens. In the example bellow (see Listing 18) two tokens (A 3 and A 3 ) are searched in N 1 . Maude's result describes a situation where it found a deadlock with two tokens on A 2 .

Evaluation
This section presents a first step of the performance evaluation of this approach. The evaluation is based on two steps. At first, a net is converted into the Maude modules. And after that step it is tested with the liveness formula (see the first formula in section 4.2).
The conversion uses a net which is build as a circle and the rule r 1 (see Figure 5). Further, it contains one token at place P 1 . The structure connects a place with two transitions (one for the pre and vice versa). Hence, it is possible to build a test which shows the performance of a net which can be scaled with the size of nodes (places and transitions).
For this work four net sizes are used, which allow to make a meaningful statement. Each net has the same semantic and should return true. Hence, only the runtime meta-data such as rewrite count and time are different. The conversion process runs in each case with nearly the same time (see Table 1). Further, the rewrites are grown linear with the size of nodes.
It takes 109 rewrites for 10 places and transitions. If the net has twice as many nodes as in the first example, it takes 209 rewrites. Only the used time grows exponentially. It changes from 13 ms to 23994 ms. If the net receives only 4 new nodes, it grows to 189939 ms (see Table 2). The resulting state-space explosion was expectable as a well known issue of LTL [Valmari, 1998].

Future Work
An outlook of the following work is shown in this section. The formal founding represents the essential part of the conversion from a reconfigurable Petri net to Maude. The aim is the verification of the soundness and correctness for the conversion and target representation of the net in Maude.
Furthermore, an integration of parts from a reconfigurable Petri net such as negative application conditions (NACs) (see [Rein et al., 2008]) or decorations (see [Ede et al., 2012]) should be realised. This enables the verification of the nets and rules from the Living Place Hamburg [Ede et al., 2012].
Finally, a benchmarking is necessary between this approach and a tool such as Charlie 7 to obtain a meaningful statement. This implies a way which converts a reconfigurable Petri net into a net that can be used from other verification tools. The main challenge is to realise a conversion which contains the net and all possible rule conditions.

Reconfigurable Petri Nets -NET.maude
mod NET is 2 including PROP .