INCLUSION CRITERIA
An entry belongs in this subdivision if and only if its modalities are indexed by actions, programs, or transitions, interpreted over labelled transition systems or a relational algebra of actions.
Required: At least one of the following:
- Program or action modalities [α]/⟨α⟩ with a transition semantics
- An algebra of actions (Kleene algebra, arrow logic) with a defined consequence relation
- A fixed-point or game extension of a program logic
Not sufficient: A single alethic modality (Alethic), a purely temporal flow with until/next (Temporal), a normative operator (Deontic).
Boundary: The modal μ-calculus lives here by the third clause and is cross-listed with Temporal (which it subsumes), with Applications/Verification (where it is model-checked), and with Applications/Game (where parity games decide it). Temporal logics belong in Temporal even though time is dynamic; PDL-style program modalities belong here. Program logics for correctness (Hoare, separation) belong in Applications/Verification; the propositional dynamic logics they build on live here. The μ-calculus appears here (PDL setting) and in Temporal and Verification by use.