Synthesis of/for robust systems

30^th October 2012, 16:00 Ashton Lecture Theatre
Ruediger Ehlers
Dept of Electrical Engineering and Computer Sciences
UC Berkeley
USA

Abstract

In the recent years, research on synthesis of reactive systems from temporal logic specifications has taken up momentum as classical theory on the subject has been complemented with results on the efficient solution of the problem in practice. Traditionally, the perception of the synthesis problem is rather binary: either there exists an implementation for a specification, and we are fine with obtaining any implementation, or there exists none. This view is a bit simplistic, as it completely ignores that different implementations for the same specification can have different levels of quality, and we typically strive for solutions of a high quality when engineering systems.

This talk shows how reactive synthesis can help with engineering systems of high robustness, which is one of the major quality considerations in practice. We say that a system is robust if it behaves reasonably in the case that some assumption about its environment is violated or in case of an internal error. First, we discuss how robustness concerns can be incorporated in a practical modern synthesis workflow. Then, we deal with the problem of increasing the robustness of manually constructed systems, and show how reactive synthesis can be utilised to compute runtime monitors for safety-critical systems that can predict problems before they actually arise.