Workshop on
Formal Methods in Systems Biology
University of Luxembourg, Luxembourg, Nov 28, 2017

This workshop aims at sharing the research experiences in the interdisciplinary fields of formal methods and systems biology. We invite researchers from University of Twente, Åbo Akademi University, and University of Luxembourg to present their work in these fields.


Workshop Programs

 

08:45-09:00

registration

Session I: Tools and Approaches for Analysing Biological Systems

09:00-09:45

Rom Langerak (University of Twente)
Discretization of continuous dynamical systems using UPPAAL

09:45-10:30

Jaco van de Pol (University of Twente)
ANIMO+ECHO: Animated Modeling of an Executable Chondrocyte

10:30-10:50

coffee break

10:50-11:35

Sébastien De Landtsheer (University of Luxembourg)
FALCON: a Matlab toolbox for the fast contextualization of logical networks

11:35-12:20

Philippe Lucarelli (University of Luxembourg)
Analyzing molecular changes during drug resistance of melanoma using a Dynamic Bayesian Network approach

12:20-14:00

lunch

Session II: Network Controllability

14:00-14:45

Ion Petre (Åbo Akademi University)
Network controllability: theory and applications

14:45-15:30

Vladimir Rogojin (Åbo Akademi University)
NetControl4BioMed - Automatic discovery of combined drug therapy

15:30-15:50

coffee break

15:50-16:35

Qixia Yuan (University of Luxembourg)
Taming asynchronous for attractor detection in large Boolean networks

16:35-17:20

Soumya Paul (University of Luxembourg)
A decomposition-based control of Boolean networks

 

Venue

 

The nearest hotel from the venue is Hotel Ibis Esch Belval, which is 7 mins walking to the venue. The hotel is just outside the Belval train station (Belval-Université, Gare). The most convenient way to reach the hotel and the venue is by train. Train timetables and further information can be found on the official website CFL.lu. A map of the campus is available here and shows how to reach the building Maison du Savoir. Bus 16 and 29 (timetables available here: 16, 29) connect the airport with the train station in Luxembourg city and the bus ticket can be used for the train too (a 2/4 hours ticket can be purchased on the bus for 2/4 euros).

 

 

Abstract of Talks

 

Speaker: Rom Langerak
University of Twente
Title: Discretization of continuous dynamical systems using UPPAAL
Abstract:
We want to enable the analysis of continuous dynamical systems (where the evolution of a vector of continuous state variables is described by differential equations) by model checking. We do this by showing how such a dynamical system can be translated into a discrete model of communicating timed automata that can be analyzed by the UPPAAL tool.

The basis of the translation is the well-known Euler approach for solving differential equations where we use fixed discrete value steps instead of fixed time steps. Each state variable is represented by a timed automaton in which the delay for taking the next value is calculated on the fly using the differential equations.  The state variable automata proceed independently but may notify each other when a value step has been completed; this leads to a recalculation of delays.

The approach has been implemented in the tool ANIMO for analyzing biological kinase networks in cells. This tool has been used in actual biological research on osteoarthritis dealing with systems where the dimension of the state vector (the number of nodes in the network) is in the order of one hundred.

 

Speaker: Jaco van de Pol
University of Twente
Title: ANIMO+ECHO: Animated Modeling of an Executable Chondrocyte
Abstract:
Together with biologists, we have designed ANIMO, a tool for the interactive modeling of cell signaling networks. ANIMO is a plugin of Cytoscape, in which biologists are used to draw static signaling networks. We provided analysis of the network dynamics by a translation to Uppaal's Timed Automata.

The tool has been used to perform in silico experiments on human chondrocytes. To this end, we modeled ECHO, the Executable CHOndrocyte, with ANIMO. We will explain the workflow of these in silico experiments, and report on their results.

 

Speaker: Sébastien de Landtsheer
Title: FALCON: a Matlab toolbox for the fast contextualization of logical networks

Abstract: Mathematical modelling of regulatory networks allows the discovery of knowledge at the systems level. However, existing modelling tools are often computation-heavy and do not offer intuitive ways to explore the model, to test hypotheses or to interpret the results biologically. We have developed a computational approach to contextualize logical models of regulatory networks with biological measurements based on a probabilistic description of rule-based interactions between the different molecules. We propose a Matlab toolbox, FALCON, to automatically and efficiently build and contextualize networks, which includes a pipeline for conducting parameter analysis, knockouts and easy and fast model investigation. Contextualized models can then provide qualitative and quantitative information about the network and suggest hypotheses about biological processes. We demonstrate the possible applications of a series of improvements relative to the published version.

 

Speaker: Philippe Lucarelli
University of Luxembourg
Title: Analyzing molecular changes during drug resistance of melanoma using a Dynamic Bayesian Network approach
Abstract: Despite remarkable scientific and clinical efforts in melanoma research, the incidence of malignant melanoma strongly increased over the last decades. While metastatic melanoma is often characterized by mutation of the kinase BRAF, the large number of different mutations represent the biggest challenge in our understanding of the disease. These mutations strongly increase the aggressiveness of the tumor offering a poor prognosis for the patient. The response to conventional therapeutic treatment usually lasts for a few months only, until drug resistance occurs, leading to tumor relapse which often coincides with increased proliferation and migration rates.

The goal of this study is to identify the critical mechanisms leading to drug resistance in A375 melanoma cell lines. For an in-depth analysis of signal transduction pathways that might confer therapy resistance, we apply a systems biology approach based on a Dynamic Bayesian Network (DBN), which integrates steady-state time-course data into a mathematical model, to identify the optimal drug combination for a successful treatment.

A mathematical model analyzing the crosstalk interactions for the death ligand TRAIL-induced apoptotic signal transduction has been established and refined based on newly acquired experimental time-course data. We employ a DBN modeling approach to analyze the molecular interactions and regulations among signaling molecules with minimal parameterization. This modeling approach allowed us to identify cell type specific reactions.

Currently, we were able to dissect the critical crosstalk mechanisms of the TRAIL signal transduction pathways by DBN modelling and are able to show the influence of the different pathways for each steady-state.

In the next step, we aim to identify which drug combinations render resistant melanoma cells sensitive towards apoptotic cell death. The newly identified targets and combinations will be validated in selected melanoma in vitro models.

 

Speaker: Ion Petre
Computational Biomodeling Laboratory,
Department of Computer Science, Åbo Akademi
Title: Network controllability: theory and applications
Abstract:
The intrinsic robustness of living systems against perturbations is a key factor that explains why many single-target drugs have been found to provide poor efficacy or to lead to significant side effects. Rather than trying to design selective ligands that target individual receptors only, network polypharmacology aims to modify multiple cellular targets to tackle the compensatory mechanisms and robustness of disease-associated cellular systems, as well as to control unwanted off-target side effects that often limit the clinical utility of many conventional drug treatments. However, the exponentially increasing number of potential drug target combinations makes the pure experimental approach quickly unfeasible, and translates into a need for algorithmic design principles to determine the most promising target combinations to effectively control complex disease systems, without causing drastic toxicity or other side-effects. Building on the increased availability of disease-specific essential genes, we concentrate on the target structural controllability problem, where the aim is to select a minimal set of driver/driven nodes which can control a given target within a network. That is, for every initial configuration of the system and any desired final configuration of the target nodes, there exists a finite sequence of input functions for the driver nodes such that the target nodes can be driven to the desired final configuration. We investigated this approach in some pilot studies linking FDA-approved drugs with cancer cell-line-specific essential genes, with some very promising results.

 

Speaker: Vladimir Rogojin
Computational Biomodelling Laboratory
Department of Computer Science, Åbo Akademi
Title: NetControl4BioMed - Automatic discovery of combined drug therapy
Abstract: 
Network controllability focuses on discovering combinations of external interventions that can drive a biological system to a desired configuration. In practice, this approach translates into finding a combined multi-drug therapy in order to induce a desired response from a cell; this can lead to developments of novel therapeutic approaches for systemic diseases like cancer. We present here a novel bioinformatics data analysis pipeline called NetControl4BioMed based on the structural control of linear networks. Our pipeline generates novel molecular interaction networks by combining pathway data from various public databases starting from the user's query. The pipeline then identifies a minimal set of nodes needed to control a given, user-defined set of disease-specific essential proteins in the network. We anticipate that our pipeline can be used by researchers for controlling and better understanding of molecular interaction networks through combinatorial multi-drug therapies, for more efficient therapeutic approaches and personalized medicine.

 

Speaker: Qixia Yuan
University of Luxembourg
Title: Taming asynchronous for attractor detection in large Boolean networks
Abstract: Boolean networks is a well-established formalism for modelling biological systems. A vital challenge for analysing a Boolean network is to identify all the attractors. This becomes more challenging for large asynchronous Boolean networks, due to the asynchronous updating scheme. Existing methods are prohibited due to the well-known state-space explosion problem in large Boolean networks. We tackle this challenge by proposing a SCC-based decomposition method. We prove the correctness of our proposed method and demonstrate its efficiency with two real-life biological networks.

 

Speaker: Soumya Paul
University of Luxembourg
Title: A decomposition-based control of Boolean networks
Abstract: We describe an approach towards the computation of minimal control in boolean networks based on the structure of their network graphs and highlight the applicability of the approach and its future extensions.

 

Contact

 

Qixia Yuan (firstname.lastname@uni.lu)