Formal Methods

Road testing has one inconvenient flaw: reality insists on happening in real time. That is a problem for autonomous vehicles, robots, drones, and other cyber-physical systems whose failures are rare, contextual, and often expensive to reproduce. Simulation helps because it lets engineers manufacture awkward situations on demand: the pedestrian who appears at the worst possible moment, the parked car blocking the lane, the unprotected turn that requires social judgement rather than just geometry. Lovely. Except simulation has its own embarrassing little issue: a failure in simulation may be a real system weakness, or it may be an artefact of synthetic sensor data wearing a lab coat. ...

TL;DR for operators ProbGuard1 is a runtime safety monitor that tries to answer a more useful question than “Has the agent broken a rule?” It asks: “Given where the agent is now, how likely is it to end up breaking a rule soon?” That shift matters. Many agent failures are not single bad actions. They are bad trajectories: the robot chooses the wrong object, the car carries too much speed into a risky scene, the workflow skips a confirmation step three moves before data is exposed. A conventional rule-based guardrail often detects the problem when the violation is already visible. ProbGuard tries to detect the probability mass moving toward the violation earlier. ...

TL;DR for operators Hospital bed allocation is not just “find an empty bed.” It is a rolling constraint problem: patients arrive, diagnoses imply treatment trajectories, treatment phases require different levels of care, rooms have different capacities and monitoring categories, some patients cannot share rooms, hospital policy may forbid mixed-gender rooms, and moving patients unnecessarily is bad practice. Yes, the spreadsheet is sweating. ...