research-article

Differential Dynamic Logic for Hybrid Systems

Author:

André PlatzerAuthors Info & Claims

Journal of Automated Reasoning, Volume 41, Issue 2

Pages 143 - 189

https://doi.org/10.1007/s10817-008-9103-8

Published: 01 August 2008 Publication History

Abstract

Hybrid systems are models for complex physical systems and are defined as dynamical systems with interacting discrete transitions and continuous evolutions along differential equations. With the goal of developing a theoretical and practical foundation for deductive verification of hybrid systems, we introduce a dynamic logic for hybrid programs, which is a program notation for hybrid systems. As a verification technique that is suitable for automation, we introduce a free variable proof calculus with a novel combination of real-valued free variables and Skolemisation for lifting quantifier elimination for real arithmetic to dynamic logic. The calculus is compositional, i.e., it reduces properties of hybrid programs to properties of their parts. Our main result proves that this calculus axiomatises the transition behaviour of hybrid systems completely relative to differential equations. In a case study with cooperating traffic agents of the European Train Control System, we further show that our calculus is well-suited for verifying realistic hybrid systems with parametric system dynamics.

References

[1]

Ábrahám-Mumm E., Steffen M., and Hannemann U.Verification of hybrid systems: formalization and proof rules in PVSICECCS2001Los AlamitosIEEE Computer Society48-57doi:10.1109/ICECCS.2001.930163

[2]

Alur R., Courcoubetis C., and Dill D.L. Model-checking for real-time systems LICS 1990 Los Alamitos IEEE Computer Society 414-425

[3]

Alur R., Courcoubetis C., Halbwachs N., Henzinger T.A., Ho P.H., Nicollin X., Olivero A., Sifakis J., and Yovine S.The algorithmic analysis of hybrid systemsTheor. Comput. Sci.199513813-34doi:10.1016/0304-3975(94)00202-T

[4]

Anai H. and Weispfenning V.Benedetto M.D.D. and Sangiovanni-Vincentelli A.L.Reach set computations using real quantifier eliminationHSCC, LNCS, vol. 20342001BerlinSpringer63-76doi:10.1007/3-540-45351-2_9

[5]

Asarin E., Dang T., and Girard A.Maler O. and Pnueli A.Reachability analysis of nonlinear systems using conservative approximationHybrid Systems: Computation and Control, 6th International Workshop, HSCC 2003 Prague, Czech Republic, April 3–5, 2003, Proceedings, LNCS, vol. 26232003BerlinSpringer20-35doi:10.1007/3-540-36580-X_5

[6]

Beckert B. D’Agostino M., Gabbay D., Hähnle R., and Posegga J. Equality and other theories Handbook of Tableau Methods 1999 Deventer Kluwer

[7]

Beckert B., Hähnle R., and Schmitt P.H. Verification of Object-Oriented Software: The KeY Approach, LNCS, vol. 4334 2007 Berlin Springer

[8]

Beckert B. and Platzer A. Furbach U. and Shankar N. Dynamic logic with non-rigid functions: a basis for object-oriented program verification IJCAR, LNCS, vol. 4130 2006 Berlin Springer 266-280

[9]

Branicky, M.S.: Studies in hybrid systems: modeling, analysis, and control. Ph.D. thesis, Dept. Elec. Eng. and Computer Sci., Massachusetts Inst. Technol., Cambridge, MA (1995)

[10]

Branicky M.S.Universal computation and other capabilities of hybrid and continuous dynamical systemsTheor. Comput. Sci.1995138167-100doi:10.1016/0304-3975(94)00147-B

[11]

Branicky M.S., Borkar V.S., and Mitter S.K.A unified framework for hybrid control: model and optimal control theoryIEEE Trans. Automat. Contr.199843131-45doi:10.1109/9.654885

[12]

Chaochen Z., Ji W., and Ravn A.P. Alur R., Henzinger T.A., and Sontag E.D. A formal description of hybrid systems Hybrid Systems, LNCS, vol. 1066 1995 Berlin Springer 511-530

[13]

Chutinan A. and Krogh B.H.Computational techniques for hybrid system verificationIEEE Trans. Automat. Contr.200348164-75doi:10.1109/TAC.2002.806655

[14]

Clarke E.M., Fehnker A., Han Z., Krogh B.H., Ouaknine J., Stursberg O., and Theobald M. Abstraction and counterexample-guided refinement in model checking of hybrid systems Int. J. Found. Comput. Sci. 2003 14 4 583-604

[15]

Clarke E.M., Grumberg O., and Peled D.A. Model Checking 1999 Cambridge MIT

[16]

Collins G.E. and Hong H. Partial cylindrical algebraic decomposition for quantifier elimination J. Symb. Comput. 1991 12 3 299-328

[17]

Cook S.A.Soundness and completeness of an axiom system for program verificationSIAM J. Comput.19787170-90doi:10.1137/0207005

[18]

Damm W., Hungar H., and Olderog E.R. Verification of cooperating travel agents Int. J. Control 2006 79 5 395-421

[19]

Damm W., Mikschl A., Oehlerking J., Olderog E.R., Pang J., Platzer A., Segelken M., and Wirtz B. Jones C.B., Liu Z., and Woodcock J. Automating verification of cooperation, control, and design in traffic applications Formal Methods and Hybrid Real-Time Systems, LNCS, vol. 4700 2007 Berlin Springer 115-169

[20]

Davoren J.M.Antsaklis P.J., Kohn W., Lemmon M.D., Nerode A., and Sastry S.On hybrid systems and the modal μ-calculusHybrid Systems, LNCS, vol. 15671997BerlinSpringer38-69doi:10.1007/3-540-49163-5_3

[21]

Davoren J.M. and Nerode A.Logics for hybrid systemsProc. IEEE2000887985-1010doi:10.1109/5.871305

[22]

Dershowitz N. and Manna Z.Proving termination with multiset orderingsCommun. ACM1979228465-476doi:10.1145/359138.359142

[23]

Dowek G., Hardin T., and Kirchner C. Theorem proving modulo J. Autom. Reason. 2003 31 1 33-72

[24]

Emerson E.A. and Clarke E.M. Using branching time temporal logic to synthesize synchronization skeletons Sci. Comput. Program. 1982 2 3 241-266

[25]

Emerson E.A. and Halpern J.Y. “Sometimes” and “Not Never” revisited: on branching versus linear time temporal logic J. Assoc. Comput. Mach. 1986 33 1 151-178

[26]

Fitting M. First-Order Logic and Automated Theorem Proving 1996 2 New York Springer

[27]

Fitting M. and Mendelsohn R.L. First-Order Modal Logic 1999 Norwell Kluwer

[28]

Fränzle M. Flum J. and Rodríguez-Artalejo M. Analysis of hybrid systems: an ounce of realism can save an infinity of states CSL, LNCS, vol. 1683 1999 Berlin Springer 126-140

[29]

Frehse G.Morari M. and Thiele L.PHAVer: algorithmic verification of hybrid systems past HyTechHSCC, LNCS, vol. 34142005BerlinSpringer258-273doi:10.1007/b106766

[30]

Giese M.Goré R., Leitsch A., and Nipkow T.Incremental closure of free variable tableauxIJCAR, LNCS, vol. 20832001BerlinSpringer545-560doi:10.1007/3-540-45744-5_46

[31]

Gödel K.Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme IMon.hefte Math. Phys.193138173-198doi:10.1007/BF01700692

[32]

Graça D.S., Campagnolo M.L., and Buescu J. Computability with polynomial differential equations Adv. Appl. Math. 2007 40 330-349

[33]

Hähnle R. and Schmitt P.H.The liberalized δ-rule in free variable semantic tableauxJ. Autom. Reason.1994132211-221doi:10.1007/BF00881956

[34]

Harel D. First-Order Dynamic Logic 1979 New York Springer

[35]

Harel D., Kozen D., and Tiuryn J. Dynamic Logic 2000 Cambridge MIT

[36]

Henzinger T.A. The theory of hybrid automata LICS 1996 Los Alamitos IEEE Computer Society 278-292

[37]

Henzinger T.A., Nicollin X., Sifakis J., and Yovine S. Symbolic model checking for real-time systems LICS 1992 Los Alamitos IEEE Computer Society 394-406

[38]

Hutter D., Langenstein B., Sengler C., Siekmann J.H., Stephan W., and Wolpers A. Gaudel M.C. and Woodcock J. Deduction in the verification support environment (VSE) FME, LNCS, vol. 1051 1996 Berlin Springer 268-286

[39]

Jifeng H. Roscoe A.W. From CSP to hybrid systems A Classical Mind: Essays in Honour of C. A. R. Hoare 1994 Hertfordshire Prentice Hall 171-189

[40]

Kesten Y., Manna Z., and Pnueli A.Verification of clocked and hybrid systemsActa Inf.20003611837-912doi:10.1007/s002360050177

[41]

Lafferriere G., Pappas G.J., and Yovine S. Vaandrager F.W. and van Schuppen J.H. A new class of decidable hybrid systems HSCC, LNCS, vol. 1569 1999 Berlin Springer 137-151

[42]

Manna Z. and Sipma H.Henzinger T.A. and Sastry S.Deductive verification of hybrid systems using STePHSCC, LNCS, vol. 13861998BerlinSpringer305-318doi:10.1007/3-540-64358-3_47

[43]

Morayne M. On differentiability of Peano type functions Colloq. Math. 1987 LIII 129-132

[44]

Mysore V., Piazza C., and Mishra B. Peled D. and Tsay Y.K. Algorithmic algebraic model checking II: Decidability of semi-algebraic model checking and its applications to systems biology ATVA, LNCS, vol. 3707 2005 Berlin Springer 217-233

[45]

Perko L. Differential equations and dynamical systems 1991 New York Springer

[46]

Platzer, A.: Combining deduction and algebraic constraints for hybrid system analysis. In: Beckert, B. (ed.) VERIFY’07 at CADE, Bremen, Germany, CEUR Workshop Proceedings, vol. 259, pp. 164–178. CEUR-WS.org (2007)

[47]

Platzer A. Olivetti N. Differential dynamic logic for verifying parametric hybrid systems TABLEAUX, LNCS, vol. 4548 2007 Berlin Springer 216-232

[48]

Platzer A. Artëmov S.N. and Nerode A. A temporal dynamic logic for verifying hybrid system invariants LFCS, LNCS, vol. 4514 2007 Berlin Springer 457-471

[49]

Platzer A. and Clarke E.M. Bemporad A., Bicchi A., and Buttazzo G. The image computation problem in hybrid systems model checking HSCC, LNCS, vol. 4416 2007 Berlin Springer 473-486

[50]

Pnueli A. The temporal logic of programs FOCS 1977 Piscataway IEEE 46-57

[51]

Pratt V.R. Semantical considerations on Floyd-Hoare logic FOCS 1976 Piscataway IEEE 109-121

[52]

Rönkkö M., Ravn A.P., and Sere K. Hybrid action systems Theor. Comput. Sci. 2003 290 1 937-973

[53]

Sibirsky K.S. Introduction to Topological Dynamics 1975 Leyden Noordhoff

[54]

Tarski A. A Decision Method for Elementary Algebra and Geometry 1951 2 Berkeley University of California Press

[55]

Tavernini L.Differential automata and their discrete simulatorsNonlinear Anal.1987116665-683doi:10.1016/0362-546X(87)90034-4

[56]

Tinelli C. Cooperation of background reasoners in theory reasoning by residue sharing J. Autom. Reason. 2003 30 1 1-31

[57]

Tiwari A.Maler O. and Pnueli A.Approximate reachability for linear systemsHybrid Systems: Computation and Control, 6th International Workshop, HSCC 2003 Prague, Czech Republic, April 3–5, 2003, Proceedings, LNCS, vol 26232003BerlinSpringer514-525doi:10.1007/3-540-36580-X_37

[58]

Walter W. Ordinary Differential Equations 1998 Berlin Springer

[59]

Zhou C., Ravn A.P., and Hansen M.R. Grossman R.L., Nerode A., Ravn A.P., and Rischel H. An extended duration calculus for hybrid real-time systems Hybrid Systems, LNCS, vol. 736 1992 Berlin Springer 36-59

Cited By

Fard MSarjoughian H(2024)A knowledge interchange broker composition modeling framework for simulating water, energy, and water-energy nexus systemsSimulation10.1177/00375497241233783100:7(657-682)Online publication date: 1-Jul-2024
https://dl.acm.org/doi/10.1177/00375497241233783
Chen Jde Mendonça JAyele BBekele BJalili SSharma PWohlfeil NZhang YJeannin J(2024)Synchronous Programming with Refinement TypesProceedings of the ACM on Programming Languages10.1145/36746578:ICFP(938-972)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674657
White LTitolo LSlagel JMuñoz CTimany ATraytel DPientka BBlazy S(2024)A Temporal Differential Dynamic Logic Formal EmbeddingProceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3636501.3636943(162-176)Online publication date: 9-Jan-2024
https://dl.acm.org/doi/10.1145/3636501.3636943
Show More Cited By

Index Terms

Differential Dynamic Logic for Hybrid Systems

Index terms have been assigned to the content through auto-classification.

Recommendations

Differential Dynamic Logic for Verifying Parametric Hybrid Systems
TABLEAUX '07: Proceedings of the 16th international conference on Automated Reasoning with Analytic Tableaux and Related Methods

We introduce a first-order dynamic logic for reasoning about systems with discrete and continuous state transitions, and we present a sequent calculus for this logic. As a uniform model, our logic supports hybrid programs with discrete and differential ...
Sequential Dynamic Logic

We introduce a substructural propositional calculus of Sequential Dynamic Logic that subsumes a propositional part of dynamic predicate logic, and is shown to be expressively equivalent to propositional dynamic logic. Completeness of the calculus with ...
Towards a Hybrid Dynamic Logic for Hybrid Dynamic Systems

We introduce a hybrid variant of a dynamic logic with continuous state transitions along differential equations, and we present a sequent calculus for this extended hybrid dynamic logic. With the addition of satisfaction operators, this hybrid logic ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Journal of Automated Reasoning

Journal of Automated Reasoning Volume 41, Issue 2

Aug 2008

91 pages

ISSN:0168-7433

Issue’s Table of Contents

© The Author(s) 2021. corrected publication 2021.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 August 2008

Accepted: 27 June 2008

Received: 23 August 2007

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

136
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Fard MSarjoughian H(2024)A knowledge interchange broker composition modeling framework for simulating water, energy, and water-energy nexus systemsSimulation10.1177/00375497241233783100:7(657-682)Online publication date: 1-Jul-2024
https://dl.acm.org/doi/10.1177/00375497241233783
Chen Jde Mendonça JAyele BBekele BJalili SSharma PWohlfeil NZhang YJeannin J(2024)Synchronous Programming with Refinement TypesProceedings of the ACM on Programming Languages10.1145/36746578:ICFP(938-972)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674657
White LTitolo LSlagel JMuñoz CTimany ATraytel DPientka BBlazy S(2024)A Temporal Differential Dynamic Logic Formal EmbeddingProceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3636501.3636943(162-176)Online publication date: 9-Jan-2024
https://dl.acm.org/doi/10.1145/3636501.3636943
Blohm PFränzle MHerber PKröger PRemke A(2024)Towards Probabilistic Contracts for Intelligent Cyber-Physical SystemsLeveraging Applications of Formal Methods, Verification and Validation. Specification and Verification10.1007/978-3-031-75380-0_3(26-47)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-75380-0_3
Platzer A(2024)The Significance of Symbolic Logic for Scientific EducationFormal Methods Teaching10.1007/978-3-031-71379-8_1(3-22)Online publication date: 10-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71379-8_1
Adelt JMensing RHerber P(2024)Reusable Specification Patterns for Verification of Resilience in Autonomous Hybrid SystemsFormal Methods10.1007/978-3-031-71177-0_14(208-228)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71177-0_14
Lercher FAlthoff M(2024)Using Four-Valued Signal Temporal Logic for Incremental Verification of Hybrid SystemsComputer Aided Verification10.1007/978-3-031-65633-0_12(259-281)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65633-0_12
Slagel JWhite LDutle AMuñoz CCrespo N(2024)A Formal Verification Framework for Runtime AssuranceNASA Formal Methods10.1007/978-3-031-60698-4_19(322-328)Online publication date: 4-Jun-2024
https://dl.acm.org/doi/10.1007/978-3-031-60698-4_19
Wetzlinger MKochdumper NBak SAlthoff M(2023)Fully-Automated Verification of Linear Systems Using Reachability Analysis with Support FunctionsProceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control10.1145/3575870.3587121(1-12)Online publication date: 9-May-2023
https://dl.acm.org/doi/10.1145/3575870.3587121
Chong SLanotte RMerro MTini SXiang J(2023)Quantitative Robustness Analysis of Sensor Attacks on Cyber-Physical SystemsProceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control10.1145/3575870.3587118(1-12)Online publication date: 9-May-2023
https://dl.acm.org/doi/10.1145/3575870.3587118
Show More Cited By

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents