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 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.

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.

BACKGROUND: Anti-tumor therapies aim at reducing to zero the number of tumor cells in a host within their end or, at least, aim at leaving the patient with a sufficiently small number of tumor cells so that the residual tumor can be eradicated by the immune system. Besides severe side-effects, a key problem of such therapies is finding a suitable scheduling of their administration to the patients. In this paper we study the effect of varying therapy-related parameters on the final outcome of the interplay between a tumor and the immune system. RESULTS: This work generalizes our previous study on hybrid models of such an interplay where interleukins are modeled as a continuous variable, and the tumor and the immune system as a discrete-state continuous-time stochastic process. The hybrid model we use is obtained by modifying the corresponding deterministic model, originally proposed by Kirschner and Panetta. We consider Adoptive Cellular Immunotherapies and Interleukin-based therapies, as well as their combination. By asymptotic and transitory analyses of the corresponding deterministic model we find conditions guaranteeing tumor eradication, and we tune the parameters of the hybrid model accordingly. We then perform stochastic simulations of the hybrid model under various therapeutic settings: constant, piece-wise constant or impulsive infusion and daily or weekly delivery schedules. CONCLUSIONS: Results suggest that, in some cases, the delivery schedule may deeply impact on the therapy-induced tumor eradication time. Indeed, our model suggests that Interleukin-based therapies may not be effective for every patient, and that the piece-wise constant is the most effective delivery to stimulate the immune-response. For Adoptive Cellular Immunotherapies a metronomic delivery seems more effective, as it happens for other anti-angiogenesis therapies and chemotherapies, and the impulsive delivery seems more effective than the piece-wise constant. The expected synergistic effects have been observed when the therapies are combined.

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

The Java virtual machine embodies a verifier that performs a set of checks on Java bytecode programs before their execution. The verifier carries out an efficient data-flow analysis applied to a type-level abstract interpretation of the code. The implementations of the bytecode verifier presented a significant problem with programs compiled with the Sun Java compiler (until version 1.4.1): there were legal Java programs which were correctly compiled into a bytecode that was rejected by the verifier. The problem was fixed by removing, in version 1.4.2 and following, some interesting features in the compilation of the try-finally Java construct. Because removing such features has a cost in terms of memory space, in this paper we propose to enhance the bytecode verifier to accept such programs, maintaining the space efficiency of the previous versions of the compiler. We define an abstract interpretation framework in which we model the enhanced version of the verifier. The defined abstract interpretation framework can be considered a good basis for other static analyses of bytecode programs.

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.

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 consid

P Systems are computing devices inspired by the structure and the functioning of a living cell. A P System consists of a hierarchy of membranes, each of them containing a multiset of objects, a set of evolution rules, and possibly other membranes. Evolution rules are applied to the objects of the same membrane with maximal parallelism. In this paper we present an extension of P Systems, called P Systems with Membrane Channels (PMC Systems), in which membranes are enriched with channels and objects can pass through a membrane only if there are channels on the membrane that enable such a passage. We show that PMC Systems are universal even if only the simplest form of evolution rules is considered, and we give two application examples.

To study systems whose dynamics changes with time, an extension of timed P systems is introduced in which evolution rules may vary with time. The proposed model is a timed automaton with a discrete time domain and in which each state is a timed P system. A result on expressive power and on features of the formalism sufficient for full expressiveness is proved and, as an application example, the model of an ecological system is given.

Abstract Bisimulations are well-established behavioural equivalences that are widely used to study properties of computer science systems. Bisimulations assume the behaviour of systems to be described as labelled transition systems, and properties of a system can be verified by assessing its bisimilarity with a system one knows to enjoy those properties. In this paper we show how semantics based on labelled transition systems and bisimulations can be defined for two formalisms for the description of biological systems, both capable of describing membrane interactions. These two formalisms are the Calculus of Looping Sequences (CLS) and Brane Calculi, and since they stem from two different approaches (rewrite systems and process calculi) bisimulation appears to be a good candidate as a general verification method. We introduce CLS and define a labelled semantics and bisimulations for which we prove some congruence results. We show how bisimulations can be used to verify properties by way of two examples: the description of the regulation of lactose degradation in Escherichia coli and the description of the EGF signalling pathway. We recall the PEP calculus (the simplest of Brane Calculi) and its translation into CLS, we define a labelled semantics and some bisimulation congruences for PEP processes, and we prove that bisimilar PEP processes are translated into bisimilar CLS terms.

This paper presents an approach to analyze stack-based assembly code with respect to leakages of private information. We consider systems implementing a multilevel security policy, where the security levels form a lattice. The approach is based on abstract interpretation of the operational semantics. We consider a representative subset of instructions of conventional stack-based assembly languages. We define a collecting small-step semantics of the language, enhanced to convey the level of the information flow during execution: this is accomplished by annotating each value with the level of the information on which it depends. Then we define an abstract semantics of the language that abstracts from actual data and maintains only the annotations on the security level. We give sufficient conditions the abstract semantics must satisfy to ensure secure information flow. The use of abstract interpretation allows, on one side, being semantics based, to accept as secure a wide class of programs, and on the other side, being rule based, to be automated fully. In fact we show how it may be combined with a model checking technique, where the conditions for security are described by temporal logic formulae that can be automatically checked on the abstract representation of the program.

The Java Virtual Machine embodies a verifier which performs a set of checks on bytecode programs before their execution. The verifier performs a data-flow analysis applied to a type-level abstract interpretation of the code. The current implementations of the bytecode verifier present a significant problem: there are legal Java programs which are correctly compiled into a bytecode that is rejected by the verifier. Also the more powerful verification techniques proposed in several papers suffer from the same problem. In this paper we propose to enhance the bytecode verifier to accept such programs, maintaining the efficiency of current implementations. The enhanced version is based on a domain of types which is more expressive than the one used in standard verification.

LOTOS is a formal specification language for concurrent and distributed systems. Basic LOTOS is the version of LOTOS without value-passing. A widely used approach to the verification of temporal properties is model checking. Often, in this approach the formal specification is translated into a labeled transition system on which formulae expressing properties are checked. A problem with this verification technique is state explosion: concurrent systems are often represented by automata with a prohibitive number of states. In this paper we show how, given a set ρ of actions, it is possible to automatically obtain for a Basic LOTOS program a reduced transition system to which only the arcs labeled by actions in ρ belong. The set ρ of actions plays a fundamental role in conjunction with a temporal logic defined by the authors in a previous paper: selective mu-calculus. The reduced system with respect to ρ preserves the truth value of all selective mu-calculus formulae with actions from the set ρ. We act at both syntactic and semantic levels. From a syntactic point of view, we define a set of transformation rules obtaining a smaller program. On the semantic side, we define a non-standard semantics which dynamically reduces the transition system during generation. We present a tool implementing both the syntactic and the semantic reduction. Copyright © 1999 John Wiley & Sons, Ltd.

The goal of this paper is to construct a semantic basis for the abstract interpretation of Prolog programs. Prolog is a well-known logic programming language which applies a depth-first search strategy in order to provide a practical approximation of Horn clause logic. While pure logic programming has clean fixpoint, model-theoretic and operational semantics the situation for Prolog is different. Difficulties in capturing the declarative meaning of Prolog programs have led to various semantic definitions which attempt to encode the search strategy in different mathematical frameworks. However, semantic based analyses of Prolog are typically achieved by abstracting the more simple but less precise declarative semantics of pure logic programs. We propose instead to model Prolog control in a simple constraint logic language which is presented together with its declarative and operational semantics. This enables us to maintain the usual approach to declarative semantics of logic programs while capturing control aspects such as search strategy and selection rule.

The theory of abstract interpretation provides a formal framework to develop advanced dataflow analysis tools. The idea is to define a nonstandard semantics which is able to compute, in finite time, an approximated model of the program. In this paper, we define an abstract interpretation framework based on a fixpoint approach to the semantics. This leads to the definition, by means of a suitable set of operators, of an abstract fixpoint characterization of a model associated with the program. Thus, we obtain a specializable abstract framework for bottom-up abstract interpretations of definite logic programs. The specialization of the framework is shown on two examples, namely, gound-dependence analysis and depth-kanalysis.