1 XCCS diagram to CCS script Conversion Algorithm Krzysztof Balicki Interdisciplinary Centre for Computational Modelling University of Rzeszów Pigonia 1, 35 - 310 Rzeszów, Poland kbalicki@ur.edu.pl Abstract. The XCCS modelling language can be viewed as a tool supporting fast and faultless development of CCS scripts or as an independent process calculus based on CCS process algebra. Having in mind the first of possible applications, we present an algorithm that converts XCCS diagrams into CCS scripts. This algorithm takes into consideration the priority of actions in the XCCS diagram and aims to retain the maximum number of original action’s names for the sake of readability. 1 Introduction The XCCS (eXtended Calculus of Communicating Systems) modelling language was formally defined in the paper [1] as a graphical extension of the Milner CCS ([2], [3], [4], [5]) process calculus. It has has been developed to replace the algebraic coding of concurrent systems with graphical modelling. XCCS models consist of two layers, a graphical and an algebraic one. In the latter we use the subset of CCS process algebra called CSS (Calculus of Sequential Systems) to describe behaviour of individual agents. CSS scripts may only contain the prefix op- erator ".", the choice operator "+" and parentheses "( )". Moreover, in the timed version of the calculus, the strong choice operator "++" and the delay operator "$" are allowed. The composition, restriction and relabel operators have graphical representations and provide simple description of the modelled system structure [1], [6], [7]. In the paper [1] we introduced simple Basic Conversion Algorithm which is proper for plain XCCS modelling language. The new Universal Conversion Algorithm pre- sented here can be applied to both plain and full XCCS diagrams. Furthermore, it con- siders the priority of actions and aims to retain the maximum number of original action’s names for the sake of readability. First, we show Trivial Conversion Algorithm that does not perform any relabelling of actions yet works correctly for limited class of models. Then, we thoroughly examine and define the properties of those diagrams that cannot be translated by Trivial Conversion Algorithm. We take into account these properties while applying proper relabeling of actions in the new algorithm. 2 Preliminaries We recall XCCS modelling language by way of example. Let us consider a simple XCCS diagram. 1 2 B1 B2 A a c B b b A = a.'b.A; B = b.'c.B; Fig. 1. Example XCCS diagram The formal definition of the XCCS diagram in Fig. 1 is as follows: XCCS = (B, CA, CSS , CR, in, out, v, ρ), where: · B = {B1 , B2 } - agent blocks · CA = {a, b, c} - communication actions, labels · CSS = {A = a.b.A, B = b.c.B} - the set of CSS scripts CA · in : B → 2 - input ports assigment in(B1 ) = {a}, in(B2 ) = {b} - labels of input ports · out : B → 2CA - output ports assigment out(B1 ) = {b}, out(B2 ) = {c} - labels of output ports OutP = {(B1 , b), (B2 , c)} = {B1 .b, B2 .c} - output ports InP = {(B1 , a), (B2 , b)} = {B1 .a, B2 .b} - input ports · CR ⊆ OutP × InP - communication relation CR = {((B1 , b), (B2 , b))} = {B1 .b → B2 .b} - connected ports · ϑ : OutP ∪ InP = P → {v, i} - visibility function ϑ(B1 .a) = ϑ(B2 .c) = v - visible ports ϑ(B1 .b) = ϑ(B2 .b) = i - invisible ports · ρ : B → CSS , ρ(B1 ) = A, ρ(B2 ) = B - assigment of CSS scripts The above XCCS diagram can be converted to the following CCS script by the Trivial Conversion Algorithm that does not perform any relabelling of actions. E = (B1 |B2 )\{b} B1 = a.b.B1 B2 = b.c.B2 Please note that the symbols ’b on the diagram and b in the script denote the same co-action with the name b. We will use the following notations and definitions: A(CSS i ) is the set of all actions of the CSSi script, e.g. A(B) = {b} A(CSS i ) is the set of all co-actions of the CSSi script, e.g. A(B) = {c} K(CSSi ) is the set of all agent constants of the CSSi script, e.g. K(B ) = {B} 2 3 Definition 1. We define the synchronization relation SR as follows: a) Let CR be a communication relation. For any port p ∈ P we define the set: CR(p) = {x ∈ P : (x, p) ∈ CR ∨ (p, x) ∈ CR}. (1) If p ∈ OutP , then the set CR(p) contains all input ports connected with the port p. If p ∈ InP , then the set CR(p) contains all output ports connected with the port p. b) We define a mapping:  P {p} if CR(p) = ∅ SR : P → 2 , SR(p) = S (2) CR(p) ∪ x∈CR(p) CR(x) if CR(p) 6= ∅ c) The synchronization relation SR is set by SR mapping: def (p1 , p2 ) ∈ SR ⊆ P × P ⇐⇒ SR(p1 ) = SR(p2 ). (3) If an equivalence class contains only one port then this port is isolated and does not communicate with any other port. If an equivalence class contains more then one port then any two complementary ports belonging to the equivalence class are connected one with the other. For the XCCS diagram in Fig.1 the equivalence classes of SR relation are P /∼ = {{B1 .a}, {B1 .b, B2 .b}, {B2 .c}}. We will use the following symbols: V = {p ∈ P : ϑ(p) = v} - the set of all visible ports I = {p ∈ P : ϑ(p) = i} - the set of all invisible ports Iso = {p ∈ P : CR(p) = ∅} - the set of all isolated ports Int(Bi ) = {a : a ∈ A(ρ(Bi )) ∧ Bi .a ∈ / InP } - the set of all inner actions of block Bi Int(Bi ) = {a : a ∈ A(ρ(Bi )) ∧ Bi .a ∈ / OutP } - the set of all inner co-actions of block Bi [ Int = Int(Bi ) - the set of all inner actions of the diagram Bi ∈B [ Int = Int(Bi ) - the set of all inner co-actions of the diagram Bi ∈B 3 Conflicts and Shadows We require that the resulting CCS script for a given XCCS diagram is in a Standard Concurrent Form and preserves properties of the diagram, that means: 1. Synchronization may occur only between those pairs of actions and co-actions which correspond to the labels of the ports connected on the diagram. 2. Actions and co-actions which correspond to inner actions are executable. 3. Actions and co-actions which correspond to visible isolated ports are executable. 4. Actions and co-actions which correspond to invisible isolated ports are not exe- cutable. 3 4 Now we roughly describe the Trivial Conversion Algorithm: 1. The names of CSS scripts become the same as names of corresponding blocks. 2. The ambiguities of names of the agent constants in CSS scripts are eliminated. 3. Output CCS script is a Standard Concurrent Form of all modified CSS scripts. 4. In the restriction set of the main equation of CCS script we place labels of all invisible ports. If we apply the Trivial Conversion Algorithm to a given XCCS diagram, then it can output a CCS script that does not satisfy requirements. We are able to precisely identify the properties of those XCCS diagrams for which the trivial algorithm does not produce a proper output. We call these properties conflicts and shadows. Shadows yield non executable actions. Conflicts entail unwanted synchronizations whereas expected synchronizations will not occur if the labels of connected ports have different names. Let us define the properties in question. Definition 2. We define the conflict of ports: a) We say that ports Bi .a ∈ OutP and Bj .a ∈ InP are in conflict, iff Bi 6= Bj ∧ (Bi .a → Bj .a) ∈ / CR. (4) We define the set of all conflicting output ports with the label a: k .OutP (a) = {Bi .a : ∃Bj .a ∈ InP : Bi 6= Bj ∧ (Bi .a → Bj .a) ∈ / CR} (5) We define the set of all conflicting input ports with the label a: k .InP (a) = {Bi .a : ∃Bj .a ∈ OutP : Bi 6= Bj ∧ (Bj .a → Bi .a) ∈ / CR} (6) Complementary ports are in conflict if they have the same labels and are placed on different blocks and are not connected. B1 B2 A = a.'b.c.'d.A; a d a d B = 'a.b.'c.d.B; A B b c b c Fig. 2. Conflicts of ports The conflicts of ports presented in Fig. 2 are as follows: i.B1 .a with v.B2 .a and v.B1 .b with i.B2 .b and i.B1 .c with i.B2 .c and v.B1 .d oraz v.B2 .d. The letters i and v indicate invisible and visible ports, respectively. Definition 3. We define conflicts of ports and inner actions as follows: a) We say that port Bi .a ∈ OutP and action a of the block Bj are in conflict, iff Bi 6= Bj ∧ a ∈ Int(Bj ). (7) 4 5 b) We say that port Bi .a ∈ InP and co-action a of the block Bj are in conflict, iff Bi 6= Bj ∧ a ∈ Int(Bj ). (8) The output port of a given block and the action of another block are in conflict if the label of the output port and the name of the inner action are the same. The input port of a given block and the co-action of another block are in conflict, if the label of the input port and the name of the inner co-action are the same. B1 B2 A B A = 'a.'b.A; a B = a.b.B; b Fig. 3. Port B1 .a and action a as well as port B2 .b and co-action b are in conflict Definition 4. The conflicts among inner action are defined as follows: a) The action a of the block Bi and co-action a of the block Bj are in conflict, iff: Bi 6= Bj ∧ a ∈ Int(Bi ) ∧ a ∈ Int(Bj ). (9) We define the set of all blocks for which the action a is conflicting: k .Int(a) = {Bi ∈ B : a ∈ Int(Bi ) ∧ a ∈ Int(Bj ) ∧ Bi 6= Bj } (10) We define the set of all blocks for which the co-action a is conflicting: k .Int(a) = {Bi ∈ B : a ∈ Int(Bi ) ∧ a ∈ Int(Bj ) ∧ Bi 6= Bj } (11) Inner action and co-action of different blocks are in conflict if they have the same names. B1 B2 A B A = 'a.b.A; a a B = a.'b.B; Fig. 4. Action b of the block B1 and co-action b of the block B2 are in conflict Definition 5. The shadows of ports are defined as follows: 5 6 a) We say that port Bi .a ∈ OutP shadows port Bj .a ∈ OutP , iff Bi 6= Bj ∧ ϑ(Bi .a) = i ∧ ϑ(Bj .a) = v (12) b) We say that port Bi .a ∈ InP shadows port Bj .a ∈ InP , iff Bi 6= Bj ∧ ϑ(Bi .a) = i ∧ ϑ(Bj .a) = v (13) c) We say that port Bi .a ∈ OutP shadows port Bi .a ∈ InP , iff ϑ(Bi .a) = i ∧ ϑ(Bi .a) = v (14) d) We say that port Bi .a ∈ InP shadows port Bi .a ∈ OutP , iff ϑ(Bi .a) = i ∧ ϑ(Bi .a) = v (15) The invisible port of the given block shadows the visible port of another block if both ports have the same label and are not complementary. The invisible port shadows the visible port on the same block if both have the same label and are complementary. B1 B2 A = 'a.b.a.A; a a a B = 'a.b.'b.B; A B b b b Fig. 5. The shadows of ports The shadows of ports presented in Fig. 5 are as follows: i.B1 .a shadows v.B2 .a and i.B2 .b shadows v.B1 .b and i.B1 .a shadows v.B1 .a and i.B2 .b shadows v.B2 .b. Definition 6. The shadows related to inner actions are defined as follows: a) We say that port Bi .a ∈ OutP shadows co-action a of the block Bj , iff Bi 6= Bj ∧ ϑ(Bi .a) = i ∧ a ∈ Int(Bj ). (16) b) We say that port Bi .a ∈ InP shadows action a of the block Bj , iff Bi 6= Bj ∧ ϑ(Bi .a) = i ∧ a ∈ Int(Bj ). (17) c) We say that port Bi .a ∈ OutP shadows action a of the block Bi , iff ϑ(Bi .a) = i ∧ a ∈ Int(Bi ). (18) d) We say that port Bi .a ∈ InP shadows co-action a of the block Bi , iff ϑ(Bi .a) = i ∧ a ∈ Int(Bi ). (19) 6 7 The invisible output port of a given block shadows an inner co-action of another block if this co-action has the same name as the label of that port. The invisible input port of a given block shadows an inner action of another block if this action has the same name as the label of that port. The invisible output port shadows his own inner action if this action has the same name as the label of the port. The invisible input port shadows his own inner co-action if this co-action has the same name as the label of the port. B1 B2 A B A = 'a.b.a.A; a B = 'a.b.'b.B; b Fig. 6. The shadows related to inner actions The shadows presented in Fig. 6 are as follows: i.B1 .a shadows co-action a of the block B2 and i.B2 .b shadows action b of the block B1 and i.B1 .a shadows action a of the block B1 and i.B2 .b shadows b of the block B2 . 4 Universal Conversion Algorithm The priority of the relabelling is as follows: labels of visible isolated ports, inner actions and co-actions, labels of visible connected ports, labels of invisible connected ports, labels of invisible isolated ports. We wish to retain the maximal number of names of visible isolated ports as they correspond to observable actions and co-actions responsible for communication with environment. On the other hand, we are the least interested in retaining names of invis- ible isolated ports as they correspond to non executable actions and co-actions. We introduce the following symbols: [ Actions = A(CSS i ) the set of all actions contained in CSS scripts CSS i ∈CSS [ Actions = A(CSS i ) the set of all co-action contained in CSS scripts CSS i ∈CSS [ Agents = K(CSS i ) the set of all agent constants contained in CSS scripts CSS i ∈CSS E is the infinite set of labels, where E ∩ Actions = ∅ ∧ E ∩ Actions = ∅ C is the infinite set of agent constants, where C ∩ Agents = ∅. Please note, the set E contains co-labels with the same names as the labels in E. We will consider some finite subset E 0 ⊂ E of the set of labels E and some finite set C 0 ⊂ C of the set of agent constants C. We will use the following notations: 7 8 – The ordered pair (Bi , CSSi ) represents the block Bi ∈ B and the CSS script CSSi = ρ(Bi ) ∈ CSS assigned to that block. – The symbol Bi∗ denotes the name of the block Bi and the symbol CSSi ∗ denotes the name of CSSi script. – The symbol #A denotes the cardinality of the set A, where # binds weaker than operations in the field of sets. The conversion algorithm is presented here: 1. The names of CSS scripts become the same as names of corresponding blocks. We create a new set CSS 0 of CSS scripts, i.e. the set of sequences of algebraic equations, in the following manner. For each agent block Bi ∈ B: a) If for a pair (Bi , CSSi ) the names of the agent block and the CSS script are the same, i.e. Bi∗ = CSSi ∗ , then we add the CSSi script to the CSS 0 set. b) If for a pair (Bi , CSSi ) the agent constant Bi∗ ∈ / K(CSSi ), then we replace the name of the CSSi script and all the CSSi ∗ agent constants belonging to this script with Bi∗ and then we add the Bi∗ script to the CSS 0 set. c) If for a pair (Bi , CSSi ) the names of the agent block and CSS script are unlike, i.e. Bi∗ 6= CSSi ∗ , but the agent constant Bi∗ ∈ K(CSSi ), then we replace all the Bi∗ agent constants belonging to the CSSi script with the next agent constant from C and then we replace the CSSi script name and all the CSSi ∗ agent constants belonging to this script with Bi∗ and then we add the Bi∗ script to the CSS 0 set. 2. The ambiguities of names of the agent constants in CSS scripts are eliminated. We create a new CSS 00 set of CSS scripts in the following manner. For each CSS script CSSi ∈ CSS 0 : For each agent constant C ∈ K(CSSi ) that is different from the name of the script, i.e. C 6= CSSi ∗ , if there is another CSSj ∈ CSS 0 script such that C ∈ K(CSSj ), then we replace all the C agent constants in the CSSi script with the next constant from C and then we add CSSi to the CSS 00 set. 3. If the XCCS diagram is plain, then for each port Bi .a ∈ OutP we apply: all actions a ∈ A(Bi∗ ) in CSS script Bi∗ are changed to co-actions a. 4. We create the quotient set P /∼ of all possible equivalence classes of the set of ports P by synchronization relation SR. To the equivalence classes of SR we will assign consecutive labels from the set E 0 or labels from the set CA. We assume that ports from equivalence classes that have been assigned labels from the set E 0 are removed from the set P . a) We eliminate conflicts among visible isolated ports. For all labels a ∈ CA of visible isolated input and output ports we apply: If 0 < #V ∩ Iso ∩ k .InP (a) < #V ∩ Iso ∩ k .OutP (a), then to the equivalence classes of ports from the set V ∩ Iso ∩ k .InP (a) we assign the next label from the set E 0 . If 0 < #V ∩ Iso ∩ k .OutP (a) ≤ #V ∩ Iso ∩ k .InP (a), then to the equivalence classes of ports from the set V ∩ Iso ∩ k .OutP (a) we assign the next label from the set E 0 . 8 9 b) We eliminate conflicts of inner actions and co-actions with visible isolated ports. For every inner action a ∈ Int and co-action a ∈ Int we apply: If the action a is in conflict with visible isolated port Bi .a ∈ OutP , then in all CSS scripts that are assigned to blocks from the set k .Int(a) all actions a assume the name of the next label from the set E 0 . If the co-action a is in conflict with visible isolated port Bi .a ∈ OutP , then in all CSS scripts that are assigned to blocks from the set k .Int(a) all co-actions a assume the name of the next label from the set E 0 . c) We eliminated conflicts among inner actions and co-actions. For every inner action a ∈ Int we apply: If 0 < #k .Int(a) < #k .Int(a), then in all CSS scripts assigned to blocks from the set k .Int(a) all actions a assume the name of the next label from the set E 0 . If 0 < #k .Int(a) ≤ #k .Int(a) then in all CSS scripts assigned to blocks from the set k .Int(a) all co-actions a assume the name of the next label from the set E0. d) We relabel visible connected ports. In this step we begin from the least numerous equivalent classes. For every equivalence class of synchronization relation SR we apply: If in the equivalence class exists a port with some label a ∈ CA and all other ports in this class when relabelled with this label a will not be conflicting with other visible ports and inner actions, then to this class we assign the label a, otherwise we assign the next label from the set E 0 . e) We relabel invisible connected ports. In this step we begin from the least numer- ous equivalent classes. For every equivalence class of synchronization relation SR we apply: If in the equivalence class exists a port with some label a ∈ CA and all other ports in this class when relabelled with this label a will not conflict and shadow with: visible ports, inner actions, other invisible connected ports and previously „relabelled ports”, then to this class we assign the label a, otherwise we assign the next label from the set E 0 . f) We relabel invisible isolated ports. For every one element equivalence class of SR we apply: If the port from this class is in conflict with or shadows: visible port, inner action or co-action, previously „relabelled ports”, then to this port we assign the next label from the set E 0 . g) We eliminate conflicts among invisible isolated ports. For all labels a ∈ CA of invisible isolated input and output ports we apply: If 0 < #I ∩ Iso ∩ k .InP (a) < #I ∩ Iso ∩ k .OutP (a), then to the equivalence classes of ports from the set I ∩ Iso ∩ k .InP (a) we assign the next label from the set E 0 . If 0 < #I ∩ Iso ∩ k .OutP (a) ≤ #I ∩ Iso ∩ k .InP (a), then to the equivalence classes of ports from the set I ∩ Iso ∩ k .OutP (a) we assign the next label from the set E 0 . 5. We relabel actions and co-actions in CSS scripts from the CSS 00 set. For every port Bi .a ∈ InP and for every port Bi .a ∈ OutP we apply: 9 10 If the equivalence class [Bi .a]SR has been assigned to the label e, then in CSS script Bi∗ all a actions are relabelled to e. If the equivalence class [Bi .a]SR has been assigned to the label e, then in CSS script Bi∗ all co-actions a are relabelled to e. 6. We create the output CCS script. The main agent equation takes the form: S = (B1 |B2 | . . . |Bn )\{Res} (20) where B1 , B2 , . . . , Bn ∈ CSS 00 , and the set Res contains all labels which has been assigned to the equivalence classes of SR with invisible ports and labels of remaining invisible ports. Under the main expression we place all definitions of CSS scripts. 4.1 Example Conversion CCS process algebra can be used to verify modular asynchronous circuits [8]. Let us then examine a simple XCCS model of NAND gate presented in Fig. 7. And a0 Neg a1 c0 a0 b0 And Neg b0 c1 a1 b1 b1 Fig. 7. XCCS model of NAND gate Definitions of CSS scripts assigned to the blocks are as follows: And = a0.(b0.’c0.And + b1.’c0.And) + a1.(b0.’c0.And + b1.’c1.And); Neg = a0.’b1.Neg + a1.’b0.Neg; The algorithm executes as follows: 1. The names of CSS scripts are already the same as names of corresponding blocks. 2. There are no any ambiguities of names of agent constants in CSS scripts. 3. Skipped as it is full XCCS diagram. 4. Assume that we have the subset E 0 = {b0_1, b1_1} ⊂ E of labels E. We partition the set of ports P into equivalence classes P /∼ of synchronization relation SR. a) For every label a ∈ CA of visible isolated input and output port: V ∩ Iso ∩ k .InP (b0) = {And.b0} V ∩ Iso ∩ k .OutP (b0) = {N eg.b0} V ∩ Iso ∩ k .InP (b1) = {And.b1} V ∩ Iso ∩ k .OutP (b0) = {N eg.b1} 10 11 The following conditions hold: 0 < #V ∩ Iso ∩ k .OutP (b0) = 1 ≤ #V ∩ Iso ∩ k .InP (b0) = 1 0 < #V ∩ Iso ∩ k .OutP (b1) = 1 ≤ #V ∩ Iso ∩ k .InP (b1) = 1 Thus, to the equivalence classes of ports from set V ∩ Iso ∩ k .OutP (b0) and V ∩ Iso ∩ k .OutP (b1) we assign consecutive labels from the set E 0 : – [N eg.b0]SR = {N eg.b0} 7→ b0_1 – [N eg.b1]SR = {N eg.b1} 7→ b1_1 b) Skipped as the diagram does not have inner actions. c) Skipped as the diagram does not have inner actions and co-actions. d) Skipped as the diagram does not have visible connected ports. e) We consider equivalence classes of invisible connected ports. In both of these classes we find a label that will not cause conflicts and shadows with visible ports and invisible connected ports when the relabelling is applied, thus: – [And.c0]SR = {And.c0, N eg.a0} 7→ c0 ∈ CA – [And.c1]SR = {And.c1, N eg.a1} 7→ c1 ∈ CA f) Skipped as the diagram does not have invisible isolated ports. g) Skipped as the diagram does not have invisible isolated ports. 5. We consider equivalence classes that have been assigned the labels: – [N eg.b0]SR = {N eg.b0} 7→ b0_1 – [N eg.b1]SR = {N eg.b1} 7→ b1_1 – [And.c0]SR = {And.c0, N eg.a0} 7→ c0 – [And.c1]SR = {And.c1, N eg.a1} 7→ c1 After the relabelling the CSS scripts look like these: – And = a0.(b0.c0.And + b1.c0.And) + a1.(b0.c0.And + b1.c1.And) – Neg = c0.b1_1.N eg + c1.b0_1.N eg 6. We specify the output CCS script: NAND = (And|N eg)\{c0, c1} And = a0.(b0.c0.And + b1.c0.And) + a1.(b0.c0.And + b1.c1.And) N eg = c0.b1_1.N eg + c1.b0_1.N eg 5 Conclusions and Future plans We presented the Universal Conversion Algorithm that is helpful when we use XCCS modelling language as a tool supporting fast and flawless development of CCS process algebra scripts. This algorithm takes into consideration the priority of actions in XCCS diagram and strife to minimize the number of relabelled actions for the sake of clarity. We plan to elaborate analogous conversion algorithm for a hierarchical version of XCCS modelling language. This would allow easy development and management of 11 12 the libraries of CCS scripts. In this approach, any CCS script can be represented as a hierarchical agent block. Two or more hierarchical blocks can be used to compile a new model. We do not need to worry about unwanted synchronizations, non-executable actions and absence of desired synchronizations. The conversion algorithm will care to produce a proper resulting CCS script. Until now, the creation and management of CCS script libraries was hardly possible due to the nature of synchronization in CCS process calculus and lack of appropriate tools. References 1. Balicki, K., Szpyrka, M.: Formal definition of XCCS modelling language. Fundamenta In- formaticae 93 (2009) 1–15 2. Milner, R.: A Calculus of Communicating Systems. Volume 92 of LNCS. Springer-Verlag (1980) 3. Milner, R.: Communication and Concurrency. Prentice-Hall (1989) 4. Fencott, C.: Formal Methods for Concurrency. International Thomson Computer Press, Boston, MA, USA (1995) 5. Aceto, L., Ingófsdóttir, A., Larsen, K., Srba, J.: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, Cambridge, UK (2007) 6. Szpyrka, M., Balicki, K.: XCCS – graphical extension of CCS language. In: Proc. of Mixdes 2006, the 14th International Conference Mixed Design of Integrated Circuits and Systems, Ciechocinek, Poland (2007) 688–693 7. Szpyrka, M., Matyasik, P.: Formal modelling and verification of concurrent systems with XCCS. In: Proceedings of the 7th International Symposium on Parallel and Distributed Com- puting (ISPDC 2008), Krakow, Poland (2008) 454–458 8. Joeli, M., Kol, R., eds.: Verification of Systems and Circuits Using L OTOS, Petri Nets, and CCS. John Wiley and Sons, Chichester, UK (2008) 12