• README ⤓ .txt 2026-10-22T165042.936 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-10-22T165042.936 000000000000912
  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-10-22T090058.000 000000000038552
  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-20T083225.000 000000000044784
  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-10-22T085923.000 000000000045824
  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-20T075111.000 000000000040168
  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 with Tests ⤓ .md 2026-08-20T025917.000 000000000046272
  Kleene (1956) introduced regular events; Conway (1971) gave the algebraic treatment. Dexter Kozen's "A completeness theorem for Kleene algebras and the algebra of regular events" (1994) fixed the axioms now standard, and "Kleene algebra with tests" (TOPLAS, 1997) added the Boolean subalgebra that turns the structure into a program logic. Kozen and Smith (1996) established the free model; Kozen (2000) showed KAT subsumes propositional Hoare logic.
• Kleene Algebra ⤓ .md 2026-08-20T025917.000 000000000046272
  Kleene (1956) introduced regular events; Conway (1971) gave the algebraic treatment. Dexter Kozen's "A completeness theorem for Kleene algebras and the algebra of regular events" (1994) fixed the axioms now standard, and "Kleene algebra with tests" (TOPLAS, 1997) added the Boolean subalgebra that turns the structure into a program logic. Kozen and Smith (1996) established the free model; Kozen (2000) showed KAT subsumes propositional Hoare logic.
• Labelled Deduction ⤓ .md 2026-08-20T030340.000 000000000037536
  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-20T030722.000 000000000049264
  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-10-22T165042.936 000000000000776
  The family grew from Fischer and Ladner's PDL (1979) as researchers asked which program constructors could be added without losing decidability. Ben-Ari, Halpern and Pnueli (1982) settled deterministic PDL; Berman and Paterson (1981) proved tests are not eliminable; Streett (1982) handled looping and converse; Harel, Pnueli and Stavi (1983) showed where non-regular programs lead; Lange and Lutz (2005) fixed the cost of intersection. Parikh's game logic (1985) is the branch in which a second player appears.
• Propositional Dynamic Logic ⤓ .md 2026-08-20T032946.000 000000000039128
  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-08-20T032726.000 000000000039216
  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.