Online Motion Planning with Soft Metric Interval Temporal Logic in Unknown Dynamic Environment

Motion planning of an autonomous system with high-level specifications has wide applications. However, research of formal languages involving timed temporal logic is still under investigation. Challenges arise when the operating environment is dynamic and unknown since the environment can be found prohibitive, leading to potentially conflicting tasks where pre-specified missions cannot be fully satisfied. Such issues become even more challenging when considering time-bound requirements. This letter proposes a control framework to address these challenges, considering hard constraints to enforce safety requirements and soft constraints to enable task relaxation. The metric interval temporal logic (MITL) specifications are employed to deal with time constraints. By constructing a relaxed timed product automaton, an online motion planning strategy is synthesized with a receding horizon controller to generate policies, achieving multiple objectives in decreasing order of priority 1) formally guarantee the satisfaction of hard safety constraints; 2) mostly fulfill soft timed tasks; 3) collect time-varying rewards as much as possible. Simulation results are provided to validate the proposed approach.