Abstract Reaction systems (RSs) are a successful natural computing framework inspired by chemical reaction networks. A RS consists of a set of entities and a set of reactions. Entities can enable or inhibit each reaction and are produced by reactions or provided by the environment. In this paper, we define two quantitative variants of RSs: the first one is along the time dimension, to specify delays for making available reactions products and durations to protract their permanency, while the second deals with the possibility to specify different concentration levels of a substance in order to enable or inhibit a reaction. Technically, both extensions are obtained by modifying in a modular way the Structural Operational Semantics (SOS) for RSs that was already defined in the literature. Our approach maintains several advantages of the original semantics definition that were: (1) providing a formal specification of the RS dynamics that enables the reuse of many formal analysis techniques and favours the implementation of tools, and (2) making the RS framework extensible, by adding or changing some of the SOS rules in a compositional way. We provide a prototype logic programming implementation and apply our tool to three different case studies: the tumour growth, the Th cell differentiation in the immune system and neural communication.

Gene regulatory networks represent the interactions among genes regulating the activation of specific cell functionalities and they have been successfully modeled using threshold Boolean networks. In this paper we propose a systematic translation of threshold Boolean networks into reaction systems. Our translation produces a non redundant set of rules with a minimal number of objects. This translation allows us to simulate the behavior of a Boolean network simply by executing the (closed) reaction system we obtain. This can be very useful for investigating the role of different genes simply by “playing” with the rules. We developed a tool able to systematically translate a threshold Boolean network into a reaction system. We use our tool to translate two well known Boolean networks modelling biological systems: the yeast-cell cycle and the SOS response in Escherichia coli. The resulting reaction systems can be used for investigating dynamic causalities among genes.

Reaction systems are a qualitative formalism for modeling systems of biochemical reactions characterized by the non-permanency of the elements: molecules disappear if not produced by any enabled reaction. Reaction systems execute in an environment that provides new molecules at each step. Brijder, Ehrenfeucht and Rozemberg introduced the idea of predictors. A predictor of a molecule s, for a given n, is the set of molecules to be observed in the environment to determine whether s is produced or not at step n by the system. We introduced the notion of formula based predictor, that is a propositional logic formula that precisely characterizes environments that lead to the production of s after n steps. In this paper we revise the notion of formula based predictor by defining a specialized version that assumes the environment to provide molecules according to what expressed by a temporal logic formula. As an application, we use specialized formula based predictors to give theoretical grounds to previously obtained results on a model of gene regulation.

Maximally parallel semantics have been proposed for many formalisms as an alternative to the standard interleaving semantics for some modelling scenarios. Nevertheless, in the probabilistic setting an affirmed interpretation of maximal parallelism st

Two forms of interferences are individuated in Cardelli and Gordon's Mobile Ambients (MA): plain interferences , which are similar to the interferences one finds in CCS and π-calculus; and grave interferences , which are more dangerous and may be regarded as programming errors. To control interferences, the MA movement primitives are modified; the resulting calculus is called Mobile Safe Ambients (SA).The modification also has computational significance. In the MA interaction rules, an ambient may enter, exit, or open another ambient. The second ambient undergoes the action; it has no control on when the action takes place. In SA this is rectified: any movement takes place only if both participants agree.Existing type systems for MA can be easily adapted to SA. The type systems for controlling mobility, however, appear to be more powerful in SA, in that (i) type systems for MA may give more precise information when transplanted onto SA , and (ii) new type systems may be defined. Two type systems are presented that remove all grave interferences.Other advantages of SA are: a useful algebraic theory; programs sometimes more robust (they require milder conditions for correctness) and/or simpler. All these points are illustrated in several examples.

In this paper we propose a process language JSP which abstractly models timed statecharts with minimal and maximal delays associated to transitions. Statecharts processes are equipped with a labelled transition system semantics that combines the basic principles of the semantics of Pnueli and Shalev with discrete time. Furthermore, we propose a compositional proof system to check quantitative temporal properties of statecharts processes. Properties are expressed in a discrete extension of µ‐calculus with reset over clocks and clock constraints. The proof system is sound in general and it is complete for the class of regular processes (including processes corresponding to statecharts).

Two forms of interferences are individuated in Cardelli and Gordon's Mobile Ambients (MA): plain interferences, which are similar to the interferences one finds in CCS and φ-calculus; and grave interferences, which are more dangerous and may be regarded as programming errors. To control interferences, the MA movement primitives are modified. On the new calculus, the Mobile Safe Ambients (SA), a type system is defined that: controls the mobility of ambients; removes all grave interferences. Other advantages of SA are: a useful algebraic theory; programs sometimes more robust (they require milder conditions for correctness) and/or simpler. These points are illustrated on several examples.