Mathematical Syntax | ASCII Syntax | Effect |
\(x := e\) | x := y; |
discrete assignment of the value of term \(e\) to variable \(x\) (jump) |
\(x := *\) | x := *; |
nondeterministic assignment of an arbitrary real number to \(x\) |
\(x_1'=f_1(x), \ldots x_n'=f_n(x) \& Q\) | {x'=2*y & x >= 0} |
continuous evolution of \(x_i\) along the differential equation system \(x_i' = f_i(x)\) restricted to evolution domain described by formula \(Q\) |
\(\alpha;~\beta\) | x := 5; x := x+1; |
sequential composition where \(\beta\) starts after \(\alpha\) finishes |
\(\alpha \cup \beta\) | x := 5; ++ y := x; |
nondeterministic choice, following either alternative \(\alpha\) or \(\beta\) |
\(\alpha^*\) | {x := x+1;}* |
nondeterministic repetition, repeating \(\alpha\) \(n\) times for any \(n \in \mathbb{N}\) |
The behavior of hybrid systems is specified as a hybrid program, which is a program notation for hybrid systems. 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 \(\theta\) 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: \(p' = v, v' = −B \& v \geq 0\), for instance, characterizes the braking mode of a car with braking force \(B\) that holds within \(v \geq 0\) and stops any time before \(v < 0\). It indicates that the rate of change of the position \(p\) 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 \leq a \leq 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.
From these basic constructs, more complex hybrid programs can be built in KeYmaera similar to regular expressions. The sequential composition \(\alpha;~\beta\) expresses that hybrid program \(\beta\) starts after hybrid program \(\alpha\) finishes. The nondeterministic choice \(\alpha \cup \beta\) expresses alternatives in the behavior of the hybrid system that are selected nondeterministically. Nondeterministic repetition \(\alpha^*\) says that the hybrid program \(\alpha\) repeats an arbitrary number of times, including zero.
Mathematical Syntax | ASCII Syntax | Meaning |
\(e\geq\tilde{e}\) | x^2>=5 | Greater equals comparison: true iff \(x^2\) is at least 5 |
\(\lnot P\) | !(x>=5) | Negation (not), true iff \(P\) is not true |
\(P\wedge Q\) | x<=10 & v>=0 | Conjunction (and), true iff both \(P\) and \(Q\) are true |
\(P\vee Q\) | v<=30 | a<2-b | Disjunction (or), true iff \(P\) is true or \(Q\) is true |
\(P\rightarrow Q\) | x>=10 -> v<=1 | Implication (implies), true iff \(P\) is false or \(Q\) is true |
\(P\leftrightarrow Q\) | x=0 <-> x^2=0 | Biimplication (equivalent), true iff \(P\) and \(Q\) are both true or both false |
\(\forall x\, P\) | \forall x x^2>=0 | Universal quantifier, true if \(P\) is true for all real values of variable \(x\) |
\(\exists x\, P\) | \exists x x^2>x^4 | Existential quantifier, true if \(P\) is true for some real value of variable \(x\) |
\([\alpha] P\) | [x:=x^2;] x>=0 | Box modality: \(P\) is true after all runs of hybrid program \(\alpha\) |
\(\langle\alpha\rangle P\) | <{x:=x+1;}*> x>=10 | Diamond modality: \(P\) is true after at least one run of hybrid program \(\alpha\) |
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
v>=0 & A>0 & B>0 -> [car]v>=0
Functions. /* function symbols cannot change their value */
R A. /* maximum acceleration */
R B. /* maximum braking */
End.
ProgramVariables. /* program variables may change their value over time */
R x. /* position */
R v. /* velocity */
R a. /* current acceleration chosen by controller */
End.
Problem.
v >= 0 & A > 0 & B > 0 /* initial condition */
->
[ /* system dynamics */
{
{a := A; ++ a := 0; ++ a := -B;} /* non-deterministic choice of accelerations */
{x' = v, v' = a & v >= 0} /* differential equation system */
}* @invariant(v >= 0) /* loop repeats transitions */
] v >= 0 /* safety/postcondition */
End.