×

Approximate bisimulation relations for constrained linear systems. (English) Zbl 1130.93365

Summary: We define the notion of approximate bisimulation relation between two continuous systems. While exact bisimulation requires that the observations of two systems are and remain identical, approximate bisimulation allows the observations to be different provided the distance between them remains bounded by some parameter called precision. Approximate bisimulation relations are conveniently defined as level sets of a so-called bisimulation function which can be characterized using Lyapunov-like differential inequalities. For a class of constrained linear systems, we develop computationally effective characterizations of bisimulation functions that can be interpreted in terms of linear matrix inequalities and optimal values of static games. We derive a method to evaluate the precision of the approximate bisimulation relation between a constrained linear system and its projection. This method has been implemented in a Matlab toolbox: MATISSE. An example of use of the toolbox in the context of safety verification is shown.

MSC:

93C05 Linear systems in control theory
93C15 Control/observation systems governed by ordinary differential equations
93B07 Observability
34K35 Control problems for functional-differential equations
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Angeli, D., A Lyapunov approach to incremental stability properties, IEEE Transactions on Automatic Control, 47, 410-422 (2002) · Zbl 1364.93552
[2] Antoulas, A. C.; Sorensen, D. C.; Gugercin, S., A survey of model reduction methods for large-scale systems, Contemporary Mathematics, 280, 193-219 (2000) · Zbl 1048.93014
[3] Asarin, E., Bournez, O., Dang, T., & Maler, O. (2000). Approximate reachability analysis of piecewise linear dynamical systems, In HSCC, Lecture Notes in Computer Science (Vol. 1790) (pp. 21-31). Berlin: Springer.; Asarin, E., Bournez, O., Dang, T., & Maler, O. (2000). Approximate reachability analysis of piecewise linear dynamical systems, In HSCC, Lecture Notes in Computer Science (Vol. 1790) (pp. 21-31). Berlin: Springer. · Zbl 0938.93502
[4] Aubin, J. P. (1991). Viability Theory. Birkhauser, 1991.; Aubin, J. P. (1991). Viability Theory. Birkhauser, 1991. · Zbl 0755.93003
[5] Chutinan, A., & Krogh, B. H. (1999). Verification of polyhedral invariant hybrid automata using polygonal flow pipe approximations. In HSCC, Lecture Notes in Computer Science (Vol. 1569) (pp. 76-90). Berlin: Springer.; Chutinan, A., & Krogh, B. H. (1999). Verification of polyhedral invariant hybrid automata using polygonal flow pipe approximations. In HSCC, Lecture Notes in Computer Science (Vol. 1569) (pp. 76-90). Berlin: Springer. · Zbl 0954.93020
[6] Clarke, E. M.; Grumberg, O.; Peled, D. A., Model checking (2000), MIT Press: MIT Press Cambridge, MA
[7] de Alfaro, L., Faella, M., & Stoelinga, M. (2004). Linear and branching metrics for quantitative transition systems. In ICALP’04, Lecture Notes in Computer Science (Vol. 3142): (pp. 1150-1162). Berlin: Springer.; de Alfaro, L., Faella, M., & Stoelinga, M. (2004). Linear and branching metrics for quantitative transition systems. In ICALP’04, Lecture Notes in Computer Science (Vol. 3142): (pp. 1150-1162). Berlin: Springer. · Zbl 1098.68092
[8] Desharnais, J.; Gupta, V.; Jagadeesan, R.; Panangaden, P., Metrics for labelled markov processes, Theoretical Computer Science, 318, 3, 323-354 (2004) · Zbl 1068.68093
[9] Freeman, R. A.; Kokotovic, P. V., Inverse optimality in robust stabilization, SIAM Journal on Control and Optimization, 34, 4, 1365-1391 (1996) · Zbl 0863.93075
[10] Girard, A. (2005). Reachability of uncertain linear systems using zonotopes. In HSCC, Lecture Notes in Computer Science (Vol. 3414) (pp. 291-305). Berlin: Springer.; Girard, A. (2005). Reachability of uncertain linear systems using zonotopes. In HSCC, Lecture Notes in Computer Science (Vol. 3414) (pp. 291-305). Berlin: Springer. · Zbl 1078.93005
[11] Girard, A., Julius, A. A., & Pappas, G. J. MATISSE (2005). \( \langle\) http://www.seas.upenn.edu/ agirard/Software/MATISSE/\( \rangle \); Girard, A., Julius, A. A., & Pappas, G. J. MATISSE (2005). \( \langle\) http://www.seas.upenn.edu/ agirard/Software/MATISSE/\( \rangle \)
[12] Girard, A., & Pappas, G. J. (2005a). Approximate bisimulations for constrained linear systems. In Proceedings of CDC and ECC (pp. 4700-4705).; Girard, A., & Pappas, G. J. (2005a). Approximate bisimulations for constrained linear systems. In Proceedings of CDC and ECC (pp. 4700-4705).
[13] Girard, A., & Pappas, G. J. (2005b). Approximate bisimulations for nonlinear dynamical systems. In Proceedings of CDC and ECC (pp. 684-689).; Girard, A., & Pappas, G. J. (2005b). Approximate bisimulations for nonlinear dynamical systems. In Proceedings of CDC and ECC (pp. 684-689).
[14] Girard, A.; Pappas, G. J., Approximation metrics for discrete and continuous systems, IEEE Transaction on Automatic Control, 52, 5, 782-793 (2007) · Zbl 1366.93032
[15] Haghverdi, E.; Tabuada, P.; Pappas, G. J., Bisimulation relations for dynamical, control, and hybrid systems, Theoretical Computer Science, 342, 2-3, 229-261 (2005) · Zbl 1077.68062
[16] Han, Z., & Krogh, B. H. (2006). Reachability analysis of large-scale affine systems using low-dimensional polytopes. In HSCC, Lecture Notes in Computer Science (Vol. 3927) (pp. 287-301). Berlin: Springer.; Han, Z., & Krogh, B. H. (2006). Reachability analysis of large-scale affine systems using low-dimensional polytopes. In HSCC, Lecture Notes in Computer Science (Vol. 3927) (pp. 287-301). Berlin: Springer. · Zbl 1178.93025
[17] Kurzhanski, A., & Varaiya, P. (2000). Ellipsoidal techniques for reachability analysis. In HSCC, Lecture Notes in Computer Science (Vol. 1790) Berlin: Springer.; Kurzhanski, A., & Varaiya, P. (2000). Ellipsoidal techniques for reachability analysis. In HSCC, Lecture Notes in Computer Science (Vol. 1790) Berlin: Springer. · Zbl 1031.93014
[18] Kvasnica, M., Grieder, P., & Baotić, M. (2004). Multi-parametric toolbox (MPT). \( \langle\) http://control.ee.ethz.ch/ mpt/\( \rangle \).; Kvasnica, M., Grieder, P., & Baotić, M. (2004). Multi-parametric toolbox (MPT). \( \langle\) http://control.ee.ethz.ch/ mpt/\( \rangle \). · Zbl 1135.93332
[19] Löfberg, J. (2004). YALMIP: a toolbox for modeling and optimization in MATLAB. In Proceedings of CACSD\( \langle\) http://control.ee.ethz.ch/ joloef/yalmip.php \(\rangle \).; Löfberg, J. (2004). YALMIP: a toolbox for modeling and optimization in MATLAB. In Proceedings of CACSD\( \langle\) http://control.ee.ethz.ch/ joloef/yalmip.php \(\rangle \).
[20] Mitchell, I., & Tomlin, C. (2000). Level set methods for computation in hybrid systems. In HSCC, Lecture Notes in Computer Science (Vol. 1790) Berlin: Springer.; Mitchell, I., & Tomlin, C. (2000). Level set methods for computation in hybrid systems. In HSCC, Lecture Notes in Computer Science (Vol. 1790) Berlin: Springer. · Zbl 0952.93006
[21] Pappas, G. J., Bisimilar linear systems, Automatica, 39, 12, 2035-2047 (2003) · Zbl 1045.93033
[22] Pola, G., van der Schaft, A. J., & Di Benedetto, M. D. (2004). Bisimulation theory for switching linear systems. In Proceedings of CDC (pp. 555-569).; Pola, G., van der Schaft, A. J., & Di Benedetto, M. D. (2004). Bisimulation theory for switching linear systems. In Proceedings of CDC (pp. 555-569).
[23] Sastry, S., Nonlinear systems: analysis, stability and control (1999), Springer: Springer Berlin
[24] Sontag, E.; Wang, Y., Lyapunov characterizations of input to output stability, SIAM Journal on Control and Optimization, 39, 226-249 (2001) · Zbl 0968.93076
[25] Sturm, J. F., Using SEDUMI 1.02, a MATLAB toolbox for optimization over symmetric cones, Optimization Methods and Softwares, 11-12, 625-653 (1999) · Zbl 0973.90526
[26] van der Schaft, A., Equivalence of dynamical systems by bisimulation, IEEE Transactions on Automatic Control, 49, 12, 2160-2172 (2004) · Zbl 1365.93212
[27] Wonham, W. M., Linear multivariable control: a geometric approach (1979), Springer: Springer Berlin · Zbl 0393.93024
[28] Yazarel, H., & Pappas, G. J. (2004). Geometric programming relaxations for linear system reachability. In Proceedings of ACC.; Yazarel, H., & Pappas, G. J. (2004). Geometric programming relaxations for linear system reachability. In Proceedings of ACC.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.