07. – 12. November 2010, Dagstuhl-Seminar 10451

Runtime Verification, Diagnosis, Planning and Control for Autonomous Systems


Klaus Havelund (NASA – Pasadena, US)
Martin Leucker (Universität Lübeck, DE)
Martin Sachenbacher (TU München, DE)
Oleg Sokolsky (University of Pennsylvania – Philadelphia, US)
Brian C. Williams (MIT – Cambridge, US)

Auskunft zu diesem Dagstuhl-Seminar erteilt

Dagstuhl Service Team


Dagstuhl Seminar Proceedings DROPS


Over the last decade and a half, a phase transition has occurred in the level of processing power that is incorporated in embedded systems. Simultaneously, a phase transition occurred in the scale of problems that can now be solved by automated reasoning methods. This is leading to a revolution in a range of disciplines, including model-based planning and scheduling, verification, diagnosis, and hybrid systems control: each discipline is applying automated reasoning to increasingly complex real-world problems, and is incorporating real-time versions of their respective methods on board embedded systems. These are employed in order to elevate the level at which the embedded system is commanded, to verify correctness of system behavior at runtime, to improve the reconfigurability of the system, and to automatically recover from failure. The future trend is to connect these computationally intensive systems into vast, networked embedded systems, such as nation-wide earth observing systems, coastal cabled observatories, or smart power grids.

The objective of this seminar is to catalyze a new field of model-based autonomous, embedded and robotic systems, with the salient characteristic that these devices incorporate a significant level of the above-mentioned online reasoning, based on a system model. A common vision is emerging of systems that combine varied forms of real-time reasoning on models within comprehensive run-time architectures, and that are programmed using new forms of high-level programming languages. However, while many of the appropriate languages and modeling formalisms exist, as well as real-time reasoning algorithms for planning and monitoring, these elements are currently spread amongst several disciplines. This seminar will therefore bring together researchers from four complementary disciplines to work towards languages and architectures for model-based autonomy:

  • Model-based Diagnosis and Execution
  • Runtime Verification
  • Continuous Planning and Dispatching
  • Control of Hybrid Discrete/Continuous Systems

Through a mix of technical presentations, tutorials, panels, and breakout discussions, we seek to map out the necessary architectures, languages, formal models, and underlying reasoning methods for predictable robust and autonomous embedded systems. Discussions at the seminar will thus help to identify research needs of autonomous systems in terms of capabilities for monitoring, verification, diagnosis, planning and control in the context of compelling applications. At the same time, participants will be able to discuss technical approaches that have emerged in various related research areas, and assess their applicability to this emerging field.

Dagstuhl-Seminar Series


  • Artifical Intelligence
  • Robotics / Data Structures
  • Algorithms
  • Complexity / Modelling
  • Simulation / Software Engineering / Verification
  • Logic


  • Runtime Verification
  • Model-based Diagnosis
  • Planning
  • Control
  • Autonomous Systems


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.