Decoupling Abstractions of Non-linear Ordinary Differential Equations

详细信息    查看全文

• 关键词：Ordinary differential equations ; Darboux polynomials ; Simulation ; Abstraction ; Decoupling
• 刊名：Lecture Notes in Computer Science
• 出版年：2016
• 出版时间：2016
• 年：2016
• 卷：9995
• 期：1
• 页码：628-644
• 全文大小：311 KB
• 参考文献：1.Abrial, J.-R., Su, W., Zhu, H.: Formalizing hybrid systems with Event-B. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 178–193. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-30885-7_​13 CrossRef
  2.Bak, S., Bogomolov, S., Johnson, T.T.: HYST: a source transformation and translation tool for hybrid automaton models. In: HSCC, pp. 128–133. ACM (2015)
  3.Berz, M., Makino, K.: Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models. Reliable Comput. 4(4), 361–369 (1998)MathSciNet CrossRef MATH
  4.Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975). doi:10.​1007/​3-540-07407-4_​17 CrossRef
  5.Conti, R., Galeotti, M.: Totally bounded cubic systems in \(\mathbb{R}^2\) . In: Macki, J.W., Zecca, P. (eds.) Dynamical Systems. LNM, vol. 1822, pp. 103–171. Springer, Heidelberg (2003). doi:10.​1007/​978-3-540-45204-1_​2 CrossRef
  6.Dumortier, F., Llibre, J., Artés, J.C.: Qualitative Theory of Planar Differential Systems. Springer, Heidelberg (2006)MATH
  7.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). doi:10.​1007/​978-3-642-54862-8_​19 CrossRef
  8.Giannakopoulou, D., Méry, D. (eds.): FM 2012. LNCS, vol. 7436. Springer, Heidelberg (2012)MATH
  9.Ginoux, J.M.: Differential Geometry Applied to Dynamical Systems. World Scientific Series on Nonlinear Science, vol. 66. World Scientific, Singapore (2009)MATH
  10.Girard, A., Pappas, G.J.: Approximate bisimulation: a bridge between computer science and control theory. Eur. J. Control 17(5–6), 568–578 (2011)MathSciNet CrossRef MATH
  11.Goriely, A.: Integrability and Nonintegrability of Dynamical Systems. Advanced Series in Nonlinear Dynamics. World Scientific, Singapore (2001)CrossRef MATH
  12.Hale, J.K., LaSalle, J.P.: Differential equations: linearity vs. nonlinearity. SIAM Rev. 5(3), 249–272 (1963)MathSciNet CrossRef MATH
  13.Han, Z., Krogh, B.: Reachability analysis of hybrid control systems using reduced-order models. In: 2004 American Control Conference, Proceedings of the 2004, vol. 2, pp. 1183–1189, June 2004
  14.Jeannin, J.-B., Ghorbal, K., Kouskoulas, Y., Gardner, R., Schmidt, A., Zawadzki, E., Platzer, A.: A formally verified hybrid system for the next-generation airborne collision avoidance system. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 21–36. Springer, Heidelberg (2015). doi:10.​1007/​978-3-662-46681-0_​2
  15.Matringe, N., Moura, A.V., Rebiha, R.: Generating invariants for non-linear hybrid systems by linear algebraic methods. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 373–389. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-15769-1_​23 CrossRef
  16.Nedialkov, N.S.: Interval tools for ODEs and DAEs. In: 12th GAMM - IMACS International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics (SCAN), p. 4, September 2006
  17.Neher, M., Jackson, K.R., Nedialkov, N.S.: On Taylor model based integration of ODEs. SIAM J. Numer. Anal. 45(1), 236–262 (2007)MathSciNet CrossRef MATH
  18.Pappas, G.J.: Bisimilar linear systems. Automatica 39(12), 2035–2047 (2003)MathSciNet CrossRef MATH
  19.Platzer, A.: A complete uniform substitution calculus for differential dynamic logic. J. Autom. Reasoning, 1–47 (2016)
  20.Platzer, A., Clarke, E.M.: Formal verification of curved flight collision avoidance maneuvers: a case study. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 547–562. Springer, Heidelberg (2009). doi:10.​1007/​978-3-642-05089-3_​35 CrossRef
  21.Robinson, J.C.: An Introduction to Ordinary Differential Equations. Cambridge University Press, Cambridge (2004)CrossRef MATH
  22.Sankaranarayanan, S.: Change-of-bases abstractions for non-linear hybrid systems. Nonlinear Anal. Hybrid Syst. 19, 107–133 (2016)MathSciNet CrossRef MATH
  23.Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing invariants for hybrid systems. Formal Methods Syst. Des. 32(1), 25–55 (2008)CrossRef MATH
  24.Sankaranarayanan, S., Tiwari, A.: Relational abstractions for continuous and hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 686–702. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-22110-1_​56 CrossRef
  25.Strogatz, S.H.: Nonlinear Dynamics and Chaos. Westview Press, New York (1994)
  26.Tarski, A.: A decision method for elementary algebra and geometry. In: Bulletin of the American Mathematical Society, vol. 59 (1951)
  27.Teschl, G.: Ordinary Differential Equations and Dynamical Systems. Graduate Studies in Mathematics, vol. 140. American Mathematical Society, Providence (2012)MATH
  28.Zhao, H., Yang, M., Zhan, N., Gu, B., Zou, L., Chen, Y.: Formal verification of a descent guidance control program of a lunar lander. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 733–748. Springer, Heidelberg (2014). doi:10.​1007/​978-3-319-06410-9_​49 CrossRef
  29.Zou, L., Lv, J., Wang, S., Zhan, N., Tang, T., Yuan, L., Liu, Y.: Verifying chinese train control system under a combined scenario by theorem proving. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 262–280. Springer, Heidelberg (2014). doi:10.​1007/​978-3-642-54108-7_​14 CrossRef
  
• 作者单位：Andrew Sogokon (17)
  Khalil Ghorbal (18)
  Taylor T. Johnson (19)
  
  17. Vanderbilt University, Nashville, Tennessee, USA
  18. Inria, Rennes, Brittany, France
  19. Vanderbilt University, Nashville, Tennessee, USA
  
• 丛书名：FM 2016: Formal Methods
• ISBN：978-3-319-48989-6
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349
• 卷排序：9995

文摘

We investigate decoupling abstractions, by which we seek to simulate (i.e. abstract) a given system of ordinary differential equations (ODEs) by another system that features completely independent (i.e. uncoupled) sub-systems, which can be considered as separate systems in their own right. Beyond a purely mathematical interest as a tool for the qualitative analysis of ODEs, decoupling can be applied to verification problems arising in the fields of control and hybrid systems. Existing verification technology often scales poorly with dimension. Thus, reducing a verification problem to a number of independent verification problems for systems of smaller dimension may enable one to prove properties that are otherwise seen as too difficult. We show an interesting correspondence between Darboux polynomials and decoupling simulating abstractions of systems of polynomial ODEs and give a constructive procedure for automatically computing the latter.