Temporal Logic
Overview
This area tracks the temporal-specification slice of Formal Methods: LTL-style languages, branching-time logics, automata-shaped tasks, monitors, and temporal objectives that constrain learning, verification, and synthesis over time. Broader verification infrastructure belongs in Formal Methods unless the temporal structure is doing the main explanatory work.
Active Questions
- Which temporal fragments are expressive enough for safety without becoming operationally brittle?
- Which safety/co-safety fragments are useful because of finite-prefix semantics, and which remain hard because of realizability complexity?
- When is a problem primarily about temporal specification, and when is it better routed to broader Formal Methods?
- How should temporal specifications be grounded in observations, abstractions, or learned state representations?
- What is the practical boundary between monitoring, masking, and offline synthesis?
- When should temporal synthesis use pure Safety Games, GR(1)-style objectives, or richer Emerson-Lei Objectives?
- When does an LTL safety formula need a centralized joint-action shield versus a factored or distributed construction?
- When can temporal task structure be learned as an automaton rather than specified upfront?
- How can temporal task structure compose through reusable subtask automata?
- How do temporal logics change when agents can revise rules, issue private queries, or carry causal state across time?
- Which temporal safety specifications can be decomposed into local assume-guarantee obligations for multi-agent shields?
- When do finite-trace temporal values serve as strategy-comparison criteria rather than only monitors or automata tasks?
- When do real-time requirements need duration-sensitive interval logics rather than event-order logics alone?
- Which temporal-logic workflows depend on automata-theoretic translations rather than only semantic trace definitions?
- Which temporal-logic workflows are best understood through monadic second-order definability over words or trees?
- When does a specification need linear-time trace semantics, and when does it need branching-time quantification over possible futures?
Key Concepts
- Linear Temporal Logic
- Branching-Time Temporal Logic
- Branching-Time Semantics
- Automata-Theoretic Logic
- Second-Order Logic
- MSO Automata Correspondence
- Safety and Co-Safety Properties
- Safety LTL Automata and Games
- Reactive Synthesis
- Safety Games
- Duration Calculus
- Duration Calculus Pacemaker Shields
- Emerson-Lei Objectives
- Emerson-Lei Game Solving
- Reward Machines
- Reward Machine Learning Methods
- Probabilistic Strategic Timed CTL
- Probabilistic Model Checking
- Runtime Verification
- Shielding
- Centralized and Factored MARL Shielding
- Distributed Shield Synthesis
- Predicate Abstraction
- Non-Markovian Reinforcement Learning
- Automata Learning
- Alternating-Time Temporal Logic
- Dynamic Epistemic Logic
- Temporal Causal Models
- Responsibility Anticipation
Key Sources
- Alshiekh2018 - Safe Reinforcement Learning via Shielding
- Vaananen2024 - Second-Order and Higher-Order Logic
- Hofmann2025 - Automata Theory and Logic
- Goranko2023 - Temporal Logics
- ElSayed-Aly2021 - Safe Multi-Agent Reinforcement Learning via Shielding
- Bartocci2018 - Introduction to Runtime Verification
- Jamroga2026 - Towards Probabilistic Strategic Timed CTL
- Varricchione2024 - Pure-Past Action Masking
- Elsayed-Aly2024 - Distributional Probabilistic Model Checking
- Alinejad2026 - Dynamic Automaton Refinement and Planning for Non-Markovian RL
- Toro Icarte2022 - Reward Machines
- Furelos-Blanco2023 - Hierarchies of Reward Machines
- Brorholt2025 - Compositional Shielding and Reinforcement Learning for Multi-Agent Systems
- Dolgorukov2024 - Dynamic Epistemic Logic of Resource Bounded Information Mining Agents
- Galimullin2025 - Changing the Rules of the Game
- Varricchione2023 - Synthesising Reward Machines for Cooperative MARL
- Gladyshev2025 - Temporal Causal Reasoning with Non-Recursive SEMs
- Parker2024 - Responsibility in a Multi-Value Strategic Setting
- Latvala2002 - Efficient Model Checking of Safety Properties
- Zhu2020 - A Symbolic Approach to Safety LTL Synthesis
- Artale2023 - Complexity of Safety and coSafety Fragments of Linear Temporal Logic
- Hausmann2024 - Symbolic Solution of Emerson-Lei Games for Reactive Synthesis
- Dole2023 - Correct-by-Construction Reinforcement Learning of Cardiac Pacemakers from Duration Calculus Requirements