Computing Distances between Reach Flowpipes

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.
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.
5. S. Basu, R. Pollack, and M.F. Roy. Algorithms in Real Algebraic Geometry. Springer-Verlag, 2006.
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.
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.
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.
11. A. Girard. Reachability of uncertain linear systems using zonotopes. In HSCC 2005, LNCS 3414, pages 291--305. Springer, 2005.
12. A. Girard and C. Le Guernic. Zonotope/hyperplane intersection for hybrid systems reachability analysis. In HSCC, LNCS 4981, pages 215--228. Springer, 2008.
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.
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.
17. A. B. Kurzhanski and P. Varaiya. Ellipsoidal techniques for reachability under state constraints. SIAM J. Contr. & Optim., 45(4):1369--1394, 2006.
18. R. Majumdar and V. S. Prabhu. Computing the Skorokhod distance between polygonal traces. In HSCC 2015, pages 199--208. ACM, 2015.
19. R. Majumdar and V.S. Prabhu. Computing distances between reach flowpipes. CoRR, 1602.03266, 2016.
20. P. Prabhakar and M. Viswanathan. A dynamic algorithm for approximate flow computations. In HSCC 2011, pages 133--142. ACM, 2011.
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

Index Terms

• Computer systems organization

  • Embedded and cyber-physical systems

• Theory of computation

  • Randomness, geometry and discrete structures

    • Computational geometry