Dagstuhl-Seminar 10271
Verification over discrete-continuous boundaries
( 04. Jul – 09. Jul, 2010 )
Permalink
Organisatoren
- Bernd Becker (Universität Freiburg, DE)
- Luca Cardelli (Microsoft Research UK - Cambridge, GB)
- Holger Hermanns (Universität des Saarlandes, DE)
- Sofiene Tahar (Concordia Univ. - Montreal, CA)
Kontakt
- Annette Beyer (für administrative Fragen)
Sponsoren
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.
- 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]
Klassifikation
- hardware
- modelling / simulation
- semantics / formal methods
- verification / logic
Schlagworte
- Discrete-continuous analysis
- qualitative and quantitative models
- analog and mixed-signal circuits
- computational biology
- quantitative verification
- hybrid systems
- formal analysis
- probabilistic and stochastic systems