Main objectives

We analyzed the computational properties of enhanced mobile membranes realizing their representation in colored Petri nets [L1]. The representation reflects the structure of the used parallelism and simultaneously is inversely invariant to the edge properties, accessibility and fairness. We exemplified a biological model of mobility of a bacteria as an enhanced membrane system and we used the colored Petri net to obtain a simulation in CPN Tools.

Contributions of the journal volume "Theoretical Computer Science" (ISI), that contains extended versions of selected works of the 2009-2011 editions of the workshop presented MeCBIC (Membrane Computing and Biologically Inspired Process calculi) are presented and classified in [L2 ].

Starting from a formalism with interaction timers and explicit locations, we presented a flexible software architecture and a language for mobile agent systems [L3]. This language supports the specification of a distributed system, namely agents and their physical distribution and allows a temporal evolution in a framework.

Without resorting to a translation in a different formalism such as event structures, we introduced the concepts of specific and general causality over multisets of objects and transitional rules in membrane systems [L4]. We defined specific causality as being obtained at a fixed transition by imposing minimality conditions and the general one as obtained by imposing similar conditions without the need for fixing a transition. We proved that we can obtain general causality by bringing together specific causes and then we introduced the inductive procedure for obtaining general causality without using the specific one, but using a characterization theorem. Finally we obtained a characterization relative to general causality through which we can decide if a multiset of objects can be obtained from another given multiset (partial accessibility decidability).

We used techniques from the field of membrane systems in mobile ambients to solve intractable problems in a polynomial number of steps (at the cost of increasing the size of the settlement area) [L5]. The formalism used is that of mobile ambients with coordination and parallelism, which is often used for the modelling of the computational mobility. We demonstrated that this formalism can give a semi-uniform solution to the SATproblem and presented a concrete example for a case with three terms and three variables.

We have introduced a class of Petri nets called  catalytic Petri nets, in which the transition strategy requires consumption of special symbols called catalysts, namely a parallel strategy with minimal local verification [L6]. We have proved a link between this class and the formalism of membrane systems with catalysts. We demonstrated that this correlation implies computational universality catalytic Petri nets that have at least two catalysts, unlike the general case of Petri nets with a special strategy of activating transitions.

The paper [L7] has been accepted for presentation at the Turing Centenary Conference in Cambridge after a competition with over 250 works submitted. We analyzed the computational power of membrane systems with controlled mobility. These types of systems use rules inspired by the biological processes of endocytosis and exocytosis, with different variations relative to the objects that control the mobility rules. We have demonstrated that using only variations of forced endocytosis and exocytosis rules a four membrane system is Turing complete (in other words, the universal computational point of view), while a system with only three membranes is not Turing complete. We have shown that the addition of rules that allow the restricted division  of membranes is not sufficient in order to allow Turing completeness; on the other hand the addition of inhibitors in a single type of rules is sufficient. In addition we have shown that using only restricted rules does not allow computational completeness.

We presented an approach in which the temporal evolution of mobile processes is characterized by local clocks that operate independently and by the duration of migration processes between locations [L8]. We defined and investigated various behavioural equivalences between processes that migrate in distributed systems, in terms of local times and locations.

We offered an alternative semantics for TiMo using an algebraic formalism called "rewriting logic" (RL), that is able to model the behaviuor of dynamic systems [L9]. TiMo is a formalism that allows control over how communication occurs between processes at the local level by introducing time constraints. We have defined a strategy based on RL model description of a maximal parallel computational step for a TiMo specification. This new semantic model is "sound" and complete. We implemented this model using the rewrite system ELAN and offered an example of how a TiMo specification is executed and how a number of behavioural properties are analysed.

We defined a nominal semantics for fusion calculus [L10]. We represented variables in the fusion calculus as atoms of the axiomatic Fraenkel-Mostowski model and the "scope" operator as a nominal abstractions. We obtained compact transition rules in which the side conditions are replaced by a proper mixing of the binding operators "any" and "new". We have demonstrated that structural  nominal congruence and the structural congruence of the fusion calculus are equivalent. The nominal semantics and the usual semantics (Parrow-Victor) of the fusion calculus have the same expressive power.

We studied mobile membranes with objects on the surface and used this class of mobile membrane to model the degradation of low density lipoprotein [L11]. We built a translation between this formalism and colorued Petri nets and using a complex software for editing, simulation and analysis of coloured Petri nets, called "CPN Tools", we discussed several important properties of mobile membranes.

We studied mobile membranes with travel time, that is a formalism inspired by biology, able to model systems using evolutionary time, explicit location and mobility [L12]. We defined a number of behavioural equivalences over this formalism and demonstrated that some equivalences are finer than others while other equivalences are incomparable.

We considered catalytic membrane systems and catalytic Petri nets over which we have introduced a discrete notion of temporality that shapes the time between consuming and creation of reactants [L13]. We obtained two formalisms called "tCatMS" and "tCatPN". We established formal links between these formalisms and we characterized certain subclasses in which different properties are decidable and can be analyzed using the software "CPN Tools".

We defined, using mathematical methodology of metric, a denotational semantics denotaţională semantics and operational semantics for an abstract concurrent language in which parallel composition is based on maximal parallelism and computations are described by multisets rewriting rules  [L14]. We then compared the two semantics in terms of this combination of concepts.

We presented two approaches called "causal correlative" and "quantitative causal" to study relationships "cause and effect" models of reaction [L15]. We have proposed a framework that integrates the two concepts in order to study causality using membrane systems. This framework is based on the fact that statistical analysis can be used to build a membrane model that can be used to analyze causal relationships in terms of multisets of objects and rules in the presence of non-determinism and parallelism. We demonstrated that the P system defined by correlation analysis provides a quantitative correspondence between the notions of quantitative causality and  correlative causality.

In addition to the above works we have achieved two technical reports [TR1] and [TR2].