Trajectory Generation under Metric Interval Temporal Logic Specifications

Abstract: Metric interval temporal logic (MITL) provides a tool to formulate high level tasks in an easyway. This allows to specify behaviour of a dynamical system in a given environment which liesbeyond the scope of simple stabilization. Finding an input of the system which satises the MITLformula, demands new techniques and algorithms. In this thesis, a novel approach is presented whichabstracts the dynamical system into a time optimal weighted transition system (WTS) and convertsthe MITL formula into a Timed Buchi Automaton (TBA). From the graph product of the WTS andTBA a sequence of environment states together with time constraints is obtained. Together with auser specied cost function, the sequence is translated into an optimization problem. The solutionof this nal optimization problem satises the MITL formula for the dynamical system in the givenenvironment and is obtained by using methods from optimal control.