|
⇓ Download ⇓
or get Source and read Book and watch Videos and follow Tutorial |
Introduction
The definitions package enables the use of any function definable as the solution of a system of ordinary differential equations (ODEs) within hybrid system models and proofs in KeYmaera X.
The package is available as of the KeYmaera X 5.0 major release.
References
The package features are described in the IJCAR'22 paper.
-
James Gallicchio, Yong Kiam Tan, Stefan Mitsch and André Platzer.
Implicit definitions with differential equations for KeYmaera X (System Description).
In Jasmin Blanchette, Laura Kovacs and Dirk Pattinson, editors, Automated Reasoning, International Joint Conference, IJCAR 2022, Haifa, Israel, August 7-12, 2022, Proceedings. volume 13385 of LNCS, pp. 723-733. Springer, 2022. © The authors
[bib | ⧉ | pdf | doi | mypdf | slides | arXiv]
Usage Examples
This section gives a brief guide to exploring and using the package, please see the KeYmaera X Tutorial for an in-depth usage guide of KeYmaera X.
To begin, click on the Import button for IJCAR22 Implicit Definitions Examples to load pre-defined example models.
You should now see a IJCAR22 subfolder containing a number of examples.
Discretely driven swing
The paper uses a discretely driven swing as a running example (see Sections 2-4).
- Click on the Discretely Driven Swing model to inspect the associated model.
- (Optional) Click Load Proof to run a stored proof for this model. The proof should be checked successfully and you will be brought to a success page.
- Return to the Discretely Driven Swing model and click New Proof. This brings up the KeYmaera X interactive proof interface.
- Begin the proof by clicking Unfold to apply automatic unfolding steps.
- Next, right-click on the formula in the succedent (right side of turnstile). You will now see a menu of common proof steps to apply.
- Select Loop Invariant and enter the following choice of invariant for J, which expresses that the total energy of the system is bounded above and the swing is kept below the horizontal:
- Init: Hover over the turnstile and click on the calculator button to call the arithmetic solver.
- Post: Click on Prop to finish the proof propositionally.
- Step: Click on Unfold again to automatically unfold the hybrid program model.
- This should complete the proof of the discretely driven swing model.
g/L*(1-cos(theta))+1/2*w^2 < g/L & -pi()/2 < theta & theta < pi()/2
You should now see three subgoals: Init, Post, and Step corresponding to the premises that need to be proved when reasoning with loop invariants.
This should result in two subgoals, corresponding to whether the push p is allowed or not.
For both subgoals, right-click on the formula in the succedent and select ODE Auto to finish the proof using KeYmaera X's ODE automation.
Defining and using custom functions
Users can declare new differentially-defined functions with the following sugared syntax in the definitions block (see Section 3):
implicit Real h(Real t) = {{initial condition}; {ODE}}
The initial condition for time t defaults to t:=0 if it is not specified.
The package defines default builtin functions exp, sin, and cos.
- Open the Arctan Identity model, which defines arctan and tan in the definitions block:
- Start the proof as before and right click on the succedent to expand the definitions of tan and arctan.
- Select diffUnfold to prove a property of these special functions by their differential unfolding (see Section 3.2).
- You should see three subgoals. The first subgoal at v=0 should prove arithmetically. The latter two subgoals prove automatically by ODE Auto.
- Definitions are parsed in order so that later implicit definitions can refer to earlier (implicit) definitions.
- The identity exp2(x) = exp(exp(x)) can be proved similarly to the arctangent identity, by first proving the identity exp1(x) = exp(x).
- The associated proof can be ran with Load Proof.
Definitions
implicit Real arctan(Real t) = {{arctan:=0;t:=0;}; {arctan'=1/(1+t^2),t'=1}};
Real tan(Real x) = sin(x)/cos(x);
Real x;
End.
Problem
arctan(tan(x)) = x
End.
Input 0 for t0 and x for v0 to prove the property starting at v=0 and evolving v forwards or backwards until reaching v=x.
For example, open the Double Iterated Exponential model, which defines an iterated exponential exp2:
Definitions
implicit Real exp1(Real t) = {{exp1:=1;}; {exp1'=exp1}};
Real E = exp1(1);
implicit Real exp2(Real t) = {{exp2:=E;t:=0;}; {exp2'=exp1(t)*exp2,t'=1}};
Real x;
End.
Problem
exp2(x) = exp(exp(x))
End.
Other examples
Additional example models that use various other features of KeYmaera X are described in the paper (Section 4 and Appendix B). These examples are included in the package.
As above, you can inspect the models, attempt your own proofs, and check their associated proofs using Load Proof
The (alphabetical) list of models is as follows:
- Arctan Identity: arctan is left-inverse of tan.
- Bouncing Ball on a Sine Curve: models a ball inelastically colliding with a sinusoidal surface.
- Discretely Driven Swing: the toy running example swing from the paper draft.
- Double Iterated Exponential: defines exp2 and proves exp2(x) = exp(exp(x)).
- Khalil Exercise 2.28 and 3.14 models interactions between two neurons.
- Robot Collision Avoidance Passive Orientation Safety and Static Safety models a robot collision avoidance problem.
Important: please ensure that the models and proofs are ran in following order because they need preceding models as lemmas, respectively:
Run Khalil Exercise 2.28 and 3.14 (tanh^2 < 1), then Khalil Exercise 2.28 and 3.14 (bound), and finally Khalil Exercise 2.28 and 3.14.
 |
Any opinions, findings, and conclusions or recommendations expressed are those of the author(s) and do not necessarily reflect the views of any sponsoring institution.