Formal Verification of P Systems with Active Membranes through Model Checking

Formal Verification of P Systems with Active Membranes through Model Checking Florentin Ipate1, Raluca Lefticaru1, Ignacio P´erez-Hurtado2, Mario J. P´erez-Jim´enez2, and Cristina Tudose1 1Department of Computer Science, University of Pitesti Str. Targu din Vale 1, 110040, Pitesti, Romania {florentin.ipate,raluca.lefticaru,cristina.tudose}@upit.ro 2Research Group on Natural Computing Dpt. of Computer Science and Artificial Intelligence, University of Sevilla Avda. Reina Mercedes s/n. 41012, Sevilla, Spain {perezh,marper}@us.es Abstract. Formal verification of P systems using model checking has attracted a significant amount of research in recent years. However, up to now only P systems with static structure have been considered. This paper makes significant advances in this area by considering P systems with active membranes, in particular P systems with division rules. The paper presents a theoretical framework for addressing this problem and reports on a complex case study involving a well-known NP-complete problem solved using P systems with membrane division rules. This is implemented in Promela and non trivial properties are verified using Spin. 1 Introduction Inspired by the behaviour and functioning of a living cell, membrane computing has emerged in recent years as a powerful modelling tool; various applications have been reported [4], especially in biology and bio-medicine, but also in many other areas, such as economics, approximate optimization and computer graphics [21]. Furthermore, software tools, such as P-Lingua [14], for simulating P systems, have been developed and used in real life problems. Naturally, such modelling and simulation tools must be accompanied by appropriate means of formally verifying that the model satisfies the required properties. One of the most widely used approaches to formal verification is through model checking. This uses a model of the implementation, given as an operational specification, and a specification, given as a temporal logic formula, and verifies, on the entire state space of the model, whether the property holds or not. If the property fails, then a counterexample is also returned. Formal verification of P systems using model-checking has attracted a significant amount of research in recent years, using tools such as Maude [1], PRISM [22], NuSMV [13], Spin [7], [12] or ProB [10]. However, up to now only P systems with static structure have been considered. Some of the aforementioned investigations consider cell dissolution rules, but in this case a simple flag, indicating whether the membrane exists or not in the current configuration, can be used to address the change in the membrane structure. This is, indeed, a clear weakness of these approaches since, in biology, the membrane structure is not static, but it evolves and changes in time. Furthermore, P systems with active membranes have a wide range of applications; in particular, P systems with division rules are used to devise efficient solutions to computationally hard problems [21]. This paper makes significant advances in the area of model checking based verification of P systems by considering P systems with active membranes. Firstly, it devises a theoretical framework for addressing this problem: it describes the Kripke structure associated with a P system with active membranes and how this can be translated into an executable implementation; it also shows how properties that can be formulated for the P system can be translated into properties of the executable implementation. Secondly, it reports on a complex case study involving a well-known NP-complete problem solved in linear time and in an uniform way using P systems with membrane division rules [17]. The solution was improved in [8], where the total cost is logarithmic in one variable and linear in the rest, but this improvement is not essential in the context of this paper. For this example, a number of non-trivial properties of the model are formulated and verified using the Spin model checker [2]. The paper is structured as follows. We start by presenting in Section 2 the notation and main concepts to be used in the paper. Section 3 presents the theoretical background for our approach. The case study and empirical results are given in the next two sections, while Section 6 discusses related work. Finally, conclusions are drawn in Section 7. 2 Background 2.1 P Systems Before presenting our approach to P system verification, let us establish the notation used and define the class of cell-like P systems addressed in the paper. Basically, a P system is defined as a hierarchical arrangement of membranes, identifying corresponding regions of the system. Each region has an associated finite multiset of objects and a finite set of rules; both may be empty. Given a finite alphabet V={a1, ..., ap},amultiset is either denoted by a string u∈ V∗(in which the order is not important, the string notation is only used as a convention), or by an associated vector of non-negative integers, ΨV(u)= (|u|a1, ..., |u|ap), where |u|aidenotes the number of aioccurrences in u,foreach 1≤i≤p. The following definition refers to cell-like P systems with active membranes (see [19, 20] or [21] page 284, for details). Definition 1. APsystemis a tuple Π=(V,H,μ,w1,...,w n,R),whereVis a finite set, called alphabet;His a finite set of labels for membranes; μis a membrane structure (a rooted tree), consisting of nmembranes injectively labelled with elements of H;wi,1≤i≤n, are strings over V, describing the multisets of objects initially placed in the nregions of μ;Risafinitesetofrules,where each rule is of one of the following forms: (a) [a→v]α h,whereh∈H,α∈{+,−,0}(electrical charges), a∈Vand vis a string over Vdescribing a multiset of objects associated with membranes and depending on the label and the charge of the membranes (evolution rules). (b) a[]α h→[b]β h,whereh∈H,α, β ∈{+,−,0},a, b ∈V(send-in communication rules). An object is introduced in the membrane, possibly modified, and the initial charge αis changed to β. (c) [a]α h→[]β hb,whereh∈H,α, β ∈{+,−,0},a, b ∈V(send-out communication rules). An object is sent out of the membrane, possibly modified, and the initial charge αis changed to β. (d) [a]α h→b,whereh∈H,α∈{+,−,0},a, b ∈V(dissolution rules). A membrane with a specific charge is dissolved in reaction with an object a (possibly modified). (e) [a]α h→[b]β h[c]γ h,whereh∈H,α, β, γ ∈{+,−,0},a, b, c ∈V(division rules). A membrane is divided into two membranes. The objects inside the membrane are replicated, except for a, that may be modified in each membrane. The membrane structure, μ, is denoted by a string of left and right brackets ([l and ]e l), each with the label lof the membrane; the electrical charge eof each membrane is also given. The environment is only used to send the answer to and we do not capture its structure into this definition. The rules are applied in maximally parallel mode, which means that they are used in all the regions at the same time and in each region all the objects to which arulecan be applied must be the subject of a rule application [19]. However, any membrane can be subject of only one rule of types (b) – (e) in one computation step. In type (e) (membrane division) rules, all the contents present before the division, except for object a, can be the subject of rules in parallel with the division. In this case we consider that in a single step two processes take place: first the contents are affected by the rules applied to them, and after that the results are replicated into the two new membranes. If a membrane is dissolved, its content (multiset and interior membranes) becomes part of the immediately external membrane which has not been dissolved at that computation step. The skin is never dissolved neither divided. The behaviour of this system is precisely the same as the behaviour mentioned in [15–17], [19–21]. Aconfiguration of the P system Πis uniquely identified by the current membrane structure μand the contents of each region in μ. A transition step from a configuration c1to a configuration c2is realized if the P system can evolve from c1to c2by using the maximal parallelism mode (as well as the rule restrictions stated above); this is denoted by c1=⇒c2. In the set of all configurations, we will distinguish halting configurations; cis a halting configuration if there is no region isuch that its contents can be further developed. 2.2 Linear Temporal Logic The Linear Temporal Logic (LTL) was introduced by Amir Pnueli in 1977 [18] for the verification of computer programs. Compared to CTL (Computation Tree Logic) [5], LTL does not have an existential path quantifier (the Eof CTL). An LTL formula has to be true over all paths, having the form Af,wherefis a path formula in which the only state subformulas permitted are atomic propositions. Given a set of atomic propositions AP , an LTL path formula [5] is either: –If p∈AP ,thenpis a path formula. –If fand gare path formulas, then ¬f,f∨g,f∧g,Xf,Ff,Gf,fUgand fRgare path formulas, where: •The Xoperator (“neXt time”, also written ) requires that a property holds in the next state of the path. •The Foperator (“eventually” or “in the future”, also written ♦)isused to assert that a property will hold at some state on the path. •Gf(“always” or “globally”, also written ) specifies that a property, f, holds at every state on the path. •fUgoperator (Umeans “until”) holds if there is a state on the path where gholds, and at every preceding state on the path, fholds. This operator requires that fhas to hold at least until g, which holds at the current or a future position. •R(“release”) is the logical dual of the Uoperator. It requires that the second property holds along the path up to and including the first state where the first property holds. However, the first property is not required to hold eventually: if fnever becomes true, gmust remain true forever. 3 Theoretical Basis for Model Checking of P Systems with Active Membranes In this section we describe the transformation of a P system with active membranes into a Kripke structure, by extending the approach given in [7] and [11] for P systems with static structure. Definition 2. A Kripke structure over a set of atomic propositions AP is a four tuple M=(S, H, I, L),whereSis a finite set of states; H⊆S×Sis a transition relation that must be left-total, that is, for every state s∈Sthere is a state s∈Ssuch that (s, s)∈H;I⊆Sis a set of initial states; L:S−→ 2AP is an interpretation function, that labels each state with the set of atomic propositions true in that state. Usually, the Kripke structure representation of a system results by giving values to every variable in each configuration of the system. Suppose var1,...,var kare the system variables, Val idenotes the set of values for variand valiis a value from Val i,1≤i≤k. Then the states of the system are S={(val1,...,val k)| val1∈Val 1,...,val k∈Val k}, and the set of atomic predicates are AP ={(vari=vali)|1≤i≤k,vali∈Val i}. Naturally, Lwill map each state (given by the values of variables) onto the corresponding set of atomic propositions. For convenience, in the sequel the expressions of AP and Lwill not be explicitly given, the implication being that they are defined as above. Obviously, in a P system with division rules the number of membranes can grow infinitely. For practical reasons, we will allow only a finite number of membranes and will assume that the upper bound kon this number is known beforehand. However, this is not a limitation because, given a specific P system, this upper bound can be estimated. Then, a configuration of a P system can be represented by a tuple c=(var1,...,var k), where variholds the current contents uiof region i(a special symbol not in Vwill be used when the ith membrane does not exist), the membrane label, its electrical charge and the number of the parent membrane. Consider a P system Π=(V,H,μ,w1,...,w n,R) with R={r1,...,r m}.The states of the Kripke structure associated with Πwill correspond to the configurations of the P system (plus two special states, as explained later). Given two configurations, cand d, there is a transition from cto dif for every membrane iin cthere exist ni 1,...,n i m, such that the following conditions hold simultaneously: –At least one rule is applied, i.e. there exists isuch that ni 1+...+ni m>0; –dis obtained from cby applying rules r1,...,r m,ni 1,...,n i mtimes, respectively, for every membrane i; –Any membrane can be subject of only one rule of type (b) – (e), i.e. for every i, there exists at most one j,1≤j≤m, such that ni j>0andrulerjis of type (b) – (e); furthermore, in this case ni j=1; –A computation from cdevelops in maximally parallel mode, i.e. for every membrane iand every j,1≤j≤m,ifrulesr1,...,r mcan be applied ni 1,...,n i j−1,(ni j+1),n i j+1 ...,n i mtimes, respectively, in cthen: (1) rjis of type (b)–(e) and (2) there exists l,1≤l≤msuch that rlis of type (b)–(e) and ni l=1. In order to keep the number of states finite, for each configuration uwe will assume that each component of ΨV(u) has an established upper bound, denoted Max, and each rule can only be applied for at most a given number of times, denoted Sup (therefore ni 1,...,n i m≤Sup in the above definition). Whenever (at least) one of these upper bounds is exceeded, extra transitions to a special state, Crash, are added. Consequently, as long as the verification is performed for “specific” P systems (and not for a class of P systems), then this upper bound is not a limiting factor. However, the upper bounds and the Crash state are added just to prevent an unexpected behaviour, caused by a P system with a misleading computation. The halting configurations of the P system (i.e. in which no rule can be applied) are also represented by extra transitions, to another special state, Halt.In order for the transition relation to be left-total, loop-back transitions in Crash and Halt are also added. One additional problem arises when implementing the Kripke structure defined above: most modelling languages (Promela included) do not support the Table 1. Reformulating the basic LTL operators for the Promela specification of a P system Property LTL specification Gp[] (p|| !pInS ) Fp<>(p&& pInS ) pUq(p|| !pInS)U(q&& pInS) XpX(!pInS U(p&& pInS)) pRq(p&& pInS )V(q|| !pInS ) existential (or the universal) quantifier. Consequently, a transition involving ∃ (as in the Kripke structure representation of a P system) is normally implemented as a sequence of transitions (e.g. a “do - od” loop in Promela) and so additional (intermediary) states are introduced into the model. Naturally, the intermediary states cannot be allowed to form infinite loops and so every possible path in the Promela executable model will contain infinitely often states corresponding to the P system configurations. These assumptions ensure that every path in the P system has at least one corresponding path in the Promela model and vice versa. Naturally, the properties to be verified (and which refer to the given P system) will need to be reformulated as equivalent formulas for the associated Promela model. Table 1 summarizes the transformations of basic LTL formulas for the Promela implementation, as formally proven in [12] (pInS is a predicate which holds in the original (non-intermediary) states). For example, ‘always b>0’ (the number of occurrences of bobjects is always greater than 0), will become, for the Promela model, ‘Globally b>0ornotpInS’ (we expect b>0only for configurations corresponding to the P system, but not for the intermediary states). 4 Case Study: The Subset Sum Problem The Subset Sum problem has been used with some classes of P systems with active membranes in order to illustrate the efficiency and power of these mechanisms for solving NP-complete problems in an uniform way ([8, 9, 15–17]). Most of these solutions follow a similar scenario with a number of stages: generation, calculation, checking and output. This is important for the approach we suggest as we can identify specific properties for some of these stages as well as global ones. The Subset Sum problem can be formulated as follows: Given a finite set A={a1,...,a n},of nelements, where each element ai has an associated weight, wi, and a constant k∈N, it is requested to determine whether or not there exists a subset B⊆Asuch that w(B)=k,wherew(B)= ai∈Bwi. For given nand k, a P system with active membranes Π(n, k) is constructed to solve the Subset Sum problem - for details see [17]. The P system is given by Π(n, k)=(Γ(n, k),{e, s},μ,w e,w s,R,i(n, k)),where –Γ(n, k)={x0,x 1,...,x n}∪{¯a0,¯a, a0,a,d 1,e 0,...,e n,q,q 0,...,q 2k+1, z0,...,z 2n+2k+2,Yes,No 0,No,#}is the alphabet; –μ=[ s[e]0 e]0 sis the membrane structure; –ws=z0,we=e0akare the initial multisets; –i(n, k)=eand contains the code xw1 1...x wn n; –the set of evolution rules, R, consists of (1) [ei]0 e→[q]− e[ei]+ e,0≤i≤n; [ei]+ e→[ei+1]0 e[ei+1]+ e,0≤i≤n−1. For each subset of Aamembrane is generated. (2) [x0→¯a0]0 e;[x0→λ]+ e;[xi→xi−1]+ e,for 1 ≤i≤n. The code from the input membrane is built in such a way that the multiplicity of xjrepresents the weight of aj∈A. These three rules calculates in ¯a0the weight of a subset. (3) [q→q0]− e;[¯a0→a0]− e;[¯a→a]− e. These rules mark the beginning of the checking stage; the weight of the subset is now coded by the multiplicity of a0. (4) [a0]− e→[]0 e#; [a]0 e→[]− e#. The number of occurrences of a0and aare compared in a checking loop. (5) [q2j→q2j+1]− e,0≤j≤k;[q2j+1 →q2j+2]0 e,0≤j≤k−1. Objects qiare utilised as counters of the checking loop. (6) [q2k+1]− e→[]0 eYes;[q2k+1]0 e→[]0 e#; [q2j+1]− e→[]− e#; 0 ≤j≤k−1. These rules provide an answer to the checking loop given that there are the same number of a0and a,morea0objects, or more aobjects, respectively. (7) [zi→zi+1]0 s,0≤i≤2n+2k+1;[z2n+2k+2 →d1No0]0 s. Objects zicontrol the checking stage in all membranes. When the checking stage is over d1and No0are released into the skin membrane. (8) [d1]0 s→[]+ sd1;[No0→No]+ s;[Yes]+ s→[]0 sYes;[No]+ s→[]0 sNo. In the final stage either Yesor No is sent out into the environment. 5 Experimental Results In the sequel we will show how different properties of the above P system, providing an answer to an instance of the Subset Sum problem, can be checked. We start with some simpler properties and then will focus on some more complex ones that have been revealed by the current literature [17]. Before starting the presentation of these properties it is important to mention that many of the properties require some transformations or adaptations in order to be checked and validated - as discussed in Section 3. We have considered different instances of the Subset Sum problem. We have considered a set Awith two and three elements, weights between one and three, Table 2. Some properties verified for the Promela specifications of two P systems, providing an answer to the Subset Sum problem Property LTL specification Result 1 Result 2 Generally, there is not YES in the environment. [ ](env.Yes == 0 || !pInS) false true Generally, there is not NO in the environment. [ ](env.No == 0 || !pInS) true false Eventually, there is YES in the environment. <>(env.Yes == 1 && pInS) true false Eventually, there is NO in the environment. <>(env.No == 1 && pInS) false true When e1appears in a specific membrane 1, with electrical charge 0, then a qwill appear with a negative electrical charge. [ ]( ( membr[1].e[1]==1 && membr[1].charge==0 -> <> (membr[1].q==1 && membr[1].charge==-1 && pInS)) || !pInS) true true When e1appears in a specific membrane 1, with electrical charge 0, then a qwill appear with a positive electrical charge. [ ]( ( membr[1].e[1]==1 && membr[1].charge==0 -> <> (membr[1].q==1 && membr[1].charge==1 && pInS)) || !pInS) false false For all i, j,ifeiappears in membrane j, with electrical charge 0, then qwill appear in the same membrane with a negative electrical charge. [ ]((i>=0 && i<3 && j>=0 && j<10 && (membr[j].e[i]==1 && membr[j].charge==0 -> <> (membr[j].q==1 && membr[j].charge==-1 && pInS))) ||!pInS) true true and values of kbetween two and four. We have tested both cases, with and without solution. In Table 2 we present some properties verified for the Promela specification of the P system. The first two columns express the properties to be verified and the last two columns the results obtained for two instances of the Subset Sum P systems. The first example is n=3,k =4,w =[1,2,2] and has the associated results in the third column, while the second example is n=3,k =3,w =[2,2,2 ] and the model checker answers are given in the last column of Table 2. We first checked whether there is a solution for a given instance of Subset Sum (“Generally, there is not NO in the environment”). As said above we had to slightly change the query due to the current codification of the P system into Promela and the associated Kripke structure. The current form of the query is [](env.No == 0 || !pInS), which means that we consider only states associated with the P system and not intermediary ones and check the variable No from the environment, env.No, to be 0. The same behaviour of the system can be checked by “Eventually, there is YES in the environment”. Based on rule of the type “(1)” it can be shown that when eiappears in a specific emembrane, or more generally, in any such membrane, with electrical charge 0, then in the membrane obtained from it with negative electrical charge, qwill appear. We have also made some experiments running simulations with both P-Lingua and the Promela code. The results obtained were the same (final configuration, number of steps, obtained membranes etc.) and the two simulations have produced values of the same order of magnitude regarding the elapsed time. This shows that the Kripke structure underlying the translation from P-Lingua to Promela does not introduce much overhead into the system. For the two instances of the Subset Sum P systems considered before, the maximum number of membranes obtained during the P system computation was 16 (corresponding to n= 3) and the verification time of each property listed in Table 2 was 7 −8 seconds. In future experiments we will test the limit for which Spin can produce a response in a reasonable time interval and will investigate how our implementation can be improved in order to cope with the well-known state explosion problem associated with model checking. We also aim to address more complex properties as well as to identify invariants of various stages. 6 Related Work A first approach on P system verification using model checking is introduced in [1]. The authors transform P systems into executable specifications written in Maude, a programming language and the software system developed around it, that uses a rewriting semantics. Further, the LTL model checker of Maude is used to verify some properties of the P systems. Other papers [6, 7] tackle the decidability problem of P system properties. The models used for experiments are, similarly to those in [1], simple cell-like P systems, generating for example n2. They present membrane dissolving rules, but no membrane division. The tools used for experimentation are Omega and Spin, the authors conclusion is that Spin is preferable over Omega for model checking P systems. Another paper that compares the experimental results obtained by two main stream model checkers is [12], which concludes that Spin achieves better performance than NuSMV for P system models. More details regarding the P system transformation into SMV, the language accepted by NuSMV, are given in [11, 13], which use the model checker counterexamples for test generation. In [22] the probabilistic model checker Prism is employed to verify a stochastic P system. The paper presents a case study representing the cell cycle in eukaryotes, described using a P system specification which is translated into Prism. Specific questions are then formulated and run against the Prism specification of the P system. Daikon, a dynamic invariant detector, has been used in a similar context to extract P systems properties, which were later validated by Prism [3].