Deterministic Workflow Auditing via Dependency–State Coupled Verification and Explainable Conflict Tracing

1  Introduction

Complex procedural workflows arise ubiquitously in real-world maintenance, laboratory protocols, and parametric design environments, where correctness depends on more than local step semantics. Unlike static recognition or semantic similarity matching, workflow auditing requires reasoning over structural dependencies among steps, precondition constraints, and the dynamic evolution of object states under execution semantics. This requirement is widely reflected in procedural and instructional understanding benchmarks that emphasize long-horizon state changes and compositional step structure, as well as multimodal grounding settings where text must align with visual evidence across time and steps [1–3]. In parametric CAD, workflow steps are further coupled by explicit geometric/constraint relations and program-like design histories, making cross-step bindings and constraint satisfaction first-class signals rather than optional priors [4,5].

In practice, workflow failures are often caused not by a single step being “semantically wrong,” but by implicit dependencies being violated or state constraints not being satisfied, such as missing prerequisite operations, inconsistent parameter bindings, or latent resource conflicts. These inconsistencies typically exhibit long-range error propagation: a small deviation early in the workflow may remain locally unnoticed yet amplify through subsequent state transitions and eventually lead to global failure. From an auditing perspective, practical systems further require reproducible decisions and solver-grade diagnostics. Given identical inputs, an auditor should return the same formal consistency decision, pinpoint the responsible step, element, or relation, and provide checkable evidence that supports repair.

Despite this need, most existing approaches to workflow assessment fall into two paradigms. The first relies on language-based evaluation, where a model generates or judges procedural correctness through chain-of-thought reasoning, self-consistency, or self-refinement prompts. While empirically useful, these approaches depend on implicit semantic representations and often suffer from non-determinism and unfaithful rationales, making it difficult to guarantee consistency, reproducibility, or actionable localization [6–8]. The second paradigm treats workflows as linear sequences and applies step alignment, edit distance, or sequence matching; closely related ideas also appear in process mining via log-to-model alignments and conformance metrics [9–11]. However, real workflows frequently contain commutable substructures, branching dependencies, and cross-step parameter couplings, which cannot be faithfully represented by purely sequential modeling. More broadly, both paradigms tend to conflate semantic plausibility with executability under constraints, and they lack a principled mechanism to expose how an early structural deviation propagates to a later failure, especially when constraints are induced from heterogeneous multimodal sources.

This paper revisits workflow auditing from a verification perspective and argues that formal workflow consistency is inherently a structural consistency problem under state evolution. Our design is inspired by executable verification traditions in planning and constraint solving, where formal consistency is determined by deterministic simulation combined with satisfiability checking [12,13], and by conformance checking work that emphasizes reproducible deviation diagnosis [10]. We propose a dependency–state coupled auditing framework that unifies (i) an explicit typed dependency graph capturing data, precondition, coupling, and mutex/resource relations with (ii) an executable state transition system for deterministic semantics.

We focus on deterministic auditing after workflow parsing, where the input is a structured audit instance consisting of an action sequence, parameter bindings, an initial state, and schema/template constraints. Upstream perception or parsing may be learned, but it is not the primary contribution of this work; its effect is analyzed separately in robustness experiments. Formal consistency is checked by forward execution with incremental satisfiability maintenance over step-wise constraint stores. When an inconsistency is detected, the framework produces compact and reproducible explanations via provenance-guided dependency slicing and traceability [14–17], together with principled conflict extraction based on diagnosis/UNSAT core-style minimality [18,19]. This verification-centric formulation also allows the proposed auditor to serve as a deterministic validator for learned parsers, generative workflow models, or agentic human–AI systems.

Experiments on MyFixit-Audit and Fusion360-Audit demonstrate strong gains over multimodal fusion and LLM-based baselines across binary consistency auditing, inconsistency typing, localization, and structural trace recovery, while ensuring fully deterministic decisions and efficient runtime.

2  Related Work

2.1 Workflow Auditing via Conformance Checking and Executable Verification

Workflow auditing is related to conformance checking in process mining, where observed traces are compared against an executable process model (often Petri nets) and deviations are diagnosed via replay or alignment [9–11,20]. Planning and executable verification provide a complementary view: a workflow is formally consistent iff it can be executed from an initial state under formal action semantics while satisfying all step-wise and cross-step constraints; plan validators such as VAL operationalize this idea for PDDL-style models [12]. SAT/SMT solvers enable deterministic decisions about formal consistency and naturally support incremental checking as constraints accumulate across steps [13,21]. Our work aligns with this verification tradition but targets workflows extracted from heterogeneous multimodal sources, requiring an explicit coupling between structural dependencies (graph) and executable state evolution (transition system).

2.2 Explainable Failure Localization: Slicing, Provenance, and UNSAT Cores

Actionable debugging has long relied on dependency analysis: program slicing isolates a compact subset relevant to a failure criterion, with dynamic variants further conditioning on a concrete execution [15]. In constraint-based verification, UNSAT cores provide a principled way to extract small conflicting constraint subsets, closely connected to diagnosis via conflicts and minimal explanations [22]. Provenance offers a formal mechanism to trace how outputs depend on inputs, originally studied in databases and later adopted broadly for traceability [16,17]. Building on these ideas, we maintain step-level provenance for state variables, slice the dependency graph at failure time, extract a (near-)minimal conflict core within the slice, and return graph-grounded propagation traces to make long-range error propagation explicit and reproducible.

2.3 Procedural Understanding, Multimodal Grounding, and LLM Graders

Procedural understanding benchmarks emphasize step-wise state changes and long-horizon dependencies [1]. Multimodal instruction grounding extends this to text–image/video alignment and step reasoning [2,3,23], while domain datasets such as repair manuals and parametric CAD sequences expose practical noise, implicit couplings, and explicit structure [4,5,24–26]. In practice, LLM-based graders using chain-of-thought, voting, and self-refinement are also used for procedural assessment, but they can be non-deterministic and their explanations may be hard to reproduce [6–8]. Even with schema-constrained outputs, format compliance does not guarantee faithful reasoning, as highlighted by structured-output benchmarks [27]. Our verifier is complementary: it allows upstream learned components (e.g., encoders or matching models) [28–31], while producing deterministic formal-consistency decisions and solver-grounded explanations (core + trace).

3  Method

3.1 Auditing Boundary and Structured Input

We separate workflow parsing from workflow verification. Let ρ denote raw evidence, such as text, images, CAD structures, or their combination. An upstream parser maps ρ to a structured audit instance:

g:ρ↦ω,ω=⟨π,s0,ℒ,Γ⟩.(1)

Here π is the action sequence, s0 is the initial state, ℒ is the schema and constraint-template library, and Γ stores grounding metadata such as entity identifiers, text–image links, CAD relations, or parser confidence scores. The verifier operates on ω, not directly on raw evidence. Thus, the formal guarantees below are conditional on the structured instance and library; empirical errors may additionally reflect upstream parsing or grounding noise. Perturbations such as image swaps may occur before parsing, whereas entity, count/specification, or relation swaps can also be injected directly into ω.

Let 𝒳={x1,…,xn} be the state variables, and let s∈𝒮 be an assignment to them. Each step is a parameterized action at(θt), where at∈𝒜 and θt∈Θ. The workflow is

π=⟨a1(θ1),…,aT(θT)⟩.(2)

Fig. 1 illustrates the overall architecture of our verifier-in-the-loop auditing pipeline. All core functional components detailed in the following subsections are encapsulated within this unified incremental verification framework.

Figure 1: Verifier-in-the-loop workflow auditing pipeline. Raw or multimodal evidence is first converted by an upstream parser into a structured audit instance. The proposed verifier then instantiates action schemas and constraint templates, maintains an executable state and a typed dependency graph, and incrementally checks preconditions, invariants, parameter couplings, and mutex/resource constraints. When a violation is detected, provenance-guided slicing, conflict-core extraction, and type-prioritized path tracing produce a deterministic inconsistent verdict with reproducible explanations.

3.2 Workflow Semantics and Constraint Templates

Action schema.

Each action type is specified by

Schema(a)=⟨R(a),W(a),Pre(a),Eff(a),Inv(a)⟩,(3)

where R(a) and W(a) are read/write sets, Pre(a) gives hard preconditions, Eff(a) defines the state update, and Inv(a) gives local type, range, unit, or object-state invariants. Execution is deterministic:

st=fat(st−1,θt)≜Apply(Eff(at),st−1,θt).(4)

Constraint-template library.

To clarify the source of post-conditions, we define

ℒ=⟨{Schema(a)}a∈𝒜,𝒯cpl,𝒯mutex,𝒯dom⟩.(5)

Schema terms provide preconditions and invariants. The template sets provide cross-step constraints: 𝒯cpl for parameter/entity bindings, 𝒯mutex for resource exclusivity or non-commutativity, and 𝒯dom for domain constraints such as repair attachment relations or CAD topology. Hence post-conditions are not an additional unexplained schema field; they are instantiated from invariants and domain templates.

For each step, constraints are instantiated as

𝒞t=𝒞tpre∪𝒞tpost,𝒞tpost=𝒞tinv∪𝒞tcpl∪𝒞tmutex∪𝒞tdom.(6)

Here 𝒞tpre is evaluated on (st−1,θt) before execution, while 𝒞tpost is checked on (st,θ≤t) after execution. Each grounded constraint is a decidable predicate

c(⋅)∈{true,false}.(7)

Definition 1 (Formal Workflow Consistency): Given ω=⟨π,s0,ℒ,Γ⟩, workflow π is formally consistent if there exists a trajectory {st}t=0T such that, for every t,

(⋀c∈𝒞tprec(st−1,θt)=true)∧st=fat(st−1,θt)∧(⋀c∈𝒞tpostc(st,θ≤t)=true).(8)

Otherwise, π is formally inconsistent. We use consistent/inconsistent throughout this paper in this formal sense.

3.3 Running Example

Consider a repair workflow

πex=⟨OpenCover(D),DisconnectBattery(B),RemoveBracket(B),LiftBattery(B)⟩.

The action LiftBattery(B) reads battery_connected(B) and bracket_removed(B), writes battery_lifted(B), and requires

¬battery_connected(B)∧bracket_removed(B).

If DisconnectBattery(B) is omitted or moved after LiftBattery(B), the verifier detects a precondition violation at the lift step. Provenance identifies the steps that produced the current battery state, slicing keeps only the relevant dependency subgraph, and the returned path explains how the missing or delayed disconnection causes the failure. If a later step refers to B′ instead of B, a coupling template instantiates B=B′, and the conflict core exposes the inconsistent binding.

3.4 Explainable State and Dependency Graph

Explainable state.

We define provenance before using it in graph construction. At each step, the verifier maintains

s~t=⟨st,provt⟩,(9)

where provt(x)⊆{1,…,t} records the steps contributing to the current value of x. Initialize prov0(x)=∅ and update

provt(x)={{t}∪⋃y∈R(at)provt−1(y),x∈W(at),provt−1(x),otherwise.(10)

Each instantiated constraint c also has a step attribution attr(c), namely the step or steps that introduce the constraint. We denote the state variables and parameter symbols in c by varsX(c) and varsΘ(c).

Typed dependency graph.

We construct G=(V,E,λ) with

V=VA∪VX∪VΘ,(11)

where VA are action nodes, VX are state-variable nodes, VΘ are parameter/binding nodes, and λ assigns edge types. The graph uses four edge families.

Data dependency. If ai is the most recent writer of x before aj reads x, add

(vai,vx),(vx,vaj)∈E,λ=data.(12)

Precondition dependency. If a precondition of aj references x, add (vx,vaj) with λ=pre. Its upstream causes are obtained from provj−1(x).

Coupling. For a binding between steps i and j, introduce vϑ∈VΘ and add two-way arcs between vϑ and the participating action nodes. The bidirectionality is for explanation traversal of symmetric equality/binding constraints; it does not imply reverse temporal causality.

Mutex/resource conflict. For a mutex or exclusive-resource template involving ai and aj, add an undirected conflict edge, stored as two directed arcs in implementation. If a domain rule is directional, such as a strict precedence relation, it is encoded as a directed dependency rather than as a mutex edge.

3.5 Verification and Conflict Tracing

Incremental verification.

Let Φt be the accumulated post-constraint store:

Φt=Φt−1∧⋀c∈𝒞tpostc(st,θ≤t),Φ0=⊤.(13)

At step t, the verifier checks 𝒞tpre, executes st=fat(st−1,θt) if all preconditions hold, updates provenance, adds post-constraints to Φt, and queries SAT(Φt). Grounded predicates are evaluated directly; symbolic formulas are checked by a decidable solver.

Slicing and core extraction.

When a failure occurs at t∗, let ℱt∗ be the failed preconditions or solver-reported failing constraints. The relevant ancestor set is

𝒰=⋃c∈ℱt∗(attr(c)∪⋃x∈varsX(c)provτ(x)),(14)

where τ=t∗−1 for precondition failures and τ=t∗ for post-constraint failures. The sliced graph is

Gt∗=G[Vt∗A∪Vt∗XΘ],(15)

where Vt∗A={vai∣i∈𝒰}∪{vat∗} and Vt∗XΘ contains adjacent variable/binding nodes appearing in the failure or core.

Within Gt∗, the verifier extracts a conflict core 𝒦. For precondition failures, 𝒦=ℱt∗. For post-constraint failures, 𝒦⊆Φt∗ is an UNSAT core when supported by the solver, or a deterministic near-minimal core obtained by deletion-based shrinking. The conflict sources are

Src=⋃c∈𝒦(attr(c)∪⋃x∈varsX(c)provτ(x)).(16)

Propagation paths.

For each i∈Src, the verifier returns a path from vai to vat∗ in Gt∗. Edge costs are fixed as

cost(e)={0,λ(e)=pre,1,λ(e)=data,2,λ(e)=cpl,3,λ(e)=mutex.(17)

The selected path is

Pi→t∗=arg⁡minP:vai⇝vat∗(∑e∈Pcost(e),len(P)),(18)

with lexicographic minimization and deterministic tie-breaking.

3.6 Full Procedure

Algorithm 1 formalizes the complete dependency-state coupled verification workflow. It takes a structured audit instance as input and returns a consistency verdict together with reproducible conflict explanations. The algorithm performs forward incremental verification: it checks preconditions before executing each step, maintains an accumulated constraint store, and terminates immediately upon detecting the first inconsistency. When a violation is found, it generates a compact explanation via dependency slicing, conflict core extraction, and propagation path tracing.

3.7 Theoretical Properties and Complexity

We state guarantees over the structured instance ω. They do not assert perfect raw parsing; they assert deterministic verification once ω is given.

Assumption 1 (Deterministic transitions): Each fa is deterministic and computable.

Assumption 2 (Decidable constraints): Each Φt belongs to a decidable constraint fragment, and the solver returns correct satisfiability results.

Assumption 3 (Deterministic instantiation): Given ω, template instantiation returns a finite deterministic set of constraints and attributions.

Theorem 1 (Soundness): If Algorithm 1 outputs consistent, then π is formally consistent by Definition 1.

Theorem 2 (Detection completeness): If π is formally inconsistent, Algorithm 1 outputs inconsistent at the first step where a precondition is violated or Φt becomes unsatisfiable.

Proposition 1 (Traceability): For any failed constraint, (10) and attr(⋅) identify a finite ancestor set; therefore the failure can be represented on Gt∗.

Let T be the number of steps, k¯ the average number of read/write variables per step, q¯ the average number of instantiated constraints per step, and |E| the number of dependency edges. Graph construction and updates cost

O(T(k¯+q¯)+|E|).(19)

Verification is dominated by incremental solving, ∑t=1TSolve(Φt). Slicing and path search are linear in the sliced graph size, O(|Et∗|). Core extraction requires one additional solver query when UNSAT cores are available; otherwise deterministic shrinking costs O(m⋅Solve) for m candidate constraints.

3.8 Domain Instantiation and Deployment Effort

The framework is domain-agnostic in form but schema-dependent in deployment. Applying it to a new dataset requires defining action types, state variables, read/write sets, preconditions, effects, invariants, coupling templates, mutex/resource templates, and the parser-to-schema mapping. This is a library-level effort; once ℒ is built, new instances are verified without hand-crafted explanations.

For physical workflows, states may encode object existence, attachments, tool status, and safety/resource conditions. For CAD workflows, states may encode parameters, units, geometric relations, topological entities, and feature dependencies. The same interface can also serve as a validator for generative or agentic systems: a model or human–AI agent proposes a workflow, the verifier checks it, and the returned core and trace provide deterministic feedback for refinement. Because schemas, templates, and dependency graphs are explicit before inference, the framework also provides an ante-hoc interpretable backbone for learned components.

4  Experiments

We evaluate the proposed dependency–state coupled auditing framework on two benchmarks, MyFixit-Audit and Fusion360-Audit. The experiments are organized to validate five key capabilities: (i) binary consistency auditing, (ii) inconsistency type recognition, (iii) error localization (step/element/relation), (iv) structural propagation tracing (Fusion360-Audit), and (v) efficiency and robustness.

4.1 Datasets

Table 1 summarizes the two datasets. MyFixit-Audit is bi-modal with text and images collected from iFixit repair manuals, while Fusion360-Audit is tri-modal with text, images, and explicit assembly structure derived from Fusion 360 CAD assemblies. Both datasets follow a 70/15/15 split and are balanced between consistent and inconsistent samples. Inconsistent samples are constructed using four perturbation families, which also define the auditing labels for inconsistency type classification.

Audit-instance construction and perturbation layer.

We distinguish raw-evidence perturbations from structured-instance perturbations. Each sample is first represented as raw or multimodal evidence, including text, images, and, for Fusion360-Audit, structural CAD information. This evidence is then mapped by the same parser/schema-mapping pipeline into a structured audit instance ω=⟨π,s0,ℒ,Γ⟩, on which the proposed verifier operates. ImageSwap is introduced at the raw-evidence level by replacing the visual evidence associated with a workflow step while keeping the corresponding procedural context fixed. EntityTextSwap and CountSpecPerturb modify textual entity mentions or numeric/specification fields and are then reflected in the parsed action parameters, entity bindings, or count/specification constraints. RelationStructSwap is applied at the structured-representation level by perturbing parsed operation relations, assembly edges, or CAD relation identifiers used by the audit instance. Therefore, the reported results evaluate a verifier operating on parsed workflows under controlled grounding and representation noise, rather than an oracle verifier with perfect symbolic inputs. This protocol separates errors caused by upstream data-to-symbol mapping from the deterministic reasoning performed by the verifier.

We report additional structural statistics used in our evaluation protocols in Table 2. Each sample is a procedural sequence of steps; Fusion360-Audit additionally contains an assembly graph.

4.2 Tasks and Metrics

We evaluate four tasks.

T1: Consistency Auditing (Binary). Given a sample with modalities I, predict y∈{Consistent,Inconsistent}. We report Accuracy and macro-F1.

T2: Inconsistency Type Classification. We perform multi-class classification over five labels: Consistent, ImageSwap, EntityTextSwap, CountSpecPerturb, and RelationStructSwap. We report macro-F1 and per-class F1.

T3: Error Localization. For inconsistent samples, we localize the corrupted source: (i) step localization, where the model predicts the corrupted step index in ranked form; we report Top-1, Top-3, Top-5, and MRR; and (ii) element localization, where the model predicts the corrupted element (swapped image id, swapped entity mention, or perturbed count-spec field); we report exact-match accuracy (ElemAcc). For Fusion360-Audit RelationStructSwap, we additionally localize the corrupted structural relation (edge) and report edge-level F1 (Rel-F1).

T4: Structural Propagation Tracing (Fusion360-Audit). For RelationStructSwap, we recover a dependency trace connecting the corrupted relation to the failure step. We define a reference trace as the type-prioritized shortest path on the assembly/dependency graph between the corrupted relation endpoints and the nearest text-referenced entities. We report trace edge-F1, normalized edit distance (NED; lower is better), and coverage, defined as the fraction of violated endpoints or variables covered by the trace.

In addition, we evaluate explanation compactness using the slice ratio |𝒰|/T, core size |𝒦|, and the average number of returned traces. For stochastic baselines, we assess determinism by running N=10 repeated evaluations with identical inputs and reporting output consistency and standard deviation.

4.3 Baselines

We compare against unimodal, multimodal fusion, LLM-based auditing, and structure-only checks.

TextOnly: RoBERTa-base encoder + MLP classifier.

ImageOnly: ViT-B/16 encoder [32] + MLP classifier.

StructOnly (Fusion360-Audit): 3-layer GraphSAGE + MLP classifier.

EarlyFuse: concatenation of modality embeddings (text+image(+graph)) + MLP.

CrossAttn: cross-attention fusion across modalities.

TriFuse (Fusion360-Audit): gated tri-modal fusion with shared latent.

CLIPMatch (MyFixit-Audit): step-level text-image similarity scoring with a threshold and swap detection via bipartite matching.

GraphOnly (Fusion360-Audit): checks structural consistency on the graph (reachability/relation constraints) without executable state transitions or satisfiability solving.

LLM-CoT: LLM grader with constrained JSON output (decision, type, step, element); base model: GPT-4o mini.

LLM-Vote: self-consistency voting with M=7 samples, aggregating decision/type/localization; base model: GPT-4o mini.

4.4 Implementation Details

Encoders and training. Unless otherwise stated, learned baselines use RoBERTa-base for text and ViT-B/16 [32] for images, while Fusion360 structure uses GraphSAGE with a hidden size of 256. We train all learned baselines with AdamW (lr=1×10−4, wd=1×10−2), a batch size of 64, and a maximum of 20 epochs, with early stopping based on validation macro-F1.

Our auditing framework. We parse each sample into a procedural step sequence. Each step is mapped to an action at(θt) with read/write sets and constraint templates (Section 3). Coupling constraints capture cross-step entity binding and count/spec consistency, while Fusion360 additionally defines relation constraints on assembly edges and mutual-exclusion rules. We maintain incremental constraint satisfiability with a per-instance timeout of 3 s. For conflict explanation, we use solver UNSAT cores with selector variables when supported; otherwise, we apply deterministic deletion-based shrinking on the sliced constraint set. Traces are extracted as type-prioritized shortest paths on the sliced dependency graph.

4.5 Main Results

Tables 3 and 4 report the main results. Overall, the proposed method improves (i) binary auditing accuracy, (ii) type discrimination under cross-modal perturbations, and (iii) localization and tracing quality, with the most significant gains on Count/Spec Perturbation and Relation/Structure Swap, where purely semantic fusion baselines are brittle. The improvements are consistent across both datasets, indicating that explicit dependency and constraint modeling generalizes beyond a single domain. In addition, the gains are not limited to accuracy: the framework provides more reliable tracing and localization, which is critical for actionable debugging.

4.6 Per-Type Performance

To analyze failure modes, Table 5 reports the per-type F1 scores for inconsistency classification (excluding the Consistent class) on both datasets, with results for MyFixit-Audit presented in the left panel and Fusion360-Audit in the right panel. The largest improvements are observed on Count/Spec Perturbation, which requires fine-grained numeric and specification consistency, and Relation/Structure Swap, which demands stronger structural reasoning capabilities.

We ablate key components to quantify their impact on tri-modal auditing and structural tracing: (i) w/o dependency graph, (ii) w/o executable state transitions (structure-only), (iii) w/o coupling constraints, (iv) w/o mutex/structure constraints, (v) w/o provenance, (vi) w/o slicing, and (vii) w/o UNSAT core (naive first-failure attribution). Table 6 presents the complete ablation results on Fusion360-Audit. The dependency graph and executable state transitions are the most critical components, with their removal causing the largest performance drops across all tasks. Dependency slicing and UNSAT core extraction are essential for generating compact explanations, as their removal significantly increases both the slice ratio and core size. All other components contribute measurable improvements to classification and reasoning accuracy.

4.7 Long-Range Dependency Stress Test

We stress-test long-range propagation on Fusion360-Audit by stratifying Relation/Structure Swap samples using the structural distance d between the corrupted relation and the nearest entity mentioned in text, measured on the assembly graph. Fig. 2 shows that performance degrades as d increases for all methods: Fig. 2a demonstrates the drop in Top-1 localization accuracy, while Fig. 2b illustrates the decline in trace edge-F1. Despite this trend, the proposed verifier exhibits a notably flatter degradation curve compared to other baselines, maintaining substantially higher localization and tracing quality due to provenance-guided slicing and graph-grounded tracing.

Figure 2: Long-range stress test on Fusion360-Audit. Performance degradation across different structural distance bins (d).

This trend should not be interpreted as a violation of the formal guarantee under the assumption of oracle structured inputs. Larger structural distances increase the number of grounded entities, intermediate dependencies, and candidate propagation paths. As a result, localization and trace matching become more sensitive to upstream grounding noise and to ambiguity in the benchmark reference trace, especially when multiple graph paths or conflict sources are logically plausible. Thus, the degradation reflects the difficulty of empirical localization and reference-trace matching in parsed multimodal data, not a loss of deterministic formal consistency checking once the structured audit instance is fixed.

4.8 Efficiency and Scalability

We measure the end-to-end auditing time per sample and provide a breakdown into three components: (i) incremental solving, (ii) dependency slicing, and (iii) core extraction plus path search. Table 7 presents the complete runtime statistics, with the median per-sample runtime breakdown shown in the left panel and the scalability analysis grouped by procedure length T in the right panel. Incremental maintenance substantially reduces computational cost compared with re-solving from scratch, and the generated explanations remain compact (slice ratio ≈0.23 and core size ≈6–7) even for longer procedures.

4.9 Robustness to Upstream Noise

Although our focus is auditing rather than perception, upstream extraction may introduce noise. We simulate (i) step insertion/deletion, (ii) local step reordering within a window of size 3, and (iii) entity/parameter perturbations, with noise rate η∈{0,5,10,20}%. Table 8 shows that the proposed verifier degrades gracefully, maintaining strong formal consistency auditing and localization under moderate noise.

4.10 Determinism

Table 9 reports output consistency across repeated runs with identical inputs. LLM-based methods show non-zero variance in both accuracy and localization, while our verifier achieves perfect consistency (zero standard deviation) due to its fully deterministic execution and explanation pipeline.

5  Conclusion

We presented a verification-centric framework for deterministic workflow auditing that couples typed dependency graphs with executable state transitions and uses slicing and conflict-core extraction to yield reproducible explanations. Across MyFixit-Audit and Fusion360-Audit, the approach delivers strong auditing accuracy and precise localization while maintaining compact explanations and low runtime, supporting practical debugging in multimodal procedural settings. Key contributions include (i) a dependency–state coupled verifier that enforces executability under constraints, (ii) provenance-guided slicing with UNSAT core based conflict identification, and (iii) deterministic, traceable explanations for long-range error propagation. Limitations include reliance on accurate upstream parsing and fixed action semantics, and the current focus on deterministic procedural workflows. We also find that compact conflict cores and graph-grounded traces make errors easier to interpret without sacrificing audit accuracy. These properties make the system a practical drop-in auditor for large-scale procedural datasets where reproducibility is critical. Future work will extend to richer stochastic settings, improve robustness to perception noise, and integrate learned parsers with formal guarantees.

Acknowledgement: Not applicable.

Funding Statement: The authors received no specific funding for this study.

Author Contributions: The authors confirm contribution to the paper as follows: Conceptualization, Xingxin Li; methodology, Jixin Xu, Xingxin Li; software, Jixin Xu; validation, Jixin Xu; formal analysis, Senlin Zhu; investigation, Qingqing Song; resources, Xingxin Li; data curation, Senlin Zhu; writing—original draft preparation, Jixin Xu; writing—review and editing, Qingqing Song, Jixin Xu; visualization, Jixin Xu; supervision, Xingxin Li; project administration, Xingxin Li; funding acquisition, Xingxin Li. All authors reviewed and approved the final version of the manuscript.

Availability of Data and Materials: The source code, schema/template definitions, perturbation scripts, split files, configuration files, and evaluation scripts will be released in an anonymized repository upon acceptance. Due to licensing restrictions of the original repair manuals and CAD assets, raw data may not be fully redistributed; however, processed annotations, split identifiers, and scripts for reproducing all reported tables will be provided.

Ethics Approval: Not applicable.

Conflicts of Interest: The authors declare no conflicts of interest.

References

1. Dalvi B, Huang L, Tandon N, Yih WT, Clark P. Tracking state changes in procedural text: a challenge dataset and models for process paragraph comprehension. In: Proceedings of the 2018 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies. Stroudsburg, PA, USA: ACL; 2018. p. 1595–604. doi:10.18653/v1/N18-1144. [Google Scholar] [CrossRef]

2. Zhukov D, Alayrac JB, Cinbis RG, Fouhey D, Laptev I, Sivic J. Cross-task weakly supervised learning from instructional videos. In: Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR). Piscataway, NJ, USA: IEEE; 2019. p. 3537–45. doi:10.1109/CVPR.2019.00365. [Google Scholar] [CrossRef]

3. Shridhar M, Thomason J, Gordon D, Bisk Y, Han W, Mottaghi R, et al. ALFRED: a benchmark for interpreting grounded instructions for everyday tasks. In: Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR). Piscataway, NJ, USA: IEEE; 2020. p. 10740–9. doi:10.1109/CVPR42600.2020.01075. [Google Scholar] [CrossRef]

4. Seff A, Ovadia Y, Zhou W, Adams RP. SketchGraphs: a large-scale dataset for modeling relational geometry in computer-aided design. arXiv:2007.08506. 2020. [Google Scholar]

5. Willis KDD, Pu Y, Luo J, Chu H, Du T, Lambourne JG, et al. Fusion 360 gallery: a dataset and environment for programmatic CAD construction from human design sequences. ACM Trans Graph. 2021;40(4):54. doi:10.1145/3450626.3459818. [Google Scholar] [CrossRef]

6. Wei J, Wang X, Schuurmans D, Bosma M, Ichter B, Xia F, et al. Chain-of-thought prompting elicits reasoning in large language models. arXiv:2201.11903. 2022. [Google Scholar]

7. Wang X, Wei J, Schuurmans D, Le QV, Chi EH, Narang S, et al. Self-consistency improves chain of thought reasoning in language models. arXiv:2203.11171. 2023. [Google Scholar]

8. Madaan A, Tandon N, Gupta P, Hallinan S, Gao L, Wiegreffe S, et al. Self-Refine: iterative refinement with self-feedback. arXiv:2303.17651. 2023. [Google Scholar]

9. van der Aalst WMP. Process mining: data science in action. 2nd ed. Berlin/Heidelberg, Germany: Springer; 2016. doi:10.1007/978-3-662-49851-4. [Google Scholar] [CrossRef]

10. Rozinat A, van der Aalst WMP. Conformance checking of processes based on monitoring real behavior. Inf Syst. 2008;33(1):64–95. doi:10.1016/j.is.2007.07.001. [Google Scholar] [CrossRef]

11. Adriansyah A, van Dongen BF, van der Aalst WMP. Conformance checking using cost-based fitness analysis. In: Proceedings of the 15th IEEE International Enterprise Distributed Object Computing Conference (EDOC 2011). Piscataway, NJ, USA: IEEE; 2011. p. 55–64. doi:10.1109/EDOC.2011.12. [Google Scholar] [CrossRef]

12. Percassi F, Scala E, Vallati M. The power of reformulation: from validation to planning in PDDL+. Proc Int Conf Autom Plan Sched. 2022;32:288–96. doi:10.1609/icaps.v32i1.19812. [Google Scholar] [CrossRef]

13. de Moura L, Bjørner N. Z3: an efficient SMT solver. In: Tools and algorithms for the construction and analysis of systems (TACAS 2008). Berlin/Heidelberg, Germany: Springer; 2008. p. 337–40. doi:10.1007/978-3-540-78800-3_24. [Google Scholar] [CrossRef]

14. Ding ZJ, Li S, Chen C, He C. Program dependence net and on-demand slicing for property verification of concurrent system and software. J Syst Softw. 2025;219(2):112221. doi:10.1016/j.jss.2024.112221. [Google Scholar] [CrossRef]

15. Agrawal H, Horgan JR. Dynamic program slicing. In: Proceedings of the ACM SIGPLAN 1990 Conference on Programming Language Design and Implementation (PLDI). New York, NY, USA: ACM; 1990. p. 246–56. doi:10.1145/93542.93576. [Google Scholar] [CrossRef]

16. Buneman P, Khanna S, Tan WC. Why and where: a characterization of data provenance. In: Van den Bussche J, Vianu V, editors. Database theory—ICDT 2001. Berlin/Heidelberg, Germany: Springer; 2001. p. 316–30. doi:10.1007/3-540-44503-X_20. [Google Scholar] [CrossRef]

17. Green TJ, Karvounarakis G, Tannen V. Provenance semirings. In: Proceedings of the 26th ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS). New York, NY, USA: ACM; 2007. p. 31–40. doi:10.1145/1265530.1265535. [Google Scholar] [CrossRef]

18. Reiter R. A theory of diagnosis from first principles. Artif Intell. 1987;32(1):57–95. doi:10.1016/0004-3702(87)90062-2. [Google Scholar] [CrossRef]

19. Liffiton MH, Sakallah KA. Algorithms for computing minimal unsatisfiable subsets of constraints. J Autom Reason. 2008;40(1):1–33. doi:10.1007/s10817-007-9084-z. [Google Scholar] [CrossRef]

20. Murata T. Petri nets: properties, analysis and applications. Proc IEEE. 1989;77(4):541–80. doi:10.1109/5.24143. [Google Scholar] [CrossRef]

21. Gocht S, Balyo T. Accelerating SAT based planning with incremental SAT solving. In: Proceedings of the Twenty-Seventh International Conference on Automated Planning and Scheduling (ICAPS 2017). Palo Alto, CA, USA: AAAI Press; 2017. p. 135–9. doi:10.1609/icaps.v27i1.13798. [Google Scholar] [CrossRef]

22. Sülflow A, Fey G, Bloem R, Drechsler R. Debugging design errors by using unsatisfiable cores. In: 11th ITG/GMM/GI-Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV). Aachen, Germany: Shaker Verlag; 2008. p. 159–68. doi:10.1142/S0129054107004942. [Google Scholar] [CrossRef]

23. Miech A, Zhukov D, Alayrac JB, Tapaswi M, Laptev I, Sivic J. HowTo100M: learning a text-video embedding by watching hundred million narrated video clips. In: 2019 IEEE/CVF International Conference on Computer Vision (ICCV). Piscataway, NJ, USA: IEEE; 2019. p. 2630–40. doi:10.1109/ICCV.2019.00272. [Google Scholar] [CrossRef]

24. Nabizadeh N, Kolossa D, Heckmann M. MyFixit: an annotated dataset, annotation tool, and baseline methods for information extraction from repair manuals. In: Proceedings of the Twelfth Language Resources and Evaluation Conference (LREC). Marseille, France: ELRA; 2020. p. 2120–8. [Google Scholar]

25. Willis KDD, Jayaraman PK, Chu H, Tian Y, Li Y, Grandi D, et al. JoinABLe: learning bottom-up assembly of parametric CAD joints. In: Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR). Piscataway, NJ, USA: IEEE; 2022. p. 15828–39. [Google Scholar]

26. Bettig B, Hoffmann CM. Geometric constraint solving in parametric computer-aided design. J Comput Inf Sci Eng. 2011;11(2):021001. doi:10.1115/1.3593408. [Google Scholar] [CrossRef]

27. Geng S, Cooper H, Moskal M, Jenkins S, Berman J, Ranchin N, et al. Generating structured outputs from language models: benchmark and studies. arXiv:2501.10868. 2025. [Google Scholar]

28. Vaswani A, Shazeer N, Parmar N, Uszkoreit J, Jones L, Gomez AN, et al. Attention is all you need. In: Advances in Neural Information Processing Systems 30 (NIPS 2017). Red Hook, NY, USA: Curran Associates, Inc.; 2017. p. 5998–6008. [Google Scholar]

29. Liu Y, Ott M, Goyal N, Du J, Joshi M, Chen D, et al. RoBERTa: a robustly optimized BERT pretraining approach. arXiv:1907.11692. 2019. [Google Scholar]

30. Hamilton WL, Ying R, Leskovec J. Inductive representation learning on large graphs. In: Advances in Neural Information Processing Systems 30 (NeurIPS 2017). Red Hook, NY, USA: Curran Associates, Inc.; 2017. p. 1024–34. [Google Scholar]

31. Radford A, Kim JW, Hallacy C, Ramesh A, Goh G, Agarwal S, et al. Learning transferable visual models from natural language supervision. In: Proceedings of the 38th International Conference on Machine Learning. Proceedings of Machine Learning Research. Cambridge, MA, USA: PMLR; 2021. p. 8748–63. [Google Scholar]

32. Dosovitskiy A, Beyer L, Kolesnikov A, Weissenborn D, Zhai X, Unterthiner T, et al. An image is worth 16x16 words: transformers for image recognition at scale. arXiv:2010.11929. 2021. [Google Scholar]