Skip Navigation


Journal of Logic and Computation Advance Access first published online on November 18, 2008
This version published online on December 5, 2008
Journal of Logic and Computation, doi:10.1093/logcom/exn070
This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Platzer, A.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

© The Author, 2008. Published by Oxford University Press. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

Original Papers

Differential-algebraic Dynamic Logic for Differential-algebraic Programs

André Platzer

University of Oldenburg, Department of Computing Science, Germany.

E-mail: platzer{at}informatik.uni-oldenburg.de

Received 16 December 2007.

We generalize dynamic logic to a logic for differential-algebraic (DA) programs, i.e. discrete programs augmented with first-order differential-algebraic formulas as continuous evolution constraints in addition to first-order discrete jump formulas. These programs characterize interacting discrete and continuous dynamics of hybrid systems elegantly and uniformly. For our logic, we introduce a calculus over real arithmetic with discrete induction and a new differential induction with which DA programs can be verified by exploiting their differential constraints algebraically without having to solve them. We develop the theory of differential induction and differential refinement and analyse their deductive power. As a case study, we present parametric tangential roundabout maneuvers in air traffic control and prove collision avoidance in our calculus.

Keywords: Dynamic logic; differential constraints; sequent calculus; verification of hybrid systems; differential induction; theorem proving



References

  1. Alur R, Dill DL. A theory of timed automata. Theoretical Computer Science (1994) 126:183–235.[CrossRef][Web of Science]
  2. Anai H, Weispfenning V. Reach set computations using real quantifier elimination. Benedetto MDD, Sangiovanni-Vincentelli AL, eds. (2001) Springer. 63–76. In Hybrid Systems: Computation and Control (HSCC). Vol. 2034 of Lecture Notes in Computer Science.
  3. Asarin E, Dang T, Girard A. Reachability analysis of nonlinear systems using conservative approximation. Maler O, Pnueli A, eds. (2003) Springer. 20–35. In Hybrid Systems: Computation and Control (HSCC). Vol. 2623 of Lecture Notes in Computer Science.
  4. Beckert B, Platzer A. Dynamic logic with non-rigid functions: a basis for object-oriented program verification. Furbach U, Shankar N, eds. (2006) Springer. 266–280. In International Joint Conference on Automated Reasoning (IJCAR), Vol. 4130 of Lecture Notes in Computer Science.
  5. Branicky MS. General hybrid dynamical systems: Modeling, analysis and control. Alur R, Henzinger TA, Sontag ED, eds. (1995) Springer. 186–200. In Hybrid Systems. Vol. 1066 of Lecture Notes in Computer Science.
  6. Clarke EM, Fehnker A, Han Z, Krogh BH, Ouaknine J, Stursberg O, Theobald M. Abstraction and counterexample-guided refinement in model checking of hybrid systems. International Journal of Foundations of Computer Science (2003) 14:583–604.[CrossRef]
  7. Collins GE, Hong H. Partial cylindrical algebraic decomposition for quantifier elimination. Journal of Symbolic Computation (1991) 12:299–328.[CrossRef][Web of Science]
  8. Collins P, Lygeros J. Computability of finite-time reachable sets for hybrid systems. (2005) 4688–4693. In IEEE Conference on Decision and Control and European Control Conference (CDC-ECC’05) (December 2005).
  9. Damm W, Mikschl A, Oehlerking J, Olderog ER, Pang J, Platzer A, Segelken M, Wirtz B. Automating verification of cooperation, control and design in traffic applications. Jones CB, Liu Z, Woodcock J, eds. (2007) Springer. 115–169. In Formal Methods and Hybrid Real-Time Systems. Vol. 4700 of Lecture Notes in Computer Science.
  10. Damm W, Pinto G, Ratschan S. Guaranteed termination in the verification of LTL properties of non-linear robust discrete time hybrid systems. Peled D, Tsay YK, eds. (2005) Springer. 99–113. In Automated Technology for Verification and Analysis (ATVA), Vol. 3707 of Lecture Notes in Computer Science.
  11. Davoren JM, Nerode A. Logics for hybrid systems. IEEE (2000) 88:985–1010.[CrossRef]
  12. Dowek G, Hardin T, Kirchner C. Theorem proving modulo. Journal of Automated Reasoning (2003) 31:33–72.[CrossRef][Web of Science]
  13. Dowek G, Muñoz C, Carreño VA. Provably safe coordinated strategy for distributed conflict resolution. (2005) In Proceedings of the AIAA Guidance Navigation and Control Conference and Exhibit 2005, AIAA-2005-6047.
  14. Fitting M. First-Order Logic and Automated Theorem Proving (1996) 2nd. New York: Springer.
  15. Fitting M, Mendelsohn RL. First-Order Modal Logic (1999) Norwell, MA, USA: Kluwer.
  16. Fränzle M. Analysis of hybrid systems: an ounce of realism can save an infinity of states. Flum J, Rodríguez-Artalejo M, eds. (1999) Springer. 126–140. In Computer Science Logic (CSL), Vol. 1683 of Lecture Notes in Computer Science.
  17. Galdino AL, Muñoz C, Ayala-Rincón M. Formal verification of an optimal air traffic conflict resolution and recovery algorithm. Leivant D, de Queiroz R, eds. (2007) Springer. 177–188. In Workshop on Logic, Language, Information and Computation (WoLLIC), Vol. 4576 of Lecture Notes in Computer Science.
  18. Gear CW. Differential-algebraic equations index transformations. SIAM. Journal of Scientific and Statistical Computing (1988) 9:39–47.[CrossRef]
  19. Gulwani S, Tiwari A. Constraint-based approach for analysis of hybrid systems. Gupta A, Malik S, eds. (2008) Springer. 190–203. In CAV. Vol. 5123 of Lecture Notes in Computer Science.
  20. Harel D, Kozen D, Tiuryn J. J. Dynamic Logic (2000) Cambridge: MIT Press.
  21. Henzinger TA. The theory of hybrid automata. In. In: LICS, Los Alamitos, IEEE Computer Society (1996) 278–292.
  22. Henzinger TA, Nicollin X, Sifakis J, Yovine S. Symbolic model checking for real-time systems. In. In: LICS, IEEE Computer Society (1992) 394–406.
  23. Hwang I, Kim J, Tomlin C. Protocol-based conflict resolution for air traffic control. Air Traffic Control Quarterly (2007) 15:1–34.
  24. Johansson KH, Sastry S, Zhang J, Lygeros J. Zeno hybrid systems. International Journal of Robust & Nonlinear Control (2001) 11:435–451.[CrossRef]
  25. Kolchin ER. Differential Algebra and Algebraic Groups (1972) New York: Academic Press.
  26. Livadas C, Lygeros J, Lynch NA. High-level modeling and analysis of TCAS. Proceedings of IEEE - Special Issue on Hybrid Systems: Theory & Applications (2000) 88:926–947.
  27. Massink M, Francesco ND. Modelling free flight with collision avoidance. In. In: ICECCS, Los Alamitos, IEEE Computer Society (2001) 270–280.
  28. Piazza C, Antoniotti M, Mysore V, Policriti A, Winkler F, Mishra B. Algorithmic algebraic model checking I: challenges from systems biology. Etessami K, Rajamani SK, eds. (2005) Springer. 5–19. In CAV. Vol. 3576 of Lecture Notes in Computer Science.
  29. Platzer A. Differential dynamic logic for verifying parametric hybrid systems. Olivetti N, ed. (2007) Springer. 216–232. In TABLEAUX. Vol. 4548 of Lecture Notes in Computer Science.
  30. Platzer A. A temporal dynamic logic for verifying hybrid system invariants. Artëmov SN, Nerode A, eds. (2007) Springer. 457–471. In Symposium on Logical Foundations of Computer Science (LFCS), Vol. 4514 of Lecture Notes in Computer Science.
  31. Platzer A. Differential dynamic logic for hybrid systems. Journal of Automated Reasoning (2008) 41:143–189.[CrossRef][Web of Science]
  32. Platzer A, Clarke EM. The image computation problem in hybrid systems model checking. Bemporad A, Bicchi A, Buttazzo G, eds. (2007) Springer. 473–486. In Hybrid Systems: Computation and Control (HSCC), Vol. 4416 of Lecture Notes in Computer Science.
  33. Platzer A, Clarke EM. Computing differential invariants of hybrid systems as fixedpoints. Gupta A, Malik S, eds. (2008) Springer. 176–189. In CAV. Vol. 5123 of Lecture Notes in Computer Science.
  34. Platzer A, Quesel JD. KeYmaera: Ahybrid theorem prover for hybrid systems. Armando A, Baumgartner P, Dowek G, eds. (2008) Springer. 171–178. In International Joint Conference on Automated Reasoning (IJCAR). Vol. 5195, of Lecture Notes in Computer Science.
  35. Platzer A, Quesel JD. Logical verification and systematic parametric analysis in train control. Egerstedt M, Mishra B, eds. (2008) Springer. 646–649. In Hybrid Systems: Computation and Control (HSCC). Vol. 4981 of Lecture Notes in Computer Science.
  36. Pour-El MB, Richards I. A computable ordinary differential equation which possesses no computable solution. Annals of Mathematical Logic (1979) 17:61–90.[CrossRef]
  37. Prajna S, Jadbabaie A. Safety verification of hybrid systems using barrier certificates. Alur R, Pappas GJ, eds. (2004) Springer. 477–492. In 7th International Workshop, Hybrid Systems: Computation and Control, (HSCC) 2004, Philadelphia, PA, USA, March 25–27, 2004, HSCC. Vol. 2993 of Lecture Notes in Computer Science.
  38. Prajna S, Jadbabaie A, Pappas GJ. A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Transactions onAutomated Control (2007) 52:1415–1429.[CrossRef]
  39. Rodríguez-Carbonell E, Tiwari A. Generating polynomial invariants for hybrid systems. Morari M, Thiele L, eds. (2005) Springer. 590–605. In Hybrid Systems: Computation and Control (HSCC), Vol. 3414 of Lecture Notes in Computer Science.
  40. Rönkkö M, Ravn AP, Sere K. Hybrid action systems. Theoretical Computer Science (2003) 290:937–973.[CrossRef][Web of Science]
  41. Sankaranarayanan S, Sipma H, Manna Z. Constructing invariants for hybrid systems. Alur R, Pappas GJ, eds. (2004) Springer. 539–554. In 7th International Workshop, Hybrid Systems: Computation and Control, (HSCC) 2004, Philadelphia, PA, USA, March 25–27, 2004, Proceedings, HSCC, Vol. 2993 of Lecture Notes in Computer Science.
  42. Schobbens PY, Raskin JF, Henzinger TA. Axioms for real-time logics. Theoretical Computer Science (2002) 274:151–182.[CrossRef][Web of Science]
  43. Sibirsky KS. Introduction to Topological Dynamics (1975) Leyden: Noordhoff.
  44. Tinelli C. Cooperation of background reasoners in theory reasoning by residue sharing. Journal of Automated Reasoning (2003) 30:1–31.[CrossRef][Web of Science]
  45. Tomlin C, Pappas GJ, Sastry S. Conflict resolution for air traffic management: a study in multi-agent hybrid systems. IEEE Transactions on Automated Control (1998) 43:509–521.[CrossRef]
  46. Walter W. Ordinary Differential Equations (1998) Springer.
  47. Zhou C, Ravn AP, Hansen MR. An extended duration calculus for hybrid real-time systems. Grossman RL, Nerode A, Ravn AP, Rischel H, eds. (1992) Springer. 36–59. In Hybrid Systems. Vol. 736 of Lecture Notes in Computer Science.

Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?



This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Platzer, A.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?