Skip to main content
SpringerLink
Log in

Dissimilarity for Linear Dynamical Systems

  • Conference paper
  • First Online:
Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems (QEST+FORMATS 2024)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 14996))

  • 98 Accesses

Abstract

We introduce backward dissimilarity (BD) for discrete-time linear dynamical systems (LDS), which relaxes existing notions of bisimulations by allowing for approximate comparisons. BD is an invariant property stating that the difference along the evolution of the dynamics governing two state variables is bounded by a constant, which we call dissimilarity. We demonstrate the applicability of BD in a simple case study and showcase its use concerning: (i) robust model comparison; (ii) approximate model reduction; and (iii) approximate data recovery. Our main technical contribution is a policy-iteration algorithm to compute BDs. Using a prototype implementation, we apply it to benchmarks from network science and discrete-time Markov chains and compare it against a related notion of bisimulation for linear control systems.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 17159
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 9437
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    The matrix A was obtained by discretizing the original model [24, Eq. 8] with time step \(10^{-2}\) and by additionally perturbing the matrix entries in the order of \(10^{-3}\), to replicate a typical real-case scenario where fragile model symmetries do not occur.

  2. 2.

    The choice of \(\lambda \) is justified by \(\max ( \Vert A \Vert _{\infty } , \Vert B \Vert _{\infty } ) < 1\).

References

  1. Althoff, M.: An introduction to CORA 2015. In: Proceedings of the Workshop on Applied Verification for Continuous and Hybrid Systems (2015)

    Google Scholar 

  2. Antoulas, A.C.: Approximation of Large-Scale Dynamical Systems. SIAM (2005). https://doi.org/10.1137/1.9780898718713

  3. Bacci, G., Bacci, G., Larsen, K.G., Mardare, R.: Converging from branching to linear metrics on Markov chains. Math. Struct. Comput. Sci. 29(1), 3–37 (2019)

    Article  MathSciNet  Google Scholar 

  4. Bacci, G., Bacci, G., Larsen, K.G., Tribastone, M., Tschaikowski, M., Vandin, A.: Efficient local computation of differential bisimulations via coupling and up-to methods. In: 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, 29 June–2 July 2021, pp. 1–14. IEEE (2021). https://doi.org/10.1109/LICS52264.2021.9470555

  5. Bacci, G., Bacci, G., Larsen, K.G., Mardare, R.: On the metric-based approximate minimization of Markov chains. In: ICALP. LIPIcs, vol. 80, pp. 104:1–104:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

    Google Scholar 

  6. Barraud, A.Y.: A numerical algorithm to solve A’XA – X = –Q. In: CDC, pp. 420–423 (1977). https://doi.org/10.1109/CDC.1977.271607

  7. Bartocci, E., Kovács, L., Stankovič, M.: Automatic generation of moment-based invariants for prob-solvable loops. In: Chen, Y.-F., Cheng, C.-H., Esparza, J. (eds.) ATVA 2019. LNCS, vol. 11781, pp. 255–276. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-31784-3_15

    Chapter  Google Scholar 

  8. Boreale, M.: Algebra, coalgebra, and minimization in polynomial differential equations. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 71–87. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54458-7_5

    Chapter  Google Scholar 

  9. Boreale, M.: Algorithms for exact and approximate linear abstractions of polynomial continuous systems. In: Prandini, M., Deshmukh, J.V. (eds.) HSCC, pp. 207–216. ACM (2018) .https://doi.org/10.1145/3178126.3178137

  10. Buchholz, P.: Exact and ordinary lumpability in finite Markov chains. J. Appl. Probab. 31(1), 59–75 (1994)

    Article  MathSciNet  Google Scholar 

  11. Buchholz, P.: Lumpability and nearly-lumpability in hierarchical queueing networks. In: Proceedings of 1995 IEEE International Computer Performance and Dependability Symposium, pp. 82–91. IEEE (1995)

    Google Scholar 

  12. Cardelli, L., Pérez-Verona, I.C., Tribastone, M., Tschaikowski, M., Vandin, A., Waizmann, T.: Exact maximal reduction of stochastic reaction networks by species lumping. Bioinformatics 37(15), 2175–2182 (2021). https://doi.org/10.1093/bioinformatics/btab081

    Article  Google Scholar 

  13. Cardelli, L., Tribastone, M., Tschaikowski, M.: From electric circuits to chemical networks. Natural Comput. (2019) https://doi.org/10.1007/s11047-019-09761-7

  14. Cardelli, L., Tribastone, M., Tschaikowski, M., Vandin, A.: Efficient syntax-driven lumping of differential equations. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 93–111. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9_6

    Chapter  Google Scholar 

  15. Cardelli, L., Tribastone, M., Tschaikowski, M., Vandin, A.: Symbolic computation of differential equivalences. In: POPL (2016)

    Google Scholar 

  16. Cardelli, L., Tribastone, M., Tschaikowski, M., Vandin, A.: ERODE: a tool for the evaluation and reduction of ordinary differential equations. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 310–328. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54580-5_19

    Chapter  Google Scholar 

  17. Cardelli, L., Tribastone, M., Tschaikowski, M., Vandin, A.: Maximal aggregation of polynomial dynamical systems. Proc. Natl. Acad. Sci. (PNAS) 114(38), 10029–10034 (2017)

    Article  Google Scholar 

  18. Cardelli, L., Tribastone, M., Tschaikowski, M., Vandin, A.: Syntactic Markovian bisimulation for chemical reaction networks. In: Aceto, L., Bacci, G., Bacci, G., Ingólfsdóttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools. LNCS, vol. 10460, pp. 466–483. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63121-9_23

    Chapter  Google Scholar 

  19. Cardelli, L., Tribastone, M., Tschaikowski, M., Vandin, A.: Guaranteed error bounds on approximate model abstractions through reachability analysis. In: McIver, A., Horvath, A. (eds.) QEST 2018. LNCS, vol. 11024, pp. 104–121. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-99154-2_7

    Chapter  Google Scholar 

  20. Chen, X., Ábrahám, E., Sankaranarayanan, S.: Taylor model flowpipe construction for non-linear hybrid systems. In: RTSS, pp. 183–192 (2012)

    Google Scholar 

  21. Condon, A.: The complexity of stochastic games. Inf. Comput. 96(2), 203–224 (1992). https://doi.org/10.1016/0890-5401(92)90048-K

    Article  MathSciNet  Google Scholar 

  22. Dantzig, G.B.: Application of the simplex method to a transportation problem. In: Koopmans, T. (ed.) Activity analysis of production and allocation, pp. 359–373. Wiley, New York (1951)

    Google Scholar 

  23. Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled Markov processes. Theor. Comput. Sci. 318(3), 323–354 (2004). https://doi.org/10.1016/j.tcs.2003.09.013

    Article  MathSciNet  Google Scholar 

  24. Fehnker, A., Ivančić, F.: Benchmarks for hybrid systems verification. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 326–341. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24743-2_22

    Chapter  Google Scholar 

  25. Feinberg, M.: Chemical reaction network structure and the stability of complex isothermal reactors—I. The deficiency zero and deficiency one theorems. Chem. Eng. Sci. 42(10), 2229–2268 (1987).https://doi.org/10.1016/0009-2509(87)80099-4. https://www.sciencedirect.com/science/article/pii/0009250987800994

  26. Ford, L.R., Fulkerson, D.R.: Solving the transportation problem. Manag. Sci. 3(1), 24–32 (1956)

    Article  Google Scholar 

  27. Franceschinis, G., Muntz, R.R.: Bounds for quasi-lumpable Markov chains. Perform. Eval. 20(1–3), 223–243 (1994)

    Article  Google Scholar 

  28. Gast, N., Bortolussi, L., Tribastone, M.: Size expansions of mean field approximation: transient and steady-state analysis. ACM SIGMETRICS Perform. Eval. Rev. 46(3), 25–26 (2019)

    Article  Google Scholar 

  29. Ghorbal, K., Goubault, E., Putot, S.: The zonotope abstract domain taylor1+. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 627–633. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02658-4_47

    Chapter  Google Scholar 

  30. Ghorbal, K., Platzer, A.: Characterizing algebraic invariants by differential radical invariants. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 279–294. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_19

    Chapter  Google Scholar 

  31. Giacalone, A., Jou, C.C., Smolka, S.A.: Algebraic reasoning for probabilistic concurrent games. In: IFIP WG 2.2/2.3, pp. 443–458 (1990)

    Google Scholar 

  32. Girard, A., Pappas, G.: Approximate bisimulations for constrained linear systems. In: 44th IEEE Conference on Decision and Control, pp. 4700–4705 (2005). https://doi.org/10.1109/CDC.2005.1582904

  33. Girard, A., Pappas, G.: Approximate bisimulations for nonlinear dynamical systems. In: 44th IEEE Conference on Decision and Control, pp. 684–689 (2005). https://doi.org/10.1109/CDC.2005.1582235

  34. Girard, A., Pappas, G.J.: Approximation metrics for discrete and continuous systems. IEEE Trans. Autom. Control 52(5), 782–798 (2007). https://doi.org/10.1109/TAC.2007.895849

    Article  MathSciNet  Google Scholar 

  35. Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The quantitative verification benchmark set. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 344–350. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17462-0_20

    Chapter  Google Scholar 

  36. Hasani, R., et al.: Closed-form continuous-depth models. arXiv preprint arXiv:2106.13898 (2021)

  37. Islam, M.A., et al.: Model-order reduction of ion channel dynamics using approximate bisimulation. Theor. Comput. Sci. 599, 34–46 (2015). https://doi.org/10.1016/j.tcs.2014.03.018

    Article  MathSciNet  Google Scholar 

  38. Katoen, J.-P., Kemna, T., Zapreev, I., Jansen, D.N.: Bisimulation minimisation mostly speeds up probabilistic model checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 87–101. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71209-1_9

    Chapter  Google Scholar 

  39. Kori, M., Ascari, F., Bonchi, F., Bruni, R., Gori, R., Hasuo, I.: Exploiting adjoints in property directed reachability analysis. In: Enea, C., Lal, A. (eds.) CAV 2023, Part II. LNCS, vol. 13965, pp. 41–63. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-37703-7_3

    Chapter  Google Scholar 

  40. Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1–28 (1991)

    Article  MathSciNet  Google Scholar 

  41. Leontief, W.: Input-Output Economics. OUP E-Books, Oxford University Press (1986)

    Google Scholar 

  42. Liberzon, D.: Calculus of Variations and Optimal Control Theory: A Concise Introduction. Princeton University Press, Princeton (2011)

    Book  Google Scholar 

  43. Liu, J., Zhan, N., Zhao, H.: Computing semi-algebraic invariants for polynomial dynamical systems. In: EMSOFT, pp. 97–106 (2011)

    Google Scholar 

  44. Liu, Y.Y., Slotine, J.J., Barabasi, A.L.: Controllability of complex networks. Nature 473, 167–73 (2011). https://doi.org/10.1038/nature10011

    Article  Google Scholar 

  45. Marin, A., Rossi, S.: On the relations between lumpability and reversibility. In: MASCOTS, pp. 427–432 (2014). https://doi.org/10.1109/MASCOTS.2014.59

  46. De Nicola, R., Montanari, U., Vaandrager, F.: Back and forth bisimulations. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 152–165. Springer, Heidelberg (1990). https://doi.org/10.1007/BFb0039058

    Chapter  Google Scholar 

  47. Orlin, J.: A faster strongly polynomial minimum cost flow algorithm. In: STOC, pp. 377–387 (1988)

    Google Scholar 

  48. Peixoto, T.P.: The Netzschleuder network catalogue and repository (2020). https://doi.org/10.5281/zenodo.7839981

  49. Perron, L., Furnon, V.: Or-tools. https://developers.google.com/optimization/

  50. Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics, Wiley, Hoboken (1994). https://doi.org/10.1002/9780470316887

    Book  Google Scholar 

  51. Salamati, M., Soudjani, S., Majumdar, R.: Approximate time bounded reachability for CTMCs and CTMDPs: a Lyapunov approach. In: McIver, A., Horvath, A. (eds.) QEST 2018. LNCS, vol. 11024, pp. 389–406. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-99154-2_24

    Chapter  Google Scholar 

  52. Sankaranarayanan, S., Dang, T., Ivančić, F.: Symbolic model checking of hybrid systems using template polyhedra. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 188–202. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_14

    Chapter  Google Scholar 

  53. Song, L., Zhang, L., Godskesen, J.C.: Bisimulations and logical characterizations on continuous-time Markov decision processes. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 98–117. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54013-4_6

    Chapter  Google Scholar 

  54. Tognazzi, S., Tribastone, M., Tschaikowski, M., Vandin, A.: EGAC: a genetic algorithm to compare chemical reaction networks. In: Genetic and Evolutionary Computation Conference, GECCO, pp. 833–840 (2017). https://doi.org/10.1145/3071178.3071265

  55. Tribastone, M., Mayer, P., Wirsing, M.: Performance prediction of service-oriented systems with layered queueing networks. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010. LNCS, vol. 6416, pp. 51–65. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16561-0_12

    Chapter  Google Scholar 

  56. Tschaikowski, M., Tribastone, M.: Tackling continuous state-space explosion in a Markovian process algebra. Theor. Comput. Sci. 517, 1–33 (2014). https://doi.org/10.1016/j.tcs.2013.08.016

    Article  MathSciNet  Google Scholar 

  57. Tschaikowski, M., Tribastone, M.: Approximate reduction of heterogenous nonlinear models with differential hulls. IEEE Trans. Autom. Control 61(4), 1099–1104 (2016). https://doi.org/10.1109/TAC.2015.2457172

    Article  MathSciNet  Google Scholar 

  58. Tschaikowski, M., Tribastone, M.: Spatial fluid limits for stochastic mobile networks. J. Perform. Eval. 109, 52–76 (2017). https://doi.org/10.1016/j.peva.2016.12.005

    Article  Google Scholar 

  59. Vaidya, P.M.: Speeding-up linear programming using fast matrix multiplication (extended abstract). In: 30th Annual Symposium on Foundations of Computer Science, Research Triangle Park, North Carolina, USA, 30 October–1 November 1989, pp. 332–337. IEEE Computer Society (1989). https://doi.org/10.1109/SFCS.1989.63499

  60. Wirsing, M., et al.: Sensoria patterns: augmenting service engineering with formal analysis, transformation and dynamicity. In: Margaria, T., Steffen, B. (eds.) ISoLA 2008. CCIS, vol. 17, pp. 170–190. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-88479-8_13

    Chapter  Google Scholar 

Download references

Acknowledgments

This work was partially supported by Poul Due Jensen Foundation grant no. 883901; the S40S Villum Investigator Grant nr. 37819 from Villum Fonden, the Fsc regional Tuscan project AUTOXAI2 J53D21003810008, the project SERICS (PE00000014) and the Tuscany Health Ecosystem (THE) project with CUP B83C22003920001, under the MUR National Recovery and Resilience Plan funded by the European Union - NextGenerationEU.

Author information

Authors and Affiliations

  1. Computer Science Department, Aalborg University, Aalborg, Denmark

    Giorgio Bacci, Giovanni Bacci, Kim Guldstrand Larsen & Max Tschaikowski

  2. SysMA Unit, IMT Lucca, Lucca, Italy

    Giuseppe Squillace & Mirco Tribastone

  3. Sant’Anna School of Advanced Studies, Pisa, Italy

    Andrea Vandin

  4. DTU Denmark, Copenhagen, Denmark

    Andrea Vandin

Authors
  1. Giorgio Bacci
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Giovanni Bacci
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Kim Guldstrand Larsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Giuseppe Squillace
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Mirco Tribastone
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Max Tschaikowski
    View author publications

    You can also search for this author in PubMed Google Scholar

  7. Andrea Vandin
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Giorgio Bacci .

Editor information

Editors and Affiliations

  1. University of Edinburgh, Edinburgh, UK

    Jane Hillston

  2. Max Planck Institute for Software Systems, Saarbrücken, Germany

    Sadegh Soudjani

  3. Kyoto University, Kyoto, Japan

    Masaki Waga

Rights and permissions

Reprints and permissions

Copyright information

© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Bacci, G. et al. (2024). Dissimilarity for Linear Dynamical Systems. In: Hillston, J., Soudjani, S., Waga, M. (eds) Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems. QEST+FORMATS 2024. Lecture Notes in Computer Science, vol 14996. Springer, Cham. https://doi.org/10.1007/978-3-031-68416-6_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-68416-6_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-68415-9

  • Online ISBN: 978-3-031-68416-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation