arXiv:2604.23523v1 [cs.SE] 26 Apr 2026
Grammar-Constrained Refinement of Safety Operational Rules Using Language in the Loop: What Could Go Wrong Khouloud Gaaloul
Zaid Ghazal
Madhu Latha Pulimi
University of Michigan–Dearborn Dearborn, MI, USA [email protected]
University of Michigan–Dearborn Dearborn, MI, USA [email protected]
University of Michigan–Dearborn Dearborn, MI, USA [email protected]
Sam Emmanuel Kathiravan University of Michigan–Dearborn Dearborn, MI, USA [email protected]
Abstract
1
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 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) [6, 8] and informed by ISO 26262 [5] and ISO/PAS 21448 (SOTIF) [14]. They are typically expressed as logical or quantitative constraints over environmental and system variables, and evaluated through simulation-based testing [21] 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 [19, 20] and by applying specification mining and machine learning (ML) methods [10, 16], typically constrained by templates rather than a domain-specific grammar. Other works use surrogate models [11, 12, 24] and genetic programming (GP) [7] as interpretable methods to infer and correct STL properties, or apply parameter mining and falsification [2, 9, 15] 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. [18] 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. [17] 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
CCS Concepts • Software and its engineering → Software safety.
Keywords Safety Operational Rule Refinement, Large Language Models, CyberPhysical Systems ACM Reference Format: Khouloud Gaaloul, Zaid Ghazal, Madhu Latha Pulimi, and Sam Emmanuel Kathiravan. 2026. Grammar-Constrained Refinement of Safety Operational Rules Using Language in the Loop: What Could Go Wrong. In 21st International Conference on Software Engineering for Adaptive and Self-Managing Systems (SEAMS ’26), April 13–14, 2026, Rio de Janeiro, Brazil. ACM, New York, NY, USA, 6 pages. https://doi.org/10.1145/3788550.3794884
This work is licensed under a Creative Commons Attribution 4.0 International License. SEAMS ’26, Rio de Janeiro, Brazil © 2026 Copyright held by the owner/author(s). ACM ISBN 979-8-4007-2445-9/2026/04 https://doi.org/10.1145/3788550.3794884
Introduction
SEAMS ’26, April 13–14, 2026, Rio de Janeiro, Brazil
Gaaloul et al.
Table 1: Consistency of an operational rule 𝑟 on a given input vector 𝑥 with respect to its rule set group and outcome 𝑦 of 𝑥.
CONSISTENT Rule
Sim ulation D at a
INCONSISTENT Rule
O perational R ules
D om ain- specific Gram m ar
H istorical R ules
Logs & Explanations
R ule R efinem ent L oop Counter factual A nalysis Re-prompt generates counterfactual inputs Counterfactual Semantic evidence Grammar-Constrained on the decision boundary of LLM R ule Synthesis Refined Validation inconsistent rule R ule
Figure 1: Operational Rule Refinement Approach Overview. 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.
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
Rule Set
Rule Verdict
𝑟 (𝑥 )
Observed 𝑦
Consistency
𝑅Pass 𝑅Fail 𝑅Pass 𝑅Fail 𝑅Pass 𝑅Fail
Pass Fail Pass Fail Pass Fail
true true true true false false
Pass Pass Fail Fail – –
Consistent Inconsistent Inconsistent Consistent Inconclusive Inconclusive
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 𝑋 ⊆ R𝑑 denote the input domain of the system under test (SUT), where each input vector 𝑥 = [𝑖 1, . . . , 𝑖𝑑 ] represents input variables. The label of 𝑥 is 𝑦, where 𝑦 = Pass if the observed system outcome satisfies the safety requirement, and 𝑦 = 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 𝑟 : 𝑋 → {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, 𝑟 (𝑥) = true means that the rule holds for 𝑥, i.e., the input is considered valid within the admissible operating region, while 𝑟 (𝑥) = false indicates that the rule does not hold. For example, given a rule 𝑟 1 : (dist_front < 5.0) ∧ (ego_speed > 0) and an input vector 𝑥 1 = (ego_speed=8.0, dist_front=4.2, lane_offset=0.1), 𝑟 1 (𝑥 1 ) = true, indicating that 𝑥 1 is valid and satisfies the admissible condition expressed by 𝑟 1 . This indicates that, at speed 8.0 the ego vehicle is operating in a safe state where the front vehicle is within 5.0 units of distance, so the scenario lies inside the region of the input space that 𝑟 1 designates as admissible for the system’s controller with respect to the safety requirement. We consider two rule sets, 𝑅Pass and 𝑅Fail , encoding all operational rules 𝑟 that imply Pass or Fail, respectively, on a given input 𝑥. Table 1 summarizes how an operational rule 𝑟 is interpreted on an input vector 𝑥 given the rule set to which 𝑟 belongs and the observed system outcome 𝑦 for 𝑥. A rule set determines the rule verdict. Rules in 𝑅Pass assign a Pass verdict when they hold on 𝑥, while rules in 𝑅Fail assign a Fail verdict when they hold on 𝑥. The column 𝑟 (𝑥) reports whether the rule holds on 𝑥. When 𝑟 (𝑥) = true, the rule makes a definitive verdict and its consistency is determined by comparing that verdict to the observed outcome 𝑦. A rule in 𝑅Pass is consistent if 𝑦 = Pass, i.e., the rule holds on 𝑥 and correctly assigns a passing verdict, and inconsistent if 𝑦 = Fail, i.e., the rule holds on 𝑥 but incorrectly assigns a Pass verdict while the observed outcome is a failure. A rule in 𝑅Fail is consistent if 𝑦 = Fail, i.e., the rule holds on 𝑥 and correctly assigns a failing verdict, and inconsistent if 𝑦 = Pass, i.e., the rule holds on 𝑥 but incorrectly assigns a Fail verdict while the observed outcome is a pass. When 𝑟 (𝑥) = false, the rule does not apply to 𝑥 and therefore yields no definitive verdict. This case is labeled inconclusive and the outcome
Grammar-Constrained Refinement of Safety Operational Rules Using Language in the Loop: What Could Go Wrong
𝑦 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 𝑟 1 ∈ 𝑅Pass as a pass rule and the observed outcome of 𝑥 1 is 𝑦1 = Fail, which makes 𝑟 1 inconsistent. This indicates that 𝑥 1 satisfies the admissible condition encoded by 𝑟 1 , so the rule assigns a pass verdict, yet the system execution on 𝑥 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 𝐺 introduced in prior work [7] to express environmental assumptions for cyber-physical systems, as it is particularly suited to the automotive context studied here. Each operational rule is a hierarchical logiRule ::= Disj cal formula built from disjunctions (𝐷𝑖𝑠 𝑗), conjunctions Disj ::= Disj ∨ Conj | Conj (𝐶𝑜𝑛 𝑗), and relational prediConj ::= Conj ∧ Rel | Rel cates (𝑅𝑒𝑙) over arithmetic exRel ::= Exp rop Exp pressions (𝐸𝑥𝑝). A rule is comrop ::=<| ≤ |>| ≥ |=|≠ posed of one or more disjuncExp ::= Exp aop Exp | const | var tive clauses, each representing aop ::= + | − | ∗ | / an alternative valid operating condition. Each predicate 𝑅𝑒𝑙 compares two expressions 𝐸𝑥𝑝 using operators {<, ≤, >, ≥, =, ≠}, where expressions are formed from arithmetic operations over constants (𝑐𝑜𝑛𝑠𝑡) and input variables (𝑣𝑎𝑟 ). Problem Statement. Given the rule sets 𝑅Pass and 𝑅Fail , and a labeled input set 𝑇 = {(𝑥𝑖 , 𝑦𝑖 )}, 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; (ii) Reduce the number of inconsistent rules; (iii) 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 𝐺). Figure 1 shows the overview of our approach. The framework takes as input (1) an operational rule set R containing
SEAMS ’26, April 13–14, 2026, Rio de Janeiro, Brazil
at least one inconsistent rule 𝑟 , (2) a grammar specification 𝐺 (3) a labeled execution dataset D of simulation or test cases. Each test case contains an input vector 𝑥 of input values and an observed outcome 𝑦 ∈ Pass, Fail with respect to a given safety specification. For example, the input vector 𝑥 1 , 𝑟 1 assigns the 𝑥 1 a Pass verdict. However, the observed system outcome for 𝑥 1 is 𝑦1 = Fail, which makes 𝑟 1 inconsistent. The approach then proceeds through the following steps: 1) Counterfactual Analysis: The counterfactual analysis step generates a counterfactual input 𝑥 ′ together with its observed outcome label 𝑦 ′ obtained by re-executing the system. Here, 𝑦 ′ denotes the system outcome for 𝑥 ′ . Intuitively, 𝑥 ′ 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 𝑟 and a labeled simulation dataset D containing test inputs and observed outcomes. It produces a counterfactual evidence file 𝐸 by generating counterfactual inputs for inputs that expose inconsistencies in 𝑟 . Concretely, for each inconsistent case (𝑥, 𝑦) ∈ D, we search for a minimally perturbed input 𝑥 ′ such that the verdict flips, yielding evidence of a local decision boundary for the predicates in 𝑟 . For our running example, the Counterfactual Analysis step generates a counterfactual input 𝑥 1′ = (ego_speed=8.0, dist_front=4.0, lane_offset=0.1) with label 𝑦 ′ = 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 𝑟 . For each counterfactual, we calculate the feature-wise perturbation as Δ = 𝑥 ′ − 𝑥. In our example, the perturbation is −0.2. The counterfactual 𝑥 ′ is obtained through an 𝐿1 minimal-change search [22] over the input space, which identifies the smallest modification that restores agreement between the rule verdict and the observed system behavior. Starting from 𝑥, the search incrementally expands the 𝐿1 radius and evaluates modified feature assignments until it finds the first configuration 𝑥 ′ that flips the verdict. The resulting evidence file 𝐸 stores the dataset D, the rule 𝑟 , the paired inputs (𝑥, 𝑥 ′ ) together with their labels (𝑦, 𝑦 ′ ) and perturbation Δ. 2) Rule Refinement Loop: This step takes the evidence 𝐸 together with the grammar specification 𝐺, 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 𝑟 . Through zero-shot instruction prompting with a reference format exemplar and constraint-based guidance, the prompt provides the paired boundary inputs (𝑥, 𝑦) and (𝑥 ′, 𝑦 ′ ) and the corresponding Δ from 𝐸 and instructs the LLM to produce 𝑟 ′ , a refinement of 𝑟 , 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: 𝐺; inconsistent rule 𝑟 ; historical rules; evidence. Task: Return a refined rule 𝑟 ′ in the syntax of 𝐺 and a short explanation. Loop: If 𝑟 ′ 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)
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
SEAMS ’26, April 13–14, 2026, Rio de Janeiro, Brazil
constraints. For our running example, the grammar-constrained refinement identifies the predicate in 𝑟 1 most responsible for the inconsistency. Since 𝑟 1 is a Pass rule whose verdict on 𝑥 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 𝑟 1★ : (dist_front < 4.1) ∧ (ego_speed > 0). Tightening the threshold from 5.0 to 4.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 (𝑥, 𝑦) ∈ D such that a pass rule and a fail rule both hold on 𝑥. We use SMT satisfiability [4] to check the satisfiability of opposite class rules and flag any potential overlap that can be treated as a contradiction. • (ii) Preserved consistency: for any (𝑥, 𝑦) ∈ D where a historical rule in R was consistent, adding the candidate refinement does not make that rule inconsistent; • (iii) 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 𝑟 ★ 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 [13]. The output of the framework is (i) the refinement rule 𝑟 ★ expressed in the syntax of the grammar, (ii) the change log summarizing the changes applied to 𝑟 , and (iii) 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 [3] 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:
Gaaloul et al.
(1) Decisiveness gain (DG) measures how consistently the rule’s verdict matches the actual simulation outcomes. We compute 1 − 𝑁 mismatch , where Nmismatch denotes the number of runs for which the 𝑁 rule does not match the ground truth verdict, and total runs 𝑁 . (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 − 𝑁invalid , where 𝑁 invalid is the number pred of invalid predicates and 𝑁 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.0 (Excellent) if the explanation (i) identifies and isolates inconsistencies in the original rule, (ii) presents the refined rule, and (iii) clearly justifies each major change. We assign 0.7 to 0.8 (High) when the explanation may not cover every edit but provides specific, well matched justifications for the main refinements. We assign 0.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 − 𝑁viol , where 𝑁 viol is the tok number of violating tokens and 𝑁 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.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.7 to 0.8 (Conservative) for moderate cleanup or added complementary operators (e.g., adding an upper bound to ARG2 > 5) without changing variables. We assign 0.4 to 0.5 (Over constrained) when the rule adds unjustified bounds that narrow its scope (e.g., ARG1 > 0 → 1 < ARG1 < 2). We assign 0.0 to 0.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 [7, 12] 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 𝑁 = 198 labeled runs and a representative pass rule for an ADS controller system in the open-source BeamNG simulator [1]. We observed a decisiveness gain of DG = 0.86, with 𝑁 mismatch = 27 runs, indicating that the pass rule was inconsistent. We then applied our approach to this inconsistent rule using 8 LLM variants [23]: 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 𝐺 and prompt template, we recorded the refined rules along with a change log and explanation. We then computed decisiveness on the 198 labeled runs for all variants. All variants reduced mismatches to 0 (DG = 1.0), corresponding to a gain of +0.14 over the baseline. These results indicate that our approach resolved
Grammar-Constrained Refinement of Safety Operational Rules Using Language in the Loop: What Could Go Wrong
Table 2: Evaluation metric scores per LLM variant. LLM
GC
SV
I
CM
LLM
GC
SV
I
CM
GPT5 Thinking GPT5 Instant Gemini Flash 2.5 Gemini Pro 2.5
1.0 1.0 1.0 1.0
1.0 0.7 1.0 0.4
0.5 0.7 0.8 0.7
0.9 0.4 0.7 0.2
Qwen3 Max DeepSeek DeepThinking DeepSeek Normal Claude Sonnet 4.5
1.0 0.5 0.7 1.0
0.8 0.5 1.0 0.2
0.7 0.7 0.5 1.0
0.7 0.3 0.8 0.0
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 8 LLM variants. 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’)]..., 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
SEAMS ’26, April 13–14, 2026, Rio de Janeiro, Brazil
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, counterfactualguided 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 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; (ii) 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 (iii) 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.
Acknowledgments 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 [1] Accessed: January 2026. BeamNG.tech. https://beamng.tech
SEAMS ’26, April 13–14, 2026, Rio de Janeiro, Brazil
[2] Eugene Asarin, Alexandre Donzé, Oded Maler, and Dejan Nickovic. 2011. Parametric identification of temporal properties. In International Conference on Runtime Verification. Springer, 147–160. [3] Matteo Biagiola and Stefan Klikovits. 2024. SBFT Tool Competition 2024 - CyberPhysical Systems Track. In Proceedings of the 17th ACM/IEEE International Workshop on Search-Based and Fuzz Testing, SBFT 2024, Lisbon, Portugal, 14 April 2024. ACM, 33–36. doi:10.1145/3643659.3643932 [4] Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 337–340. [5] Rami Debouk. 2019. Overview of the second edition of ISO 26262: Functional safety—Road vehicles. Journal of System Safety 55, 1 (2019), 13–21. [6] Laura Fraade-Blanar, Marjory S. Blumenthal, James M. Anderson, and Nidhi Kalra. 2018. Measuring Automated Vehicle Safety: Forging a Framework. RAND Corporation, Santa Monica, CA. https://www.rand.org/pubs/research_reports/ RR2662.html [7] Khouloud Gaaloul, Claudio Menghi, Shiva Nejati, Lionel C Briand, and Yago Isasi Parache. 2021. Combining genetic programming and model checking to generate environment assumptions. IEEE Transactions on Software Engineering 48, 9 (2021), 3664–3685. [8] Alfredo García, David Llopis-Castelló, and Francisco Javier Camacho-Torregrosa. 2022. From the vehicle-based concept of operational design domain to the roadbased concept of operational road section. Frontiers in Built Environment 8 (2022), 901840. [9] Bardh Hoxha, Adel Dokhanchi, and Georgios 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 (2018), 79– 93. [10] Susmit Jha, Ashish Tiwari, Sanjit A Seshia, Tuhin Sahai, and Natarajan Shankar. 2019. TeLEx: learning signal temporal logic from positive examples using tightness metric. Formal Methods in System Design 54, 3 (2019), 364–387. [11] Baharin A Jodat, Abhishek Chandar, Shiva Nejati, and Mehrdad Sabetzadeh. 2024. Test generation strategies for building failure models and explaining spurious failures. ACM Transactions on Software Engineering and Methodology 33, 4 (2024), 1–32. [12] Baharin A Jodat, Khouloud Gaaloul, Mehrdad Sabetzadeh, and Shiva Nejati. 2025. Automated Test Oracles for Flaky Cyber-Physical System Simulators: Approach
Gaaloul et al.
and Evaluation. arXiv preprint arXiv:2508.20902 (2025). [13] Khouloud Gaaloul, Zaid Ghazal, Madhu Latha Pulimi, Sam Emmanuel Kathiravan. 2026. Additional Materials. https://replication66.github.io/SEAMS2026/. [14] OM Kirovskii and VA 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. IOP Publishing, 012019. [15] Panagiotis Kyriakis, Jyotirmoy V Deshmukh, and Paul Bogdan. 2019. Specification mining and robust design under uncertainty: A stochastic temporal logic approach. ACM Transactions on Embedded Computing Systems (TECS) 18, 5s (2019), 1–21. [16] Caroline Lemieux, Dennis Park, and Ivan Beschastnikh. 2015. General LTL specification mining (T). In 2015 30th IEEE/ACM International Conference on Automated Software Engineering (ASE). IEEE, 81–92. [17] Junle Li, Meiqi Tian, and Bingzhuo Zhong. 2025. Automatic Generation of Safetycompliant Linear Temporal Logic via Large Language Model: A Self-supervised Framework. arXiv preprint arXiv:2503.15840 (2025). [18] Ali Nouri, Beatriz Cabrero-Daniel, Fredrik Törner, Håkan Sivencrona, and Christian Berger. 2024. Engineering safety requirements for autonomous driving with large language models. In 2024 IEEE 32nd International Requirements Engineering Conference (RE). IEEE, 218–228. [19] Amir Pnueli. 1977. The temporal logic of programs. In 18th annual symposium on foundations of computer science (sfcs 1977). ieee, 46–57. [20] Nicholas Rescher and Alasdair Urquhart. 2012. Temporal logic. Vol. 3. Springer Science & Business Media. [21] Cumhur Erkan Tuncali, Georgios Fainekos, Hisahiro Ito, and James Kapinski. 2018. Simulation-based adversarial test generation for autonomous vehicles with machine learning components. In 2018 IEEE intelligent vehicles symposium (IV). IEEE, 1555–1562. [22] Sandra Wachter, Brent Mittelstadt, and Chris Russell. 2017. Counterfactual explanations without opening the black box: Automated decisions and the GDPR. Harv. JL & Tech. 31 (2017), 841. [23] Wayne Xin Zhao, Kun Zhou, Junyi Li, Tianyi Tang, Xiaolei Wang, Yupeng Hou, Yingqian Min, Beichen Zhang, Junjie Zhang, Zican Dong, et al. 2023. A survey of large language models. arXiv preprint arXiv:2303.18223 1, 2 (2023). [24] Xiubin Zhu, Dan Wang, Witold Pedrycz, and Zhiwu Li. 2022. Fuzzy rule-based local surrogate models for black-box model explanation. IEEE Transactions on Fuzzy Systems 31, 6 (2022), 2056–2064.