No / Recent research in membrane computing examines and confirms the anticipated modelling potential of kernel P systems in several case studies. On the one hand, this computational model is destined to be an abstract archetype which advocates the unity and integrity of P systems onto a single formalism. On the other hand, this envisaged convergence is conceived at the expense of a vast set of primitives and intricate semantics, an exigent context when considering the development of simulation and verification methodologies and tools. Encouraged and guided by the success and steady progress of similar undertakings, in this paper we directly address the issue of formal verification of kernel P systems by means of model checking and unveil a software framework, kpWorkbench, which integrates a set of related tools in support of our approach. A case study that centres around the well known Subset Sum problem progressively demonstrates each stage of the proposed methodology: expressing a kP system model in recently introduced kP-Lingua; the automatic translation of this model into a Promela (Spin) specification; the assisted, interactive construction of a set of LTL properties based on natural language patterns; and finally, the formal verification of these properties against the converted model, using the Spin model checker.

No / In this short paper one overviews the two years development of kernel P systems (kP systems for short), a basic class of P systems combining features of different variants of such systems. The definition of kP systems is given, some examples illustrate various features of the model and the most significant results are presented.

Yes / A kernel P system integrates in a coherent and elegant manner some of the most successfully used features of the P systems employed in modelling various applications. It also provides a theoretical framework for analysing these applications and a software environment for simulating and verifying them. In this paper, we illustrate the modelling capabilities of kernel P systems by showing how other classes of P systems can be represented with this formalism and providing a number of kernel P system models for a sorting algorithm and a broadcasting problem. We also show how formal verification can be used to validate that the given models work as desired. Finally, a test generation method based on automata is extended to non-deterministic kernel P systems. / The work of MG, FI and RL were supported by a grant of the Romanian National Author- ity for Scientific Research, CNCS-UEFISCDI (project number: PN-II-ID-PCE-2011-3-0688); RCUK

No / Kernel P systems integrate in a coherent and elegant manner many of the features of different P system variants, successfully used for modelling various applications. In this paper, we present our initial attempt to extend the software framework developed to support kernel P systems: a formal verification tool based on the NuSMV model checker and a large scale simulation environment based on FLAME. The use of these two tools for modelling and analysis of biological systems is illustrated with a synthetic biology example.

No / The paper presents the use of a membrane computing model for specifying a synthetic biology pulse generator example and discusses some simulation results produced by the tools associated with this model and compare their performances. The results show the potential of the simulation approach over the other analysis tools like model checkers.

Yes / P colonies, tissue-like P systems with very simple components, have received constant attention from the membrane computing community and in the last years several new variants of the model have been considered. Another P system model, namely kernel P system, integrating the most successfully used features of membrane systems, has recently attracted interest and some important developments have been reported. In this paper we study connections among several classes of P colonies and kernel P systems, by showing how the behaviour of these P colony systems can be represented as kernel P systems. An example illustrates the way it is modelled by using P colonies and kernel P systems and some properties of it are formally proved in the latter approach. / Grant No. K 120558 of the NKFIH—National Research, Development, and Innovation Office, Hungary; Romanian National Authority for Scientific Research, CNCS-UEFISCDI (Project No. PN-III-P4-ID-PCE-2016-0210).

Yes / Structural and behavioural properties of models are very important in development of complex systems and applications. In this paper, we investigate such properties for some classes of SN P systems. First, a class of SN P systems associated to a set of routing problems are investigated through their matrix representation. This allows to make certain connections amongst some of these problems. Secondly, the behavioural properties of these SN P systems are formally verified through a natural and direct mapping of these models into kP systems which are equipped with adequate formal verification methods and tools. Some examples are used to prove the effectiveness of the verification approach. / EPSRC research grant EP/R043787/1; DOST-ERDT research grants; Semirara Mining Corp; UPD-OVCRD;

yes / This Workshop on Membrane Computing, at the Conference of Unconventional Computation and Natural Computation (UCNC), 12th July 2016, Manchester, UK, is the second event of this type after the Workshop at UCNC 2015 in Auckland, New Zealand*. Following the tradition of the 2015 Workshop the Proceedings are published as technical report. The Workshop consisted of one invited talk and six contributed presentations (three full papers and three extended abstracts) covering a broad spectrum of topics in Membrane Computing, from computational and complexity theory to formal verification, simulation and applications in robotics. All these papers – see below, but the last extended abstract, are included in this volume. The invited talk given by Rudolf Freund, “P SystemsWorking in Set Modes”, presented a general overview on basic topics in the theory of Membrane Computing as well as new developments and future research directions in this area. Radu Nicolescu in “Distributed and Parallel Dynamic Programming Algorithms Modelled on cP Systems” presented an interesting dynamic programming algorithm in a distributed and parallel setting based on P systems enriched with adequate data structure and programming concepts representation. Omar Belingheri, Antonio E. Porreca and Claudio Zandron showed in “P Systems with Hybrid Sets” that P systems with negative multiplicities of objects are less powerful than Turing machines. Artiom Alhazov, Rudolf Freund and Sergiu Ivanov presented in “Extended Spiking Neural P Systems with States” new results regading the newly introduced topic of spiking neural P systems where states are considered. “Selection Criteria for Statistical Model Checker”, by Mehmet E. Bakir and Mike Stannett, presented some early experiments in selecting adequate statistical model checkers for biological systems modelled with P systems. In “Towards Agent-Based Simulation of Kernel P Systems using FLAME and FLAME GPU”, Raluca Lefticaru, Luis F. Macías-Ramos, Ionuţ M. Niculescu, Laurenţiu Mierlă presented some of the advatages of implementing kernel P systems simulations in FLAME. Andrei G. Florea and Cătălin Buiu, in “An Efficient Implementation and Integration of a P Colony Simulator for Swarm Robotics Applications" presented an interesting and efficient implementation based on P colonies for swarms of Kilobot robots. *http://ucnc15.wordpress.fos.auckland.ac.nz/workshop-on-membrane-computingwmc- at-the-conference-on-unconventional-computation-natural-computation/