research-article

Abstraction, discretization, and robustness in temporal logic control of dynamical systems

Authors:

Necmiye OzayAuthors Info & Claims

HSCC '14: Proceedings of the 17th international conference on Hybrid systems: computation and control

Pages 293 - 302

https://doi.org/10.1145/2562059.2562137

Published: 15 April 2014 Publication History

Abstract

Abstraction-based, hierarchical approaches to control synthesis from temporal logic specifications for dynamical systems have gained increased popularity over the last decade. Yet various issues commonly encountered and extensively dealt with in control systems have not been adequately discussed in the context of temporal logic control of dynamical systems, such as inter-sample behaviors of a sampled-data system, effects of imperfect state measurements and un-modeled dynamics, and the use of time-discretized models to design controllers for continuous-time dynamical systems. We discuss these issues in this paper. The main motivation is to demonstrate the possibility of accounting for the mismatches between a continuous-time control system and its various types of abstract models used for control synthesis. We do this by incorporating additional robustness measures in the abstract models. Such robustness measures are gained at the price of either increased non-determinism in the abstracted models or relaxed versions of the specification being realized. Under a unified notion of abstraction, we provide concrete means of incorporating these robustness measures and establish results that demonstrate their effectiveness in dealing with the above mentioned issues.

References

[1]

R. Alur, T. A. Henzinger, O. Kupferman, and M. Y. Vardi. Alternating refinement relations. In Proc. International Conference on Concurrency Theory (CONCUR), pages 163--178, 1998.

Digital Library

[2]

D. Angeli. A Lyapunov approach to incremental stability properties. IEEE Trans. on Automatic Control, 47(3):410--421, 2002.

[3]

G. E. Fainekos, A. Girard, H. Kress-Gazit, and G. J. Pappas. Temporal logic motion planning for dynamic robots. Automatica, 45:343--352, 2009.

Digital Library

[4]

G. E. Fainekos and G. J. Pappas. Robustness of temporal logic specifications for continuous-time signals. Theoretical Computer Science, 410(42):4262--4291, 2009.

Digital Library

[5]

G. F. Franklin, M. L. Workman, and D. Powell. Digital Control of Dynamic Systems. Addison-Wesley Longman Publishing Co., Inc., 1997.

Digital Library

[6]

A. Girard and G. Pappas. Approximation metrics for discrete and continuous systems. IEEE Trans. on Automatic Control, 52:782--798, 2007.

[7]

S. Karaman and E. Frazzoli. Sampling-based algorithms for optimal motion planning with deterministic μ-calculus specifications. In Proc. of American Control Conference (ACC), pages 735--742, 2012.

[8]

M. Kloetzer and C. Belta. A fully automated framework for control of linear systems from temporal logic specifications. IEEE Trans. Automatic Control, 53:287--297, 2008.

[9]

H. Kress-Gazit, G. E. Fainekos, and G. J. Pappas. Temporal-logic-based reactive mission and motion planning. IEEE Trans. Robotics, 25:1370--1381, 2009.

Digital Library

[10]

D. Liberzon. Limited-information control of hybrid systems via reachable set propagation. In Proc. of the 16th International Conference on Hybrid Systems: Computation and Control (HSCC), pages 11--20, 2013.

Digital Library

[11]

J. Liu, N. Ozay, U. Topcu, and R. Murray. Synthesis of reactive switching protocols from temporal logic specifications. IEEE Trans. on Automatic Control, 58(7):1771--1785, 2013.

[12]

J. Liu, U. Topcu, N. Ozay, and R. M. Murray. Reactive controllers for differentially flat systems with temporal logic constraints. In Proc. of the 51st IEEE Conference on Decision and Control (CDC), pages 7664--7670, 2012.

[13]

R. Majumdar, E. Render, and P. Tabuada. Robust discrete synthesis against unspecified disturbances. In Proc. of the 14th International Conference on Hybrid Systems: Computation and Control (HSCC), pages 211--220, 2011.

Digital Library

[14]

O. Mickelin, N. Ozay, and R. M. Murray. Synthesis of correct-by-construction control protocols for hybrid systems using partial state information. In Proc. of American Control Conference (ACC), 2014.

[15]

S. Mouelhi, A. Girard, and G. Gössler. Cosyma: a tool for controller synthesis using multi-scale abstractions. In Proc. of the 16th International Conference on Hybrid Systems: Computation and Control (HSCC), pages 83--88, 2013.

Digital Library

[16]

G. Orosz and S. P. Shah. A nonlinear modeling framework for autonomous cruise control. In Proc. of ASME Annual Dynamic Systems and Control Conference joint with JSME Motion & Vibration Conference, pages 467--471, 2012.

[17]

N. Ozay, J. Liu, P. Prabhakar, and R. M. Murray. Computing augmented finite transition systems to synthesize switching protocols for polynomial switched systems. In Proc. of American Control Conference (ACC), 2013.

[18]

G. Pola, P. Pepe, M. D. Di Benedetto, and P. Tabuada. Symbolic models for nonlinear time-delay systems using approximate bisimulations. Systems & Control Letters, 59(6):365--373, 2010.

[19]

G. Pola and P. Tabuada. Symbolic models for nonlinear control systems: Alternating approximate bisimulations. SIAM J. Control Optim., 48:719--733, 2009.

Digital Library

[20]

G. Reiszig. Computing abstractions of nonlinear systems. IEEE Trans. Automatic Control, 56:2583--2598, 2011.

[21]

P. Tabuada. Verification and Control of Hybrid Systems: A Symbolic Approach. Springer, 2009.

Digital Library

[22]

P. Tabuada and G. J. Pappas. Linear time logic control of discrete-time linear systems. IEEE Trans. Automatic Control, 51:1862--1877, 2006.

[23]

Y. Tazaki and J. Imura. Discrete abstractions of nonlinear systems based on error propagation analysis. IEEE Trans. Automatic Control, 57:550--564, 2012.

[24]

U. Topcu, N. Ozay, J. Liu, and R. M. Murray. On synthesizing robust discrete controllers under modeling uncertainty. In Proc. of the 15th ACM International Conference on Hybrid Systems: Computation and Control (HSCC), pages 85--94, 2012.

Digital Library

[25]

E. M. Wolff and R. M. Murray. Optimal control of nonlinear systems with temporal logic specifications. In Proc. of the International Symposium on Robotics Research (ISRR), 2013.

[26]

T. Wongpiromsarn, U. Topcu, and R. M. Murray. Receding horizon temporal logic planning. IEEE Trans. Automatic Control, 57:2817--2830, 2012.

[27]

T. Wongpiromsarn, U. Topcu, N. Ozay, H. Xu, and R. M. Murray. TuLiP: a software toolbox for receding horizon temporal logic planning. In Proc. of the 14th International Conference on Hybrid Systems: Computation and Control (HSCC), 2011.

Digital Library

[28]

M. Zamani, G. Pola, M. Mazo Jr, and P. Tabuada. Symbolic models for nonlinear control systems without stability assumptions. IEEE Trans. Automatic Control, 57:1804--1809, 2012.

Cited By

Baxevani KTanner H(2023)Multi-behavioral Multi-Robot Systems driven by Motivation Dynamics2023 American Control Conference (ACC)10.23919/ACC55779.2023.10156084(1467-1472)Online publication date: 31-May-2023
https://doi.org/10.23919/ACC55779.2023.10156084
Zhao YLi YSentis LTopcu ULiu J(2022)Reactive task and motion planning for robust whole-body dynamic locomotion in constrained environmentsThe International Journal of Robotics Research10.1177/0278364922107771441:8(812-847)Online publication date: 25-May-2022
https://doi.org/10.1177/02783649221077714
Badithela AWongpiromsarn TMurray R(2021)Leveraging Classification Metrics for Quantitative System-Level Analysis with Temporal Logic Specifications2021 60th IEEE Conference on Decision and Control (CDC)10.1109/CDC45484.2021.9683611(564-571)Online publication date: 14-Dec-2021
https://doi.org/10.1109/CDC45484.2021.9683611
Show More Cited By

Index Terms

Abstraction, discretization, and robustness in temporal logic control of dynamical systems

Recommendations

Robust Abstractions for Control Synthesis: Completeness via Robustness for Linear-Time Properties
HSCC '17: Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control

We define robust abstractions for synthesizing provably correct and robust controllers for (possibly infinite) uncertain transition systems. It is shown that robust abstractions are sound in the sense that they preserve robust satisfaction of linear-...
Supervisory Control of Discrete Event Systems with CTL* Temporal Logic Specifications

The supervisory control problem of discrete event systems with temporal logic specifications is studied. The full branching time logic of CTL* is used for expressing specifications of discrete event systems. The control problem of CTL* is reduced to the ...
Robust Alternating-Time Temporal Logic
Logics in Artificial Intelligence
Abstract
In multi-agent system design, a crucial aspect is to ensure robustness, meaning that for a coalition of agents A, small violations of adversarial assumptions only lead to small violations of A’s goals. In this paper we introduce a logical ... $^{}$ $^{}$ $^{}$ $^{}$

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

HSCC '14: Proceedings of the 17th international conference on Hybrid systems: computation and control

April 2014

328 pages

ISBN:9781450327329

DOI:10.1145/2562059

Program Chairs:
Martin Fráänzle
Carl von Ossietziky Universität Oldenburg, Germany
,
John Lygeros
ETH Zurich, Switzerland

Copyright © 2014 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 the author(s) 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: 15 April 2014

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

HSCC'14

Sponsor:

SIGBED

HSCC'14: 17th International Conference on Hybrid Systems: Computation and Control

April 15 - 17, 2014

Berlin, Germany

Acceptance Rates

HSCC '14 Paper Acceptance Rate 29 of 69 submissions, 42%;

Overall Acceptance Rate 153 of 373 submissions, 41%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

39
Total Citations
View Citations
323
Total Downloads

Downloads (Last 12 months)13
Downloads (Last 6 weeks)3

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Baxevani KTanner H(2023)Multi-behavioral Multi-Robot Systems driven by Motivation Dynamics2023 American Control Conference (ACC)10.23919/ACC55779.2023.10156084(1467-1472)Online publication date: 31-May-2023
https://doi.org/10.23919/ACC55779.2023.10156084
Zhao YLi YSentis LTopcu ULiu J(2022)Reactive task and motion planning for robust whole-body dynamic locomotion in constrained environmentsThe International Journal of Robotics Research10.1177/0278364922107771441:8(812-847)Online publication date: 25-May-2022
https://doi.org/10.1177/02783649221077714
Badithela AWongpiromsarn TMurray R(2021)Leveraging Classification Metrics for Quantitative System-Level Analysis with Temporal Logic Specifications2021 60th IEEE Conference on Decision and Control (CDC)10.1109/CDC45484.2021.9683611(564-571)Online publication date: 14-Dec-2021
https://doi.org/10.1109/CDC45484.2021.9683611
Tajvar PMeyer PTumova J(2021)Closed-loop incremental stability for efficient symbolic control of non-linear systemsIFAC-PapersOnLine10.1016/j.ifacol.2021.08.48554:5(121-126)Online publication date: 2021
https://doi.org/10.1016/j.ifacol.2021.08.485
Prabhakar PLiu J(2021)Simulation Relations for Abstraction-based Robust Control of Hybrid Dynamical SystemsIFAC-PapersOnLine10.1016/j.ifacol.2021.08.48454:5(115-120)Online publication date: 2021
https://doi.org/10.1016/j.ifacol.2021.08.484
Liu J(2021)Closing the Gap Between Discrete Abstractions and Continuous Control: Completeness via Robustness and ControllabilityFormal Modeling and Analysis of Timed Systems10.1007/978-3-030-85037-1_5(67-83)Online publication date: 24-Aug-2021
https://dl.acm.org/doi/10.1007/978-3-030-85037-1_5
Kobayashi TSalay RHasuo ICzarnecki KIshikawa FKatsumata S(2021)Robustifying Controller Specifications of Cyber-Physical Systems Against Perceptual UncertaintyNASA Formal Methods10.1007/978-3-030-76384-8_13(198-213)Online publication date: 19-May-2021
https://doi.org/10.1007/978-3-030-76384-8_13
He BLee JTopcu USentis L(2020)BP-RRT: Barrier Pair Synthesis for Temporal Logic Motion Planning2020 59th IEEE Conference on Decision and Control (CDC)10.1109/CDC42340.2020.9304240(1404-1409)Online publication date: 14-Dec-2020
https://doi.org/10.1109/CDC42340.2020.9304240
Beneš NBrim LDražanová JPastva SŠafránek DOzay NPrabhakar P(2019)Facetal abstraction for non-linear dynamical systems based on δ-decidable SMTProceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control10.1145/3302504.3311793(99-108)Online publication date: 16-Apr-2019
https://dl.acm.org/doi/10.1145/3302504.3311793
Mallik KSchmuck ASoudjani SMajumdar R(2019)Compositional Synthesis of Finite-State AbstractionsIEEE Transactions on Automatic Control10.1109/TAC.2018.286974064:6(2629-2636)Online publication date: Jun-2019
https://doi.org/10.1109/TAC.2018.2869740
Show More Cited By

View Options

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

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents