research-article

Computing Distances between Reach Flowpipes

Authors:

Rupak Majumdar,

Vinayak S. PrabhuAuthors Info & Claims

HSCC '16: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control

Pages 267 - 276

https://doi.org/10.1145/2883817.2883850

Published: 11 April 2016 Publication History

Abstract

We investigate quantifying the difference between two hybrid dynamical systems under noise and initial-state uncertainty. While the set of traces for these systems is infinite, it is possible to symbolically approximate trace sets using \emph{reachpipes} that compute upper and lower bounds on the evolution of the reachable sets with time. We estimate distances between corresponding sets of trajectories of two systems in terms of distances between the reachpipes.

In case of two individual traces, the Skorokhod distance has been proposed as a robust and efficient notion of distance which captures both value and timing distortions. In this paper, we extend the computation of the Skorokhod distance to reachpipes, and provide algorithms to compute upper and lower bounds on the distance between two sets of traces. Our algorithms use new geometric insights that are used to compute the worst-case and best-case distances between two polyhedral sets evolving with time.

References

[1]

H. Abbas, B. Hoxha, G.E. Fainekos, J.V. Deshmukh, J. Kapinski, and K. Ueda. Conformance testing as falsification for cyber-physical systems. CoRR, abs/1401.5200, 2014.

[2]

H. Abbas, H. D. Mittelmann, and G. E. Fainekos. Formal property verification in a conformance testing framework. In MEMOCODE 2014, pages 155--164. IEEE, 2014.

Digital Library

[3]

H. Alt and M. Godau. Computing the Fréchet distance between two polygonal curves. Int. J. Comput. Geometry Appl., 5:75--91, 1995.

[4]

D. Avis, D. Bremner, and R. Seidel. How good are convex hull algorithms? Comput. Geom., 7:265--301, 1997.

Digital Library

[5]

S. Basu, R. Pollack, and M.F. Roy. Algorithms in Real Algebraic Geometry. Springer-Verlag, 2006.

Digital Library

[6]

X. Chen, E. Abrahám, and S. Sankaranarayanan. Taylor model flowpipe construction for non-linear hybrid systems. In RTSS 2012, pages 183--192. IEEE Computer Society, 2012.

Digital Library

[7]

A. Chutinan and B. H. Krogh. Computational techniques for hybrid system verification. IEEE Trans. Automat. Contr., 48(1):64--75, 2003.

[8]

M. Colón and S. Sankaranarayanan. Generalizing the template polyhedral domain. In ESOP 2011, LNCS 6602, pages 176--195. Springer, 2011.

Digital Library

[9]

J. V. Deshmukh, R. Majumdar, and V. S. Prabhu. Quantifying conformance using the Skorokhod metric. In CAV 2015, LNCS 9207, pages 234--250 Part(II). Springer, 2015.

[10]

G. Frehse, C. Le Guernic, A. Donzé, S. Cotton, R. Ray, O. Lebeltel, R. Ripado, A. Girard, T. Dang, and O. Maler. Spaceex: Scalable verification of hybrid systems. In CAV 2011, LNCS 6806, pages 379--395. Springer, 2011.

Digital Library

[11]

A. Girard. Reachability of uncertain linear systems using zonotopes. In HSCC 2005, LNCS 3414, pages 291--305. Springer, 2005.

Digital Library

[12]

A. Girard and C. Le Guernic. Zonotope/hyperplane intersection for hybrid systems reachability analysis. In HSCC, LNCS 4981, pages 215--228. Springer, 2008.

Digital Library

[13]

A. Girard, C. Le Guernic, and O. Maler. Efficient computation of reachable sets of linear time-invariant systems with inputs. In HSCC 2006, LNCS 3927, pages 257--271. Springer, 2006.

Digital Library

[14]

G.M.Ziegler. Lectures on Polytopes. Springer, 1995.

[15]

C. Le Guernic and A. Girard. Reachability analysis of linear systems using support functions. Nonlinear Analysis: Hybrid Systems, 4(2):250--262, 2010.

[16]

Z. Han and B. H. Krogh. Reachability analysis of large-scale affine systems using low-dimensional polytopes. In HSCC 2006, LNCS 3927, pages 287--301. Springer, 2006.

Digital Library

[17]

A. B. Kurzhanski and P. Varaiya. Ellipsoidal techniques for reachability under state constraints. SIAM J. Contr. & Optim., 45(4):1369--1394, 2006.

Digital Library

[18]

R. Majumdar and V. S. Prabhu. Computing the Skorokhod distance between polygonal traces. In HSCC 2015, pages 199--208. ACM, 2015.

Digital Library

[19]

R. Majumdar and V.S. Prabhu. Computing distances between reach flowpipes. CoRR, 1602.03266, 2016.

Digital Library

[20]

P. Prabhakar and M. Viswanathan. A dynamic algorithm for approximate flow computations. In HSCC 2011, pages 133--142. ACM, 2011.

Digital Library

[21]

S. Sankaranarayanan, T. Dang, and F. Ivancic. A policy iteration technique for time elapse over template polyhedra. In HSCC 2008, LNCS 4981, pages 654--657. Springer, 200

Digital Library

Cited By

Ghorbel BPrabhu V(2023)Quantitative Robustness for Signal Temporal Logic With Time-Freeze QuantifiersIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2023.328329642:12(4436-4449)Online publication date: Dec-2023
https://doi.org/10.1109/TCAD.2023.3283296
Roehm HRausch AAlthoff M(2022)Reachset Conformance and Automatic Model Adaptation for Hybrid SystemsMathematics10.3390/math1019356710:19(3567)Online publication date: 29-Sep-2022
https://doi.org/10.3390/math10193567
Prabhu VSavaliya M(2022)Towards Efficient Input Space Exploration for Falsification of Input Signal Class Augmented STL2022 20th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE)10.1109/MEMOCODE57689.2022.9954597(1-11)Online publication date: 13-Oct-2022
https://doi.org/10.1109/MEMOCODE57689.2022.9954597
Show More Cited By

Index Terms

Computing Distances between Reach Flowpipes
1. Computer systems organization
  1. Embedded and cyber-physical systems
2. Theory of computation
  1. Randomness, geometry and discrete structures
    1. Computational geometry

Recommendations

Computing the Skorokhod distance between polygonal traces

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

The Skorokhod distance is a natural metric on traces of continuous and hybrid systems. It measures the best match between two traces, each mapping a time interval [0, T] to a metric space O, when continuous bijective timing distortions are allowed. ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

HSCC '16: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control

April 2016

324 pages

ISBN:9781450339551

DOI:10.1145/2883817

Program Chairs:
Alessandro Abate
University of Oxford, UK
,
Georgios Fainekos
Arizona State University, USA

Copyright © 2016 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: 11 April 2016

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Toyota Motors
FCT

Conference

HSCC'16

Sponsor:

SIGBED

HSCC'16: 19th International Conference on Hybrid Systems: Computation and Control

April 12 - 14, 2016

Vienna, Austria

Acceptance Rates

HSCC '16 Paper Acceptance Rate 28 of 65 submissions, 43%;

Overall Acceptance Rate 153 of 373 submissions, 41%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
75
Total Downloads

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

Reflects downloads up to 05 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Ghorbel BPrabhu V(2023)Quantitative Robustness for Signal Temporal Logic With Time-Freeze QuantifiersIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2023.328329642:12(4436-4449)Online publication date: Dec-2023
https://doi.org/10.1109/TCAD.2023.3283296
Roehm HRausch AAlthoff M(2022)Reachset Conformance and Automatic Model Adaptation for Hybrid SystemsMathematics10.3390/math1019356710:19(3567)Online publication date: 29-Sep-2022
https://doi.org/10.3390/math10193567
Prabhu VSavaliya M(2022)Towards Efficient Input Space Exploration for Falsification of Input Signal Class Augmented STL2022 20th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE)10.1109/MEMOCODE57689.2022.9954597(1-11)Online publication date: 13-Oct-2022
https://doi.org/10.1109/MEMOCODE57689.2022.9954597
Roehm HOehlerking JWoehrle MAlthoff M(2019)Model Conformance for Cyber-Physical SystemsACM Transactions on Cyber-Physical Systems10.1145/33061573:3(1-26)Online publication date: 20-Aug-2019
https://dl.acm.org/doi/10.1145/3306157
Kido KSedwards SHasuo I(2019)Switching Delays and the Skorokhod Distance in Incrementally Stable Switched SystemsCyber Physical Systems. Design, Modeling, and Evaluation10.1007/978-3-030-17910-6_9(109-126)Online publication date: 13-Apr-2019
https://doi.org/10.1007/978-3-030-17910-6_9
Bartocci EDeshmukh JDonzé AFainekos GMaler ONičković DSankaranarayanan S(2018)Specification-Based Monitoring of Cyber-Physical Systems: A Survey on Theory, Tools and ApplicationsLectures on Runtime Verification10.1007/978-3-319-75632-5_5(135-175)Online publication date: 11-Feb-2018
https://doi.org/10.1007/978-3-319-75632-5_5
Majumdar RPrabhu VAbate AFainekos G(2016)Computing Distances between Reach FlowpipesProceedings of the 19th International Conference on Hybrid Systems: Computation and Control10.1145/2883817.2883850(267-276)Online publication date: 11-Apr-2016
https://dl.acm.org/doi/10.1145/2883817.2883850
Xue BShe ZEaswaran A(2016)Under-Approximating Backward Reachable Sets by PolytopesComputer Aided Verification10.1007/978-3-319-41528-4_25(457-476)Online publication date: 13-Jul-2016
https://doi.org/10.1007/978-3-319-41528-4_25

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.

Figures

Tables

Media

View Table of Conten