Trajectory sample databases store finite sequences of measured space-time locations of moving objects, along with a speed bound for each object. These databases can be seen as uncertain databases. We propose a language that allows the formulation of queries about the uncertainty in trajectory sample databases. As part of that language, we introduce the notion of visit events, which are used to describe certain constraints on the movement of an object. In our language, an atomic query asks whether a moving object can, given its limitations, realise such an event. We give complexity results for this realisability problem, in various settings. 2012 ACM Subject Classification Information systems -> Spatial-temporal systems; Information systems -> Query languages
Music is the art of arranging sounds in time so as to produce a continuous, unified, and evocative composition. Electronic dance music (EDM) is a collection of musical sub-genres produced using computers and electronic instruments and often presented through the medium of DJing, where tracks are curated and mixed sequentially into a continuous stream of music to offer unique listening and dancing experiences over time periods ranging from several minutes to several hours. A DJ's actions and decisions occur at several levels of temporal granularity, from real-time audio manipulation (e.g. of tempo) for smooth inter-track transitions to long-term planning of track selection and sequencing for mix content and flow. While human DJs can instinctively operate across these different temporal resolutions, replicating this capability in an end-to-end automated DJing system presents significant challenges. In this paper, we analyse existing works in DJ mix information retrieval and generation from this temporal perspective. We first explain the close link between DJing and the temporal notion of musical rhythm, then describe a framework for categorising DJing actions by temporal granularity. Using this framework, we summarise and contrast potential approaches for automating and augmenting sequential DJ decision making, and discuss the unique characteristics of DJ mix track selection as a sequential recommendation task. In doing so, we hope to facilitate the implementation of more robust and complete automated DJing systems in future research. 2012 ACM Subject Classification Applied computing -> Sound and music computing; Computing methodologies -> Control methods; Computing methodologies -> Planning under uncertainty
We consider a variant of the Vertex Cover problem on temporal graphs, called Minimum Timeline Cover (k-MinTimelineCover). Temporal graphs are used to model complex systems, describing how edges (relations) change in a discrete time domain. The k-MinTimelineCover problem has been introduced in complex data summarization and synthesis jobs. Given a temporal graph G, k-MinTimelineCover asks to define k activity intervals for each vertex, such that each temporal edge is covered by at least one active interval. The objective function is the minimization of the sum of interval lengths. k-MinTimelineCover is NP-hard and even hard to approximate within any factor for k > 1. While the literature has mainly focused on the cases k = 1, in this contribution we consider the case k > 1. We first present an ILP formulation that is able to solve the problem on moderate size instances. Then we develop an efficient heuristic, based on local search which is built on top of the solution of an existing literature method. Finally, we present an experimental evaluation of our algorithms on synthetic data sets, that shows in particular that our heuristic has a consistent improvement on the state-of-the art method. 2012 ACM Subject Classification Mathematics of computing -> Graph algorithms; Theory of computation -> Design and analysis of algorithms; Theory of computation -> Mathematical optimization; Theory of computation -> Discrete optimization
Clinical trials are typically specified with protocols that define eligibility criteria, treatment regimens, follow-up schedules, and outcome assessments. Temporality is a hallmark of all clinical trials, reflected within and across trial components, with complex dependencies unfolding across multiple time points. Despite their importance, clinical trial protocols are described in free-text format, limiting their semantic precision and the ability to support automated reasoning, leverage data across studies and sites, or simulate trial execution under varying assumptions using Real-World Data. This paper introduces a formalized representation of clinical trials using Temporal Ensemble Logic (TEL). TEL incorporates metricized modal operators, such as "always until t" ( ◻ t ) and "possibly until t" ( ♢ t ), where t is a time-length parameter, to offer a logical framework for capturing phenotypes in biomedicine. TEL is more expressive in syntax than classical linear temporal logic (LTL) while maintaining the simplicity of semantic structures. The attributes of TEL are exploited in this paper to formally represent not only individual clinical trial components, but also the timing and sequential dependencies of these components as a whole. Modeling strategies and demonstration case studies are provided to show that TEL can represent the entirety of clinical trials, whereby providing a formal logical framework that can be used to represent the intricate temporal dependencies in trial structure specification. Since clinical trials are a cornerstone of evidence-based medicine, serving as the scientific basis for evaluating the safety, efficacy, and comparative effectiveness of therapeutic interventions, results reported here can serve as a stepping stone that leads to scalable, consistent, and reproducible representation and simulation of clinical trials across all disease domains.
Composite activity recognition systems analyse streams of low-level, symbolic events to identify instances of complex activities based on their formal definitions. Crafting these definitions is a challenging task, as it often requires specifying intricate spatio-temporal constraints, and acquiring labeled data for automated learning is difficult. To address this challenge, we introduce a method that leverages pre-trained Large Language Models (LLMs) to generate composite activity definitions, in the language of the Run-Time Event Calculus, from natural language descriptions. 2012 ACM Subject Classification Computing methodologies -> Temporal reasoning
Linear temporal logic (LTL), most commonly defined as a propositional modal logic, is the de-facto standard language for specifying temporal properties of systems in formal verification, artificial intelligence, and other fields. First-order linear temporal logic (FOLTL) lifts LTL to the setting of first-order logic, obtaining a remarkably flexible and expressive formalism. First-order modal and temporal logics have a long history, but recent years have seen a rise of interest in (well-behaved fragments of) FOLTL for the specification of complex infinite-state systems. This tutorial is a gentle introduction to the field of first-order temporal logics, starting from classic results and exploring recent directions. 2012 ACM Subject Classification Theory of computation -> Modal and temporal logics
LTLf reactive synthesis under environment specifications, which concerns the automated generation of strategies enforcing logical specifications, has emerged as a powerful technique for developing autonomous AI systems. It shares many similarities with Fully Observable Nondeterministic (fond) planning. In particular, nondeterministic domains can be expressed as LTLf environment specifications. However, this is not needed since nondeterministic domains can be transformed into deterministic finite-state automata (dfa) to be used directly in the synthesis process. In this paper, we present a practical symbolic technique for translating domains expressed in Planning Domain Definition Language (pddl) into dfas. The technique allows for the integration of the planning domain, reduced to dfa in a symbolic form, into current symbolic LTLf synthesis tools. We implemented our technique in a new tool, pddl2dfa, and applied it to solve fond planning by using state-of-the-art reactive synthesis techniques in a tool called syft4fond. Our empirical results confirm the effectiveness of our approach. 2012 ACM Subject Classification Computing methodologies -> Planning and scheduling; Theory of computation -> Logic and verification; Computing methodologies -> Symbolic and algebraic manipulation
The logical reasoning skills of Large Language Models (LLMs) is poorly understood and often overstated. Current evaluation suites rely on algebraic or commonsense puzzles that mix reasoning with symbolic manipulation and/or provide static datasets that quickly saturate or leak into pretraining corpora. In purely logical terms, the most relevant reasoning skill is the meta-mathematical task of valid formula recognition, which is at the foundation of higher-level reasoning tasks (including deduction and minimization of assertions, to name just a few). In the current landscape of LLMs benchmarking, puzzles are most often stated in propositional or first-order logic, with a few exceptions for point-based temporal logic, such as LTL; yet, in the real world, event-based temporal statements are prevalent, and they are more naturally expressed in interval-based temporal logic. Interval temporal logic offers a much richer (w.r.t. point-based temporal logic, for example) variety of problems, and not only do different languages present different expressive powers, but also the computational complexity of the validity problem can vary widely. In this paper, we tackle the problem of assessing the ability of LLMs to reason about interval-based statements in the form of validity recognition. We explore whether their accuracy is sensible to the underlying language, the computational complexity of the associated validity problem, and the intrinsic hardness of the problem in terms of formula length and modal depth of the problem. We benchmark several frontier LLMs (Gemma 3 27b It, Llama 4 Maverick, DeepSeek Chat V3 release 0324, Qwen 3 32b, and Qwen 3 235b) and show that, despite apparently impressive performance on algebraic or commonsense benchmarks, they falter on logically rigorous tasks. 2012 ACM Subject Classification Theory of computation -> Modal and temporal logics; Theory of computation -> Theory and algorithms for application domains
We present QualiNet, an end-to-end deep learning framework that acquires Bird's Eye View (BEV) qualitative spatial relations directly from 2D images, eliminating the need for depth sensors. The system combines 2D object detection, masking, and classification to infer Rectangle Algebra (RA) and Qualitative Distance Calculus (QDC) relations. Evaluated on NuScenes and PandaSet datasets, QualiNet achieves 91% accuracy for RA, 80% for QDC, and 99% top-2 accuracy, demonstrating robust performance for automated vehicle perception. 2012 ACM Subject Classification Computing methodologies -> Artificial intelligence; Computing methodologies -> Spatial and physical reasoning; Computing methodologies -> Scene understanding
Space-time prisms have been extensively studied as a model to describe the uncertainty of the spatio-temporal location of a moving object in between measured space-time locations. In many applications, the desire has been expressed to provide an internal structure to these prisms, that includes what has been called "visit probability". Although several proposals have been studied in the past decades, a precise definition of this concept has been missing. The contribution of this paper is to provide such a specification by means of a formal framework for visit probability. Once this concept is established, we are able to derive on which parts of a prism, visit probability can be seen to give rise to a probability space. 2012 ACM Subject Classification Information systems -> Spatial-temporal systems; Mathematics of computing -> Probability and statistics
Space-time prisms provide a framework to model the uncertainty on the space-time points that a moving object may have visited between measured space-time locations, provided that a bound on the speed of the moving object is given. In this model, the alibi query asks whether two moving objects, given by their respective measured space-time locations and speed bound, may have met. An analytical solution to this problem was first given by Othman [5]. In this paper, we address the generalised alibi query that asks the same question for an arbitrary number n >= 2 of moving objects. We provide several solutions (mainly via the spatial and temporal projection) to this query with varying time complexities. These algorithmic solutions rely on techniques from convex and semi-algebraic geometry. We also address variants of the generalised alibi query where the question is asked for a given spatial location or a given moment in time. 2012 ACM Subject Classification Information systems -> Spatial-temporal systems; Information systems -> Query languages
The talk gives a survey of recent results on two types of problems for linear temporal logics: one is related to the existence of a Craig interpolant for a given implication in a temporal logic, the other to the existence of a temporal query separating two given sets of temporal data instances. 2012 ACM Subject Classification Theory of computation -> Modal and temporal logics
The study of safety and liveness is crucial in the context of formal languages on infinite words, providing a fundamental classification of system properties. They have been studied extensively as fragments for regular languages and Linear Temporal Logic (LTL), both from the theoretical and practical point of view, especially in the context of model checking. In contrast, despite the growing interest in Linear Temporal Logic over finite traces (LTLf) as a specification formalism for finite-length executions, the notions of safety and liveness for finite words have remained largely unexplored. In this work, we address this gap by defining the safety and liveness fragments of languages on finite words, mirroring the definition used for infinite words. We show that safety languages are exactly those that are prefix-closed, from which a bounded model property for all safety languages follows. We also provide criteria for determining whether a given language belongs to the safety or liveness fragment and analyze the computational complexity of this classification problems. Moreover, we show that certain LTL formulas classified as safety or liveness over infinite words may not preserve this classification when interpreted over finite words, and vice versa. We further establish that the safety-liveness decomposition theorem - asserting that every omega-regular language can be expressed as the intersection of a safety language and a liveness language - also holds in the finite-word setting. Finally, we examine the implications of these results for the model checking problem in LTLf. 2012 ACM Subject Classification Theory of computation -> Modal and temporal logics
Timed Automata (TA) are a popular formalism to model systems in dense linear time. However, due to their finite state-space, they can only model systems with a finitary logical behavior. There are extensions to e.g., timed pushdown systems and timed recursive state machines. Higher-Order Recursion Schemes (HORS) are another popular model for infinite-state, non-regular systems, naturally stratified by their type-theoretic order. We recently introduced Real-Time Recursion schemes as an approximation of HORS to real-time systems. This paper updates Real-Time Recursion Schemes into Higher-Order Timed Automata, a formalism that defines a tree-shaped timed automaton, which is more suitable to model actual systems. We show that the model-checking problem against the timed version of the modal mucalculus exhibits the expected complexity bounds, i.e., an increase by one exponential towards the untimed version. We also show that, in the presence of tail recursion, half an exponential can be recovered, mirroring similar gains in the untimed setting. We also give a matching lower bound for the special case of order-1 HORTA. We conjecture that this can be generalized for all orders. 2012 ACM Subject Classification Theory of computation -> Timed and hybrid models; Theory of computation -> Tree languages; Theory of computation -> Automata over infinite objects
This paper presents a novel system, called Temporal GraphQL, for supporting temporal data in web services. A temporal web service is a service that provides a temporal view of data, that is, a view of the current data as well as past or future states of the data. Capturing the history of the data is important in data forensics, data auditing, and subscriptions, where an application continuously reads data. GraphQL is a technology for improving the development and management of web services. Originally developed by Facebook and widely used in industry, GraphQL is a query language for web services. This paper introduces Temporal GraphQL. We show how to use tree grammars to model GraphQL schemas, data, and queries, and propose temporal tree grammars to model Temporal GraphQL. We extend GraphQL with temporal snapshot, slice, and delta operators. To the best of our knowledge, this is the first work on Temporal GraphQL and temporal tree grammars. 2012 ACM Subject Classification Information systems -> Temporal data; Information systems -> Service discovery and interfaces; Information systems -> Query languages
A Simple Temporal Network with Uncertainty (STNU) is a data structure for representing and reasoning about temporal constraints on activities, including those with uncertain durations. An STNU is dispatchable if it can be flexibly and efficiently executed in real time while guaranteeing that all relevant constraints are satisfied. Typically, dispatchability requires inserting conditional wait constraints, thereby forming an Extended STNU (ESTNU). The number of edges in an ESTNU affects the computational work that must be done during real-time execution. The MinDispESTNU problem is that of finding an equivalent dispatchable ESTNU having a minimal number of edges. Recent work presented an O(kn(3))-time algorithm for solving the MinDispESTNU problem, where n is the number of timepoints and k is the number of actions with uncertain durations. A subsequent paper presented a faster O(n(3))-time algorithm, but it has been shown to be incomplete. This paper presents a new O( mn + n(2)k + n(2) log n)-time algorithm for solving the MinDispESTNU problem, where m is the number of constraints in the network. The correctness of the algorithm is based on a novel theory of the canonical form of nested diamond structures. An empirical evaluation demonstrates the order-of-magnitude improvement in performance. 2012 ACM Subject Classification Computing methodologies -> Temporal reasoning; Theory of computation -> Dynamic graph algorithms
We introduce strict first-time semantics for the Until operator from linear-time temporal logic which makes assertions not just about some future moment but about the first time in the future that its argument should hold. We investigate Metric Linear-Time Temporal Logic under this interpretation in terms of expressive power, relative succinctness and computational complexity. While the expressiveness does not exceed that of pure LTL, there are properties definable in this logic which can only be expressed in LTL with exponentially larger formulas. Yet, we show that the complexity of the satisfiability problem remains PSPACE-complete which is in contrast to the EXPSPACE-completeness of Metric LTL. The motivation for this logic originates in a study of the expressive power of State Space Models, a recently proposed alternative to the popular transformer architectures in machine learning. 2012 ACM Subject Classification Theory of computation -> Modal and temporal logics; Theory of computation -> Automata over infinite objects
We present GradSTL, the first fully comprehensive implementation of signal temporal logic (STL) suitable for integration with neurosymbolic learning. In particular, GradSTL can successfully evaluate any STL constraint over any signal, regardless of how it is sampled. Our formally verified approach specifies smooth STL semantics over tensors, with formal proofs of soundness and of correctness of its derivative function. Our implementation is generated automatically from this formalisation, without manual coding, guaranteeing correctness by construction. We show via a case study that using our implementation, a neurosymbolic process learns to satisfy a pre-specified STL constraint. Our approach offers a highly rigorous foundation for integrating signal temporal logic and learning by gradient descent. 2012 ACM Subject Classification Theory of computation -> Modal and temporal logics; Computing methodologies -> Neural networks
