Incentive Design for Temporal Logic Objectives

被引:0
作者
Savas, Yagiz [1 ]
Gupta, Vijay [2 ]
Ornik, Melkior [3 ,4 ]
Ratliff, Lillian J. [5 ]
Topcu, Ufuk [1 ]
机构
[1] Univ Texas Austin, Dept Aerosp Engn, Austin, TX 78712 USA
[2] Univ Notre Dame, Dept Elect Engn, Notre Dame, IN 46556 USA
[3] Univ Illinois, Dept Aerosp Engn, Urbana, IL USA
[4] Univ Illinois, Coordinated Sci Lab, Urbana, IL USA
[5] Univ Washington, Dept Elect Engn, Seattle, WA 98195 USA
来源
2019 IEEE 58TH CONFERENCE ON DECISION AND CONTROL (CDC) | 2019年
关键词
MODEL CHECKING;
D O I
暂无
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
We study the problem of designing an optimal sequence of incentives that a principal should offer to an agent so that the agent's optimal behavior under the incentives realizes the principal's objective expressed as a temporal logic formula. We consider an agent with a finite decision horizon, and model its behavior as a Markov decision process (MDP). Under certain assumptions, we present a polynomial-time algorithm to synthesize an incentive sequence that minimizes the cost to the principal. We show that if the underlying MDP has only deterministic transitions, the principal can hide its objective from the agent and still realize the desired behavior through incentives. On the other hand, an MDP with stochastic transitions may require the principal to share its objective with the agent. Finally, we demonstrate the proposed method in motion planning examples where a principal changes the optimal trajectory of an agent by providing incentives.
引用
收藏
页码:2251 / 2258
页数:8
相关论文
共 50 条
  • [41] FORMAL DESIGN VERIFICATION OF SEQUENTIAL-MACHINES BASED ON SYMBOLIC MODEL CHECKING FOR BRANCHING TIME REGULAR TEMPORAL LOGIC
    HAMAGUCHI, K
    HIRAISHI, H
    YAJIMA, S
    [J]. IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES, 1992, E75A (10) : 1220 - 1229
  • [42] A Lazy Approach to Temporal Epistemic Logic Model Checking
    Cimatti, Alessandro
    Gario, Marco
    Tonetta, Stefano
    [J]. AAMAS'16: PROCEEDINGS OF THE 2016 INTERNATIONAL CONFERENCE ON AUTONOMOUS AGENTS & MULTIAGENT SYSTEMS, 2016, : 1218 - 1226
  • [43] Model checking for event graphs and event temporal logic
    Xia, Wei
    Yao, Yi-Ping
    Mu, Xiao-Dong
    [J]. Ruan Jian Xue Bao/Journal of Software, 2013, 24 (03): : 421 - 432
  • [44] The Linear Temporal Logic of Rewriting Maude Model Checker
    Bae, Kyungmin
    Meseguer, Jose
    [J]. REWRITING LOGIC AND ITS APPLICATIONS, 2010, 6381 : 208 - 225
  • [45] Model checking of pushdown systems for projection temporal logic
    Zhao, Liang
    Wang, Xiaobing
    Duan, Zhenhua
    [J]. THEORETICAL COMPUTER SCIENCE, 2019, 774 : 82 - 94
  • [46] Optimal Proofs for Linear Temporal Logic on Lasso Words
    Basin, David
    Bhatt, Bhargav Nagaraja
    Traytel, Dmitriy
    [J]. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS (ATVA 2018), 2018, 11138 : 37 - 55
  • [47] Alternating-time temporal logic with resource bounds
    Hoang Nga Nguyen
    Alechina, Natasha
    Logan, Brian
    Rakib, Abdur
    [J]. JOURNAL OF LOGIC AND COMPUTATION, 2018, 28 (04) : 631 - 663
  • [48] Identifying XML Schema Constraints Using Temporal Logic
    Zhao, Ruifang
    Liu, Ke
    Yang, Hongli
    Qiu, Zongyan
    [J]. DEPENDABLE SOFTWARE ENGINEERING: THEORIES, TOOLS, AND APPLICATIONS, 2016, 9984 : 136 - 146
  • [49] Counting Models of Linear-Time Temporal Logic
    Finkbeiner, Bernd
    Torfah, Hazem
    [J]. LANGUAGE AND AUTOMATA THEORY AND APPLICATIONS (LATA 2014), 2014, 8370 : 360 - 371
  • [50] A Theoretic Approach To Translation Of Linear Temporal Logic Into An Automaton
    Zhang, Duo
    Long, Shi Gong
    [J]. 2014 10TH INTERNATIONAL CONFERENCE ON NATURAL COMPUTATION (ICNC), 2014, : 1111 - 1115