Optimal Control of Mixed Logical Dynamical Systems with Linear Temporal Logic Specifications

Call Number:

NULL

Accession Number:

NULL

Other Number:

NULL

URL:

https://hybrid.soe.ucsc.edu/files/preprints/31.pdf

Keywords:

hybrid systems

Abstract:

Recently, Linear Temporal Logic (LTL) has been employed as a tool for formal speci?cation in dynamical control systems. With this formal approach, control systems can be designed to provably accomplish a large class of complex tasks speci?ed via LTL. For this purpose, language generating Buchi automata with ?nite abstractions of dynamical systems have been used in the literature. In this paper, we take a mathematical programming-based approach to control of a broad class of discrete-time dynamical systems, called Mixed Logic Dynamical (MLD) systems, with LTL speci?cations. MLDs include discontinuous and hybrid piecewise discrete-time linear systems. We apply these tools for model checking and optimal control of MLD systems with LTL speci?cations. Our algorithms exploit Mixed Integer Linear Programming (MILP) as well as, in the appropriate setting, Mixed Integer Quadratic Programming (MIQP) techniques. Our solution approach introduces a general technique useful in representing LTL constraints as mixed-integer linear constraints

NULL