Vision-Based Runtime Monitoring under Varying Specifications using Semantic Latent Representations

# Vision-Based Runtime Monitoring under Varying Specifications using Semantic Latent Representations
Source: [https://arxiv.org/html/2605.13923](https://arxiv.org/html/2605.13923)
Bardh Hoxha1, Oliver Schön2, Hideki Okamoto1, Lars Lindemann2, Georgios Fainekos11B\. Hoxha, H\. Okamoto, and G\. Fainekos are with Toyota NA R&D2Oliver Schön and Lars Lindemann are with ETH Zürich

###### Abstract

We study certified runtime monitoring of past\-time signal temporal logic \(ptSTL\) from visual observations under partial observability\. The monitor must infer safety\-relevant quantities from images and provide finite\-sample guarantees, while being*reusable*: once trained and calibrated, it should certify any formula in a target fragment without per\-formula retraining\. For fragments induced by a finite dictionary of temporal atoms, we prove that the*semantic basis*, the vector of atom robustness scores, is the minimum prediction target within the class of monotone, 1\-Lipschitz reusable interfaces: any formula is evaluated by a deterministic decoder derived from the parse tree, and a single conformal calibration pass certifies the entire fragment with no union bound\. We also introduce a*rolling prediction monitor*that predicts only current predicate values and reconstructs temporal history online; this is easier to learn but grows conservative at long horizons\. On a pedestrian\-crossroad benchmark, rolling achieves tighter certified bounds at short horizons while the semantic\-basis monitor is up to 4\-times tighter at long horizons\. We validate the presented monitors on real\-world Waymo driving data, where both monitors satisfy the conformal coverage guarantee empirically\.

## IINTRODUCTION

Runtime monitors provide a mechanism for assessing whether specified safety conditions are satisfied during deployment of autonomous systems\. In practice, these conditions are often not fixed once and for all: different missions may require different safety and performance specifications, and operators may update the specifications used at deployment\. Accordingly, a practical runtime monitor should be*reusable*\(see Fig\.[1](https://arxiv.org/html/2605.13923#S1.F1)\): after training and calibration, it should support certification for a range of specifications in a target fragment without requiring retraining for each new specification\. This motivates a*semantic interface*between observations and specifications: a pre\-trained encoder produces a fixed intermediate representation, and formula\-specific values are then computed at query time by a deterministic, analytically derived decoder, without additional learning\.

Partial observability introduces an additional challenge\. The monitor has access only to visual observations, while safety predicates are defined over latent physical quantities \(e\.g\., distances, velocities, and clearances\) but the monitor observes only images\. Safety\-relevant quantities must therefore be inferred from pixels, and the resulting prediction uncertainty must be accounted for in the certificate\. This paper combines the problems of reusable specification monitoring and certified learning under partial observability\.

A formula\-specific certified baseline is to predict the satisfaction measure of a fixed formula and apply conformal prediction to obtain a certified lower bound\[[1](https://arxiv.org/html/2605.13923#bib.bib1)\]\. This works, but offers no reuse: when the specification changes, both the predictor and the calibration are tied to that formula\. To avoid this limitation, the monitor must predict areusableintermediate representation\. The choice of representation determines the scope of reuse, the difficulty of visual prediction, and the tightness of the resulting conformal bounds\.

![Refer to caption](https://arxiv.org/html/2605.13923v1/multi_spec_monitor_idea.pdf)![Refer to caption](https://arxiv.org/html/2605.13923v1/multi_spec_monitor_idea.pdf)encθ\\operatorname\{enc\}\_\{\\theta\}
![Refer to caption](https://arxiv.org/html/2605.13923v1/multi_spec_monitor_idea.pdf)decφ1\\operatorname\{dec\}\_\{\\varphi\_\{1\}\}
![Refer to caption](https://arxiv.org/html/2605.13923v1/multi_spec_monitor_idea.pdf)decφ2\\operatorname\{dec\}\_\{\\varphi\_\{2\}\}
ρ​\(φ1,x,t\)\\rho\(\\varphi\_\{1\},x,t\)
A: Predicate\-Window History

ρ​\(φ2,x,t\)\\rho\(\\varphi\_\{2\},x,t\)
![Refer to caption](https://arxiv.org/html/2605.13923v1/multi_spec_monitor_idea.pdf)Formula\-SpecificDecoders![Refer to caption](https://arxiv.org/html/2605.13923v1/multi_spec_monitor_idea.pdf)μ1,t−K​⋯​μ1,t\\small\\mu\_\{1,t\-K\}\\,\\cdots\\,\\mu\_\{1,t\}
μm,t−K​⋯​μm,t\\small\\mu\_\{m,t\-K\}\\cdots\\mu\_\{m,t\}
ℬt𝒫=\\small\{\\mathcal\{B\}\}\_\{t\}^\{\\mathcal\{P\}\}=
![Refer to caption](https://arxiv.org/html/2605.13923v1/multi_spec_monitor_idea.pdf)ℬt𝒫=\\small\{\\mathcal\{B\}\}\_\{t\}^\{\\mathcal\{P\}\}=
Figure 1:*Left:*A single trained encoderencθ\\operatorname\{enc\}\_\{\\theta\}maps vision inputs to a latent interfaceℬt\{\\mathcal\{B\}\}\_\{t\}from which formula\-specific decoders evaluate any formulaφ∈ℱ\\varphi\\in\\mathcal\{F\}in a target fragmentℱ\\mathcal\{F\}\.*Right:*Two choices of interface basis\.We investigate two reusable monitoring interfaces\. The first predicts all safety\-relevant quantities at each timestep within the specification’s look\-back window\. This is maximally flexible, since any temporal property can be evaluated from it, but the encoder must regress a high\-dimensional output whose size grows with window length\. For a specification fragment over a fixed set of temporal operators such as “always safe over the lastKKsteps” or “eventually reach the goal withinKKsteps”, we prove that a strictly smaller representation, the*semantic basis*, suffices to evaluate every specification in the family, and that no smaller representation can\.

We use*conformal prediction*\(CP\)\[[1](https://arxiv.org/html/2605.13923#bib.bib1),[2](https://arxiv.org/html/2605.13923#bib.bib2),[3](https://arxiv.org/html/2605.13923#bib.bib3)\]to convert prediction residuals into certified lower bounds, and show that the tightness of these bounds depends critically on whether calibration is applied before or after temporal aggregation in the decoder\.

Contributions:

1. 1\.*Semantic basis as a reusable interface \(Section[IV](https://arxiv.org/html/2605.13923#S4)\):*For any ptSTL fragment induced by a finite atomic dictionary, we prove that the semantic basis is minimal within the class of monotone,11\-Lipschitz reusable interfaces\.
2. 2\.*Compositional conformal certification \(Section[V](https://arxiv.org/html/2605.13923#S5)\):*Because every formula is decoded by a monotone, 1\-Lipschitz function, single atom\-wise conformal bounds certify the entire fragment simultaneously \(Thm\.[2](https://arxiv.org/html/2605.13923#Thmtheorem2)\)\.
3. 3\.*Rolling prediction monitor:*We introduce a rolling prediction monitor that updates the predicate basis online\. This reduces the encoder dimension substantially, making the learning problem substantially easier\. We provide empirical evidence that this results in higher prediction accuracy and tighter conformal bounds at short horizons\.

## IIRELATED WORK

Signal temporal logic \(STL\) provides a framework for specifying and evaluating temporal properties of continuous\-valued signals, with robustness semantics quantifying distance from violation\[[4](https://arxiv.org/html/2605.13923#bib.bib4),[5](https://arxiv.org/html/2605.13923#bib.bib5)\]\. Efficient online monitoring algorithms for past\-time STL are well established\[[6](https://arxiv.org/html/2605.13923#bib.bib6),[7](https://arxiv.org/html/2605.13923#bib.bib7)\]\. We build on these semantics while addressing partial observability through learned vision models\.

Conformal prediction \(CP\) has been used in STL monitoring to provide finite\-sample coverage guarantees\[[1](https://arxiv.org/html/2605.13923#bib.bib1),[2](https://arxiv.org/html/2605.13923#bib.bib2),[3](https://arxiv.org/html/2605.13923#bib.bib3)\]\. Beyond monitoring, CP has also been used in safe planning and prediction\[[8](https://arxiv.org/html/2605.13923#bib.bib8),[9](https://arxiv.org/html/2605.13923#bib.bib9)\]; unlike these works, we study reusable fragment\-wide certification from a single calibration pass\.

Neural monitoring under partial observability has been studied for fixed properties and small template families\[[10](https://arxiv.org/html/2605.13923#bib.bib10),[11](https://arxiv.org/html/2605.13923#bib.bib11)\]\. We extend this setting to certify an entire∧⁣/⁣∨\\wedge/\\vee\-closed fragment from a single predictor and characterize the minimal interface required to do so\.

Compositional uncertainty\-aware STL semantics have been studied under partial and uncertain observations\. Robust satisfaction intervals for partial traces were introduced in\[[5](https://arxiv.org/html/2605.13923#bib.bib5)\]; interval\-valued semantics that propagate uncertainty through STL operators were developed in\[[12](https://arxiv.org/html/2605.13923#bib.bib12),[13](https://arxiv.org/html/2605.13923#bib.bib13)\]; and a related setting based on affine arithmetic and SMT is studied in\[[14](https://arxiv.org/html/2605.13923#bib.bib14)\]\. Our rolling and semantic\-basis monitors build on this compositional viewpoint, adding a minimality result for the prediction target and an explicit calibration tradeoff analysis\. In\[[15](https://arxiv.org/html/2605.13923#bib.bib15),[16](https://arxiv.org/html/2605.13923#bib.bib16)\], the papers present monitoring for perception systems, but do not provide finite\-sample certified ptSTL robustness bounds from learned latent visual representations\.

*Predictive state representations*\(PSRs\) construct minimal sufficient statistics for partially observable systems\[[17](https://arxiv.org/html/2605.13923#bib.bib17),[18](https://arxiv.org/html/2605.13923#bib.bib18)\]: a linear PSR identifies the minimum\-rank basis from which any observable test can be linearly decoded, without modeling a latent belief state explicitly\. More recently, temporal logic specifications have been embedded directly into latent spaces via*embedding temporal logic*\(ETL\), with satisfaction checked through learned distance thresholds, but without certified coverage bounds\[[19](https://arxiv.org/html/2605.13923#bib.bib19)\]\. Concept embedding models extend latent representations to probabilistic concept membership for concurrent concept reasoning, also without formal guarantees\[[20](https://arxiv.org/html/2605.13923#bib.bib20)\]\. Our semantic basis is the ptSTL\-monitoring analogue of a PSR: the minimum statistic for which monotone, 1\-Lipschitz decoders suffice over all signals, and it is precisely this Lipschitz restriction that enables the conformal certification in Section[V](https://arxiv.org/html/2605.13923#S5)\.

Adaptive conformal methods offer orthogonal improvements to trajectory\-level tightness under distribution shift; integrating them with our compositional certification structure is a possible direction for future work\[[21](https://arxiv.org/html/2605.13923#bib.bib21)\]\.

## IIIPROBLEM FORMULATION

### III\-ADynamical System and Observations

We consider discrete\-time dynamical systems with a statext∈𝕏⊂ℝdxx\_\{t\}\\in\\mathbb\{X\}\\subset\\mathbb\{R\}^\{d\_\{x\}\}evolving as

xt\+1\\displaystyle x\_\{t\+1\}=fX​\(xt,ut,vt\),ot=fO​\(xt,wt\),\\displaystyle=f\_\{X\}\(x\_\{t\},u\_\{t\},v\_\{t\}\),\\qquad o\_\{t\}=f\_\{O\}\(x\_\{t\},w\_\{t\}\),\(1\)whereut∈ℝduu\_\{t\}\\in\\mathbb\{R\}^\{d\_\{u\}\}is a control input andvt,wtv\_\{t\},w\_\{t\}are noise terms\. At each timet∈ℤ≥0t\\in\\mathbb\{Z\}\_\{\\geq 0\}, the state generates an observationot∈𝕆⊂ℝdoo\_\{t\}\\in\\mathbb\{O\}\\subset\\mathbb\{R\}^\{d\_\{o\}\}; e\.g\.,oto\_\{t\}may be overhead camera images subject to different sensor nuisance\. In this paper, the monitor has access only to the observation sequence\{oτ\}τ≤t\\\{o\_\{\\tau\}\\\}\_\{\\tau\\leq t\}; the statextx\_\{t\}is never directly observed\.

### III\-BTemporal Logic Specifications

Let𝒫=\{μ1,…,μm\}\\mathcal\{P\}=\\\{\\mu\_\{1\},\\dots,\\mu\_\{m\}\\\}be a finite set of*atomic predicates*over signalsx:ℤ≥0→𝕏\{x\}\\colon\\mathbb\{Z\}\_\{\\geq 0\}\\to\\mathbb\{X\}, where eachμk:𝕏×ℤ≥0→\{⊤,⊥\}\\mu\_\{k\}\\colon\\mathbb\{X\}\\times\\mathbb\{Z\}\_\{\\geq 0\}\\to\\\{\\top,\\bot\\\}is defined by a scalar predicate functionhk:𝕏→ℝh\_\{k\}\\colon\\mathbb\{X\}\\to\\mathbb\{R\}via

\(μk​\(x,t\)=⊤\)⇔hk​\(xt\)≥0\.\\big\(\\mu\_\{k\}\(x,t\)=\\top\\big\)\\Leftrightarrow h\_\{k\}\(x\_\{t\}\)\\geq 0\.We writeρ​\(μk,x,t\):=hk​\(xt\)\\rho\(\\mu\_\{k\},\{x\},t\):=h\_\{k\}\(x\_\{t\}\)for the*robustness*ofμk\\mu\_\{k\}\.

###### Definition 1\(ptSTL syntax and quantitative semantics\)\.

*Past\-time STL*\(ptSTL\)\[[22](https://arxiv.org/html/2605.13923#bib.bib22)\]formulas over predicates𝒫\\mathcal\{P\}in*positive normal form*\(PNF\) are given by the grammar

φ::=μk∣φ1∧φ2∣φ1∨φ2∣⊡\[a,b\]φ∣⟐\[a,b\]φ,\\displaystyle\\varphi::=\\mu\_\{k\}\\mid\\varphi\_\{1\}\\wedge\\varphi\_\{2\}\\mid\\varphi\_\{1\}\\vee\\varphi\_\{2\}\\mid\\boxdot\_\{\[a,b\]\}\\,\\varphi\\mid\\Diamonddot\_\{\[a,b\]\}\\,\\varphi,whereμk∈𝒫\\mu\_\{k\}\\in\\mathcal\{P\},φ1,φ2\\varphi\_\{1\},\\varphi\_\{2\}are ptSTL formulas, and\[a,b\]⊆ℤ≥0\[a,b\]\\subseteq\\mathbb\{Z\}\_\{\\geq 0\}\. The*robustness*ρ​\(φ,x,t\)∈ℝ\\rho\(\\varphi,\{x\},t\)\\in\\mathbb\{R\}is defined recursively over a signalx:ℤ≥0→𝕏\{x\}\\colon\\mathbb\{Z\}\_\{\\geq 0\}\\to\\mathbb\{X\}at timet∈ℤ≥0t\\in\\mathbb\{Z\}\_\{\\geq 0\}as:

ρ​\(μk,x,t\)\\displaystyle\\rho\(\\mu\_\{k\},x,t\)=hk​\(xt\),\\displaystyle=h\_\{k\}\(x\_\{t\}\),ρ​\(φ1∧φ2,x,t\)\\displaystyle\\rho\(\\varphi\_\{1\}\\wedge\\varphi\_\{2\},\{x\},t\)=min⁡\{ρ​\(φ1,x,t\),ρ​\(φ2,x,t\)\},\\displaystyle=\\min\\big\\\{\\rho\(\\varphi\_\{1\},\{x\},t\),\\,\\rho\(\\varphi\_\{2\},\{x\},t\)\\big\\\},ρ​\(φ1∨φ2,x,t\)\\displaystyle\\rho\(\\varphi\_\{1\}\\vee\\varphi\_\{2\},\{x\},t\)=max⁡\{ρ​\(φ1,x,t\),ρ​\(φ2,x,t\)\},\\displaystyle=\\max\\big\\\{\\rho\(\\varphi\_\{1\},\{x\},t\),\\,\\rho\(\\varphi\_\{2\},\{x\},t\)\\big\\\},ρ\(⊡\[a,b\]φ,x,t\)\\displaystyle\\rho\(\\boxdot\_\{\[a,b\]\}\\varphi,\{x\},t\)=inft′∈\[t−b,t−a\]ρ​\(φ,x,t′\),\\displaystyle=\\inf\_\{t^\{\\prime\}\\in\[t\-b,t\-a\]\}\\rho\(\\varphi,\{x\},t^\{\\prime\}\),ρ​\(⟐\[a,b\]​φ,x,t\)\\displaystyle\\rho\(\\Diamonddot\_\{\[a,b\]\}\\varphi,\{x\},t\)=supt′∈\[t−b,t−a\]ρ​\(φ,x,t′\)\.\\displaystyle=\\sup\_\{t^\{\\prime\}\\in\[t\-b,t\-a\]\}\\rho\(\\varphi,\{x\},t^\{\\prime\}\)\.A signalx\{x\}satisfies a formulaφ\\varphiat timettiffρ​\(φ,x,t\)≥0\\rho\(\\varphi,\{x\},t\)\\geq 0\.

We define the*formula horizon*hor​\(φ\)∈ℕ\\mathrm\{hor\}\(\\varphi\)\\in\\mathbb\{N\}as the largest backward time lag needed to evaluateφ\\varphiat timett, so thatρ​\(φ,x,t\)\\rho\(\\varphi,\{x\},t\)depends only onxt−hor​\(φ\):t∈ℝdx×\(hor​\(φ\)\+1\)\{x\}\_\{t\-\\mathrm\{hor\}\(\\varphi\):t\}\\in\\mathbb\{R\}^\{d\_\{x\}\\times\(\\mathrm\{hor\}\(\\varphi\)\+1\)\}\.

### III\-CInduced Specification Fragments

We now define the class of specifications addressed in this paper\. The key idea is to fix a finite dictionary of*temporal atoms*, namely base ptSTL formulas that serve as irreducible generators, and close it under conjunction and disjunction \(see Fig\.[2](https://arxiv.org/html/2605.13923#S3.F2)\)\. The result is a fragment of ptSTL with a rich algebraic structure that admits tight compositional conformal certification via the semantic basis introduced in Section[IV](https://arxiv.org/html/2605.13923#S4)\.

μ1\\mu\_\{1\}μ2\\mu\_\{2\}μk\\mu\_\{k\}μm\\mu\_\{m\}⋯\\cdotsPredicates𝒫\\mathcal\{P\}:⊡Iμ1\\boxdot\_\{I\}\\mu\_\{1\}⟐I​μ1\\Diamonddot\_\{I\}\\mu\_\{1\}⊡I′μk\\boxdot\_\{I^\{\\prime\}\}\\\!\\mu\_\{k\}⋯\\cdotsTemporal atoms𝒜\\mathcal\{A\}:a1∧a2a\_\{1\}\\wedge a\_\{2\}a2∨a3a\_\{2\}\\vee a\_\{3\}⋯\\cdotsFragmentℱ​\(𝒜\)\\mathcal\{F\}\(\\mathcal\{A\}\):∧\\wedge∨\\veeFigure 2:Fragment structure\.*Top*: predicatesμk∈𝒫\\mu\_\{k\}\\in\\mathcal\{P\}\.*Middle*: temporal atomsaq∈𝒜a\_\{q\}\\in\\mathcal\{A\}, e\.g\., each applying a single past\-time operator \(⊡I\\boxdot\_\{I\}or⟐I\\Diamonddot\_\{I\}\) to one predicate\.*Bottom*: induced fragmentℱ​\(𝒜\)\\mathcal\{F\}\(\\mathcal\{A\}\), formed by closing𝒜\\mathcal\{A\}under conjunction \(solid,∧\\wedge\) and disjunction \(dashed,∨\\vee\)\.###### Definition 2\(Atomic dictionary and induced fragment\)\.

A finite set𝒜=\{a1,…,ar\}\\mathcal\{A\}=\\\{a\_\{1\},\\dots,a\_\{r\}\\\}of ptSTL formulas is an*atomic dictionary*\. The*induced fragment*ℱ​\(𝒜\)\\mathcal\{F\}\(\\mathcal\{A\}\)is the smallest set containing𝒜\\mathcal\{A\}and closed under conjunction and disjunction:

φ∈ℱ\(𝒜\)⟺φ::=aq∣φ1∧φ2∣φ1∨φ2,aq∈𝒜,\\varphi\\in\\mathcal\{F\}\(\\mathcal\{A\}\)\\;\\Longleftrightarrow\\;\\varphi::=a\_\{q\}\\mid\\varphi\_\{1\}\\wedge\\varphi\_\{2\}\\mid\\varphi\_\{1\}\\vee\\varphi\_\{2\},\\quad a\_\{q\}\\in\\mathcal\{A\},withφ1,φ2∈ℱ​\(𝒜\)\\varphi\_\{1\},\\varphi\_\{2\}\\in\\mathcal\{F\}\(\\mathcal\{A\}\)\. The*maximum horizon*of the fragmentℱ​\(𝒜\)\\mathcal\{F\}\(\\mathcal\{A\}\)isKmax:=maxq⁡hor​\(aq\)K\_\{\\max\}:=\\max\_\{q\}\\,\\mathrm\{hor\}\(a\_\{q\}\)\.

The elements of𝒜\\mathcal\{A\}are “atomic” in the sense that they are irreducible withinℱ​\(𝒜\)\\mathcal\{F\}\(\\mathcal\{A\}\): no formula in the fragment can be decomposed further below these atoms\. Crucially, the choice of𝒜\\mathcal\{A\}is a design decision that determines the expressiveness of the fragment\. Larger or richer dictionaries admit more complex specifications but require predicting a higher\-dimensional semantic basis; see Section[IV](https://arxiv.org/html/2605.13923#S4)\.

###### Example 1\.

In the experiments \(Section[VII](https://arxiv.org/html/2605.13923#S7)\), we use the depth\-1 atomic dictionary

𝒜=\{⊡Iμk,⟐Iμk∣μk∈𝒫,I∈ℐ\},\\mathcal\{A\}=\\big\\\{\\boxdot\_\{I\}\\,\\mu\_\{k\},\\;\\Diamonddot\_\{I\}\\,\\mu\_\{k\}\\mid\\mu\_\{k\}\\in\\mathcal\{P\},\\;I\\in\\mathcal\{I\}\\big\\\},\(2\)whereℐ\\mathcal\{I\}is a finite set of time intervals, yieldingr=2​m​\|ℐ\|r=2m\|\\mathcal\{I\}\|atoms\. Each atom applies a single temporal operator to one predicate; the induced fragment then allows arbitrary∧⁣/⁣∨\\wedge/\\veecombinations of these temporal queries\. The two\-level structure is illustrated in Fig\.[2](https://arxiv.org/html/2605.13923#S3.F2)\.

In the following, we may suppress the dependence ofℱ\\mathcal\{F\}on𝒜\\mathcal\{A\}when the dictionary is clear from context, and writeℱ\\mathcal\{F\}to denote the target fragment for brevity\.

### III\-DProblem Statement

We consider vision\-based monitors that, at each given timett, have access only to the observation history\{oτ\}τ=0t\\\{o\_\{\\tau\}\\\}\_\{\\tau=0\}^\{t\}and not the true state history\{xt\}τ=0t\\\{\{x\}\_\{t\}\\\}\_\{\\tau=0\}^\{t\}\. In particular, we focus on monitors that operate on a learned latent representation of the observation history \(ℬt\{\\mathcal\{B\}\}\_\{t\}\), which is a common approach in practice for vision\-based systems; recall Fig\.[1](https://arxiv.org/html/2605.13923#S1.F1)\.

To this end, an encoderencθ:𝕆H→ℝdℬ\\operatorname\{enc\}\_\{\\theta\}\\colon\\mathbb\{O\}^\{H\}\\to\\mathbb\{R\}^\{d\_\{\\mathcal\{B\}\}\}maps a sliding history ofH\>0H\>0observations111Note thatHHandKmaxK\_\{\\max\}are independent parameters:KmaxK\_\{\\max\}measures the length of the*state*history required to evaluate formulas in the fragmentℱ\\mathcal\{F\}, whileHHmeasures the length of the*observation*history fed into the encoder\.to a latent representationℬt=encθ⁡\(ot−H\+1:t\)∈ℝdℬ\{\\mathcal\{B\}\}\_\{t\}=\\operatorname\{enc\}\_\{\\theta\}\(o\_\{t\-H\+1:t\}\)\\in\\mathbb\{R\}^\{d\_\{\\mathcal\{B\}\}\}\. At runtime, the monitor has access only toℬt\{\\mathcal\{B\}\}\_\{t\}; the physical statextx\_\{t\}is never directly observed\.

Let a dataset𝒟=\{\(o0:Tii,x0:Tii\)\}i=1N\\mathcal\{D\}=\\\{\(o^\{i\}\_\{0:T\_\{i\}\},x^\{i\}\_\{0:T\_\{i\}\}\)\\\}\_\{i=1\}^\{N\}withNNepisodes of respective lengthTi\>0T\_\{i\}\>0drawn from the system in \([1](https://arxiv.org/html/2605.13923#S3.E1)\) be split into training, calibration, and test episodes, and fix a target fragmentℱ\\mathcal\{F\}of temporal logic formulas \(with maximum horizonKmaxK\_\{\\max\}\) and confidence level1−α∈\[0,1\]1\-\\alpha\\in\[0,1\]\.

###### Problem 1\(Reusable Certified Online Monitoring\)\.

Construct a monitor that, at each valid timet≥Kmaxt\\geq K\_\{\\max\}, uses only the observation history\{oτ\}τ≤t\\\{o\_\{\\tau\}\\\}\_\{\\tau\\leq t\}to output, for any queried formulaφ∈ℱ\\varphi\\in\\mathcal\{F\}, a certified lower boundρ¯tφ∈ℝ\\underline\{\\rho\}\_\{t\}^\{\\varphi\}\\in\\mathbb\{R\}such that:

1. \(i\)*Validity:*ℙ​\(ρ¯tφ≤ρ​\(φ,x,t\)\)≥1−α\\mathbb\{P\}\(\\underline\{\\rho\}\_\{t\}^\{\\varphi\}\\leq\\rho\(\\varphi,\{x\},t\)\)\\geq 1\-\\alpha;
2. \(ii\)*Reusability:*a single trained encoder and a single calibration pass support allφ∈ℱ\\varphi\\in\\mathcal\{F\}, with no per\-formula retraining\.

We consider two instantiations of the validity guarantee, differing in what the probability in Problem[1](https://arxiv.org/html/2605.13923#Thmproblem1)\(i\) is taken over\.*Level\-1*\(episodewise\):ℙ\\mathbb\{P\}is jointly over theNNcalibration episodes and the test episode, and the bound holds simultaneously for all valid timestt\.*Level\-2*\(random\-time\):ℙ\\mathbb\{P\}additionally includes a uniformly sampled evaluation timeτ\\tauwithin the test episode, and the bound holds atτ\\tau\.

## IVSUFFICIENT STATISTICS FOR REUSABLE VISION\-BASED MONITORING

The central question of reusable monitoring is:*what must the latent representationℬt\{\\mathcal\{B\}\}\_\{t\}encode so that every formula in the target fragmentℱ\\mathcal\{F\}can be decoded from it by a monotone, 1\-Lipschitz function, for any possible signalx\{x\}?*We seek the smallest such representation, thereby identifying the minimum prediction target needed to support the entire fragment\. We restrict the decoder class to monotone, 1\-Lipschitz functions, which are the natural choice for ptSTL because its robustness semantics are built frommin\\min,max\\max, and coordinate projections, and because this is precisely the class that enables tight conformal certification \(Section[V](https://arxiv.org/html/2605.13923#S5)\)\.

We present two choices ofℬt\{\\mathcal\{B\}\}\_\{t\}with complementary properties\. \(1\) The*predicate\-history*basisℬt𝒫\{\\mathcal\{B\}\}^\{\\mathcal\{P\}\}\_\{t\}is a*fragment\-agnostic*statistic: it supports every bounded\-horizon ptSTL formula over𝒫\\mathcal\{P\}without any prior knowledge of the target fragment\. \(2\) The*semantic basis*ℬt𝒜\{\\mathcal\{B\}\}^\{\\mathcal\{A\}\}\_\{t\}is a*fragment\-specific*statistic: given a chosen fragmentℱ​\(𝒜\)\\mathcal\{F\}\(\\mathcal\{A\}\), it is the minimum representation from which every formula in the fragment admits a monotone, 1\-Lipschitz decoder, uniformly over all signals\.

### IV\-APredicate\-History Basis

The*predicate history*collects the robustness values of all atomic predicates𝒫\\mathcal\{P\}over the full fragment horizonKmaxK\_\{\\max\}:

ℬt𝒫:=\(μk​\(x,t−j\)\)k=1,…,m,j=0,…,Kmax∈ℝm​\(Kmax\+1\)\.\{\\mathcal\{B\}\}^\{\\mathcal\{P\}\}\_\{t\}:=\\big\(\\mu\_\{k\}\(\{x\},t\-j\)\\big\)\_\{k=1,\\dots,m,\\;j=0,\\dots,K\_\{\\max\}\}\\in\\mathbb\{R\}^\{m\(K\_\{\\max\}\+1\)\}\.\(3\)It is fragment\-agnostic in the following sense\.

###### Proposition 1\(Predicate history factorization\)\.

For any ptSTL formulaφ\\varphiin PNF with predicates𝒫\\mathcal\{P\}andhor​\(φ\)≤Kmax\\mathrm\{hor\}\(\\varphi\)\\leq K\_\{\\max\}, and anyt≥Kmaxt\\geq K\_\{\\max\}, there exists a monotone, 1\-Lipschitz \(under∥⋅∥∞\\\|\\cdot\\\|\_\{\\infty\}\) decoderdecφ:ℝm​\(Kmax\+1\)→ℝ\\operatorname\{dec\}\_\{\\varphi\}\\colon\\mathbb\{R\}^\{m\(K\_\{\\max\}\+1\)\}\\to\\mathbb\{R\}such that

ρ​\(φ,x,t\)=decφ⁡\(ℬt𝒫\)\.\\rho\(\\varphi,\{x\},t\)=\\operatorname\{dec\}\_\{\\varphi\}\(\{\\mathcal\{B\}\}^\{\\mathcal\{P\}\}\_\{t\}\)\.

###### Proof\.

Every predicate robustness valueμk​\(x,t−j\)\\mu\_\{k\}\(\{x\},t\-j\)appearing in the evaluation ofφ\\varphiis a coordinate ofℬt𝒫\{\\mathcal\{B\}\}^\{\\mathcal\{P\}\}\_\{t\}\. The decoderdecφ\\operatorname\{dec\}\_\{\\varphi\}is constructed by structural induction, composing coordinate projections,min\\min, andmax\\maxaccording to the parse tree ofφ\\varphi\. Each of these operations is monotone and 1\-Lipschitz under∥⋅∥∞\\\|\\cdot\\\|\_\{\\infty\}, implying the result\. ∎

The predicate history is the natural fragment\-agnostic baseline: it can be predicted once and then decoded to any formula at query time, with no knowledge of the target fragment \(within ptSTL over𝒫\\mathcal\{P\}\) required at training or calibration time\. Its dimensionm​\(Kmax\+1\)m\(K\_\{\\max\}\+1\)grows linearly with the number of predicates and the fragment horizon, making it the most expensive representation we consider\.

This motivates asking whether a smaller representation suffices when the target fragment is known\. The following subsection answers this precisely\.

### IV\-BSemantic Basis

Suppose a target fragmentℱ​\(𝒜\)\\mathcal\{F\}\(\\mathcal\{A\}\)has been fixed \(Definition[2](https://arxiv.org/html/2605.13923#Thmdefinition2)\)\. Rather than retaining the full predicate history \([3](https://arxiv.org/html/2605.13923#S4.E3)\), we ask whether a smaller statistic suffices to evaluate every formula inℱ​\(𝒜\)\\mathcal\{F\}\(\\mathcal\{A\}\)\. The answer is yes: it is enough to retain the robustness values of the atomsa∈𝒜a\\in\\mathcal\{A\}\. We call this basis the*semantic basis*ℬt𝒜\{\\mathcal\{B\}\}^\{\\mathcal\{A\}\}\_\{t\}which is the minimum in an information\-theoretic sense \(Definition[4](https://arxiv.org/html/2605.13923#Thmdefinition4)\)\.

###### Definition 3\(Semantic basis\)\.

For an atomic dictionary𝒜=\{a1,…,ar\}\\mathcal\{A\}=\\\{a\_\{1\},\\dots,a\_\{r\}\\\}, the*semantic basis*is

ℬt𝒜:=\(ρ​\(aq,x,t\)\)q=1r∈ℝr\.\{\\mathcal\{B\}\}^\{\\mathcal\{A\}\}\_\{t\}:=\\big\(\\rho\(a\_\{q\},\{x\},t\)\\big\)\_\{q=1\}^\{r\}\\in\\mathbb\{R\}^\{r\}\.\(4\)

The semantic basis stores exactly one robustness value per atom in𝒜\\mathcal\{A\}\. In general, a basisℬt\{\\mathcal\{B\}\}\_\{t\}*supports*ℱ​\(𝒜\)\\mathcal\{F\}\(\\mathcal\{A\}\)if everyφ∈ℱ​\(𝒜\)\\varphi\\in\\mathcal\{F\}\(\\mathcal\{A\}\)admits a monotone, 1\-Lipschitz decoderdecφ\\operatorname\{dec\}\_\{\\varphi\}satisfyingρ​\(φ,x,t\)=decφ⁡\(ℬt\)\\rho\(\\varphi,\{x\},t\)=\\operatorname\{dec\}\_\{\\varphi\}\(\{\\mathcal\{B\}\}\_\{t\}\)for all signalsx\{x\}and all timest≥Kmaxt\\geq K\_\{\\max\}\. Uniformity over signals is crucial: without it, the downstream conformal guarantees would not transfer beyond the calibration distribution\. To state the minimality claim precisely, we compare bases by their information content\.

###### Definition 4\(Information order\)\.

For two deterministic statisticsℬt\(1\)=T1​\(ℬt𝒫\)\{\\mathcal\{B\}\}\_\{t\}^\{\(1\)\}=T\_\{1\}\(\{\\mathcal\{B\}\}^\{\\mathcal\{P\}\}\_\{t\}\)andℬt\(2\)=T2​\(ℬt𝒫\)\{\\mathcal\{B\}\}\_\{t\}^\{\(2\)\}=T\_\{2\}\(\{\\mathcal\{B\}\}^\{\\mathcal\{P\}\}\_\{t\}\), whereT1,T2T\_\{1\},T\_\{2\}are arbitrary deterministic maps, writeℬt\(1\)⪯ℬt\(2\)\{\\mathcal\{B\}\}\_\{t\}^\{\(1\)\}\\preceq\{\\mathcal\{B\}\}\_\{t\}^\{\(2\)\}if there exists a deterministic maphhsuch thatℬt\(1\)=h​\(ℬt\(2\)\)\{\\mathcal\{B\}\}\_\{t\}^\{\(1\)\}=h\(\{\\mathcal\{B\}\}\_\{t\}^\{\(2\)\}\)for all signalsx\{x\}and all valid timest≥Kmaxt\\geq K\_\{\\max\}\. Thenℬt\(2\)\{\\mathcal\{B\}\}\_\{t\}^\{\(2\)\}is*at least as informative as*ℬt\(1\)\{\\mathcal\{B\}\}\_\{t\}^\{\(1\)\}\.

The semantic basisℬt𝒜\{\\mathcal\{B\}\}^\{\\mathcal\{A\}\}\_\{t\}is the minimum of this order among all statistics that supportℱ​\(𝒜\)\\mathcal\{F\}\(\\mathcal\{A\}\)\.

###### Theorem 1\(Minimality of the semantic basis\)\.

Let𝒜=\{a1,…,ar\}\\mathcal\{A\}=\\\{a\_\{1\},\\dots,a\_\{r\}\\\}and letℱ​\(𝒜\)\\mathcal\{F\}\(\\mathcal\{A\}\)be its∧⁣/⁣∨\\wedge/\\vee\-closure\.

1. \(i\)For everyφ∈ℱ​\(𝒜\)\\varphi\\in\\mathcal\{F\}\(\\mathcal\{A\}\), there exists a monotone, 1\-Lipschitz \(under∥⋅∥∞\\\|\\cdot\\\|\_\{\\infty\}\) decoderdecφ:ℝr→ℝ\\operatorname\{dec\}\_\{\\varphi\}\\colon\\mathbb\{R\}^\{r\}\\to\\mathbb\{R\}such thatρ​\(φ,x,t\)=decφ⁡\(ℬt𝒜\)\\rho\(\\varphi,\{x\},t\)=\\operatorname\{dec\}\_\{\\varphi\}\(\{\\mathcal\{B\}\}^\{\\mathcal\{A\}\}\_\{t\}\)\.
2. \(ii\)ℬt𝒜\{\\mathcal\{B\}\}^\{\\mathcal\{A\}\}\_\{t\}is the minimum statistic: for everyℬt\{\\mathcal\{B\}\}\_\{t\}that supportsℱ​\(𝒜\)\\mathcal\{F\}\(\\mathcal\{A\}\), we haveℬt𝒜⪯ℬt\{\\mathcal\{B\}\}^\{\\mathcal\{A\}\}\_\{t\}\\preceq\{\\mathcal\{B\}\}\_\{t\}\.

###### Proof\.

For \(i\), definedecφ\\operatorname\{dec\}\_\{\\varphi\}recursively:decaq⁡\(b\)=bq\\operatorname\{dec\}\_\{a\_\{q\}\}\(b\)=b\_\{q\},decφ1∧φ2=min⁡\{decφ1,decφ2\}\\operatorname\{dec\}\_\{\\varphi\_\{1\}\\wedge\\varphi\_\{2\}\}=\\min\\\{\\operatorname\{dec\}\_\{\\varphi\_\{1\}\},\\allowbreak\\operatorname\{dec\}\_\{\\varphi\_\{2\}\}\\\},decφ1∨φ2=max⁡\{decφ1,decφ2\}\\operatorname\{dec\}\_\{\\varphi\_\{1\}\\vee\\varphi\_\{2\}\}=\\max\\\{\\operatorname\{dec\}\_\{\\varphi\_\{1\}\},\\allowbreak\\operatorname\{dec\}\_\{\\varphi\_\{2\}\}\\\}\. Monotonicity and 1\-Lipschitz continuity follow becausemin\\min,max\\max, and coordinate projections have these properties under∥⋅∥∞\\\|\\cdot\\\|\_\{\\infty\}\. For \(ii\), by \(i\)ℬt𝒜\{\\mathcal\{B\}\}^\{\\mathcal\{A\}\}\_\{t\}supportsℱ​\(𝒜\)\\mathcal\{F\}\(\\mathcal\{A\}\)\. For minimality, each atomaqa\_\{q\}belongs toℱ​\(𝒜\)\\mathcal\{F\}\(\\mathcal\{A\}\), so anyℬt\{\\mathcal\{B\}\}\_\{t\}that supportsℱ​\(𝒜\)\\mathcal\{F\}\(\\mathcal\{A\}\)admits a decoderdec¯q\\overline\{\\operatorname\{dec\}\}\_\{q\}withρ​\(aq,x,t\)=dec¯q​\(ℬt\)\\rho\(a\_\{q\},\{x\},t\)=\\overline\{\\operatorname\{dec\}\}\_\{q\}\(\{\\mathcal\{B\}\}\_\{t\}\)\. Stacking givesℬt𝒜=dec¯​\(ℬt\)\{\\mathcal\{B\}\}^\{\\mathcal\{A\}\}\_\{t\}=\\overline\{\\operatorname\{dec\}\}\(\{\\mathcal\{B\}\}\_\{t\}\), soℬt𝒜⪯ℬt\{\\mathcal\{B\}\}^\{\\mathcal\{A\}\}\_\{t\}\\preceq\{\\mathcal\{B\}\}\_\{t\}\. ∎

Theorem[1](https://arxiv.org/html/2605.13923#Thmtheorem1)establishes that, for a fixed atomic dictionary𝒜\\mathcal\{A\}and decoder class restricted to monotone11\-Lipschitz maps under∥⋅∥∞\\\|\\cdot\\\|\_\{\\infty\}, the semantic basis is the smallest prediction target that supports the entire fragmentℱ​\(𝒜\)\\mathcal\{F\}\(\\mathcal\{A\}\)\.

The predicate\-history basis \([3](https://arxiv.org/html/2605.13923#S4.E3)\) recovers the semantic basis \([4](https://arxiv.org/html/2605.13923#S4.E4)\) in the limit; e\.g\., consider𝒜\\mathcal\{A\}in \([2](https://arxiv.org/html/2605.13923#S3.E2)\) with degenerate intervalsℐ=\[j,j\]\\mathcal\{I\}=\[j,j\]for allj∈\{0,…,Kmax\}j\\in\\\{0,\\dots,K\_\{\\max\}\\\}, thenℬt𝒜=ℬt𝒫\{\\mathcal\{B\}\}^\{\\mathcal\{A\}\}\_\{t\}=\{\\mathcal\{B\}\}^\{\\mathcal\{P\}\}\_\{t\}, i\.e\., the two coincide and no compression is possible\.

## VCONFORMAL CERTIFICATION/CALIBRATION

The previous sections assume exact knowledge ofℬt∈\{ℬt𝒫,ℬt𝒜\}\{\\mathcal\{B\}\}\_\{t\}\\in\\\{\{\\mathcal\{B\}\}^\{\\mathcal\{P\}\}\_\{t\},\{\\mathcal\{B\}\}^\{\\mathcal\{A\}\}\_\{t\}\\\}\. In practice, the encoder predicts an estimateℬ^t\\widehat\{\\mathcal\{B\}\}\_\{t\}from images \(Fig\.[1](https://arxiv.org/html/2605.13923#S1.F1)\), so prediction errors propagate into the decoded robustness predictions\. We use CP to turn error bounds on the basis coordinatesℬt,ℓ\{\\mathcal\{B\}\}\_\{t,\\ell\}into valid lower bounds on the robustness of any formula in the fragmentsℱ​\(𝒫\)\\mathcal\{F\}\(\\mathcal\{P\}\)andℱ​\(𝒜\)\\mathcal\{F\}\(\\mathcal\{A\}\), respectively\. The key is that the monotone, 1\-Lipschitz decoder structure allows us to certify all formulas simultaneously from a single set of conformal bounds on the basis elementsℬt,ℓ\{\\mathcal\{B\}\}\_\{t,\\ell\}\.

To this end, for each basis coordinateℓ\\ell, define the one\-sided overestimation erroret,ℓ:=max⁡\(0,ℬ^t,ℓ−ℬt,ℓ\)e\_\{t,\\ell\}:=\\max\(0,\\widehat\{\\mathcal\{B\}\}\_\{t,\\ell\}\-\{\\mathcal\{B\}\}\_\{t,\\ell\}\)and letσℓ\>0\\sigma\_\{\\ell\}\>0be a coordinatewise scaling factor\. Based on this, we define the*fragment\-wide score*

sℱ​\(t\):=maxℓ⁡et,ℓσℓ\.s^\{\\mathcal\{F\}\}\(t\):=\\max\_\{\\ell\}\\,\\frac\{e\_\{t,\\ell\}\}\{\\sigma\_\{\\ell\}\}\.\(5\)For a formulaφ\\varphi, the*active\-support score*restricts to its basis coordinates:

sφ​\(t\):=maxℓ∈supp​\(φ\)⁡et,ℓσℓ≤sℱ​\(t\),s^\{\\varphi\}\(t\):=\\max\_\{\\ell\\in\\mathrm\{supp\}\(\\varphi\)\}\\frac\{e\_\{t,\\ell\}\}\{\\sigma\_\{\\ell\}\}\\leq s^\{\\mathcal\{F\}\}\(t\),\(6\)wheresupp​\(φ\)\\mathrm\{supp\}\(\\varphi\)denote the set of atom indices on whichdecφ\\operatorname\{dec\}\_\{\\varphi\}depends\. Errors in atoms outsidesupp​\(φ\)\\mathrm\{supp\}\(\\varphi\)do not affect the decoded robustness\. This can also be seen in Fig\.[2](https://arxiv.org/html/2605.13923#S3.F2), where each formula in the fragmentℱ\\mathcal\{F\}is associated with a subset of the basis coordinates through its support, and the score for each formula is the maximum normalized error over its active coordinates\.

###### Proposition 2\(Active\-support error bound\)\.

For any estimateℬ^t∈ℝr\\widehat\{\\mathcal\{B\}\}\_\{t\}\\in\\mathbb\{R\}^\{r\}of basisℬt\{\\mathcal\{B\}\}\_\{t\}and anyφ∈ℱ\\varphi\\in\\mathcal\{F\}in the associated fragment, we have

\|ρ​\(φ,x,t\)−decφ⁡\(ℬ^t\)\|≤maxi∈supp​\(φ\)⁡\|ℬt,i−ℬ^t,i\|\.\\big\|\\,\\rho\(\\varphi,\{x\},t\)\-\\operatorname\{dec\}\_\{\\varphi\}\(\\widehat\{\\mathcal\{B\}\}\_\{t\}\)\\,\\big\|\\leq\\max\_\{i\\in\\mathrm\{supp\}\(\\varphi\)\}\|\{\\mathcal\{B\}\}\_\{t,i\}\-\\widehat\{\\mathcal\{B\}\}\_\{t,i\}\|\.

###### Proof\.

decφ\\operatorname\{dec\}\_\{\\varphi\}is 1\-Lipschitz under∥⋅∥∞\\\|\\cdot\\\|\_\{\\infty\}and depends only on coordinates insupp​\(φ\)\\mathrm\{supp\}\(\\varphi\)\. ∎

###### Example 2\.

In our experiments, the atomic dictionary is𝒜\\mathcal\{A\}defined in \([2](https://arxiv.org/html/2605.13923#S3.E2)\) withm=7m=7predicates,ℐ=\{\[0,1\],\[0,2\],\[0,4\],\[0,8\],\[0,16\]\}\\mathcal\{I\}=\\\{\[0,1\],\[0,2\],\[0,4\],\[0,8\],\[0,16\]\\\}, andKmax=16K\_\{\\max\}=16\. The resulting semantic basis hasr=2​m​\|ℐ\|=70r=2m\|\\mathcal\{I\}\|=70coordinates; the predicate history hasm​\(Kmax\+1\)=119m\(K\_\{\\max\}\+1\)=119\. This gives a41%41\\%reduction in representation size for the same target fragment\.

![Refer to caption](https://arxiv.org/html/2605.13923v1/x1.png)Figure 3:Monitor architectures for both benchmarks\. Both share a CNN\+attention encoder and temporal fusion module\.\(a\)The rolling monitor predictsmmcurrent\-timestep predicates, accumulates them in a streaming buffer, and applies the conformal radiusqφq\_\{\\varphi\}*before*temporal composition \(interval STL\)\.\(b\)The semantic\-basis monitor predicts2​m​\|ℐ\|2m\|\\mathcal\{I\}\|temporal atoms directly;qφq\_\{\\varphi\}is applied*after*composition via the formula’s parse tree\.As a concrete instance, the safety specificationφsafe=⊡\[0,K\]μclear\\varphi\_\{\\mathrm\{safe\}\}=\\boxdot\_\{\[0,K\]\}\\mu\_\{\\mathrm\{clear\}\}has decoderdecφsafe\(ℬt𝒜\)=ρ\(⊡\[0,K\]μclear,x,t\)\\operatorname\{dec\}\_\{\\varphi\_\{\\mathrm\{safe\}\}\}\(\{\\mathcal\{B\}\}^\{\\mathcal\{A\}\}\_\{t\}\)=\\rho\(\\boxdot\_\{\[0,K\]\}\\mu\_\{\\mathrm\{clear\}\},\{x\},t\)—a single coordinate ofℬt𝒜\{\\mathcal\{B\}\}^\{\\mathcal\{A\}\}\_\{t\}\. The reach\-avoid specificationφra=⟐\[0,Kg\]μgoal∧⊡\[0,Kc\]μclear\\varphi\_\{\\mathrm\{ra\}\}=\\Diamonddot\_\{\[0,K\_\{g\}\]\}\\mu\_\{\\mathrm\{goal\}\}\\wedge\\boxdot\_\{\[0,K\_\{c\}\]\}\\mu\_\{\\mathrm\{clear\}\}has decoderdecφra\(ℬt𝒜\)=min\{ρ\(⟐\[0,Kg\]μgoal,x,t\),ρ\(⊡\[0,Kc\]μclear,x,t\)\}\\operatorname\{dec\}\_\{\\varphi\_\{\\mathrm\{ra\}\}\}\(\{\\mathcal\{B\}\}^\{\\mathcal\{A\}\}\_\{t\}\)=\\min\\bigl\\\{\\rho\(\\Diamonddot\_\{\[0,K\_\{g\}\]\}\\mu\_\{\\mathrm\{goal\}\},\{x\},t\),\\,\\rho\(\\boxdot\_\{\[0,K\_\{c\}\]\}\\mu\_\{\\mathrm\{clear\}\},\{x\},t\)\\bigr\\\}—amin\\minof two basis coordinates\.

#### Quantiles:

Given calibration scoresS1,…,SnS\_\{1\},\\dots,S\_\{n\}, let

Q^1−α​\(S1:n\):=S\(min⁡\{n,⌈\(n\+1\)​\(1−α\)⌉\}\)\\widehat\{Q\}\_\{1\-\\alpha\}\(S\_\{1:n\}\):=S\_\{\(\\min\\\{n,\\lceil\(n\+1\)\(1\-\\alpha\)\\rceil\\\}\)\}denote the split\-conformal quantile\. WithC~:=Q^1−α\\widetilde\{C\}:=\\widehat\{Q\}\_\{1\-\\alpha\}of the fragment\-wide scores, the runtime lower bound on coordinateℓ\\ellisℬ¯t,ℓ:=ℬ^t,ℓ−C~​σℓ\\underline\{\{\\mathcal\{B\}\}\}\_\{t,\\ell\}:=\\widehat\{\\mathcal\{B\}\}\_\{t,\\ell\}\-\\widetilde\{C\}\\,\\sigma\_\{\\ell\}\.

###### Lemma 1\(Shared conformal bound\)\.

Ifℬ¯t≤ℬt\\underline\{\{\\mathcal\{B\}\}\}\_\{t\}\\leq\{\\mathcal\{B\}\}\_\{t\}coordinatewise, thendecφ⁡\(ℬ¯t\)≤ρ​\(φ,x,t\)\\operatorname\{dec\}\_\{\\varphi\}\(\\underline\{\{\\mathcal\{B\}\}\}\_\{t\}\)\\leq\\rho\(\\varphi,x,t\)for allφ∈ℱ\\varphi\\in\\mathcal\{F\}, by monotonicity ofdecφ\\operatorname\{dec\}\_\{\\varphi\}\.

Lemma[1](https://arxiv.org/html/2605.13923#Thmlemma1)is the key to reusability: conformal bounds on the basis elementsℬt,ℓ\{\\mathcal\{B\}\}\_\{t,\\ell\}are sufficient to certify every formula in the fragmentℱ\\mathcal\{F\}simultaneously, without a union bound\.

![Refer to caption](https://arxiv.org/html/2605.13923v1/x2.png)Figure 4:\(a\) Crossroad scenario: robot \(blue\) navigates toward the goal \(green\) via a CBF controller while three pedestrians converge\. Cones show predicate sectors \(45∘45^\{\\circ\}half\-angle\); dashed circle:dsafe=1\.0d\_\{\\mathrm\{safe\}\}\{=\}1\.0m\. \(b–d\)64×6464\{\\times\}64observations under image nuisances \(fog, compression, noise\)\.Temporal aggregation:The choice of score determines the strength of the guarantee\.*Level\-1*uses the episode\-wise maximumS\(i\):=maxt⁡sℱ​\(t\)S^\{\(i\)\}:=\\max\_\{t\}s^\{\\mathcal\{F\}\}\(t\), yielding a bound valid uniformly over all valid timest≥Kmaxt\\geq K\_\{\\max\}and allφ∈ℱ\\varphi\\in\\mathcal\{F\}within a test episode\.*Level\-2*samples one timeτi∼Unif​\{Kmax,…,Ti\}\\tau\_\{i\}\\sim\\mathrm\{Unif\}\\\{K\_\{\\max\},\\dots,T\_\{i\}\\\}per episode and setsS\(i\):=sℱ​\(τi\)S^\{\(i\)\}:=s^\{\\mathcal\{F\}\}\(\\tau\_\{i\}\), giving a random\-time guarantee at lower conservatism\. We evaluate both levels experimentally\.

###### Theorem 2\(Simultaneous validity\)\.

Under exchangeable episodes, withℬ¯t,ℓ:=ℬ^t,ℓ−C~​σℓ\\underline\{\{\\mathcal\{B\}\}\}\_\{t,\\ell\}:=\\widehat\{\\mathcal\{B\}\}\_\{t,\\ell\}\-\\widetilde\{C\}\\,\\sigma\_\{\\ell\}andC~=Q^1−α​\(S1:n\)\\widetilde\{C\}=\\widehat\{Q\}\_\{1\-\\alpha\}\(S\_\{1:n\}\):

1. \(i\)*\(Level\-2\)*ℙ\(∀φ∈ℱ:decφ\(ℬ¯τ\)≤ρ\(φ,x,τ\)\)≥1−α\\mathbb\{P\}\(\\forall\\varphi\\in\\mathcal\{F\}\\colon\\operatorname\{dec\}\_\{\\varphi\}\(\\underline\{\{\\mathcal\{B\}\}\}\_\{\\tau\}\)\\leq\\rho\(\\varphi,x,\\tau\)\)\\geq 1\{\-\}\\alpha\.
2. \(ii\)*\(Level\-1\)*ℙ\(∀t≥Kmax,∀φ∈ℱ:decφ\(ℬ¯t\)≤ρ\(φ,x,t\)\)≥1−α\\mathbb\{P\}\(\\forall t\\geq K\_\{\\max\},\\,\\forall\\varphi\\in\\mathcal\{F\}\\colon\\operatorname\{dec\}\_\{\\varphi\}\(\\underline\{\{\\mathcal\{B\}\}\}\_\{t\}\)\\leq\\rho\(\\varphi,x,t\)\)\\geq 1\{\-\}\\alpha\.

###### Proof\.

Split conformal calibration on the exchangeable scores\{S\(i\)\}\\\{S^\{\(i\)\}\\\}yieldsℙ​\(S\(test\)≤C~\)≥1−α\\mathbb\{P\}\(S^\{\(\\mathrm\{test\}\)\}\\leq\\widetilde\{C\}\)\\geq 1\{\-\}\\alpha, henceℬ¯≤ℬ\\underline\{\{\\mathcal\{B\}\}\}\\leq\{\\mathcal\{B\}\}coordinatewise at the relevant time\(s\)\. Apply Lemma[1](https://arxiv.org/html/2605.13923#Thmlemma1)\. ∎

Sincesφ​\(t\)≤sℱ​\(t\)s^\{\\varphi\}\(t\)\\leq s^\{\\mathcal\{F\}\}\(t\), restricting to the active support of a queried formula always yields a tighter or equal bound, at the cost of certifying only that formula rather than the whole fragment\. Thus,sφs^\{\\varphi\}requires recalibrating when the query formula changes\.

We writeqφ:=Q^1−α​\(s1:nφ\)q\_\{\\varphi\}:=\\widehat\{Q\}\_\{1\-\\alpha\}\(s^\{\\varphi\}\_\{1:n\}\)for the formula\-specific conformal radius obtained from active\-support scoring\.

## VIMONITOR ARCHITECTURES

All monitor variants share the same perception backbone \(a CNN encoder mapping an observation window to a128128\-dimensional latent vector\) and differ only in the prediction target and where conformal calibration is applied relative to temporal composition \(see Fig\.[3](https://arxiv.org/html/2605.13923#S5.F3)\)\. The rolling monitor predictsmmvalues per step \(calibrated before composition; supports full ptSTL\)\. The semantic\-basis monitor predicts2​m​\|ℐ\|2m\|\\mathcal\{I\}\|values \(calibrated after composition; supportsℱ​\(𝒜\)\\mathcal\{F\}\(\\mathcal\{A\}\)\)\.

#### Semantic\-Basis Prediction:

For the fragment induced by the atomic dictionary𝒜\\mathcal\{A\}, the monitor predicts the semantic basisℬ^t𝒜∈ℝ2​m​\|ℐ\|\\widehat\{\\mathcal\{B\}\}^\{\\mathcal\{A\}\}\_\{t\}\\in\\mathbb\{R\}^\{2m\|\\mathcal\{I\}\|\}\. By Theorem[1](https://arxiv.org/html/2605.13923#Thmtheorem1), this is the minimum sufficient statistic for reusable monitoring overℱ​\(𝒜\)\\mathcal\{F\}\(\\mathcal\{A\}\)\. Any queried formula is decoded by a deterministicmin\\min/max\\maxtree derived from its parse tree—no per\-formula training is required\.

#### Rolling Prediction:

The rolling monitor predicts only the current predicate vectorμ^​\(t\)∈ℝm\\hat\{\\mu\}\(t\)\\in\\mathbb\{R\}^\{m\}\(estimated from the observation windowot−H\+1:to\_\{t\-H\+1:t\}\) and accumulates predictions in a streaming buffer that reconstructs the predicate windowℬ^t𝒫\\widehat\{\\mathcal\{B\}\}^\{\\mathcal\{P\}\}\_\{t\}online\. Formula evaluation then applies the same interval\-arithmetic decoder as any window\-based monitor\. This produces a larger representation than the semantic basis \(m​\(Kmax\+1\)m\(K\_\{\\max\}\{\+\}1\)vs\.2​m​\|ℐ\|2m\|\\mathcal\{I\}\|entries forℱ​\(𝒜\)\\mathcal\{F\}\(\\mathcal\{A\}\)\), but is easier to learn: the head solves a per\-timestep regression \(mmoutputs\) rather than predicting temporal aggregates \(2​m​\|ℐ\|2m\|\\mathcal\{I\}\|outputs\)\. Since the predicate windowℬt𝒫\{\\mathcal\{B\}\}^\{\\mathcal\{P\}\}\_\{t\}supports the full bounded\-horizon ptSTL fragmentℱ​\(𝒫\)\\mathcal\{F\}\(\\mathcal\{P\}\), the rolling monitor can certify any formula inℱ​\(𝒫\)⊇ℱ​\(𝒜\)\\mathcal\{F\}\(\\mathcal\{P\}\)\\supseteq\\mathcal\{F\}\(\\mathcal\{A\}\)\. For the target fragmentℱ​\(𝒜\)\\mathcal\{F\}\(\\mathcal\{A\}\), this representation is sufficient but not minimal; the semantic basis provides a tighter interface\.

#### Pre\- vs\. Post\-Composition Calibration:

A key distinction is whether conformal calibration is applied*before*or*after*temporal composition\. The rolling monitor calibrates before: the conformal radiusqφq\_\{\\varphi\}is computed on raw per\-timestep prediction errors, then propagated through the temporalmin\\min/max\\maxoperators of the STL formula\. As the horizon grows, the score must protect against the worst error across more temporal lags, soqφq\_\{\\varphi\}increases with\|supp𝒫​\(φ\)\|\|\\mathrm\{supp\}^\{\\mathcal\{P\}\}\(\\varphi\)\|\. The semantic\-basis monitor calibrates after: it predicts temporal aggregates directly, soqφq\_\{\\varphi\}is computed on the aggregated output\. Post\-composition calibration avoids the horizon penalty, makingqφq\_\{\\varphi\}nearly insensitive to temporal depth, but at the cost of a harder prediction problem\. Both architectures are encoder\-agnostic: the prediction heads and conformal calibration depend only on the latent dimension, not the encoder architecture\. A pretrained vision backbone \(e\.g\., a ViT\) could replace the CNN with only the head retrained\.

## VIIEXPERIMENTS

We demonstrate that the optimal architecture depends on both the domain and the calibration level\. On simulated data, a horizon\-dependent crossover occurs: rolling wins at short horizons, semantic at long\. On real\-world driving data \(Section[VII\-B](https://arxiv.org/html/2605.13923#S7.SS2)\), semantic dominates at all horizons under Level\-2 calibration\. Under the stronger Level\-1 guarantee, rolling recovers the advantage on both benchmarks\. Both architectures decisively outperform a Bonferroni\-corrected observer baseline \(Section[VII\-A](https://arxiv.org/html/2605.13923#S7.SS1.SSS0.Px2)\) on every formula tested\.

![Refer to caption](https://arxiv.org/html/2605.13923v1/x3.png)Figure 5:Rolling and semantic monitors on a WOMD scenario \(8888steps,8\.88\.8s\)\. \(a\) Bird’s\-eye view of the ego vehicle \(blue\) and surrounding agents \(red\); inset:3030m monitoring viewport\. \(b–c\) Rolling monitor for⊡\[0,4\]pfront\\boxdot\_\{\[0,4\]\}p\_\{\\mathrm\{front\}\}and⊡\[0,4\]pclear\\boxdot\_\{\[0,4\]\}p\_\{\\mathrm\{clear\}\}\. \(d–e\) Semantic monitor for the same specifications\. Ground truth: black; prediction: dashed; conformal band: blue; white==Safe, gray==Uncertain\. Animated version:[video](https://youtu.be/B4XxOAdq9HI)\.### VII\-ACrossroad Scenario

A CBF\-controlled robot navigates a pedestrian crossroad\[[23](https://arxiv.org/html/2605.13923#bib.bib23)\]\(Fig\.[4](https://arxiv.org/html/2605.13923#S5.F4)\)\. The monitor observes64×6464\{\\times\}64overhead images and predictsm=7m\{=\}7safety predicates \(clearance, directional clearances, front margin, goal reach, speed margin\) withKmax=16K\_\{\\max\}\{=\}16and intervals

ℐ=\{\[0,1\],\[0,2\],\[0,4\],\[0,8\],\[0,16\]\}\.\\mathcal\{I\}=\\\{\[0,1\],\[0,2\],\[0,4\],\[0,8\],\[0,16\]\\\}\.
The rolling monitor predicts77values per step; the semantic monitor predicts7070basis atoms\. Both share a CNN encoder \(128128\-dim latent,H=4H\{=\}4frame history; architecture details in the appendix\)\. The crossroad dataset has5,0005\{,\}000training,1,0001\{,\}000calibration, and500500test episodes\. Ground\-truth predicates are computed from full state; at deployment, only the calibration set requires state access\. All results use one\-sided scoring withα=0\.10\\alpha\{=\}0\.10\. All conformal radii in TABLE[I](https://arxiv.org/html/2605.13923#S7.T1)use formula\-specific active\-support scoring \(qφq\_\{\\varphi\}\): calibration residuals are stored once, andqφq\_\{\\varphi\}is recomputed at query time from the cached scores\. Changing the queried formula requires no new data collection or model inference\.

#### Conformal Tightness:

Fig\.[6](https://arxiv.org/html/2605.13923#S7.F6)shows the conformal radiusqφq\_\{\\varphi\}vs\. horizonKKforφ=⊡\[0,K\]pf\\varphi=\\boxdot\_\{\[0,K\]\}p\_\{f\}: semantic’s radius remains roughly constant while rolling’s inflates steadily, driven by the support\-size penalty that post\-composition calibration avoids\. Rolling is initially tighter belowK≈3K\{\\approx\}3due to decoder complexity being kept equal but having to predict fewer values\. ByK=16K\{=\}16, rolling reachesqφ=2\.25q\_\{\\varphi\}\{=\}2\.25while semantic’s remains atqφ=0\.56q\_\{\\varphi\}\{=\}0\.56—a 4\-times gap \(TABLE[I](https://arxiv.org/html/2605.13923#S7.T1)\)\.

202^\{0\}212^\{1\}222^\{2\}232^\{3\}242^\{4\}0\.20\.512K≈3K\{\\approx\}3HorizonKKqφq\_\{\\varphi\}RollingSemanticFigure 6:Conformal radiusqφq\_\{\\varphi\}vs\. horizonKKfor⊡\[0,K\]pf\\boxdot\_\{\[0,K\]\}p\_\{f\}\(crossroad, Level\-2\)\.
#### Observer Baseline:

We compare against an observer\-style baseline\[[5](https://arxiv.org/html/2605.13923#bib.bib5),[12](https://arxiv.org/html/2605.13923#bib.bib12),[14](https://arxiv.org/html/2605.13923#bib.bib14),[1](https://arxiv.org/html/2605.13923#bib.bib1)\]\. Using the same encoder, the baseline predicts per\-predicate values, constructs symmetric conformal intervals, and propagates them through interval STL semantics\. To ensure a validα\\alpha\-level guarantee, we apply a Bonferroni correction over the active predicate\-lag supportsupp𝒫​\(φ\)\\mathrm\{supp\}^\{\\mathcal\{P\}\}\(\\varphi\)\. The baseline provides the same coverage guarantees as Level\-2, but with far looser radii due to the union bound \(TABLE[I](https://arxiv.org/html/2605.13923#S7.T1)\)\. Level\-1 provides a stronger episodewise guarantee at the cost of larger quantiles\.

### VII\-BReal\-World Validation: Waymo Open Motion Dataset

On the Waymo Open Motion Dataset \(WOMD, v1\.3\.1\)\[[24](https://arxiv.org/html/2605.13923#bib.bib24),[25](https://arxiv.org/html/2605.13923#bib.bib25)\], each scenario provides8\.88\.8s \(8888timesteps at1010Hz\)\. We render64×6464\{\\times\}64bird’s eye view images and extractm=7m\{=\}7predicates \(see TABLE[I](https://arxiv.org/html/2605.13923#S7.T1)\), using the same encoder and50,00050\{,\}000training,1,0661\{,\}066calibration,567567test scenarios \(49,89649\{,\}896timesteps\)\. Calibration and test scenarios are drawn as disjoint random subsets of the*validation\_interactive*split; exchangeability is assumed under i\.i\.d\. sampling within the split\. To address distribution shift within the dataset \(e\.g\., across geographic regions or weather conditions\), robust conformal methods\[[3](https://arxiv.org/html/2605.13923#bib.bib3)\]can be applied\.

TABLE I:Results under Level\-2 \(random\-time\) and Level\-1 \(episodewise\) calibration \(α=0\.10\\alpha\{=\}0\.10\)\. CSR: certified safe rate\. Prec: precision \(fraction of safe certifications that are correct\)\. FPR: false\-positive rate\. GT: ground\-truth safe rate \(“—” when GT=100%\{=\}100\\%\)\.Level\-2Level\-1∗Observer BaselineSemanticRollingSemanticRollingSpecificationφ\\varphiGT%qφq\_\{\\varphi\}↓\\downarrowCSR↑\\uparrowPrec↑\\uparrowFPR↓\\downarrowqφq\_\{\\varphi\}↓\\downarrowCSR↑\\uparrowPrec↑\\uparrowFPR↓\\downarrowqφq\_\{\\varphi\}↓\\downarrowCSR↑\\uparrowPrec↑\\uparrowFPR↓\\downarrowqφq\_\{\\varphi\}↓\\downarrowCSR↑\\uparrowqφq\_\{\\varphi\}↓\\downarrowCSR↑\\uparrowCrossroad*Horizon scaling \(pfp\_\{f\}\)*⊡\[0,1\]pf\\boxdot\_\{\[0,1\]\}p\_\{f\}1001\.3686\.7100—\.3398\.999\.9—\.2198\.699\.9—5\.7854\.26\.6753\.0⊡\[0,4\]pf\\boxdot\_\{\[0,4\]\}p\_\{f\}1003\.7655\.9100—\.3996\.799\.9—\.3895\.899\.9—5\.8249\.86\.6749\.1⊡\[0,16\]pf\\boxdot\_\{\[0,16\]\}p\_\{f\}1006\.6836\.2100—\.5687\.499\.7—2\.2560\.099\.9—5\.6136\.56\.6736\.2*Compound*⊡\[0,4\]pf∧⊡\[0,4\]pl\\boxdot\_\{\[0,4\]\}p\_\{f\}\{\\wedge\}\\boxdot\_\{\[0,4\]\}p\_\{l\}985\.6212\.599\.90\.11\.0076\.199\.80\.11\.1272\.499\.90\.16\.468\.17\.475\.6*Eventually*⟐\[0,4\]​pf\\Diamonddot\_\{\[0,4\]\}p\_\{f\}1003\.7668\.5100—\.2899\.7100—\.3899\.9100—5\.8957\.66\.6756\.3WOMD*Horizon scaling \(pfp\_\{f\}\)*⊡\[0,1\]pf\\boxdot\_\{\[0,1\]\}p\_\{f\}1002\.0190\.2100—\.8198\.1100—\.9198\.1100—5\.9670\.74\.2778\.8⊡\[0,4\]pf\\boxdot\_\{\[0,4\]\}p\_\{f\}1003\.0079\.2100—\.8296\.9100—1\.6491\.0100—6\.3664\.14\.2775\.4⊡\[0,16\]pf\\boxdot\_\{\[0,16\]\}p\_\{f\}1005\.4946\.4100—1\.9185\.5100—2\.9474\.4100—8\.7840\.74\.2765\.5*Safety\-critical predicates \(K=4K\{=\}4\)*⊡\[0,4\]ps\\boxdot\_\{\[0,4\]\}p\_\{s\}967\.7430\.599\.81\.92\.1185\.098\.531\.92\.2571\.999\.410\.46\.0252\.05\.2946\.1⊡\[0,4\]pτ\\boxdot\_\{\[0,4\]\}p\_\{\\tau\}627\.290\.175\.90\.11\.9232\.691\.47\.42\.0316\.396\.71\.45\.004\.34\.153\.0⊡\[0,4\]ph\\boxdot\_\{\[0,4\]\}p\_\{h\}4013\.220\.999\.60\.03\.8821\.294\.32\.04\.9314\.198\.70\.311\.853\.611\.003\.8*Compound*⊡\[0,4\]pf∧⊡\[0,4\]pl∧⊡\[0,4\]pr\\boxdot\_\{\[0,4\]\}p\_\{f\}\{\\wedge\}\\boxdot\_\{\[0,4\]\}p\_\{l\}\{\\wedge\}\\boxdot\_\{\[0,4\]\}p\_\{r\}1005\.8042\.8100—1\.5976\.8100—2\.2968\.4100—8\.1132\.65\.8243\.4⊡\[0,4\]pf∧⊡\[0,4\]pτ\\boxdot\_\{\[0,4\]\}p\_\{f\}\{\\wedge\}\\boxdot\_\{\[0,4\]\}p\_\{\\tau\}627\.290\.196\.00\.12\.2525\.392\.84\.82\.589\.597\.20\.76\.660\.55\.110\.6⊡\[0,4\]ps∧⊡\[0,4\]pτ∧⊡\[0,4\]ph\\boxdot\_\{\[0,4\]\}p\_\{s\}\{\\wedge\}\\boxdot\_\{\[0,4\]\}p\_\{\\tau\}\{\\wedge\}\\boxdot\_\{\[0,4\]\}p\_\{h\}3413\.220\.91000\.04\.482\.694\.90\.25\.310\.21000\.011\.940\.011\.020\.0*Eventually*⟐\[0,4\]​pf\\Diamonddot\_\{\[0,4\]\}p\_\{f\}1003\.0091\.3100—\.8199\.2100—1\.6497\.2100—4\.9981\.74\.2784\.7⟐\[0,4\]​pτ\\Diamonddot\_\{\[0,4\]\}p\_\{\\tau\}727\.290\.699\.30\.02\.0142\.293\.59\.82\.0333\.194\.96\.05\.036\.34\.158\.7

∗Level\-1 omits Prec and FPR \(Prec100%100\\%, FPR0for all specs\)\.

TABLE[I](https://arxiv.org/html/2605.13923#S7.T1)reports both architectures on both benchmarks under Level\-2 and Level\-1 calibration\. Fig\.[5](https://arxiv.org/html/2605.13923#S7.F5)shows a single WOMD scenario;Safe\(white\) andUncertain\(gray\) regions are separated by the zero crossing of the conformal lower boundμ^−qφ\\hat\{\\mu\}\-q\_\{\\varphi\}\.

1\. Semantic is uniformly tighter\.At Level\-2, semantic achieves a tighter conformal radius at every horizon on WOMD \(qφ=0\.81q\_\{\\varphi\}\{=\}0\.81vs\.0\.910\.91atK=1K\{=\}1;qφ=1\.91q\_\{\\varphi\}\{=\}1\.91vs\.2\.942\.94atK=16K\{=\}16\)\. Unlike in the crossroad experiment, rolling shows no initial advantage, likely because the learnability gap between the architectures is smaller on real\-world data\.

2\. Soundness and conservatism\.Both monitors are empirically sound: empirical coverage stays above1−α=90%1\{\-\}\\alpha\{=\}90\\%on all specifications, confirming the coverage guarantee of Problem[1](https://arxiv.org/html/2605.13923#Thmproblem1)\(i\)\. The key distinction is conservatism: semantic certifies substantially more timesteps \(e\.g\.,32\.6%32\.6\\%vs\.16\.3%16\.3\\%CSR on⊡\[0,4\]pτ\\boxdot\_\{\[0,4\]\}p\_\{\\tau\}\) because post\-composition calibration yields a tighterqφq\_\{\\varphi\}\.

3\. Liveness and compound formulas\.Switching from⊡\\boxdotto⟐\\Diamonddotrecovers substantial CSR: front clearance rises from91%91\\%to97%97\\%\(rolling\) and from97%97\\%to99%99\\%\(semantic\)\. The compound lane\-change rule⊡\[0,4\]pf∧⊡\[0,4\]pl∧⊡\[0,4\]pr\\boxdot\_\{\[0,4\]\}p\_\{f\}\{\\wedge\}\\boxdot\_\{\[0,4\]\}p\_\{l\}\{\\wedge\}\\boxdot\_\{\[0,4\]\}p\_\{r\}certifies77%77\\%\(semantic\) and68%68\\%\(rolling\) of timesteps with zero false certifications\.

## VIIICONCLUSION

We presented a framework for certified reusable monitoring from vision\. The semantic\-basis monitor predicts the minimal representation needed to decode every formula in the target fragment via a monotone, 1\-Lipschitz decoder, enabling fragment\-wide certification from a single conformal calibration pass\. The rolling monitor trades this minimality for a simpler per\-step learning problem by calibrating before temporal composition\. Both architectures outperform a Bonferroni\-corrected observer baseline on every tested formula\. Their ranking depends on the domain and calibration level: on crossroad, a crossover occurs nearK≈3K\{\\approx\}3, with rolling tighter at short horizons and semantic tighter at long horizons \(TABLE[I](https://arxiv.org/html/2605.13923#S7.T1)\)\. The framework is encoder\-agnostic\. The semantic basis is also amenable to specification mining\[[26](https://arxiv.org/html/2605.13923#bib.bib26)\]\. the monotone decoder structure allows the predicted atom values to directly reveal which specifications are satisfied without enumerating the fragment\. Future work includes richer modalities and adaptive conformal methods\[[21](https://arxiv.org/html/2605.13923#bib.bib21)\]\.

## References

- \[1\]L\. Lindemann, X\. Qin, J\. V\. Deshmukh, and G\. J\. Pappas, “Conformal prediction for STL runtime verification,” in*ACM/IEEE International Conference on Cyber\-Physical Systems*, 2023, pp\. 142–153\.
- \[2\]F\. Cairoli, N\. Paoletti, and L\. Bortolussi, “Conformal quantitative predictive monitoring of STL requirements for stochastic processes,” in*ACM International Conference on Hybrid Systems: Computation and Control*, 2023, pp\. 1–11\.
- \[3\]Y\. Zhao, B\. Hoxha, G\. Fainekos, J\. V\. Deshmukh, and L\. Lindemann, “Robust conformal prediction for STL runtime verification under distribution shift,” in*ACM/IEEE International Conference on Cyber\-Physical Systems*, 2024, pp\. 169–179\.
- \[4\]G\. E\. Fainekos and G\. J\. Pappas, “Robustness of temporal logic specifications for continuous\-time signals,”*Theoretical Computer Science*, vol\. 410, no\. 42, pp\. 4262–4291, 2009\.
- \[5\]J\. V\. Deshmukh, A\. Donzé, S\. Ghosh, X\. Jin, G\. Juniwal, and S\. A\. Seshia, “Robust online monitoring of signal temporal logic,”*Formal Methods in System Design*, vol\. 51, no\. 1, pp\. 5–30, 2017\.
- \[6\]A\. Dokhanchi, B\. Hoxha, and G\. Fainekos, “On\-line monitoring for temporal logic robustness,” in*International Conference on Runtime Verification*\. Springer, 2014, pp\. 231–246\.
- \[7\]T\. Yamaguchi, B\. Hoxha, and D\. Ničković, “RTAMT: Runtime robustness monitors with application to CPS and robotics,”*Softw\. Tools Technol\. Transfer*, vol\. 26, no\. 1, pp\. 79–99, 2024\.
- \[8\]L\. Lindemann, M\. Cleaveland, G\. Shim, and G\. J\. Pappas, “Safe planning in dynamic environments using conformal prediction,”*IEEE Robotics and Automation Letters*, vol\. 8, no\. 8, pp\. 5116–5123, 2023\.
- \[9\]A\. Dixit, L\. Lindemann, S\. X\. Wei, M\. Cleaveland, G\. J\. Pappas, and J\. W\. Burdick, “Adaptive conformal prediction for motion planning among dynamic agents,” in*Learning for Dynamics and Control Conference*\. PMLR, 2023, pp\. 300–314\.
- \[10\]L\. Bortolussi, F\. Cairoli, N\. Paoletti, S\. A\. Smolka, and S\. D\. Stoller, “Neural predictive monitoring,” in*International Conference on Runtime Verification*\. Springer, 2019, pp\. 129–147\.
- \[11\]F\. Cairoli, L\. Bortolussi, and N\. Paoletti, “Neural predictive monitoring under partial observability,” in*International Conference on Runtime Verification*\. Springer, 2021, pp\. 121–141\.
- \[12\]B\. Zhong, C\. Jordan, and J\. Provost, “Extending signal temporal logic with quantitative semantics by intervals for robust monitoring of cyber\-physical systems,”*ACM Transactions on Cyber\-Physical Systems*, vol\. 5, no\. 2, pp\. 1–25, 2021\.
- \[13\]L\. Baird, A\. Harapanahalli, and S\. Coogan, “Interval signal temporal logic from natural inclusion functions,”*IEEE Control Systems Letters*, vol\. 7, pp\. 3555–3560, 2023\.
- \[14\]B\. Finkbeiner, M\. Fränzle, F\. Kohn, and P\. Kröger, “A truly robust signal temporal logic: Monitoring safety properties of interacting cyber\-physical systems under uncertain observation,”*Algorithms*, vol\. 15, no\. 4, p\. 126, 2022\.
- \[15\]A\. Balakrishnan, J\. Deshmukh, B\. Hoxha, T\. Yamaguchi, and G\. Fainekos, “PerceMon: Online monitoring for perception systems,” in*Proc\. 21st International Conference on Runtime Verification \(RV\)*, 2021, pp\. 297–308\.
- \[16\]M\. Hekmatnejad, B\. Hoxha, J\. V\. Deshmukh, Y\. Yang, and G\. Fainekos, “Formalizing and evaluating requirements of perception systems for automated vehicles using spatio\-temporal perception logic,”*IJRR*, vol\. 43, no\. 2, pp\. 203–238, 2024\.
- \[17\]M\. Littman and R\. S\. Sutton, “Predictive representations of state,”*Advances in Neural Information Processing Systems*, vol\. 14, 2001\.
- \[18\]S\. Singh, M\. R\. James, and M\. R\. Rudary, “Predictive state representations: A new theory for modeling dynamical systems,” in*Conference on Uncertainty in Artificial Intelligence*, 2004, pp\. 512–519\.
- \[19\]P\. Kapoor, A\. Hammer, A\. Kapoor, K\. Leung, and E\. Kang, “Pretrained embeddings as a behavior specification mechanism,”*arXiv preprint arXiv:2503\.02012*, 2025\.
- \[20\]F\. De Santis, G\. Ciravegna, P\. Bich, D\. Giordano, and T\. Cerquitelli, “V\-CEM: Bridging performance and intervenability in concept\-based models,” in*World Conference on Explainable Artificial Intelligence*, 2025, pp\. 48–67\.
- \[21\]I\. Gibbs and E\. Candes, “Adaptive conformal inference under distribution shift,”*Advances in Neural Information Processing Systems*, vol\. 34, pp\. 1660–1672, 2021\.
- \[22\]O\. Maler and D\. Nickovic, “Monitoring temporal properties of continuous signals,” in*International Symposium on Formal Techniques in Real\-Time and Fault\-Tolerant Systems*\. Springer, 2004, pp\. 152–166\.
- \[23\]M\. Black, G\. Fainekos, B\. Hoxha, H\. Okamoto, and D\. Prokhorov, “CBFKit: A control barrier function toolbox for robotics applications,” in*IEEE/RSJ Int\. Conference on Intelligent Robots and Systems*, 2024\.
- \[24\]S\. Ettinger, S\. Cheng, B\. Caine, C\. Liu, H\. Zhao, S\. Pradhan, Y\. Chai, B\. Sapp, C\. R\. Qi, Y\. Zhou, Z\. Yang, A\. Chouard, P\. Sun, J\. Ngiam, V\. Vasudevan, A\. McCauley, J\. Shlens, and D\. Anguelov, “Large scale interactive motion forecasting for autonomous driving: The waymo open motion dataset,” in*Proceedings of the IEEE/CVF International Conference on Computer Vision \(ICCV\)*, October 2021, pp\. 9710–9719\.
- \[25\]K\. Chen, R\. Ge, H\. Qiu, R\. Ai\-Rfou, C\. R\. Qi, X\. Zhou, Z\. Yang, S\. Ettinger, P\. Sun, Z\. Leng, M\. Mustafa, I\. Bogun, W\. Wang, M\. Tan, and D\. Anguelov, “WOMD\-LiDAR: Raw sensor dataset benchmark for motion forecasting,” in*Proceedings of the IEEE International Conference on Robotics and Automation \(ICRA\)*, May 2024\.
- \[26\]B\. Hoxha, A\. Dokhanchi, and G\. Fainekos, “Mining parametric temporal logic properties in model\-based design for cyber\-physical systems,”*International Journal on Software Tools for Technology Transfer*, vol\. 20, no\. 1, pp\. 79–93, 2018\.