Proceedings of CompoNet and SUMo 2011 Distributed Verification of Modular Systems M.C. Boukala1 and L. Petrucci2 1 LSI, Computer Science department, USTHB BP 32 El-Alia Algiers, ALGERIA boukala@lsi-usthb.dz 2 LIPN, CNRS UMR 7030, Université Paris XIII 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 in- dustrial 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, symme- tries, 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 modu- lar analysis to perform verification of basic behavioural properties such as reachability, deadlock states, liveness, and home states and their dis- tributed analysis for modular systems. Each module is assigned to a process which explores independently the internal activity of the mod- ule, 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 reach- ability 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. 1 Proceedings of CompoNet and SUMo 2011 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 mea- sure, and discards states that will not be encountered further in the construc- tion; modular verification [LP04]; partial order reductions [Val92,NG97]; sym- metries [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 be- haviour of each subsystem, and then separately considers the synchronisation between the subsystems. In this fashion, exploring the many possible interleav- ings of activity of the subsystems is avoided, thus reducing the state space. In this work, we propose to combine modular analysis and distributed pro- cessing 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 algo- rithms 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 dis- joint: ∀s1 , s2 ∈ S : [s1 6= s2 ⇒ (Ps1 ∪ Ts1 ) ∩ (Ps2 ∪ Ts2 ) = ∅]. 2 Proceedings of CompoNet and SUMo 2011 S S – P = Ps and T = 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. S In the following, TF also denotes tf ∈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 syn- chronised with different transitions (a sub-action of several more complex ac- tions). 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 : P P W (p, tg) = W (p, t), W (tg, p) = W (t, p). t∈tg 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 en- abled 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). Figure 1 depicts a modular Petri net consisting of three modules A, B and C. Modules A and B both contain transitions labelled F1 and F3 , while modules B and C both contain transition F2 . These matched transitions are assumed to form three transitions fusion sets. 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 A1 B1 C1 , 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 A2 B2 C1 . 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 v c to denote the component to which v belongs. 3 Proceedings of CompoNet and SUMo 2011 A1 B1 C1 F1 F1 F2 tB A2 B2 C2 F3 F2 tA A3 B3 F3 Fig. 1: A modular Petri net with 3 modules 2.2 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: Y ∀M ∈ [M0 i : M c = Msc . 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 , S As ) is the local state space of module s: (a) Vs = [vis v∈VSG 4 Proceedings of CompoNet and SUMo 2011 A1 B1 C1 F1 A2 B2 C1 tB F2 tA A2 B3 C2 A3 B2 C1 tB tA F3 F2 A3 B3 C2 Fig. 2: The state space of the modular net of figure 1 (b) As = {(M1 , t, M2 ) ∈ Vs × (T \ TF )s × Vs | M1 [tiM2 } 2. SG = (VSG , ASG ) is the synchronisation graph of MN : (a) VSG = [[M0 iic ∪ M0 0 c 0 (b) ASG = {(M1 , (M1 , tf ), M2c ) ∈ VSG × ([M0 ic × TF ) × VSG | M1 ∈ [[M1 i ∧ c c 0 M1 [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 repre- sentative 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. 5 Proceedings of CompoNet and SUMo 2011 The arcs of the synchronisation graph represent all occurrences of fused tran- sitions. 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 B1 C1 A1 B1 C1 A1 B1 C1 , F1 A2 B2 tB C2 A2 B2 C1 tA A2 B2 C1 , F2 A3 B3 A2 B3 C2 A3 B3 C2 , F3 Fig. 3: The modular state space of the net in figure 1 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 dis- tributed 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]. 6 Proceedings of CompoNet and SUMo 2011 The coordinator constructs the synchronisation graph, coordinates the differ- ent 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() 1 begin /* Process states in Waiting */ 2 while ¬EndOfGeneration do 3 while Waiting 6= ∅ do 4 Choose M ∈ Waiting s 5 forall the t 6∈ TF s.t. M [tiM 0 do /* t is an enabled internal transition */ 6 Add (M 0 ) 7 Arc (M, t, M 0 ) 8 UpdateSCC () 9 forall the tf ∈ TF s.t. M [tf i do /* M enables a fused transition tf */ 10 TFWaiting ← TFWaiting ∪ {(M, tf )}; 11 Waiting s ← Waiting s \ {M } 12 if TFWaiting = ∅ then 13 EndOfGeneration = true 14 else 15 while TFWaiting 6= ∅ do 16 Choose (M, tf ) ∈ TFWaiting s.t. M [tf iM 0 17 Waiting s ← Waiting s ∪ {M 0 } 18 TW .label = M c 19 TW .AncSCC = AncSCC (M ) 20 TW .tr = tf 21 TW .SuccSCC = M 0c 22 Send (Sender = s, Dest = Coordinator, Type = SynchTrans, 23 Content = TW ) 24 Send (Sender = s, Dest = Coordinator, Type = END_GENERATION) 25 end 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 7 Proceedings of CompoNet and SUMo 2011 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. Actu- ally, 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 algo- rithm 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 syn- chronisation 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 reachabil- ity 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 [M0 i. 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. 8 Proceedings of CompoNet and SUMo 2011 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 , · · · , vN c ) ∈ VSG do 7 foreach pm ∈ PM and pm 6= s do 8 Wpm = {w ∈ SGWaiting pm s.t. c 9 (w.AncSCC = vpm ) ∧ (w.tr = tf )} /* Wpm : markings enabling tf , with vpm as ancestor */ 10 foreach np 6∈ PM and np 6= s do 11 Wnp = {•} /* any marking of a non-participating module enables synchronisation */ 12 Ws = {Message.Content} 13 foreach C = (c1 , c2 , · · · , cN ) s.t. ∀i ∈ PM , ci ∈ Wi do c c c 14 v 0 = (v 0 1 , v 0 2 , · · · , v 0 N ) where: c c 15 ∀i ∈ PM , v 0 i = ci .SuccSCC and ∀i 6∈ PM , v 0 i = vic 0 16 Add (v ) 17 AddArc (v, (C , ft), v 0 ) 18 foreach pm ∈ PM do 19 Send (Sender = Coordinator, Dest = pm, Type = NEW_NODE, 0 20 Content = vpm ) 21 SGWaiting s = SGWaiting s ∪ Message.Content .. . 22 end 9 Proceedings of CompoNet and SUMo 2011 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 ∈ [M0 i 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 synchroni- sation 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]. 10 Proceedings of CompoNet and SUMo 2011 2. A transition t ∈ Ts is live ⇔ [∀scc ∈ Term(SCCSG ) : ∃v ∈ scc : t ∈ Trans([vs is )] ∧ [∀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. 4.4 Home States 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 ∈ [M0 i 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 syn- chronisation 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 prob- lem and Automated Guided Vehicles (AGV) problem, and draw conclusions. 11 Proceedings of CompoNet and SUMo 2011 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). Nb Philo Nb States Nb Trans Nb Cross. arcs Nb Mess. CPU Time (sec) 5 11 30 18 36 <0.01 10 123 680 242 494 <0.01 15 1,364 11,310 2,731 5477 0.06 20 15,127 167,240 30,236 60,493 2.52 25 167,761 2,318,400 315,718 631,587 32.58 30 1,728,813 28,686,031 3,572,821 7,156,116 7547.45 Table 1: Distributed generation based on partitioning the state space 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 syn- chronisation 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. Nb Philo Nodes N Arcs Mess Nb CPU Time (sec) CPU time (1 proc) 20 470 2162 26 0.04 0.08 40 948 4372 52 0.04 0.16 60 1462 6846 84 0.04 0.25 80 2120 10664 120 0.05 0.39 100 3354 21010 230 0.16 0.61 Table 2: Modular distributed generation 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 12 Proceedings of CompoNet and SUMo 2011 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 prop- erties, with the philosophers problem of 10 modules with 10 philosophers in each one, the experimental results are given in the table 3. Properties CPU Time (sec) Mess Nb Reachability1 < 0.01 20 Reachability2 0.03 20 Reachability3 0.02 20 Liveness (Internal tr) 0.17 4278 Liveness (F uzed tr) 0.15 4116 Home state 0.21 4432 Table 3: Distributed modular verification of properties of the philosophers example 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 mod- ules 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 mark- ing 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 synchro- nisation 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. 5.2 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 modu- lar 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. 13 Proceedings of CompoNet and SUMo 2011 CPU Time (sec) Mess Nb State Space Generation 0.02 82 Deadlocks search 0.03 11 Reachability1 < 0.01 22 Reachability2 0.02 22 Reachability3 0.02 22 Liveness (Internal tr) 0.09 3313 Liveness (F uzed tr) 0.08 3062 Home state 0.15 3415 Table 4: Distributed verification of properties for the 5 AGVs example 6 Conclusion In this paper, we proposed steps towards distributed modular analysis of Petri net models, based on the construction framework of [LP04]. Using these algo- rithms, 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 be- haviour of the system. Moreover, it is also possible to check properties using the distributed modu- lar 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 complex- ity. 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 ex- tend 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. References [AAC87] S. Aggarwal, R. Alonso, and C. Courcoubetis. Distributed reachability anal- ysis for protocol verification environments. In P. Varaiya and H. Kurzhan- ski, editors, Discrete Event Systems: Models and Application, volume 103 of LNCIS, pages 40–56. Springer-Verlag, 1987. 14 Proceedings of CompoNet and SUMo 2011 [AHI98] K. Ajami, S. Haddad, and J.-M. Ilié. Exploiting symmetry in linear temporal model checking: One step beyond. In Proc. 4th Int. Conf. Tools and Algo- rithms for the Construction and Analysis of Systems (TACAS’98), volume 1384 of Lecture Notes in Computer Science, pages 52–67, 1998. [BBS01] J. Barnat, L. Brim, and J. Strîbrnà. Distributed LTL model checking in SPIN. In Proc. 8th International SPIN workshop on Model Checking Software (SPIN’2001), volume 2057 of Lecture Notes in Computer Science, pages 200– 216. Springer-Verlag, 2001. [BO03] S. Blom and S. Orzan. Distributed state space minimization. Electronic Notes in Theoretical Computer Science, 80:1–15, 2003. [BP07] M.C. Boukala and L. Petrucci. Towards distributed verification of Petri nets properties. In British Computer Society eWIC, editor, In Proc. 1st Interna- tional Workshop on Verification and Evaluation of Computer and Communi- cation Systems (VECOS’07), Algiers, Algeria, pages 15–26, 2007. [CFJ93] E. M. Clarke, T. Filkorn, and S. Jha. Exploiting symmetry in temporal logic model checking. In Proc. 5th Int. Conf. Computer Aided Verification (CAV’93), volume 697 of Lecture Notes in Computer Science, pages 450–462. Springer-Verlag, 1993. [GMS01] H. Garavel, R. Mateescu, and I. Smarandache. Parallel state space construc- tion for model-checking. In Proc. 8th International SPIN workshop on Model Checking Software (SPIN’2001), volume 2057 of Lecture Notes in Computer Science, pages 217–234. Springer-Verlag, 2001. [KP04] L. Kristensen and L. Petrucci. An approach to distributed state exploration for coloured Petri nets. In Proc. 25th Int. Application and Theory of Petri Nets (ICATPN’2004), volume 3099 of Lecture Notes in Computer Science, pages 474–483. Springer-Verlag, 2004. [LP04] C. Lakos and L. Petrucci. Modular analysis of systems composed of semiau- tonomous subsystems. In In Proc. 4th Int. Conf. on Application of Concur- rency to System Design (ACSD’2004), Hamilton, Canada., pages 185–194. IEEE Computer Society Press, 2004. [LS99] F. Lerda and R. Sisto. Distributed-memory model checking with SPIN. In Proc. 5th and 6th International SPIN workshops on Model Checking Software (SPIN’1999), volume 1680 of Lecture Notes in Computer Science, pages 22– 39. Springer-Verlag, 1999. [NG97] R. Nalumasu and G. Gopalakrishnan. A new partial order reduction al- gorithm for concurrent systems. In Proc. Int. Conf. Hardware Description Languages and their Applications (CHDL’97). Chapman & Hall, 1997. [Sch04] K. Schmidt. Automated generation of a progress measure for the sweep-line method. In Proc. 10th Int. Conf. Tools and Algorithms for the Construc- tion and Analysis of Systems (TACAS’04), volume 2988 of Lecture Notes in Computer Science, pages 192–204. Springer-Verlag, 2004. [Val92] A. Valmari. A stubborn attack on state explosion. Formal Methods in Systems Design, 1(4):297–322, 1992. 15 Proceedings of CompoNet and SUMo 2011 16