November 7 – 12 , 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)

For support, please contact

Dagstuhl Service Team


Dagstuhl Seminar Proceedings DROPS
List of Participants


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