Verifikation von Karten

Wieso überhaupt?

Das ist wohl die typischste Fragestellung bei technischen Lösungen.

Die einfache Antwort ist, dass Karten Fehler enthalten können, die beim Erstellen nicht direkt auffallen. Autonome Fahrzeuge vertrauen diesen Karten blind, weshalb selbst kleine Fehler schnell gefährlich werden können.

Was kann schiefgehen?

Die Konsequenzen sind vielfältig. Simple Fehler wie kleine Lücken im Straßennetz können die autonome Fahrfunktion mitten auf der Autobahn abschalten.

Durch Sensor- oder Verdsarbeitungsfehler können falsche Straßen erkannt und daraufhin eine falsche Trajektorie geplant werden. Auch fehlende Nachbarschaftsrelationen zwischen Lanelets können zu Problemen beim Planen führen.

Wie verifiziert man Karten?

Die bekanntesten Ansätze sind Answer Set Programming (ASP), Ontologien mit Description Logic (DL) und Satisfiability Modulo Theories (SMT). ASP und DL prüfen die Karte auf logische Konsistenz, SMT wird eher zur Reparatur von Trajektorien genutzt.

Alle drei haben aber Schwächen. DL kennt keine Variablen, weshalb sich komplexe Abhängigkeiten zwischen mehreren Kartenelementen nicht direkt ausdrücken lassen. Der Umweg über Logikprogrammierung macht den Ansatz unentscheidbar. SMT garantiert Entscheidbarkeit bei universeller Quantifizierung nicht immer.

Higher-Order Logic als vielversprechenderer Ansatz

Maierhofer et al. schlagen Higher-Order Logic (HOL) vor. Die Idee ist simpel: eine fehlerfreie Karte ist eine Karte, die eine Liste von HOL-Regeln erfüllt. Regeln wie “jedes Lanelet muss einen gültigen Nachfolger referenzieren” oder “linke und rechte Fahrspurgrenze dürfen sich nicht schneiden”. Verletzt die Karte eine Regel, ist das ein Fehler.

Im Vergleich war HOL durchgängig schneller als ASP, DL und SMT, teilweise um ein Vielfaches.

Reparatur von Kartenfehlern

Verifikation alleine reicht natürlich nicht. Zu jeder HOL-Regel gibt es daher eine Reparaturfunktion. Aber man kann nicht einfach alle Regeln der Reihe nach feuern und reparieren, denn eine Reparatur kann andere Teile der Karte beeinflussen. Repariert man zum Beispiel eine fehlerhafte Polylinie, können dadurch Nachbarschaftsrelationen ungültig werden.

Deshalb sind die Regeln in priorisierte Gruppen eingeteilt. Die Reihenfolge folgt den Abhängigkeiten zwischen den Kartenebenen. Ein einfaches Beispiel: geometrische Korrekturen müssen vor topologischen kommen, weil die Topologie von der Geometrie abhängt. Stimmen die Endpunkte zweier Lanelets geometrisch nicht überein, ist auch die Nachfolgerreferenz zwischen ihnen falsch. Repariert man die Topologie zuerst, kann eine spätere geometrische Korrektur sie wieder ungültig machen.

Schneiden sich zum Beispiel die Grenzen eines Lanelets, werden die Punkte an der Kreuzungsstelle zwischen den Polylinien getauscht, sodass sie sich entflechten.

Fehlt dagegen eine Nachfolgerreferenz, wird sie einfach gesetzt. Das läuft so lange, bis die Karte alle Regeln erfüllt.

Ausblick

Kartenverifikation ist eines von vielen Themen, mit denen wir uns im Team aktuell beschäftigen. Ein weiteres ist zum Beispiel die Verifikation der Navigation selbst, also ob das Fahrzeug sich regelkonform durch die Karte bewegt. Dazu wird es in Zukunft noch mehr zu berichten geben.