Temporal Logic

Follow this topic Ask about this topic

Latest papers

19 papers4 papers in the last four weeks, against 1 the four weeks before. 0.0% of all new papers.

Oct 14, 2026

Neurosymbolic Learning of Interpretable World Models

World models aim to learn compact representations of an environment from observations, enabling agents to predict future states and plan their behaviour. However, most existing approaches learn black-box representations, with limited ability to incorporate prior knowledge about the world. We introduce Concept-Grounded World Models (CGWMs), a neurosymbolic world model design that instead learns interpretable concept representations. We learn these concepts from observations using explicit and complete knowledge, expressed in temporal logic, that specifies the valid world states and the temporal relations governing their dynamics. Furthermore, we directly use this knowledge by formulating planning as differentiable reasoning, optimising the agent's actions by gradient ascent to satisfy a goal. We experimentally compare CGWM with a purely neural baseline and a neurosymbolic baseline on two game environments. We find that CGWMs ground concepts much more accurately, even over long horizons, resulting in significantly more robust planning both in and out of distribution.

Riccardo Andreoni, Massimiliano Ronzani, Chiara Ghidini +2

Fondazione Bruno Kessler · Free University of Bozen-Bolzano · Vrije Universiteit Amsterdam

Temporal Logic World Model Learning World Models World Model-Based Planning Neurosymbolic Learning Neuro-Symbolic Planning

Oct 11, 2026

TL;QR: Querying Temporal Discursive Patterns in Textual Corpora

Many questions about large textual corpora concern patterns that unfold over time, such as a political group whose stance on a topic drifts from support to criticism over several years of debates. We present TL;QR (Too Long; Query with logical temporal Reasoning), a declarative query language and open-source engine for finding such temporal discursive patterns. In TL;QR, a single query combines natural-language predicates, whose truth is judged by a Large Language Model (LLM), with regular expressions and the operators of a temporal logic. The LLM answers only local questions about individual text passages; a symbolic engine then aggregates these judgments over time and links every match to the recorded passages and predicate decisions behind it. With this division of labor, the temporal and relational reasoning stays exact and auditable even over long time horizons. In addition, when a query includes a regular-expression pre-filter, only a small fraction of the corpus ever reaches the LLM. On a suite of controlled synthetic benchmarks with temporally and semantically complex patterns, TL;QR is substantially more accurate than LLM-only baselines. In a case study on ten years of European Parliament debates (442,593 multilingual speeches), TL;QR identifies candidate shifts in the political groups' stances on the GDPR privacy regulation.

François Hublet, Vladimir Krsmanovic, Jesus Solano +2

ETH Zürich · CISPA Helmholtz Center for Information Security · IST Austria

Temporal Logic Temporal IR Temporal Reasoning

Oct 6, 2026

Explainable Rule Mining of IPv6 Extension-Header Presence Patterns from Paired-Vantage Captures

IPv6 extension headers (EHs), such as fragmentation, segment routing, and in-situ telemetry, are operationally important yetwidely dropped in transit, and characterising their behaviour from packet captures is a recurring measurement problem. We ask whetheran explainable miner can recover human-readable rules of EH behaviour, and we contribute two reusable tools: a negative-control protocol that diagnoses whether a mined "temporal" network rule reflects genuine cross-packet dynamics or mere within-packetco-occurrence, and a sender-conditioned, per-family EH-retention measurement. Applying an interpretable temporal-logic rule miner to the JAMES paired-vantage dataset, we recover a portable Fragment-EH rule that the protocol reveals to be a within-packet,near-definitional co-occurrence rather than a temporal pattern, so the temporal-logic machinery does no work for this dominant rule;the retention measurement independently recovers the expected within-window ordering of EH observability. Our main result istherefore an honest, controlled negative finding, corroborated by executed decision-tree and large-language-model baselines: on theevaluated JAMES traces network-temporal structure does not carry the dominant Fragment-EH signal, and we supply the controls thatestablish when it would, validated on a synthetic positive control containing a genuine cross-packet dependency.

Priyanka Sinha, Nikolaos Kekatos, Stylianos Basagiannis +5

IIT Kharagpur, India · Clone Systems, CY · IHU, GR +1

Temporal Reasoning Temporal Logic

Oct 3, 2026

Differentiable Ternary Temporal Logic Semantics with Polynomial Surrogate Networks

Temporal logic provides designers a formal reasoning tool for specifying complex spatio-temporal behaviors and tasks for autonomous systems. Many techniques exist for control synthesis according to temporal logic specifications, spanning a large variety of systems, including robotics. However, the vast majority of implementations are limited to Boolean temporal logics. Boolean temporal logic does not have an innate mechanism for quantifying abstention, rather verdicts are either definitively True or False. Recent work demonstrates that ternary logic is a capable formalism for reasoning about robotic behaviors, with the natural ability to classify uncertainty with the Unknown literal. Ternary temporal logic is still in its infancy, with work limited to synthesis for linear systems and monitoring. This work proposes a probabilistic relaxation of ternary temporal logic that allows for value and gradient computation through the same network while retaining exact verdicts on actual data. The relaxed network can be used as an objective in gradient-based control synthesis for both offline and online robotic control applications. We demonstrate the utility of our framework with two robotic manipulator tasks, one offline and one online, involving intermediate checking and sequencing of subtasks to demonstrate the benefit of our approach in terms of correct and timely execution.

Ryan Matheu, Sai Sandeep Damera, John S. Baras +1

Institute for Systems Research, University of Maryland, College Park, USA

Temporal Logic Differentiable Logic Robotic Control

Sep 19, 2026

A Geometric Decision Procedure for STL Feasibility and Repair

Feasibility of a Signal Temporal Logic (STL) specification asks whether, from a given initial state, an admissible control input can satisfy its continuous-time requirements under actuator limits. Establishing feasibility is essential for detecting unrealizable tasks and repairing specifications before execution. State-of-the-art Mixed-Integer Linear Programming (MILP) methods face growing model sizes as temporal horizons and formula complexity increase, and can accept control witnesses that violate continuous-time STL semantics between samples. We propose a geometric approach to STL feasibility and temporal repair that translates temporal requirements into spatial constraints evaluated at the initial state. Its compiled feasibility check is independent of horizon length for fixed compiled dimensions. We prove nonnegative continuous robustness under a joint controller assumption. On 6D UAV benchmarks, median geometric repair times are 0.265--1.510 ms; we show up to 1.68x10^4 speedup over MILP feasibility checker. All geometric runs pass continuous STL validation, whereas majority of completed MILP control witnesses violate continuous-time STL.

Avinash Malik

Department of Electrical, Computer, and Software Engineering, University of Auckland, Auckland, New Zealand

Reachability Analysis Signal Temporal Logic Formal Verification STL Planning Temporal Logic STL Motion Planning

Aug 17, 2026

Backward through Time, Algebraically

Linear temporal logic is a modal extension of propositional logic that allows one to state how a system should behave over time. Its canonical domain is the booleans, but discretely-valued judgements are of little use in steering softly-valued systems (neural policies, adaptive controllers, sequence models, etc). In such cases, the goal formula's (dis)satisfaction becomes a training signal, and differentiability becomes a prime concern. Candidate differentiable semantics abound, but navigating them is tricky. Implementations, where available, are shallow embeddings, demanding an upfront commitment to a single semantic algebra and its (usually implicit) conduct. The paper casts the reader as a functional programmer asked to come to terms with this predicament, and refusing. Out of that refusal comes an evaluation engine that is algebra-generic and amenable to differentiation, together with an executable specification of the algebras it can accept. Various algebras are implemented and audited for their behavior, both forward and backward. Each algebra turns out to be a choice of which direction to disappoint, and how. Everything described (and more) is part of the PyTorch library telos, to be found at https://github.com/konstantinosKokos/telos.

Konstantinos Kogkalidis

Differentiable Logic Temporal Logic Linear Temporal Logic Differentiable Programming

Aug 3, 2026

Infinite Trace Objectives with Finite Trace Techniques: Translating LTL to LTLf+

Linear Temporal Logic (LTL) is one of the most widely adopted languages for specifying temporal extended objectives in AI, with applications ranging from reactive synthesis to stochastic planning in Markov decision processes and reinforcement learning. Traditionally, solving any of these problems requires translating the LTL specification to a nondeterministic automata on infinite words and then determinizing it, a step that is notoriously difficult in theory and in practice. Recent work has introduced LTLf+, which lifts the finite-trace logic LTLf to infinite traces. LTLf+ has the same expressive power as LTL, yet it retains most of the crucial advantages of its base logic LTLf. Most reasoning in LTLf+ rests on finite automata on finite words, for which we have not only a canonical minimal representation but also an efficient determinization procedure. In this work we present the first translation from LTL to LTLf+. We first normalize an LTL formula into the syntactic reactivity fragment of the Manna-Pnueli hierarchy, to create the general fragment-based shape of LTLf+. We then present linear translations for each individual component of that fragment. As a consequence of this translation, the expanding body of techniques developed for LTLf+ now becomes available to many AI problems currently formulated in LTL. We further show that this comes at no asymptotic cost, as the pipeline from LTL to automaton via LTLf+ remains doubly exponential.

Christoph Weinhuber, Maximilian Prokop, Giuseppe De Giacomo +1

University of Oxford · 2Technical University of Munich · 3Masaryk University Brno +1

Temporal Reasoning Formal Verification Linear Temporal Logic Temporal Logic

Jul 12, 2026

Learning Linear Temporal Specifications from Demonstrations with Uncertainty

Learning temporal logic specifications from system demonstrations is essential for tasks such as formal verification and controller synthesis, especially in safety-critical domains. Existing approaches typically assume demonstrations are correct or only affected by misclassification errors. In practice, however, system traces are often uncertain or incomplete due to sensor faults, measurement errors, or data loss. We present a framework for learning minimal Linear Temporal Logic (LTL) formulas from demonstrations with uncertainty. Our approach models uncertainty via Hamming distance to generate possible estimates around each observed trace, which are grouped with constraints requiring that at least one trace per group is consistent with the learned formula. Our problem is then reduced to an equivalent Pseudo-Boolean Optimization. We evaluate our method against state-of-the-art LTL learning approaches and show that it recovers specifications that more closely align with ground-truth formulas under uncertainty.

Parastou Fahim, Constantino Lagoa, Rômulo Meira-G'oes

School of Electrical Engineering and Computer Science at The Pennsylvania State University, State College, USA

Formal Verification Learning from Demonstration Linear Temporal Logic Temporal Logic

Jul 3, 2026

Incentivizing Vision Language Models to Search for Long Video Question Answering

We introduce VSeek, an agentic framework that transforms long-video question answering (LVQA) from a passive, single-pass perception task into a multi-turn retrieval process. VSeek utilizes a natural language-driven search to identify relevant context within long videos and is post-trained with reinforcement learning (RL) to jointly formulate targeted search queries and reason over retrieved clips for LVQA. While RL post-training has revolutionized reasoning in symbolic domains such as mathematics and code, its application to long-video understanding remains hindered by a lack of verified rewards. To ensure that the retrieved context is relevant, we propose a novel neuro-symbolic approach that bridges open-ended natural language with discrete visual verification. Specifically, complex user queries are compiled into formal temporal logic specifications for systematically decomposing natural language questions into a definitive checklist of required atomic visual primitives, such as key objects and activities, along with their temporal ordering. These systematically derived grounding events provide the critical feedback signal for RL post-training, enabling dense, verifiable rewards based on the successful retrieval of these specific visual elements rather than relying entirely on outcome-only answer accuracy. By explicitly optimizing for this verifiable evidence-seeking behavior, VSeek improves Pass@1 scores by up to 8% and Pass@4 scores by 15% on long-video understanding benchmarks compared to base models. We open-source our code at https://utaustin-swarmlab.github.io/VSeek.

Harsh Goel, S P Sharan, Sahil Shah +4

The University of Texas at Austin, Austin, TX, USA

Tool Use in VLMs Temporal Logic Long-Video QA RL for VLMs

Jun 29, 2026

First-Order Temporal Logic Tensor Networks

Most of the existing neuro-symbolic AI methods focus on the scenario of static knowledge where objects do not change according to a temporal dimension. Temporal neuro-symbolic works are still under explored and are mainly developed for time-interval logic or propositional linear temporal logic. There is a lack of models studying linear temporal logics with predicates that deal with objects whose properties and relations change through the time. We present First-Order Temporal Logic Tensor Networks (FOT-LTN) that is an extension of Logic Tensor Networks (LTN) that fills this gap by considering a linear-temporal dimension. In particular, FOT-LTN joins the syntax of First-Order Linear Temporal Logic with the fuzzy (and real-valued) semantics of LTN obtaining a framework that supports both temporal operators and quantifiers and is totally differentiable. A first evaluation regards a temporal knowledge graph completion task on two synthetic datasets showing better performance of FOT-LTN with respect to dedicated (purely neural) methods.

Luca Boscarato, Ivan Donadello, Alessandro Artale +2

Free University of Bozen-Bolzano

Tensor Networks Logic Tensor Networks Neuro-Symbolic AI Temporal KGs Linear Temporal Logic Temporal Logic

Jun 25, 2026

An Algebraic Framework for Quantitative Semantics of Spatio-Temporal Logic with Graph Operators

Spatio-Temporal Logic with Graph Operators (STL-GO) extends Signal Temporal Logic (STL) to multi-agent systems via graph operators that count neighboring agents satisfying a property, together with multi-agent quantifiers. While Boolean semantics for STL-GO are well-defined, quantitative semantics have not yet been developed and existing quantitative semantics for spatio-temporal logics such as STREL cannot capture the counting constraints in STL-GO's graph operators. We develop quantitative semantics for STL-GO as a layered algebraic construction that separates temporal aggregation from graph-operator aggregation (governed by an abstract accumulator with a monotone fold and readout). We prove that soundness and completeness reduce to monotonicity conditions on these components. We implement the framework and evaluate it on two multi-agent environments: a 2D bounded region with stochastic Dubins-car dynamics and a 3D Earth-satellite system, under four semantic instantiations (Boolean, min-max, signed-deficit, and a hybrid), demonstrating the tradeoffs between accumulator choices and reporting scalability in the number of agents and time horizon.

Sheryl Paul, Vidisha Kudalkar, Anand Balakrishnan +3

University of Southern California, Los Angeles, CA, USA · University of Texas at Austin, Austin, TX, USA · ETH Zürich, Zürich, Switzerland

Signal Temporal Logic Multi-Agent Systems Temporal Logic

Jun 1, 2026

TLG: Temporal-Logic Grounding for Video Question Answering via Source-Annotation Reconstruction and Category-Targeted Reasoning

The TimeLogic Challenge evaluates formal temporal-logic reasoning over video - 16 operators (before, after, until, since, always, co-occur, ordering, ...) in boolean and 4-way multiple-choice form. End-to-end video-language models (VLMs) hover near chance on this task because they treat video as a bag of frames and cannot localize when actions occur. We present TLG (Temporal-Logic Grounding), a three-tier system that (i) reconstructs each video's action timeline from the public source-dataset annotations the benchmark was generated from, parses every question into a temporal-logic program, and executes it deterministically; (ii) falls back to a strong open VLM where no annotation exists; and (iii) routes only the question categories where the VLM is empirically weakest to a frontier reasoning model. TLG raises test accuracy from a 46.9% VLM baseline to 71.37%, a +24.5 absolute gain, reaching within 3 points of the leaderboard top. We report extensive ablations, including three model-based timeline-reconstruction variants that all underperform a holistic VLM, isolating temporal grounding as the irreducible bottleneck and showing that real annotations - not larger models - drive accuracy.

Ali Alavi

The Ohio State University

Temporal Video Grounding Logical Reasoning Video QA VLM Reasoning Temporal Logic Temporal QA

May 31, 2026

Temporal Evidence Routing with Structured Visual Evidence for TimeLogicQA

TimeLogicQA evaluates whether video question answering systems can reason over temporal relations such as event existence, ordering, persistence, boundary conditions, and overlap. We address this task with a visual evidence routing pipeline that separates perception from symbolic temporal reasoning. The system first parses each question into event targets, answer mode, candidate options, and temporal operators. It then routes videos according to duration and operator difficulty, using ordered full-frame evidence for short clips and event-focused candidate windows for long videos. A multimodal large language model produces structured visual evidence for the relevant events, while programmatic verifiers recover dense action intervals and a deterministic reducer applies operator-specific temporal rules to produce the final answer. Conservative fusion accepts an answer only when the visual evidence, temporal program, and confidence checks agree, reducing noisy answer flips. On the official test evaluation, our final system achieves an AvgAcc of 81.8.

Yuyang Sun, Yongliang Wu, Xingyu Zhu +8

Southeast University · National University of Singapore · Independent Researcher +2

Video QA Structured Reasoning Video Reasoning Visually Grounded Reasoning Temporal Video Understanding Long-Video QA+3

May 1, 2026

Value Functions for Temporal Logic: Optimal Policies and Safety Filters

While Bellman equations for basic reach, avoid, and reach-avoid problems are well studied, the relationship between value optimality and policy optimality becomes subtle in the undiscounted infinite-horizon setting, particularly for more complicated tasks. Greedily maximizing the Q-function can produce policies that indefinitely defer task completion for reach-avoid problems, or equivalently, Until specifications, even when the value function is optimal. Building upon recent results decomposing the value function for temporal logic (TL) into a graph of constituent value functions, we construct non-Markovian policies based on state history that avoid this pathology and prove their optimality with respect to the quantitative robustness score for nested Until, Globally, and Globally-Until specifications. We further show how the Q function can serve as a safety filter for complex TL specifications, extending prior results beyond simple avoid or reach-avoid tasks.

Oswin So, William Sharpless, Sylvia Herbert +1

Massachusetts Institute of Technology, Cambridge, MA 02139, USA · University of California, San Diego, CA 92093, USA

Sequential Decision Making Safe RL Temporal Logic

Apr 27, 2026

Logic of Fuzzy Paths

We introduce a new family of temporal logics intended for specifications in motion planning (MP). It builds upon the signal temporal logic (STL), which is a linear-time logic over real-valued signals that possess quantitative semantics and thus became popular in the areas of cyber-physical systems, robotics, and specifically robot MP. However, in contrast to STL, the proposed logic works with paths as first-class citizens, separating the concerns of geometry and of logic. This in turn leads to simpler and more understandable formulae, and a more refined notion of satisfaction being able to reflect also preferences over behaviours. Technically, the logic is built on fuzzy, time-varying signal constraints. As a consequence of this expressivity, it is (i) more usable for human-given specifications in MP and (ii) more amenable to learning specifications from demonstrations than other logics. The former is important for the traditional style of verification in robot MP; the latter is becoming recognized as crucial for mining data-given tasks and controller synthesis in human-aware MP. We expose the advantages of our proposed logic on examples and show the versatility and flexibility of the framework on a number of scenarios. Finally, we give a learning algorithm with a prototype implementation and discuss the possibilities of model checking and monitoring.

Kush Grover, Pratham Gupta, Jan Křetínský

Fondazione Bruno Kessler · Indian Institute of Science · Masaryk University

Temporal Reasoning Signal Temporal Logic Robot Motion Planning Temporal Logic STL Motion Planning

Apr 18, 2026

Logic-Based Verification of Task Allocation for LLM-Enabled Multi-Agent Manufacturing Systems

Manufacturing industries are facing increasing product variability due to the growing demand for personalized products. Under these conditions, ensuring safety becomes challenging as frequent reconfigurations can lead to unintended hazardous behaviors. Multi-agent control architectures have been proposed to improve flexibility through decentralized decision-making and coordination. However, these architectures are based on predefined task models, which limit their ability to adapt task planning to new product requirements while preserving safety. Recently, large language models have been introduced into manufacturing systems to enhance adaptability, but reliability remains a key challenge. To address this issue, we propose a control architecture that leverages the flexibility of large language models while preserving safety on the manufacturing shop floor. Specifically, the proposed framework verifies large language model-enabled task allocations by using temporal logic and discrete event systems. The effectiveness of the proposed framework is demonstrated through a case study that involves a multi-robot assembly scenario, showing that unsafe tasks can be allocated safely before task execution.

Jonghan Lim, Mostafa Tavakkoli Anbarani, Rômulo Meira-Góes +1

Department of Industrial and Manufacturing Engineering, Pennsylvania State University, State College, USA · Department of Mechanical Engineering, Pennsylvania State University, State College, USA · Department of Electrical Engineering, Pennsylvania State University, State College, USA

Multi-Agent Control Formal Verification Multi-Robot Task Allocation Temporal Logic

Apr 16, 2026

Vibe-Coding: Feedback-Based Automated Verification with no Human Code Inspection, a Feasibility Study

Vibe coding inherently assumes iterative refinement of LLM-generated code through feedback loops. While effective for conventional software tasks, its reliability in runtime-adaptive systems is unclear -- especially when generated code is not manually inspected. This paper studies feedback-based automated verification of LLM-generated adaptation managers in Collective Adaptive Systems (CAS). We focus on the key challenges of verification in the loop: how to detect failures of generated code at runtime and how to report them precisely enough for an LLM to fix them. We combine the adaptation loop with a vibe-coding feedback loop where correctness is checked against (i) generic architectural constraints and (ii) functional constraints formalized in Functional Constraints Logic (FCL), a novel first-order temporal logic over potentially finite traces. Conducting the Dragon Hunt CAS case study, we show that fine-grained constraint violations provide actionable feedback that typically yields a valid adaptation manager within a few iterations, while simple coarse metric-based feedback often stalls. Our findings suggest that feedback precision is the dominant factor for reliable vibe coding in systems designed by domain experts with no programming skills, thereby obviating the need for human code inspection.

Michal Töpfer, František Plášil, Tomáš Bureš +1

Charles University Prague, Czech Republic

LLM Self-Correction Formal Verification Temporal Logic LLM Code Generation Runtime Verification

Mar 16, 2026

Applications of Intuitionistic Temporal Logic to Temporal Answer Set Programming

The relationship between intuitionistic or intermediate logics and logic programming has been extensively studied, prominently featuring Pearce's equilibrium logic and Osorio's safe beliefs. Equilibrium logic admits a fixpoint characterization based on the logic of here-and-there, akin to theory completion in default and autoepistemic logics. Safe beliefs are similarly defined via a fixpoint operator, albeit under the semantics of intuitionistic or other intermediate logics. In this paper, we investigate the logical foundations of Temporal Answer Set Programming through the lens of Temporal Equilibrium Logic, a formalism combining equilibrium logic with linear-time temporal operators. We lift the seminal approaches of Pearce and Osorio to the temporal setting, establishing a formal correspondence between temporal intuitionistic logic and temporal logic programming. Our results deepen the theoretical underpinnings of Temporal Answer Set Programming and provide new avenues for research in temporal reasoning.

Pedro Cabalar, Martín Diéguez, David Fernández-Duque +3

University of Corunna, Spain · University of Angers, France · University of Barcelona, Spain +2

Answer Set Programming Temporal Reasoning Temporal Logic

Feb 20, 2026

Feedback-based Automated Verification in Vibe Coding of CAS Adaptation Built on Constraint Logic

In CAS adaptation, a challenge is to define the dynamic architecture of the system and changes in its behavior. Implementation-wise, this is projected into an adaptation mechanism, typically realized as an Adaptation Manager (AM). With the advances of generative LLMs, generating AM code based on system specification and desired AM behavior (partially in natural language) is a tempting opportunity. The recent introduction of vibe coding suggests a way to target the problem of the correctness of generated code by iterative testing and vibe coding feedback loops instead of direct code inspection. In this paper, we show that generating an AM via vibe coding feedback loops is a viable option when the verification of the generated AM is based on a very precise formulation of the functional requirements. We specify these as constraints in a novel temporal logic FCL that allows us to express the behavior of traces with much finer granularity than classical LTL enables. Furthermore, we show that by combining the adaptation and vibe coding feedback loops where the FCL constraints are evaluated for the current system state, we achieved good results in the experiments with generating AMs for two example systems from the CAS domain. Typically, just a few feedback loop iterations were necessary, each feeding the LLM with reports describing detailed violations of the constraints. This AM testing was combined with high run path coverage achieved by different initial settings.

Michal Töpfer, František Plášil, Tomáš Bureš +1

Charles University, Czech Republic

Temporal Logic LLM-Based Program Synthesis Formal Verification Temporal Reasoning