ABSTRACT. Symmetries arise naturally in rule-based models, and under various forms. Besides automorphisms between site graphs, which are usually built within the semantics, symmetries can take the form of pairs of sites having the same capability of interactions, of some protein variants behaving exactly the same way, or of some linear, planar, or 3D molecular complexes which could be see modulo permutations of their axis and/or mirror-image symmetries.

In this talk, we propose a unifying handling of symmetries in Kappa. We follow an algebraic approach, that is based on the single pushout semantics of Kappa. We model classes of symmetries as finite groups of transformations between site graphs, which are compatible with the notion of embedding (that is to say that it is always possible to restrict a transformation that is applied with the co-domain of an embedding to the domain of this embedding) and we provide some assumptions that ensure that symmetries are compatible with pushouts. Then, we characterize when a set of rules is symmetric with respect to a group of transformations and, in such a case, we give sufficient conditions so that this group of transformations induces a forward bisimulation and/or a backward bisimulation over the population semantics.

ABSTRACT. The response of a biomolecular system is usually investigated thanks to heterogenous and incomplete data. More precisely, to address a control a biological system, we may have at hand only partial knowledge about molecular interactions together with observations of a subset of molecules. The issue we wish to address is how can take benefit of this multi-scale amount of information. In this talk, we will explain how answer set programming can be used both to model in a uniform langage several problem of data integration and to solve difficult combinatorial problems related to heregeneity and data incompleteness. All together, these modelling and solving technologies allow identifying robust controllers of biological systems. We will illustrate this on issues about metabolic networks and logical signaling networks.

ABSTRACT. We study observational semantics for networks of chemical reactions as used in systems biology. Reaction networks without kinetic information, as we consider, can be identified with Petri nets. We present a new observational semantics for reaction networks that we call the attractor equivalence. The main idea of the attractor equivalence is to observe reachable attractors and reachability of an attractor divergence in all possible contexts.  The attractor equivalence can support powerful simplifications for reaction networks as we illustrate at the example of the TetOn system.  Alternative semantics based on bisimulations or traces, in contrast, do not support all needed simplifications.

ABSTRACT. We propose a novel approach for the formal verification of biological systems based on the use of a modal linear logic. 

We show how such a logic can be used, with worlds as instants of time, as an unified framework to encode both biological systems and temporal properties of their dynamic behaviour.

To illustrate our methodology, we consider a model of the P53/Mdm2 DNA-damage repair mechanism. We prove several properties that are important for such a model to satisfy and serve to illustrate the promise of our approach.  We formalize the proofs of these properties in the Coq Proof Assistant, with the help of a Lambda Prolog prover for partial automation of the proofs. 

ABSTRACT. In a simulation study aimed at developing a model that answers questions of interest about a target system, phases of model development and refinement are interwoven with phases of experimentation. During this process, a variety of experiments are typically executed, including parameter scans, optimization, or sensitivity analysis. Domain-specific languages, their expressiveness and succinctness, play a central role, not only to describe and revise a model, but also to specify and generate experiments, and thus to facilitate their reproduction. We will elucidate this role with the external domain-specific language ML-Rules (a rule-based multi-level modeling language for biochemical systems), SESSL (an internal domain-specific language for specifying simulation experiments), and a case study analyzing the impact of membrane dynamics on the Wnt signaling pathway.