From Specifications to Behavior: Maneuver Verification in a Semantic State Space
This addresses the approval trap for product liability in autonomous vehicles by enabling formal verification of high-level behavior against traffic rules, representing an incremental step towards safety of intended functionality.
The paper tackles the problem of verifying autonomous vehicle behavior planning by formalizing traffic rules in linear temporal logic and checking maneuvers in a semantic state space, demonstrating effectiveness with the NuSMV model checker and providing runtime properties for verification.
To realize a market entry of autonomous vehicles in the foreseeable future, the behavior planning system will need to abide by the same rules that humans follow. Product liability cannot be enforced without a proper solution to the approval trap. In this paper, we define a semantic abstraction of the continuous space and formalize traffic rules in linear temporal logic (LTL). Sequences in the semantic state space represent maneuvers a high-level planner could choose to execute. We check these maneuvers against the formalized traffic rules using runtime verification. By using the standard model checker NuSMV, we demonstrate the effectiveness of our approach and provide runtime properties for the maneuver verification. We show that high-level behavior can be verified in a semantic state space to fulfill a set of formalized rules, which could serve as a step towards safety of the intended functionality.