Logique Temporelle Linéaire (LTL)

Une logique temporelle interprétée sur des structures de temps linéaires où les formules sont évaluées sur des séquences infinies uniques (chronologies) ; les opérateurs usuels incluent X (suivant), F (éventuellement), G (toujours) et U (jusqu'à).