research-article

Efficient finite abstraction of mixed monotone systems

Authors:

Murat ArcakAuthors Info & Claims

HSCC '15: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control

Pages 58 - 67

https://doi.org/10.1145/2728606.2728607

Published: 14 April 2015 Publication History

Abstract

We present an efficient computational procedure for finite abstraction of discrete-time mixed monotone systems by considering a rectangular partition of the state space. Mixed monotone systems are decomposable into increasing and decreasing components, and significantly generalize the well known class of monotone systems. We tightly overapproximate the one-step reachable set from a box of initial conditions by computing a decomposition function at only two points, regardless of the dimension of the state space. We apply our results to verify the dynamical behavior of a model for insect population dynamics and to synthesize a signaling strategy for a traffic network.

References

[1]

M. W. Hirsch, "Systems of differential equations that are competitive or cooperative II: Convergence almost everywhere," SIAM Journal on Mathematical Analysis, vol. 16, no. 3, pp. 423--439, 1985.

Digital Library

[2]

H. L. Smith, Monotone dynamical systems: An introduction to the theory of competitive and cooperative systems. American Math. Soc., 1995.

[3]

M. Hirsch and H. Smith, "Monotone maps: a review," Journal of Difference Equations and Applications, vol. 11, no. 4--5, pp. 379--398, 2005.

[4]

D. Angeli and E. Sontag, "Monotone control systems," IEEE Transactions on Automatic Control, vol. 48, no. 10, pp. 1684--1698, 2003.

[5]

J. Gouzé and K. Hadeler, "Monotone flows and order intervals," Nonlinear World, vol. 1, pp. 23--34, 1994.

[6]

H. Smith, "The discrete dynamics of monotonically decomposable maps," Journal of Mathematical Biology, vol. 53, no. 4, pp. 747--758, 2006.

[7]

H. Smith, "Global stability for mixed monotone systems," Journal of Difference Equations and Applications, vol. 14, no. 10--11, pp. 1159--1164, 2008.

[8]

G. Enciso, H. Smith, and E. Sontag, "Nonmonotone systems decomposable into monotone systems with negative feedback," Journal of Differential Equations, vol. 224, no. 1, pp. 205--227, 2006.

[9]

R. Alur, T. A. Henzinger, G. Lafferriere, and G. J. Pappas, "Discrete abstractions of hybrid systems," Proceedings of the IEEE, vol. 88, no. 7, pp. 971--984, 2000.

[10]

A. Tiwari and G. Khanna, "Series of abstractions for hybrid automata," in Hybrid Systems: Computation and Control, pp. 465--478, Springer, 2002.

Digital Library

[11]

P. Tabuada, Verification and control of hybrid systems: a symbolic approach. Springer, 2009.

[12]

T. Wongpiromsarn, U. Topcu, and R. Murray, "Receding horizon temporal logic planning," IEEE Transactions on Automatic Control, vol. 57, pp. 2817--2830, Nov 2012.

[13]

J. Liu, N. Ozay, U. Topcu, and R. Murray, "Synthesis of reactive switching protocols from temporal logic specifications," IEEE Transactions on Automatic Control, vol. 58, pp. 1771--1785, July 2013.

[14]

E. M. Clarke, O. Grumberg, and D. A. Peled, Model checking. MIT press, 1999.

Digital Library

[15]

C. Baier and J. Katoen, Principals of Model Checking. MIT Press, 2008.

Digital Library

[16]

T. A. Henzinger, P. W. Kopke, A. Puri, and P. Varaiya, "What's decidable about hybrid automata?," Journal of Computer and System Sciences, vol. 57, no. 1, pp. 94--124, 1998.

Digital Library

[17]

P. Tabuada and G. Pappas, "Linear time logic control of discrete-time linear systems," IEEE Transactions on Automatic Control, vol. 51, no. 12, pp. 1862--1877, 2006.

[18]

A. Girard and G. J. Pappas, "Approximation metrics for discrete and continuous systems," IEEE Transactions on Automatic Control, vol. 52, no. 5, pp. 782--798, 2007.

[19]

A. Girard, G. Pola, and P. Tabuada, "Approximately bisimilar symbolic models for incrementally stable switched systems," IEEE Transactions on Automatic Control, vol. 55, no. 1, pp. 116--126, 2010.

[20]

G. Reißig, "Computing abstractions of nonlinear systems," IEEE Transactions on Automatic Control, vol. 56, no. 11, pp. 2583--2598, 2011.

[21]

B. Yordanov, J. Tůmová, I. Černá, J. Barnat, and C. Belta, "Temporal logic control of discrete-time piecewise affine systems," IEEE Transactions on Automatic Control, vol. 57, no. 6, pp. 1491--1504, 2012.

[22]

D. Adzkiya, B. De Schutter, and A. Abate, "Finite abstractions of max-plus-linear systems," IEEE Transactions on Automatic Control, vol. 58, pp. 3039--3053, Dec 2013.

[23]

T. Moor and J. Raisch, "Abstraction based supervisory controller synthesis for high order monotone continuous systems," in Modelling, Analysis, and Design of Hybrid Systems, pp. 247--265, Springer, 2002.

[24]

D. Gromov and J. Raisch, "Detecting and enforcing monotonicity for hybrid control systems synthesis," in Proc. 2nd IFAC Conf. on Analysis and Design of Hybrid Systems, pp. 7--9, 2006.

[25]

N. Ramdani, N. Meslem, and Y. Candau, "Computing reachable sets for uncertain nonlinear monotone systems," Nonlinear Analysis: Hybrid Systems, vol. 4, no. 2, pp. 263--278, 2010.

[26]

J. M. Cushing, An introduction to structured population dynamics. SIAM, 1998.

[27]

M. Kulenovic and O. Merino, "A global attractivity result for maps with invariant boxes," Discrete and Continuous Dynamical Systems Series B, vol. 6, no. 1, p. 97, 2006.

[28]

D. Peled and T. Wilke, "Stutter-invariant temporal properties are expressible without the next-time operator," Information Processing Letters, vol. 63, no. 5, pp. 243--246, 1997.

Digital Library

[29]

A. Kurzhanskiy and P. Varaiya, "Computation of reach sets for dynamical systems," in The Control Systems Handbook, ch. 29, CRC Press, second ed., 2010.

[30]

R. Costantino, J. Cushing, B. Dennis, and R. A. Desharnais, "Experimentally induced transitions in the dynamic behaviour of insect populations," Nature, vol. 375, no. 6528, pp. 227--230, 1995.

[31]

G. J. Holzmann, "The model checker SPIN," IEEE Transactions on Software Engineering, vol. 23, pp. 279--295, 1997.

Digital Library

[32]

S. Coogan, E. A. Gol, M. Arcak, and C. Belta, "Traffic network control from temporal logic specifications," 2014. arXiv:1408.1437.

[33]

C. F. Daganzo, "The cell transmission model, part II: Network traffic," Transportation Research Part B: Methodological, vol. 29, no. 2, pp. 79--93, 1995.

Cited By

Aminzadeh ASwikir AHaddadin SLavaei A(2024)Compositional Safety Verification of Infinite Networks: A Data-Driven Approach2024 European Control Conference (ECC)10.23919/ECC64448.2024.10591289(545-551)Online publication date: 25-Jun-2024
https://doi.org/10.23919/ECC64448.2024.10591289
Aminzadeh ALavaei A(2024)Compositional Synthesis of Safety Barrier Certificates for Infinite Networks2024 European Control Conference (ECC)10.23919/ECC64448.2024.10591247(1234-1239)Online publication date: 25-Jun-2024
https://doi.org/10.23919/ECC64448.2024.10591247
Abate MMote MDor MKlett CPhillips SLang KTsiotras PFeron ECoogan S(2024)Run Time Assurance for Spacecraft Attitude Control Under Nondeterministic AssumptionsIEEE Transactions on Control Systems Technology10.1109/TCST.2023.334062432:3(862-873)Online publication date: May-2024
https://doi.org/10.1109/TCST.2023.3340624
Show More Cited By

Index Terms

Efficient finite abstraction of mixed monotone systems
1. Computing methodologies
  1. Artificial intelligence
    1. Control methods
      1. Computational control theory
2. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods

Recommendations

Efficient verification for stochastic mixed monotone systems
ICCPS '18: Proceedings of the 9th ACM/IEEE International Conference on Cyber-Physical Systems

We present an efficient computational procedure to perform model checking on discrete-time, mixed monotone stochastic systems subject to an affine random disturbance. Specifically, we exploit the structure of such systems in order to efficiently compute ...
Stability verification for monotone systems using homotopy algorithms

A monotone self-mapping of the nonnegative orthant induces a monotone discrete-time dynamical system which evolves on the same orthant. If with respect to this system the origin is attractive then there must exist points whose image under the monotone ...
Graph-Theoretic Stability Conditions for Metzler Matrices and Monotone Systems

This paper studies the graph-theoretic conditions for stability of positive monotone systems. Using concepts from input-to-state stability and network small-gain theory, we first establish necessary and sufficient conditions for the stability of linear ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

HSCC '15: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control

April 2015

321 pages

ISBN:9781450334334

DOI:10.1145/2728606

Program Chairs:
Antoine Girard
Université Joseph Fourier, Grenoble, France
,
Sriram Sankaranarayanan
University of Colorado at Boulder

Copyright © 2015 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

IEEE-CSS: Control Systems Society
SIGBED: ACM Special Interest Group on Embedded Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 April 2015

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

HSCC '15

Sponsor:

IEEE-CSS
SIGBED

HSCC '15: 18th International Conference on Hybrid Systems: Computation and Control

April 14 - 16, 2015

Washington, Seattle

Acceptance Rates

Overall Acceptance Rate 153 of 373 submissions, 41%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

71
Total Citations
View Citations
455
Total Downloads

Downloads (Last 12 months)45
Downloads (Last 6 weeks)5

Reflects downloads up to 21 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Aminzadeh ASwikir AHaddadin SLavaei A(2024)Compositional Safety Verification of Infinite Networks: A Data-Driven Approach2024 European Control Conference (ECC)10.23919/ECC64448.2024.10591289(545-551)Online publication date: 25-Jun-2024
https://doi.org/10.23919/ECC64448.2024.10591289
Aminzadeh ALavaei A(2024)Compositional Synthesis of Safety Barrier Certificates for Infinite Networks2024 European Control Conference (ECC)10.23919/ECC64448.2024.10591247(1234-1239)Online publication date: 25-Jun-2024
https://doi.org/10.23919/ECC64448.2024.10591247
Abate MMote MDor MKlett CPhillips SLang KTsiotras PFeron ECoogan S(2024)Run Time Assurance for Spacecraft Attitude Control Under Nondeterministic AssumptionsIEEE Transactions on Control Systems Technology10.1109/TCST.2023.334062432:3(862-873)Online publication date: May-2024
https://doi.org/10.1109/TCST.2023.3340624
Ganai MGao SHerbert S(2024)Hamilton-Jacobi Reachability in Reinforcement Learning: A SurveyIEEE Open Journal of Control Systems10.1109/OJCSYS.2024.34491383(310-324)Online publication date: 2024
https://doi.org/10.1109/OJCSYS.2024.3449138
Ding LHashimoto KTakai S(2024)Synthesis of event-triggered controllers for SIRS epidemic modelsNonlinear Analysis: Hybrid Systems10.1016/j.nahs.2023.10143751(101437)Online publication date: Feb-2024
https://doi.org/10.1016/j.nahs.2023.101437
Harapanahalli AJafarpour SCoogan S(2024)immrax: A Parallelizable and Differentiable Toolbox for Interval Analysis and Mixed Monotone Reachability in JAXIFAC-PapersOnLine10.1016/j.ifacol.2024.07.42858:11(75-80)Online publication date: 2024
https://doi.org/10.1016/j.ifacol.2024.07.428
Yen MDullerud GWang Y(2023)Statistical Verification of Traffic Systems with Expected Differential Privacy2023 American Control Conference (ACC)10.23919/ACC55779.2023.10156637(3496-3501)Online publication date: 31-May-2023
https://doi.org/10.23919/ACC55779.2023.10156637
Khajenejad MYong S(2023)Tight Remainder-Form Decomposition Functions With Applications to Constrained Reachability and Guaranteed State EstimationIEEE Transactions on Automatic Control10.1109/TAC.2023.325051568:12(7057-7072)Online publication date: Dec-2023
https://doi.org/10.1109/TAC.2023.3250515
Apaza-Perez WGirard A(2023)Abstraction Refinement for Attractivity Controllers Using Quantitative SynthesisIEEE Transactions on Automatic Control10.1109/TAC.2022.322737168:9(5745-5751)Online publication date: Sep-2023
https://doi.org/10.1109/TAC.2022.3227371
Sinyakov VGirard A(2023)Abstraction of Continuous-Time Systems Based on Feedback Controllers and Mixed MonotonicityIEEE Transactions on Automatic Control10.1109/TAC.2022.320542368:8(4508-4522)Online publication date: Aug-2023
https://doi.org/10.1109/TAC.2022.3205423
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