LTL
Linear Temporal Logic