| Summary: | Membrane systems, also known as P systems, constitute an innovative computational paradigm inspired by the structure and dynamics of the living cell. A P system consists of a hierarchical arrangement of compartments and a finite set of multiset rewriting and communication rules, which operate in a maximally parallel manner. The organic vision of concurrent dynamics captured by membrane systems stands in antithesis with conventional formal modelling methods which focus on algebraic descriptions of distributed systems. As a consequence, verifying such models in a mathematically rigorous way is often elusive and indeed counter-intuitive when considering established approaches, which generally require sequential process representations or highly abstract theoretical frameworks. The prevalent investigations with this objective in the field of membrane computing are ambivalent and inconclusive in the wider application scope of P systems. In this thesis we directly address the formal verification of membrane systems by means of model checking. A fundamental distinction between the agnostic perspective on parallelism, advocated by process calculi, and P systems' emblematic maximally parallel execution strategy is identified. On this basis, we establish that an intuitional translation to traditional process models is inadequate for the purpose of formal verification, due to a state space growth disparity. The observation is essential for this research project: on one hand it implies the feasibility of model checking P systems, and on the other hand it underlines the suitability of this formal verification technique in the context of membrane computing. Model checking entails an exhaustive state space exploration and does not derive inferences based on the independent instructions comprising a state transition. In this respect, we define a new sequential modelling strategy which is optimal for membrane systems and targets the SPIN formal verification tool. We introduce elementary P systems, a distributed computational model which subsumes the feature diversity of the membrane computing paradigm and distils its functional vocabulary. A suite of supporting software tools which gravitate around this formalism has also been developed, comprising of 1. the eps modelling language for elementary P systems; 2. a parser for the eps specification; 3. a model simulator and 4. a translation tool which targets the Promela specification of the SPIN model checker. The formal verification approach proposed in this thesis is progressively demonstrated in four heterogeneous case studies, featuring 1. a parallel algorithm applicable to a structured model; 2. a linear time solution to an NP-complete problem; 3. an innovative implementation of the Dining Philosophers scenario (a synchronisation problem) using an elementary P system and 4. a quantitative analysis of a simple random process implemented without the support of a probabilistic model.
|
|---|
