⚡ electrical engineering

NeuroSymbolic Robustness Analysis for Discrete Systems with Respect to Transition Deviations

This paper proposes a neurosymbolic framework that combines Large Language Models for inferring feasible transition deviations with symbolic analysis to compute robustness guarantees for discrete-event systems, effectively addressing the scalability and conservatism limitations of existing methods.

Original authors: Shih-Jie Shih, Jonghan Lim, Ilya Kovalenko, Rômulo Meira-Góes

Published 2026-06-03

📖 4 min read☕ Coffee break read

CC BY 4.0

Original authors: Shih-Jie Shih, Jonghan Lim, Ilya Kovalenko, Rômulo Meira-Góes

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are building a very strict traffic controller for a busy intersection. You write a perfect rulebook (the "supervisor") that tells cars exactly when to stop and go, ensuring no accidents happen. This rulebook works perfectly if the cars and the road behave exactly as you drew them on your blueprint.

But in the real world, things don't always go according to the blueprint. A car might stall, a sensor might glitch, or a driver might make a mistake. In engineering terms, these are "deviations." If your rulebook doesn't account for these real-world glitches, your traffic controller might fail, and accidents could happen.

The Problem: Too Many "What-Ifs"

Engineers have tried to solve this by asking: "What if the car does ANYTHING different than the blueprint?"

The problem is that the number of "anything different" scenarios is astronomically huge. It's like trying to check every single possible way a car could malfunction in the entire universe.

It's too slow: Checking every single possibility takes so much computer power that it's impossible for anything but the simplest systems.
It's too silly: Many of these "what-if" scenarios are physically impossible. For example, a blueprint might say a car could suddenly teleport to the other side of the road. While mathematically possible in a computer model, it's physically impossible in real life. Checking these silly scenarios wastes time and confuses the results.

The Solution: A "Neurosymbolic" Team-Up

This paper proposes a clever team-up between two types of artificial intelligence to fix these problems. Think of it as hiring a Creative Detective and a Strict Accountant to work together.

1. The Creative Detective (The "Neural" Part)

First, the team uses a Large Language Model (LLM)—the same kind of AI that writes stories or answers questions.

What it does: The AI reads the engineering blueprints and the natural language descriptions of how the system should work (e.g., "Cars can't teleport," "Machines can't process parts before they arrive").
The Analogy: Imagine the AI is a detective who looks at the blueprint and says, "Okay, I know this machine. It can't just spontaneously shoot parts out of thin air. That's against the laws of physics. So, I will ignore that impossible scenario."
The Result: Instead of checking millions of impossible glitches, the AI filters them out and gives the team a short, realistic list of things that could actually go wrong.

2. The Strict Accountant (The "Symbolic" Part)

Once the Creative Detective provides the short, realistic list of glitches, the Strict Accountant takes over.

What it does: This part uses traditional, math-heavy logic (symbolic reasoning) to rigorously test the system against only that short list.
The Analogy: The accountant doesn't guess; they run the numbers. They check: "If the machine jams like this, does the traffic controller still keep everyone safe?"
The Result: Because the list is small and realistic, the accountant can finish the job quickly and give a mathematically perfect guarantee of safety.

How It Works in Practice

The researchers tested this "Detective + Accountant" team on three real-world scenarios:

A Factory Machine: Checking if a machine could overflow a storage bin if parts arrived too fast or got stuck.
The Therac-25 (A Medical Machine): A famous historical case where a radiation machine caused accidents due to a design flaw. They checked if the safety rules could handle an operator pressing buttons too fast or choosing the wrong mode.
A Communication Protocol: Checking if a message system could handle lost or duplicated data packets without crashing.

The Results

The paper found that this new method is a huge improvement:

It cuts the noise: The AI successfully filtered out over 90% of the "silly, impossible" scenarios in some cases.
It keeps the safety: Even though they checked fewer scenarios, the safety guarantees they found were just as strong as if they had checked every possible scenario.
It's faster: By ignoring the impossible glitches, the computer didn't have to work as hard to find the answer.

In a Nutshell

This paper introduces a way to make safety checks for machines smarter. Instead of trying to predict every single thing that could go wrong (including impossible magic tricks), it uses AI to figure out what actually could go wrong in the real world, and then uses strict math to prove the system is safe against those specific, realistic risks. It's like checking a bridge for rust and cracks, rather than worrying about it being hit by a meteor.

Technical Summary: NeuroSymbolic Robustness Analysis for Discrete Systems with Respect to Transition Deviations

Problem Statement

In the supervisory control of discrete-event systems (DES), controllers are synthesized to enforce specifications on a plant model. While classical methods provide "correct-by-construction" guarantees, these guarantees are strictly dependent on the accuracy of the plant model. In practice, mismatches arising from unmodeled dynamics, sensor noise, or abstraction errors cause the real system to deviate from its nominal model, potentially compromising safety.

Recent work has addressed this by defining discrete robustness as the set of all possible transition deviations (additional transitions added to the nominal plant) against which a supervisor maintains safety. However, this transition-based approach faces two critical limitations:

Scalability: The space of possible deviations grows exponentially with the state and action spaces, making exhaustive enumeration computationally intractable for all but the smallest systems.
Conservatism: The vast majority of mathematically possible deviations are physically infeasible (e.g., a machine spontaneously outputting a part without input). Including these infeasible deviations inflates the search space and yields robustness results that do not accurately reflect real-world system behavior.

Existing attempts to filter infeasible deviations using formal system constraints ( $P_{sys}$ ) require domain experts to manually encode physical laws into formal specifications, creating a significant burden and adding overhead to the analysis pipeline.

Methodology

The paper proposes a neurosymbolic computing framework to address these scalability and feasibility challenges. The approach decouples the reasoning about physical feasibility from the formal computation of robustness guarantees, utilizing a two-stage process:

1. Neural Feasibility Filtering (LLM Layer)

The first stage leverages Large Language Models (LLMs) to infer a subset of physically feasible deviation transitions ( $D$ ).

Input: The framework ingests formal LTS models of the plant and supervisor, natural language descriptions of system states and events, safety specifications, and domain knowledge regarding physical laws (e.g., "a part cannot be in two places at once").
Process: A structured prompt template guides the LLM to reason about these inputs. The LLM is tasked with identifying transitions that represent realistic faults or deviations consistent with the system's semantics and physical constraints.
Output: A reduced set of feasible deviations $D \subseteq (Q_E \times Act_E \times Q_E) \setminus R_E$ , significantly smaller than the full transition space.

2. Symbolic Robustness Verification (Symbolic Layer)

The second stage performs formal verification on the reduced set $D$ .

Process: A brute-force algorithm (Algorithm 1) iterates through all subsets of the feasible deviations $D$ . For each candidate deviation set $d$ , it uses standard model checking to verify if the deviated system $E_d$ controlled by supervisor $S$ satisfies the safety property $P$ (i.e., $E_d/S \models P$ ).
Refinement: The algorithm extracts only the maximal robust deviations (those not contained within other robust deviations) to form the final robustness set $\Delta_f$ .
Guarantee: Because the verification is performed symbolically on a formally defined transition system, the resulting robustness guarantees remain mathematically correct with respect to the inferred set $D$ .

Key Contributions

The paper outlines two primary contributions:

A Neurosymbolic Framework: A novel architecture that combines LLMs for inferring physically feasible deviation models with symbolic methods for computing robustness guarantees. This approach automates the extraction of physical constraints from natural language and domain knowledge, removing the need for manual formal encoding of $P_{sys}$ .
Prototype and Evaluation: The implementation of a prototype tool and its experimental evaluation on three distinct case studies: a manufacturing system, the Therac-25 radiation therapy interface, and the Alternate Bit Protocol (ABP).

Experimental Results

The framework was evaluated on three case studies using LLMs (GPT-5.2 and Claude 3.5 Sonnet) for feasibility filtering and a Python-based symbolic verifier.

Manufacturing System: The LLM identified 18 feasible deviations (out of a theoretical space of 108). The symbolic layer found one maximal robust deviation set, confirming the system is robust against 15 specific transitions but vulnerable to specific buffer unloading faults.
Therac-25: The analysis identified 9 feasible deviations. The system was found robust against repeated operator "enter" presses but vulnerable to the specific race condition involving the selection of electron therapy, accurately capturing the historical design flaw.
ABP Protocol: The LLM identified 16 feasible deviations. The analysis confirmed robustness against message loss, duplication, and corruption, aligning with the protocol's design intent.

Quantitative Findings:

Feasibility Reduction: The LLMs significantly reduced the search space. The reduction ranged from 67% (Therac-25) to 99% (ABP) compared to the full transition space.
Feasibility Accuracy: For the manufacturing example, 89% of GPT-generated transitions were physically feasible, compared to 54% for Claude. On more complex systems like ABP, feasibility rates dropped for both models (63% and 36%, respectively), indicating a need for improved prompt engineering or domain ontologies.
Robustness Equivalence: Despite operating on a reduced set of deviations, the framework produced robustness guarantees comparable to those obtained from full transition-based analysis in the evaluated cases.

Significance and Claims

The paper claims that this neurosymbolic approach successfully addresses the trade-off between scalability and the inclusion of infeasible deviations in discrete robustness analysis. By using LLMs to filter the solution space based on semantic and physical understanding, the method makes robustness analysis tractable for systems where exhaustive enumeration is impossible.

The authors emphasize that while the LLM component introduces a probabilistic element in identifying feasible deviations, the subsequent symbolic verification ensures that the final robustness guarantees are formally correct with respect to the inferred set. The work demonstrates that it is possible to recover robustness analyses comparable to full-space methods while operating on a drastically smaller, physically meaningful subset of deviations.

The paper concludes modestly, noting that the current implementation of the brute-force algorithm requires optimization for larger systems and that future work will focus on improving prompt engineering, incorporating domain ontologies to enhance LLM accuracy, and investigating interactive refinement loops where symbolic results guide LLM queries.