http://www.dagstuhl.de/16491

04. – 09. Dezember 2016, Dagstuhl Seminar 16491

Symbolic-Numeric Methods for Reliable and Trustworthy Problem Solving in Cyber-Physical Domains

Organisatoren

Sergiy Bogomolov (Australian National University – Canberra, AU)
Martin Fränzle (Universität Oldenburg, DE)
Kyoko Makino (Michigan State University – East Lansing, US)
Nacim Ramdani (University of Orléans, FR)

Auskunft zu diesem Dagstuhl Seminar erteilt

Dagstuhl Service Team

Dokumente

Dagstuhl Report, Volume 6, Issue 12 Dagstuhl Report
Motivationstext
Teilnehmerliste
Gemeinsame Dokumente

Summary

With the advent of cyber-physical systems increasingly penetrating our life, we are facing an ever-growing and permanent dependency on their reliable availability, continued function, and situationally adequate behavior even in highly sensitive application domains. As cyber-physical systems comprise complex, heteromorphic software systems, their reliability engineering calls for combinations of theories and methods traditionally considered separate. While we have recently seen some of the necessary combinations blossom, e.g. the theory of hybrid systems bridging continuous control with reactive systems, other areas remain less developed and explored. A prominent one is the role of numerics in cyber-physical systems: while it is obvious that cyber-physical systems increasingly rely on numerical software components, e.g., in signal processing or in state representation and extrapolation during situation assessment and planning, specific methods for addressing the issues associated, like consequences of numerical inaccuracy and methods for confining propagation of errors, are just in their infancy. This is in stark contrast to the use of numerics in more mature branches of computing, like signal processing or numerical analysis, where quantization effects as well as genesis and propagation of numerical error is well-understood and dedicated methods for controlling it in critical application, like various forms of interval-based numerical algorithms, are readily available. The aforementioned ``traditional'' methods are, however, not versatile enough to cope with the cyber-physical setting, where numerical results, like state extrapolations over significant temporal horizons, enter into complex and safety-critical decision making, rendering error propagation potentially highly discontinuous. It seems that future critical applications, like automated driving contributing to the EU's "Vision Zero" of eliminating fatalities in road-bound traffic, consequently call for novel means of analyzing and controlling the impact of numerics on system correctness, complemented by pertinent means of verification for establishing the safety case. The germs of such methods obviously have to be sought in the fields of design and verification of cyber-physical systems, i.e. in particular, (1) hybrid discrete-continuous systems, as well as (2) verified numerics, arithmetic constraint solving also involving symbolic reasoning, and (3) planning and rigorous optimization in arithmetic domains. The seminar gathered prominent researchers from all these fields in order to address the pressing problems induced by our societal dependence on cyber-physical systems.

As argued above, bringing together researchers dealing with hybrid discrete-continuous systems, with verified numerics in arithmetic constraint solving, and with planning and optimization in arithmetic domains can help improve the state of the art in rigorously interpreting and controlling cyber-physical phenomena. In the sequel, we review existing and potential contributions of the three fields to problem solving in cyber-physical domains and sketch potentials for cross-fertilization, which was the aim of the proposed seminar.

License
  Creative Commons BY 3.0 Unported license
  Sergiy Bogomolov, Martin Fränzle, Kyoko Makino, and Nacim Ramdani

Classification

  • Artificial Intelligence / Robotics
  • Semantics / Formal Methods
  • Verification / Logic

Keywords

  • Cyber-physical systems
  • Hybrid systems
  • Verification
  • Constraint solving
  • Verified numerical methods
  • Planning
  • Optimization methods

Buchausstellung

Bücher der Teilnehmer 

Buchausstellung im Erdgeschoss der Bibliothek

(nur in der Veranstaltungswoche).

Dokumentation

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

Publikationen

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.