http://www.dagstuhl.de/10271

July 4 – 9 , 2010, Dagstuhl Seminar 10271

Verification over discrete-continuous boundaries

Organizers

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)


The Dagstuhl Foundation gratefully acknowledges the donation from:

  •   Microsoft Research, Cambridge, UK

For support, please contact

Dagstuhl Service Team

Documents

Dagstuhl Seminar Proceedings DROPS
List of Participants

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.

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

Book exhibition

Books from the participants of the current Seminar 

Book exhibition in the library, ground floor, during the seminar week.

Documentation

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).

Publications

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

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.