Abstract We develop a process-algebraic framework for multiset reaction systems (MRSs), in which both reactions and system states are represented as multisets rather than sets. This representation enables quantitative reasoning about resources and naturally supports nondeterministic behaviour: unlike standard reaction systems, unconsumed resources persist into the next state, and several maximally enabled multisets of reactions may coexist at the same state. We equip the framework with a compositional operational semantics defined by structural operational semantics (SOS) rules, introduce a process representation for MRSs and the notion of maximal interactive processes, and prove that the induced labelled transition system faithfully corresponds to the rewriting dynamics of MRSs (Theorem 1). Building on this foundation, we extend the framework to distributed multiset reaction systems (DMRSs), in which processes are located at nodes of a network and communicate asynchronously by sending products to neighbouring locations. A distinguishing feature of the model is that reactions may dynamically modify the network topology through controlled division mechanisms, thereby integrating locality, asynchronous communication, and structural evolution within a single operational semantics. Finally, we investigate the computational power of DMRSs by studying their ability to solve the NP-complete Subset Sum problem. We present two constructions: a semi-uniform one, in which a dedicated DMRS is built for each problem instance, and a uniform one, in which a single DMRS handles all instances of a fixed size while the instance parameters are supplied as contextual resources. In both cases the system solves Subset Sum in at most $$2n+3$$ 2 n + 3 computation steps, where n is the number of input integers, by exploiting nondeterminism and large-scale parallelism: division generates all $$2^n$$ 2 n candidate subsets in parallel, and resource-based cancellation detects valid solutions. These results demonstrate that DMRSs constitute a powerful and flexible formal framework for distributed, resource-driven computation.

Abstract The evolution of a reaction system is usually achieved by applying a maximal set of reactions in a deterministic manner. In this paper, we consider reaction systems characterized by nondeterministic behaviour, where the set of applied reactions does not contain all enabled reactions, but only a subset of them based on specific constraints, particularly emphasizing on asynchronous reaction systems and restricted reaction systems. The nondeterministic approach facilitates a more realistic modelling of complex systems, where multiple potential behaviours can arise from a given set of reactions. Our aim is to explore different types of nondeterminism in reaction systems, investigating their behavioural properties, and examining the connections between the behaviour of asynchronous reaction systems and the behaviour of restricted reaction systems.

Are the membrane systems able of performing arithmetic operations? In the last dozen years, there were published several implementations of the arithmetic operations based on membrane systems by using all available topologies (cell-like, tissue-like, or neural-like). In particular, the spiking neural P systems perform arithmetic operations by using the numbers represented in binary base. In this paper, we consider numbers represented in unary base (to each number n corresponds an object with multiplicity n), and we propose two encodings for the main arithmetic operations (addition, subtraction, multiplication and division) between numbers given in unary base: (i) for each pair of input values generate an instance of a spiking neural P system with astrocytes producing calcium with rules based on these values; (ii) generate a spiking neural P system with astrocytes producing calcium that does not depend on these values. While the second approach is commonly used in membrane computing to construct only a system for each operation, the first approach is interesting because each system is uniquely constructed based on a pair of input values , and so it performs faster the desired arithmetic operation. The main advantage (with respect to other attempts) of using any of these two approaches to perform arithmetic operations consists in the reduced size of created systems (number of locations and used rules). Additionally, we extend a semantic interpreter (in Haskell) for spiking neural P systems to test all the encodings of the arithmetic operations presented in this paper.

In membrane systems evolution rules are constructed using only objects from a finite alphabet. In this paper we investigate rules in which variables are used. Namely, we define Variable P systems in which the rules containing variables need to be instantiated at the start of each computational step with values from some predefined sets of sets of objects. The modelling power of variable P systems is described by simulating some basic arithmetic operations over a (multi)set of positive numbers (addition, multiplication, or a combination of them). The main advantage of using variable P systems consists in the small number of used rules regardless how many numbers are involved in the operation: e.g., the addition requires only 3 rules, while the multiplication only 27 rules.

Abstract We study the dynamics of information sharing in web-based social networks and analyse in a stochastic manner some aspects of this phenomenon. We define the stochastic sharing calculus by considering probabilistic factors and stochastic evolutions that could be analysed statistically. A rate-based operational semantics allows specific observations and results regarding sharing in web-based social networks. To reason about the dynamics of the social networks, we verify statistically various aspects of information sharing expressed in CTL by employing an existing statistical model checker (after a translation of our processes into stochastic automata). Some queries related to the stochastic behaviours in social networks are illustrated by a running example.

The astrocytes are cells which play an essential role in the functioning and interaction of neurons by feeding the respective neurons with calcium ions. Drawing inspiration from this two-way relationship in which the astrocytes influence and are influenced by the neurons by means of calcium ions, in this paper, we define and study spiking neural P systems with astrocytes producing calcium. Distinct from the usual firing rules in spiking neural P systems, the firing condition not only depends on the spikes collected in a neuron but also on the calcium units received from astrocytes. From the perspective of topological structure, the new variant is shown as a directed graph in which synapses link either astrocytes or neurons, as well as astrocytes to neurons and conversely. The computational power of spiking neural P systems with astrocytes producing calcium is investigated; it is proved that these systems using a limited number of rules are Turing universal as both number generating and number accepting devices. It is also presented how to obtain normal forms by removing forgetting rules and delays while preserving the computational power.

This article explores the proof theory necessary for recommending an expressive but decidable first-order system, named MAV1, featuring a De Morgan dual pair of nominal quantifiers. These nominal quantifiers called “new” and “wen” are distinct from the self-dual Gabbay-Pitts and Miller-Tiu nominal quantifiers. The novelty of these nominal quantifiers is they are polarised in the sense that “new” distributes over positive operators while “wen” distributes over negative operators. This greater control of bookkeeping enables private names to be modelled in processes embedded as formulae in MAV1. The technical challenge is to establish a cut elimination result from which essential properties including the transitivity of implication follow. Since the system is defined using the calculus of structures, a generalisation of the sequent calculus, novel techniques are employed. The proof relies on an intricately designed multiset-based measure of the size of a proof, which is used to guide a normalisation technique called splitting . The presence of equivariance, which swaps successive quantifiers, induces complex inter-dependencies between nominal quantifiers, additive conjunction, and multiplicative operators in the proof of splitting. Every rule is justified by an example demonstrating why the rule is necessary for soundly embedding processes and ensuring that cut elimination holds.

This special issue marks the 60th birthday of Professor Gabriel Ciobanu.It consists of 7 original contributions from colleagues who have accompanied Gabriel through his scientific life in one way or another, be it in joint projects, research articles, or even the writing of complete books.We would like to thank all the contributors to this special issue for their hard work and

We present an expressive but decidable first-order system (named MAV1) defined by using the calculus of structures, a generalisation of the sequent calculus. In addition to first-order universal and existential quantifiers the system incorporates a de Morgan dual pair of nominal quantifiers called `new' and `wen', distinct from the self-dual Gabbay-Pitts and Miller-Tiu nominal quantifiers. The novelty of the operators `new' and `wen' is they are polarised in the sense that `new' distributes over positive operators while `wen' distributes over negative operators. This greater control of bookkeeping enables private names to be modelled in processes embedded as predicates in MAV1. Modelling processes as predicates in MAV1 has the advantage that linear implication defines a precongruence over processes that fully respects causality and branching. The transitivity of this precongruence is established by novel techniques for handling first-order quantifiers in the cut elimination proof.