http://www.dagstuhl.de/16491

December 4 – 9 , 2016, Dagstuhl Seminar 16491

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

Organizers

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)

For support, please contact

Dagstuhl Service Team

Documents

Dagstuhl Report, Volume 6, Issue 12 Dagstuhl Report
Aims & Scope
List of Participants
Shared Documents

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

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.

NSF young researcher support