LTLf Synthesis for Motion Planning in Autonomous Vehicles
Contact: Yong Li
Project Overview
This project focuses on Linear Temporal Logic over finite traces (LTLf) synthesis for motion planning in autonomous vehicles (AVs). LTLf is a formal language used to specify temporal properties of a system, and this project will use it to express high-level goals and constraints for motion planning, such as avoiding obstacles, following traffic rules, or reaching a destination before reaching the destination. The goal is to automatically synthesize a motion plan that satisfies these temporal specifications while navigating complex environments.
Objectives
- Define temporal specifications: use LTLf to encode motion planning objectives. Examples include:
- safety: “always avoid collisions with obstacles”;
- navigation: “eventually reach the destination”;
- traffic compliance: “after stopping at a red light, move forward once the light turns green”.
- Synthesis of motion plans: develop an algorithm that synthesizes motion plans (sequences of control actions) from temporal specifications. This could involve:
- translating the LTLf specification into a deterministic finite automaton (DFA);
- using model checking or satisfiability modulo theories (SMT) solvers to find valid motion plans that satisfy the temporal logic constraints.
- Integration with sampling: during the planning, we can also use sampling as local planner to sample feasible trajectories within a bounded distance, to handle unexpected events (e.g., pedestrians crossing), and changing traffic conditions.
Deliverables
- LTLf specification framework: a set of example LTLf formulas for various motion planning objectives.
- Motion plan synthesis algorithm: a working algorithm that translates LTLf specifications into motion plans.
- Evaluation report: a report demonstrating the synthesized plans’ performance, safety, and efficiency in simulated scenarios.
- Codebase: a well-documented codebase for the LTLf synthesis algorithm and simulation integration.