Trajectory Verification for Networked and Autonomous Vehicles using Temporal Logic and Model Checking

Abstract

This paper presents a verification method for the trajectory planning of networked and autonomous vehicles using temporal logic. The method consists of two parts. First, traffic scenarios are verified. Since the verification is not realtime capable, this is done offline. The verification tool provides counterexamples, if collisions or deadlocks are possible for the corresponding traffic scenarios. These counterexamples are generalized and formulated as rule sets. For each class of traffic scenario, we formulate a rule set. Second, during trajectory planning, the method checks if the resulting trajectories fulfill the rules for the current traffic scenario. If the rules are fulfilled, no collision or deadlock is possible. As we show in the evaluation, the rule checking can be performed in real-time.

Authors 4

1. Maximilian Kloock Aachen Chair for Embedded Software

   RWTH Aachen University

   Affiliation as printed

   Chair for Embedded Software, RWTH Aachen University, Aachen, Germany

2. Qingyun He Aachen Chair for Embedded Software

   RWTH Aachen University

   Affiliation as printed

   Chair for Embedded Software, RWTH Aachen University, Aachen, Germany

3. Stefan Kowalewski Aachen Chair for Embedded Software

   RWTH Aachen University

   Affiliation as printed

   Chair for Embedded Software, RWTH Aachen University, Aachen, Germany

4. Bassam Alrifaee Aachen Chair for Embedded Software

   RWTH Aachen University

   Affiliation as printed

   Chair for Embedded Software, RWTH Aachen University, Aachen, Germany