Checking, while the robot runs, that what it is doing satisfies a property: “never closer than a metre to a person”, “every request is answered within two seconds”. Model checking asks whether every possible run is correct. A runtime monitor judges only the run it is watching. That is a smaller promise, and it can be kept on real robots.
Decidability
- A monitor judges one observed trace (Leucker and Schallhart).
- LTL3 gives three answers: true, false, or not yet known. Only 54 of 97 usable specification patterns can ever be decided from a finite trace.
- “Eventually” without a deadline never resolves. A property such as “the robot eventually reaches the dock” stays inconclusive forever, so liveness needs a time bound before a monitor can check it. The split between safety and liveness goes back to Pnueli.
- Signal temporal logic robustness adds a margin, so a monitor can warn before a violation happens.
- Timed automata make timeouts exactly checkable. Hybrid automata show that adding a single stopwatch makes reachability undecidable. Real robot dynamics are past that line, so in practice robot safety gets checked at runtime.
Inputs
No monitor promises that its input is correct. SOTER assumes accurate state estimates, shields read simulator state, Simplex trusts the measurement. A spoofed sensor fools the switch as easily as it fools the controller. Seshia and others call turning environment assumptions into monitors, and deciding what to do when one fires, “a largely unsolved problem”.
The survey by Luckcuck and others found runtime monitoring in 3 of 63 core robot papers, against 32 for model checking. Konur’s swarm verification handles hundreds of identical robots by counting them, and so can’t represent one robot that deviates. MCMAS checks multi-agent systems against epistemic properties (“the robot knows that…”).
Learned components
C-3PO is a perception module that monitors itself: it certifies its own pose estimate or abstains. For learned policies, see the detectors in failure recovery. ROSMonitoring and Caldas and others cover what practitioners actually do with ROS: monitors exist, and their reactions are crude.
Questions
- Monitors on a team with a changing communication graph: this cell is empty in Caldas’s survey of practice.
- Can a monitor know when its own inputs are uncertified, and say so?
- What should a monitor that fires on a teammate do: warn, exclude, or ask a third robot?
Related: robust estimation, safe control, cyber-physical security, robust robotics.