LFCS Seminar: 25 February 2020 - Paritosh Pandya

Title: Logical Specification and Optimal Synthesis of Robust Controllers and Runtime Enforcement Shields

Abstract:

We will present a logic for  specifying robust controllers as well as runtime enforcement shields. The specification consists of regular properties given in an interval temporal logic QDDC. Our specification encompasses both hard robustness and soft robustness. Here, hard robustness guarantees invariance of commitment under user-specified relaxed (weakened) assumptions. A systematic framework for logically specifying the assumption weakening by means of a formula, called the Robustness Criterion, is presented. The soft robustness pertains to the ability of the controller to maintain the commitment for as many inputs as possible, irrespective of any assumption. We present a uniform method for the synthesis of a robust controller which guarantees the specified hard robustness and it optimizes the specified soft robustness. The method is implemented using a tool DCSynth, which provides soft requirement optimized controller synthesis. We will also consider logical specification and synthesis of runtime enforcement shields which correct sporadic errors in human designed controllers while minimizing deviation from the human designed controller's output at runtime. Experimental results will illustrate the performance of our tool as well as that of the synthesized controllers.

 (Joint work with Amol Wakankar)