Search arXiv⌕ Search

arXiv · 2610.27971

Execution-Time Validation of Context-Carrying Action Intents in Industrial Cyber-Physical Systems

Abstract

In industrial cells, commands from learned policies, operators and schedulers reach the controller after inference, confirmation and transport, and the plant may have changed meanwhile, for instance by an operator pause. Such a command is released, or takes effect, when it is no longer correct. We call this the execution gap and ask which component should make the last check, and against which version of which state. The Action Intent Schema (AIS) is a contract in which a producer states how long its decision stays valid and what it assumes. The runtime XAIR rechecks each intent before release, can commit its authorization atomically in the context store, and can release it as a version-conditional command, which the controller executes only if its version of the state is unchanged. In controlled ablations with declared ground truth on emulated and physical cells, OpenPLC and ARM and RISC-V boards, a check on a replica always left an unprotected interval: a pause written from a few to over 100ms after submission escaped it. Only a check in the scan of a software controller, either a controller-local interlock or the version-conditional command, closed the interval for the state that controller owns; only the version-conditional command also refused commands after a pause that had been undone. A global version revoked up to every valid command under unrelated updates. Versions scoped to what the intent reads, or to the truth of its predicates, did not; with continuous signals on the variables the intent reads, only the latter avoided false revocations, though it burdens the store as predicates accumulate. On one embedded-board core, XAIR validated 148-168 intents/s.

Explore related subjects

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Luca D'Agati, Giuseppe Tricomi, Fabio Orazio Mirto, Giovanni Merlino. 2026-10-20. Execution-Time Validation of Context-Carrying Action Intents in Industrial Cyber-Physical Systems. https://arxiv.org/abs/2610.27971

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

Operon: Incremental Construction of Ragged Data via Named Dimensions

Modern data processing workflows frequently encounter ragged data: multidimensional collections whose inner lengths vary and are revealed only at runtime. Ragged data is prevalent in domains throughout science and computing, yet existing workflow engines treat it as nested containers. This representation leaves shape semantics ambiguous, obscures task dependencies when upstream coordinates are not yet enumerated, and imposes coarse synchronization barriers that stall independent work across tasks. We argue that ragged data is fundamentally a flat function over a coordinate space, and that making this view explicit resolves all three difficulties at once. We realize this insight in Operon, a statically verifiable workflow engine built around a formalism of named dimensions with explicit dependency relations. Users declare pipelines in the Operon DSL by annotating data flow with dimension names, where the static checker verifies that every task does not include faulty iterations regardless of runtime lengths. At runtime, the system models in-progress arrays as partial functions over downward-closed coordinate domains, which provides a natural representation for partially-unknown data states, an exact notion of per-task indegree before all upstream coordinates are enumerated, and a sound basis for fault recovery without programmer intervention.

cs.PL↗

Multiobjective Preexpectation Reasoning for Probabilistic Programs

Probabilistic programs with nondeterminism model planning problems in which a strategy typically resolves the nondeterminism to meet a specification. We study the multiobjective setting, meeting several specifications at once along a Pareto front, and provide a deductive, program-level account of strategy synthesis. Its core is a multiobjective preexpectation transformer mapping a tuple of postexpectations to the set of simultaneously achievable values, an element of the convex Hoare powerdomain. It conservatively extends weakest preexpectations and lifts standard loop rules. We develop rules to synthesize witnessing strategies as mixed determinizations that solve nondeterminism probabilistically. We prove the transformer and synthesis rules sound against an operational Markov decision process (MDP) semantics, without requiring a finite state space: our approach can be seen as a symbolic approach - at program level - for multiobjective optimization over infinite MDPs. We demonstrate our machinery using two case studies.

cs.PL↗

Foundational Refinement Proofs for EVM Bytecode, at the Price of Tokens

Relating executable code to a high-level model of its behavior has been a central concern of programming-language research for decades. Formally verified compilers, translation validators and certifying compilers address this problem through different trade-offs between proof effort, automation, generality, and the size of the trusted base. Recently, large language models (LLMs) have begun to change the economics of formal verification. Agentic proof development is now capable of producing machine-checked proofs, sometimes unsupervised, at a scale and speed that were previously out of reach. We propose a verification architecture that takes advantage of this shift. An executable obtains a machine-checked proof that it behaves according to a high-level model, independently of the compiler that produced it. The proof is written by an LLM agent. We evaluate the feasibility of this architecture for the Ethereum Virtual Machine (EVM). We build EquiVM, a foundational framework in Lean comprising an executable EVM semantics and a formal specification language, Stele, that gives a high-level authoritative model of the bytecode's behavior, but commits to no source language or compilation toolchain. We state what it means for EVM bytecode to refine a Stele spec and we build a proof library to facilitate proof construction. We evaluate the capabilities of frontier LLMs to construct such proofs, as well as the cost of proof production and repair. Our results show that agents prove 35 real production contracts end to end, without modifying their source or bytecode, among them core contracts of Safe, Morpho, Compound and Uniswap protocols, with bytecode of size close to the maximum the EVM allows. Several proofs need only the initial prompt, the rest a handful of human inputs, and existing proofs are repaired in a fraction of the original time when the source or the compiler configuration changes.

cs.PL↗