Time-constrained temporal logic control of multi-affine systems

In this paper, we consider the problem of controlling a dynamical system such that its trajectories satisfy a temporal logic property in a given amount of time. We focus on multi-affine systems and specifications given as syntactically co-safe linear temporal logic formulas over rectangular regions in the state space. The proposed algorithm is based on estimating the time bounds for facet reachability problems and solving a time optimal reachability problem on the product between a weighted transition system and an automaton that enforces the satisfaction of the specification. A random optimization algorithm is used to iteratively improve the solution.This work was partially supported at Boston University by grants AFOSR YIP FA9550-09-1-0209, ARO W911NF-09-1-0088, NSF CNS-0834260, ONR MURI N00014-10-10952, and ONR MURI N00014-09-1051. (AFOSR YIP FA9550-09-1-0209 - Boston University; ARO W911NF-09-1-0088 - Boston University; NSF CNS-0834260 - Boston University; ONR MURI N00014-10-10952 - Boston University; ONR MURI N00014-09-1051 - Boston University