Constructing MDP Abstractions Using Data With Formal Guarantees

被引:8
|
作者
Lavaei, Abolfazl [1 ]
Soudjani, Sadegh [2 ]
Frazzoli, Emilio [1 ]
Zamani, Majid [3 ,4 ]
机构
[1] Swiss Fed Inst Technol, Inst Dynam Syst & Control, CH-8092 Zurich, Switzerland
[2] Newcastle Univ, Sch Comp, Newcastle Upon Tyne NE4 5TG, Tyne & Wear, England
[3] Univ Colorado, Comp Sci Dept, Boulder, CO 80309 USA
[4] Ludwig Maximilians Univ Munchen, Dept Comp Sci, D-80539 Munich, Germany
来源
基金
瑞士国家科学基金会; 英国工程与自然科学研究理事会;
关键词
Stochastic processes; Trajectory; Control systems; Stochastic systems; Probabilistic logic; Markov processes; Picture archiving and communication systems; Data-driven synthesis; MDP abstractions; stochastic bisimulation functions; formal guarantees; STOCHASTIC-SYSTEMS; VERIFICATION; SAFETY;
D O I
10.1109/LCSYS.2022.3188535
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
This letter is concerned with a data-driven technique for constructing finite Markov decision processes (MDPs) as finite abstractions of discrete-time stochastic control systems with unknown dynamics while providing formal closeness guarantees. The proposed scheme is based on notions of stochastic bisimulation functions (SBF) to capture the probabilistic distance between state trajectories of an unknown stochastic system and those of finite MDP. In our proposed setting, we first reformulate corresponding conditions of SBF as a robust convex program (RCP). We then propose a scenario convex program (SCP) associated to the original RCP by collecting a finite number of data from trajectories of the system. We ultimately construct an SBF between the data-driven finite MDP and the unknown stochastic system with a given confidence level by establishing a probabilistic relation between optimal values of the SCP and the RCP. We also propose two different approaches for the construction of finite MDPs from data. We illustrate the efficacy of our results over a nonlinear jet engine compressor with unknown dynamics. We construct a data-driven finite MDP as a suitable substitute of the original system to synthesize controllers maintaining the system in a safe set with some probability of satisfaction and a desirable confidence level.
引用
收藏
页码:460 / 465
页数:6
相关论文
共 50 条
  • [11] Formal Abstractions for Packet Scheduling
    Mohan, Anshuman
    Liu, Yunhe
    Foster, Nate
    Kappe, Tobias
    Kozen, Dexter
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2023, 7 (OOPSLA): : 1338 - 1362
  • [12] Formal Guarantees in Data-Driven Model Identification and Control Synthesis
    Sadraddini, Sadra
    Belta, Calin
    HSCC 2018: PROCEEDINGS OF THE 21ST INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL (PART OF CPS WEEK), 2018, : 147 - 156
  • [13] Formal architectural abstractions for interactive software
    Markopoulos, P
    Johnson, P
    Rowson, J
    INTERNATIONAL JOURNAL OF HUMAN-COMPUTER STUDIES, 1998, 49 (05) : 675 - 715
  • [14] Integrating formal methods by unifying abstractions
    Boute, R
    INTEGRATED FORMAL METHODS, PROCEEDINGS, 2004, 2999 : 441 - 460
  • [15] Keys in formal verification: Abstractions for progress
    Pnueli, A
    ENGINEERING THEORIES OF SOFTWARE INTENSIVE SYSTEMS, 2005, 195 : 177 - 213
  • [16] On using data abstractions for model checking refinements
    Derrick, John
    Wehrheim, Heike
    ACTA INFORMATICA, 2007, 44 (01) : 41 - 71
  • [17] On using data abstractions for model checking refinements
    John Derrick
    Heike Wehrheim
    Acta Informatica, 2007, 44 : 41 - 71
  • [18] DATA ABSTRACTIONS
    CRARY, F
    IEEE SOFTWARE, 1989, 6 (02) : 4 - 4
  • [19] PROTECTION IN DATA TYPE ABSTRACTIONS USING CONSTRAINTS ON DATA VALUES
    SHORT, KW
    COMPUTER JOURNAL, 1981, 24 (02): : 118 - 124
  • [20] CONSTRUCTING ABSTRACTIONS FOR OBJECT-ORIENTED APPLICATIONS
    CUNNINGHAM, W
    BECK, K
    JOURNAL OF OBJECT-ORIENTED PROGRAMMING, 1989, 2 (02): : 17 - 19