Mutual mobile membranes with objects on surface

In this paper we study systems of mutual mobile membranes with objects on surface using pino/exo/phago rules. Their rules are applicable whenever there is a mutual agreement between membranes expressed by appropriate objects and co-objects on their surfaces. We investigate the computational power of these systems, and also relate them to brane calculi by encoding the PEP fragment of brane calculus into the systems of mutual mobile membranes with objects on surface.     

Membrane Systems with Marked Membranes

Membrane computing is a biologically inspired computational paradigm. Motivated by brane calculi we investigate membrane systems which differ from conventional membrane systems by the following features: (1) biomolecules (proteins) can move through the regions of the systems, and can attach onto (and de-attach from) membranes, and (2) membranes can evolve depending on the attached molecules. The evolution of membranes is performed by using rules that are motivated by the operation of pinocytosis (the pino rule) and the operation of cellular dripping (the drip rule) that take place in living cells. We show that such membrane systems are computationally universal. We also show that if only the second feature is used then one can generate at least the family of Parikh images of the languages generated by programmed grammars without appearance checking (which contains non-semilinear sets of vectors). If, moreover, the use of pino/drip rules is non-cooperative (i.e., not dependent on the proteins attached to membranes), then one generates a family of sets of vectors that is strictly included in the family of semilinear sets of vectors. We also consider a number of decision problems concerning reachability of configurations and boundness.     

P Systems with Mobile Membranes

P systems with active membranes are among the central ones in membrane computing, and they were shown to be both computationally universal (able to simulate Turing machines) and computationally efficient (able to solve hard problems in polynomial time). However, in all cases, these results were obtained by making use of several powerful features, such as membrane polarization, label changing, division of non-elementary membranes, priorities, or cooperative rules. This paper contributes to the research effort of introducing a class of P systems with active membranes having none of the features mentioned above, but still preserving the power and the efficiency. The additional feature we consider instead are the operations of endocytosis and exocytosis: moving a membrane inside a neighboring membrane, or outside the membrane where it is placed. We investigate the power and the efficiency of these systems (also using membrane division) by first proving that they can simulate (with a linear slowdown and without introducing non-determinism) rewriting P systems with 2-replication, for which the universality and the possibility of solving NP-complete problems in polynomial time are known. In this way, the universality and efficiency are also obtained for our systems. We also give a direct and simple proof for the universality result – without using division rules (the proof uses nine membranes, but we do not know whether this number can be decreased).     

P systems with minimal parallelism

A current research topic in membrane computing is to find more realistic P systems from a biological point of view, and one target in this respect is to relax the condition of using the rules in a maximally parallel way. We contribute in this paper to this issue by considering the minimal parallelism of using the rules: if at least a rule from a set of rules associated with a membrane or a region can be used, then at least one rule from that membrane or region must be used, without any other restriction (e.g., more rules can be used, but we do not care how many). Weak as it might look, this minimal parallelism still leads to universality. We first prove this for the case of symport/antiport rules. The result is obtained both for generating and accepting P systems, in the latter case also for systems working deterministically. Then, we consider P systems with active membranes, and again the usual results are obtained: universality and the possibility to solve NP-complete problems in polynomial time (by trading space for time).     

A Simple Calculus for Proteins and Cells

The use of process calculi to represent biological systems has led to the design of different calculi such as brane calculi [Luca Cardelli. Brane calculi. In CMSB, pages 257–278, 2004] and κ-calculus [Vincent Danos and Cosimo Laneve. Formal molecular biology. Theoritical Computer Science, 325(1):69–110, 2004]. Both have proved to be useful to model different types of biological systems.As an attempt to unify the two directions, we introduce the bioκ-calculus, a simple calculus for describing proteins and cells, in which bonds are represented by means of shared names and interactions are modelled at the domain level. Protein-protein interactions have to be at most binary and cell interactions have to fit with sort constraints.We define the semantics of bioκ-calculus, analyse its properties, and discuss its expressiveness by modelling two significant examples: a signalling pathway and a virus infection.     

On the power and size of extended gemmating P systems

In [3] P systems with gemmation of mobile membranes were examined. It was shown that (extended) systems with eight membranes are as powerful as the Turing machines. Moreover, it was proved that extended gemmating P systems with only pre-dynamical rules are still computationally complete: in this case nine membranes are needed to obtain this computational power. In this paper we improve the above results concerning the size bound of extended gemmating P systems, namely we prove that these systems with at most five membranes (with meta-priority relations and without communication rules) form a class of universal computing devices, while in the case of extended systems with only pre-dynamical rules six membranes are enough to determine any recursively enumerable language.     

P systems with energy accounting ∗

We consider P systems where each evolution rule “Produces” or “Consumes” some quantity of energy, in amounts which are expressed as integer numbers. In each moment and in each membrane the total energy involved in an evolution step should be positive, but if “Soo much” energy is present in a membrane, then the membrane will be destroyed (dissolved). We show that this feature is rather powerful. In the case of multisets of symbol-objects we find that systems with two membranes and arbitrary energy associated with rules, or with arbitrarily many membranes and a bounded energy associated with rules characterize the recursively enumerable sets of vectors of natural numbers (catalysts and priorities are used). In the case of string-objects we have only proved that the recursively enumerable languages can be generated by systems with arbitrarily many membranes and bounded energy; when bounding the number of membranes and leaving free the quantity of energy associated with each rule we have only generated all matrix languages. Several research topics are also pointed out.     

Further remark on P systems with active membranes and two polarizations

P systems (or membrane systems) are a class of distributed parallel computing devices of a biochemical type. In this paper, some restrictions on the general form of the developing rules are considered, under which it is still possible to solve NP-complete problems. We present an algorithm for deterministically deciding SAT in linear time by P systems with active membranes using two polarizations and rules of restricted versions of types (a), (c), (e). The result obtained in this paper answered an open problem proposed by Alhazov and Freund in the aspect of computing efficiency.     

Tissue P Systems and (Mem)Brane Systems with Mate and Drip Operations Working on Strings

We investigate tissue P systems with (non-restricted, symmetric) versions of mate and drip operations and prove that such systems are computationally complete with the minimal number of two cells when working on strings. Moreover, we consider the variant of scattered context tissue P systems with mate and drip operations and show a similar computational completeness result with using at most four cells during any computation. In all cases, the corresponding results for (mem)brane systems are established, too.     

P Systems with Global Rules

We contribute to the vivid area of membrane computing (P systems) by considering the case when the same evolution rules are valid in all regions of a system. Such a P system is called with global rules . We consider the case of string-objects, with the evolution rules based on splicing and by rewriting. Universality results are proved for both types of systems. For splicing we also try to minimize the diameter of the used rules, while for rewriting systems we improve a result from the literature, proving that two membranes suffice for simulating Turing machines.     

Tree models and (labeled) categorial grammar

This paper studies the relation between some extensions of the non-associative Lambek Calculus NL and their interpretation in tree models (free groupoids). We give various examples of sequents that are valid in tree models, but not derivable in NL. We argue why tree models may not be axiomatizable if we add finitely many derivation rules to NL, and proceed to consider labeled calculi instead.We define two labeled categorial calculi, and prove soundness and completeness for interpretations that are almost the intended one, namely for tree models where some branches of some trees may be resp. all branches of all trees must be infinitely extending. Extrapolating from the experiences in our quite simple systems, we briefly discuss some problems involved with the introduction of labels in categorial grammar, and argue that many of the basic questions are not yet understood.     

An embedding of Timed Transition Systems in HOL

The theory of Timed Transition Systems developed by Henzinger, Manna, and Pnueli provides a formal framework for specifying and reasoning about real-time systems. In this paper, we report on some preliminary investigations into the mechanization of this theory using the HOL theorem prover.We review the main ideas of the theory and describe how it has been formally embedded in HOL. A graphical notation of timed transition diagrams and a real-time temporal logic for requirements have also been embedded in HOL using the embedding of timed transition systems. The proof rules proposed by Henzinger et al have been verified formally and we illustrate their use, as well as some problems we have encountered, by reference to a small example. More work is required on interfaces and proof methods to have a generally usable system.     

Solving the Subset-Sum problem by P systems with active membranes

We present the first membrance computing solution to the Subset-Sum problem using a family of deterministic P systems with active membranes. We do not use priority among rules, membrane dissolution nor cooperation; it suffices to control the electrical charges of the membranes and to introduce some counters. The number of steps of any computation is of the linear order (but it is necessary a polynomial-time of precomputed resources).     

Stream processing coalgebraically

We study various operations for splitting, partitioning, projecting and merging streams of data. These operations are motivated by their use in dataflow programming and stream processing languages. We use the framework of stream calculus and stream circuits for defining and proving properties of such operations using behavioural differential equations and coinduction proof principles. As a featured example we give proofs of results, observed by Moessner, from elementary number theory using our framework. We study the invariance of certain well patterned classes of streams, namely rational and algebraic streams, under splitting and merging. Finally we show that stream circuits extended with gates for dyadic split and merge are expressive enough to realise some non-rational algebraic streams, thereby going beyond ordinary stream circuits.     

Trading polarizations for labels in P systems with active membranes

This paper addresses the problem of removing the polarization of membranes from P systems with active membranes - and this is achieved by allowing the change of membrane labels by means of communication rules or by membrane dividing rules. As consequences of these results, we obtain the universality of P systems with active membranes which are allowed to change the labels of membranes, but do not use polarizations. Universality results are easily obtained also by direct proofs. By direct constructions, we also prove that SAT can be solved in linear time by systems without polarizations and with label changing possibilities. If non-elementary membranes can be divided, then SAT can be solved in linear time without using polarizations and label changing. Several open problems are also formulated.Received: 29 October 2003, Published online: 29 October 2004Artiom Alhazov: artiome.alhazov@estudiantsLinqiang Pan: lp@fll.urv.esGheorghe Pun: george.paun@imar.ro     

On the expressive power of movement and restriction in pure mobile ambients

Pure mobile ambients is a process calculus suitable to focus on issues related to mobility, abstracting away from aspects concerning process communication. However, it incorporates name restriction (i.e. the (νn) binder) and ambient movement (i.e. the in and out capabilities) that can be seen as characteristics adapted, or directly borrowed, from the tradition of communication-based process calculi. For this reason, we retain that it is worth to investigate whether or not these features can be removed from pure mobile ambients without losing expressive power.To this aim, we consider two variants of pure mobile ambients which differ in the way infinite processes can be defined; the former exploits process replication, while the latter is more general and permits recursive process definition. We analyse whether or not the elimination of ambient movement and/or name restriction reduces the expressive power of these two calculi, using the decidability of process termination as a yardstick. We prove that name restriction can be removed from both calculi without reducing the expressive power. On the other hand, the elimination of both ambient movement and name restriction strictly reduces the expressive power of both calculi. As far as the elimination of only ambient movement is concerned, we prove an interesting discrimination result: process termination is undecidable under recursive process definition, while it turns out to be decidable under process replication.     

Dynamic self-assembly in living systems as computation

Biochemical reactions taking place in living systems that map different inputs to specific outputs are intuitively recognized as performing information processing. Conventional wisdom distinguishes such proteins, whose primary function is to transfer and process information, from proteins that perform the vast majority of the construction, maintenance, and actuation tasks of the cell (assembling and disassembling macromolecular structures, producing movement, and synthesizing and degrading molecules). In this paper, we examine the computing capabilities of biological processes in the context of the formal model of computing known as the random access machine (RAM) [Dewdney AK (1993) The New Turing Omnibus. Computer Science Press, New York], which is equivalent to a Turing machine [Minsky ML (1967) Computation: Finite and Infinite Machines. Prentice-Hall, Englewood Cliffs, NJ]. When viewed from the RAM perspective, we observe that many of these dynamic self-assembly processes – synthesis, degradation, assembly, movement – do carry out computational operations. We also show that the same computing model is applicable at other hierarchical levels of biological systems (e.g., cellular or organism networks as well as molecular networks). We present stochastic simulations of idealized protein networks designed explicitly to carry out a numeric calculation. We explore the reliability of such computations and discuss error-correction strategies (algorithms) employed by living systems. Finally, we discuss some real examples of dynamic self-assembly processes that occur in living systems, and describe the RAM computer programs they implement. Thus, by viewing the processes of living systems from the RAM perspective, a far greater fraction of these processes can be understood as computing than has been previously recognized.     

Bond computing systems: a biologically inspired and high-level dynamics model for pervasive computing

Targeting at modeling the high-level dynamics of pervasive computing systems, we introduce bond computing systems (BCS) consisting of objects, bonds and rules. Objects are typed but addressless representations of physical or logical (computing and communicating) entities. Bonds are typed multisets of objects. In a BCS, a configuration is specified by a multiset of bonds, called a collection. Rules specify how a collection evolves to a new one. A BCS is a variation of a P system introduced by Gheorghe Paun where, roughly, there is no maximal parallelism but with typed and unbounded number of membranes, and hence, our model is also biologically inspired. In this paper, we focus on regular bond computing systems (RBCS), where bond types are regular, and study their computation power and verification problems. Among other results, we show that the computing power of RBCS lies between linearly bounded automata (LBA) and LBC (a form of bounded multicounter machines) and hence, the regular bond-type reachability problem (given an RBCS, whether there is some initial collection that can reach some collection containing a bond of a given regular type) is undecidable. We also study a restricted model (namely, B-boundedness) of RBCS where the reachability problem becomes decidable.     

Calculi of meta-variables

The notion of meta-variable plays a fundamental role when we define formal systems such as logical and computational calculi. Yet it has been usually understood only informally as is seen in most textbooks of logic. Based on our observations of the usages of metavariables in textbooks, we propose two formal systems that have the notion of meta-variable. In both calculi, each variable is given a level (non-negative integer), which classifies variables into object variables (level 0), meta-variables (level 1), metameta-variables (level 2) and so on. Then, simple arity systems are used to exclude meaningless terms like a meta-level function operating on the metameta-level. A main difference of the two calculi lies in the definitions of substitution. The first calculus uses textual substitution, which can often be found in definitions of quantified formulae: when a term is substituted for a meta-variable, free object-level variables in the term may be captured. The second calculus is based on the observation that predicates can be regarded as meta-level functions on object-level terms, hence uses capture-avoiding substitution. We show that both calculi enjoy a number of properties including Church-Rosser and Strong Normalization, which are indispensable when we use them as frameworks to define logical systems.