Mathematical Syntax | ASCII Syntax | Effect |
x := e | x := x*y+1; |
discrete assignment of the value of term e to variable x (jump) |
x := * | x := *; |
nondeterministic assignment of an arbitrary real number to x |
x1'=f1(x), ... xn'=fn(x) & Q | {x'=2*y & x >= 0} |
continuous evolution of x along the differential equation system x'=2*y
restricted to evolution domain described by formula x >= 0 |
α ; β | v := 5; {x'=v} |
sequential composition where β starts after α finishes |
α ∪ β | x := 0; ++ x := x+1; |
nondeterministic choice, following either alternative α or β |
α* | {x := x+1;}* |
nondeterministic repetition, repeating α n times for any n ∈ ℕ |
The syntax of hybrid programs is shown together with an informal semantics in the table above. The basic terms
(called e
in the table) are either rational number constants, real-valued variables or (possibly
nonlinear) polynomial or rational arithmetic expressions built from those.
The effect of x := e
is an instantaneous discrete jump
assigning the value of e
to the variable x. The term e
can be an arbitrary polynomial.
The controller could, for example, assign braking power -B
to the acceleration
by the assignment a := -B
when using brakes of force B>0
.
The effect of x' = f(x) & Q
is an ongoing continuous evolution
controlled by the differential equation x' = f(x)
that
is restricted to remain within the evolution domain Q,
which is a formula of real arithmetic over unprimed variables.
The evolution is allowed to stop at any point in Q
but it must not leave Q. Systems of differential equations
and higher-order derivatives are defined accordingly:
{x' = v, v' = -B & v ≥ 0}
, for instance, characterizes
the braking mode of a car with braking force B
that
holds within v ≥ 0
and stops any time before v < 0
.
It indicates that the rate of change of the position x is given by the velocity v
, which in turn changes at the rate -B
.
For discrete control, the test action ?F
(read as "assume
F") is used as a condition statement. It succeeds
without changing the state if F
is true in the current
state, otherwise it aborts all further evolution. For example,
a car controller can check whether the chosen acceleration
is within physical limits by ?(-B ≤ a ≤ A)
.
If a computation branch does not satisfy this condition,
that branch is discontinued and aborts. From a modeling
perspective, tests should only fail if a branch is not
possible in the original system, as it will no longer be
possible in the model of the system. Therefore, during
verification we consider only those branches of a system
where all tests succeed.
For example, a := *; ?(-B ≤ a ≤ A)
first assigns any arbitrary real number to a
, but then subsequently tests that a
is in between -B
and A
. This combination ensures that a
is changed to any arbitrary real number within this range.
From these basic constructs, more complex hybrid
programs can be built in KeYmaera similar to regular
expressions. The sequential composition α ; β
expresses
that hybrid program β
starts after hybrid program α
finishes. The nondeterministic choice
α ∪ β
expresses alternatives in the behavior of the hybrid
system that are selected nondeterministically. Nondeterministic
repetition α*
says that the hybrid program α
repeats an arbitrary number of times, including zero.
Mathematical Syntax | ASCII Syntax | Meaning |
e ≥ t | x^2>=y+1 | Greater equals comparison: true iff value of t is at least t |
e = t | x^2=y+1 | Equality comparison: true iff value of t and t equal |
¬ P | !(x>=5) | Negation (not), true iff P is not true |
P ∧ Q | x<=10 & v>=0 | Conjunction (and), true iff both P and Q are true |
P ∨ Q | v<=30 | a<2-b | Disjunction (or), true iff P is true or Q is true |
P → Q | x>=10 -> v<=1 | Implication (implies), true iff P is false or Q is true |
P ⟷ Q | x=0 <-> x^2=0 | Biimplication (equivalent), true iff P and Q are both true or both false |
∀x P | \forall x x^2>=0 | Universal quantifier, true if P is true for all real values of variable x |
∃x P | \exists x x^2>x^4 | Existential quantifier, true if P is true for some real value of variable x |
[α]P | [x:=x^2;] x>=0 | Box modality: P is true after all runs of hybrid program α |
<α>P | <{x'=5}> x>=10 | Diamond modality: P is true after at least one run of hybrid program α |
Formulas of differential dynamic logic (dL), with typical names P and Q, are defined by the syntax shown above. The basic idea for dL formulas is to have formulas of the form [α]φ to specify that the hybrid system α always remains within region P, i.e., all states reachable by following the transitions of hybrid system α statisfy the formula P. Dually, the dL formula <α>P expresses that the hybrid system α is able to reach region P, i.e., there is a state reachable by following the transitions of hybrid system α that satisfies the formula P. In either case, the hybrid system α is given as a full operational model in terms of a hybrid program. Using other propositional connectives, one can state the following dL formula
P → [α]Q
v>=0 & A>0 & B>0 -> [car]v>=0
This is an example of a .kyx
model file that can be loaded into KeYmaera X.
Definitions /* function symbols cannot change their value */
Real A; /* maximum acceleration constant of arbitrary value */
Real B; /* maximum braking constant of arbitrary value */
End.
ProgramVariables /* program variables may change their value over time */
Real x; /* position of a point moving along a straight line */
Real v; /* velocity */
Real a; /* current acceleration chosen by controller */
End.
Problem /* The differential dynamic logic formula to prove */
v >= 0 & A > 0 & B > 0 /* initial condition */
-> /* implies that */
[ /* all behavior of hybrid program: */
{ /* system dynamics */
{a := A; ++ a := 0; ++ a := -B;} /* non-deterministic acceleration choice */
{x' = v, v' = a & v >= 0} /* differential equation system in v>=0 */
}* @invariant(v >= 0) /* loop repeats transitions */
] v >= 0 /* satisfies safety/postcondition */
End.