Reference for Logics and operators

---

Path Quantifiers

---

Path Quantifiers, or first-order logic

Syntax	Operator	Description
A(φ)	All paths	φ holds on all computation paths
E(φ)	Exists path	φ holds on at least one computation path

Temporal Operators

---

Temporal Logic, or TL.

Syntax	Operator	Description
X(φ)	Next	φ holds in the next state
F(φ)	Future/Finally	φ will eventually hold
Globally/Always	G(φ)	φ holds continuously
U(φ)	Until	φ holds until another property is true

Computation Tree Logic

---

Computation Tree Logic (CTL) extends propositional logic with path quantifiers (A, E) combined with temporal operators (X, F, G, U) to reason about branching time structures. One extension is PCTL (Probabilitstic CTL), used in PRISM¹

Computation Tree Logic, or CTL.

Syntax	Operator	Description
AG(φ)	Always globally	φ holds globally on all paths (φ is always true)
EF(φ)	Eventually possible	φ eventually holds on some path (φ is possibly true)
AX(φ)	Next on all paths	φ holds in the next state on all paths
AF(φ)	Always eventually	φ eventually holds on all paths (φ is inevitable)
EG(φ)	Possibly always	φ holds globally on some path (φ can remain true forever)

Dynamic Epistemic Logic

---

Dynamic Epistemic Logic, or DEL. See also encyclopedia of philosophy entry.

Epistemic Logic formalizes reasoning about knowledge and belief, where the basic knowledge operator K(i, φ) satisfies axioms like: if K(i, φ) then φ (knowledge implies truth).

Common Knowledge (GCK) is particularly important as it represents infinite mutual knowledge - not only does everyone know φ, but everyone knows that everyone knows φ, recursively.

Syntax	Operator	Description
K(i, φ)	Knowledge	Agent i knows proposition φ
GK(G, φ)	Group Knowledge	Every agent in group G knows φ
GCK(G, φ)	General Common Knowledge	Common knowledge among group G that φ (everyone knows, everyone knows that everyone knows, etc. infinitely)
DK(G, φ)	Distributed Knowledge	Group G collectively has enough information to deduce φ, even if no individual agent knows φ

Public Announcement Logic

---

Public Announcement Logic is a DEL extension growing in popularity.

Syntax	Operator	Description
PAL(φ, ψ)	Knowledge/Belief updates	After φ is truthfully announced, ψ holds

Strategic Logic

---

(Alternating-time temporal logic) , or ATL

Alternating-time Temporal Logic (ATL) quantifies over strategies rather than just paths, allowing coalitions to guarantee outcomes regardless of opponents' actions.

Syntax	Operator	Description
<group1>F(φ)	Strategic Eventually	The coalition "Group" has a strategy to eventually make φ true
<group1>G(φ)	Strategic Always	The coalition can maintain φ forever
<group1>X(φ)	Strategic Next	The coalition can make φ true in the next step

Obligation Logic

---

Deontic Logic, aka DL, deals with obligations or "colors".

Operator	Syntax	Description
O(φ)	Obligation	φ is an obligation

Since partitioning predicates as either "obliged" or "permissible" is a simple enrichment to true/false, there's lots of ways to frame this and interpret it.
ISPL calls this "RedStates" and "GreenStates", and introduces reserved keywords for each Agent to express more complex requirements.

References

---