Litcius/Paper detail

Autonomous Vehicle Decision-Making and Monitoring based on Signal Temporal Logic and Mixed-Integer Programming

Yunus Emre Sahin, Rien Quirynen, Stefano Di Cairano

202041 citationsDOI

Abstract

We propose a decision-making system for auto-mated driving with formal guarantees, synthesized from Signal Temporal Logic (STL) specifications. STL formulae specifying overall and intermediate driving goals and the traffic rules are encoded as mixed-integer inequalities and combined with a simplified vehicle motion model, resulting in a mixed-integer optimization problem. The specification satisfaction for the actual vehicle motion is guaranteed by imposing constraints on the quantitative semantics of STL. For reducing the com-putational burden, we propose an STL encoding that results in a block-sparse structure. The same STL formulae are used for monitoring faults due to imperfect prediction on the vehicle and environment. We demonstrate our method on an urban scenario with intersections, obstacles, and no-pass zones.

Topics & Concepts

Integer programmingComputer scienceInteger (computer science)Block (permutation group theory)Semantics (computer science)SIGNAL (programming language)Programming languageAlgorithmReal-time computingMathematical optimizationMathematicsGeometryFormal Methods in VerificationModel-Driven Software Engineering TechniquesAdvanced Software Engineering Methodologies
Autonomous Vehicle Decision-Making and Monitoring based on Signal Temporal Logic and Mixed-Integer Programming | Litcius