LSB on Saturday, July 10th

09:00‑10:00 Session 1
Chair: James F. Lynch
Location: IF 4.31+4.33
09:00 Marta Kwiatkowska (University of Oxford)
Probabilistic Model Checking for Systems Biology

Probabilistic model checking is a formal verification technique that has been successfully applied to analyse performance of communication protocols and distributed systems. More recently, probabilistic model checking has also proved useful to analyse the dynamics of biological systems such as molecular signalling. One advantage of this approach is the rich selection of quantitative properties that can be automatically established; a limitation is the relatively small size of the models that can be handled at present. This lecture will focus on the challenges of applying probabilistic model checking to realistic examples in systems biology, outlining some of the available techniques.

10:30‑12:30 Session 2
Chair: James F. Lynch
Location: IF 4.31+4.33
10:30 Peter Gennemark (University of Gothenburg and Uppsala University)
Modelling Yeast Osmoregulation at Different Levels of Resolution

Real-world systems can be modelled at different levels of resolution. The choice is typically based on the amount and quality of available data, prior information of the system, and the research question in focus. In molecular biology, it is often the case that a single system is modelled at different levels of resolution, using various modelling techniques. To exemplify, we give an overview of proposed mathematical models of the response to osmotic stress in yeast. These models mainly differ in the choice of mathematical representation (e.g. Bayesian networks, ordinary differential equations or agent-based models), to what extent modelling is data-driven, and predictability. Based on this overview, we discuss how models with different levels of resolution can complement each other to gain insight into the system, the chronological order of the models in comparison to their resolution, and how hybrid models can be designed to achieve a reasonable balance between model resolution and model complexity for the specific modelling problem.

11:30 Ion Petre (Åbo Akademi University)
Molecular Self-Assembly Models of Variable Resolution

The cytoskeleton of eukaryotic cells is an intricate network of protein filaments that extends throughout the cytoplasm. There are three types of protein filaments: intermediate filaments (IFs), microtubules, and actin filaments. Together with other proteins that attach to them, they form a system of girders, ropes, and motors that gives the cell its mechanical strength, controls its shape, and drives and guides its movements. IFs have an important structural function in reinforcing the cells, organizing cells into tissues, and most importantly, distributing the tensile forces across the cells in a tissue. Contrary to the other protein filaments which are assembled from globular protein, IFs subunits are alpha-helical rods that assemble into rope-like filaments. Their assembly proceeds through a series of intermediate structures, which associate by lateral and end-to-end interactions. Major degenerative diseases of skin, muscle, and neurons are caused by disruptions of the IF cytoskeleton or its connections to other cell structures. A thorough understanding of the assembling principles of IFs can provide new insights into these abnormal conditions, as well as a better basis for diagnostic and possible treatment.

We focus in this talk on the quantitative kinetic strategies for the in vitro assembly of IFs from human vimentin proteins. We investigate a molecular model for it recently introduced in the literature. We associate to it a simple mass action-based mathematical model where all filaments are collected into a single variable, regardless of their length. We consider several knockdown mutant models where various combinations of assembly sub-mechanisms are analyzed separately to establish their contribution to the overall model kinetics. We then discuss how to increase the resolution of the model up to a given n>0 in such a way that filaments of length up to n are differentiated based on their length. We discuss the increase in the model complexity as a result of the increase in the model resolution. Finally, we briefly discuss a computer science-based modeling approach that, in the case of the intermediate filament assembly, yields exactly our model of maximum resolution.

14:00‑15:00 Session 3
Chair: James F. Lynch
Location: IF 4.31+4.33
14:00 Jasmin Fisher (Microsoft Research Cambridge)
Bio-Logic: The Challenges Facing Formal Modelling of Biology

As time goes by, it becomes more and more apparent that the puzzles of life involve more and more molecular pieces that fit together in increasingly complex ways. Biology is not an exact science. It is messy and noisy, and most often vague and ambiguous. We cannot assign clear rules to the way cells behave and interact with one another. And we often cannot quantify the exact amounts of molecules, such as genes and proteins, in the resolution of a single cell. To make matters worse (so to speak), the combinatorial complexity observed in biological networks (e.g., metabolic and signalling pathways) is staggering, which renders the comprehension and analysis of such systems a major challenge. Recent efforts to create executable models of complex biological phenomena entail great promise for new scientific discoveries, shading new light on the puzzle of life. At the same time, this ‘new wave of the future’ called Systems Biology forces Computer Science to stretch far and beyond, and in ways never considered before, in order to deal with the enormous complexity observed in biology. In this talk, I will summarize some of the major milestones on the way to conquer such complexity and to crack the logic behind biological processes --- Bio-Logic.

15:30‑17:30 Session 4
Chair: James F. Lynch
Location: IF 4.31+4.33
15:30 John K. Heath (University of Birmingham)
Protein Computing: a Phospho-Calculus?

Modeling biological pathways using computational tools based on process calculi has proved to be remarkably fruitful. Part of the reason for this is the ability to faithfully articulate ‘real world’ biological processes using a small number of primitives: molecules, states, transitions and compartments linked by a time evolution narrative. If a computer can behave like a pathway can a pathway compute? And if so how would they do it? In this light biological pathways are reactive computer systems which can exist in many possible and dynamically reconfigurable states. The standard biological view supposes a fixed (although not necessarily known) architecture and deterministic execution so if the questioned could be answered we would have new biological insight. Put another way does real biology exhibit the properties of a computing device? Here we explore the possibility that multi-site phosphorylation/ de-phosphorylation (ie state changes) provides a mechanistic basis for a computing device based on protein. We define some rules for the “phospho-calculus” based on known biological results and demonstrate the potential for computing functions. A phospho – computer would exhibit extreme parallelism; real-time responses, resilience to faults; distributed control and context-dependant responses. Could such a device be made? Perhaps it already has.

16:30 Steven Watterson (University of Edinburgh)
Signalling Pathway Logic in the Immune Response. How Can We Make Complex Problems More Tractable?

Cells interact with their environment through a complex and tentatively understood network of signalling pathways. This network of pathways acts as a signal processing layer that mediates and modulates the cellular response. The response, which is both genetic and proteomic in nature, targets the cell’s environment, but also targets the structure of the pathways themselves, making the cell a system with very complex feedback.

Here we discuss some of the practical challenges involved in untangling this network of signalling pathways and we present some recent results obtained from studying key pathways in the immune response. We explore many methodologies, amongst which are binary and multi-valued logics that we use to explore the dependency structure of pathway systems.