[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

A Temporal Dynamic Logic for Verifying Hybrid System Invariants

  • Conference paper
Logical Foundations of Computer Science (LFCS 2007)

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

Included in the following conference series:

  • 592 Accesses

Abstract

We combine first-order dynamic logic for reasoning about possible behaviour of hybrid systems with temporal logic for reasoning about the temporal behaviour during their operation. Our logic supports verification of hybrid programs with first-order definable flows and provides a uniform treatment of discrete and continuous evolution. For our combined logic, we generalise the semantics of dynamic modalities to refer to hybrid traces instead of final states. Further, we prove that this gives a conservative extension of dynamic logic. On this basis, we provide a modular verification calculus that reduces correctness of temporal behaviour of hybrid systems to non-temporal reasoning. Using this calculus, we analyse safety invariants in a train control system and symbolically synthesise parametric safety constraints.

This research was supported by a fellowship of the German Academic Exchange Service (DAAD). It was also sponsored by the German Research Council (DFG) as part of the Transregional Collaborative Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS, see www.avacs.org ).

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking for real-time systems. In: LICS, pp. 414–425. IEEE Computer Society Press, Los Alamitos (1990)

    Google Scholar 

  2. Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)

    Google Scholar 

  3. Beckert, B., Platzer, A.: Dynamic logic with non-rigid functions: A basis for object-oriented program verification. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 266–280. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  4. Beckert, B., Schlager, S.: A sequent calculus for first-order dynamic logic with trace modalities. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 626–641. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  5. Bemporad, A., Bicchi, A., Buttazzo, G. (eds.): HSCC 2007. LNCS, vol. 4416. Springer, Heidelberg (2007)

    MATH  Google Scholar 

  6. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  7. Damm, W., Hungar, H., Olderog, E.-R.: On the verification of cooperating traffic agents. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2003. LNCS, vol. 3188, pp. 77–110. Springer, Heidelberg (2004)

    Google Scholar 

  8. Davoren, J.M., Coulthard, V., Markey, N., Moor, T.: Non-deterministic temporal logics for general flow systems. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 280–295. Springer, Heidelberg (2004)

    Google Scholar 

  9. Davoren, J.M., Nerode, A.: Logics for hybrid systems. Proceedings of the IEEE 88(7), 985–1010 (2000), citeseer.ist.psu.edu/article/davoren00logics.html

    Article  Google Scholar 

  10. Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2(3), 241–266 (1982)

    Article  MATH  Google Scholar 

  11. Emerson, E.A., Halpern, J.Y.: “Sometimes” and “Not Never” revisited: on branching versus linear time temporal logic. J. ACM 33(1), 151–178 (1986)

    Article  MATH  MathSciNet  Google Scholar 

  12. Faber, J., Meyer, R.: Model checking data-dependent real-time properties of the European Train Control System. In: FMCAD, Nov. 2006, pp. 76–77. IEEE Computer Society Press, Los Alamitos (2006)

    Google Scholar 

  13. Harel, D., Kozen, D., Tiuryn, J.: Dynamic logic. MIT Press, Cambridge (2000)

    MATH  Google Scholar 

  14. Henzinger, T.A.: The theory of hybrid automata. In: LICS, pp. 278–292 (1996)

    Google Scholar 

  15. Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. In: LICS, pp. 394–406. IEEE Computer Society Press, Los Alamitos (1992)

    Google Scholar 

  16. Hutter, D., Langenstein, B., Sengler, C., Siekmann, J.H., Stephan, W., Wolpers, A.: Deduction in the verification support environment (VSE). In: Gaudel, M.-C., Woodcock, J.C.P. (eds.) FME 1996. LNCS, vol. 1051, pp. 268–286. Springer, Heidelberg (1996)

    Google Scholar 

  17. Leivant, D.: Partial correctness assertions provable in dynamic logics. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 304–317. Springer, Heidelberg (2004)

    Google Scholar 

  18. Mysore, V., Piazza, C., Mishra, B.: Algorithmic algebraic model checking II: Decidability of semi-algebraic model checking and its applications to systems biology. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 217–233. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  19. Platzer, A.: Differential dynamic logic for verifying parametric hybrid systems (2007)

    Google Scholar 

  20. Platzer, A.: Differential logic for reasoning about hybrid systems. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 746–749. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  21. Platzer, A.: A temporal dynamic logic for verifying hybrid system invariants. Reports of SFB/TR 14 AVACS 12 (February 2007), available at http://www.avacs.org

  22. Platzer, A.: Towards a hybrid dynamic logic for hybrid dynamic systems. In: Blackburn, P., Bolander, T., Braüner, T., de Paiva, V., Villadsen, J. (eds.) Proc., LICS International Workshop on Hybrid Logic, 2006, Seattle, USA. ENTCS (2007)

    Google Scholar 

  23. Platzer, A., Clarke, E.M.: The image computation problem in hybrid systems model checking. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 473–486. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  24. Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46–57. IEEE Computer Society Press, Los Alamitos (1977)

    Google Scholar 

  25. Pratt, V.R.: Process logic. In: POPL, pp. 93–100 (1979)

    Google Scholar 

  26. Zhou, C., Ravn, A.P., Hansen, M.R.: An extended duration calculus for hybrid real-time systems. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) Hybrid Systems. LNCS, vol. 736, pp. 36–59. Springer, Heidelberg (1993)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Oldenburg, Department of Computing Science, Germany, Carnegie Mellon University, Computer Science Department, Pittsburgh, PA,  

    André Platzer

Authors
  1. André Platzer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Sergei N. Artemov Anil Nerode

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer Berlin Heidelberg

About this paper

Cite this paper

Platzer, A. (2007). A Temporal Dynamic Logic for Verifying Hybrid System Invariants . In: Artemov, S.N., Nerode, A. (eds) Logical Foundations of Computer Science. LFCS 2007. Lecture Notes in Computer Science, vol 4514. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-72734-7_32

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-72734-7_32

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-72732-3

  • Online ISBN: 978-3-540-72734-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation