The state machine model in the below figure considers four in-flight states of a small unmanned aerial system (sUAS). The model uses transition probabilities and Linear Temporal Logic (LTL) for the transition from one state to another.

• Flight Path, where the sUAS is following the initial calculated flight path, while also monitoring the environment for external objects that could be located on, or intersecting, the flight path.
• Adjust Path, in which the sUAS is calculating a revised flight path when an object is detected on the initial flight path.
• Corrected Path, which is the sUAS path determined to avoid the risk of collision with the detected objects.
• Collision Path, when the sUAS is not able to avoid the total failure resulted from a collision with an object in the external environment; collision could occur in the case of object non-detection, failed path adjustment, or improper revised (corrected) path.
• a) Derive the invariant(s) for sUAS collision with an external object. Write each invariant(s) such that, if not violated, it will only evaluate to FALSE during system execution. An invariant is a statement that does not change its truth evaluation during system execution. The transitions between the states of the system include probabilities of failure (which are the probabilities of object non-detection) Pfp, Pap, and Pcp, as well as LTL statements that you need to consider when writing the invariant.

  State-Machine Transition Timeline
  Step 1	Step 2	Step 3	Step 4	Step 5	Step 6
  Object	Object Detection	Flight Path	Adjust Path	Corrected Path	Collision
  False	False	False	False	False	False

  For example, the first row (which is given) represents the case in which the sUAS is on the ground (non-operational). There is no object (actually, it is not important if there is any object since the sUAS is non-operational). Since the sUAS is non-operational, the object detection system is not working (not detecting objects) and the sUAS is not on either of the FlightPath, AdjustedPath, or CorrectedPath. So, all of those events and states evaluate to FALSE. Obviously, there is no collision (since again sUAS is non-operational) so the Collision cell evaluates to FALSE as well.

(1 -PfpA (-Object) DI (Plp)A(Object) CollisionPath (Object) FlightPath (1 -PfpA (Object) (Pap)(Object) (Pcp)(Object (1 -Pcp) (Object) Adjust Path (Pap)A(Object) (Pcp)/([Object) CorrectedPath (1 -Pap) (7Object)