International Symposium On Leveraging Applications of Formal Methods, Verification and Validation • Crete, Greece
Time: Thursday, 31.10
Room: Room 4
Authors: Christian Schilling
Abstract: We consider the problem of synthesizing safety strategies for control systems, also known as shields. Since the state space is infinite, shields are typically computed over a finite-state abstraction, with the most common abstraction being a rectangular grid. However, for many systems, such a grid does not align well with the safety property or the system dynamics. That is why a coarse grid is rarely sufficient, but a fine grid is typically computationally infeasible to obtain. In this paper, we show that appropriate state-space transformations can still allow to use a coarse grid at almost no computational overhead. We demonstrate in three case studies that our transformation-based synthesis outperforms a standard synthesis by several orders of magnitude. In the first two case studies, we use domain knowledge to select a suitable transformation. In the third case study, we instead report on results in engineering a transformation without domain knowledge.
Slides: Efficient_Shield_Synthesis_via_State-Space_Transformation-slides.pdf
Paper: Efficient_Shield_Synthesis_via_State-Space_Transformation-paper.pdf