Cautious Planning with Incremental Symbolic Perception: Designing Verified Reactive Driving Maneuvers

TL;DR

This paper introduces a method for cautious, verified reactive driving control using incremental symbolic perception, enabling autonomous vehicles to handle partially occluded environments with provable safety guarantees.

Contribution

It proposes a novel symbolic refinement tree representation and integrates it with assume-guarantee specifications for reactive control synthesis in autonomous driving.

Findings

Effective control synthesis in occluded environments

Incremental perception improves safety and reliability

Verified reactive plans ensure traffic rule compliance

Abstract

This work presents a step towards utilizing incrementally-improving symbolic perception knowledge of the robot's surroundings for provably correct reactive control synthesis applied to an autonomous driving problem. Combining abstract models of motion control and information gathering, we show that assume-guarantee specifications (a subclass of Linear Temporal Logic) can be used to define and resolve traffic rules for cautious planning. We propose a novel representation called symbolic refinement tree for perception that captures the incremental knowledge about the environment and embodies the relationships between various symbolic perception inputs. The incremental knowledge is leveraged for synthesizing verified reactive plans for the robot. The case studies demonstrate the efficacy of the proposed approach in synthesizing control inputs even in case of partially occluded environments.