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

被引：107

作者：

Karaman, Sertac ^{[1
]}

Sanfelice, Ricardo G. ^{[1
]}

Frazzoli, Emilio ^{[1
]}

机构：

[1] MIT, Informat & Decis Syst Lab, Cambridge, MA 02139 USA

来源：

47TH IEEE CONFERENCE ON DECISION AND CONTROL, 2008 (CDC 2008) | 2008年

关键词：

D O I：

10.1109/CDC.2008.4739370

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

Recently, Linear Temporal Logic (LTL) has been employed as a tool for formal specification in dynamical control systems. With this formal approach, control systems can be designed to provably accomplish a large class of complex tasks specified via LTL. For this purpose, language generating Buchi automata with finite 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 specifications. 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 specifications. 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.

引用

页码：2117 / 2122

页数：6

共 17 条

[1]

[Anonymous], 2003, CPLEX US MAN

[2] Control of systems integrating logic, dynamics, and constraints [J].

Bemporad, A ;

Morari, M .

AUTOMATICA, 1999, 35 (03) :407-427

[3] SOME RESULTS AND EXPERIMENTS IN PROGRAMMING TECHNIQUES FOR PROPOSITIONAL LOGIC [J].

BLAIR, CE ;

JEROSLOW, RG ;

LOWE, JK .

COMPUTERS & OPERATIONS RESEARCH, 1986, 13 (05) :633-645

[4]

Clarke EM, 1999, MODEL CHECKING, P1

[5]

Fedjki C., 1990, ANN MATH ARTIF INTEL, V1, P123

[6] The model checker SPIN [J].

Holzmann, GJ .

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1997, 23 (05) :279-295

[7]

Karaman S., 2008, AM CONTR C WASH US

[8]

Karaman S., 2008, AIAA C GUID NAV CONT

[9] A fully automated framework for control of linear systems from temporal, logic specifications [J].

Kloetzer, Marius ;

Bella, Calin .

IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2008, 53 (01) :287-297

[10] Temporal logic planning and control of robotic swarms by hierarchical abstractions [J].

Kloetzer, Marius ;

Belta, Calin .

IEEE TRANSACTIONS ON ROBOTICS, 2007, 23 (02) :320-330

← 1 2 →