Besides the textbook, more information on the input syntax can be found on the Wiki

Hybrid Programs

grammar The behavior of hybrid systems is specified as a hybrid program, which is the programming language for hybrid systems.
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.

Differential Dynamic Logic

grammar Differential dynamic logic can specify and verify the behavior of hybrid programs.
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
which expresses that, if hybrid program α initially starts in a state satisfying P, then it always remains in the region characterized by Q. This dL formula expresses a safety contract for hybrid system α namely that the system always is in Q when it initially starts in P. For instance, the following dL formula expresses that for the state of a car controller car, the property x≤m always holds true when starting in a state where v>=0 and A≥0 and B>0 are true:
v>=0 & A>0 & B>0 -> [car]v>=0
In this model x is the position of the car, v the velocity of the car, B its braking power, and A its maximum acceleration.

Example

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.

More Information

Compendia