• 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-07-15T070922.000 000000000015448
  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-07-15T052745.000 000000000026680
  Vaughan Pratt introduced Propositional Dynamic Logic (PDL) in 1976, combining modal logic with regular expressions over programs. David Harel extended it to first-order (1979). Fischer and Ladner analyzed complexity. Foundational for program verification and reasoning about actions.
• Fixed-Point Logic ⤓ .md 2026-07-15T060052.000 000000000020680
  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-07-15T054808.000 000000000025352
  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-17T120407.600 000000000000776
  Kozen (1996). Algebraic program logic. Regular operations. Propositional tests. Foundation for program algebra.
• Labelled Deduction ⤓ .md 2026-07-15T064847.000 000000000017856
  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-07-17T120407.600 000000000000848
  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-07-17T120407.600 000000000000776
  Various (1980s-present). Test-free, deterministic, concurrent PDL. Process logics. Beyond basic PDL. Rich program logics.
• Propositional Dynamic Logic ⤓ .md 2026-07-17T120407.600 000000000000880
  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-17T120407.600 000000000000736
  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.