February 22 – 27 , 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)

For support, please contact

Dagstuhl Service Team


Dagstuhl Seminar Proceedings DROPS
List of Participants
Dagstuhl's Impact: Documents available

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


In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.


Download overview leaflet (PDF).

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.


Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.