Loading...

Tutorial: Discover Constraints Using KeYmaera

320 views

Loading...

Loading...

Transcript

The interactive transcript could not be loaded.

Loading...

Rating is available when the video has been rented.
This feature is not available right now. Please try again later.
Published on Oct 19, 2013

EDIT: In order to discover constraints in KeYmaera, you must go to the advanced options tab and disable "Universal Closure on QE". You are advised to turn this back on when done, as it is very useful for proving properties that are true.
____________________________________________________

This video is part of a tutorial series for the Theorem Prover KeYmaera.
http://symbolaris.com/info/KeYmaera.html
____________________________________________________

It isn't always the case that the theorem we write down about a particular hybrid system will be provable. In some cases, you may have initial conditions or a loop invariant that are too weak to guarantee the property that you're trying to prove. In these cases, we can interact with KeYmaera to try to discover or synthesize stronger conditions.

Take this simple theorem as an example, where z is the position and v is the velocity of a train. We want to prove that the train does not move beyond a stopping point m if it applies braking force b.

However, we've only assumed that the position of the train is initially behind m, and have no guarantees about its initial velocity. This property won't prove, since the train may be moving too fast to stop in time.

We can load this property in KeYmaera to try to prove it and see what it will give us as open goals. Some of the goals will just be contradictions of the assumptions that we want to make on our system, like assuming velocity is negative or the train is already past point m. However, looking through the cases may yield a formula that does not contradict your assumptions. This may be the constraint you need.

Copy this formula to the initial conditions in your .key file. This formula may have a strange format because it is what is returned by Quantifier Elimination. By rewriting the formula, we discover that it can be derived from standard kinematic equations and that it requires the initial distance be greater than the stopping distance of the train.

Loading...

When autoplay is enabled, a suggested video will automatically play next.

Up next


to add this to Watch Later

Add to

Loading playlists...