Paper deep dive
Grammar-Constrained Refinement of Safety Operational Rules Using Language in the Loop: What Could Go Wrong
Khouloud Gaaloul, Zaid Ghazal, Madhu Latha Pulimi, Sam Emmanuel Kathiravan
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 97%
Last extracted: 6/21/2026, 6:58:11 AM
Summary
The paper introduces a framework for the grammar-constrained refinement of safety operational rules in Cyber-Physical Systems (CPS), specifically targeting autonomous driving systems. The framework addresses inconsistencies between operational rules and observed system behavior by combining counterfactual reasoning with a Large Language Model (LLM) guided by a domain-specific grammar. The process involves using counterfactual analysis to localize inconsistency boundaries through minimal input perturbations, followed by an LLM-driven refinement loop that ensures syntactic correctness and semantic validity. The approach aims to resolve rule inconsistencies while preserving the original safety requirements and the Operational Design Domain (ODD).
Entities (6)
Relation Signals (4)
Operational Rule → belongsto → Cyber-Physical Systems
confidence 100% · Safety specifications in cyber-physical systems (CPS) capture the operational conditions...
Domain-Specific Grammar → constrains → Large Language Model
confidence 100% · The core novelty is combining counterfactual analysis with a grammar-constrained LLM...
Counterfactual Analysis → localizes → Inconsistency Boundaries
confidence 100% · The counterfactual analysis step... localizes a nearby decision boundary for the inconsistent rule.
Large Language Model → performs → Rule Refinement
confidence 90% · A grammar-constrained LLM acts as a synthesis assistant to propose a candidate refinement of rr.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Safety specifications in cyber-physical systems (CPS) capture the operational conditions the system must satisfy to operate safely within its intended environment. As operating environments evolve, operational rules must be continuously refined to preserve consistency with observed system behavior during simulation-based verification and validation. Revising inconsistent rules is challenging because the changes must remain syntactically correct under a domain-specific grammar. Language-in-the-loop refinement further raises safety concerns beyond syntactic violations, as it can produce semantically unjustified refinements that overfit to the observed outcomes. We introduce a framework that combines counterfactual reasoning with a grammar-constrained refinement loop to refine operational rules, aligning them with the observed system behavior. Applied to an autonomous driving control system, our approach successfully resolved the inconsistencies in an operational rule inferred by a conventional baseline while remaining grammar compliant. An empirical large language model (LLM) study further revealed model-dependent refinement quality and safety lessons, which motivate rigorous grammar enforcement, stronger semantic validation, and broader evaluation in future work.
Tags
Links
- Source: https://arxiv.org/abs/2604.23523v1
- Canonical: https://arxiv.org/abs/2604.23523v1
Trouble viewing inline? Open PDF directly →
Full Text
40,521 characters extracted from source content.
Expand or collapse full text
by Grammar-Constrained Refinement of Safety Operational Rules Using Language in the Loop: What Could Go Wrong Khouloud Gaaloul University of Michigan–DearbornDearbornMIUSA kgaaloul@umich.edu , Zaid Ghazal University of Michigan–DearbornDearbornMIUSA zghazal@umich.edu , Madhu Latha Pulimi University of Michigan–DearbornDearbornMIUSA pulimiml@umich.edu and Sam Emmanuel Kathiravan University of Michigan–DearbornDearbornMIUSA samanuel@umich.edu (2026) Abstract. Safety specifications in cyber-physical systems (CPS) capture the operational conditions the system must satisfy to operate safely within its intended environment. As operating environments evolve, operational rules must be continuously refined to preserve consistency with observed system behavior during simulation-based verification and validation. Revising inconsistent rules is challenging because the changes must remain syntactically correct under a domain-specific grammar. Language-in-the-loop refinement further raises safety concerns beyond syntactic violations, as it can produce semantically unjustified refinements that overfit to the observed outcomes. We introduce a framework that combines counterfactual reasoning with a grammar-constrained refinement loop to refine operational rules, aligning them with the observed system behavior. Applied to an autonomous driving control system, our approach successfully resolved the inconsistencies in an operational rule inferred by a conventional baseline while remaining grammar compliant. An empirical large language model (LLM) study further revealed model-dependent refinement quality and safety lessons, which motivate rigorous grammar enforcement, stronger semantic validation, and broader evaluation in future work. Safety Operational Rule Refinement, Large Language Models, Cyber-Physical Systems †journalyear: 2026†copyright: c†conference: 21st International Conference on Software Engineering for Adaptive and Self-Managing Systems; April 13–14, 2026; Rio de Janeiro, Brazil†booktitle: 21st International Conference on Software Engineering for Adaptive and Self-Managing Systems (SEAMS ’26), April 13–14, 2026, Rio de Janeiro, Brazil†doi: 10.1145/3788550.3794884†isbn: 979-8-4007-2445-9/2026/04†ccs: Software and its engineering Software safety 1. Introduction Safety specifications for cyber-physical systems (CPS) rely on operational rules that translate safety requirements into testable conditions on system executions for verification and validation. In autonomous driving, these rules are scoped by the Operational Design Domain (ODD) (Fraade-Blanar et al., 2018; García et al., 2022) and informed by ISO 26262 (Debouk, 2019) and ISO/PAS 21448 (SOTIF) (Kirovskii and Gorelov, 2019). They are typically expressed as logical or quantitative constraints over environmental and system variables, and evaluated through simulation-based testing (Tuncali et al., 2018) to ensure safe operation within the declared operational boundaries. However, as the operating conditions evolve, the observed system outcomes may shift and expose inconsistencies with the verdict of the operational rule. Maintaining rule validity and ensuring continued alignment with observed executions is a recurring challenge. This motivates an automated rule refinement process that restores consistency while preserving the underlying safety requirement and keeping the stated ODD unchanged. Mining operational rules from observed traces has commonly been performed by learning linear temporal logic (LTL) properties (Rescher and Urquhart, 2012; Pnueli, 1977) and by applying specification mining and machine learning (ML) methods (Jha et al., 2019; Lemieux et al., 2015), typically constrained by templates rather than a domain-specific grammar. Other works use surrogate models (Jodat et al., 2025, 2024; Zhu et al., 2022) and genetic programming (GP) (Gaaloul et al., 2021) as interpretable methods to infer and correct STL properties, or apply parameter mining and falsification (Asarin et al., 2011; Hoxha et al., 2018; Kyriakis et al., 2019) to tune bounds that make observed behaviors satisfy a fixed specification. No prior work is designed to automatically refine an existing inconsistent operational rule under a domain-specific grammar. Recent work has explored using large language models (LLMs) to support the construction and maintenance of safety specification artifacts. Nouri et al. (Nouri et al., 2024) propose a prompt-based pipeline for an automotive SafetyOps workflow that generates safety requirements and then checks the resulting rule set for redundancy, contradictions, and other quality issues. Li et al. (Li et al., 2025) use LLMs to generate LTL specifications under safety restrictions, then iteratively refine candidate formulas using language inclusion checks and counterexamples. Both works commonly combine LLM generation with automated validation. However, to our knowledge, no prior work uses grammar-constrained LLMs to refine an existing inconsistent operational rule to align with observed system behavior. Moreover, validation in LLM-based specification synthesis pipelines typically targets syntactic or format compliance, rather than consistency with runtime outcomes. We propose an approach for refining operational rules to resolve inconsistencies between rule verdicts and observed system behavior. Refinement is restricted to operational rules that operationalize a fixed safety requirement within a stated ODD. Rather than constructing a formal proof of requirement satisfaction, our approach is guided by observed counterfactual evidence. The core novelty is combining counterfactual analysis with a grammar-constrained LLM guided by a domain-specific grammar to synthesize minimal refinements of operational rules while preserving syntactic correctness and semantic validity. The main contribution of this paper is a rule refinement framework that combines counterfactual reasoning to localize inconsistency boundaries between operational rules and observed behavior, and grammar-constrained LLMs to generate interpretable, syntactically valid refinements to the operational rules that capture a pre-specified safety requirement within a stated ODD. We report an initial empirical study on an autonomous driving subsystem (ADS), evaluating effectiveness against a conventional baseline. We further assess the model-dependent language-in-the-loop refinement quality across multiple LLM variants and derive safety lessons. Organization. The remainder of this paper is organized as follows. Section 2 presents the operational rule refinement framework, including the rule semantics, the domain-specific grammar, and the counterfactual guided, grammar constrained refinement loop. Section 3 reports our experimental exploration on an autonomous driving subsystem and summarizes the results of the LLM variant study. Section 4 concludes and outlines directions for future work. Figure 1. Operational Rule Refinement Approach Overview. Overview of the operational rule refinement pipeline showing inputs (rule set, grammar, labeled executions), a counterfactual step to localize inconsistency boundaries, a grammar constrained LLM refinement loop, and validation producing an updated rule. 2. Operational Rule Refinement Framework To address inconsistencies between operational rules and observed system behavior, we introduce a grammar-constrained rule refinement framework that leverages counterfactual reasoning combined with grammar-constrained LLM to produce interpretable, syntactically and semantically valid refinements of operational rules. The framework can be applied as a corrective mechanism for outdated operational rules within safety specifications that have become inconsistent with evolving system behavior. As a running example, we consider an autonomous driving controller parameterized by three scenario features; the ego vehicle speed (ego_speed), the longitudinal distance to the front vehicle (dist_front), and the lateral offset within the lane (lane_offset). In the context of autonomous driving, these features directly influence lane keeping behavior and collision risk. Operational rules encode admissible regions of the input space in which the unchanged safety requirement is intended to hold, i.e., minimum headway constraints at a given speed or allowable lane deviation under certain road conditions. Such rules capture the safety requirement into conditions over the variables, and may lose consistency with observed controller behavior as the operating environment changes or evolves. When these rules become inconsistent, they can yield misleading verdicts even if the underlying safety requirement is unchanged, motivating refinement of the rules rather than adaptation of the safety specification. 2.1. Operational Rules and Semantics Let X⊆ℝdX ^d denote the input domain of the system under test (SUT), where each input vector x=[i1,…,id]x=[i_1,…,i_d] represents input variables. The label of x is y, where y=y= Pass if the observed system outcome satisfies the safety requirement, and y=y= Fail if it violates the safety requirement. We assume these outcome labels reflect the SUT simulator ground truth for the underlying safety requirement, handling label noise is outside our refinement objectives. An operational rule is a predicate r:X→,r:X→\ true, false\ that constrains the operating region of the system. Here, true and false denote the logical evaluation of the rule on a given input. Specifically, r(x)=r(x)= true means that the rule holds for x, i.e., the input is considered valid within the admissible operating region, while r(x)=r(x)= false indicates that the rule does not hold. For example, given a rule r1:(dist_front<5.0)∧(ego_speed>0)r_1:\ ( dist\_front<5.0)\ \ ( ego\_speed>0) and an input vector x1=(ego_speed=8.0, dist_front=4.2, lane_offset=0.1)x_1= (ego\_speed=8.0,\ dist\_front=4.2,\ lane\_offset=0.1), r1(x1)=r_1(x_1)= true, indicating that x1x_1 is valid and satisfies the admissible condition expressed by r1r_1. This indicates that, at speed 8.08.0 the ego vehicle is operating in a safe state where the front vehicle is within 5.05.0 units of distance, so the scenario lies inside the region of the input space that r1r_1 designates as admissible for the system’s controller with respect to the safety requirement. Table 1. Consistency of an operational rule r on a given input vector x with respect to its rule set group and outcome y of x. This table describes the interpretation of an operational rule on an input vector given the rule set to which the rule belongs and the observed system outcome. A rule set determines the rule verdict. Rule Set Rule Verdict r(x)r(x) Observed y Consistency R_ Pass Pass true Pass Consistent R_ Fail Fail true Pass Inconsistent R_ Pass Pass true Fail Inconsistent R_ Fail Fail true Fail Consistent R_ Pass Pass false – Inconclusive R_ Fail Fail false – Inconclusive We consider two rule sets, R_ Pass and R_ Fail, encoding all operational rules r that imply Pass or Fail, respectively, on a given input x. Table 1 summarizes how an operational rule r is interpreted on an input vector x given the rule set to which r belongs and the observed system outcome y for x. A rule set determines the rule verdict. Rules in R_ Pass assign a Pass verdict when they hold on x, while rules in R_ Fail assign a Fail verdict when they hold on x. The column r(x)r(x) reports whether the rule holds on x. When r(x)=r(x)= true, the rule makes a definitive verdict and its consistency is determined by comparing that verdict to the observed outcome y. A rule in R_ Pass is consistent if y=y= Pass, i.e., the rule holds on x and correctly assigns a passing verdict, and inconsistent if y=y= Fail, i.e., the rule holds on x but incorrectly assigns a Pass verdict while the observed outcome is a failure. A rule in R_ Fail is consistent if y=y= Fail, i.e., the rule holds on x and correctly assigns a failing verdict, and inconsistent if y=y= Pass, i.e., the rule holds on x but incorrectly assigns a Fail verdict while the observed outcome is a pass. When r(x)=r(x)= false, the rule does not apply to x and therefore yields no definitive verdict. This case is labeled inconclusive and the outcome y is not used (shown as “–”). In this paper, we refine inconsistent rules, since they expose discrepancies between operational rules and observed system behavior. In our running example, consider r1∈Rr_1∈ R_ Pass as a pass rule and the observed outcome of x1x_1 is y1=Faily_1=Fail, which makes r1r_1 inconsistent. This indicates that x1x_1 satisfies the admissible condition encoded by r1r_1, so the rule assigns a pass verdict, yet the system execution on x1x_1 violates the safety requirement. Each operational rule is expressed using a domain-specific grammar that defines the syntactic space of valid predicates over the system inputs. In general, the structure of the grammar is guided by domain knowledge, which determines the form and semantics of admissible expressions. In the automotive domain, operational rules for cyber-physical systems are typically expressed as arithmetic and relational constraints over configuration parameters and input variables. While it may vary across domains, in this paper we adopt the grammar G introduced in prior work (Gaaloul et al., 2021) to express environmental assumptions for cyber-physical systems, as it is particularly suited to the automotive context studied here. Each operational Rule ::=Disj :=Disj Disj ::=Disj∨Conj∣Conj :=Disj Conj ::=Conj∧Rel∣Rel :=Conj Rel ::=ExpropExp :=Exp\ rop\ Exp rop ::=<∣≤∣>∣≥∣=∣≠ :=< ≤ > ≥ = ≠ Exp ::=ExpaopExp∣const∣var :=Exp\ aop\ Exp aop ::=+∣−∣∗∣/ :=+ - * / rule is a hierarchical logical formula built from disjunctions (DisjDisj), conjunctions (ConjConj), and relational predicates (RelRel) over arithmetic expressions (ExpExp). A rule is composed of one or more disjunctive clauses, each representing an alternative valid operating condition. Each predicate RelRel compares two expressions ExpExp using operators <,≤,>,≥,=,≠\<,≤,>,≥,=,≠\, where expressions are formed from arithmetic operations over constants (constconst) and input variables (varvar). Problem Statement. Given the rule sets R_ Pass and R_ Fail, and a labeled input set T=(xi,yi)T=\(x_i,y_i)\, the objective is to derive refined rule sets as changes in the components of existing rules, such as constants, input variables, relational operators, or logical connectors, so that they satisfy the following conditions: (i) Maintain semantic consistency with the grammar; (i) Reduce the number of inconsistent rules; (i) Preserve previously consistent rules; (iv) Eliminate contradictory rules. Note that the safety requirement and the stated ODD remain fixed. We refine operational rules that capture acceptance criteria for verification when their verdicts become inconsistent with observed outcomes. A refined rule is therefore a hypothesis about admissible operating conditions, not an authorization to broaden the safety envelope in response. 2.2. Approach Overview The grammar-constrained rule refinement framework operates on simulation or testing data and existing operational rules to resolve inconsistencies between operational rules and observed system behavior. In this work, we assume the presence of a safety operational rule set evaluated for inconsistencies using a manual review process or an automated consistency checking mechanism. We also assume that the rules are expressed in temporal logic according to a predefined grammar that constrains the admissible structure of rules (e.g., grammar G). Figure 1 shows the overview of our approach. The framework takes as input (1) an operational rule set ℛR containing at least one inconsistent rule r, (2) a grammar specification G (3) a labeled execution dataset D of simulation or test cases. Each test case contains an input vector x of input values and an observed outcome y∈Pass,Faily∈Pass,Fail with respect to a given safety specification. For example, the input vector x1x_1, r1r_1 assigns the x1x_1 a Pass verdict. However, the observed system outcome for x1x_1 is y1=Faily_1=Fail, which makes r1r_1 inconsistent. The approach then proceeds through the following steps: 1) Counterfactual Analysis: The counterfactual analysis step generates a counterfactual input x′x together with its observed outcome label y′y obtained by re-executing the system. Here, y′y denotes the system outcome for x′x . Intuitively, x′x shows a minimally perturbed input whose observed outcome aligns with the rule assigned verdict, thereby localizing a nearby decision boundary for the inconsistent rule. The step takes as input an inconsistent operational rule r and a labeled simulation dataset D containing test inputs and observed outcomes. It produces a counterfactual evidence file E by generating counterfactual inputs for inputs that expose inconsistencies in r. Concretely, for each inconsistent case (x,y)∈(x,y) , we search for a minimally perturbed input x′x such that the verdict flips, yielding evidence of a local decision boundary for the predicates in r. For our running example, the Counterfactual Analysis step generates a counterfactual input x1′=(ego_speed=8.0, dist_front=4.0, lane_offset=0.1)x_1 = (ego\_speed=8.0, dist\_front=4.0, lane\_offset=0.1) with label y′=Passy =Pass, indicating that a small change to dist_front is sufficient to flip the observed outcome and localize a nearby decision boundary for predicates in r. For each counterfactual, we calculate the feature-wise perturbation as Δ=x′−x =x -x. In our example, the perturbation is −0.2-0.2. The counterfactual x′x is obtained through an L1L_1 minimal-change search (Wachter et al., 2017) over the input space, which identifies the smallest modification that restores agreement between the rule verdict and the observed system behavior. Starting from x, the search incrementally expands the L1L_1 radius and evaluates modified feature assignments until it finds the first configuration x′x that flips the verdict. The resulting evidence file E stores the dataset D, the rule r, the paired inputs (x,x′)(x,x ) together with their labels (y,y′)(y,y ) and perturbation Δ . 2) Rule Refinement Loop: This step takes the evidence E together with the grammar specification G, and historical consistent rules used for the semantic validation. First, a grammar-constrained LLM acts as a synthesis assistant to propose a candidate refinement of r. Through zero-shot instruction prompting with a reference format exemplar and constraint-based guidance, the prompt provides the paired boundary inputs (x,y)(x,y) and (x′,y′)(x ,y ) and the corresponding Δ from E and instructs the LLM to produce r′r , a refinement of r, with minimal, grammar-compliant predicate changes such as threshold adjustments, operator replacements, or selective addition or removal of conjuncts and disjuncts. The template is provided below: Prompt template. Input: G; inconsistent rule r; historical rules; evidence. Task: Return a refined rule r′r in the syntax of G and a short explanation. Loop: If r′r uses out-of-vocabulary tokens or conflicts with historical rules, re-prompt with the failure summary and regenerate. Format exemplar: (0<ARG2<5)∧(ARG1>0)∨(8<ARG2<12)(0<ARG2<5) (ARG1>0)\ \ (8<ARG2<12) The objective of the refinement is to restore consistency with the observed system behavior while preserving the rule’s original semantics and interpretability and remaining within the grammar constraints. For our running example, the grammar-constrained refinement identifies the predicate in r1r_1 most responsible for the inconsistency. Since r1r_1 is a Pass rule whose verdict on x1x_1 is Pass while the observed outcome is Fail, the refinement makes the rule more restrictive to exclude the failing region. The LLM proposes tightening the dist_front condition and the candidate refinement yields r1⋆:(dist_front<4.1)∧(ego_speed>0)r_1 :( dist\_front<4.1) ( ego\_speed>0). Tightening the threshold from 5.05.0 to 4.14.1 therefore shrinks the admissible region so that it excludes the failing neighborhood while preserving the original intent of the rule and keeping the refinement minimal. In addition to the objective, the prompt instructs the LLM to propose a candidate refinement that remains consistent with the rule set ℛR. The rule set consistency is enforced by checking rule candidates on the labeled executions D before acceptance, subject to the following conditions: • (i) No contradictions: there is no (x,y)∈(x,y) such that a pass rule and a fail rule both hold on x. We use SMT satisfiability (De Moura and Bjørner, 2008) to check the satisfiability of opposite class rules and flag any potential overlap that can be treated as a contradiction. • (i) Preserved consistency: for any (x,y)∈(x,y) where a historical rule in ℛR was consistent, adding the candidate refinement does not make that rule inconsistent; • (i) Target inconsistency resolved: the candidate reduces mismatches between the target rule verdict and the observed outcome label. If the candidate violates the allowed vocabulary, or fails these checks, the loop re-initializes the refinement process. Before termination, each surviving candidate undergoes semantic validation on D to ensure that it restores consistency without introducing new inconsistencies. The refinement rule r⋆r is returned only if it passes validation; otherwise, the loop continues. The grammar conformance is enforced through prompt-level constraints, including a whitelist of allowed tokens and operators (e.g., ∧,∨,<,>,≤,≥\ , ,<,>,≤,≥\) and domain feature names. The full prompt and the examples are provided in our shared package (Khouloud Gaaloul, Zaid Ghazal, Madhu Latha Pulimi, Sam Emmanuel Kathiravan, 2026). The output of the framework is (i) the refinement rule r⋆r expressed in the syntax of the grammar, (i) the change log summarizing the changes applied to r, and (i) a short explanation of how the refinement addresses the observed inconsistencies. 3. Experimental Exploration In this section, we conduct a first experimental exploration on our running case-study system, an autonomous driving control system (Biagiola and Klikovits, 2024) that implements autopilot control for both lateral and longitudinal guidance in lane-following scenarios. The input vector includes numeric signals from both the ego-vehicle and the environment such as speed, steering angle, road curvature, weather, and obstacle distance. The system processes the inputs to compute throttle and steering adjustments that ensure lane keeping. The safety requirement is that the vehicle maintains its lane within admissible bounds. We randomly generate 198 inputs, execute one run per input, and label each run Pass if the requirement holds, and Fail otherwise. To evaluate our framework, we report five evaluation metrics: (1) Decisiveness gain (DG) measures how consistently the rule’s verdict matches the actual simulation outcomes. We compute 1−NℎN1- N_mismatchN, where NℎN_mismatch denotes the number of runs for which the rule does not match the ground truth verdict, and total runs N. (2) Semantic validity (SV) measures whether the refined rule stays grounded in the provided ODD and current operational rules. We use expert ratings to mark a predicate as invalid if it introduces an out-of-range bound, a variable not present in the input vector, or an unsupported operator that violates the grammar or data constraints. We compute 1−N1- N_invalidN_pred, where N_invalid is the number of invalid predicates and N_pred is the total number of predicates. (3) Interpretability (I) measures whether the LLM explanation is easy to follow and justifies all refinements. We use expert ratings: 1.01.0 (Excellent) if the explanation (i) identifies and isolates inconsistencies in the original rule, (i) presents the refined rule, and (i) clearly justifies each major change. We assign 0.70.7 to 0.80.8 (High) when the explanation may not cover every edit but provides specific, well matched justifications for the main refinements. We assign 0.50.5 (Low) when the explanation remains generic and does not justify the specific changes that were needed for most predicates. (4) Grammar compliance (GC) measures the structural correctness of the refined rule, i.e., whether it preserves the grammar’s disjunctive and conjunctive structure and follows the format exemplar in the prompt. We tokenize the rule (e.g., ‘operator’, ARG, Value, ‘(’, ‘(’) and count the structural violations as tokens that break the grammar. We then compute 1−N1- N_violN_tok, where N_viol is the number of violating tokens and N_tok is the total number of tokens. (5) Change minimality (CM) measures how conservatively the LLM refines the rule while preserving the original constraints. We use expert ratings: 1.01.0 (Optimal) for pruning to the logical core with minimal edits and the same variables (e.g., ARG2 > 3 AND ARG2 > 5 → ARG2 > 5). We assign 0.70.7 to 0.80.8 (Conservative) for moderate cleanup or added complementary operators (e.g., adding an upper bound to ARG2 > 5) without changing variables. We assign 0.40.4 to 0.50.5 (Over constrained) when the rule adds unjustified bounds that narrow its scope (e.g., ARG1 > 0 → 1 < ARG1 < 2). We assign 0.00.0 to 0.30.3 (Low) for extensive rewrites where most predicates change and the rule logic shifts substantially. Conventional baseline. We adopt a genetic programming based baseline from prior work for inferring grammar constrained assertions (Gaaloul et al., 2021; Jodat et al., 2025) that assign pass and fail verdicts to system test inputs. Prior results report high inconsistency rates, quantified using accuracy and misprediction metrics across multiple systems and requirements. From the prior work, we used a dataset of N=198N=198 labeled runs and a representative pass rule for an ADS controller system in the open-source BeamNG simulator (2). We observed a decisiveness gain of =0.86DG=0.86, with Nℎ=27N_mismatch=27 runs, indicating that the pass rule was inconsistent. We then applied our approach to this inconsistent rule using 88 LLM variants (Zhao et al., 2023): GPT-5 (Thinking and Instant), Claude Sonnet 4.5, DeepSeek (DeepThinking and Normal), Qwen3 Max, and Gemini 1.5 (Pro and Flash). Under the same grammar G and prompt template, we recorded the refined rules along with a change log and explanation. We then computed decisiveness on the 198198 labeled runs for all variants. All variants reduced mismatches to 0 (=1.0DG=1.0), corresponding to a gain of +0.14+0.14 over the baseline. These results indicate that our approach resolved the inconsistencies of the original rule and improved alignment between operational rule verdicts and observed system behavior. LLM Variant Study. Given the promising preliminary observations, we assess how refinement quality varies with model choice in our language-in-the-loop setting and we retrieve lessons learned about LLM use in safety operational contexts. We analyze the refined rules, change logs, and explanations generated by our approach configured with the 88 LLM variants. Table 2. Evaluation metric scores per LLM variant. This table reports, for each evaluated LLM variant, the scores of four evaluation metrics: GC (grammar compliance), SV (semantic validity), I (interpretability), and CM (change minimality). Higher values indicate better performance on the corresponding metric; boldface highlights the best observed scores. LLM GC SV I CM LLM GC SV I CM GPT5 Thinking 1.0 1.0 0.5 0.9 Qwen3 Max 1.0 0.8 0.7 0.7 GPT5 Instant 1.0 0.7 0.7 0.4 DeepSeek DeepThinking 0.5 0.5 0.7 0.3 Gemini Flash 2.5 1.0 1.0 0.8 0.7 DeepSeek Normal 0.7 1.0 0.5 0.8 Gemini Pro 2.5 1.0 0.4 0.7 0.2 Claude Sonnet 4.5 1.0 0.2 1.0 0.0 Table 2 reports four metric scores for each LLM. GPT5 Thinking mode shows the strongest combination of semantic validity and minimality while staying fully grammar compliant. Gemini Flash 2.5 and Qwen3 also remain grammar compliant with relatively strong semantic validity. In contrast, Gemini Pro 2.5 and Claude Sonnet 4.5 are grammar compliant and fairly interpretable. DeepSeek exhibits mixed behavior, with the Normal variant achieving high semantic validity and minimality but lower interpretability, while DeepThinking shows weaker grammar compliance and more extensive changes. We retrieve the following lessons: Lesson 1: Even with the same grammar, prompt, and simulation data, different LLMs vary in outcome. Some rules look correct but include formatting that breaks the expected structure and variable naming. These should be treated as unsafe to apply. For example, DeepSeek DeepThinking returned the rule inside a markdown code block and wrapped the rule with an extra outer list , which violates the structure. The expected rule is [(’greater_than_func’,’ARG1’,’0’)]… [('greater\_than\_func','ARG1','0')]..., but the model returned [[(’greater_than_func’,’ARG1’,’0’)]...]. Lesson 2: LLMs tend to increase apparent safety by tightening bounds and occasionally adding extra constraints, but this can over constrain the rule in a conservative way that is not correctly grounded in the provided ODD, yielding many unnecessary nominal restrictions. For example, a refined rule may turn a simple threshold into a tight range, changing 0 < ARG1 to 0 < ARG1 < 8. This can look safer, yet it may be unsupported by the provided ODD and therefore unjustified. In safety critical use, validity checks against the ODD should be adopted to flag new or tightened bounds that are not semantically valid, and an iterative feedback loop should be triggered whenever the model makes large threshold shifts, violates the grammar, or introduces new variables, even if the explanation appears convincing. Lesson 3: There is a link between how much a model changes the rule and how easy its output is to interpret. When changes are broader, the model explicitly critiques the original inconsistencies and justifies each major change. For example GPT5 Thinking mode makes small, targeted refinements, reducing the rule to ARG1 > 0 or ARG2 > 3, and its justification only focuses on redundancy removal and fixing a malformed predicate. In contrast, Gemini Pro 2.5 introduces new conjunctive constraints and new variables (ARG3) alongside operator changes, and it provides a structured rationale for each addition, for example explaining the shift to >= at the boundary and motivating the new < caps. This initial study shows that grammar-constrained, counterfactual-guided refinement can eliminate baseline inconsistencies, while the LLM variant study reveals model dependent quality and safety trade-offs that illustrate “what can go wrong”. Although grammar guidance supports syntactic correctness, safety guarantees require additional strategies. Additional limitations and future directions are summarized in the next section. 4. Conclusion and Future Work Safety operational rules can lose alignment with observed system behavior as systems and operating environments evolve. This paper introduced a rule refinement framework that combines counterfactual reasoning with a grammar-constrained LLM refinement loop to produce interpretable refinements that are syntactically correct and semantically valid. An initial study on an autonomous driving subsystem showed that our loop eliminates inconsistencies produced by the selected conventional method, with +0.14+0.14 decisiveness. An LLM variant study further exposed model dependent quality and safety trade offs, including syntactic violations and overly conservative refinements that risk overfitting to the observed dataset. Limitations and Future Work. The results of our initial exploration showed that grammar guidance alone does not provide safety guarantees and may still yield semantically unjustified refinements under limited evidence. Our current study is preliminary and focuses on a single subsystem and dataset. Accordingly, future work focuses on (i) strengthening grammar enforcement via a strongly typed rule generator and a parser based acceptance mechanism that rejects any output violating the grammar or structural format; (i) reinforcing semantic validation beyond a static regression test suite through simulation based falsification and robustness testing to ensure consistency over a broader input space and the stated ODD, while flagging unjustified tightened constraints and exposing unsafe overfitting; and (i) mitigating overly conservative refinements by incorporating change minimality into an independent selection mechanism so edits are penalized even when decisiveness is high. For the evaluation, we will broaden baselines and study subjects to determine whether grammar-constrained LLM refinement offers clear benefits over established interpretable rule learning and specification mining, including decision trees and decision rules and temporal specification mining methods. We will then scale experiments across multiple ADS subsystems, requirements, and ODDs, and study how expanded grammars, prompting strategies, and robust validation mechanisms affect refinement quality and reduce safety risks. Acknowledgements.This material is based upon work supported by the National Science Foundation under Grant No. 2347294. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation. References E. Asarin, A. Donzé, O. Maler, and D. Nickovic (2011) Parametric identification of temporal properties. In International Conference on Runtime Verification, p. 147–160. Cited by: §1. [2] (Accessed: January 2026)BeamNG.tech(Website) External Links: Link Cited by: §3. M. Biagiola and S. Klikovits (2024) SBFT tool competition 2024 - cyber-physical systems track. In Proceedings of the 17th ACM/IEEE International Workshop on Search-Based and Fuzz Testing, SBFT 2024, Lisbon, Portugal, 14 April 2024, p. 33–36. External Links: Link, Document Cited by: §3. L. De Moura and N. Bjørner (2008) Z3: an efficient smt solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, p. 337–340. Cited by: 1st item. R. Debouk (2019) Overview of the second edition of iso 26262: functional safety—road vehicles. Journal of System Safety 55 (1), p. 13–21. Cited by: §1. L. Fraade-Blanar, M. S. Blumenthal, J. M. Anderson, and N. Kalra (2018) Measuring automated vehicle safety: forging a framework. RAND Corporation, Santa Monica, CA. External Links: ISBN 978-1-9774-0164-9, Link Cited by: §1. K. Gaaloul, C. Menghi, S. Nejati, L. C. Briand, and Y. I. Parache (2021) Combining genetic programming and model checking to generate environment assumptions. IEEE Transactions on Software Engineering 48 (9), p. 3664–3685. Cited by: §1, §2.1, §3. A. García, D. Llopis-Castelló, and F. J. Camacho-Torregrosa (2022) From the vehicle-based concept of operational design domain to the road-based concept of operational road section. Frontiers in Built Environment 8, p. 901840. Cited by: §1. B. Hoxha, A. Dokhanchi, and G. Fainekos (2018) Mining parametric temporal logic properties in model-based design for cyber-physical systems. International Journal on Software Tools for Technology Transfer 20 (1), p. 79–93. Cited by: §1. S. Jha, A. Tiwari, S. A. Seshia, T. Sahai, and N. Shankar (2019) TeLEx: learning signal temporal logic from positive examples using tightness metric. Formal Methods in System Design 54 (3), p. 364–387. Cited by: §1. B. A. Jodat, A. Chandar, S. Nejati, and M. Sabetzadeh (2024) Test generation strategies for building failure models and explaining spurious failures. ACM Transactions on Software Engineering and Methodology 33 (4), p. 1–32. Cited by: §1. B. A. Jodat, K. Gaaloul, M. Sabetzadeh, and S. Nejati (2025) Automated test oracles for flaky cyber-physical system simulators: approach and evaluation. arXiv preprint arXiv:2508.20902. Cited by: §1, §3. Khouloud Gaaloul, Zaid Ghazal, Madhu Latha Pulimi, Sam Emmanuel Kathiravan (2026) Additional materials. Note: https://replication66.github.io/SEAMS2026/ Cited by: §2.2. O. Kirovskii and V. Gorelov (2019) Driver assistance systems: analysis, tests and the safety case. iso 26262 and iso pas 21448. In IOP Conference Series: Materials Science and Engineering, Vol. 534, p. 012019. Cited by: §1. P. Kyriakis, J. V. Deshmukh, and P. Bogdan (2019) Specification mining and robust design under uncertainty: a stochastic temporal logic approach. ACM Transactions on Embedded Computing Systems (TECS) 18 (5s), p. 1–21. Cited by: §1. C. Lemieux, D. Park, and I. Beschastnikh (2015) General ltl specification mining (t). In 2015 30th IEEE/ACM International Conference on Automated Software Engineering (ASE), p. 81–92. Cited by: §1. J. Li, M. Tian, and B. Zhong (2025) Automatic generation of safety-compliant linear temporal logic via large language model: a self-supervised framework. arXiv preprint arXiv:2503.15840. Cited by: §1. A. Nouri, B. Cabrero-Daniel, F. Törner, H. Sivencrona, and C. Berger (2024) Engineering safety requirements for autonomous driving with large language models. In 2024 IEEE 32nd International Requirements Engineering Conference (RE), p. 218–228. Cited by: §1. A. Pnueli (1977) The temporal logic of programs. In 18th annual symposium on foundations of computer science (sfcs 1977), p. 46–57. Cited by: §1. N. Rescher and A. Urquhart (2012) Temporal logic. Vol. 3, Springer Science & Business Media. Cited by: §1. C. E. Tuncali, G. Fainekos, H. Ito, and J. Kapinski (2018) Simulation-based adversarial test generation for autonomous vehicles with machine learning components. In 2018 IEEE intelligent vehicles symposium (IV), p. 1555–1562. Cited by: §1. S. Wachter, B. Mittelstadt, and C. Russell (2017) Counterfactual explanations without opening the black box: automated decisions and the gdpr. Harv. JL & Tech. 31, p. 841. Cited by: §2.2. W. X. Zhao, K. Zhou, J. Li, T. Tang, X. Wang, Y. Hou, Y. Min, B. Zhang, J. Zhang, Z. Dong, et al. (2023) A survey of large language models. arXiv preprint arXiv:2303.18223 1 (2). Cited by: §3. X. Zhu, D. Wang, W. Pedrycz, and Z. Li (2022) Fuzzy rule-based local surrogate models for black-box model explanation. IEEE Transactions on Fuzzy Systems 31 (6), p. 2056–2064. Cited by: §1.