Search

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]

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

Biochemical pathways are abstract descriptions of the interactions among the molecular species involved in a cellular process. Different molecular species mentioned in a pathway often represent different states of the same biological entity, such as the unbound and bound states of a certain molecule. Hence, a pathway can be seen as a network of interactions between entities changing state synchronously by means of reactions. We consider such biological entities as pathway components. We define a semi-automatic algorithm to infer the components from their interactions described in the pathway. In case the interactions are not sufficient to resolve all the reactions, help from a domain expert may be needed to resolve any ambiguity that should arise. As an example of application, we apply the algorithm to a model of the EGF signaling pathway from the literature in order to identify its components. From the theoretical point of view, we formally prove the correctness of the algorithm, its termination under any input pathway and a (weak) confluence property. [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]

We propose sync-programs, an automata-based formalism for the description of biological systems, and a modular verification technique for such a formalism that allows properties expressed in the universal fragment of CTL to be verified on suitably chosen fragments of models, rather than on whole models. As an application we show the modelling of the lac operon regulation process and the modular verification of some properties. Verification of properties is performed by using the NuSMV model checker and we show that by applying our modular verification technique we can verify properties in shorter times than those necessary to verify the same properties in the whole model. [ABSTRACT FROM AUTHOR]

The Calculus of Looping Sequences is a formalism for describing evolution of biological systems by means of term rewriting rules. We propose to enrich this calculus by labelling elements of sequences. Since two elements with the same label are considered to be linked, this allows us to represent protein interaction at the domain level. Well-formedness of terms are ensured by both a syntactic constraint and a type system: we discuss the differences between these approaches through the description of a biological system, namely the EGF pathway. [ABSTRACT FROM AUTHOR]

A formal model for diagnostics of biological systems modelled as P systems is presented. We assume the presence of some biologically motivated changes (frequently pathological) in the systems behavior and investigate when these changes could be diagnosed by an external observer by exploiting some techniques originally developed for reasoning on system security. [ABSTRACT FROM AUTHOR]

Abstract: In this paper, we present a formalization of biological systems based on multiset rewriting and we investigate the use of abstract interpretation on its semantics. We consider a probabilistic semantics, which is well suited to represent the non-deterministic evolution of real biological systems. Abstract interpretation allows us to deal with systems in which the kinetic rates of the evolution rules are not precisely known. On the (abstract) systems, we perform probabilistic model checking obtaining lower and upper bounds for the probabilities of reaching states satisfying the given properties. We apply abstract probabilistic model checking to verify reachability properties in a model of tumor growth. [Copyright &y& Elsevier]

Abstract: We propose a variant of the CCS process algebra with new features aiming at allowing multiscale modeling of biological systems. In the usual semantics of process algebras for modeling biological systems actions are instantaneous. When different scale levels of biological systems are considered in a single model, one should take into account that actions at a level may take much more time than actions at a lower level. Moreover, it might happen that while a component is involved in one long lasting high level action, it is involved also in several faster lower level actions. Hence, we propose a process algebra with operations and with a semantics aimed at dealing with these aspects of multiscale modeling. We give both a reduction semantics and an SOS semantics for our new algebra with a result of operational correspondence between the two. Moreover, we study behavioral equivalences for such an algebra and give some examples. [Copyright &y& Elsevier]

Abstract: We introduce Stochastic String MultiSet Rewriting (sSMSR), and propose this formalism as an intermediate language for the simulation of biomolecular systems. Higher level formalisms for biological systems description can be translated into sSMSR, and the features of sSMSR allow the development of efficient simulators. In this paper, we show the encoding into sSMSR of two formalisms for the description of biological systems, namely Stochastic CLS and the Stochastic -calculus. We prove soundness and completeness of both the encodings. [Copyright &y& Elsevier]