Technische Samenvatting: Afscherming voor Hogere-Orde Veiligheid

1. Probleemstelling

Klassieke veiligheidsafschermingen (safety shields) zijn runtime-handhavingsmechanismen die ontworpen zijn om de acties van een controller te beperken om veiligheid te garanderen. Traditioneel worden deze afschermingen gesynthetiseerd voor toestandspredicaten, waarbij een fysieke toestand wordt geclassificeerd als veilig of onveilig. Echter, in veel cyber-fysieke toepassingen is dit binaire beeld onvoldoende. Veiligheid hangt vaak af van de afgeleiden van de toestand, en niet alleen van de toestand zelf. Een voertuig dat een obstakel nadert, moet bijvoorbeeld een botsing vermijden (positie), maar moet ook de snelheidslimieten respecteren (eerste afgeleide), krachtlimieten veroorzaakt door versnelling (tweede afgeleide) en jerk-limieten (derde afgeleide) om letsel te voorkomen.

Het kernprobleem dat wordt aangepakt, is hoe men systematisch veiligheidsrestricties kan definiëren en afdwingen over eigenschappen die gedefinieerd zijn via discrete afgeleiden van positionele toestanden in een discrete-tijd, discrete-toestand setting. De uitdaging ligt in het feit dat een order-$k$ restrictie afhankelijk is van een venster van $k+1$ opeenvolgende toestanden, wat geheugen vereist dat schaalt met de orde van de restrictie, en wat efficiënte synthese-algoritmen noodzakelijk maakt die geen onhaalbare regio's van de toestandsruimte verkennen.

2. Methodologie

Differentieel Veiligheidseigenschappen

De auteurs introduceren differentiele veiligheidseigenschappen, een taal voor het specificeren van restricties over discrete afgeleiden.

• Discrete Afgeleiden: Gedefinieerd recursief met behulp van achterwaartse eindige differenties over een gediscretiseerde toestandsruimte $S \subseteq \mathbb{R}^d$ met een tijdstap $\Delta \tau$. De $k$-de afgeleide op index $t$ is afhankelijk van het venster van toestanden $(s_{t-k}, \dots, s_t)$.
• Syntaxis en Semantiek: Eigenschappen zijn Booleaanse expressies over atomen van de vorm $\partial^k \in R$, waarbij $R$ een veilige verzameling is. Een eigenschap van orde $k$ wordt globaal geïnterpreteerd over een sequentie als deze geldt voor alle vensters van lengte $k+1$.
• Expressiviteit: Het artikel bewijst dat order-$k$ differentiele veiligheidseigenschappen exact equivalent zijn aan predicaten over vensters van $k+1$ opeenvolgende toestanden.

Schild-synthese Benaderingen

Het artikel stelt drie benaderingen voor om maximaal permissieve winnende strategieën (schilden) voor deze eigenschappen te synthetiseren, gemodelleerd als turn-based veiligheidsspellen.

A. Baseline Synthese (History Games)

Deze benadering reduceert het differentiele veiligheidsspel tot een gewoon veiligheidsspel door de toestandsruimte uit te breiden.

• Constructie: De toestandsruimte wordt uitgebreid om historieën van lengte $k+1$ op te slaan. De differentiele veiligheidseigenschap wordt een toestand-invariant op deze historie-toestanden.
• Resultaat: Een geheugenloze strategie op het historie-spel induceert een $(k+1)$-historie afhankelijke strategie voor het oorspronkelijke spel.
• Complexiteit: $O(|S|^{k+1} \cdot |A|)$.

B. Directe Synthese (Geheugen-Optimaal)

De auteurs presenteren een geoptimaliseerd algoritme dat dezelfde maximaal permissieve shield berekent, maar slechts $k$ voorgaande toestanden hoeft op te slaan (historiën van lengte $k$).

• Mechanisme: Het algoritme initialiseert veilige acties voor historieën van lengte $< k$ (waar de $k$-de afgeleide ongedefinieerd is). Voor historieën van lengte-$k$ controleert het of alle opvolgende toestanden de eigenschap voldoen. Vervolgens worden conflicten achterwaarts gepropageerd: als een historie geen veilige acties heeft, wordt deze als onveilig gemarkeerd, en worden acties die naar deze historie leiden verwijderd uit de predecessor-historiën.
• Geheugenlimiet: Het artikel bewijst dat $k$-historie afhankelijkheid noodzakelijk en nauwkeurig is; er bestaan spellen waar een winnende strategie $k$-historie afhankelijkheid vereist, maar waar geen $(k-1)$-historie afhankelijke strategie bestaat.
• Optimalisatie: Het algoritme kan worden beperkt tot pad-verbonden historieën (historiën die daadwerkelijk kunnen voorkomen in een spel), wat de complexiteit reduceert tot $O(|S| \cdot B^k \cdot |A|)$, waarbij $B$ de bovengrens is op de transitiegraad.

C. Iteratieve Synthese (Hiërarchisch)

Voor eigenschappen die een hiërarchie vormen (bijv. positie $\land$ snelheid $\land$ versnelling), stellen de auteurs een iteratieve procedure voor.

• Principe: Als een venster onveilig is voor een lagere orde eigenschap (bijv. snelheid), is het inherent onveilig voor elke hogere orde eigenschap die deze bevat.
• Procedure: Het algoritme lost de hiërarchie niveau voor niveau op. Op niveau $i$ construeert het kandidaat-vensters die aan de $i$-de orde eigenschap voldoen en waarvan het suffix (de laatste $i-1$ toestanden) een winnend venster is voor niveau $i-1$. Dit reduceert de zoekruimte aanzienlijk voordat hogere-orde restricties worden geëvalueerd.
• Complexiteit: In het slechtste geval komt het overeen met directe synthese, maar in de praktijk biedt het aanzienlijke efficiëntiewinsten door grote regio's die bekend staan als onveilig op lagere niveaus te vermijden.

3. Belangrijkste Bijdragen

1. Definitie van Differentiele Veiligheidseigenschappen: Een formele taal voor restricties over discrete afgeleiden, bewezen equivalent aan predicaten over glijdende vensters van toestanden.
2. Baseline Reductie: Een standaard reductie van differentiele veiligheidsspelen naar gewone veiligheidsspelen over $(k+1)$-toestand historieën.
3. Direct Synthese Algoritme: Een geheugen-optimaal algoritme dat maximaal permissieve schilden berekent met gebruik van slechts $k$-toestand historieën, inclusief een bewijs dat deze geheugenlimiet nauwkeurig is.
4. Iteratieve Synthese: Een algoritme voor hiërarchische differentiele veiligheidseigenschappen dat restricties oplost in toenemende volgorde van complexiteit, waarbij lagere niveaus worden gebruikt om de toestandsruimte te snoeien.
5. Experimentele Evaluatie: Implementatie en evaluatie op 2D-voertuigmodellen, waarbij wordt aangetoond dat directe en iteratieve synthese de tijd- en geheugenkosten aanzienlijk verminderen vergeleken met de baseline, vooral naarmate de orde van de restricties toeneemt.

4. Experimentele Resultaten

De auteurs evalueerden de syntheseprocedures op een gediscretiseerd 2D-automodel dat muren of obstakels nadert met verschillende snelheid-, acceleratie-, jerk- en snap-restricties.

• Prestaties: De baseline methode liep vaak vast (60s limiet) op grotere instanties of hogere orden. Zowel directe als iteratieve synthese losten deze instanties binnen seconden op.
• Efficiëntie: Iteratieve synthese presteerde beter dan directe synthese wanneer het aantal gesnoeide toestanden groot was (bijv. 89,5% snoeiing in sommige benchmarks), wat het nut van de hiërarchische benadering bevestigt.
• Trace Gedrag: Simulaties toonden aan dat hogere-orde schilden agenten eerder dwingen om afstand te houden tot hoge snelheden en scherpe bochten, waardoor "gedoemde" toestanden effectief worden voorkomen waar een botsing onvermijdelijk is door momentum, zelfs als de huidige positie veilig is.
• Afgeleide Druk: De auteurs introduceerden een metriek om de voldoening van restricties te visualiseren, waarbij werd getoond dat hogere-orde schilden een lagere druk behouden over alle afgeleide-ordes vergeleken met lagere-orde schilden.

5. Betekenis en Claims

Het artikel claimt een systematisch kader te bieden voor hogere-orde veiligheid in cyber-fysieke systemen. De betekenis ligt in:

• Het Gat Dichten: Verder gaan dan eenvoudige toestandspredicaten om dynamische restricties (snelheid, versnelling, jerk) te includeren, die cruciaal zijn voor fysieke veiligheid en comfort.
• Geheugenefficiëntie: Aantonen dat de hoeveelheid geheugen die nodig is voor het afdwingen van orde-$k$ restricties kan worden gereduceerd van $k+1$ naar $k$ toestanden, en dat deze reductie theoretisch noodzakelijk is.
• Schaalbaarheid: Laten zien dat hiërarchische synthese het computationeel haalbaar maakt om complexe, meerlagige veiligheidsrestricties af te dwingen door de structuur van veiligheidshiërarchieën te gebruiken om de toestandsruimte te snoeien.
• Runtime Handhaving: Het genereren van maximaal permissieve schilden, wat ervoor zorgt dat het handhavingsmechanisme (bijv. een geleerd beleid) alleen ingrijpt wanneer dat strikt noodzakelijk is om veiligheid te garanderen.

De auteurs merken op dat hoewel de benadering offline een eindig adversarieel spel oplost, het de worst-case, maximaal permissieve schilden oplevert voor de gekozen abstractie. Zij erkennen dat toekomstig werk symbolische fixed-point methoden zou kunnen verkennen om explicit state enumeration te verbeteren en de combinatie van differentiele restricties met andere sliding-window specificaties.