Atomic Proposition	S0	S1	S2	S3..∞	+
P
Formula	S0	S1	S2	S3..∞
next(P)					Remove

Syntax Cheatsheet

Concept	Description	Examples
Atomic propositions	Symbolic names (uppercase letters) that are either true or false in a state.	A B
Logical connectives	Operators from propositional logic.	not(A) and(A, B) or(A, B, C) implies(A, B)
Temporal operators	Operators that deal with time.	next(A) eventually(B) always(C) until(A, B)