---
kind: concept
slug: temporal-logic-runtime-monitoring
title: Temporal-logic runtime monitoring
summary: >-
  How to check that a run obeys rules about order and duration, not only its end state. Write each rule as a temporal-logic formula over per-step predicates, compile it to an automaton, step it through the trace and score violations per triggered event. Two cards: a robot-manipulation benchmark with author-reported results, and a position paper with no experiments.
tags: [safety, runtime-monitoring, temporal-logic, formal-verification, robotics, benchmarks]
papers: ["2605.12386", "2411.14520"]
related: [robot-simulation, functional-safety]
status: draft
updated_at: 2026-10-25
---

## Overview

A task can succeed while breaking a rule on the way: a gripper lets go before
the object is set down, or a clean item touches raw food. Checks on the final
state miss these. Isolated state checks and cumulative cost signals are weak
on rules that depend on order or duration [arxiv:2605.12386 §1]
[arxiv:2605.12386 §2].

The method with results is the benchmark card's. It has four parts:

- **Rules in LTLf.** Each rule is a finite-trace temporal-logic formula over
  named Boolean predicates, such as a stable grasp, read from simulator state
  at every step [arxiv:2605.12386 §3.3].
- **Automaton per rule.** Each rule compiles to a deterministic finite
  automaton (DFA). A monitor steps it once per frame. Reaching the rejecting
  sink opens a violation episode [arxiv:2605.12386 §3.4].
- **Recovery.** Each episode has a recovery formula. The episode closes when
  recovery holds, and the rule's automaton returns to its start state
  [arxiv:2605.12386 §3.4].
- **Per-trigger scoring.** Violations are divided by the number of times the
  rule's trigger fired, not by the number of rollouts. A policy that attempts
  more situations is not penalised just for attempting them
  [arxiv:2605.12386 §4.2].

The second card is a position paper on verifying autonomous driving. It argues
that systems built from black-box components need runtime checks of each
component's assumptions and guarantees, and that the verdicts must allow for
uncertainty. It gives no monitor and no results [arxiv:2411.14520 §2]
[arxiv:2411.14520 §3.1] [arxiv:2411.14520 §5].

Evidence is thin. The method rests on one benchmark paper. Its results are
author-reported, and its repository has no license, so implement from the
paper's description and do not copy code [arxiv:2605.12386 §4.1]
[arxiv:2605.12386 app. F].

## Variants

### Offline replay of recorded traces

This is the mode that was evaluated. The monitor runs over a recorded state
trace after the rollout, outside the policy loop [arxiv:2605.12386 app. F].
The authors audit seven policies on LIBERO and five Multitask policies on
RoboCasa365, with 50 rollouts per task [arxiv:2605.12386 §4.1]
[arxiv:2605.12386 app. B]. Card: [SafeManip](/papers/2605.12386).

### Online monitoring inside the loop

The introduction and the Figure 1 caption of the benchmark describe monitoring
as online [arxiv:2605.12386 §1] [arxiv:2605.12386 fig. 1]. None of its reported
results come from in-loop monitoring. The grounding also reads privileged
simulator state (full contact lists, body poses, fixture joints), which a
physical robot does not have [arxiv:2605.12386 app. F]
[arxiv:2605.12386 §6]. The position paper also proposes checking contracts
while the system runs [arxiv:2411.14520 §3.1]. Both treat in-loop use as an
aim, not a tested variant.

### Contracts for black-box components with uncertain verdicts

The position paper frames the problem as composition. Each component states
assumptions (what it needs from the rest of the system) and guarantees (what
it provides when it runs correctly). Runtime verification then checks these
while the system runs. Because perception outputs are uncertain, the paper
says plain true or false verdicts are not enough [arxiv:2411.14520 §3.1]
[arxiv:2411.14520 §4]. Its sketch leaves the verdict type, the evaluation
function and the monitor undefined, and it names uncertain runtime
verification as needed work, not as a solved technique [arxiv:2411.14520 §3.1]
[arxiv:2411.14520 §4]. Card: [Open Challenges in the Formal Verification of
Autonomous Driving](/papers/2411.14520).

### Bounded obligations instead of open-ended ones

"Eventually" obligations with no deadline get a timeout in the enforced set.
Release and transfer settling use 100 frames, which is 5 s at 20 Hz. Forbidden
contact gets a 20-frame tolerance [arxiv:2605.12386 app. F.1]
[arxiv:2605.12386 tab. 6]. "Until" obligations become weak until, so a rollout
that ends mid-obligation is not marked as violated [arxiv:2605.12386 app. F.1].
The contact tolerance changes verdicts: human agreement stays at 100% up to
20 frames and falls to 75% at 40 frames [arxiv:2605.12386 app. E.2].

### Scoring per triggered event or per rollout

The monitor pools violations, violating frames and triggers over rollouts, then
divides by triggers [arxiv:2605.12386 §4.2]. The authors argue that unnormalised
violation counts grow with how often a policy attempts the relevant situations,
which hides per-opportunity reliability [arxiv:2605.12386 §4.2]
[arxiv:2605.12386 §5.1].

## When to use which

| Situation | Use | Why |
|---|---|---|
| Recorded rollouts with full simulator state, comparing policies | Offline replay with per-trigger scores | This is the evaluated setup. Per-trigger scores separate safety from attempt count [arxiv:2605.12386 §4.2] [arxiv:2605.12386 §5.1] |
| Policies attempt different numbers of safety-relevant situations | Per-trigger normalisation | Raw totals rise with attempts [arxiv:2605.12386 §4.2] |
| Rules with open-ended "eventually" clauses, rollouts that can end early | Timeouts plus weak until | Stops end-of-rollout obligations counting as violations [arxiv:2605.12386 app. F.1] |
| Black-box components with documented assumptions and guarantees, such as perception stacks in a vehicle | Contract checks at runtime, as a design direction | Position paper only. It suggests runtime verification with uncertainty, with no monitor and no tests [arxiv:2411.14520 §3.1] [arxiv:2411.14520 §5] |
| Only camera or sensor inputs on hardware | Not tested by either card | Grounding is privileged in the benchmark, and reliability under perceptual error is untested [arxiv:2605.12386 app. F] [arxiv:2605.12386 §6]. The position paper names uncertainty as open [arxiv:2411.14520 §4] |
| Live intervention in the policy loop | Not shown by either card | Evaluation is offline [arxiv:2605.12386 app. F]. The position paper does not build one [arxiv:2411.14520 §5] |

Only two simulators are evaluated, and only with the authors' predicates. Do
not assume the rule set transfers to other domains without new grounding.

## Implementation sketch

The steps follow the description in the benchmark paper. Predicate thresholds
are set per simulator and are not repeated here [arxiv:2605.12386 app. F.4].

```pseudocode
# Turn simulator state into named booleans, once per frame  [arxiv:2605.12386 §3.3]
def grounded_predicates(state):
    # Each predicate reads state the policy never sees  [arxiv:2605.12386 app. F]
    return {
        "StableGrasp": grasp_is_stable(state),
        "ObjReleased": gripper_opened_on(state),
        # ... one entry per proposition in the spec set
    }

# Build the automata before the run, not per frame  [arxiv:2605.12386 §3.4]
monitors = [Monitor(rule.dfa, rule.recovery) for rule in rules]

class Monitor:
    # Advance the rule's DFA while no violation is open  [arxiv:2605.12386 §3.4]
    def step(self, t, pv):
        if self.in_violation:
            # Track recovery; the main automaton is paused  [arxiv:2605.12386 §3.4]
            self.rec = self.recovery.delta(self.rec, pv)
            if self.recovery.accepting(self.rec):
                self.close_episode(t, recovered=True)
                self.in_violation = False
                # Reset to the start state once recovery holds  [arxiv:2605.12386 §3.4]
                self.state = self.dfa.start
            return
        self.state = self.dfa.delta(self.state, pv)
        if self.dfa.rejecting(self.state):
            # Open an episode and start recovery on the same frame  [arxiv:2605.12386 §3.4]
            self.in_violation = True
            self.rec = self.recovery.delta(self.recovery.start, pv)
            self.open_episode(t)

# Per-trigger scores for one rule, pooled over rollouts  [arxiv:2605.12386 §4.2]
def per_trigger_scores(rollouts, rule):
    # Triggers are antecedent activations  [arxiv:2605.12386 §4.2]
    n = count_triggers(rollouts, rule)
    # Violation episodes and violating frames  [arxiv:2605.12386 §4.2]
    v = count_violations(rollouts, rule)
    u = count_violating_frames(rollouts, rule)
    # Divide by triggers, not by rollouts  [arxiv:2605.12386 §4.2]
    return v / n, u / n
```

## Contradictions

The two cards make no conflicting numerical claims. The position paper reports
no measurements [arxiv:2411.14520 §5], so there is nothing to set against the
benchmark numbers. Within the benchmark paper:

- **Online or offline.** The introduction and Figure 1 caption say online
  [arxiv:2605.12386 §1] [arxiv:2605.12386 fig. 1]. The appendix describes replay
  over recorded traces [arxiv:2605.12386 app. F].
- **Policy count.** Section 5 refers to ten policies and training variants. The
  tables list five RoboCasa365 policies, three GR00T ablation settings with three
  checkpoints each, and seven LIBERO policies. The paper does not reconcile these
  [arxiv:2605.12386 §5] [arxiv:2605.12386 app. B].
- **Sign of the correlation.** On LIBERO, violations per triggered event and task
  success are strongly negatively correlated across seven policies (r = −0.99).
  On RoboCasa365 the correlation across five policies is positive (r = +0.66)
  and not significant [arxiv:2605.12386 §5.1]. The paper reads these as separate
  axes, not one trend.

## Papers

- [SafeManip: A Property-Driven Benchmark for Temporal Safety Evaluation in Robotic Manipulation](/papers/2605.12386): defines eight categories of LTLf safety rules, a per-step DFA monitor with recovery, and per-trigger scoring on RoboCasa365 and LIBERO.
- [Open Challenges in the Formal Verification of Autonomous Driving](/papers/2411.14520): position paper on verifying systems of black-box components. Suggests assume-guarantee checks with runtime verification and uncertainty, without a monitor or results.