Conference Organization SUMo Programme Committee
External Reviewers
CompoNet Programme Committee
Distributed Veri cation of Modular Systems : : : : : : : : : : : : : : : : : : : : : : : : : :
Mohand Cherif Boukala, Laure Petrucci Compositional Analysis of Discrete Time Petri nets : : : : : : : : : : : : : : : : : : : Yann Thierry-Mieg, Beatrice Berard, Fabrice Kordon, Didier Lime, Olivier H. Roux On the modularity in Petri Nets of Active Resources : : : : : : : : : : : : : : : : : :
Vladimir A. Bashkin
Optimising the compilation of Petri net models : : : : : : : : : : : : : : : : : : : : : : :
Lukasz Fronc, Franck Pommereau Generalized Buchi Automata versus Testing Automata for Model Checking 65
Ala Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon When Gra ti Brings Order : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : Alban Linard, Didier Buchs 81 1 17 33 49 Distributed Verification of Modular Systems
M.C. Boukala1 and L. Petrucci2
BP 32 El-Alia Algiers, ALGERIA boukala@lsi-usthb.dz
99, avenue Jean-Baptiste Clément
F-93430 Villetaneuse, FRANCE
Laure.Petrucci@lipn.univ-paris13.fr Abstract. The use of distributed or parallel processing gained interest in the recent years to fight the state space explosion problem. Many industrial systems are described with large models, and the state space being even larger, it does not fit completely into the memory of a single computer.
To avoid the high space requirement, several reduction techniques have been proposed: modular verification, partial order reductions, symmetries, using symbolic or compact representations like BDDs.
Another way to alleviate the state space explosion problem is to use modular analysis, which takes advantage of the modular structure of a system specification, particularly for systems where the modules exhibit strong cohesion and weak coupling.
In this paper, we propose to combine distributed processing and modular analysis to perform verification of basic behavioural properties such as reachability, deadlock states, liveness, and home states and their distributed analysis for modular systems. Each module is assigned to a process which explores independently the internal activity of the module, allowing a significant reduction in the size of the state space rather than in an interleaved fashion.
Keywords: Modular systems, distributed verification, modular analysis, Petri nets. 1
Introduction Systems developed nowadays are both more and more complex and critical. When addressing the design of such systems, it is necessary to ensure reliability, by verifying the system properties. The main approach to verification consists in the generation and analysis of the state space. Some properties such as reachability or deadlocks can be verified on-the-fly, and only require information on states reachable from the initial marking. On the contrary, liveness and home states are elaborate properties which require a full generation of the state space including not only nodes but also arcs. Even for small models, the size of the state space may be too huge to fit in the memory of a single computer.
To cope with the state space explosion problem, several reduction techniques have been proposed: on-the-fly verification checks properties during the state space construction; sweep-line construction [Sch04] considers a progress measure, and discards states that will not be encountered further in the construction; modular verification [LP04]; partial order reductions [Val92,NG97]; symmetries [AHI98,CFJ93]; using symbolic or compact representations like BDDs and Kronecker algebra.
Recently, several studies addressed distributed verification, many of them focussing on distributed LTL model-checking [BBS01,BO03,LS99,BP07]. These works are mainly based on the partionning of the state space.
The performances of distributed verification depends on several criteria, e.g. load balancing of the partitioned state space, but also, more importantly, on a good partitioning. Therefore, choosing an adequate hash function to assign nodes to processors is important.
In [LP04] the modular analysis approach examines in isolation the local behaviour of each subsystem, and then separately considers the synchronisation between the subsystems. In this fashion, exploring the many possible interleavings of activity of the subsystems is avoided, thus reducing the state space.
In this work, we propose to combine modular analysis and distributed processing to improve consequently the systems verification. We focus on checking usual properties such as reachability, liveness and home states.
The paper is organised as follows. We assume the reader is familiar with basic Petri nets notions. Hence, we recall in Section 2 only the modular concepts, i.e. Modular Petri nets and Modular State Spaces. In section 3, we introduce algorithms based on distributed modular construction of the state space. In section 4 distributed verification of various properties is presented. These algorithms have been implemented in a prototype tool and experimental results are presented in section 5. Finally, section 6 concludes the paper. 2
Modular Petri Nets In this paper, we consider only modules synchronised through shared transitions as in [LP04]. 2.1
Definition of Modular Petri Nets Definition 1 (Modular Petri net). A modular Petri net is a pair MN = (S, TF ), satisfying: 1. S is a finite set of modules such that: – Each module, s ∈ S, is a Petri net: s = (Ps, Ts, Ws, M0s ). – The sets of nodes corresponding to different modules are pair-wise disjoint: ∀s1, s2 ∈ S : [s1 6= s2 ⇒ (Ps1 ∪ Ts1 ) ∩ (Ps2 ∪ Ts2 ) = ∅]. – P = S Ps and T = S Ts are the sets of all places and all transitions s∈S s∈S of all modules. 2. TF ⊆ 2T is a finite set of non-empty transition fusion sets.
In the following, TF also denotes Stf ∈TF tf . We now introduce transition groups.
Definition 2 (transition group). A transition group tg ⊆ T consists of either a single non-fused transition t ∈ T \ TF or all members of a transition fusion set tf ∈ TF .
The set of transition groups is denoted by TG.
A transition can be a member of several transition groups as it can be synchronised with different transitions (a sub-action of several more complex actions). Hence, a transition group corresponds to a synchronised action. Note that all transition groups have at least one element.
Next, we extend the arc weight function W to transition groups, i.e. ∀p ∈ P, ∀tg ∈ TG :
W (p, tg) = P W (p, t), t∈tg
W (tg, p) = P W (t, p).
t∈tg Markings of modular Petri nets are defined as markings of Petri nets, over the set P of all places of all modules. The restriction of a marking M to a module s is denoted by Ms. The enabling and occurrence rules of a modular Petri net can now be expressed.
Definition 3 (Transition group enabledness). A transition group tg is enabled in a marking M , denoted by M [tgi, iff:
∀p ∈ P : W (p, tg) 6 M (p) When a transition group tg is enabled in a marking M1, it may occur, changing the marking M1 to another marking M2, defined by:
∀p ∈ P : M2(p) = (M1(p) − W (p, tg)) + W (tg, p).
Example: The (full) state space for the modular Petri net of figure 1 is shown in figure 2. Note that the initial state is shown as A1B1C1, thus indicating that place A1 is marked with a token in module A, place B1 is marked with a token in module B, and place C1 is marked with a token in module C. In this initial state, only transition F1 is enabled, its occurrence leading to state A2B2C1.
When considering the modular state space, as well as checking properties of the system, we will use Strongly Connected Components. The set of all strongly connected components is denoted by SCC. For a node v and a component c ∈ SCC we use v ∈ c to denote that v is one of the nodes in c. A similar notation is used for arcs. We use vc to denote the component to which v belongs. A1 F1 A2 F3 tB A3 tA
C1 F2
C2
Modular State Spaces In the definition of modular state spaces, we denote the set of states reachable from M by occurrences of local (non-fused) transitions only, in all the individual modules, by [[M i.
The notation with a subscript s means the restriction to module s, e.g. [M is is the set of all nodes reachable from the global marking M by occurrences of transitions in module s only.
We use M [[σiiM 0 to denote that M 0 is reachable from M by a sequence σ ∈ (T \ T F )∗T F of internal transitions followed by a fused transition. In the definition of modular state spaces we need a compact notation to capture the states reachable from M in all the individual modules. It turns out that we can use a product of SCCs of the individual modules to express this representative node: for any reachable marking M , we use M c to denote the product (or tuple) of Strongly Connected Components (SCCs) Msc of the individual modules: ∀M ∈ [M0i : M c =
YMsc. s∈S The definition of a modular state space consists of two parts: the state spaces of the individual modules and the synchronisation graph.
Definition 4 (Modular state space). Let MN = (S, TF ) be a modular Petri net with the initial marking M0. The modular state space of MN is a pair MSS = ((SS s)s∈S , SG), where: 1. SS s = (Vs, As) is the local state space of module s: (a) Vs = S [vis v∈VSG
A2B3C2 F3 (b) As = {(M1, t, M2) ∈ Vs × (T \ TF )s × Vs | M1[tiM2} 2. SG = (VSG, ASG) is the synchronisation graph of MN : (a) VSG = [[M0iic (b) ASG = {(M1c, (M∪M10c,0ctf ), M2c) ∈ VSG × ([M0ic × TF ) × VSG | M10 ∈ [[M1i ∧
M10 [tf iM2}
A detailed explanation of the definition is given in [LP04]: (1) The definition of the state space graphs of the modules is a generalization of the usual definition of state spaces.
(1a) The set of nodes of the state space graph of a module contains all states locally reachable from any node of the synchronisation graph.
(1b) Likewise the arcs of the state space graph of a module correspond to all enabled internal transitions of the module. (2) Each node of the synchronisation graph is labelled by a M c and is a representative for all the nodes reachable from M by occurrences of local transitions only, i.e. [[M i. The synchronisation graph contains the information on the nodes reachable by occurrences of fused transitions.
(2a) The nodes of the synchronisation graph represent all markings reachable from another marking by a sequence of internal transitions followed by a fused transition. The initial node is also represented.
(2b) The arcs of the synchronisation graph represent all occurrences of fused transitions.
The state space graphs of the modules contain only local information, i.e. the markings of the module and the arcs corresponding to local transitions but not the arcs corresponding to fused transitions. All the information concerning these is stored in the synchronisation graph.
The nodes of the synchronisation graph represent all markings reachable from another marking by a sequence of internal transitions followed by a fused transition. The initial node is also represented.
The arcs of the synchronisation graph represent all occurrences of fused transitions. Each arc is labelled by the corresponding fired transition and by the SCCs of the markings which enabled this transition. But only the SCCs of the participating modules do appear.
Example: The modular state space for the modular Petri net of figure 1 is shown in figure 3. Note that there is a local state space for each module, as well as a synchronisation graph which captures the occurrence of fused transitions. We do not distinguish between nodes and SCCs since, in this case, all SCCs consist of a single node (which is seldom the case in practice).
Module A
Module B
Module C
Synch. Graph A1 A2
A3
B1 B2 B3 tB
C1 C2
A1B1C1
Although sketches of algorithms were introduced in [LP04], we give here the description of the distributed algorithms for the construction of the state space and for the verification of the reachability, dead markings, liveness, and home states properties. 3
Distributed Construction of the Modular State Space Several works have developed distributed tools generating and exploring the state space on a cluster of workstations. Partitioning the set of states over the different stations is done using a hash function [GMS01,KP04,AAC87,LP04]. This approach can handle larger state spaces but still remains limited.
Here, we consider a different approach based on modularity to achieve a distributed construction of the state space and the verification of various properties.
In this approach we also used two types of processes. They consist in a coordinator process and N worker processes, one worker process for each module, as in [KP04].
The coordinator constructs the synchronisation graph, coordinates the different worker processes and determines the termination of the modular state space construction, while every worker generates the local state space of the module it is assigned by firing only internal transitions.
The coordinator process starts by sending the initial marking M0s restricted to module s to each worker process, and waits for receiving the states enabling fused transitions from the workers processes.
Algorithm 1: Internal State Space Generation() 24 25 end forall the tf ∈ TF s.t. M [tf i do /* M enables a fused transition tf */
TFWaiting ← TFWaiting ∪ {(M, tf )};
Waitings ← Waitings \ {M } if TFWaiting = ∅ then
EndOfGeneration = true else while TFWaiting 6= ∅ do
Choose (M, tf ) ∈ TFWaiting s.t. M [tf iM 0 Waitings ← Waitings ∪ {M 0} TW .label = M c TW .AncSCC = AncSCC (M ) TW .tr = tf TW .SuccSCC = M 0c Send (Sender = s, Dest = Coordinator, Type = SynchTrans,
Content = TW )
Send (Sender = s, Dest = Coordinator, Type = END_GENERATION)
When a worker process s receives the initial marking, it adds it to the sets Vs and W aitings, that correspond respectively to the set of local markings and the set of markings which are visited but not explored yet. The worker process then invokes algorithm 1 to generate the internal state space of the module it is assigned. Function Add (M ) adds the marking M to both sets Vs and W aitings if it is not already in Vs.
The workers send enabled fused transitions to the coordinator process. Actually, the message sent to the coordinator not only contains the fused transition tf but also the SCC number M c of the marking enabling tf , and the SCC number of its predecessor marking in the synchronisation graph (in a field AncSCC ).
The communications are asynchronous. Thus, when receiving a message, the coordinator and worker processes are preempted and a handler function MessageHandler() is invoked. Algorithm 2 describes the actions performed by the coordinator when it receives a fused transition from the worker process s.
The parts handling other messages are not detailed. They concern the algorithm termination (and is similar to the termination in [KP04]), as well as the analysis messages introduced in section 4.
First, the coordinator creates the initial node v0 = M0c ∈ VSG. When a fused transition tf is received from a process s, the successors of a node v = (v1, v2, . . . vN ) ∈ VSG are computed as follows: – we consider the set PM of the modules (processes) participating in the synchronisation of the fused transition tf ; – we construct the sets: • Wpm corresponding to the fused transition tf received earlier from other processes; • Ws corresponding to the fused transition received from process s; • Wnp contains • for modules not participating in the synchronisation; – for all possible combinations, the successor nodes in the synchronisation graph are calculated.
The successor states thus computed are sent to the worker processes for an additional round of internal state space generation. 4
Properties A major issue is the analysis of concurrent systems properties. The reachability graph is the basic model on which most verifications are built. Behavioural properties, which depend on initial marking, and the reachability graph are often used to perform such analysis.
In this work we focus on basic behavioural properties: reachability, deadlocks, liveness, home state and their distributed analysis. 4.1
Reachability The reachability problem for Petri nets consists in proving that a given marking M is in [M0i. This property is often used to check whether a faulty state M is reachable, e.g. an elevator moving while the door is open. It is convenient to look for erroneous states. Algorithm 2: Message Handler() 1 begin . .
. 2 if Message.Type = SynchTrans then
/* message received contains an enabled fused transition */ 3 tf = Message.Content.tr 4 s = Message.Sender 5 PM = {i s.t. tf ∈ Ti}
/* PM: modules participating in the synchronisation of tf */ 6 foreach v = (v1c, v2c, · · · , vNc ) ∈ VSG do 7 foreach pm ∈ PM and pm 6= s do 8 Wpm = {w ∈ SGWaitingpm s.t. 9 (w.AncSCC = vpcm) ∧ (w.tr = tf )}
/* Wpm: markings enabling tf , with vpm as ancestor */ Ws = {Message.Content} foreach C = (c1, c2, · · · , cN ) s.t. ∀i ∈ PM , ci ∈ Wi do v0 = (v0c1, v0c2, · · · , v0cN ) where:
∀i ∈ PM , v0ic = ci.SuccSCC and ∀i 6∈ PM , v0ic = vic Add (v0) AddArc (v, (C , ft), v0) foreach pm ∈ PM do
Send (Sender = Coordinator, Dest = pm, Type = NEW_NODE,
Content = vp0m) SGWaitings = SGWaitings ∪ Message.Content
In some applications, one may be interested in the markings of a subset of places and not care about the others places in the net. This leads to a submarking reachability problem.
Reachability is known to be decidable. For modular systems, determining whether a given state M is reachable from the initial marking can be done in a parallel way: each worker process s searches through its local state space Vs. Then, if one of the worker processes does not find Ms in its local state space Vs, marking M is not reachable. Otherwise i.e. (∀s ∈ {1..N } Ms ∈ Vs), all the workers send the ancestor SCCs of Ms to the coordinator. The coordinator stores the SCCs received from each worker s and checks whether there exists a combination of these in the set of nodes of the synchronisation graph VSG. 4.2
Deadlocks The algorithm used to find dead markings in a modular state space is based on the following proposition: Proposition 1 (Deadlocks).
M ∈ [M0i is a deadlock ⇔ [ ∀s ∈ S : (M s)c ∈ T erm(SCCs) ∩ T rivial(SCCs)) ∧(∀(v1, (M1c, tf ), v2) ∈ ASG : M1c 6= M c)]
Each worker process s searches in its local state space for the local dead markings which consist in trivial terminal SCCs. If there exists a worker process without such a node, the module assigned to this worker always allows a local behaviour. Hence, the system is deadlock-free. Otherwise, every worker process sends the SCCs corresponding to the locally dead markings to the coordinator process.
The coordinator process stores the SCCs received from the workers. It then checks each combination of such markings: if it labels an arc in the synchronisation graph, the corresponding fused transition is enabled and the marking is not a deadlock. Otherwise, if the marking is effectively reachable, then it is a deadlock. 4.3
Liveness To verify whether a transition t is live or not, two cases are distinguished: if t is a fused transition (t ∈ TF ), or t is an internal transition. The verification is based on the following proposition.
Proposition 2 (Liveness). 1. A transition tf ∈ TF is live ⇔
[∀scc ∈ Term(SCCSG) : tf ∈ Trans(scc)] ∧ [∀v ∈ VSG : ∀M ∈ [[vi :(∀s ∈ S : Msc ∈ Term(SCCs))
⇒ ∃(v, (M1, tf 0), v2) ∈ ASG : M1 ∈ [[M i]. 2. A transition t ∈ Ts is live ⇔
[∀scc ∈ Term(SCCSG) : ∃v ∈ scc : t ∈ Trans([vsis)] ∧ [∀v ∈ VSG : ∀M ∈ [[vi : (Msc ∈ Term(SCCs))
⇒ (t ∈ T rans(Msc) ∨ ∃(v, (M1, tf ), v2) ∈ ASG : M1 ∈ [[M i))].
To check if a fused transition tf is live, the coordinator checks if there exists a terminal SCC in the synchronisation graph which does not contain transition tf , in which case transition tf is not live. Otherwise, for each node v ∈ VSG of the synchronisation graph, the coordinator sends vs to the worker process s and waits to receive the terminal SCCs reachable from vs in module s. Then, it checks whether the combinations of the terminal SCCs label fused transitions are in SG, considering only the modules participating in the synchronisation of this fused transition. If this is not the case, tf is not live.
When transition t is an internal transition of module s, the worker process s detects the terminal SCCs which do not enable t, that may invalidate liveness. For each node v ∈ VSG of the synchronisation graph, the coordinator sends vs to the worker process s. The worker processes check whether these problematic SCCs are reachable from vs, and send them to the coordinator. The coordinator checks if there exists a combination that does not label a fused transition, in which case transition t is not live. The verification of whether a reachable state MH is a home state or not is based on the following proposition.
Proposition 3 (Home state).
A state MH ∈ [M0i is a home state ⇔
[∀scc ∈ Term(SCCSG) : ∃v ∈ scc : MH ∈ [[vi] ∧ [∀v ∈ VSG : ∀M ∈ [[vi : (∀s ∈ S : Msc ∈ Term(SCCs))
⇒ MH ∈ [[M i ∨ ∃(v, (M1, tf , M2), v2) ∈ ASG : M1 ∈ [[M i].
To check such a property, we first check whether the state MH is reachable from all nodes of the synchronisation graph. Then, for every node v of the synchronisation graph, the coordinator asks the worker processes for the terminal SCCs reachable from v by firing internal transitions only. The coordinator checks then that all combinations label an arc, or correspond to the SCC containing MH . Otherwise MH is not a home state. 5
Implementation and experiments The previous algorithms were implemented within a prototype tool. The tests were carried on a cluster composed of 12 stations (Pentium IV with 512 Mbytes of memory), one of them is assigned to the coordinator process while the others run the worker processes.
In this section, we give the results obtained for the dining philosophers problem and Automated Guided Vehicles (AGV) problem, and draw conclusions. 5.1
The dining philosophers problem The distributed generation based on partitioning the state space over a cluster of stations, allows for handling large size problems. In [BP07], the philosophers problem was handled with various sizes (see Table 1). But this approach is still limited. The total number of exchanged messages is very high, due to the amount of cross arcs.
In the distributed modular based approach, the original Petri net is split into a Modular Petri net with N modules and each module, which can contain m philosophers, is assigned to a worker process. Philosopher i of module l shares its forks with the philosophers i − 1 and i + 1 of the same module for 2 ≤ i ≤ m − 1. Philosophers 1 in module l and m in module (l − 1) mod N + 1 also share a fork.
The nature of the Petri net gives 4 SCCs in each module graph. The synchronisation graph size is 2N nodes and N.2N arcs. For a problem with 100 philosophers, if we consider 10 modules with 10 philosophers each, we obtain 1,024 nodes and 10,240 arcs in the synchronisation graph, 233 nodes and 1,132 arcs in each local graph. The reachability graph size for the original problem is greater than 7 × 1020 nodes and 7 × 1022 arcs.
In Table 2, we give the modular state space sizes for the philosophers problem considering 10 philosophers per module each time. The average of CPU times of the coordinator is also given.
The CPU time of the workers is generally equal to 0.04 s (for 10 philosophers per module). Thus, in the first cases the global CPU time corresponds to the local state space generation, the synchronisation graph generation CPU time is less then 0.01 s. In the last cases the synchronisation graph generation spends more time since its size became larger.
Various tests were performed for reachability, liveness and home state properties, with the philosophers problem of 10 modules with 10 philosophers in each one, the experimental results are given in the table 3.
For reachability, we considered three cases: in the first, the marking is not reachable in some modules; in the second, the marking is reachable in the modules but not reachable as a global marking; and in the third case, the marking is reachable. The number of exchanged messages is the same and correspond to messages sent by the coordinator to the worker processes to transmit the marking to check (10 messages) and to the answers of the workers (10 messages). The liveness and home state verifications are performed with a relatively large number of exchanged messages: since all transitions are live, the coordinator must obtain the terminal SCCs reachable from each node of the synchronisation graph. When the coordinator moves from a node to its successor in the synchronisation graph, it transmits messages only to the workers corresponding to the changed components to have their terminal SCCs. This allows for minimising the number of messages transmitted by the coordinator.
Automated Guided Vehicles The Automated Guided Vehicles (AGVs) problem has been solved by means of Modular State Spaces in [LP04]. The problem is that of a factory floor which consists of three workstations which operate on parts, two input and one output stations, and five AGVs which move parts from one station to another.
The 5 AGVs example is loosely coupled. Therefore, much interleaving is avoided when building the modular state space and this leads to very good results. This model has 30,965,760 states (see [LP04]). However, with modular analysis we obtain only 900 states with 2,687 arcs. The analysis based on modular distribution gives also good results as shown in table 4.
CPU Time (sec) Mess Nb In this paper, we proposed steps towards distributed modular analysis of Petri net models, based on the construction framework of [LP04]. Using these algorithms, it is possible to verify standard Petri nets properties, such as reachability, deadlocks, home states and liveness, in a distributed manner.
The main advantage of such an approach is the possibility to consider very large systems with several modules, sharing transitions, and assign them among a set of machines, thus limiting the drawbacks of the state space explosion problem.
Each machine (process) generates only the state space of the module it is assigned. The synchronisation graph provides the global knowledge of the behaviour of the system.
Moreover, it is also possible to check properties using the distributed modular state space directly, i.e. without unfolding to the ordinary state space. When designing algorithms there is often a trade-off between time and space complexity. For state space analysis it is attractive to have a rather fast way to decide properties, but the state space explosion problem makes it absolutely necessary to minimise memory usage.
Experiments were performed on a cluster of 12 stations. Both the AGVs, and the philosophers problems were considered, with different sizes. The results obtained for the generation of the modular state space were very interesting and allow for checking properties of very large systems. Future work will extend properties verification to temporal logic properties. Further experiments on larger case studies are also necessary for a better assessment of the benefits of this approach. Proceedings of CompoNet and SUMo 2011
80 When Graffiti Brings Order?
Alban Linard and Didier Buchs Université de Genève, Centre Universitaire d’Informatique
7 route de Drize, 1227 Carouge, Suisse Abstract. Most researchers use Petri nets as a formal notation with mathematically defined semantics. Their graphical part is usually only seen as a notation, that does not carry semantics.
Contrary to this tradition, we show in this article that, when created by a human, there is inherent semantics in the positions of places, transitions and arcs. We propose to use the full definition of Petri nets: whereas they have been deteriorated to their mathematically defined part only, their graphical information should be considered in their definition. 1 Graphical information of Petri nets usually does not appear in their formal definitions. For instance, Figure 1 presents the traditional graphical Petri net representation of two dining philosophers, a textual, and a mathematical representation of the same Petri net. In research, we almost always consider them as equivalent. The graphical representation is used by the modeler, or for figures in articles, the textual representation is an example of input format for a tool, and the mathematical representation is used for scientific publications.
Are all these representations really equivalent? When we ask researchers in
Petri nets, they often believe it. But their equivalence is only an assumption,
it might thus be false. Why do people strive to maintain layouts in the model
transformation field, for instance in [
Dialogue 1: Question of Placehopper
Throughout this article, we propose to investigate the problem raised by Master Transition, by extracting semantics from the graphical part of Petri ?Thanks to Matteo Risoldi for proposing this title. Left0
Right0 Think0 Eat0 Eat1
Think1 Fork0
Right1
Left1
Places
Think0, Think1 = 1 Fork0 , Fork1 = 1 Left0, Right0, Eat0 = 0
Left1, Right1, Eat1 = 0 Transitions
Think0 + Fork0 ! Left0
Think0 + Fork1 ! Right0 Fork1 Left0 + Fork1 ! Eat0
Right0 + Fork0 ! Eat0 Eat0 ! Fork0 + Fork1 + Think0 Think1 + Fork1 ! Left1 Think1 + Fork0 ! Right1 Left1 + Fork0 ! Eat1 Right1 + Fork1 ! Eat1
Eat1 ! Fork0 + Fork1 + Think1 PN = hP;TAi
P = (Think0;Left0;Right0;Eat0;Fork0)
Think1;Left1;Right1;Eat1;Fork1 T = (r0;s0;t0;u0;v0) r1;s1;t1;u1;v1 kT L0 tghR0 taE0 rkoF0 ikhnT1 fteL1 itghR1 taE1 rkoF1 0 ihn fte i kT L0 tghR0 taE0 rkoF0 ikhnT1 fteL1 itghR1 taE1 rkoF1 0 ihn fte i Fig.1: Graphical, textual and mathematical representations of a Petri net nets. This semantics is unclear, as it depends on the modeler and the model. Thus, we check that the extracted semantics can be useful to improve model checking performance of the Petri nets.
Section 2 presents the methodology of this work: how semantics extracted from the graphical information is used to improve model checking performance. Then we propose to use alignments of places and transitions in Section 3. As this only information is not always sufficient to improve model checking performance, we also propose to use graphical distances in Section 3. Then we propose in Section 4 to use surfaces delimited by arcs, for models with no alignments. The approach is generalized to colored Petri nets in Section 5. As we cannot give semantics to graphical information of all models, two counter-examples are provided in Section 6. Section 7 discusses about when and how graphical information can be used, before conclusion in Section 8. 2
How do we assess the quality of semantics extracted
from graphical information?
The Software Modeling and Verification Group has developed the Algebraic
Petri Net Analyzer (AlPiNA) [
By default, AlPiNA has rather good computation times [
Clusters c0 , c1 ; Rules c l u s t e r o f in Think0 , Left0 , Right0 , Fork0 , Eat0 i s c0 ; c l u s t e r o f in Think1 , Left1 , Right1 , Fork1 , Eat1 i s c1 ; c0 < c1 ;
Listing 1: Example of clustering
Several articles already give heuristics to infer variable orders from Petri
nets [
In this article, we propose to use the graphical information of Petri nets to define the clustering, together with ordering of the variables in the clusters. We try to group together tokens and places that belong to the same process.
To assess the inferred clustering, we check if it improves the model checker
performances. Instead of using AlPiNA, we use PNXDD [
All the examples in this article are taken from the Model Checking Contest of the SUMo 2011 workshop. Choosing models that were not created by our group allows us to avoid a possible bias that may be introduced if we had too much knowledge about the models.
For each model, we compare the efficiency of our graphical clustering and ordering with fully random ones (500 random clusterings and orderings for each clustering proposed in this article). This benchmark shows the experimental probability of obtaining clustering and ordering with the same efficiency. Then we compare our graphical clustering and ordering with all the algorithms implemented in PNXDD. It shows how we perform against several existing algorithms.
The results are not intended to show that our approach is more efficient
than other ordering algorithms, for instance those used by [
We provide a VirtualBox image of the tools and scripts used in the benchmarks at http://smv.unige.ch/members/dr-alban-linard/ sumo2011-when-graffiti-brings-order-image (use login/pass: sumo2011 for the Linux session). 3
Using alignment of places and transitions We start the exploration of usual graphical semantics in Petri nets with the Flexible Manufacturing System (FMS) model. It is a Place/Transition Petri net represented in Figure 2. Initial marking is not shown as it is irrelevant in our approach. Note that this model is parameterized by its initial marking. The full model is presented in the SUMo 2011 workshop.
Even with absolutely no knowledge of the modeled system, it is obvious that the PN has vertically aligned places and transitions, linked by arcs in the alignment. Alignment, either vertical or horizontal, is one usual way for the modelers to show graphically the processes. Figure 2a shows the four vertical (a) Aligned places and transitions (b) With places added to nearest group
Fig. 2: Flexible Manufacturing System alignments of places and transitions, and one horizontal alignment. Thus, maximal non-overlapping chains of consecutive and aligned places and transitions define groups. All the places of each group can be put in a same cluster. From this example, we can state Assumption 1: Assumption 1 Aligned places and transitions may correspond to a process. 3.2 Alignment with graphical distance
After applying Assumption 1, some places do not belong to any group. Usually, the modelers use them either to represent shared data or for local data. In Figure 2a, the horizontal alignment shows a shared data. The remaining marked places are each near the middle of a cluster, and thus are likely to represent local data. On the contrary, the remaining unmarked places are found at the extremity of the clusters, and thus they can either represent the processes or local data. So, after defining the groups, we extend them using Assumption 2: Assumption 2 Local data of a process is more likely to be near its process.
Figure 2b shows the result of application of Assumption 2 to the groups of Figure 2a. Each place is added to the nearest group it is related to, where nearest means graphical distance. For instance, the unmarked places are added to the vertical groups instead of the horizontal one, because they are linked to transitions aligned with the vertical clusters.
We also define ordering of the places inside the clusters and ordering of the clusters. Inside each cluster, the places are ordered from top to bottom or from left to right. The local data places are put randomly before or after the nearest process place. To order the clusters, we also chose graphical distance. In the FMS model, and are next to each other. is far from all other clusters, but its nearest neighbor is . As is between and , we get the following order for the clusters: < < < <
The results of the benchmarks for the FMS 50, i.e., with initial marking
parameter set to 50. All random clusters and orders were too slow, and thus could
not finish computation. Graphical clustering and ordering gives better results
than all algorithms implemented in PNXDD. We give only the number of the
algorithm, instead of its name, for a concise diagram. The corresponding algorithm
names are found in [
For the human eye, the kanban model is composed of four components, each one with four places. All components have rather similar shapes. They differ by some arcs and also by a symmetry. Detecting these small differences is not a trivial task.
The components are visible because the arcs draw the shapes of the components. For instance, the modeler used arcs with two inflexion points where he could have drawn a direct arc. From this example, we can deduce Assumption 3: Assumption 3 Arcs may draw shapes, the surface of which may contain related places.
We investigate different ways to use the shapes. First, Figure 3a identifies three different components in the model. Each one is found by searching maximal surfaces in the graphical Petri net. When two surfaces are linked by a place, they are merged, as one place can only belong to one cluster.
The maximal surfaces approach can lead to huge clusters. The worst case is when the whole Petri net is enclosed by arcs, and thus all its places are in the same cluster. We thus propose a second way to search surfaces. Instead of identifying maximal surfaces, we can use minimal surfaces. They are defined (a) Maximal surfaces (b) Minimal surfaces (c) Minimal connected surfaces with nearest remaining places
Fig. 3: Kanban System as the surfaces that do not enclose another surface. Figures 3b and 3c show the Kanban model with minimal surfaces. In Figure 3b, the choice of minimal surfaces to consider leads to four clusters, whereas in Figure 3c another choice leads to three clusters. As the surfaces that touch the same place must be merged, we have to choose either Figure 3b or Figure 3c. Otherwise, the three surfaces in the middle block are merged, and the clustering is equivalent to the one of Figure 3a.
We compare Figure 3a and Figure 3b in the benchmarks. Places are ordered inside the clusters by following the boundaries of minimal surfaces. Clusters are ordered by graphical proximity, giving the clusters below: < <
< < < (Figure 3a) (Figure 3b)
The results of the benchmarks for the Kanban model are given below. All random clusters and orders were again too slow, and thus could not finish computation. The same applies to some algorithms of PNXDD (1,2,6,12,21). Whereas graphical clustering shows a small improvement over existing algorithms for the FMS model, it gives here huge improvements over algorithms in PNXDD.
Extension to colored Petri nets The Shared Memory model of the SUMo 2011 workshop is given in Figure 4. It is a Symmetric Petri net, which is a particular kind of colored Petri net. Of course, our approach can be extended to the unfolded Place/Transition Petri net equivalent to a colored Petri net, when this equivalence exists. But the unfolding must then generate positions (possibly in three or more dimensions) to avoid superposition of unfolded places and transitions.
Without unfolding, we can still in some cases use graphical information to define clusters. Clusters for colored Petri nets are groups of unfolded places, i.e., places together with colors. Two policies can coexist: – Grouping in the same cluster all colors for one place, – Distributing in its own cluster each color for one place.
The first policy works usually well for places representing shared data, whereas the second one leads usually to good results for places representing processes or data local to a process. Assumptions 4 and 5 describe these two policies. Assumption 4 One place related to other places using different variables may represent a shared data.
Assumption 5 Several places related to each other using the same variable, or equal ones, may represent a process.
In the Shared Memory model, both Assumption 1 and Assumption 3 can be applied, as we find both aligned places and transitions and surfaces. 5.1 Using surfaces
To consider surfaces, we use Assumption 3. Its clustering is given in Figure 4a. We divided the model in four minimal surfaces. As there are places common to several surfaces, we obtain two groups. All places (a; b; c; e) in the group have the same domain, except one (e) that is not colored (shown using ). We create one cluster for each color 1 , 2 , 3 , or 4 , as shown in Listing 2. Place e can only belong to one cluster, as its domain is the black token . Thus, we also create its own separate cluster.
Clusters c , c1 , c2 , c3 , c4 ; Rules c l u s t e r o f in e i s c ; c l u s t e r o f 1 in a; b; c i s c1 ; c l u s t e r o f 2 in a; b; c i s c2 ; c l u s t e r o f 3 in a; b; c i s c3 ; c l u s t e r o f 4 in a; b; c i s c4 ;
Listing 2: Clustering using surfaces for places a; b; c; e
The group contains two places: d and f . Place f has domain f 1 ; 2 ; 3 ; 4 g, whereas the domain of the place d is a couple of colors. For each color, we create one cluster. Listing 3 completes Listing 2 with the new clusters. (a) Minimal surfaces and Identity, with nearest Identity y y x c x x 6= m x; m
x; y c x x x 6= m x; m
x; y m m m m m m x x 1 2 3 4 1 2 3 4 f d e f d e (b) Alignment and Identity, with nearest Identity
Fig. 4: Shared Memory Each token in place f is put in the cluster of its color. In place d, each token is a couple of colors. We have to choose which component of the couple predominates. Here, there is no obvious choice, so we choose the first element. Thus all tokens in place d are put in the cluster of the color of the first component.
Clusters d1 , d2 , d3 , d4 ; Rules c l u s t e r of 1 in f i s d1 ; c l u s t e r of 2 in f i s d2 ; c l u s t e r of 3 in f i s d3 ; c l u s t e r of 4 in f i s d4 ; c l u s t e r of f 1 g f 1 , 2 , 3 , 4 g in d i s d1 ; c l u s t e r of f 2 g f 1 , 2 , 3 , 4 g in d i s d2 ; c l u s t e r of f 3 g f 1 , 2 , 3 , 4 g in d i s d3 ; c l u s t e r of f 4 g f 1 , 2 , 3 , 4 g in d i s d4 ; c < c1 < d1 < c2 < d2 < c3 < d3 < c4 < d4 ;
Listing 3: Clustering using surfaces for places d; f 5.2
Using alignments
Using Assumption 1 gives a totally different result. It is shown in Figure 4b. Listing 4 shows the clustering obtained using Assumption 1.
We first identify aligned places and transitions: places b; c; d belong to one group. Places b and c have the same colored domain, whereas the tokens of place d are couples of colors.
We then try to add to the group what seems local data or part of the processes. All places a; f; e are near the group. Place a is linked to the group using only variable x. This clearly shows that an identity is passed along the arcs. So, this place is added to the group.
Place e contains black tokens. Because of this domain, it cannot be added in the clusters of colors, so we create its own cluster, as in Listing 2.
The last place is f . The variables that relate this place to d are used in the second part of the couple, whereas the variables that relate d to the places in its group are in the first part. So, f probably represents a shared data. We thus put place f in its own cluster, for all colors.
Clusters c , c1 , c2 , c3 , c4 , f; Rules c l u s t e r of in e i s c; c l u s t e r of 1 in a; b; c i s c1 ; c l u s t e r of 2 in a; b; c i s c2 ; c l u s t e r of 3 in a; b; c i s c3 ; c l u s t e r of 4 in a; b; c i s c4 ; c l u s t e r of 1 in f i s f; c l u s t e r of 2 in f i s f; c l u s t e r of 3 in f i s f; c l u s t e r of 4 in f i s f; c l u s t e r of f 1 g f 1 , 2 , 3 , 4 g in d i s c1 ; c l u s t e r of f 2 g f 1 , 2 , 3 , 4 g in d i s c2 ; c l u s t e r of f 3 g f 1 , 2 , 3 , 4 g in d i s c3 ; c l u s t e r of f 4 g f 1 , 2 , 3 , 4 g in d i s c4 ; c < c1 < c2 < c3 < c4 < f;
Listing 4: Clustering using alignment
Figure 4b shows the result of this analysis. Note that for each color 1 , 2 , 3 , or 4 , we create a cluster that contains all the highlighted places for this color only. For place d, each cluster contains all possible colors for the second part of the Cartesian product.
We compare both clusterings below. For this third model, the state space generation could not finish using some algorithms of PNXDD (2,12,21). Graphical clustering and ordering is still better than all algorithms implemented in PNXDD. As for other models, none of the random clusterings could finish. il()rca4gaphb il()rcga4aaph )(6xnpdd ()1xpndd ,()811xpndd )(13xpndd random pnxdd(2,12,21) 0 state space generation time (linear scale)
When we fail at understanding the model The Model Checking Contest of SUMo 2011 workshop uses seven models, three of which are Place/Transition Petri nets and the four others Symmetric Petri nets. In this article, we provide clustering for Flexible Manufacturing System, Kanban and Shared Memory. Two models are not discussed: Philosophers and Token Ring. The Philosophers model has been studied a lot for use with Decision Diagrams. Before writing this article, we already knew that the best order is when each philosopher and its left (or right) fork is put in its own cluster. Because of this knowledge, trying to find graphical information would be biased. The Token Ring model does not contain enough places (1) and transitions (2).
The two remaining models are MAPK (Figure 5) and Peterson’s algorithm (Figure 6). For them, we did not find how to give semantics to the graphical information. Note that these two models are considered as hard to understand by humans. This might be an explanation: because their modelers could not find a good disposition of places and transitions, we cannot give semantics to graphical information, and thus the models are hard to understand. 7
Discussion on the approach We propose in this article to extract semantics from the graphical part of a Petri net. It works on some models, but does not work on some others. Moreover, all people do not always agree on how to identify the processes in the Petri net. This approach is thus fragile. We provide in this section some remarks on its applicability, and on other techniques that could be used along graphical information to improve clustering.
This approach depends on the school of modeling.
Depending on where we have studied, and where we work, we may not create models in the same way. The most obvious difference is putting aligned processes horizontally or vertically. But some people can also prefer to show processes using surfaces instead of alignments. We should investigate which representations are used, and where they are modeled.
A side effect is that every Petri net should define an author and the
institutes where the author has studied and workse Using this information, giving
semantics to graphical information could be enhanced. The “author” field is
already present in the Petri Net Markup Language [
Graphical information cannot be processed easily
The Petri Net Markup Language handles absolute positions for the Petri net
elements (places, transitions, labels. . . ). The problem with absolute positioning
is that analysis of the graphical information is not easy. Some other positioning
schemes exist. For instance, TikZ [
Labels can also be used to detect components.
We use only graphical information on Place/Transition Petri nets in this article. For Symmetric Petri nets, we also use domains and variables on the arcs. Another interesting information to compute clustering is the labels of places and transitions. In Place/Transition Petri nets, they are often composed of a textual prefix, a textual suffix, and some numbers in the middle. These numbers correspond to colors in an equivalent colored Petri nets. Extracting the naming patterns of places can greatly enhance the clustering.
This approach may be redundant with graph analysis.
Ordering the Decision Diagrams used during the model checking of a Petri
net has been explored for a long time. We can cite again [
Instead of using the graphical information, they are usually based on the graph structure of the Petri net. These techniques, from the structural analysis field, can lead to very good results. Note that combining them with graphical information and naming analysis is often possible.
First, traps and siphons [
We extract semantics from several kinds of graphical information: the alignment of places and transition, the graphical proximity of places and groups, and the surfaces delimited by arcs. This semantics is used to define clustering and ordering of the places and tokens.
For all these examples, we use the graphical information to improve symbolic model checking of the Petri net. To do so, we extract clustering and ordering from the graphical part of each model. Using them, we compare the time taken to generate the state space with several clustering and ordering algorithms implemented in PNXDD, and with fully random clusters and orders. In all models where graphical clustering could be defined, we obtain improvements over PNXDD. No random clusters and orders could run in the time and memory limits, which shows that the semantics extracted from graphical information makes sense.
At the beginning of this work, we were only hoping to obtain improvements over some of the algorithms in PNXDD. Prior the benchmarks, we did no selection of the models, and of the inferred graphical semantics. Thus, the good results seem promising.
From these examples, two conclusions arise: (1) in education, Petri nets are always introduced as a graphical formalism. In research, they have been deteriorated into a mathematical only formalism, by losing graphical information; (2) graphical information in Petri nets has semantics, but unclear one.
We believe that, contrary to their usual presentation in scientific publications, Petri nets are truly a graphical formalism, and their mathematical representation is only a projection.
Further work should identify more graphical semantics, and the cases in which they apply. We may not be able to create algorithms to extract always semantics from graphical information. But when it is possible, a study with fully automatic algorithms should check that the inferred semantics can be used with no user knowledge of the models.
References
K 9 K ER 1k R 1
E 2
k 6 3 e s a 6 h P
P K R E 8 2 k P P K E M 6 1 k 2 e s 3 a 1 h k P 4
K 5 2 R 6 k E 2
k K 0 R 3
k E 3 e s a h P _ P P 3 e s a h P _ P P P K E M _
4 2 1 se k a h P _ P P K E M 2 e 7 M 8 1 k 7 2 k 9 2 k 0 2 k 5 1 k 2 2 k 4 2 k
P P K R E
P P K E M _ P K R E 3 2 k P f 9 a k R _
K 7 E k M
P K E 0
1 M k 8 k 1 e s a 6 h P 4
k P 1
k T sG 2 a 2 1 k 1 1 k P f a R 1 e s a h P _ P f a R T G s a
P f a R _ P K E M 6 k f a 2 R k R _ 3 fa k R e d a k s a k e s a n i k n i e t o r p d e t a v i t c a n e g o t i g i
F CLASS Process is 0..N; Tour is 0..N-1; Bool is [T, F]; DOMAIN ProcTour is <Process, Tour>; TourProc is <Tour, Process>; ProcTourProc is <Process, Tour, Process>; ProcBool is <Process, Bool>; VAR i in Process; k in Process; j in Tour; WantSection <Process.all, F>
ProcBool <i, T>
<i, F> <i, j>
<i, j, k> ContinueLoop <i, 0>
Process Ask <i, j> UpdateTurn <i, j>
TestTurn
ProcTour <j, i> <j, i> <j, i> <j, k>
Turn TourProc <Tour.all, 0> TurnDiff
<i, j> [i<>k]
<i, j> <i, j> ProgressTurn
AccessCS CS
Process
EndLoop <Process.all> AskForSection ProcTour
<i, j> <i, j, 0> TurnEqual
BeginLoop ProcTourProc <i, j , i> Identity
<i, j , i> <i, j ,k> <i, j, k++1> <i, j, k> <i, j++1>
<i, j> Loop [k <> N] <i, j, N> <i, T>
<i, F>
Fig. 6: Peterson’s algorithm Author Index
B D F K L P R T
Bashkin, Vladimir A.
Berard, Beatrice Ben Salem, Ala Eddine Boukala, Mohand Cherif Buchs, Didier Duret-Lutz, Alexandre Fronc, Lukasz Kordon, Fabrice Lime, Didier Linard, Alban Petrucci, Laure Pommereau, Franck Roux, Olivier H.
Thierry-Mieg, Yann 33 17 65 1 81 1 49