PLTL
Propositional Linear Temporal Logic