We use a temporal logic to express desired properties of Process (REF ). Classical temporal logics such as LTL specifications [1]}, however, are interpreted over infinite behaviors (traces), and given the high levels of uncertainty of Process (REF ) (unknown dynamics as well as noise), its infinite behaviors have trivial probabilities. Therefore, we instead employ recently developed LTL over finite traces (LTLf) [2]}, which has the same syntax as LTL but its semantics is defined over finite traces.
