Automatic Control Design Synthesis under Metric Interval Temporal Logic Specifications

Abstract: The problem of synthesizing controllers for motion planning of multi-agent systems under Linear Temporal Logic (LTL) high-level specifications has been of great interest and has been widely studied over the last years. However, LTL cannot handle time constraints as specifications. The time aspect would allow more complicated and specific tasks and it is therefore desirable to incorporate. This work aims to determine how control synthesis for a continuous linear system can be performed based on Metric Interval Temporal Logic (MITL), which is able to handle desired time constraints to high-level specifications. Firstly, a control design synthesis method for a single-agent, based on previous work within both the field of LTL and MITL is presented. Secondly, a control design synthesis method for multi-agent systems considering both local an global MITL specifications is presented. Extended simulations has been performed in MATLAB environment demonstrating the two proposed methodologies. The result shows that the methods guarantee that the MITL specifications are satisfied, for all cases for which a solution is found.