Skip to main content
SpringerLink
Log in

Temporal Logic Verification for Delay Differential Equations

  • Conference paper
  • First Online:
Theoretical Aspects of Computing – ICTAC 2016 (ICTAC 2016)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9965))

Included in the following conference series:

Abstract

Delay differential equations (DDEs) play an important role in the modeling of dynamic processes. Delays may arise in contemporary control schemes like networked distributed control and may cause deterioration of control performance, invalidating both stability and safety properties. This induces an interest in DDE especially in the area of modeling embedded control and formal methods for its verification. In this paper, 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 interval-based Taylor over-approximation method to enclose the solution of the DDE. As the solution of the DDE gets represented as a timed state sequence in terms of the Taylor coefficients, we can effectively solve temporal-logic verification problems represented as time-bounded MITL formulae. We encode necessary conditions for their 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 MITL specifications by the trajectories induced by a DDE. In contrast to our preliminary work in [34], we can verify arbitrary time-bounded MITL formulae, including nesting of modalities, rather than just invariance properties.

This research is funded by the Deutsche Forschungsgemeinschaft as part of the Research Training Group DFG GRK 1765 SCARE.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • 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.

    http://projects.informatik.uni-freiburg.de/projects/isat3/.

  2. 2.

    The corresponding prototype implementation of the interval Taylor over-approximation method for DDEs as well as some examples are available for download from https://github.com/liangdzou/isat-dde.

References

  1. Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116–146 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  2. Babin, G., Aït-Ameur, Y., Nakajima, S., Pantel, M.: Refinement and proof based development of systems characterized by continuous functions. In: Li, X., Liu, Z., Yi, W. (eds.) SETTA 2015. LNCS, vol. 9409, pp. 55–70. Springer, Heidelberg (2015). doi:10.1007/978-3-319-25942-0_4

    Chapter  Google Scholar 

  3. Bellman, R., Cooke, K.L.: Differential-difference equations. Technical report R-374-PR, The RAND Corporation, Santa Monica, California, January 1963

    Google Scholar 

  4. 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)

    Article  MathSciNet  MATH  Google Scholar 

  5. Butler, M.J., Abrial, J.-R., Banach, R.: Modelling and refining hybrid systems in Event-B and Rodin. In: Petre, L., Sekerinski, E. (eds.) From Action Systems to Distributed Systems - The Refinement Approach, pp. 29–42. Chapman and Hall/CRC, Boca Raton (2016)

    Chapter  Google Scholar 

  6. Chutinan, A., Krogh, B.H.: Computing polyhedral approximations to flow pipes for dynamic systems. In: Proceedings of the 37th International Conference on Decision and Control (CDC 1998) (1998)

    Google Scholar 

  7. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000). doi:10.1007/10722167_15

    Chapter  Google Scholar 

  8. Eggers, A., Fränzle, M., Herde, C.: SAT modulo ODE: a direct SAT approach to hybrid systems. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 171–185. Springer, Heidelberg (2008). doi:10.1007/978-3-540-88387-6_14

    Chapter  Google Scholar 

  9. Fainekos, G.E., Girard, A., Pappas, G.J.: Temporal logic verification using simulation. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 171–186. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  10. Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for finite state sequences in metric spaces. Technical report MS-CIS-06-05, Dept. of CIS, Univ. of Pennsylvania (2006)

    Google Scholar 

  11. Fort, J., Méndez, V.: Time-delayed theory of the neolithic transition in Europe. Phys. Rev. Lett. 82(4), 867 (1999)

    Article  Google Scholar 

  12. Fränzle, M., Herde, C., Ratschan, S., Schubert, T., Teige, T.: Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure. J. Satisfiability, Boolean Model. Comput. - Special Issue on SAT/CP Integr. 1, 209–236 (2007)

    MATH  Google Scholar 

  13. Gao, S., Kong, S., Clarke, E.M.: Satisfiability modulo ODEs. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, pp. 105–112. IEEE, 20–23 October 2013

    Google Scholar 

  14. 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)

    Chapter  Google Scholar 

  15. Glass, L., Mackey, M.C.: From Clocks to Chaos: The Rhythms of Life. Princeton University Press, Princeton (1988)

    MATH  Google Scholar 

  16. Ikeda, K., Matsumoto, K.: High-dimensional chaotic behavior in systems with time-delayed feedback. Physica D 29(1–2), 223–235 (1987)

    Article  MATH  Google Scholar 

  17. Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990)

    Article  Google Scholar 

  18. Kupferschmid, S., Becker, B.: Craig interpolation in the presence of non-linear constraints. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 240–255. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  19. Kurzhanski, A.B., Varaiya, P.: Ellipsoidal techniques for hybrid dynamics: the reachability problem. In: Kurzhanski, A.B., Varaiya, P. (eds.) New Directions and Applications in Control Theory. LNCIS, vol. 321, pp. 193–205. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  20. Lakshmanan, M., Senthilkumar, D.V.: Dynamics of Nonlinear Time-Delay Systems. Springer, Heidelberg (2011)

    Book  MATH  Google Scholar 

  21. Le Guernic, C., Girard, A.: Reachability analysis of linear systems using support functions. Nonlinear Anal. Hybrid Syst. 4(2), 250–262 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  22. Lohner, R.: Einschließung der Lösung gewöhnlicher Anfangs- und Randwertaufgaben. Ph.D. thesis, Fakultät für Mathematik der Universität Karlsruhe, Karlsruhe (1988)

    Google Scholar 

  23. Mackey, M.C., Glass, L., et al.: Oscillation and chaos in physiological control systems. Science 197(4300), 287–289 (1977)

    Article  Google Scholar 

  24. McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003). doi:10.1007/978-3-540-45069-6_1

    Chapter  Google Scholar 

  25. Moore, R.E.: Automatic local coordinate transformation to reduce the growth of error bounds in interval computation of solutions of ordinary differential equations. In: Ball, L.B. (ed.) Error in Digital Computation, vol. II, pp. 103–140. Wiley, New York (1965)

    Google Scholar 

  26. Neher, M., Jackson, K.R., Nedialkov, N.S.: On Taylor model based integration of ODEs. SIAM J. Numer. Anal. 45(1), 236–262 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  27. Ouaknine, J., Worrell, J.: On the decidability of metric temporal logic. In: Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS 2005), Chicago, IL, USA, pp. 188–197. IEEE Computer Society, 26–29 June 2005

    Google Scholar 

  28. Ouaknine, J., Worrell, J.: Some recent results in metric temporal logic. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 1–13. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  29. Scheiber, K.: iSAT3 Manual, April 2014

    Google Scholar 

  30. Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using induction and a SAT-solver. In: Hunt, W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 127–144. Springer, Heidelberg (2000). doi:10.1007/3-540-40922-X_8

    Chapter  Google Scholar 

  31. Stauning, O.: Automatic validation of numerical solutions. Ph.D. thesis, Technical University of Denmark, Lyngby (1997)

    Google Scholar 

  32. Szydłowski, M., Krawiec, A.: The stability problem in the kaldor-kalecki business cycle model. Chaos, Solitons & Fractals 25(2), 299–305 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  33. Szydłowski, M., Krawiec, A., Toboła, J.: Nonlinear oscillations in business cycle model with time lags. Chaos, Solitons & Fractals 12(3), 505–517 (2001)

    Article  MATH  Google Scholar 

  34. Zou, L., Fränzle, M., Zhan, N., Nazier Mosaad, P.: Automatic verification of stability and safety for delay differential equations. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015, Part II. LNCS, vol. 9207, pp. 338–355. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Carl v. Ossietzky Universität, Oldenburg, Germany

    Peter Nazier Mosaad, Martin Fränzle & Bai Xue

Authors
  1. Peter Nazier Mosaad
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Martin Fränzle
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Bai Xue
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Peter Nazier Mosaad .

Editor information

Editors and Affiliations

  1. Universidade Federal de Pernambuco Centro de Informática, Recife, Pernambuco, Brazil

    Augusto Sampaio

  2. Deptartment of Electrical Engineering BL, National Taiwan University, Taipei, Taiwan

    Farn Wang

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Nazier Mosaad, P., Fränzle, M., Xue, B. (2016). Temporal Logic Verification for Delay Differential Equations. In: Sampaio, A., Wang, F. (eds) Theoretical Aspects of Computing – ICTAC 2016. ICTAC 2016. Lecture Notes in Computer Science(), vol 9965. Springer, Cham. https://doi.org/10.1007/978-3-319-46750-4_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-46750-4_23

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-46749-8

  • Online ISBN: 978-3-319-46750-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation