Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Embedding Differential Dynamic Logic in PVS

J. Tanner Slagel, Mariano Moscato, Lauren White, César A. Muñoz, Swee Balachandran, Aaron Dutle

TL;DR

This paper addresses formal reasoning about hybrid systems by embedding differential dynamic logic (dL) into the PVS theorem prover through Plaidypvs. It defines the syntax and semantics of hybrid programs, encodes the dL sequent calculus as verifiable lemmas in PVS, and provides strategy-based automation to reason about HPs inside PVS, leveraging NASALib for imported mathematical theories. The key contributions are a formally verified embedding of dL's axiom and rule set, a substitution calculus for hybrid programs, and the ability to reason about parametric and class-wide HPs within PVS, enabling meta-reasoning about hybrid systems. This integration expands PVS capabilities for hybrid systems verification with practical NASA-oriented applications, and the authors outline future work on tooling, liveness properties, and more robust ODE handling to enhance usability and reach.

Abstract

Differential dynamic logic (dL) is a formal framework for specifying and reasoning about hybrid systems, i.e., dynamical systems that exhibit both continuous and discrete behaviors. These kinds of systems arise in many safety- and mission-critical applications. This paper presents a formalization of dL in the Prototype Verification System (PVS) that includes the semantics of hybrid programs and dL's proof calculus. The formalization embeds dL into the PVS logic, resulting in a version of dL whose proof calculus is not only formally verified, but is also available for the verification of hybrid programs within PVS itself. This embedding, called Plaidypvs (Properly Assured Implementation of dL for Hybrid Program Verification and Specification), supports standard dL style proofs, but further leverages the capabilities of PVS to allow reasoning about entire classes of hybrid programs. The embedding also allows the user to import the well-established definitions and mathematical theories available in PVS.

Embedding Differential Dynamic Logic in PVS

TL;DR

This paper addresses formal reasoning about hybrid systems by embedding differential dynamic logic (dL) into the PVS theorem prover through Plaidypvs. It defines the syntax and semantics of hybrid programs, encodes the dL sequent calculus as verifiable lemmas in PVS, and provides strategy-based automation to reason about HPs inside PVS, leveraging NASALib for imported mathematical theories. The key contributions are a formally verified embedding of dL's axiom and rule set, a substitution calculus for hybrid programs, and the ability to reason about parametric and class-wide HPs within PVS, enabling meta-reasoning about hybrid systems. This integration expands PVS capabilities for hybrid systems verification with practical NASA-oriented applications, and the authors outline future work on tooling, liveness properties, and more robust ODE handling to enhance usability and reach.

Abstract

Differential dynamic logic (dL) is a formal framework for specifying and reasoning about hybrid systems, i.e., dynamical systems that exhibit both continuous and discrete behaviors. These kinds of systems arise in many safety- and mission-critical applications. This paper presents a formalization of dL in the Prototype Verification System (PVS) that includes the semantics of hybrid programs and dL's proof calculus. The formalization embeds dL into the PVS logic, resulting in a version of dL whose proof calculus is not only formally verified, but is also available for the verification of hybrid programs within PVS itself. This embedding, called Plaidypvs (Properly Assured Implementation of dL for Hybrid Program Verification and Specification), supports standard dL style proofs, but further leverages the capabilities of PVS to allow reasoning about entire classes of hybrid programs. The embedding also allows the user to import the well-established definitions and mathematical theories available in PVS.
Paper Structure (13 sections, 1 theorem, 35 equations, 10 figures)

This paper contains 13 sections, 1 theorem, 35 equations, 10 figures.

Table of Contents

  1. Introduction
  2. Specification of hybrid programs
  3. Environment, real expressions, Boolean expressions
  4. Hybrid programs
  5. Quantified statements about hybrid programs
  6. Embedding differential dynamic logic
  7. dL-sequents
  8. Basic logical and structural rules of dL
  9. Hybrid program rewriting rules
  10. Rules for differential equations
  11. Using Plaidypvs
  12. Related work
  13. Conclusion and future work

Key Result

Lemma $<$dL-rule-name$>$

For all lists of Boolean expressions $\Gamma, \Delta$,

Figures (10)

  • Figure 1: Dubins path modeling an aircraft turning.
  • Figure 2: Propositional dL rules
  • Figure 3: Quantification dL rules
  • Figure 4: Structural dL rules
  • Figure 5: dL proof commands
  • ...and 5 more figures

Theorems & Definitions (8)

  • Example 2.1: Environments, Real and Boolean Expressions
  • Example 2.2: HP
  • Example 2.3: Allruns
  • Lemma $<$dL-rule-name$>$
  • Example 3.1: dL-sequent example
  • Example 3.2: dL-sequent example continued
  • Example 3.3: dL-sequent example continued
  • Example 4.1: Verified connection to Dubins paths