Abstract
Reachability analysis is a fundamental problem for safety verification and falsification of Cyber-Physical Systems (CPS) whose dynamics follow physical laws usually represented as differential equations. In the last two decades, numerous reachability analysis methods and tools have been proposed for a common class of dynamics in CPS known as ordinary differential equations (ODE). However, there is lack of methods dealing with differential algebraic equations (DAE), which is a more general class of dynamics that is widely used to describe a variety of problems from engineering and science, such as multibody mechanics, electrical circuit design, incompressible fluids, molecular dynamics, and chemical process control. Reachability analysis for DAE systems is more complex than ODE systems, especially for high-index DAEs because they contain both a differential part (i.e., ODE) and algebraic constraints (AC). In this paper, we propose a scalable reachability analysis for a class of high-index large linear DAEs. In our approach, a high-index linear DAE is first decoupled into one ODE and one or several AC subsystems based on the well-known Marz decoupling method utilizing admissible projectors. Then, the discrete reachable set of the DAE, represented as a list of star-sets, is computed using simulation. Unlike ODE reachability analysis where the initial condition is freely defined by a user, in DAE cases, the consistency of the initial condition is an essential requirement to guarantee a feasible solution. Therefore, a thorough check for the consistency is invoked before computing the discrete reachable set. Our approach successfully verifies (or falsifies) a wide range of practical, high-index linear DAE systems in which the number of state variables varies from several to thousands.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Althoff, M., Krogh, B.: Reachability analysis of nonlinear differential-algebraic systems. IEEE Trans. Autom. Control 59(2), 371–383 (2014). https://doi.org/10.1109/TAC.2013.2285751
Althoff, M.: An introduction to CORA 2015. In: Proceedings of the Workshop on Applied Verification for Continuous and Hybrid Systems (2015)
Bak, S., Beg, O.A., Bogomolov, S., Johnson, T.T., Nguyen, L.V., Schilling, C.: Hybrid automata: from verification to implementation. Int. J. Softw. Tools Technol. Transf. 21(1), 87–104 (2019). https://doi.org/10.1007/s10009-017-0458-1
Bak, S., Bogomolov, S., Johnson, T.T.: HYST: a source transformation and translation tool for hybrid automaton models. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, pp. 128–133. ACM (2015)
Bak, S., Duggirala, P.S.: Simulation-equivalent reachability of large linear systems with inputs. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 401–420. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63387-9_20
Bak, S., Tran, H.D., Johnson, T.T.: Numerical verification of affine systems with up to a billion dimensions. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019, pp. 23–32. ACM, New York (2019). https://doi.org/10.1145/3302504.3311792
Banagaaya, N., Alì, G., Schilders, W.H.: Index-Aware Model Order Reduction Methods. Springer, Cham (2016). https://doi.org/10.2991/978-94-6239-189-5
Byrne, G., Ponzi, P.: Differential-algebraic systems, their applications and solutions. Comput. Chem. Eng. 12(5), 377–382 (1988)
Chahlaoui, Y., Van Dooren, P.: A collection of benchmark examples for model reduction of linear time invariant dynamical systems (2002)
Chen, X., Ábrahám, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258–263. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_18
Cross, E.A., Mitchell, I.M.: Level set methods for computing reachable sets of systems with differential algebraic equation dynamics. In: American Control Conference, pp. 2260–2265. IEEE (2008)
Dai, L.: Singular Control Systems. Lecture Notes in Control and Information Sciences. Springer, Heidelberg (1989)
Dang, T., Donzé, A., Maler, O.: Verification of analog and mixed-signal circuits using hybrid system techniques. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 21–36. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30494-4_3
Duan, G.R.: Analysis and Design of Descriptor Linear Systems, vol. 23. Springer, New York (2010)
Duggirala, P.S., Mitra, S., Viswanathan, M., Potok, M.: C2E2: a verification tool for stateflow models. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 68–82. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_5
Duggirala, P.S., Viswanathan, M.: Parsimonious, simulation based verification of linear systems. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 477–494. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41528-4_26
Eich-Soellner, E., Führer, C.: Numerical Methods in Multibody Dynamics, vol. 45. Springer, Wiesbaden (1998). https://doi.org/10.1007/978-3-663-09828-7
Fan, C., Qi, B., Mitra, S., Viswanathan, M., Duggirala, P.S.: Automatic reachability analysis for nonlinear hybrid models with C2E2. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 531–538. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41528-4_29
Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_30
Gerdin, M.: Parameter estimation in linear descriptor systems. Citeseer (2004)
Girard, A.: Reachability of uncertain linear systems using zonotopes. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 291–305. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31954-2_19
Guernic, C.L., Girard, A.: Reachability analysis of linear systems using support functions. Nonlinear Anal. Hybrid Syst. 4(2), 250–262 (2010). https://doi.org/10.1016/j.nahs.2009.03.002
Han, Z., Krogh, B.H.: Reachability analysis of large-scale affine systems using low-dimensional polytopes. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 287–301. Springer, Heidelberg (2006). https://doi.org/10.1007/11730637_23
Ho, C.W., Ruehli, A., Brennan, P.: The modified nodal approach to network analysis. IEEE Trans. Circuits Syst. 22(6), 504–509 (1975)
Kong, S., Gao, S., Chen, W., Clarke, E.: dreach: \(\delta \)-reachability analysis for hybrid systems, pp. 200–205 (2015)
März, R.: Canonical projectors for linear differential algebraic equations. Comput. Math. Appl. 31(4–5), 121–135 (1996)
Mehrmann, V., Stykel, T.: Balanced truncation model reduction for large-scale systems in descriptor form. In: Benner, P., Sorensen, D.C., Mehrmann, V. (eds.) Dimension Reduction of Large-Scale Systems. LNCSE, vol. 45, pp. 83–115. Springer, Heidelberg (2005). https://doi.org/10.1007/3-540-27909-1_3
Mitchell, I.M., Susuki, Y.: Level set methods for computing reachable sets of hybrid systems with differential algebraic equation dynamics. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 630–633. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78929-1_51
Musau, P., Lopez, D.M., Tran, H.D., Johnson, T.T.: Linear differential-algebraic equations (benchmark proposal). EPiC Ser. Comput. 54, 174–184 (2018)
Schon, T., Gerdin, M., Glad, T., Gustafsson, F.: A modeling and filtering framework for linear differential-algebraic equations. In: 42nd IEEE Conference on Decision and Control. Proceedings, vol. 1, pp. 892–897. IEEE (2003)
Tran, H.D., Bao, T., Johnson, T.T.: Discrete-space analysis of partial differential equations. EPiC Seri. Comput. 54, 185–195 (2018)
Tran, H.D., Nguyen, L.V., Hamilton, N., Xiang, W., Johnson, T.T.: Reachability analysis for high-index linear differential algebraic equations: extended version. In: 17th International Conference on Formal Modeling and Analysis of Timed Systems (2019)
Tran, H.D., Nguyen, L.V., Johnson, T.T.: Large-scale linear systems from order-reduction (benchmark proposal). In: 3rd Applied Verification for Continuous and Hybrid Systems Workshop (ARCH), Vienna, Austria (2016)
Tran, H.D., Nguyen, L.V., Xiang, W., Johnson, T.T.: Order-reduction abstractions for safety verification of high-dimensional linear systems. Discrete Event Dyn. Syst. 27(2), 443–461 (2017)
Tran, H.D., Xiang, W., Bak, S., Johnson, T.T.: Reachability analysis for one dimensional linear parabolic equations. IFAC-PapersOnLine 51(16), 133–138 (2018)
Acknowledgments
The material presented in this paper is based upon work supported by the National Science Foundation (NSF) under grant numbers CNS 1464311, CNS 1713253, SHF 1527398, and SHF 1736323, the Air Force Office of Scientific Research (AFOSR) through contract numbers FA9550-15-1-0258, FA9550-16-1-0246, and FA9550-18-1-0122. The U.S. government is authorized to reproduce and distribute reprints for Governmental purposes notwithstanding any copyright notation thereon. Any opinions, findings, and conclusions or recommendations expressed in this publication are those of the authors and do not necessarily reflect the views of AFOSR or NSF.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Tran, HD., Nguyen, L.V., Hamilton, N., Xiang, W., Johnson, T.T. (2019). Reachability Analysis for High-Index Linear Differential Algebraic Equations. In: André, É., Stoelinga, M. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2019. Lecture Notes in Computer Science(), vol 11750. Springer, Cham. https://doi.org/10.1007/978-3-030-29662-9_10
Download citation
DOI: https://doi.org/10.1007/978-3-030-29662-9_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-29661-2
Online ISBN: 978-3-030-29662-9
eBook Packages: Computer ScienceComputer Science (R0)