Optimal Control of Markov Decision Processes With Linear Temporal Logic Constraints

被引：139

作者：

Ding, Xuchu ^{[1
]}

Smith, Stephen L. ^{[2
]}

Belta, Calin ^{[3
]}

Rus, Daniela ^{[4
]}

机构：

[1] United Technol Res Ctr, E Hartford, CT 06108 USA

[2] Univ Waterloo, Dept Elect & Comp Engn, Waterloo, ON N2L 3G1, Canada

[3] Boston Univ, Dept Mech Engn, Boston, MA 02215 USA

[4] MIT, Elect Engn & Comp Sci Dept, Comp Sci & Artificial Intelligence Lab, Cambridge, MA 02139 USA

来源：

IEEE TRANSACTIONS ON AUTOMATIC CONTROL | 2014年 / 59卷 / 05期

关键词：

Computation tree logic (CTL); linear temporal logic (LTL); Markov decision process (MDP; AUTOMATA;

D O I：

10.1109/TAC.2014.2298143

中图分类号：

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

学科分类号：

0812 ;

摘要：

In this paper, we develop a method to automatically generate a control policy for a dynamical system modeled as a Markov Decision Process (MDP). The control specification is given as a Linear Temporal Logic (LTL) formula over a set of propositions defined on the states of the MDP. Motivated by robotic applications requiring persistent tasks, such as environmental monitoring and data gathering, we synthesize a control policy thatminimizes the expected cost between satisfying instances of a particular proposition over all policies that maximize the probability of satisfying the given LTL specification. Our approach is based on the definition of a novel optimization problem that extends the existing average cost per stage problem. We propose a sufficient condition for a policy to be optimal, and develop a dynamic programming algorithm that synthesizes a policy that is optimal for a set of LTL specifications.

引用

页码：1244 / 1257

页数：14

共 29 条

[1] Alterovitz R., 2007, P ROB SCI SYST ATL G
[2] [Anonymous], 2011, IFAC P
[3] Baier C, 2004, INT FED INFO PROC, V155, P493
[4] Baier C, 2008, PRINCIPLES OF MODEL CHECKING, P1
[5] Robust solutions of uncertain linear programs
Ben-Tal, A
Nemirovski, A
[J]. OPERATIONS RESEARCH LETTERS, 1999, 25 (01) : 1 - 13
[6] Bertsekas D., 2007, DYNAMIC PROGRAMMING, VII, P246
[7] Chen YS, 2012, IEEE INT CONF ROBOT, P5177, DOI 10.1109/ICRA.2012.6225075
[8] Clarke EM, 1999, MODEL CHECKING, P1
[9] Markov decision processes and regular events
Courcoubetis, C
Yannakakis, M
[J]. IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 1998, 43 (10) : 1399 - 1418
[10] DEALFARO L, 1997, THESIS STANFORD U ST

← 1 2 3 →