Specification Verification and Controller Synthesis Using (γ,δ)-Similarity

被引:0
|
作者
Pirastehzad, Armin [1 ]
van der Schaft, Arjan [1 ]
Besselink, Bart [1 ]
机构
[1] Univ Groningen, Bernoulli Inst Math Comp Sci & Artificial Intelli, NL-9700 AK Groningen, Netherlands
来源
2023 62ND IEEE CONFERENCE ON DECISION AND CONTROL, CDC | 2023年
基金
荷兰研究理事会;
关键词
COMPOSITIONAL ANALYSIS;
D O I
10.1109/CDC49753.2023.10384281
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
We address the problems of specification verification and controller synthesis in the context of (gamma,delta)-similarity, a notion of approximate system comparison that measures to what extent the external behaviors of two potentially non-deterministic systems are similar in an L-2 sense. Expressing specifications in terms of input-output trajectories of a dynamical system, we use (gamma,delta)-similarity to verify whether the external behavior of a system satisfies such specifications in an approximate sense. We characterize this problem as a linear matrix inequality feasibility problem. In case a control system fails to satisfy specifications with a desired accuracy, we synthesize a dynamic controller that enforces specification satisfaction. We characterize the synthesis problem in terms of a bilinear matrix inequality feasibility problem. Aware of the computational costs for solving such problem, we obtain a sufficient condition for the existence of the controller that can be expressed in terms of a linear matrix inequality. Based on this, we propose an algorithm to construct the controller.
引用
收藏
页码:1692 / 1697
页数:6
相关论文
共 50 条
  • [1] Specification, Verification, and Synthesis using Extended State Machines with Callbacks
    Fowze, Farhaan
    Yavuz, Tuba
    2016 ACM/IEEE INTERNATIONAL CONFERENCE ON FORMAL METHODS AND MODELS FOR SYSTEM DESIGN (MEMOCODE), 2016, : 95 - 104
  • [2] Using Computer Algebra techniques for the specification, verification and synthesis of recursive programs
    Popov, Nikolaj
    Jebelean, Tudor
    MATHEMATICS AND COMPUTERS IN SIMULATION, 2009, 79 (08) : 2302 - 2309
  • [3] SPECIFICATION AND VERIFICATION USING DEPENDENT TYPES
    HANNA, FK
    DAECHE, N
    LONGLEY, M
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1990, 16 (09) : 949 - 964
  • [4] An Approach for the Specification, Verification and Synthesis of Secure Systems
    Martinelli, Fabio
    Matteucci, Ilaria
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2007, 168 : 29 - 43
  • [5] Experimental Verification of Control Rules for A Lane-keeping Controller Using Similarity Fuzzy Reasoning
    Nishiyama, Yuka
    Shinomiya, Yuki
    Yamamoto, Toshimi
    Hoshino, Yukinobu
    2020 JOINT 11TH INTERNATIONAL CONFERENCE ON SOFT COMPUTING AND INTELLIGENT SYSTEMS AND 21ST INTERNATIONAL SYMPOSIUM ON ADVANCED INTELLIGENT SYSTEMS (SCIS-ISIS), 2020, : 91 - 94
  • [6] Formal verification of embedded logic controller specification with computer deduction in temporal logic
    Grobelna, Iwona
    PRZEGLAD ELEKTROTECHNICZNY, 2011, 87 (12A): : 47 - 50
  • [7] Requirements engineering and verification using specification animation
    Hazel, D
    Strooper, P
    Traynor, O
    13TH IEEE INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, PROCEEDINGS, 1998, : 302 - 305
  • [8] Specification and verification of media constraints using UPPAAL
    Bowman, H
    Faconti, GP
    Massink, M
    DESIGN, SPECIFICATION AND VERIFICATION OF INTERACTIVE SYSTEMS'98, 1998, : 261 - 277
  • [10] FORMAL HARDWARE SPECIFICATION AND VERIFICATION USING PROLOG
    BREZOCNIK, Z
    HORVAT, B
    MICROPROCESSING AND MICROPROGRAMMING, 1989, 27 (1-5): : 163 - 170