Question

Consider the following requirement: when the cruise-controller is "on," assuming the driver does not issue any further input events, eventually the speed becomes equal to the desired cruising speed and stays equal. Express this requirement in LTL using the variables on, speed, cruiseSpeed, cruise, inc, and dec.

Answer 1

Expressing the given requirement in LTL would involve stating that if the cruise control is activated and no further inputs are given, the vehicle's speed will match and maintain the desired cruising speed.

Step-by-step explanation:

The requirement given can be translated into Linear Temporal Logic (LTL) as follows: if the cruise control is turned on (on) and assuming no other inputs from the driver (like inc for increase speed or dec for decrease speed), the vehicle's speed (speed) will eventually become equal to the desired cruising speed (cruiseSpeed) and remains there. The LTL formula would be: G(on → F(speed = cruiseSpeed)) AND G(on → (speed = cruiseSpeed → G(speed = cruiseSpeed))). What this formula states in LTL is that globally (G), if the cruise control is on, it will eventually (F) reach the cruiseSpeed and will globally remain at cruiseSpeed (stay equal) thereafter.