{Testing Linear Temporal Logic Formulae on Finite Execution Traces}