Search

Cause/effect analysis of complex systems is instrumental in better understanding many natural phenomena. Moreover, formal analysis requires the availability of suitable abstract computational models that somehow preserve the features of interest. Our contribution focuses on the analysis of Reaction Systems (RSs), a qualitative computational formalism inspired by biochemical reactions in living cells. The primary challenge lies in dealing with inhibition mechanisms. On the one hand, inhibitors enhance the expressiveness of the computational abstraction; on the other hand, they can introduce nonmonotonic behaviors that can be computationally hard to deal with in the analysis. We propose an encoding of RSs into an equivalent formulation without inhibitors (called Positive RSs, PRSs for short) that is easier to handle, because PRSs exhibit monotonic behaviors. The effectiveness of our transformation is witnessed by its impact on two different techniques for cause/effect analysis. The first, called slicing, allows detecting the causes of some unforeseen phenomenon by reasoning backward along a given computation. Here, PRSs can be exploited to improve the quality of the analysis. The second technique, predictor analysis, is addressed by introducing a novel tool called MuMa, which is based on must/maybe sets, whence the tool name, an original abstraction for approximating ancestor formulas. MuMa exploits PRSs to improve the performance of the analysis. [ABSTRACT FROM AUTHOR]

This paper forges a strong connection between two well known computational frameworks for representing biological systems, in order to facilitate the seamless transfer of techniques between them. Boolean networks are a well established formalism employed from biologists. They have been studied under different (synchronous and asynchronous) update semantics, enabling the observation and characterisation of distinct facets of system behaviour. Recently, a new semantics for Boolean networks has been proposed, called most permissive semantics, that enables a more faithful representation of biological phenomena. Reaction systems offer a streamlined formalism inspired by biochemical reactions in living cells. Reaction systems support a full range of analysis techniques that can help for gaining deeper insights into the underlying biological phenomena. Our goal is to leverage the available toolkit for predicting and comprehending the behaviour of reaction systems within the realm of Boolean networks. In this paper, we first extend the behaviour of reaction systems to several asynchronous semantics, including the most permissive one, and then we demonstrate that Boolean networks and reaction systems exhibit isomorphic behaviours under the synchronous, general/fully asynchronous and most permissive semantics. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

In reaction systems, preimages and nth ancestors are sets of reactants leading to the production of a target set of products in either 1 or n steps, respectively. Many computational problems on preimages and ancestors, such as finding all minimum-cardinality nth ancestors, computing their size or counting them, are intractable. In this paper, we characterize all nth ancestors using a Boolean formula that can be computed in polynomial time. Once simplified, this formula can be exploited to easily solve all preimage and ancestor problems. This allows us to directly relate the difficulty of ancestor problems to the cost of the simplification so that new insights into computational complexity investigations can be achieved. In particular, we focus on two problems: (i) deciding whether a preimage/nth ancestor exists and (ii) finding a preimage/nth ancestor of minimal size. Our approach is constructive, it aims at finding classes of reactions systems for which the ancestor problems can be solved in polynomial time, in exact or approximate way. [ABSTRACT FROM AUTHOR]

When a person is concurrently interacting with different systems, the amount of cognitive resources required (cognitive load) could be too high and might prevent some tasks from being completed. When such human multitasking involves safety-critical tasks, such as in an airplane, a spacecraft, or a car, failure to devote sufficient attention to the different tasks could have serious consequences. For example, using a GPS with high cognitive load while driving might take the attention away for too long from the safety-critical task of driving the car. To study this problem, we define an executable formal model of human attention and multitasking in Real-Time Maude. It includes a description of the human working memory and the cognitive processes involved in the interaction with a device. Our framework enables us to analyze human multitasking through simulation, reachability analysis, and LTL and timed CTL model checking, and we show how a number of prototypical multitasking problems can be analyzed in Real-Time Maude. We illustrate our modeling and analysis framework by studying: (i) the interaction with a GPS navigation system while driving, (ii) some typical scenarios involving human errors in air traffic control (ATC), and (iii) a medical operator setting multiple infusion pumps simultaneously. We apply model checking to show that in some cases the cognitive load of the navigation system could cause the driver to keep the focus away from driving for too long, and that working memory overload and distraction may cause an air traffic controller or a medical operator to make critical mistakes. [ABSTRACT FROM AUTHOR]

Reaction systems are a qualitative formalism for the modelling of systems of biochemical reactions. In their original formulation, a reaction system executes in an environment (or context) that can supply it with new objects at each evolution step. The context drives the behaviour of a reaction system: it can provide different inputs to the system that can lead to different behaviours. In order to more faithfully deal with open systems, in this paper we propose a more powerful notion of context having not only the capability to provide objects, but also to absorb (or remove) objects at each evolution step. For such reaction systems with generalized context we investigate properties of dynamic causality by revising the previously proposed concept of formula based predictor. A formula based predictor is a Boolean formula characterising all contexts that lead to the production of a certain object after a given number of steps. In this paper, we revise the theory of formula based predictors in order to deal with reaction systems executed in a context of the new kind. As applications, we show an example of interaction between biochemical pathways and a reaction system modelling cell metabolism and respiration. [ABSTRACT FROM AUTHOR]

Reactions forming a pathway can be rewritten by making explicit the different molecular components involved in them. A molecular component represents a biological entity, such as a protein, in all its states (free, bound, degraded, etc.). Component identification, which is made possible by the mass conservation principle, allows subpathways to be computed to better understand the pathway functioning. In this paper we show the application of a previously-defined component identification algorithm to a number of real-world models to experimentally validate the approach; precisely, we have processed all the curated SBML models of the BioModels repository. In order to extend the applicability of our approach, we propose both (i) a preprocessing phase aiming at transforming a given pathway into a format suitable as input for the algorithm, and (ii) a dynamic model correction procedure that could allow some erroneous situations to be solved. We also prove the correctness of the preprocessing phase, and a property characterizing the structure of pathways with erroneous reactions. [ABSTRACT FROM AUTHOR]

We present Spatial P systems, a variant of P systems which embodies the concept of space and position inside a membrane. Objects in membranes are associated with positions. Rules specify, in the usual way, the objects which are consumed and the ones which are produced; in addition, they can specify the positions of the produced objects. Objects belong to two different sets: the set of ordinary objects and the set of mutually exclusive objects. Every position inside a membrane can accommodate an arbitrary number of ordinary objects, but at most one mutually exclusive object. We prove that Spatial P systems are universal even if only non-cooperating rules are allowed. We also show how Spatial P systems can be used to model the evolution of populations in presence of geographical separations. [ABSTRACT FROM AUTHOR]