• README ⤓ .txt 2026-07-17T121634.146 000000000000720
  Logics whose modalities are indexed by actions, programs, or transitions, so that [α]φ reads "after every execution of α, φ holds." Meaning is given over labelled transition systems and the algebra of actions, making these the modal logics of change and computation.
• Alternating-time Temporal Logic ⤓ .md 2026-08-19T182940.000 000000000018304
  Alur, Henzinger, Kupferman (2002). Strategic reasoning in multi-agent systems. Coalition modalities: ⟨⟨A⟩⟩φ. Agents can enforce properties. Foundation for game-theoretic verification.
• Arrow Logic ⤓ .md 2026-07-15T061749.000 000000000018280
  Venema and others developed arrow logic (1990s). Modal logic of transitions/arrows. Combines aspects of relation algebra and modal logic. Models binary relations as first-class objects. Foundation for dynamic semantics and process algebra connections.
• Dynamic Logic ⤓ .md 2026-08-19T183007.000 000000000027736
  Vaughan Pratt introduced dynamic logic in 1976 ("Semantical considerations on Floyd–Hoare logic"), reading programs as modalities. Fischer and Ladner isolated the propositional fragment PDL, combining modal logic with regular expressions over programs, and settled its complexity (1977, 1979). David Harel developed the first-order theory (1979). Foundational for program verification and reasoning about actions.
• Fixed-Point Logic ⤓ .md 2026-08-19T183036.000 000000000021128
  Fixed-point extensions of first-order logic emerged in 1970s-80s. LFP (least fixed point) and IFP (inflationary fixed point) capture P on ordered structures (Immerman, Vardi). Connects logic and complexity theory. Foundation for descriptive complexity.
• Game Logic ⤓ .md 2026-08-19T182841.000 000000000026792
  Rohit Parikh introduced propositional game logic (1985). Builds on dynamic logic, adding game-theoretic operations. Models strategic interaction where outcomes depend on choices of multiple agents. Connects logic, game theory, and verification. Extended by various researchers for different game-theoretic concepts.
• Kleene Algebra ⤓ .md 2026-07-15T211301.000 000000000012072
  Kozen (1996). Algebraic program logic. Regular operations. Propositional tests. Foundation for program algebra.
• Labelled Deduction ⤓ .md 2026-08-19T182953.000 000000000017912
  Gabbay (1990s). Labels encode semantic information. Worlds as labels in proof system. Relational atoms for accessibility. Uniform proof theory for modal logics.
• Modal Mu-Calculus ⤓ .md 2026-08-19T232002.000 000000000030120
  Dana Scott and Jaco de Bakker used fixed points in program semantics (1969); Park (1969, 1976) on fixpoint induction. Dexter Kozen, "Results on the propositional μ-calculus" (1983), gave the system and its axiomatization; Walukiewicz (1995) proved completeness. The modal mu-calculus combines modal logic with fixed-point operators. Subsumes CTL, LTL, PDL in expressive power. Foundation for model checking algorithms (OBDD-based, game-based).
• PDL Extensions ⤓ .md 2026-08-19T182831.000 000000000014888
  Various (1980s-present). Test-free, deterministic, concurrent PDL. Process logics. Beyond basic PDL. Rich program logics.
• Propositional Dynamic Logic ⤓ .md 2026-07-15T211400.000 000000000016656
  Fischer and Ladner introduced PDL (1979). Modal logic of programs. Combines propositional logic with regular expressions over actions. Foundation for program verification. Decidable fragment of dynamic logic.
• Sabotage Logic ⤓ .md 2026-07-15T061548.000 000000000018592
  Van Benthem introduced sabotage games and logic (2002). Dynamic modality: removing edges from graph. Models adversarial graph modification. Combines modal logic with graph games. Foundation for studying robustness and planning under adversarial conditions.
• CRITERIA ⤓ .txt 2026-07-16T002350.000 000000000009496
  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.