Kernel P Systems Modelling, Testing and Veri cation

Kernel P Systems Modelling, Testing and Verification Marian Gheorghe1, Rodica Ceterchi2, Florentin Ipate2,3and Savas Konur1 1School of Electrical Engineering and Computer Science, University of Bradford Bradford BD7 1DP, UK {m.gheorghe, s.konur}@bradford.ac.uk 2Department of Computer Science, University of Bucharest Str. Academiei nr. 14, 010014, Bucharest, Romania [email protected], [email protected] 3Department of Computer Science, University of Pite¸sti Str Targul din Vale, nr 1, 110040, Arge¸s, Romania Summary. A kernel P system (kP system, for short) integrates in a coherent and elegant manner many of the P system features most successfully used for modelling various applications and, consequently, it provides a framework for analyzing these models. In this paper, we illustrate the modeling capabilities of kernel P systems by showing how other classes of P systems can be represented with this formalism and providing a number of kP system models for sorting algorithms. Furthermore, the problem of testing systems modelled as kP systems is also discussed and a test generation method based on automata is proposed. We also demonstrate how formal verification can be used to validate that the given models work as desired. 1 Introduction Membrane systems were introduced in [27] as a new natural computing paradigm inspired by the structure and distribution of the compartments of living cells, as well as by the main bio-chemical interactions occurring within compartments and at the inter-cellular level. They were later also called P systems. An account of the basic fundamental results can be found in [28] and a comprehensive description of the main research developments in this area is provided in [29]. The key challenges of the membrane systems area and a discussion on some future research directions, are available in a more recent survey paper [20]. In recent years, significant progress has been made in using P systems to model and simulate systems and problems from various areas. However, in order to facilitate the modelling, in many cases various features have been added in an ad-hoc manner to these classes of P systems. This has led to a multitude of P systems variants, without a coherent integrating view. The newly introduced concept of 206 M. Gheorghe et al kernel P systems (kP systems) [16, 17] provides a response to this problem. A kP system integrates in a coherent and elegant manner many of the P system features most successfully used for modelling various applications and, consequently, it provides a framework for analyzing these models. Furthermore, the expressive power of these systems has been illustrated by a number of representative case studies [19, 17]. The kP system model is supported by a modelling language, called kP- Lingua, capable of mapping a kP system specification into a machine readable representation. Furthermore, kP systems are supported by a software framework, kPWorkbench [21], which integrates a set of related simulation and verification tools and techniques. Another complementary method to simulation and verification is testing, a major activity in the lifecycle of software systems. In practice, software products are almost always validated through testing. Testing has been discussed for celllike P systems and various strategies, such as rule coverage based and automata based techniques, have been proposed [15, 24]. Until now, however, testing has not been discussed in the context of kP systems. In this paper we further illustrate the modeling capabilities of kernel P systems by showing that other classes of P systems can be represented with this formalisms and by providing a number of kP system models for sorting algorithms. We present in this paper the relationship between kP systems and active membrane systems with electrical charges, whereas in [16, 17, 18] we have also investigated the relationship with neural-like P systems. We also study here the relationship between kP systems and P systems with symport/antiport rules. Furthermore, the problem of testing systems modelled as kP systems is also discussed and a test generation method based on automata is proposed. We also demonstrate how formal verification can be used to validate that the given models work as desired. 2 kP Systems - Main Concepts and Definitions We consider that standard P system concepts such as strings, multisets, rewriting rules, and computation are well-known and refer to [28] for their formal notations and precise definitions. The kP system concepts and definitions introduced below are from [16, 17]; some are slightly changed and this will be mentioned. Definition 1. Tis a set of compartment types,T={t1, . . . , ts},where ti= (Ri, σi),1≤i≤s, consists of a set of rules, Ri, and an execution strategy, σi, defined over Lab(Ri), the labels of the rules of Ri. Remark 1. The compartments that appear in the definition of the kP systems will be instantiated from these compartment types. The types of rules and the execution strategies will be discussed later. Definition 2. Akernel P (kP) system of degree nis a tuple kΠ = (A, µ, C1, . . . , Cn, i0), Kernel P Systems Modelling, Testing and Verification 207 where Ais a finite set of elements called objects;µdefines the initial membrane structure, which is a graph, (V, E), where Vare vertices indicating components, and Eedges; Ci= (ti, wi),1≤i≤n, is a compartment of the system consisting of a compartment type from Tand an initial multiset,wiover A;iois the output compartment where the result is obtained. 2.1 kP System Rules The discussion below assumes that the rules we refer to belong to the same compartment, Ci. Each rule rmay have a guard gwhich refers to the multiset where the rule is applied to. Its generic form is r{g}. The rule ris applicable to a multiset wwhen its left hand side is contained into wand gis true for w. The guards are constructed using multisets over A, as operands, and relational and Boolean operators. Let us first introduce some notations. For a multiset wover Aand an element a∈A, we denote by |w|athe number of objects aoccurring in w. Let us denote Rel ={<, ≤,=,6=,≥, >}, the set of relational operators, γ∈Rel, a relational operator, ana multiset and r{g}a rule with guard g. We first introduce an abstract relational expression which is evaluated for any multiset where the rule is applied to. Definition 3. If gis the abstract relational expression γanand wis the multiset it refers to, then the guard denotes the relational expression |w|aγn. The guard g is true for the multiset wif |w|aγn is true. One can consider the Boolean operators ¬(negation), ∧(conjunction) and ∨(disjunction), listed with respect to the decreasing precedence order. Abstract Boolean expressions are obtained by connecting abstract relational expressions by Boolean operators. Definition 4. If gis the abstract Boolean expression and the current multiset is w, then the guard denotes the Boolean expression for w, obtained by replacing abstract relational expressions with relational expressions for w. The guard gis true for the multiset wwhen the Boolean expression for wis true. Definition 5. A guard is: (i) one of the Boolean constants true or false; (ii) an abstract relational expression; or (iii) an abstract Boolean expression. Example 1. If gis the guard ≥a5∧ ≥ b3∨ ¬ > c and wa multiset it refers to, then gis true in wif it has at least 5 a0s and 3 b0s or no more than one c. Definition 6. A rule from a compartment Cli= (tli, wli)can have one of the following types: •(a) rewriting and communication rule: x→y{g}, where x∈A+and yhas the form y= (a1, t1). . . (ah, th),h≥0,aj∈A and tjindicates a compartment type from T– see Definition 2 – with instance 208 M. Gheorghe et al compartments linked to the current compartment; tjmight also indicate the type of the current compartment, tli, (in this case it is not present on the right hand side of the rule); if a link does not exist (i.e., there is no link between the two compartments in E) then the rule is not applied; if a target, tj, refers to a compartment type that has more than one instance connected to Cli, then one of them will be non-deterministically chosen; •(b) structure changing rules; the following types of rules are considered: – (b1) membrane division rule: [x]tli→[y1]ti1. . . [yp]tip{g}, where x∈A+and yj∈A∗; the compartment Cliwill be replaced by p compartments; the j-th compartment, instantiated from the compartment type tijcontains the same objects as Cli, but x, which will be replaced by yj; all the links of Cliare inherited by each of the newly created compartments; – (b2) membrane dissolution rule: []tli→λ{g}; the compartment Cliwill be destroyed together with its links; – (b3) link creation rule: [x]tli; []tlj→[y]tli−[]tlj{g}; the current compartment is linked to a compartment of type tljand xis transformed into y; if more than one instance of the compartment type tlj exists then one of them will be non-deterministically picked up; gis a guard that refers to the compartment instantiated from the compartment type tl1; – (b4) link destruction rule: [x]tli−[]tlj→[y]tli; []tlj{g}; is the opposite of link creation and means that the compartments are disconnected. The membrane division is defined slightly differently here compared to [16, 17]. Currently, the right hand side of the rule uses simple multisets with no target compartments, as they were initially introduced in [16, 17]. 2.2 kP System Execution Strategies In kP systems the way in which rules are executed is defined for each compartment type tfrom T– see Definition 1 and Remark 1. As in Definition 1, Lab(R) is the set of labels of the rules R. Definition 7. For a compartment type t= (R, σ)from Tand r∈Lab(R), r1, . . . , rs∈Lab(R), the execution strategy,σ, is defined by the following •σ=λ, means no rule from the current compartment will be executed; •σ={r}– the rule ris executed; •σ={r1, . . . , rs}– one of the rules labelled r1, . . . , rswill be chosen nondeterministically and executed; if none is applicable then none is executed; this is called alternative or choice; •σ={r1, . . . , rs}∗– the rules are applied an arbitrary number of times ( arbitrary parallelism); •σ={r1, . . . , rs}>– the rules are executed according to maximal parallelism strategy x; Kernel P Systems Modelling, Testing and Verification 209 •σ=σ1&. . . &σs, means executing sequentially σ1, . . . , σs, where σi,1≤i≤ s, describes any of the above cases, namely λ, one rule, a choice, arbitrary parallelism or maximal parallelism; if one of σifails to be executed then the rest is no longer executed; •for any of the above σstrategy only one single structure changing rule is allowed. Arbitrary parallelism and maximal parallelism for rewriting and communication rules, as well as for structure changing rules (cell division, dissolution), are discussed in [29]. Remark 2. In certain cases the operator & will be ignored and the sequential execution will be denoted as σ=σ1. . . σs. Remark 3. A computation, as usual in membrane computing, is defined as a sequence of finite steps starting from the initial configuration, with the initial multisets distributed in compartments. In each step the rules are selected according to the execution strategy and this is given by the execution strategy in each compartment. The result of a computation will be the number of objects collected in the output compartment. For a kP systems kΠ, the set of all these numbers will be denoted by M(kΠ). Remark 4. When a terminal alphabet, F, is considered, the result of a computation will be the number of objects from Fcollected in the output compartment and this will be denoted by Mt(kΠ) 3 kP Systems and Other Classes of P Systems In this section we will investigate the relationship between kP systems and P systems with active membranes, but other relevant classes of P systems will be also considered, especially those with various applications, such as symport/antiport P systems. In [17, 18] neural-like P systems have been also considered. 3.1 P Systems with Active Membranes versus kP Systems We study how P systems with active membranes are simulated by kP systems. In this case we are dealing with a cell-like system, so the underlying structure is a tree and we have a set of labels (types) for the compartments of the system. The way the relationship between these P systems is presented in the sequel is a natural extension of the method proposed in [16, 17, 18]. In the previous investigations the set of objects from the output compartment has been mixed up with the rest of the objects of the system. In this investigation we separate the objects corresponding to the output compartment and provide a more consistent notation for the kP system involved. We also deal in this investigation with active membrane systems with an upper bound for the number of active components 210 M. Gheorghe et al Definition 8. A P system with active membranes of initial degree nis a tuple (see [29], Chapter 11) Π= (O, H, µ, w1,0, . . . , wn,0, R, i0)where: •Ois an alphabet of objects, w1,0, . . . , wn,0are the initial strings in the ninitial compartments and i0is the output compartment; •His the set of labels for compartments; •µdefines the tree structure associated with the system; •Rconsists of rules of the following types: – (a) rewriting rules:[u→v]e h, for h∈H,e∈ {+,−,0}(set of electrical charges), u∈O+,v∈O∗; – (b) in communication rules:u[]e1 h→[v]e2 h, for h∈H,e1, e2∈ {+,−,0}, u∈O+,v∈O∗; – (c) out communication rules:[u]e1 h→[]e2 hv, for h∈H,e1, e2∈ {+,−,0}, u∈O+,v∈O∗; – (d) dissolution rules:[u]e h→v, for h∈H\{s},sdenotes the skin membrane (the outmost one), e∈ {+,−,0},u∈O+,v∈O∗; – (e) division rules for elementary membranes:[u]e1 h→[v]e2 h[w]e3 h, for h∈H, e1, e2, e3∈ {+,−,0},u∈O+,v, w ∈O∗; The rules are executed in accordance with the maxim parallelism, but in each compartment only one of the rules (b)-(e) is executed. In the sequel we assume that the output compartment is neither dissolved nor divided. The result of a computation, obtained in i0is denoted by M(Π). The following result shows how the computation of a P system with active membranes starting with n1compartments and an upper bound to the number of active compartments can be performed by a kP system using only rewriting and communication rules. A first idea of this result has been given in [16, 17, 18]. Theorem 1. If Πis a P system with active membranes having n1initial compartments and an upper bound to the number of active compartments in any computation, then there exists a kP system, kΠ, of degree 2and using only rewriting and communication rules, such that M(Π) = M(kΠ). Proof. Let Π= (O, H, µ, w1,0, . . . , wn1,0, R, i0) be a P system with active membranes of initial degree n1. Initially, the polarizations of the n1compartments are all 0, i.e., e1=. . . =en1= 0. We will build a kP system with two compartments. Compartment C1will capture the contents and rules of all the compartments of Π. The other compartment, C2will be associated to i0and this will collect the result. We will need to keep track of a dynamic system of membranes, since we have dissolution and division of elementary membranes. We will identify a membrane by a pair (i, h) where i∈Iis an index associated with an instance of the membrane and h∈His its label. We use the index in addition to the label as the same label might appear several times in the system, especially after a membrane division rule has been applied. We work under the assumption that Iis finite. Its cardinal is equal to the maximum number of active membranes that may appear in any Kernel P Systems Modelling, Testing and Verification 211 computation – this is assumed to have an upper limit. We let i0∈Iand i0∈H. We will denote by (I×H)cthe currently used pairs (i, h). We assume that for any (i, h)∈(I×H)cand (j, h0)∈(I×H)c, we have i6=j. This way we make sure that the cardinal of (I×H)cis always at most the cardinal of I. Whenever a membrane dissolution takes place, its index and label are removed from (I×H)c. When a membrane division rule is applied the index and label of the divided compartment are removed from (I×H)cand two new values of indices with the same label are selected and added to the set (I×H)c. The tuple (i0, i0) is always in (I×H)c We will codify a compartment [w]e hby two tuples < e, i, h > and < w, i, h >, with (i, h)∈(I×H)c, and where, for a multiset w=a1. . . am,< w, i, h > denotes < a1, i, h > . . . < am, i, h >. These tuples appear in C1. When h=i0then in addition to the tuples present in C1, in C2, for [w]e i0we have eand w. For a compartment with label hand electrical charge ein Πthere is only one tuple < e, i, h > in C1, when h6=i0, or an ein C2, otherwise. By p(i, h) we denote the parent of the membrane with label hand of index i. If p(i, h)=(i0, h0) it means that the membrane with label h0and index i0is the parent of the membrane with label hand index i. By < x, p(i, h)>and < e, p(i, h)>we denote the tuples < x, i0, h0>and < e, i0, h0>, respectively. A new symbol, δ, will be used for the membrane dissolution and division to control the transfer of objects after these rules have been applied. Hence, we will use the guard =δall := ^(¬=< δ, i, h >|i∈I, h ∈H). We also introduce a guard checking that the symbols γ1ans γ2, related with the communication with the output compartment, i0, do not appear in the current multiset: =γall := (¬=γ1)∧(¬=γ2). We construct kΠ using T={t1, t2}, where tj= (R0 j, σj) (where R0 jand σj will be defined later), 1 ≤j≤2, as follows: kΠ = (A, µ0, C1, C2,2), where the elements of the system are given below. •µ0is the graph with nodes C1, C2and the edge linking them; •The alphabet is A=O∪ {0,00,+,+0,−,−0, γ1, γ2} ∪(S(i,h)∈I×H({< a, i, h >|a∈O∪ {δ}} ∪ {< e, i, h >|e∈ {0,+,−}})) •Cj= (tj, w0 j,0w00 j,0), 1 ≤j≤2 and C2is the output compartment. – The initial multiset, w0 1,0w00 1,0, is given by w0 1,0=< w1,0,1, h1> . . . < wn1,0, n1, hn1> wi0,0 where wi0,0means that wi0,0does not appear in the initial multiset of C1 (it will appear in C2). w00 1,0={< e1,1, h1> . . . < en1, n1, hn1> ei0 212 M. Gheorghe et al where e1=. . . =en1= 0, for all the initial multisets and initial membranes of Π, and, similar to the above case, ei0means that ei0does not appear in the initial multiset. The initial multiset w0 2,0w00 2,0, is given by w0 2,0=wi0,0, w00 2,0=ei0. Initially, the indices (I×H)1={(1, h1). . . (n1, hn1)}\{(i0, i0)}are used in association with compartment C1and (i0, i0) for C2. The currently used indices are (I×H)c= (I×H)1∪ {(i0, i0)}. –R0 1and R0 2contain the rules below. (a.1) For each (i, h)∈I×H\ {(i0, i0)}and each rule [u→v]e h∈R,e∈ {+,−,0}, we add to R0 1the rule < u, i, h >→< v, i, h > {=< e, i, h > ∧=δall ∧=γall}; these rules are applied only when the polarization e appears in the compartment with index iand label hand none of the (δ, j, h0), γ1,γ2appears, i.e., no dissolution or division has started and no communication with the output compartment, i0, takes place – see below. (a.2) For (i, h) = (i0, i0), we add to R0 1the rule < u, i0, i0>→< v, i0, i0> {=< e, i0, i0>∧=δall ∧=γall}and the rule u→v{=e∧=γall}to R0 2. (b.1) For each (i, h)∈I×H\ {(i0, i0)}, such that p(i, h)6= (i0, i0), and each rule u[]e1 h→[v]e2 h∈R,e1, e2∈ {+,−,0}, we add to R0 1the rule < u, p(i, h)>< e1, i, h >→< v, i, h >< e2, i, h > {=δall ∧=γall}; these rules will transform < u, p(i, h)>corresponding to ufrom the parent compartment to < v, i, h > corresponding to vfrom the compartment with index iand label h; the polarization is changed; as there is only one object < e1, i, h >, it follows that only one single rule corresponding to the compartment can be applied at any moment of the computation. (b.2) When (i, h) = (i0, i0), then the rules added to R0 1are < u, p(i0, i0)>< e1, i0, i0>→< v, i0, i0>< e2, i0, i0>(ve0 2γ1,2)γ1{=δall ∧=γall}and γ1→λ; and the rules added to R0 2are e0 2→e2{=γ1}and γ1e→λ, e∈ {0,+,−}. The first rule apart from simulating the communication rule, also introduces γ1in both compartments. In C2it helps changing the polarization of it and in C1it helps with the synchronisation of the computation. Then the symbol disappears. (b.3) When p(i, h) = (i0, i0), then we add to R0 1the rules < u, i0, i0>< e1, i, h >→< v, i, h >< e2, i, h > (γ2,2)γ2{=δall ∧=γall}and γ2→λ. The rule uγ2→λis added to R0 2. Similar to (b.2), γ2is introduced in both compartments and in C2it helps removing u. (c.1) For each (i, h)∈I×H\ {(i0, i0)}, such that p(i, h)6= (i0, i0), and each rule [u]e1 h→[]e2 hv∈R,e1, e2∈ {+,−,0}, we add the rule < u, i, h >< e1, i, h >→< v, p(i, h)>< e2, i, h > {=δall ∧=γall}. (c.2) When (i, h)=(i0, i0), then we add to R0 1the rule < u, i0, i0>< e1, i0, i0>→< v, p(i0, i0)>< e2, i0, i0>(e0 2γ1,2)γ1{=δall ∧=γall}. As in (b.2), we use γ1→λin R0 1and e0 2→e2{=γ1}in R0 2. We need to Kernel P Systems Modelling, Testing and Verification 213 add to R0 2the rule uγ1e→λ. The rules make sure that in C1we simulate the communication rule and in C2udisappears and the polarization is changed to e2. (c.3) When p(i, h) = (i0, i0), then the rule added to R0 1is < u, i, h >< e1, i, h >→< v, i0, i0>< e2, i, h > (v, 2) {=δall ∧=γall}. This rule simulates the communication rule and introduces vinto C2. (d.1) for each (i, h)∈I×H\ {(i0, i0)}, such that p(i, h)6= (i0, i0), and each rule [u]e h→v∈R,e∈ {+,−,0}, we add to R0 1the rule < u, i, h >< e, i, h >→< v, p(i, h)>< δ, i, h > {=δall ∧=γall}; all the objects corresponding to those from the compartment of index iand label h must be moved to the parent compartment - this will happen in the presence of (δ, i, h) when no other transformation will take place; this is obtained by using in R0 1rules < a, i, h >→< a, p(i, h)>{=< δ, i, h >}, a∈Oand < δ, i, h >→λ; the set (I×H)cwill change now by removing the pair (i, h) from it. (d.2) When p(i, h)=(i0, i0), then the rules above will become < u, i, h >< e, i, h >→< v, i0, i0>< δ, i, h > (v, 2) {=δall ∧=γall}and < a, i, h >→< a, i0, i0>(a, 2) {= (δ, i, h)},a∈O. (e) For each (i, h)∈I×H\ {(i0, i0)}and each rule [u]e1 h→[v]e2 h[w]e3 h∈R, e1, e2, e3∈ {+,−,0}; we add to R0 1the rule < u, i, h >< e1, i, h >→< v, j1, h >< e2, j1, h >< w, j2, h >< e3, j2, h >< δ, i, h > {=δall ∧ =γall}– the pair (i, h) is removed from (I×H)cand two new pairs (j1, h) and (j2, h), existing in I×H, with j16=j2, are added to (I×H)c and one < u, i, h > is transformed into < v, j1, h > and < w, j2, h > and their associated electrical charges; then the content corresponding to compartment of index iand label hwill be moved to those of index j1and j2and the same label h, hence rules < a, i, h >→< a, j1, h >< a, j2, h > {=< δ, i, h >},a∈Oare added to R0 1; finally, < δ, i, h >→λ is also included in the set of rules of C1; it is clear that only one division rule for the same compartment is applied in any step of the computation. We note that in C0 2there are no rules for dissolution and division as the output compartment is not afected by these rules. The execution strategy in both compartments, C1and C2is maximal parallelism. For a sequence of rules applied in Π, we have a corresponding sequence of rules in kΠ. Obviously the objects obtained in the output compartment of Πare the same with those obtained in C2of kΠ. 3.2 P Systems with Symport/Antiport versus kP Systems The following definition is from [29]. Definition 9. A P system (of degree d≥1) with antiport and/or symport rules is a construct 220 M. Gheorghe et al Theorem 5. The above algorithm sorts in ascending order a sequence of n, n ≥1, positive integer numbers in n−1steps. Remark 6. 1. The kP system kΠ3has simpler rules (non-cooperative) than kΠ2 (cooperative rules), but the guards of the rules in kΠ2are simpler than those belonging to kΠ3. 2. The number of rules applied in each step to interchange axi iand axi+1 i+1 is max{xi, xi+1}for kΠ2and xi+xi+1 for kΠ3. Hence, kΠ2uses less rules than kΠ3in each one of the n−1 steps. 4.3 A kP System for Sorting in Constant Time We suppose the integers to be sorted x1,· · · xndistinct. We use a total of n2+ 2ncompartments: -Ci,j, 1 ≤i, j ≤n, where each Ci,j will be responsible for a comparison; -Ci, 1 ≤i≤2n, where each Ci, 1 ≤i≤n, will collect the results of comparing xito the rest; and Ci,n+ 1 ≤i≤2n, will collect the sorted result. The connections between compartments are given by the set of edges E=∪n i=1Ei where Ei={(Ci, Ci,j)|1≤j≤n}∪{(Ci, Ck)|n+ 1 ≤k≤2n},1≤i≤n. Each Ci,j , 1 ≤i, j ≤n, will contain the initial multiset wi,j,0=aixiajxjaand the rules r0 i,j :ai→ajF{> aifj(·)};r00 i,j :aj→ai{< ajfi(·)};r000 i,j :a→a0; ri,j :a0→(F, i){≥ F}, where fi(z) = |z|aiand fj(z) = |z|aj. The execution strategy is σi,j ={r0 i,j, r00 i,j, r000 i,j, ri,j}>. Note that the rules r0 i,j, r00 i,j implement a comparator between xiand xj, similar to the one of the previous section. The modified comparator produces also a symbol F(False) when xi> xj, signifying that xi≤xjis false. If the rewriting rules r0 i,j, r00 i,j and r000 i,j have acted, then a single Fwill be sent to compartment Ci(by using the rule ri,j). In compartment Ci,1≤i≤n, we have the initial multiset wi,0=aixiaand the rules r0 i:a→a0;r00 i:a0→a00; ri,0:ai→(a, n + 1){< F ∧=a00};ri,k :ai→(a, n +k+ 1){=Fk∧=a00}, 1≤k≤n−1. The execution strategy is σi={r0 i, r00 i, ri,0,· · · , ri,n−1}>. Compartments Ci, n + 1 ≤i≤2n, are initially empty and contain no rules. The functioning of the system is as follows. Initially, in compartments Ci,j , 1 ≤ i, j ≤n, the rules r0 i,j, r00 i,j,and r000 i,j act. If xi> xjthe values will be interchanged Kernel P Systems Modelling, Testing and Verification 221 and some Fs will be produced (rules r0 i,j, r00 i,j are used), signifying that xi≤xjis false. Also r000 i,j is used to transform ain a0. If at least one Fis produced in Ci,j, then a single Fwill be sent to Ci, using rule ri,j. In parallel, in each compartment Ci, 1 ≤i≤n, in the first two steps the rules r0 iand r00 iare applied. After these two steps, no rules are applicable in Ci,j, 1 ≤i, j ≤n, and in Ci, 1 ≤i≤n, the rules ri,k, 0 ≤k≤n−1,might be applicable, depending on the number of Fs collected.The number of Fs tells us how many comparisons xi≤xj, 1 ≤j≤n, are false. If we have ksuch Fs in Ci, it means that xiis greater than exactly kother values, which means that in the sorted order it must be the (k+ 1)-th component. This is accomplished by sending axiin Cn+k+1. The maximum number of Fs in Ciis n−1 because Ci,i will never produce an F. If there are no Fs in Ci, this means that xiis the minimum, and axiwill be sent to Cn+1. Compartments Cn+i, 1 ≤i≤n, collect the result of sorting. Each such Cn+iwill contain at the end of the computation the string axki,xkibeing the i-th value in the sorted order. The computation has three steps, the first two ones in which Ci,j , 1 ≤i, j ≤n, work, and a third one in which Ci, 1 ≤i≤n, work. Theorem 6. The above kP system sorts nintegers in 3 steps. 4.4 Sorting in Constant Time with Membrane Division The algorithm in the previous section uses only rewriting and communication rules. This solution, although computationally efficient, requires an initial, quite complex, arrangement of compartments and multisets. We present here an algorithm which creates its working space by using membrane division rules. We want to sort ndistinct integers, x1,· · · xn, represented as a1x1,· · · , anxn. We start with a total of 3ncompartments: -Ci, 1 ≤i≤n, where each Ci, will collect the results of comparing xito the rest; -Ci,n+ 1 ≤i≤2n, will collect the sorted result; -Ck, 2n+ 1 ≤k≤3n, such that C2n+i⊂Ci, responsible for creating the comparator compartments. The connections between compartments are given by the set of edges E=∪n i=1Ei where Ei={(Ci, C2n+i)}∪{(Ci, Ck)|n+ 1 ≤k≤2n},1≤i≤n. In compartment Ci,1≤i≤n, we have the initial multiset wi,0=aixiaand the rules r0 i:a→a0;r00 i:a0→a00;r000 i:a00 →a000; ri,0:ai→(a, n + 1){< F ∧=a000};ri,k :ai→(a, n +k+ 1){=Fk∧=a000}, 1≤k≤n−1. The execution strategy is σi={r0 i, r00 i, r000 i, ri,0,· · · , ri,n−1}>. 222 M. Gheorghe et al Compartments Ci, n + 1 ≤i≤2n, are initially empty and contain no rules. Compartments C2n+i, 1 ≤i≤n, contain an initial multiset s, where sis a new object, and the membrane division rules [s]2n+i→[a1x1aixia]i,1· · · [ajxjaixia]i,j · · · [anxnaixia]i,n,1≤i≤n. These rules will generate in each Cithe compartments Ci,j, 1 ≤j≤n. In each Ci,j we will have the multiset ajxjaixia, and the rules r0 i,j :ai→ajF{> aifj(·)};r00 i,j :aj→ai{< ajfi(·)};r000 i,j :a→a0; ri,j :a0→(F, i){≥ F}, where fi(z) = |z|aiand fj(z) = |z|aj. The execution strategy is σi,j ={r0 i,j, r00 i,j, r000 i,j, ri,j}>. Note that this is the comparator of the previous section, which sends a single Fin Ciif xi≤xjis false. During the first step, in compartment Cirule r0 iis executed, while in C2n+i the membrane division rule is applied, generating the Ci,j, 1 ≤j≤n. The next three steps are identical to the ones of the previous algorithm. Theorem 7. The above kP system sorts nintegers in 4 steps. 5 Simulating and Verifying kP Systems In Section 4, we have illustrated that kP systems provide a coherent and expressive language that allow us to model various systems that were originally implemented by different P system variants. In addition to the modelling aspect, there has been a significant progress on analysing kP systems using various simulation and verification methodologies. The methods and tools developed in this respect have been integrated into a software platform, called kPWorkbench, to support the modelling and analysis of kP systems. The ability of simulating kernel P systems is an important feature of this tool. Currently, there are two different simulation approaches, kPWorkbench Simulator and Flame (Flexible Large-Scale Agent Modelling Environment). Both simulators receive as input a kP system model written in kP–Lingua and outputs a trace of the execution, which is mainly used for checking the evolution of a system and for extracting various results out of the simulation. The simulators provide traces of execution for a kP system model, and an interface displaying the current configuration (the content of each compartment) at each step. It is useful for checking the temporal evolution of a kP system and for inferring various information from the simulation results. Another important analysis method that kPWorkbench features is formal verification, requiring an exhaustive analysis of system models against some queries to be verified. The automatic verification of kP systems brings in some challenges as they feature a dynamic structure by preserving the structure changing rules such as membrane division, dissolution and link creation/destruction. kPWorkbench Kernel P Systems Modelling, Testing and Verification 223 Prop. Pattern (i) Informal query, (ii) Formal query using patterns 1 Existence (i) The numbers will be eventually sorted, i.e. the multisets representing the numbers will be in ascending order in the compartments (ii) eventually (c1.a <=c2.a & c2.a <=c3.a & c3.a <=c4.a & c4.a <=c5.a & c5.a <=c6.a) 2 Universality (i) Counters in different compartments are always sync’ed (ii) always (c1.c = c2.c & c2.c = c3.c & c3.c = c4.c & c4.c = c5.c & c5.c = c6.c) 3 Steady-state (i) In the state-state, the numbers are sorted (ii) steady-state (c1.a <=c2.a & c2.a <=c3.a & c3.a <=c4.a & c4.a <=c5.a & c5.a <=c6.a) 4 Existence (i) The algorithm will eventually stop (ii) eventually (ci.c = 0) 5 Response (i) An unsorted state of two adjacent compartments will always be followed by a sorted one (ii) (ci.a >ci+1.a) followed-by (ci.a <=ci+1.a) Table 1: List of properties derived from the property language and their representations in different formats. employs different verification strategies to allieviate these issues. The framework supports both Linear Temporal Logic (LTL) and Computation Tree Logic (CTL) properties by making use of the Spin [22] and NuSMV [13] model checkers. In order to facilitate the formal specification, kPWorkbench features a property language, called kP-Queries, comprising a list of natural language statements representing formal property patterns, from which the formal syntax of the Spin and NuSMV formulas are automatically generated. The property language editor interacts with the kP-Lingua model in question and allows users to directly access the native elements in the model, which results in less verbose and shorter state expressions, and hence more comprehensible formulas. kP-Queries also features a grammar for the most common property patterns. These features and the natural language like syntax of the language make the property construction much easier. Some of the commonly used patterns are “next”, “existence”, “absence”, “universality”, “recurrence”, “steady-state”, “until”, “response” and “precedence”. The details can be found in [21]. We now illustrate the usage of the query patters on the sorting algorithm given in Section 4.1. The other algorithms can be considered in a similar manner. In order to verify that the algorithm works as desired, we have constructed a set of properties specified in kP-Queries, listed in Table 1. The applied pattern types are given in the second column of the table. For each property we provide the following information; (i) informal description of each kP-Query, and (ii) the formal kP- Query using the patterns. The queries given in Table 1 capture that the algorithm given in Section 4.1 works as desired. We note that both kP–Lingua model and the queries are automatically converted into the languages required by the corresponding model checkers. So, the verification process in kPWorkbench is carried out in automatic manner. 224 M. Gheorghe et al 6 Testing kP Systems Using Automata Based Techniques In this section we outline how the kP systems obtained in the previous sections can be tested using automata based testing methods. The approach presented here follows the blueprint presented in [24] and [15] for cell-like P systems. We illustrate our approach on kΠ1, the application of our approach on the other kP system modeling sorting algorithms is similar. Naturally, in order to apply an automata based testing method to a kP model, a finite automata needs to be obtained first. In general, the computation of a kP system cannot be fully modelled by a finite automaton and so an approximate automaton will be sought. The problem will be addressed in two steps. •Firstly, the computation tree of a P system will be represented as a deterministic finite automaton. In order to guarantee the finiteness of this process, an upper bound kon the length of any computation will be set and only computations of maximum ktransitions will be considered at a time. •Secondly, a minimal model, that preserves the required behaviour, will be defined on the basis of the aforementioned derivation tree. Let Mk= (Ak, Qk, q0,k, Fk, hk) be the finite automaton representation of the computation tree, where Akis the finite input alphabet, Qkis the finite set of states, q0,k ∈Qkis the initial state, Fk⊆Qkis the set of final states, and hk:Qk×Ak−→ Qkis the next-state function. Akis composed of the tuples of multisets that label the transition of the computation tree. The states of Tkcorrespond to the nodes of the tree. For testing purposes we will consider all the states as final. It is implicitly assumed that a non-final “sink” state qsink that receives all “rejected” transitions, also exists. Consider kΠ1, the kP system in section 4.1, n= 6 and the sequence to be sorted 3, 6, 9, 5, 7, 8. Then the initial multisets are: w1,0=a3c10p;w2,0=a6c10;w3,0=a9c10p;w4,0=a5c10;w5,0=a7c10p;w6,0= a8c10. As kΠ1is a deterministic kP system, there are no ramification in the computation tree. For k= 3, this is represented below. Compartments - Step C1C2C3C4C5C6 0rr3 1,1r2,1r rr9 1,3r2,3r rr7 1,5r2,5r 1rr3,1rr3 4,2rr3,3rr5 4,4r4 5,4rr3,5rr7 4,6 2r rr6 1,2r2,2r rr9 1,4r2,4r rr2,6 3r rr0 3,2rr5 1,3r5,3rr0 3,4rr7 1,5r2 5,5rr0 3,6 Let us denote α1= (rr3 1,1r2,1, r, rr9 1,3r2,3, r, rr7 1,5r2,5, r), α2= (rr3,1, rr3 4,2, rr3,3, rr5 4,4r4 5,4, rr3,5, rr7 4,6), α3= (r, rr6 1,2r2,2, r, rr9 1,4r2,4, r, rr2,6), α4= (r, rr0 3,2, rr5 1,3r5,3, rr0 3,4, rr7 1,5r2 5,5, rr0 3,6). Kernel P Systems Modelling, Testing and Verification 225 Then, for k= 3, Mk= (Ak, Qk, q0,k, Fk, hk), where Ak={α1, α2, α3, α4},Qk={q0,k, q1,k, q2,k, q3,k, q4,k},Fk=Qk, and hk, the nextstate function, is defined by: hk(qi−1,k, αi) = qi,k), 1 ≤i≤4. As Mkis a deterministic finite automaton over Ak, one can find the minimal deterministic finite automaton that accepts exactly the language defined by Mk. However, as only sequences of at most ktransitions are considered, it is irrelevant how the constructed automaton will behave for longer sequences. Consequently, a deterministic finite cover automaton of the language defined by Mkwill be sufficient. Adeterministic finite cover automaton (DFCA) of a finite language Uis a deterministic finite automaton that accepts all sequences in Uand possibly other sequences that are longer than any sequence in U[4], [5]. A minimal DFCA of Uis a DFCA of Uhaving the least possible states. A minimal DFCA may not be unique (up to a renaming of its states). The great advantage of using a minimal DFCA instead of the minimal deterministic automaton that accepts precisely the language Uis that the size (number of states) of the minimal DFCA may be much less than that of the minimal deterministic automaton that accepts U. Several algorithms for constructing a minimal DFCA (starting from the deterministic automaton that accepts the language U) exist, the best known algorithm [26] requires O(n log n) time, where ndenotes the number of states of the original automaton. For details about the construction of a minimal DFCA we refer the reader to [24] and [26]. A minimal DFCA of the language defined by Mk,k= 3, is M= (A, Q, q0, F, h), where A=Ak,Q={q0, q1, q2, q3},F=Qand hdefined by: h(qi−1, αi) = qi, 1≤i≤3 and h(q3, α4) = q0. Now, suppose we have a finite state model (automaton) of the system we want to test. In conformance testing one constructs a finite set of input sequences, called test suite, such that the implementation passes all tests in the test suite if and only if it behaves identically to the specification on any input sequence. Naturally, the implementation under test can also be modelled by an unknown deterministic finite automaton, say M0. This is not known, but one can make assumptions about it (e.g. that may have a number of incorrect transitions, missing or extra states). One of the least restrictive assumptions refers to its size (number of states). The W-method [12] assumes that the difference between the number of states of the implementation model and that of the specification has to be at most β, a nonnegative integer estimated by the tester. The W-method involves the selection of two sets of input sequences, a state cover Sand a characterization set W[12]. In our case, we have constructed a DFCA model of the system and we are only interested of the behavior of the system for sequences of length up to an upper bound k. Then, the set suite will only contain sequences of up to length k and its successful application to the implementation under test will establish that the implementation will behave identically to the specification for any sequence of length less then or equal to k. This situation is called conformance testing for bounded sequences. Recently, it was shown that the underlying idea of the W-method can also be applied in the case of bounded sequences, provided that 226 M. Gheorghe et al the sets Sand Wused in the construction of the test suite satisfy some further requirements; these are called a proper state cover and strong characterization set, respectively [23]. In what follows we informally define these two concepts and illustrate them on our working example. For formal definitions we refer the reader to [23] or [24]. Aproper state cover of a deterministic finite automaton M= (A, Q, q0, F, h) is a set of sequences S⊆A∗such that for every state q∈Q,Scontains a sequence of minimum length that reaches q. Consider Mthe DFCA in our example. Then λ is the sequence of minimum length that reaches q0,σ1is a sequence of minimum length that reaches q1,α1α2is a sequence of minimum length that reaches q2, α1α2α3is a sequence of minimum length that reaches q3. Furthermore, we can use any input symbol in A\ {α1}to reach the (implicit) “sink” state, for example α2. Thus, S={λ, α1, α1α2, α1α2α3, α2}is a proper state cover of M. Astrong characterization set of a minimal deterministic finite automaton M= (A, Q, q0, F, h) is a set of sequences W⊆A∗such that for every two distinct states q1, q2∈Q,Wcontains a sequence of minimum length that distinguishes between q1and q2. Consider again our running example. λdistinguishes between the (non-final) “sink” state and all the other (final) states. A transition labelled α1 is defined from q0, but not from q1,q2or q3, so α1is a sequence of minimum length that distinguishes q0from q1,q2and q3. Similarly, α2is a sequence of minimum length that distinguishes q1from q2and q3and α3is a sequence of minimum length that distinguishes between q2and q3. Thus W={λ, α1, α2, α3}is a strong characterization set of M, Once we have established the sets Sand Wand the maximum number βof extra states that the implementation under test may have, a test suite is constructed by extracting all sequences of length up to kfrom the set S(A0∪A1∪. . . ∪Aβ)W, where Aidenotes the set of input sequences of length i≥0. Note that some test sequences may be accepted by the DFCA model - these are called positive tests - but some others may not be accepted (they end up in the (non-final) “sink” state) - these are called negative tests. 7 Conclusions In this paper, we have investigated the relationships between kP systems, on the one hand, and active membrane systems with polarization and symport/antiport membrane systems, on the other hand. We have also illustrated the modeling power of kP systems by providing a number of kP system models for sorting algorithms. We have also discussed the problem of testing systems modelled as kernel P systems and proposed a test generation method based on automata. Namely, we have outlined how the kP systems can be tested using automata based Kernel P Systems Modelling, Testing and Verification 227 testing methods. Furthermore, we have shown how formal verification can be used to validate that the given models work as desired. We have also begun a study on the ability of kP aytems to simulate other particular classes of P systems, We have presented here the case of P systems with active membranes, and P systems with symport/antiport rules. In future studies we aim to connect kP systems with other classes of P systems, especially those utilised in various applications, and to show how other problems can be solved, tested and verified by using kP systems. Acknowledgements. MG and SK acknowledge the support provided for synthetic biology research by EPSRC ROADBLOCK (project number: EP/I031812/1). The work of FI and MG were supported by a grant of the Romanian National Authority for Scientific Research, CNCS-UEFISCDI (project number: PN-II-ID-PCE-2011-3-0688). References 1. A. Alhazov, D. Sburlan, Static Sorting Algorithms for P Systems, Pre-Proc. 4th Workshop on Membrane Computing (A. Alhazov et al., eds.), GRLMC Rep. 28/03, Tarragona, 17 – 40, 2003. 2. A. Alhazov, D. Sburlan, Static Sorting P Systems. In [14], 215 – 252, 2006. 3. J.J. Arulanandham, Implementing Bead-Sort with P Systems, Unconventional Models of Computation (C.S. Calude et al., eds.), Lecture Notes in Computer Science, 2509, 115–125, 2002. 4. C. Cˆampeanu, N. Santean, S. Yu. Minimal Cover-Automata for Finite Languages, Workshop on Implementing Automata (J.-M. Champarnaud et al., eds.), Lecture Notes in Computer Science, 1660, 43 – 56, 1998. 5. C. Cˆampeanu, N. Santean, S. Yu. Minimal Cover-Automata for Finite Languages. Theoretical Computer Science, 267(1-2), 3 – 16, 2001. 6. R. Ceterchi, C. Mart´ın-Vide, P Systems with Communication for Static Sorting. In Pre-Proc. 1st Brainstorming Week on Membrane Computing (M. Cavaliere et al., eds.), Technical Report no 26, Rovira i Virgili Univ., Tarragona, 101 – 117, 2003. 7. R. Ceterchi , C. Mart´ın-Vide, Dynamic P Systems, Proc. 4th Workshop on Membrane Computing (Gh. P˘aun et al., eds.), Lecture Notes in Computer Science, 2597, 146 – 186, 2003. 8. R. Ceterchi, M.J. P´erez-Jim´enez, A.I. Tomescu, Simulating the Bitonic Sort Using P Systems, Proc. 8th Workshop on Membrane Computing (G. Eleftherakis et al., eds.), Lecture Notes in Computer Science, 4860, 172 – 192, 2007. 9. R. Ceterchi, M.J. P´erez-Jim´enez, A.I. Tomescu, Sorting Omega Networks Simulated With P Systems: Optimal Data Layouts, (D. Diaz-Pernil et al., eds.), Pre-Proc. 6th Brainstorming Week on Membrane Computing,RGNC Rep. 01/08, F´enix Editora, pp. 79 – 92, 2008. 10. R. Ceterchi, A. I. Tomescu, Implementing Sorting Networks with Spiking Neural P Systems, Fundamenta Informaticae, 87(1), 35 – 48, 2008. 228 M. Gheorghe et al 11. R. Ceterchi, D. Sburlan, Membrane Computing and Computer Science, Chapter 22 of [29], 553–583, 2010. 12. T. S. Chow Testing Software Design Modeled by Finite-State Machines. IEEE Transactions on Software Engineering, 4(3), 178 – 187, 1978. 13. A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, A. Tacchella, NuSMV Version 2: An Open Source Tool for Symbolic Model Checking, Proc. International Conference on Computer-Aided Verification (CAV 2002), (W.A. Hunt, Jr and F. Somenzi, eds.), Lecture Notes in Computer Science, 2404, 359 – 364, 2002. 14. G. Ciobanu, Gh. P˘aun, M. J. P´erez-Jim´enez, eds., Applications of Membrane Computing, Springer, 2006. 15. M. Gheorghe, F. Ipate. On Testing P Systems, Proc. 9th Workshop on Membrane Computing, (D.W. Corne et al., eds.), Lecture Notes in Computer Science, 5391, 204 – 216, 2009. 16. M. Gheorghe, F. Ipate, C. Dragomir, Kernel P Systems, Pre-proc. 10th Brainstorming Week on Membrane Computing, (M. A. Mart´ınez-del-Amor et al., eds.), F´enix Editora, Universidad de Sevilla, 153 – 170, 2012. 17. M. Gheorghe, F. Ipate, C. Dragomir, L. Mierl˘a, L. Valencia-Cabrera, M. Garc´ıa- Quismondo, M.J. P´erez-Jim´enez, Kernel P Systems – Version 1, Pre-Proc. 11th Brainstorming Week on Membrane Computing, (L. Valencia-Cabrera et al., eds.), F´enix Editora, Universidad de Sevilla, 97 – 124, 2013. 18. M. Gheorghe, F. Ipate, S. Konur, Kernel P Systems and Relationships with other Classes of P Systems, Multidisciplinary Creativity, (M. Gheorghe et al., eds.), Spandugino Publishing House, 64 – 76, 2015. 19. M. Gheorghe, F. Ipate, R. Lefticaru, M.J. P´erez-Jim´enez, A. T¸urcanu, L. Valencia- Cabrera, M. Garc´ıa-Quismondo, L. Mierl˘a, 3-COL Problem Modelling Using Simple kernel P Systems, International Journal of Computer Mathematics, 90(4), 816 – 830, 2013. 20. M. Gheorghe, Gh. P˘aun, M.J. P´erez-Jim´enez, G. Rozenberg, Research Frontiers of Membrane Computing: Open Problems and Research Topics, International Journal of Foundations of Computer Scienve, 24, 547 – 624, 2013. 21. M. Gheorghe, S. Konur, F. Ipate, L. Mierl˘a, M. E. Bakir, M. Stannett, An Integrated Model Checking Toolset for Kernel P Systems, Proc. 16th Conference on Membrane Computing, (G. Rozenberg et al., eds.), Lecture Notes in Computer Science, 9504, 153 – 170, 2015. 22. G. J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, 23(5), 275 – 295, 1997. 23. F. Ipate, Bounded Sequence Testing from Deterministic Finite State Machines, Theoretical Computer Science, 411(16-18), 1770 – 1784, 2010. 24. F. Ipate, M. Gheorghe. Finite State Based Testing of P Systems, Natural Computing, 8(4), 833 – 846, 2009. 25. D.E. Knuth, The Art of Computer Programming, vol. 3, Sorting and Searching, Addison-Wesley, 1973. 26. H. K¨orner. On Minimizing Cover Automata for Finite Languages in O(n log n) Time, Proc. 7th Conference on Implementation and Application of Automata, (J.-M. Champarnaud and D. Morel, eds.), Lecture Notes in Computer Science, 2608, 117 – 127, 2002. 27. Gh. P˘aun, Computing with Membranes, Journal of Computer and System Sciences, 61(1), 108 – 143, 2000. Kernel P Systems Modelling, Testing and Verification 229 28. Gh. P˘aun, Membrane Computing - An Introduction, Springer, 2002. 29. Gh. P˘aun, G. Rozenberg, A. Salomaa, eds., The Oxford Handbook of Membrane Computing, Oxford University Press, 2010. 30. D. Sburlan, A Static Sorting Algorithm for P Systems with Mobile Catalysts, Analele S¸tiint¸ifice Universitatea Ovidius Constant¸a, 11(1), 195 – 205, 2003.