kPWorkbench: A Software Framework for Kernel P Systems

kPWorkbench: A Software Framework for Kernel P Systems Marian Gheorghe1, Florentin Ipate2, Laurentiu Mierla2, and 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] Summary. Psystems are the computational models introduced in the context of membrane computing, a computational paradigm within the more general area of unconventional computing. Kernel P (kP) systems are defined to unify the specification of different variants of P systems, motivated by challenging theoretical aspects and the need to model different problems. In this paper, we present kPWorkbench, a software framework developed to support kP systems. kPWorkbench integrates several simulation and verification tools and methods, and provides a software suit for the modelling and analysis of membrane systems. 1 Introduction Membrane computing is a computational paradigm, within the more general area of unconventional computing [24], inspired by the structure and behaviour of the eukaryotic cell. The formal models introduced in this context are called membrane systems or P systems. After their introduction [22], membrane systems have been widely investigated for computational properties and complexity aspects, but also as a model for various applications [23]. The introduction of different variants of P systems has been motivated by challenging theoretical aspects, but also by the need to model different problems. An account of the theoretical developments is presented in [23], a set of general applications can be found in [6], whereas specific applications in systems and synthetic biology are provided in [11] and some of the future challenges are presented in [14]. More recently, applications in optimisations and graphics [16] and synchronisation of distributed systems [9] have been developed. Several variants of P systems have been introduced and studied to model and analyse different problems, e.g., systems and synthetic biology [11], synchronisation of distributed systems [9], optimisations and graphics [16]. While the introduction of new variants allowed modelling different sets of problems, the ad-hoc addition 180 M. Gheorghe et al. of new features has caused an abundance of P system variants, with a lack of a coherent integrating view, and well-defined framework would allow us to analyse, verify and validate the system behaviour. We introduced kernel P systems (kP systems) [15] as an attempt to target these issues and create more general membrane computing models, integrating the most used concepts from P systems. A revised version of the model and the specification language can be found in [12] and its usage to specify the 3-colouring problem and a comparison to another solution provided in a similar context [8], is described in [13]. The kP systems have been also used to specify and analyse, through formal verification, synthetic biology systems [21, 20]. We have previously studied the theoretical aspects [15] and the verification and simulation techniques developed for kP systems [10, 3, 2]. In this paper, we present kPWorkbench (available and can be downloaded from its website http://www.kpworkbench.org), a software framework developed to support the analysis of kP systems. kPWorkbench integrates several simulation and verification tools and methods. The framework also facilitates verification by incorporating a property language based on natural language statements, which makes the property specification a very easy task. These features make kPWorkbench the only available tool supporting the non-probabilistic analysis of membrane systems through simulation and verification. The usability and novelty of our approach have been illustrated by some case studies [21, 20] chosen from synthetic biology (a new and emerging branch of biology that aspires to the engineering of new biological systems). The paper is organised as follows: in Section 2 are introduced the key concepts and definitions related to kP systems; the kPWorkbench is discussed in Section 3; in Section 4 are summarised some kP systems applications; Section 5 illustrates through some examples the use of the kPWorkbench platform and final conclusions are provided in Section 6. 2 Kernel P Systems A kP system is made of compartments placed in a graph-like structure. A compartment Cihas a type ti= (Ri, σi), ti∈T, where Trepresents the set of all types, describing the associated set of rules Riand the execution strategy that the compartment may follow. Note that, unlike traditional P system models, in kP systems each compartment may have its own rule application strategy. The following definitions are largely from [15]. Definition 1. Akernel P (kP) system of degree nis a tuple kΠ = (A, µ, C1, . . . , Cn, i0), where Ais a finite set of elements called objects;µdefines the 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 Software Framework for Kernel P Systems 181 a compartment type from Tand an initial multiset,wiover A;i0is the output compartment where the result is obtained. Each rule rmay have a guard gdenoted as r{g}. The rule ris applicable to a multiset wwhen its left hand side is contained into wand gholds for w. The guards are constructed using multisets over Aand relational and Boolean operators. For example, rule r:ac →c{≥ a3∧ ≥ b2∨ ¬ > c}can be applied iff the current multiset, w, includes the left hand side of r, i.e., ac and the guard holds for wit has at least 3 a0s and 2 b0s or no more than a c. A formal definition may be found in [15]. Definition 2. A rule associated with a compartment type lican 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∈Aand tj indicates a compartment type from T– see Definition 1 – with instance compartments linked to the current compartment; tjmight indicate the type of the current compartment, i.e., tli– in this case it is ignored; if a link does not exist (the two compartments are not 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 li, then one of them will be non-deterministically chosen; (b) structure changing rules; the following types are considered: (b1) membrane division rule: [x]tli→[y1]ti1. . . [yp]tip{g}, where x∈A+and yjhas the form yj= (aj,1, tj,1). . . (aj,hj, tj,hj)like in rewriting and communication rules; the compartment liwill be replaced by pcompartments; the j-th compartment, instantiated from the compartment type tij contains the same objects as li, but x, which will be replaced by yj; all the links of liare inherited by each of the newly created compartments; (b2) membrane dissolution rule: [x]tli→λ{g}; the compartment liand its entire contents is destroyed together with its links. This contrasts with the classical dissolution semantics where the inner multiset is passed to the parent membrane - in a tree-like membrane structure; (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 tljexists then one of them will be non-deterministically picked up; gis a guard that refers to the compartment instantiated from the compartment type tli; (b4) link destruction rule: [x]tli−[]tlj→[y]tli; []tlj{g}; is the opposite of link creation and means that the compartments are disconnected. Each compartment can be regarded as an instance of a particular compartment type and is therefore subject to its associated rules. One of the main distinctive features of kP systems is the execution strategy which is now statutory to types 182 M. Gheorghe et al. rather than unitary across the system. Thus, each membrane applies its type specific instruction set, as coordinated by the associated execution strategy. An execution strategy can be defined as a sequence σ=σ1&σ2&. . . &σn, where σidenotes an atomic component of the form: •, an analogue to the generic skip instruction; is generally used to denote an empty execution strategy; •r, a rule from the set Rt(the set of rules associated with type t). If ris applicable, then it is executed, advancing towards the next rule in the succession; otherwise, the compartment terminates the execution thread for this particular computational step and thus, no further rule will be applied; •(r1, . . . , rn), with ri∈Rt,1≤i≤nsymbolizes a non-deterministic choice within a set of rules. One and only one applicable rule will be executed if such a rule exists, otherwise the atom is simply skipped. In other words the non-deterministic choice block is always applicable; •(r1, . . . , rn)∗, with ri∈Rt,1≤i≤nindicates the arbitrary execution of a set of rules in Rt. The group can execute zero or more times, arbitrarily but also depending on the applicability of the constituent rules; •(r1, . . . , rn)>, ri∈Rt,1≤i≤nrepresents the maximally parallel execution of a set of rules. If no rules are applicable, then execution proceeds to the subsequent atom in the chain. The execution strategy itself is a notable asset in defining more complex behaviour at the compartment level. For instance, weak priorities can be easily expressed as sequences of maximally parallel execution blocks: (r1)>&(r2)>&. . . &(r3)> or non-deterministic choice groups if single execution is required. Together with composite guards, they provide an unprecedented modelling fluency and plasticity for membrane systems. Whether such macro-like concepts and structures are preferred over traditional modelling with simple but numerous compartments in complex arrangements is a debatable aspect. The kP system models are described in a machine readable language, called kP–Lingua [10]. Below, we illustrate the kP systems concepts on an example, which is slightly adjusted from [10, 2]. Example 1. A type definition in kP–Lingua. type C1 { choice { > 2b : 2b -> b, a(C2) . b -> 2b . } } type C2 { choice { a -> a, {b, 2c}(C1) . } } m1 {2x, b} (C1) - m2 {x} (C2) . A Software Framework for Kernel P Systems 183 Above, C1,C2 denote two compartment types, which are instantiated as m1,m2, respectively. m1 starts with the initial multiset 2x,band m2 starts with x. The rules of C1 are chosen non-deterministically, only one at a time – this is achieved by the use of the key word choice. The first rule is fired only when its guard becomes true; in other words, only when the current multiset has at least three b’s. This rule also sends an ato the instance of C2 that is linked. In the type C2, there is only one rule to be fired, which happens only when there is an ain the compartment C1. 3 kPWorkbench kPWorkbench is an integrated software suit developed to provide a tool support for kP systems. kPWorkbench employs a set of tools and methods, allowing one to model membrane systems and to analyse them through simulation and verification. In the following, we briefly discuss some features of the software framework. 3.1 Features Modeling. kPWorkbench accepts kP system models specified in an intuitive modelling language, kP–Lingua. kP systems accumulate the most important aspects of various P system variants, so kP–Lingua provides a generic language to model various membrane systems. kPWorkbench features a graphical model editor, permitting to create new model files and editing existing files. The grammar of the kP–Lingua language is written in ANTLR (ANother Tool for Language Recognition) [1], automatically generating the necessary syntactic and semantic analysers. ANTLR also constructs the data structures that represent the corresponding abstract syntax tree (AST) together with a traversing functionality. Simulation. kPWorkbench offers two different approaches to simulate kP systems. In both approaches, a kP–Lingua model is provided as an input, and the execution traces of the model are returned as an output. These traces permit exploring the dynamics of the system and observing how the system evolves over time. In the first approach, we have developed a custom simulation tool [3], which recreates the system dynamics as a set of simulation runs. The tool translates a kP– Lingua specification into an internal data structure, which permits representing compartments, containing multisets of objects and rules, and their connections with other compartments. In the second approach, we have integrated the Flame simulator [7], a general purpose large scale agent based simulation environment. Flame is based on the X- machine formalism [17], a type of extended finite state machine whose transitions 184 M. Gheorghe et al. Prop. Pattern Lang. Construct LTL formula CTL formula Next next pXpEX p Existence eventually pFpEF p Absence never p¬(F p)¬(EF p) Universality always pGpAG p Recurrence infinitely-often pG F pAG EF p Steady-State steady-state pF G pAF AG p Until puntil q p UqA (pUq) Response pfollowed-by qG (p→Fq) AG (p→EF q) Precedence ppreceded-by q¬(¬pU (¬p∧q)) ¬(E (¬pU (¬p∧q))) Table 1: Some property patterns defined in kP–Queries and the LTL and CTL translations. Note that LTL implicitly quantifies universally over paths (i.e. “necessity”). To complement this semantics, in CTL we translate some formulas by assuming quantification over some paths (i.e. “possibility”). are labelled by processing functions that operate on a (possibly infinite) set called memory, that models the system data. Flame has been successfully used in various applications, ranging from biology to macroeconomics. In order to simulate kernel P system models using the Flame framework, an automated model translation has been implemented for converting the kP–Lingua specification into communicating X-machines [17]. One of the main advantages of this approach is the high scalability degree and efficiency for simulating large scale models. Verification. Although there have been some efforts to apply formal verification, in particular model checking, methods and methodologies for various P systems (e.g., [19, 4]), utilising a comprehensive, integrated and automated verification approach is a very challenging task in the context of membrane computing. For example, it is very difficult to transform some complex features, e.g. membrane division, dissolution and link creation/destruction, into suitable abstractions in model checking tools. We have successfully addressed these issues, and developed a verification environment [10, 2] for kPWorkbench, integrating some state of the art model checking tools, e.g. the Spin [18] and NuSMV [5]. The translations from a kP–Lingua representation to the corresponding Spin and NuSMV inputs (i.e. Promela and Smv, respectively) are automatically performed. In order to facilitate the property specification task, kPWorkbench features a property language, kP–Queries, based on natural language statements. The language also provides a list of property patterns (templates), generated from most commonly used queries (see Table 1). The property language permits specifying the target logic (i.e. LTL and CTL) for different properties without placing a requirement on a specific model checker. In this way, we can use the same set of properties in various verification experiments. A Software Framework for Kernel P Systems 185 3.2 System architecture Fig. 1: The overview architecture of kPWorkbench framework Figure 1 depicts an overview of the kPWorkbench system architecture, which consists of three modules: 1. The kernel P (kP) module takes a kP system model specified in kP–Lingua, which can be created or edited using a dedicated model editor, as input. The kP– Lingua module parses the input file and validates its syntax via ANTLR (which generates the necessary syntactic and semantic analysers). The kP–Model module accommodates the corresponding data structures of the input model, comprising compartment types, execution strategies, rules, multiset of objects and connections between compartments. The kP–Lingua module instantiates a kP–Model object and maps the AST generated by ANTLR to that object. This object is used as Data Transfer Object (DTO) between different modules of the framework. This separation helps developers to easily add new components to the framework. 2. The Simulation module consists of two components, kPWorkbench Simulator and Flame Translator. Both require the kP–Model object and simulator parameters, e.g. number of steps, as input. The kPWorkbench Simulator component is a custom simulator, which processes the multisets of objects of the input model with respect to its execution strategies and rules. The Flame Translator transforms the kP–Model object into a Flame Model object that aggregates agent, function, input, condition and output classes. It assigns each compartment to an agent, and the rules and the multiset of objects are stored as agent data. It creates a specific function for each type of execution strategy. In addition it creates C functions that represent the system behaviour (they are executed by Flame 186 M. Gheorghe et al. when the agent makes a transition from one state to another). The Flame Translator uses the ANTLR template group feature to produce the Flame simulator specifications from the Flame Model object. 3. The Verification module contains three components: the Spin and NuSMV translators and the kP–Queries module: The Spin Translator has two main components: Translator and Promela (Spin’s specification language). The Promela component aggregates the Promela language specifications: MType,Array,Do statement,If statement,Init, etc. The Translator maps the kP–Model object to a Promela object using the following procedure [10]: (i) A compartment type is translated into a data type definition with the multiset of objects and links to other compartments, and also with temporary storage variables that provide the parallelism of P systems. (ii) Multiset of objects is assigned to an integer array where an index denotes the object and its value represents the multiplicity of the object. (iii) The set of rules are organised according to the execution strategies mapped by a Proctype definition – a Promela process. (iv) Maximal parallelism and arbitrary execution strategies are mapped to the Do statement, and choice execution strategy is mapped to If statement. After the mapping process, the Translator component translates the Promela object to the corresponding Promela model, used by the Spin model checker. However, this translation is not simple and straightforward, especially the structure changing rules, and arbitrary and maximal parallelism execution strategies complicate the translation process. More details about the translation from kP System model to the Spin model checker specification can be found in [10]. Similarly, the NuSMV Translator translates the kP–Model object to the corresponding NuSMV representation (NuSMV’s specification language). The translator has two main components: Translator and NuSMV. The NuSMV component consists of subcomponents representing the NuSMV language objects, such as module,variables,INVARs,Case Statements,Conditions, and logical connectives. The Translator maps the kP–Model object to the NuSMV object as follows: (i) Each compartment is translated into a module. (ii) The content of compartments is translated into variables. (iii) The initial multisets of the compartment are assigned into module parameters. (iv) Rules and guards are translated into the case statements. (v) The behaviour of execution strategies and the parallelism of P systems are achieved by introducing custom variables. After the mapping process, the Translator component generates the NuSMV model from the NuSMV object, which is then provided as input to the NuSMV model checker. During the mapping process, we have overcome a few challenging domain specific restrictions. For example, unlike Promela, NuSMV has restrictions on defining arrays, and only allows accessing a value of array by a symbolic constant index; but it does not allow assigning a value by a symbolic constant. Therefore, instead of using arrays, we created a variable for each multiset of objects. Also, in Promela, we can non-deterministically pick a true statement among branches when there are more than one true statements; whereas, in NuSMV the selections are only deterministic. It always chooses the first true statement from a list of A Software Framework for Kernel P Systems 187 conditions. We overcome that issue by introducing an INVAR declaration whenever a non-determinism behaviour is required. The kP–Queries module receives a property, natural language based statements, as input. The user can build properties from the property language editor. The editor interacts with the kP–Lingua model, and permits accessing the native model elements, which simplifies the property building process. The kP– Queries’ domain language has its own grammar, which is independent from and much simpler than the target model checking languages. The DSL (domain specific language) of the property language is written in ANTLR, receiving the EBNF grammar as input and generates the corresponding syntactic and semantic analysers as well as the corresponding AST. In order to simplify the traversal of the AST, we adapt a strategy, which maps the AST to a better structured internal data representation. To traverse between the elements of the internal data structure (a tree-like hierarchy), we follow the Visitor design pattern. Namely, the internal data nodes are treated as visitable entities, which are able to accept visitors and request to visit them. Each visitor has a specific functionality for visiting every single node. The visitor design pattern approach enables the kP–Queries module to translate every node of the internal presentation of property into the target model checker’s corresponding property specification language. 4 Applications Although membrane computing is mainly inspired from biology, its application to biological systems has been very limited due to the lack of a coherent and welldefined framework that allows us to analyse, verify and validate these systems. The methods and methodologies we have developed in [15, 10, 3, 2] to tackle these issues have filled an important gap in this respect. kPWorkbench, implementing these methodologies and algorithms, now provides a fully automated tool support, facilitating the modelling and analysis of biological systems through simulation and verification. The usability and novelty of our approach has already been illustrated in some well-known case studies, chosen from systems and synthetic biology. In [21], we showed how our approach utilises the non-deterministic analysis of two biological systems, the quorum sensing in P. aeruginosas (a bacterial pathogen) and the synthetic pulse generator. Namely, we used our approach to observe various phenomena in genetic regulatory networks, e.g. various interactions between molecular species and various dependencies between molecules. Likewise, in [20], we showed how our approach can be used to formally analyse unconventional programs, e.g. some genetic Boolean gates. We believe that our methods and techniques, and hence the kPWorkbench platform, provide significant contributions to the membrane & unconventional computing communities.