Efficient Shield Synthesis via State-Space Transformation

TL;DR

This paper introduces a method for synthesizing safety shields for control systems using state-space transformations, enabling the use of coarse grids for abstraction, which significantly improves computational efficiency without sacrificing accuracy.

Contribution

The paper proposes a novel transformation-based approach that allows effective shield synthesis with coarse state-space grids, reducing computational costs substantially.

Findings

Transformation-based synthesis outperforms standard methods by several orders of magnitude.

Using domain knowledge to select transformations enhances performance.

The approach is effective even without domain knowledge, as shown in the third case study.

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.