LTLC: Linear Temporla Logic (LTL) for Control

example: In his example we control a helicopter at near hover speed: A helicopter is flying at 2 m/sec speed. Can we make it stop within 1.6 sec or can we accelerate it to 5 m/sec within 2.5 sec?

system:
    #############################################################
    # input  constraints
    #############################################################

    #elevator position min, max and rate max
    const   pi = 3.141592;
    const   rmin = -pi*20/180, rmax = -rmin, rrmax = pi*10/180;

    #############################################################
    # system dynamics
    #############################################################

    #near hover dynamics
    const   A = [   0.9608,    -0.0005,  -0.0010;
                    0.0980,    1,         0;
                   -0.0888,    0.9790,    0.9981   ],
            B = [   0.6171;
                    0.0311;
                    0.9457  ];

    #x = [pitch rate, pitch angle, velocity]'
    var x[3]: state,
    dr: input ,            #rotor angle
    p: output ,            #pitch angle
    v: output ;            #speed

    x = A * x + B * dr;    #system dynamics
    p = [0, 1, 0] * x;     #pitch angle
    v = [0, 0, 1] * x;     #speed
 
specification:
    output horizon: 25;    #when the system arrive at a steady state
    input  horizon: 24;    #when we stop changing the input

    rp0(t): dr(t) >= rmin; #rotor angle constraint
    rp1(t): dr(t) <= rmax;
    rr0(t): dr(t+1) - dr(t) <=  rrmax; #rotor rate constraint
    rr1(t): dr(t+1) - dr(t) >= -rrmax;

    x0(t): x[0](t) = 0;    #initial pitch angle and pitch rate are 0
    x1(t): x[1](t) = 0;

    vi(t): v(t) = 2;       #initial speed
    vs(t): v(t+16) = 0;    #stop from 1.6sec
    vr(t): v(t) >= 5;      #faster than 5m/sec

    !(    x0 /\ x1 /\
          [] ( rp0 /\ rp1 /\ rr0 /\ rr1 ) /\
          vi /\
          ( [] vs \/ <> [] vr));