Linear Temporal Logic

Also known as LTL

Linear Temporal Logic expresses requirements about how events unfold over time, such as requiring a safety condition to hold until a goal is reached. Common methods translate formulas into automata for controller synthesis, planning, and verification, while progression-based techniques track how requirements evolve during execution. Researchers also study learning specifications from demonstrations or natural language, and integrating temporal constraints into reinforcement learning and robot planning. A central challenge is balancing expressive specifications and rigorous guarantees with the computational cost of automata, while ensuring that learned or translated formulas capture their intended meaning.

Latest papers

32 papers0 papers in the last four weeks, against 2 the four weeks before. 0.0% of all new papers.

Formal Explanations for Linear Temporal Logic over Finite Traces
Oct 26, 2026Valeria Fionda, Antonio Ielo, Francesco RiccaCounterfactual Explanations Linear Temporal Logic
University of Calabria, Italy
Progression- vs Automata-based Anticipatory Monitoring of LTL over Finite Traces (Extended Version)
Sep 26, 2026Sarah Winkler, Toryn Klassen, Sheila McIlraith +1Runtime Verification Linear Temporal Logic
Free University of Bozen-Bolzano, Italy · University of Toronto, Canada
Predictive Varanus: Combining CSP Conformance Monitoring with Predictive LTL Runtime Verification
Sep 15, 2026Angelo Ferrando, Matt Luckcuck, Pedro RibeiroFormal Verification Linear Temporal Logic
Department of Physics, Informatics and Mathematics, University of Modena and Reggio Emilia, Italy · School of Computer Science, University of Nottingham, UK · Department of Computer Science, University of York, UK
Linear Temporal Logic Translation via Human-Inspired Self-Constrained Reasoning for Robot Task Specification
Aug 28, 2026Haofei Hou, Fanxu Meng, Shunyi Zhao +4Constraint-Guided Reasoning in Language Models Linear Temporal Logic
School of Advanced Manufacturing and Robotics, Peking University, Beijing 100871, China. · School of Integrated Circuits, Peking University, Beijing 100871, China.
When Automata Meet Streams: Temporal Logic Compilation for Stream-Based Robotics Task and Motion Planning
Aug 19, 2026Sayem Nazmuz Zaman, Cyrus NearyMotion Planning Linear Temporal Logic
Department of Electrical and Computer Engineering University of British Columbia Vancouver, BC, Canada
Backward through Time, Algebraically
Aug 17, 2026Konstantinos KogkalidisDifferentiable Logic Temporal Logic
Time to Reason: Scalable Neurosymbolic Learning for LTLf via Fuzzy Semantics
Aug 17, 2026Riccardo Andreoni, Andrei Buliga, Alessandro Daniele +4Differentiable Logic Neuro-Symbolic Reasoning
Fondazione Bruno Kessler, Via Sommarive, 18, Trento, 38123, Italy · Free University of Bozen-Bolzano, Via Bruno Buozzi, 1, Bolzano, 39100, Italy · Università di Bologna, Via Mura Anteo Zamboni 7, Bologna, 40126, Italy
Learning Context-Free Grammars for Grammar-Constrained Decoding via Declarative Agentic Programming with Guarantees
Aug 6, 2026Kevin Cheang, Geoff Hulette, Rahul Kumar +5LLM-Based Program Synthesis Linear Temporal Logic
Amazon Web Services · Purdue University
Exact Model-Free Policy Iteration for Co-safe LTL Planning
Aug 5, 2026Zetong Xuan, Yu WangReinforcement Learning Policy Iteration
Department of Mechanical and Aerospace Engineering, University of Florida, Gainesville, FL 32611 USA
Optimal Constrained sc-LTL Planning in MDPs via Switching Policies
Aug 5, 2026Zetong Xuan, Yu WangMarkov Decision Processes Linear Temporal Logic
Department of Mechanical and Aerospace Engineering, University of Florida, Gainesville, FL 32611 USA
Infinite Trace Objectives with Finite Trace Techniques: Translating LTL to LTLf+
Aug 3, 2026Christoph Weinhuber, Maximilian Prokop, Giuseppe De Giacomo +1Temporal Reasoning Formal Verification
University of Oxford · 2Technical University of Munich · 3Masaryk University Brno +1
Learning Linear Temporal Specifications from Demonstrations with Uncertainty
Jul 12, 2026Parastou Fahim, Constantino Lagoa, Rômulo Meira-G'oesFormal Verification Learning from Demonstration
School of Electrical Engineering and Computer Science at The Pennsylvania State University, State College, USA
First-Order Temporal Logic Tensor Networks
Jun 29, 2026Luca Boscarato, Ivan Donadello, Alessandro Artale +2Tensor Networks Logic Tensor Networks
Free University of Bozen-Bolzano
Temporal logics and formal synthesis for robot planning and control
Jun 19, 2026Jana Tumova, Joris Verhagen, Matti VahsRobotics Signal Temporal Logic
KTH Royal Institute of Technology
As You Wish: Mission Planning with Formal Verification using LLMs in Precision Agriculture
Jun 16, 2026Marcos Abel Zuzuárregui, Stefano CarpinLarge Language Model-Based Robot Planning Formal Verification
Department of Computer Science and Engineering, University of California, Merced, CA, USA
Neuro-Symbolic Injection of LTLf Constraints in Autoregressive Reinforcement Learning Policies
Jun 6, 2026Ashkan Ansarifard, Matteo Mancanelli, Elena Umili +1Reinforcement Learning Transformer-Based RL
Sapienza University of Rome · University of Rome La Sapienza, Rome, Italy
Meta-Programming for Linear-time Temporal Answer Set Programming
May 28, 2026Susana Hahn, Amadé Nemes, Javier Romero +1Temporal Reasoning Answer Set Programming
University of Potsdam, Germany · Potassco Solutions, Germany
NeuroNL2LTL: A Neurosymbolic Framework for Natural Language Translation of Linear Temporal Logic
May 20, 2026Paapa Kwesi Quansah, Ernest BonnahFormal Verification Neuro-Symbolic AI
Baylor University, Waco TX 76706, USA
Formal Methods Meet LLMs: Auditing, Monitoring, and Intervention for Compliance of Advanced AI Systems
May 15, 2026Parand A. Alamdari, Toryn Q. Klassen, Sheila A. McIlraithLLM Auditing Formal Verification
University of Toronto, Vector Institute, Canada
Monitoring Data-aware Temporal Properties (Extended Version)
May 14, 2026Alessandro Gianola, Marco Montali, Sarah WinklerFormal Verification Satisfiability Modulo Theories
INESC-ID/Instituto Superior T´ecnico, Universidade de Lisboa, Portugal · Free University of Bozen-Bolzano, Italy
SafeManip: A Property-Driven Benchmark for Temporal Safety Evaluation in Robotic Manipulation
May 12, 2026Chengyue Huang, Khang Vo Huynh, Mellon M. Zhang +3Robot Safety Robotic Manipulation
Department of Machine Learning, Georgia Institute of Technology · Department of Computer Science, University of Virginia
Optimal LTLf Synthesis
May 12, 2026Yujian Cao, Sven Schewe, Qiyi Tang +1Program Synthesis Formal Verification
University of Liverpool
SpecRLBench: A Benchmark for Generalization in Specification-Guided Reinforcement Learning
Apr 27, 2026Zijian Guo, İlker Işık, H. M. Sabbir Ahmad +1RL Benchmarks Reinforcement Learning
Boston University
SemML 2.0: Synthesizing Controllers for LTL
Apr 27, 2026Jan Křetínský, Tobias Meggendorfer, Maximilian ProkopProgram Synthesis Formal Verification
Masaryk University, Brno, Czech Republic · Technical University of Munich, Germany · Lancaster University Leipzig, Germany
Towards Causally Interpretable Wi-Fi CSI-Based Human Activity Recognition with Discrete Latent Compression and LTL Rule Extraction
Apr 24, 2026Luca Cotti, Luca Lavazza, Marco Cominelli +10Representation Learning Human Activity Recognition
University of Brescia, Italy. · Università La Sapienza Roma, Italy. · DEIB, Politecnico di Milano, Italy. +8
Symbolic Synthesis for LTLf+ Obligations
Apr 20, 2026Giuseppe De Giacomo, Christian Hagemeier, Daniel Hausmann +1Program Synthesis Formal Verification
University of Oxford, UK · University of Liverpool, UK · University of Gothenburg and Chalmers University of Technology, Sweden
Live LTL Progress Tracking: Towards Task-Based Exploration
Apr 18, 2026Noel Brindise, Cedric Langbort, Melkior OrnikReinforcement Learning Linear Temporal Logic
Coordinated Science Laboratory, University of Illinois Urbana-Champaign, Urbana, USA
Syntax Is Easy, Semantics Is Hard: Evaluating LLMs for LTL Translation
Apr 8, 2026Priscilla Kyei Danso, Mohammad Saqib Hasan, Niranjan Balasubramanian +1Linear Temporal Logic LLM Evaluation
Stony Brook University, Stony Brook, USA
LTLGuard: Formalizing LTL Specifications with Compact Language Models and Lightweight Symbolic Reasoning
Mar 5, 2026Medina Andresel, Cristinel Mateis, Dejan Nickovic +3Autoformalization Linear Temporal Logic
AIT Austrian Institute of Technology, Vienna, Austria · Aristotle University of Thessaloniki, Thessaloniki, Greece · Northeatern University, Boston, MA, USA
Mining Beyond the Bools: Learning Data Transformations and Temporal Specifications
Mar 5, 2026Sam Nicholas Kouteili, William Fishell, Christian Scaff +2Linear Temporal Logic Program Synthesis
Yale University · Columbia University · Barnard College, Columbia University

Oct 26, 2026J/K move · Enter open · S save

Formal Explanations for Linear Temporal Logic over Finite Traces

Valeria Fionda, Antonio Ielo, Francesco Ricca

University of Calabria, Italy

Counterfactual Explanations Linear Temporal Logic Abductive Reasoning

Open paper AskPDF arXiv

Linear Temporal Logic over Finite Traces (LTLf) is widely used in Artificial Intelligence to specify desired temporal behavior and determine whether finite traces satisfy or violate it. Explaining these outcomes is essential for debugging and trust. However, existing approaches typically capture either sufficient reasons or counterfactual causes, without clarifying their relationship. We introduce a native characterization of abductive (AXps) and contrastive (CXps) explanations directly over finite traces, based on locking and unlocking time-indexed events. We prove its equivalence to the classifier-based formulation, and show that CXps coincide with a recently proposed temporal causality semantics for LTLf. This characterization enables an efficient implementation based on the enumeration of minimal unsatisfiable cores and minimal correction sets of ASP programs. Experiments on real-world event logs demonstrate the effectiveness of the approach.