TOP
Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminars
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Publishing
Within this website:
External resources:
dblp
Within this website:
External resources:
  • the dblp Computer Science Bibliography


Dagstuhl Seminar 10271

Verification over discrete-continuous boundaries

( Jul 04 – Jul 09, 2010 )

(Click in the middle of the image to enlarge)

Permalink
Please use the following short url to reference this page: https://www.dagstuhl.de/10271

Organizers

Contact

Sponsors
The Dagstuhl Foundation gratefully acknowledges the donation from


Summary

The seminar aimed at bringing together researchers working on the analysis of systems, where the analysis uses abstractions or embeddings from discrete to continuous or from continuous to discrete domains. Such analysis across discrete-continuous boundaries appears in a large spectrum of practical and industrially relevant applications. They often play a pivotal role to arrive at useful analysis results. On the other hand, they necessarily incur some error, and make the question how to give proper correctness guarantees for the system behavior a notoriously difficult one.

Seminar Context

Formal models of computation have for long been considered independent of the concrete world, viewing hardware and software as discrete models of computation. However, there is nowadays a striking need to incorporate continuous physical reality, caused by very different trends and challenges, including embedded and cyber-physical systems, deep sub-micron effects, biology-inspired computation, or analog and mixed-signal circuits design.

On the other hand there are many application areas of scientific computing, that have traditionally treated their matter as of a mostly continuous nature, but are starting to see the need to consider discrete structures, e.g. in some parts of cell biology and chemical kinetics, in numerical mathematics, and in distributed control. In these areas it also occurs more and more, that a shift from (or to) a discrete interpretation to (or from) a continuous interpretation is a major step in model analysis. Often analyzing a continuous system by computer aided tools requires to switch to an appropriately truncated discrete approximation. Conversely, there are cases where the opposite strategy has proven succesful: A prominent example of this is integer linear programming, where e.g. the cutting plane method proceeds via an iteration over LP problems working on a continuous domain. Other examples e.g. emerge in the area of mean field analysis applied to distributed computing, where the interaction of large quantities of discrete components is summarized by an averaging continuous value.

Seminar Objectives

In the future, but even nowadays, it is becoming rather common in modelling and analysis to switch between a discrete and a continuous view on a system. The consequences of such an abstraction step are often overlooked however, especially if several of these switches occur during the modelling. For instance, a fluid mixture of chemical substrates, consisting of a discrete number of molecules, is represented by a differential equation with real valued parameters, which are analyzed by simulating the system in a floating point representation and in discrete time steps. Each of the switches induces an error in the analysis, and the effect on the accuracy of the analysis results might be extreme.

This seminar aimed at bringing together, for the first time, researchers from independent areas working on the boundary of discrete and continuous modelling and verification, with the intention to cross-fertilize their individual research topics.

We were striving for a broad coverage of instances where one or several of these boundary crossings occur, paired with technical discussions about possibilities to quantify induced errors. This created impulses for a cross-fertilizing research agenda that relates scientific and industrial contexts.


Participants
  • Alessandro Abate (TU Delft, NL) [dblp]
  • Erika Abraham (RWTH Aachen, DE) [dblp]
  • Jacob A. Abraham (University of Texas - Austin, US)
  • Ernst Althaus (Universität Mainz, DE) [dblp]
  • Rolf Backofen (Universität Freiburg, DE) [dblp]
  • Rena Bakhshi (Free University of Amsterdam, NL)
  • Bernd Becker (Universität Freiburg, DE) [dblp]
  • Luca Cardelli (Microsoft Research UK - Cambridge, GB) [dblp]
  • Tugrul Dayar (Bilkent University - Ankara, TR)
  • Lorenzo Dematte (Microsoft Research - University Trento, IT)
  • Alexander Dreyer (Fraunhofer ITWM - Kaiserslautern, DE)
  • Andreas Eggers (Universität Oldenburg, DE)
  • Jasmin Fisher (Microsoft Research UK - Cambridge, GB) [dblp]
  • Goran Frehse (VERIMAG - Grenoble, FR) [dblp]
  • Gert-Martin Greuel (TU Kaiserslautern, DE) [dblp]
  • Christoph Grimm (TU Wien, AT)
  • Radu Grosu (SUNY - Stony Brook, US) [dblp]
  • Ernst Moritz Hahn (Universität des Saarlandes, DE)
  • Boudewijn Haverkort (University of Twente, NL) [dblp]
  • Lars Hedrich (Goethe-Universität - Frankfurt a. M., DE)
  • Holger Hermanns (Universität des Saarlandes, DE) [dblp]
  • Kevin Jones (City University - London, GB)
  • Marek Kwiatkowski (University of Edinburgh, GB)
  • Mark Lawford (McMaster University - Hamilton, CA) [dblp]
  • Jean-Yves Le Boudec (EPFL - Lausanne, CH) [dblp]
  • David Lester (University of Manchester, GB)
  • Oded Maler (VERIMAG - Grenoble, FR) [dblp]
  • Maria-Emanuela-Canini Mateescu (EPFL - Lausanne, CH)
  • Linar Mikeev (Universität des Saarlandes, DE)
  • Ian M. Mitchell (University of British Columbia - Vancouver, CA) [dblp]
  • Pieter J. Mosterman (McGill University - Montreal, CA) [dblp]
  • Chris J. Myers (Univ. of Utah, US) [dblp]
  • Joachim Niehren (INRIA - University of Lille 1, FR) [dblp]
  • Gethin Norman (University of Glasgow, GB) [dblp]
  • David Parker (University of Oxford, GB) [dblp]
  • Andrew Phillips (Microsoft Research UK - Cambridge, GB) [dblp]
  • Lee Pike (Galois - Portland, US)
  • Stefan Ratschan (Academy of Science - Prague, CZ) [dblp]
  • Peter Schrammel (INRIA - Grenoble, FR) [dblp]
  • David Spieler (Universität des Saarlandes, DE)
  • Sofiene Tahar (Concordia Univ. - Montreal, CA)
  • Ralf Wimmer (Universität Freiburg, DE) [dblp]
  • Verena Wolf (Universität des Saarlandes, DE) [dblp]
  • Chao Yan (University of British Columbia - Vancouver, CA)
  • Mohamed Zaki (University of British Columbia - Vancouver, CA)
  • Lijun Zhang (Technical University of Denmark - Lyngby, DK) [dblp]

Classification
  • hardware
  • modelling / simulation
  • semantics / formal methods
  • verification / logic

Keywords
  • Discrete-continuous analysis
  • qualitative and quantitative models
  • analog and mixed-signal circuits
  • computational biology
  • quantitative verification
  • hybrid systems
  • formal analysis
  • probabilistic and stochastic systems