22. – 27. Februar 2009, Dagstuhl-Seminar 09091

Formal Methods in Molecular Biology


Rainer Breitling (University of Groningen, NL)
David Gilbert (University of Glasgow, GB)
Monika Heiner (BTU Cottbus, DE)
Corrado Priami (Microsoft Research – University Trento, IT)

Auskunft zu diesem Dagstuhl-Seminar erteilt

Dagstuhl Service Team


Dagstuhl Seminar Proceedings DROPS
Dagstuhl's Impact: Dokumente verfügbar

Seminar Relevant Information


The Life Sciences, and in particular Molecular Biology, are a rather new application area for advanced computational concepts. Living systems, from cells to entire organisms, function by the complex, dynamic interaction of a large number of components (proteins, nucleic acids, metabolites). The set of “molecular players” continues to be explored in genome sequencing projects and related experiments. Their physical and regulatory relationships are determined in detailed molecular studies and represented in cellular “wiring diagrams” and “flow charts”. Such schematic pictures are used by biologists to reason about the expected behavior of biological systems, e.g. in response to disease processes or drug treatment. They can also be translated into quantitative mathematical descriptions of the system. With the recent explosion of biological knowledge, such approaches need to become more common and more formalized.

Formal logical models play an increasing role in the newly emerging field of Systems Biology. Compared to the classical, well-established approach of modeling biological processes using continuous and stochastic differential equations, formal logical models offer a number of important advantages: Easy compositionality, which allows the generation and management of large cellular models from a number of pre-defined and reliably manipulated building blocks; model checking for the rigorous exploration of model consistency, including the comprehensive exploration of state-space and the identification of necessary additions to an existing system description; unambiguous visualization based on the strictly enforced syntax of the modeling language. In addition, a number of recent studies have explored the combination of formal logical models with continuous and stochastic differential equation models, showing important relationships between the two approaches and further expanding the expressivity of the resulting models.

Many different formal modeling paradigms have been applied to molecular biology, each with its own community, formalisms and tools. The present seminar is intended to stimulate closer interaction within the field and to create a common platform for discussion. The program covered a large fraction of the diversity of formal modeling in molecular biology, including sessions on

  • ordinary differential equation models,
  • process calculi,
  • state machines
  • process algebras,
  • logics,
  • constraints-based modeling.

A major area of interest was the debate over the relative merits of the different approaches to modeling that were presented in the meeting, and the emerging interest in directly executable specifications in terms of the analytical techniques that can be used. In addition to computational modelers, the participants also included a number of high-profile systems biologists who presented important new developments at the experimental side of the life sciences in keynote speeches and provided crucial critical feedback on the validity of the formal modeling concepts. The meeting was particularly friendly and productive, and had a good mix of young and established researchers. Numerous new collaborations were established across the fields and are now followed up in longer-term research projects.

Modeling Competition

A central feature of the seminar was a modeling competition (with a highly collaborative flavor) of various modeling paradigms. This provided a unique opportunity for participants to directly compare their approaches and find common ground. It turned out that Dagstuhl is an ideal place to encourage this kind of productive and challenging interaction: new teams started to form already on the first day and many new analyses or collaborations took place during intense personal interactions and in small groups in front of the computer.

All contributions to the competition were evaluated by a committee of judges, supplemented by a public vote, based on informal presentations during the conference. This turned out to be a challenging task, as many contributions were of excellent quality, including some by teams that had just met for the first time at the seminar.

All votes were statistically evaluated with software based on the algorithm presented in [BAAH04], revealing an extremly good correlation between the total assessment by the committee of judges and the total assessment by the public vote.

Dagstuhl-Seminar Series


  • Modeling/simulation
  • Networks
  • Semantics/specification/formal Methods
  • Verifcation/logic


  • Petri nets
  • Statecharts
  • Pi-calculus
  • Concurrency
  • Constraints
  • Process algebra
  • Model checking
  • Boolean networks
  • Communicating automata
  • Hybrid models
  • Differntial equations
  • Stochastic modeling


Bücher der Teilnehmer 

Buchausstellung im Erdgeschoss der Bibliothek

(nur in der Veranstaltungswoche).


In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.


Download Übersichtsflyer (PDF).


Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.