Model Checking Delay Differential Equations Against Metric Interval Temporal Logic

Published in Volume XXVII, Issue 1, 2017, pages 77-109, doi: 10.7561/SACS.2017.1.77

Authors: P.N. Mosaad, M. Fränzle, B. Xue

Abstract

Delay differential equations (DDEs) play an important role in the modeling of dynamic processes. Delays arise in contemporary control schemes like networked distributed control and can cause deterioration of control performance, invalidating both stability and safety properties. This induces an interest in DDE especially in the area of modeling and verification of embedded control. In this article, we present an approach aiming at automatic safety verification of a simple class of DDEs against requirements expressed in a linear-time temporal logic. As requirements specification language, we exploit metric interval temporal logic (MITL) with a continuous-time semantics evaluating signals over metric spaces. We employ an over-approximation method based on interval Taylor series to enclose the solution of the DDE and thereby reduce the continuous-time verification problem for MITL formulae to a discrete-time problem over sequences of Taylor coefficients. We encode sufficient conditions for satisfaction as SMT formulae over polynomial arithmetic and use the iSAT3 SMT solver in its bounded model-checking mode for discharging the resulting proof obligations, thus proving satisfaction of time-bounded MITL specifications by the trajectories induced by a DDE. In contrast to our preliminary work in [44], we can verify arbitrary time-bounded MITL formulae, including nesting of modalities, rather than just invariance properties.

Full Text (PDF)

References

[1] R. Alur, T. Feder, and T.A. Henzinger. The benefits of relaxing punctuality. Journal of the ACM, 43(1):116–146, 1996. doi: 10.1145/227595.227602.

[2] G. Babin, Y.A. Ameur, S. Nakajima, and M. Pantel. Refinement and proof based development of systems characterized by continuous functions. In X. Li, Z. Liu, and W. Yi, editors, Dependable Software Engineering: Theories, Tools, and Applications – First International Symposium, SETTA 2015, Nanjing, China, November 4-6, 2015, Proceedings, volume 9409 of Lecture Notes in Computer Science, pages 55–70. Springer, 2015. doi:10.1007/978-3-319-25942-0_4.

[3] R. Bellman and K.L. Cooke. Differential-difference equations. Technical Report R-374-PR, The RAND Corporation, Santa Monica, California, January 1963.

[4] M. Berz and K. Makino. Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models. Reliable Computing, 4(4):361–369, 1998. doi:10.1023/A:1024467732637.

[5] M.J. Butler, J.-R. Abrial, and R. Banach. Modelling and refining hybrid systems in Event-B and Rodin. In L. Petre and E. Sekerinski, editors, From Action Systems to Distributed Systems – The Refinement Approach., pages 29–42. Chapman and Hall/CRC, 2016. doi:10.1201/ b20053-5.

[6] M. Chen, M. Fr¨anzle, Y. Li, P. Nazier Mosaad, and N. Zhan. Validated simulation-based verification of delayed differential dynamics. In J.S. Fitzgerald, C.L. Heitmeyer, S. Gnesi, and A. Philippou, editors, FM 2016: Formal Methods – 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings, volume 9995 of Lecture Notes in Computer Science, pages 137–154, 2016. doi: 10.1007/978-3-319-48989-6_9.

[7] A. Chutinan and B.H. Krogh. Computing polyhedral approximations to flow pipes for dynamic systems. In Decision and Control, 1998. Proceedings of the 37th IEEE Conference on, volume 2, pages 2089– 2094. IEEE, 1998. doi:10.1109/CDC.1998.758642.

[8] E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In E.A. Emerson and A.P. Sistla, editors, Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings, volume 1855 of Lecture Notes in Computer Science, pages 154–169. Springer, 2000. doi:10.1007/10722167_15.

[9] A. Eggers, M. Fr¨anzle, and C. Herde. SAT modulo ODE: A direct SAT approach to hybrid systems. In S.D. Cha, J.-Y. Choi, M. Kim, I. Lee, and M. Viswanathan, editors, Automated Technology for Verification and Analysis, 6th International Symposium, ATVA 2008, Seoul, Korea, October 20-23, 2008. Proceedings, volume 5311 of Lecture Notes in Computer Science, pages 171–185. Springer, 2008. doi:10.1007/978-3-540-88387-6_14.

[10] G.E. Fainekos, A. Girard, and G.J. Pappas. Temporal logic verification using simulation. In E. Asarin and P. Bouyer, editors, Formal Modeling and Analysis of Timed Systems, 4th International Conference, FORMATS 2006, Paris, France, September 25-27, 2006, Proceedings, volume 4202 of Lecture Notes in Computer Science, pages 171–186. Springer, 2006. doi:10.1007/11867340_13.

[11] G.E. Fainekos and G.J. Pappas. Robustness of temporal logic specifications for finite state sequences in metric spaces. Technical report, Technical Report MS-CIS-06-05, Dept. of CIS, Univ. of Pennsylvania, 2006.

[12] J. Fort and V. Méndez. Time-delayed theory of the neolithic transition in Europe. Physical review letters, 82(4):867–870, 1999. doi:10.1103/ PhysRevLett.82.867.

[13] M. Fränzle, C. Herde, T. Teige, S. Ratschan, and T. Schubert. Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. Journal on Satisfiability, Boolean Modeling and Computation, 1(3-4):209–236, 2007. URL: https://satassociation.org/jsat/index.php/jsat/article/view/16/12.

[14] S. Gao, S. Kong, and E.M. Clarke. Satisfiability modulo ODEs. In Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013, pages 105–112. IEEE, 2013. doi:10.1109/FMCAD.2013.6679398.

[15] A. Girard. Reachability of uncertain linear systems using zonotopes. In M. Morari and L. Thiele, editors, Hybrid Systems: Computation and Control, 8th International Workshop, HSCC 2005, Zurich, Switzerland, March 9-11, 2005, Proceedings, volume 3414 of Lecture Notes in Computer Science, pages 291–305. Springer, 2005. doi:10.1007/978-3-540-31954-2_19.

[16] L. Glass and M.C. Mackey. From clocks to chaos: the rhythms of life. Princeton University Press, 1988.

[17] G.B. Gustafson. Systems of differential equations. In Manuscript for Course Eng Math 2250-1 Spring 2014, chapter 11. Dpt. of Mathematics, University of Utah, 2014.

[18] Z. Huang, C. Fan, and S. Mitra. Bounded invariant verification for time-delayed nonlinear networked dynamical systems. Nonlinear Analysis: Hybrid Systems, 23:211–229, 2017. doi:10.1016/j.nahs.2016.05.005.

[19] K. Ikeda and K. Matsumoto. High-dimensional chaotic behavior in systems with time-delayed feedback. Physica D: Nonlinear Phenomena, 29(1-2):223–235, 1987. doi:10.1016/0167-2789(87)90058-3.

[20] R. Koymans. Specifying real-time properties with metric temporal logic. Real-Time Systems, 2(4):255–299, 1990. doi:10.1007/BF01995674.

[21] S. Kupferschmid and B. Becker. Craig interpolation in the presence of non-linear constraints. In U. Fahrenberg and S. Tripakis, editors, Formal Modeling and Analysis of Timed Systems – 9th International Conference, FORMATS 2011, Aalborg, Denmark, September 21-23, 2011. Proceedings, volume 6919 of Lecture Notes in Computer Science, pages 240–255. Springer, 2011. doi:10.1007/978-3-642-24310-3_17.

[22] A.B. Kurzhanski and P. Varaiya. Ellipsoidal techniques for reachability analysis. In N.A. Lynch and B.H. Krogh, editors, Hybrid Systems: Computation and Control, Third International Workshop, HSCC 2000, Pittsburgh, PA, USA, March 23-25, 2000, Proceedings, volume 1790 of Lecture Notes in Computer Science, pages 202–214. Springer, 2000. doi:10.1007/3-540-46430-1_19.

[23] M. Lakshmanan and D.V. Senthilkumar. Dynamics of nonlinear time- delay systems. Springer Science & Business Media, 2011. doi:10.1007/978-3-642-14938-2.

[24] C. Le Guernic and A. Girard. Reachability analysis of linear systems using support functions. Nonlinear Analysis: Hybrid Systems, 4(2):250– 262, 2010. doi:10.1016/j.nahs.2009.03.002.

[25] R. Lohner. Einschließung der Lösung gewöhnlicher Anfangs-und Randwertaufgaben. PhD thesis, Fakultät für Mathematik der Universität Karlsruhe, Karlsruhe, 1988.

[26] M.C. Mackey and L. Glass. Oscillation and chaos in physiological control systems. Science, 197(4300):287–289, 1977. doi:10.1126/ science.267326.

[27] O. Maler and D. Nickovic. Monitoring temporal properties of continuous signals. In Y. Lakhnech and S. Yovine, editors, Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Joint International Conferences on Formal Modelling and Analysis of Timed Systems, FORMATS 2004 and Formal Techniques in Real-Time and Fault- Tolerant Systems, FTRTFT 2004, Grenoble, France, September 22-24, 2004, Proceedings, volume 3253 of Lecture Notes in Computer Science, pages 152–166. Springer, 2004. doi:10.1007/978-3-540-30206-3_12.

[28] Z. Manna and A. Pnueli. The temporal logic of reactive and concurrent systems – specification. Springer, 1992. doi:10.1007/978-1-4612-0931-7.

[29] K.L. McMillan. Interpolation and SAT-based model checking. In W.A. Hunt Jr. and F. Somenzi, editors, Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings, volume 2725 of Lecture Notes in Computer Science, pages 1–13. Springer, 2003. doi:10.1007/978-3-540-45069-6_1.

[30] R.E. Moore. Automatic local coordinate transformation to reduce the growth of error bounds in interval computation of solutions of ordinary differential equations. In L. B. Ball, editor, Error in Digital Computation, volume II, pages 103–140. Wiley, New York, 1965.

[31] M. Neher, K.R. Jackson, and N.S. Nedialkov. On Taylor model based integration of ODEs. SIAM Journal on Numerical Analysis, 45(1):236– 262, 2007. doi:10.1137/050638448.

[32] J. Ouaknine and J. Worrell. On the decidability of metric temporal logic. In 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA, Proceedings, pages 188–197. IEEE Computer Society, 2005. doi:10.1109/LICS.2005.33.

[33] J. Ouaknine and J. Worrell. Some recent results in metric temporal logic. In F. Cassez and C. Jard, editors, Formal Modeling and Analysis of Timed Systems, 6th International Conference, FORMATS 2008, Saint Malo, France, September 15-17, 2008. Proceedings, volume 5215 of Lecture Notes in Computer Science, pages 1–13. Springer, 2008. doi:10.1007/978-3-540-85778-5_1.

[34] E. Plaku, L.E. Kavraki, and M.Y. Vardi. Falsification of LTL safety properties in hybrid systems. In S. Kowalewski and A. Philippou, editors, Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, volume 5505 of Lecture Notes in Computer Science, pages 368–382. Springer, 2009. doi:10.1007/978-3-642-00768-2_31.

[35] Stephen Prajna and Ali Jadbabaie. Methods for safety verification of time-delay systems. In Proceedings of the 44th IEEE Conference on Decision and Control, pages 4348–4353. IEEE, 2005. doi:10.1109/CDC. 2005.1582846.

[36] A. Robinson and A. Voronkov. Handbook of automated reasoning, volume 1. Elsevier, 2001. doi:10.1016/B978-0-444-50813-3.50032-1.

[37] S. Sankaranarayanan and G.E. Fainekos. Falsification of temporal properties of hybrid systems using the cross-entropy method. In T. Dang and I.M. Mitchell, editors, Hybrid Systems: Computation and Control (part of CPS Week 2012), HSCC’12, Beijing, China, April 17-19, 2012, pages 125–134. ACM, 2012. doi:10.1145/2185632.2185653.

[38] K. Scheibler. iSAT3 Manual, December 2016. Available at https://projects.avacs.org/attachments/download/671/ isat3_manual-0.03-20161213.pdf.

[39] M. Sheeran, S. Singh, and G. Stålmarck. Checking safety properties using induction and a SAT-solver. In W.A. Hunt Jr. and S.D. Johnson, editors, Formal Methods in Computer-Aided Design, Third International Conference, FMCAD 2000, Austin, Texas, USA, November 1-3, 2000, Proceedings, volume 1954 of Lecture Notes in Computer Science, pages 108–125. Springer, 2000. doi:10.1007/3-540-40922-X_8.

[40] O. Stauning. Automatic Validation of Numerical Solutions. PhD thesis, Technical University of Denmark, Lyngby, 1997. URL: http://www2.imm.dtu.dk/documents/ftp/phdliste/phd36_97.ps.

[41] M. Szydlowski and A. Krawiec. The stability problem in the Kaldor– Kalecki business cycle model. Chaos, Solitons & Fractals, 25(2):299–305, 2005. doi:10.1016/j.chaos.2004.11.012.

[42] M. Szydlowski, A. Krawiec, and J. Tobola. Nonlinear oscillations in business cycle model with time lags. Chaos, Solitons & Fractals, 12(3):505–517, 2001. doi:10.1016/S0960-0779(99)00207-6.

[43] G.S. Tseitin. On the complexity of derivation in propositional calculus. In Automation of reasoning, pages 466–483. Springer, 1983. doi:10.1007/978-3-642-81955-1_28.

[44] L. Zou, M. Fränzle, N. Zhan, and P. Nazier Mosaad. Automatic verification of stability and safety for delay differential equations. In D. Kroening and C.S. Pasareanu, editors, Computer Aided Verification – 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II, volume 9207 of Lecture Notes in Computer Science, pages 338–355. Springer, 2015. doi:10.1007/978-3-319-21668-3_20.

Bibtex

@article{sacscuza:mosaad2017mcddeamitl,
  title={Model Checking Delay Differential Equations Against Metric Interval Temporal Logic},
  author={P.N. Mosaad and M. Fränzle and B. Xue},
  journal={Scientific Annals of Computer Science},
  volume={27},
  number={1},
  organization={``A.I. Cuza'' University, Iasi, Romania},
  year={2017},
  pages={77--109},
  doi={10.7561/SACS.2017.1.77},
  publisher={``A.I. Cuza'' University Press}
}