Efficient Shield Synthesis via State-Space Transformation
This addresses the computational infeasibility of fine-grid abstractions for safety strategy synthesis in control systems, offering a method to reduce overhead while maintaining effectiveness.
The paper tackles the problem of synthesizing safety strategies (shields) for control systems by using state-space transformations to enable efficient computation with coarse grids, demonstrating performance improvements of several orders of magnitude in case studies.
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.