Verse framework speeds safety checks for multi-agent cyber physical systems
Verse: Semantics and Verification of Hybrid Multi-Agent Scenarios
Formal Languages and Automata Theory
Summary
Checking safety in systems where many robots or vehicles interact is hard because their actions depend on sensors and maps, and the possible behaviors multiply quickly. The authors created Verse, a way to describe agents, maps, and sensors like regular computer programs and translate them into a precise model for safety analysis. Verse only explores scenarios that actually happen instead of every possible combination, making verification much faster. Tests show Verse works well on cars and drones in 2D and 3D maps and can handle multiple safety checks efficiently.
What this means in practice
- •For autonomous vehicle developers: Check safety properties of interacting vehicles and drones in realistic maps faster than existing tools.
- •For robotics software engineers: Create and verify scenarios involving multiple robots with noisy sensors and complex environmental maps using familiar programming syntax.
Authors
Yangge Li, Katherine Braught, Alex Yuan, Sayan Mitra
Abstract
Verifying cyber-physical systems with many interacting agents remains difficult because interactions are mediated by sensors, individual decisions are constrained by environment (map) structure, and the resulting mode space scales combinatorially. We present Verse, a framework for writing agents, maps, and sensors in a familiar programming language syntax, with a formal semantics for the resulting scenarios. A compiler translates each scenario to a hybrid automaton whose executions correspond exactly to the runs of the scenario. Reachability analysis on this automaton builds an execution tree from two post operators, one for continuous flow over a time step and one for a single agent's mode change, and checks safety assertions at every vertex. The tree expands only the modes that are reached, without enumerating the global mode space. Experiments highlight expressive modeling across cars and drones, 2D/3D maps (including OpenDRIVE imports), noisy sensors, and multiple simultaneous safety assertions. Verse verifies a scenario with 7 agents and 37 modes in 90 seconds on a standard laptop; it is competitive with CORA and JuliaReach on ARCH benchmarks, and on multi-agent scenarios is an order of magnitude faster than JuliaReach at the cost of looser reachable sets.