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.

This paper presents a calculus inspired by the spiking neural P systems. Its operational and denotational semantics are defined; they are related by using the metric semantics methodology, showing that the denotational semantics is correct with respect to the operational one. We use the continuations for concurrency to describe precisely the nondeterministic behaviour, the time delays between firings and spikings, as well as the synchronized functioning specific to spiking neural P systems.

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.

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.

Summary We investigate a language similar to a process algebra introduced by Cardelli for DNA computing. For such a language, we relate two formal semantics. We define a new denotational semantics by using complete metric spaces, in which various semantic functions are defined as fixed points of appropriate higher‐order mappings. We compare this denotational semantics with an operational semantics and establish a formal relationship between them by using an abstraction operator and a fixed point argument. In this way, we prove the correctness of the denotational semantics with respect to the operational one. Copyright © 2015 John Wiley & Sons, Ltd.

We present a theory of abstract interpretations in the framework of invariant sets by translating the notions of lattices and Galois connections into this framework, and presenting their properties in terms of finitely supported objects. We introduce the notions of invariant correctness relation and invariant representation function, emphasize an equivalence between them, and establish the relationship between these notions and invariant Galois connections. Finally, we provide some widening and narrowing techniques in order to approximate the least fixed points of finitely supported transition functions.

We introduce a process algebra with processes able to migrate between different explicit locations of a distributed environment defined by a number of distinct locations. We use timing constraints over local clocks to control migration and communication, together with local maximal concurrency in the way actions are executed. Two processes may communicate if they are present at the same location and, in addition, they have appropriate access permissions to communicate over a shared channel. Access permissions can be acquired or lost while moving from one location to another. Timing constraints coordinate and control both communication between processes and migration between locations. We completely characterize the situations in which a process is guaranteed to possess safe access permissions in all possible environments. In this way, one can design systems in which processes are not blocked (deadlocked) due to the lack of dynamically changing access permissions.

Abstract The process algebras Timed Mobility (TiMo) and its extension Permissions, Timers and Mobility (PerTiMo) were recently proposed to support engineering applications in distributed system design.TiMoprovides a formal framework in which process migration between distinct locations and timing constraints linked to local clocks can be modelled and analysed. This is extended inPerTiMoby associating access permissions to communication to model security aspects of a distributed system. In this paper we develop a new semantic model forTiMousing Rewriting Logic (RL) and strategies, with the aim of providing a foundation for tool support; in particular, strategies are used to capture the locally maximal concurrent step of aTiMospecification which previously required the use of action rules based on negative premises. This RL model is then extended with access permissions in order to develop a new semantic model forPerTiMo. These RL semantical models are formally proved to be sound and complete with respect to the original operational semantics on which they were based. We present examples of how the developed RL models forTiMoandPerTiMocan be implemented within the strategy-based rewriting systemElanand illustrate the range of (behavioural) properties that can be analysed using such a tool.

Mobile distributed systems involve specific aspects such as migration, communication and concurrency, usually under temporal constraints. In this paper, we deal with formal modelling of timed migrating and communicating processes, as provided by the TiMo calculus. In this framework, mobile processes can move between different locations and communicate when collocated, all this happening in the presence of local timers. Our contribution is a general framework for reasoning about systems specified using TiMo. We use the Event-B modelling method as the target for translating TiMo specifications. Subsequently, we utilise the supporting Rodin platform of Event-B to verify system properties using the embedded theorem-provers and model checkers. The main feature of our encoding include a generic model capturing the syntax and semantics of TiMo, together with a concrete model corresponding to each specific TiMo specification. We illustrate our approach by a non-trivial example featuring different concepts of TiMo.

We study indexed multisets in the context of multiset rewriting systems, using indexes to capture the number of the step in which a rule is applied or an object is produced. We show that the evolution of a multiset rewriting system is accurately reflected by its indexed version and we extend this result to maximal parallelism. We analyse situations in which indexed rule application can be postponed, and introduce an equivalence relation based on such situations. We introduce the notions of cause and of causal chains, and show how adding indexes allows us to decompose evolution into independent causal chains.

We introduce and study the nominal groups, providing some algebraic properties of this new structure. We focus on the properties of nominal homomorphisms, and study the correspondence between some results obtained in the Fraenkel-Mostowski framework (where only finitely supported objects are allowed) and those obtained in the classical Zermelo-Fraenkel framework.

Models of biological systems expressed as multiset rewriting systems can be very complex, impeding the analysis of their behaviour. In this paper we propose a practical solution to this problem, in the form of change monitors, i.e. computational inst

The paper presents a method of reasoning about the behaviour of asynchronous programs in denotational models designed with metric spaces and continuation semantics for concurrency.

TiMo is a process calculus for mobile systems where timers could be to used to control process mobility and interaction. Despite its syntactic simplicity, TiMo is able to describe complex systems. Interesting properties of such systems refers to process migration, time constraints, bounded liveness and optimal reachability. In this work we describe a tool, called TiMo@PAT, developed by using Process Analysis Toolkit (PAT), an extensible platform for model checkers. We illustrate the capability of TiMo@PAT by analyzing some properties of a distributed system.

SUMMARY In this paper, we present a flexible software architecture and a language for systems of mobile agents starting from a formalism with timed interactions and explicit locations. The language supports the specification of a distributed system, that is, agents and their physical distribution, and allows a timed migration in a distributed environment. Advanced software technologies are used to define the software architecture and the agents language, facilitating also the agents development. We illustrate the system by a dynamic network discovery in which the agents take into account the latency and the CPU load when choosing where to migrate. Copyright © 2011 John Wiley & Sons, Ltd.

Software systems have become increasingly distributed, dynamic and mobile. The complex state and dynamic interfaces of software components and their concurrent interactions provide challenging research issues in system specification and design. An effective combination of structured state-based formalism and dynamic action-based calculus may be a good solution for modeling complex distributed mobile systems. In this paper, we investigate the semantic links between Object-Z and /spl pi/ calculus and consequently introduce a powerful specification technique PiOZ that brings the strengths of the two together. The operational semantics of PiOZ integrates state transition semantics of Object-Z and /spl pi/-calculus reduction rules. The typing rules of PiOZ are developed and reasoning of a system property is presented.

The paper proposes a high-level model to represent spatio-temporal relations between Web sites or fragments of Web sites in order to facilitate resource discovery, cataloging or describe information. This model is based on the Resource Description Framework (RDF) recommendation of the World-Wide Web Consortium, a general purpose technology that enables the description of resources on the Web. The representation of the spatio-temporal relationships is expressed by an XML-based language.