Search

Reaction Systems (RSs) are a computational framework inspired by biochemical mechanisms. An RS defines a finite set of reactions over a finite set of entities (molecules, proteins, etc). Starting from an initial set of entities (the initial state), a computation is performed by applying all reactions to a state in order to produce the following state, giving rise to a sequence of sets of entities. RSs have shown to be a general computational framework whose application ranges from the modeling of biological phenomena to molecular chemistry and computer science. In this paper, we contribute to research on the application of RSs for modeling biological systems. We consider the problem of modeling hemostasis, for which several models have been defined, starting from the 1960s. Previous models are based on sets of ordinary differential equations, while we develop a discrete model in RSs for pathways of the secondary hemostasis. Then, we implement our model in BioReSolve, a computational framework for RSs that we have previously defined which provides tools for the specification and verification of properties. By using the tools in BioReSolve we derive important observations on the model behaviour for hemostasis, and in particular, we study the role of three important inhibitors, verifying that their presence or absence leads to phenomena such as thrombophilia, or thromboembolism, or excessive coagulation, etc. We can also study computationally the causality relations between the molecules involved in the reactions showing which entities play a fundamental role, thus contributing to the design of more effective and specialized drugs. Our work can hence help to show how to model complex biological systems in RSs and derive computationally and biologically relevant properties of the systems. [ABSTRACT FROM AUTHOR]

Reaction Systems (RSs) are a successful computational framework for modeling systems inspired by biochemistry. An RS defines a set of rules (reactions) over a finite set of entities (e.g., molecules, proteins, genes, etc.). A computation in this system is performed by rewriting a finite set of entities (a computation state) using all the enabled reactions in the RS, thereby producing a new set of entities (a new computation state). The number of entities in the reactions and in the computation states can be large, making the analysis of RS behavior difficult without a proper automated support. In this paper, we use the Maude language—a programming language based on rewriting logic—to define a formal executable semantics for RSs, which can be used to precisely simulate the system behavior as well as to perform reachability analysis over the system computation space. Then, by enriching the proposed semantics, we formalize a forward slicer algorithm for RSs that allows us to observe the evolution of the system on both the initial input and a fragment of it (the slicing criterion), thus facilitating the detection of forward causality and influence relations due to the absence/presence of some entities in the slicing criterion. The pursued approach is illustrated by a biological reaction system that models a gene regulation network for controlling the process of differentiation of T helper lymphocytes. [ABSTRACT FROM AUTHOR]

Concurrent Constraint Programming (CCP) is a declarative model for concurrency where agents interact by telling and asking constraints (pieces of information) in a shared store. Some previous works have developed (approximated) declarative debuggers for CCP languages. However, the task of debugging concurrent programs remains difficult. In this paper we define a dynamic slicer for CCP (and other language variants) and we show it to be a useful companion tool for the existing debugging techniques. We start with a partial computation (a trace) that shows the presence of bugs. Often, the quantity of information in such a trace is overwhelming, and the user gets easily lost, since she cannot focus on the sources of the bugs. Our slicer allows for marking part of the state of the computation and assists the user to eliminate most of the redundant information in order to highlight the errors. We show that this technique can be tailored to several variants of CCP, such as the timed language ntcc , linear CCP (an extension of CCPbased on linear logic where constraints can be consumed) and some extensions of CCP dealing with epistemic and spatial information. We also develop a prototypical implementation freely available for making experiments. [ABSTRACT FROM AUTHOR]

Background: Biochemical reactions are often modelled as discrete-state continuous-time stochastic processes evolving as memoryless Markov processes. However, in some cases, biochemical systems exhibit non-Markovian dynamics. We propose here a methodology for building stochastic simulation algorithms which model more precisely non-Markovian processes in some specific situations. Our methodology is based on Constraint Programming and is implemented by using Gecode, a state-of-the-art framework for constraint solving. Results: Our technique allows us to randomly sample waiting times from probability density functions that not necessarily are distributed according to a negative exponential function. In this context, we discuss an important case-study in which the probability density function is inferred from single-molecule experiments that describe the distribution of the time intervals between two consecutive enzymatically catalysed reactions. Noticeably, this feature allows some types of enzyme reactions to be modelled as non-Markovian processes. Conclusions: We show that our methodology makes it possible to obtain accurate models of enzymatic reactions that, in specific cases, fit experimental data better than the corresponding Markovian models. [ABSTRACT FROM AUTHOR]

Timed Concurrent Constraint Programming (tcc) is a declarative model for concurrency offering a logic for specifying reactive systems, i.e., systems that continuously interact with the environment. The universal tcc formalism (utcc) is an extension of tcc with the ability to express mobility. Here mobility is understood as communication of private names as typically done for mobile systems and security protocols. In this paper we consider the denotational semantics for tcc, and extend it to a “collecting” semantics for utcc based on closure operators over sequences of constraints. Relying on this semantics, we formalize a general framework for data flow analyses of tcc and utcc programs by abstract interpretation techniques. The concrete and abstract semantics that we propose are compositional, thus allowing us to reduce the complexity of data flow analyses. We show that our method is sound and parametric with respect to the abstract domain. Thus, different analyses can be performed by instantiating the framework. We illustrate how it is possible to reuse abstract domains previously defined for logic programming to perform, for instance, a groundness analysis for tcc programs. We show the applicability of this analysis in the context of reactive systems. Furthermore, we also make use of the abstract semantics to exhibit a secrecy flaw in a security protocol. We also show how it is possible to make an analysis which may show that tcc programs are suspension-free. This can be useful for several purposes, such as for optimizing compilation or for debugging. [ABSTRACT FROM PUBLISHER]

Languages that integrate functional and logic programming with a complete operational semantics are based on narrowing, a unification-based goal-solving mechanism which subsumes the reduction principle of functional languages and the […]

Needed narrowing is a complete and optimal operational principle for modern declarative languages which integrate the best features of lazy functional and logic programming. We investigate the formal relation between needed narrowing and another (not so lazy) narrowing strategy which is the basis for popular implementations of lazy functional logic languages. We demonstrate that needed narrowing and lazy narrowing are computationally equivalent over the class of uniform programs. We also introduce a complete refinement of lazy narrowing, called uniform lazy narrowing, which is still equivalent to needed narrowing over the aforementioned class. Since actual implementations of functional logic languages are based on the transformation of the original program into a uniform one—which is then executed using a lazy narrowing strategy—our results can be thought of as a formal basis for the correctness of these implementations. [ABSTRACT FROM PUBLISHER]

In the area of Natural Computing, Reaction Systems (RSs) are a qualitative abstraction inspired by the functioning of living cells, suitable to model the main mechanisms of biochemical reactions. RSs interact with a context, and pose challenges for modularity, compositionality, extendibility and behavioural equivalence. In this paper we define a modular encoding of RSs as processes in the chained Core Network Algebra (cCNA), which is a new variant of the link-calculus. The encoding represents the behaviour of each entity separately and preserves faithfully their features, and we prove its correctness and completeness. Our encoding provides a Labelled Transition System (LTS) semantics for RSs. Based on the LTS semantics, we adapt the classical notion of bisimulation to define a novel equivalence, called bio-similarity, for studying properties of RSs. In particular, we define a new assertion language based on regular expressions, which allows us to specify the properties of interest, and use it to extend Hennessy-Milner logic to our setting. We prove that our bio-similarity relation and the logical equivalence, that are defined parametrically on some assertion of interest, coincide. Finally, we claim that our encoding contributes to increase the expressiveness of RSs, by exploiting the interaction among different RSs. [ABSTRACT FROM AUTHOR]

Reaction Systems (RSs) are a successful computational framework inspired by biological systems. A RS pairs a set of entities with a set of reactions over them. Entities can be used to enable or inhibit each reaction, and are produced by reactions. Entities can also be provided by an external context sequence to simulate in silico biological experiments. In this paper we define an extension of RSs considering nondeterministic and recursive context operators, and give an original labelled transition system (LTS) for extended RSs in the structural operational semantics (SOS) style. Thanks to extended contexts, a single LTS can now account for several biological experiments. The rich information recorded in transition labels is useful to guarantee the compositionality of SOS inference rules as well as to define an assertion language to tailor behavioural and logical equivalences on some specific properties or entities. The SOS rules have been also exploited to design a flexible prototype implementation in logic programming that allows to inspect the LTS and to extract useful information when performing experiments on a RS. Our implementation provides a rapid prototyping tool for (extensions of) RSs, with a user friendly online interface to our interpreter. A parser allows to introduce the logical formulas and the contexts using the usual comfortable concrete syntax. The user can visualise and inspect the LTS for a RS and make some analysis of its underlying computation patterns, can check if the main RS satisfies a given property and if it is equivalent to a second adversarial RS. Finally, the SOS approach is suited to drive additional enhancements of RSs. [ABSTRACT FROM AUTHOR]