research-article

Public Access

Formal Guarantees in Data-Driven Model Identification and Control Synthesis

Authors:

Sadra Sadraddini,

Calin BeltaAuthors Info & Claims

HSCC '18: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)

Pages 147 - 156

https://doi.org/10.1145/3178126.3178145

Published: 11 April 2018 Publication History

Abstract

For many performance-critical control systems, an accurate (simple) model is not available in practice. Thus, designing controllers with formal performance guarantees is challenging. In this paper, we develop a framework to use input-output data from an unknown system to synthesize controllers from signal temporal logic (STL) specifications. First, by imposing mild assumptions on system continuity, we find a set-valued piecewise affine (PWA) model that contains all the possible behaviors of the concrete system. Next, we introduce a novel method for STL control of PWA systems with additive disturbances. By taking advantage of STL quantitative semantics, we provide lower-bound certificates on the degree of STL satisfaction of the closed-loop concrete system. Illustrative examples are presented.

References

[1]

Derya Aksaray, Austin Jones, Zhaodan Kong, Mac Schwager, and Calin Belta. 2016. Q-learning for robust satisfaction of signal temporal logic specifications. In Decision and Control (CDC), 2016 IEEE 55th Conference on. IEEE, 6565--6570.

[2]

Mohammed Alshiekh, Roderick Bloem, Ruediger Ehlers, Bettina Könighofer, Scott Niekum, and Ufuk Topcu. 2017. Safe Reinforcement Learning via Shielding. arXiv preprint arXiv.1708.08611 (2017).

[3]

Raieev Alur and Nimit Singhania. 2014. Precise piecewise affine models from input-output data. In Embedded Software (EMSOFT), 2014 International Conference on. IEEE, 1--10.

Digital Library

[4]

Anil Aswani, Humberto Gonzalez, S Shankar Sastry, and Claire Tomlin. 2013. Provably safe and robust learning-based model predictive control. Automatica 49, 5 (2013), 1216--1226.

Digital Library

[5]

Christel Baier and Joost-Pieter Katoen. 2008. Principles of model checking. Vol. 26202649. MIT press Cambridge.

[6]

Grégory Batt, Boyan Yordanov, Ron Weiss, and Calin Belta. 2007. Robustness analysis and tuning of synthetic gene networks. Bioinformatics 23, 18 (2007), 2415--2422.

Digital Library

[7]

Calin Belta, Boyan Yordanov, and Ebru Aydin Gol. 2016. Formal Methods for Discrete-Time Dynamical Systems. Springer.

[8]

A. Bemporad, A. Garulli, S. Paoletti, and A. Vicino. 2005. A bounded-error approach to piecewise affine system identification. IEEE Trans. Automat. Control 50, 10 (Oct 2005), 1567--1580.

[9]

Alberto Bemporad and Manfred Morari. 1999. Control of systems integrating logic, dynamics, and constraints. Automatica 35, 3 (1999), 407--427.

Digital Library

[10]

F. Blanchini. 1999. Set invariance in control-a survey. Automatica 35, 11 (1999), 1747--1767.

Digital Library

[11]

J. P. Calliess. 2017. Lipschitz optimisation for Lipschitz Interpolation. In 2017 American Control Conference (ACC). 3141--3146.

[12]

S. Coogan, E. A. Gol, M. Arcak, and C. Belta. 2016. Traffic Network Control From Temporal Logic Specifications. IEEE Transactions on Control of Network Systems 3, 2 (June 2016), 162--172.

[13]

Samira S Farahani, Vasumathi Raman, and Richard M Murray. 2015. Robust Model Predictive Control for Signal Temporal Logic Synthesis. IFAC-PapersOnLine 48, 27 (2015), 323--328.

[14]

Timothy S Gardner, Charles R Cantor, and James J Collins. 2000. Construction of a genetic toggle switch in Escherichia coli. Nature 403, 6767 (2000), 339.

[15]

Mohammad S Ghasemi and Ali A Afzalian. 2017. Robust tube-based MPC of constrained piecewise affine systems with bounded additive disturbances. Nonlinear Analysis: Hybrid Systems 26 (2017), 86--100.

[16]

Sertac Karaman, Ricardo G. Sanfelice, and Emilio Frazzoli. 2008. Optimalcontrol of Mixed Logical Dynamical systems with Linear Temporal Logic specifications. In 2008 47th IEEE Conference on Decision and Control. IEEE, 2117--2122.

[17]

Oded Maler and Dejan Nickovic. 2004. Monitoring Temporal Properties of Continuous Signals. In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems. Springer, 152- 166.

[18]

David Q Mayne, María M Seron, and SV Raković. 2005. Robust model predictive control of constrained linear systems with bounded disturbances. Automatica 41, 2 (2005), 219--224.

Digital Library

[19]

Mario Milanese and Carlo Novara. 2004. Set membership identification of nonlinear systems. Automatica 40, 6 (2004), 957--975.

Digital Library

[20]

Joël Ouaknine and James Worrell. 2006. Safety metric temporal logic is fully decidable. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 411--425.

Digital Library

[21]

Simone Paoletti, Aleksandar Lj Juloski, Giancarlo Ferrari-Trecate, and René Vidal. 2007. Identification of hybrid systems a tutorial. European journal of control 13, 2-3 (2007), 242--260.

[22]

SV Rakovic, Eric C Kerrigan, David Q Mayne, and Konstantinos I Kouramas. 2007. Optimized robust control invariance for linear discrete-time systems: Theoretical foundations. Automatica 43, 5 (2007), 831--841.

Digital Library

[23]

Sasa V Raković, P Grieder, M Kvasnica, D Q Mayne, and M Morari. 2004. Computation of invariant sets for piecewise affine discrete time systems subject to bounded disturbances. In Decision and Control, 2004. CDC. 43rd IEEE Conference on, Vol. 2. IEEE, 1418--1423.

[24]

Vasumathi Raman, Alexandre Donzé, Mehdi Maasoumy, Richard M Murray, Alberto Sangiovanni-Vincentelli, and Sanjit A Seshia. 2014. Model predictive control with signal temporal logic specifications. In 53rd IEEE Conference on Decision and Control. IEEE, 81--87.

[25]

Vasumathi Raman, Alexandre Donzé, Dorsa Sadigh, Richard M Murray, and Sanjit A Seshia. 2015. Reactive synthesis from signal temporal logic specifications. In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. ACM, 239--248.

Digital Library

[26]

Matthias Rungger, Manuel Mazo, and Paulo Tabuada. 2013. Controller synthesis for linear systems and safe linear-time temporal logic. In Proceedings of the 16th international conference on Hybrid systems: computation and control. ACM, 333--342.

Digital Library

[27]

Dorsa Sadigh, Eric S Kim, Samuel Coogan, S Shankar Sastry, and Sanjit A Seshia. 2014. A learning based approach to control synthesis of markov decision processes for linear temporal logic specifications. In 53rd IEEE Conference on Decision and Control. IEEE, 1091--1096.

[28]

S. Sadraddini and C. Belta. 2015. Robust temporal logic model predictive control. In 2015 53rd Annual Allerton Conference on Communication, Control, and Computing (Allerton). 772--779.

[29]

Sadra Sadraddini and Calin Belta. 2017. Formal Methods for Adaptive Control of Dynamical Systems. In 56th IEEE Conference on Decision and Control (CDC). IEEE, 1782--1787.

[30]

P Tabuada. 2008. Verification and Control of Hybrid Systems. Springer Science & Business Media.

Digital Library

[31]

Paulo Tabuada and George J. Pappas. 2006. Linear time logic control of discrete-time linear systems. IEEE Trans. Automat. Control 51, 12 (2006), 1862--1877.

[32]

C Tomlin, G J Pappas, and S S Sastry. 1998. Conflict resolution for air traffic management: {A} study in multiagent hybrid systems. IEEE Trans. Automat. Control 43, 4 (1998), 509--521.

[33]

Mahdi Yousefi, Klaske van Heusden, Guy A Dumont, and J Mark Ansermino. 2015. Safety-preserving closed-loop control of anesthesia. In Engineering in Medicine and Biology Society (EMBC), 2015 37th Annual International Conference of the IEEE. IEEE, 454--457.

[34]

Majid Zamani, Giordano Pola, Manuel Mazo, and Paulo Tabuada. 2012. Symbolic models for nonlinear control systems without stability assumptions. Automatic Control, IEEE Transactions on 57, 7 (2012), 1804--1809.

Cited By

Qiao JYang SFu A(2025)An intelligent piecewise linear modeling approach from noisy data and its applications to water supply systemInternational Journal of Systems Science10.1080/00207721.2025.2456030(1-14)Online publication date: 24-Jan-2025
https://doi.org/10.1080/00207721.2025.2456030
Badings TRomao LAbate AJansen N(2024)A Stability-Based Abstraction Framework for Reach-Avoid Control of Stochastic Dynamical Systems with Unknown Noise Distributions2024 European Control Conference (ECC)10.23919/ECC64448.2024.10590865(564-570)Online publication date: 25-Jun-2024
https://doi.org/10.23919/ECC64448.2024.10590865
Berger GNarasimhamurthy MSankaranarayanan S(2024)Algorithms for Identifying Flagged and Guarded Linear SystemsProceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control10.1145/3641513.3650140(1-13)Online publication date: 14-May-2024
https://dl.acm.org/doi/10.1145/3641513.3650140
Show More Cited By

Index Terms

Formal Guarantees in Data-Driven Model Identification and Control Synthesis
1. Applied computing
  1. Physical sciences and engineering
    1. Engineering
2. Theory of computation

Recommendations

Relaxed fuzzy control synthesis of nonlinear networked systems under unreliable communication links

HighlightsA novel fuzzy controller and a new kind of slack variable approach are developed.The criterion takes the form of an LMI which is computationally tractable.The obtained stabilization conditions are less conservative. This paper proposes relaxed ...
Relaxed H ∞ control design of discrete-time Takagi-Sugeno fuzzy systems

This paper investigates the problem of fuzzy H ∞ control design for a class of discrete-time nonlinear control systems via a multi-samples approach. A new fuzzy H ∞ controller, which is parameter-dependent on not only the current-time but also the one-...
High-level scheduling model and control synthesis for a broad range of design applications
ICCAD '97: Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design

This paper presents a versatile scheduling model and an efficient control synthesis methodology which enables architectural (high-level) design/synthesis systems to seamlessly support a broad range of architectural design applications from datapath-...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

HSCC '18: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)

April 2018

296 pages

ISBN:9781450356428

DOI:10.1145/3178126

Copyright © 2018 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGBED: ACM Special Interest Group on Embedded Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 April 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Funding Sources

NSF

Conference

HSCC '18

Sponsor:

SIGBED

HSCC '18: 21st International Conference on Hybrid Systems: Computation and Control

April 11 - 13, 2018

Porto, Portugal

Acceptance Rates

Overall Acceptance Rate 153 of 373 submissions, 41%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

41
Total Citations
View Citations
908
Total Downloads

Downloads (Last 12 months)107
Downloads (Last 6 weeks)12

Reflects downloads up to 01 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Qiao JYang SFu A(2025)An intelligent piecewise linear modeling approach from noisy data and its applications to water supply systemInternational Journal of Systems Science10.1080/00207721.2025.2456030(1-14)Online publication date: 24-Jan-2025
https://doi.org/10.1080/00207721.2025.2456030
Badings TRomao LAbate AJansen N(2024)A Stability-Based Abstraction Framework for Reach-Avoid Control of Stochastic Dynamical Systems with Unknown Noise Distributions2024 European Control Conference (ECC)10.23919/ECC64448.2024.10590865(564-570)Online publication date: 25-Jun-2024
https://doi.org/10.23919/ECC64448.2024.10590865
Berger GNarasimhamurthy MSankaranarayanan S(2024)Algorithms for Identifying Flagged and Guarded Linear SystemsProceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control10.1145/3641513.3650140(1-13)Online publication date: 14-May-2024
https://dl.acm.org/doi/10.1145/3641513.3650140
Makdesi AGirard AFribourg L(2024)Data-Driven Models of Monotone SystemsIEEE Transactions on Automatic Control10.1109/TAC.2023.334679369:8(5294-5309)Online publication date: Aug-2024
https://doi.org/10.1109/TAC.2023.3346793
Berger GSankaranarayanan S(2024)Template-based piecewise affine regressionResearch Directions: Cyber-Physical Systems10.1017/cbp.2024.32Online publication date: 6-Nov-2024
https://doi.org/10.1017/cbp.2024.3
Xiao WLi ACassandras CBelta C(2024)Toward model-free safety-critical control with humans in the loopAnnual Reviews in Control10.1016/j.arcontrol.2024.10094457(100944)Online publication date: 2024
https://doi.org/10.1016/j.arcontrol.2024.100944
Liu SSchürmann BAlthoff M(2023)Guarantees for Real Robotic Systems: Unifying Formal Controller Synthesis and Reachset-Conformant IdentificationIEEE Transactions on Robotics10.1109/TRO.2023.327726839:5(3776-3790)Online publication date: Oct-2023
https://doi.org/10.1109/TRO.2023.3277268
Gruber FAlthoff M(2023)Scalable Robust Safety Filter With Unknown Disturbance SetIEEE Transactions on Automatic Control10.1109/TAC.2023.329232968:12(7756-7770)Online publication date: Dec-2023
https://doi.org/10.1109/TAC.2023.3292329
Nejati ALavaei AJagtap PSoudjani SZamani M(2023)Formal Verification of Unknown Discrete- and Continuous-Time Systems: A Data-Driven ApproachIEEE Transactions on Automatic Control10.1109/TAC.2023.325514168:5(3011-3024)Online publication date: May-2023
https://doi.org/10.1109/TAC.2023.3255141
Coppola RPeruffo AMazo M(2023)Data-driven Abstractions for Verification of Linear SystemsIEEE Control Systems Letters10.1109/LCSYS.2023.3288731(1-1)Online publication date: 2023
https://doi.org/10.1109/LCSYS.2023.3288731
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Figures

Tables

Media

View Table of Conten