Technische Samenvatting: Neurosymbolische Robuustheidsanalyse voor Discrete Systemen met Betrekking tot Transitie-afwijkingen

Probleemstelling

In de supervisiecontrole van discrete-event systemen (DES) worden controllers gesynthetiseerd om specificaties op een plantmodel af te dwingen. Hoewel klassieke methoden "correct-by-construction" garanties bieden, zijn deze garanties strikt afhankelijk van de nauwkeurigheid van het plantmodel. In de praktijk veroorzaken mismatches die voortvloeien uit ongemodelleerde dynamiek, sensorgruis of abstractiefouten dat het werkelijke systeem afwijkt van het nominale model, wat de veiligheid potentieel in gevaar brengt.

Recent werk heeft dit aangepakt door discrete robuustheid te definiëren als de verzameling van alle mogelijke transitie-afwijkingen (aanvullende transities toegevoegd aan het nominale plant) waartegen een supervisor de veiligheid handhaaft. Deze transitie-gebaseerde aanpak staat echter voor twee kritieke beperkingen:

1. Schaalbaarheid: De ruimte van mogelijke afwijkingen groeit exponentieel met de staat- en actieruimtes, waardoor uitputtende enumeratie computationeel onhaalbaar is voor alle systemen behalve de kleinste.
2. Conservatisme: Het overgrote deel van de wiskundig mogelijke afwijkingen is fysiek onhaalbaar (bijvoorbeeld een machine die spontaan een onderdeel uitspuugt zonder input). Het opnemen van deze onhaalbare afwijkingen blaast de zoekruimte op en levert robuustheidsresultaten op die de werkelijke gedrag van het systeem niet accuraat reflecteren.

Bestaande pogingen om onhaalbare afwijkingen te filteren met behulp van formele systeembeperkingen ($P_{sys}$) vereisen dat domeinexperts fysieke wetten handmatig coderen in formele specificaties, wat een aanzienlijke last vormt en overhead toevoegt aan de analysepijplijn.

Methodologie

Het paper stelt een neurosymbolisch rekenframework voor om deze schaalbaarheids- en haalbaarheidsuitdagingen aan te pakken. De aanpak ontkoppelt het redeneren over fysieke haalbaarheid van de formele berekening van robuustheidsgaranties via een tweestaps-proces:

1. Neurale Haalbaarheidsfiltering (LLM-laag)

De eerste fase maakt gebruik van Large Language Models (LLMs) om een subset van fysiek haalbare afwijkingstransities ($D$) af te leiden.

• Input: Het framework verwerkt formele LTS-modellen van de plant en de supervisor, natuurlijke taalbeschrijvingen van systeemtoestanden en gebeurtenissen, veiligheidsspecificaties en domeinkennis over fysieke wetten (bijv. "een onderdeel kan niet op twee plaatsen tegelijk zijn").
• Proces: Een gestructureerd prompt-template stuurt de LLM aan om over deze inputs te redeneren. De LLM krijgt de taak om transities te identificeren die realistische fouten of afwijkingen vertegenwoordigen die consistent zijn met de systeemsemantiek en fysieke beperkingen.
• Output: Een gereduceerde set haalbare afwijkingen $D \subseteq (Q_E \times Act_E \times Q_E) \setminus R_E$, die aanzienlijk kleiner is dan de volledige transitieruimte.

2. Symbolische Robuustheidsverificatie (Symbolische Laag)

De tweede fase voert formele verificatie uit op de gereduceerde set $D$.

• Proces: Een brute-force algoritme (Algoritme 1) iterereert door alle deelverzamelingen van de haalbare afwijkingen $D$. Voor elke kandidaat-afwijkingsset $d$ gebruikt het standaard model checking om te verifiëren of het afgeweken systeem $E_d$ gecontroleerd door supervisor $S$ de veiligheidseigenschap $P$ voldoet (d.w.z. $E_d/S \models P$).
• Verfijning: Het algoritme extraheert alleen de maximale robuuste afwijkingen (die niet bevat zijn binnen andere robuuste afwijkingen) om de uiteindelijke robuustheidsverzameling $\Delta_f$ te vormen.
• Garantie: Omdat de verificatie symbolisch wordt uitgevoerd op een formeel gedefinieerd transitiesysteem, blijven de resulterende robuustheidsgaranties wiskundig correct met betrekking tot de afgeleide verzameling $D$.

Belangrijkste Bijdragen

Het paper schetst twee primaire bijdragen:

1. Een Neurosymbolisch Framework: Een nieuwe architectuur die LLMs combineert voor het afleiden van fysiek haalbare afwijkingsmodellen met symbolische methoden voor het berekenen van robuustheidsgaranties. Deze aanpak automatiseert de extractie van fysieke beperkingen uit natuurlijke taal en domeinkennis, waardoor de noodzaak voor handmatige formele codering van $P_{sys}$ vervalt.
2. Prototype en Evaluatie: De implementatie van een prototype-tool en de experimentele evaluatie ervan op drie verschillende casestudy's: een fabricagesysteem, de Therac-25 radiotherapie-interface en het Alternate Bit Protocol (ABP).

Experimentele Resultaten

Het framework werd geëvalueerd op drie casestudy's met behulp van LLMs (GPT-5.2 en Claude 3.5 Sonnet) voor haalbaarheidsfiltering en een Python-gebaseerde symbolische verifieerder.

• Fabricagesysteem: De LLM identificeerde 18 haalbare afwijkingen (uit een theoretische ruimte van 108). De symbolische laag vond één maximale robuuste afwijkingsset, waarmee werd bevestigd dat het systeem robuust is tegen 15 specifieke transities maar kwetsbaar is voor specifieke bufferontlaadfouten.
• Therac-25: De analyse identificeerde 9 haalbare afwijkingen. Het systeem bleek robuust tegen herhaalde "enter"-drukken van de operator, maar kwetsbaar voor de specifieke race condition waarbij de selectie van elektronentherapie betrokken is, wat de historische ontwerpfout accuraat vastlegt.
• ABP Protocol: De LLM identificeerde 16 haalbare afwijkingen. De analyse bevestigde robuustheid tegen berichtverlies, duplicatie en corruptie, wat overeenkomt met de ontwerpintentie van het protocol.

Kwantitatieve Bevindingen:

• Reductie van Haalbaarheid: De LLMs reduceerden de zoekruimte aanzienlijk. De reductie varieerde van 67% (Therac-25) tot 99% (ABP) vergeleken met de volledige transitieruimte.
• Haalbaarheidsnauwkeurigheid: Voor het fabricagevoorbeeld waren 89% van de door GPT gegenereerde transities fysiek haalbaar, vergeleken met 54% voor Claude. Bij complexere systemen zoals ABP daalde de haalbaarheidsgraad voor beide modellen (respectievelijk 63% en 36%), wat wijst op een behoefte aan verbeterde prompt engineering of domein-ontologieën.
• Robuustheidsequivalentie: Ondanks het werken op een gereduceerde set afwijkingen, produceerde het framework robuustheidsgaranties die vergelijkbaar zijn met die verkregen uit volledige transitie-gebaseerde analyse in de geëvalueerde gevallen.

Betekenis en Claims

Het paper claimt dat deze neurosymbolische aanpak succesvol de trade-off tussen schaalbaarheid en de inclusie van onhaalbare afwijkingen in discrete robuustheidsanalyse aanpakt. Door LLMs te gebruiken om de oplossingsruimte te filteren op basis van semantisch en fysiek begrip, maakt de methode robuustheidsanalyse hanteerbaar voor systemen waar uitputtende enumeratie onmogelijk is.

De auteurs benadrukken dat hoewel de LLM-component een probabilistisch element introduceert bij het identificeren van haalbare afwijkingen, de daaropvolgende symbolische verificatie ervoor zorgt dat de uiteindelijke robuustheidsgaranties formeel correct zijn met betrekking tot de afgeleide set. Het werk demonstreert dat het mogelijk is om robuustheidsanalyses te herstellen die vergelijkbaar zijn met full-space methoden, terwijl er wordt gewerkt op een aanzienlijk kleinere, fysiek betekenisvolle subset van afwijkingen.

Het paper concludeert bescheiden door op te merken dat de huidige implementatie van het brute-force algoritme optimalisatie vereist voor grotere systemen en dat toekomstig werk zich zal richten op het verbeteren van prompt engineering, het integreren van domein-ontologieën om de nauwkeurigheid van de LLM te vergroten, en het onderzoeken van interactieve verfijningslussen waarbij symbolische resultaten LLM-queries sturen.