Linear temporal logic

https://en.wikipedia.org/wiki/Linear_temporal_logic

Language:

• P - a set of propositional variables. It includes T (true) and ⊥ (false).
• Connectives: ∧, v, ¬, →, ←→, ◇, ◻, O (next), U (until)
• brackets: (, )

What is L_{LTL}(P):

P

In this case we assume that our frame is (N, ≤)

Motivation: N - time

dp i O p → dp U p