Volume
LIPIcs, Volume 355
32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)
Publication Details
- published at: 2025-10-13
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-401-7
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 355, TIME 2025, Complete Volume
Abstract
LIPIcs, Volume 355, TIME 2025, Complete Volume
Cite as
32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 1-242, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Proceedings{vidal_et_al:LIPIcs.TIME.2025,
title = {{LIPIcs, Volume 355, TIME 2025, Complete Volume}},
booktitle = {32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
pages = {1--242},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-401-7},
ISSN = {1868-8969},
year = {2025},
volume = {355},
editor = {Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025},
URN = {urn:nbn:de:0030-drops-248904},
doi = {10.4230/LIPIcs.TIME.2025},
annote = {Keywords: LIPIcs, Volume 355, TIME 2025, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 0:i-0:xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{vidal_et_al:LIPIcs.TIME.2025.0,
author = {Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
pages = {0:i--0:xvi},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-401-7},
ISSN = {1868-8969},
year = {2025},
volume = {355},
editor = {Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.0},
URN = {urn:nbn:de:0030-drops-248899},
doi = {10.4230/LIPIcs.TIME.2025.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
Interpolation and Separation Problems for Linear Temporal Logics (Invited Talk)
Abstract
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.
Cite as
Michael Zakharyaschev. Interpolation and Separation Problems for Linear Temporal Logics (Invited Talk). In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{zakharyaschev:LIPIcs.TIME.2025.1,
author = {Zakharyaschev, Michael},
title = {{Interpolation and Separation Problems for Linear Temporal Logics}},
booktitle = {32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
pages = {1:1--1:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-401-7},
ISSN = {1868-8969},
year = {2025},
volume = {355},
editor = {Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.1},
URN = {urn:nbn:de:0030-drops-244473},
doi = {10.4230/LIPIcs.TIME.2025.1},
annote = {Keywords: Linear temporal logic, Craig interpolation, query-by-example}
}
Document
Invited Talk
An Introduction to First-Order Linear Temporal Logic (Invited Talk)
Abstract
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.
Cite as
Nicola Gigante. An Introduction to First-Order Linear Temporal Logic (Invited Talk). In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 2:1-2:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{gigante:LIPIcs.TIME.2025.2,
author = {Gigante, Nicola},
title = {{An Introduction to First-Order Linear Temporal Logic}},
booktitle = {32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
pages = {2:1--2:6},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-401-7},
ISSN = {1868-8969},
year = {2025},
volume = {355},
editor = {Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.2},
URN = {urn:nbn:de:0030-drops-244481},
doi = {10.4230/LIPIcs.TIME.2025.2},
annote = {Keywords: Temporal logic, first-order logic, knowledge-representation, infinite-state systems}
}
Document
Metric Linear-Time Temporal Logic with Strict First-Time Semantics
Abstract
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.
Cite as
Eric Alsmann and Martin Lange. Metric Linear-Time Temporal Logic with Strict First-Time Semantics. In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 3:1-3:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{alsmann_et_al:LIPIcs.TIME.2025.3,
author = {Alsmann, Eric and Lange, Martin},
title = {{Metric Linear-Time Temporal Logic with Strict First-Time Semantics}},
booktitle = {32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
pages = {3:1--3:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-401-7},
ISSN = {1868-8969},
year = {2025},
volume = {355},
editor = {Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.3},
URN = {urn:nbn:de:0030-drops-244491},
doi = {10.4230/LIPIcs.TIME.2025.3},
annote = {Keywords: linear-time temporal logic, metric temporal logic, computational complexity, Streett automata}
}
Document
Assessing the (In)Ability of LLMs to Reason in Interval Temporal Logic
Abstract
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.
Cite as
Pietro Bellodi, Pietro Casavecchia, Alberto Paparella, Guido Sciavicco, and Ionel Eduard Stan. Assessing the (In)Ability of LLMs to Reason in Interval Temporal Logic. In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 4:1-4:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{bellodi_et_al:LIPIcs.TIME.2025.4,
author = {Bellodi, Pietro and Casavecchia, Pietro and Paparella, Alberto and Sciavicco, Guido and Stan, Ionel Eduard},
title = {{Assessing the (In)Ability of LLMs to Reason in Interval Temporal Logic}},
booktitle = {32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
pages = {4:1--4:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-401-7},
ISSN = {1868-8969},
year = {2025},
volume = {355},
editor = {Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.4},
URN = {urn:nbn:de:0030-drops-244504},
doi = {10.4230/LIPIcs.TIME.2025.4},
annote = {Keywords: Large Language Models, Benchmarking, Interval Temporal Logic}
}
Document
Higher-Order Timed Automata and Tail Recursion
Abstract
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 mu-calculus 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.
Cite as
Florian Bruse. Higher-Order Timed Automata and Tail Recursion. In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{bruse:LIPIcs.TIME.2025.5,
author = {Bruse, Florian},
title = {{Higher-Order Timed Automata and Tail Recursion}},
booktitle = {32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
pages = {5:1--5:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-401-7},
ISSN = {1868-8969},
year = {2025},
volume = {355},
editor = {Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.5},
URN = {urn:nbn:de:0030-drops-244519},
doi = {10.4230/LIPIcs.TIME.2025.5},
annote = {Keywords: Timed Automata, Higher-Order Recursion Schemes, Tree Automata, Tail Recursion}
}
Document
GradSTL: Comprehensive Signal Temporal Logic for Neurosymbolic Reasoning and Learning
Abstract
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.
Cite as
Mark Chevallier, Filip Smola, Richard Schmoetten, and Jacques D. Fleuriot. GradSTL: Comprehensive Signal Temporal Logic for Neurosymbolic Reasoning and Learning. In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 6:1-6:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{chevallier_et_al:LIPIcs.TIME.2025.6,
author = {Chevallier, Mark and Smola, Filip and Schmoetten, Richard and Fleuriot, Jacques D.},
title = {{GradSTL: Comprehensive Signal Temporal Logic for Neurosymbolic Reasoning and Learning}},
booktitle = {32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
pages = {6:1--6:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-401-7},
ISSN = {1868-8969},
year = {2025},
volume = {355},
editor = {Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.6},
URN = {urn:nbn:de:0030-drops-244528},
doi = {10.4230/LIPIcs.TIME.2025.6},
annote = {Keywords: Signal temporal logic, spatio-temporal reasoning, neurosymbolic learning}
}
Document
PDDL to DFA: A Symbolic Transformation for Effective Reasoning
Abstract
ltl_f 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 ltl_f 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 ltl_f 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.
Cite as
Giuseppe De Giacomo, Antonio Di Stasio, and Gianmarco Parretti. PDDL to DFA: A Symbolic Transformation for Effective Reasoning. In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 7:1-7:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{degiacomo_et_al:LIPIcs.TIME.2025.7,
author = {De Giacomo, Giuseppe and Di Stasio, Antonio and Parretti, Gianmarco},
title = {{PDDL to DFA: A Symbolic Transformation for Effective Reasoning}},
booktitle = {32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
pages = {7:1--7:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-401-7},
ISSN = {1868-8969},
year = {2025},
volume = {355},
editor = {Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.7},
URN = {urn:nbn:de:0030-drops-244532},
doi = {10.4230/LIPIcs.TIME.2025.7},
annote = {Keywords: Fully Observable Nondeterministic Planning, Linear Temporal Logics on finite traces, Reactive Synthesis, DFA}
}
Document
Heuristics for Covering the Timeline in Temporal Graphs
Abstract
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.
Cite as
Riccardo Dondi, Rares-Ioan Mateiu, and Alexandru Popa. Heuristics for Covering the Timeline in Temporal Graphs. In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 8:1-8:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{dondi_et_al:LIPIcs.TIME.2025.8,
author = {Dondi, Riccardo and Mateiu, Rares-Ioan and Popa, Alexandru},
title = {{Heuristics for Covering the Timeline in Temporal Graphs}},
booktitle = {32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
pages = {8:1--8:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-401-7},
ISSN = {1868-8969},
year = {2025},
volume = {355},
editor = {Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.8},
URN = {urn:nbn:de:0030-drops-244542},
doi = {10.4230/LIPIcs.TIME.2025.8},
annote = {Keywords: Temporal Networks, Activity Timeline, Vertex Cover, Heuristic, Dynamic Programming}
}
Document
Temporal GraphQL: A Tree Grammar Approach
Abstract
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.
Cite as
Curtis E. Dyreson and Bishal Sarkar. Temporal GraphQL: A Tree Grammar Approach. In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 9:1-9:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{dyreson_et_al:LIPIcs.TIME.2025.9,
author = {Dyreson, Curtis E. and Sarkar, Bishal},
title = {{Temporal GraphQL: A Tree Grammar Approach}},
booktitle = {32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
pages = {9:1--9:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-401-7},
ISSN = {1868-8969},
year = {2025},
volume = {355},
editor = {Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.9},
URN = {urn:nbn:de:0030-drops-244556},
doi = {10.4230/LIPIcs.TIME.2025.9},
annote = {Keywords: Temporal databases, temporal queries, GraphQL, web services}
}
Document
Safety and Liveness on Finite Words
Abstract
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 ǐceversa. We further establish that the safety-liveness decomposition theorem - asserting that every ω-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.
Cite as
Luca Geatti, Stefano Pessotto, and Stefano Tonetta. Safety and Liveness on Finite Words. In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{geatti_et_al:LIPIcs.TIME.2025.10,
author = {Geatti, Luca and Pessotto, Stefano and Tonetta, Stefano},
title = {{Safety and Liveness on Finite Words}},
booktitle = {32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
pages = {10:1--10:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-401-7},
ISSN = {1868-8969},
year = {2025},
volume = {355},
editor = {Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.10},
URN = {urn:nbn:de:0030-drops-244566},
doi = {10.4230/LIPIcs.TIME.2025.10},
annote = {Keywords: Safety, Liveness, Temporal Logic}
}
Document
A Better Algorithm for Converting an STNU into Minimal Dispatchable Form
Abstract
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³)-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³)-time algorithm, but it has been shown to be incomplete. This paper presents a new O(mn+n²k+n²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.
Cite as
Luke Hunsberger and Roberto Posenato. A Better Algorithm for Converting an STNU into Minimal Dispatchable Form. In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 11:1-11:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{hunsberger_et_al:LIPIcs.TIME.2025.11,
author = {Hunsberger, Luke and Posenato, Roberto},
title = {{A Better Algorithm for Converting an STNU into Minimal Dispatchable Form}},
booktitle = {32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
pages = {11:1--11:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-401-7},
ISSN = {1868-8969},
year = {2025},
volume = {355},
editor = {Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.11},
URN = {urn:nbn:de:0030-drops-244578},
doi = {10.4230/LIPIcs.TIME.2025.11},
annote = {Keywords: Temporal constraint networks, dispatchable networks}
}
Document
On the Complexity of the Realisability Problem for Visit Events in Trajectory Sample Databases
Abstract
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.
Cite as
Arthur Jansen and Bart Kuijpers. On the Complexity of the Realisability Problem for Visit Events in Trajectory Sample Databases. In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 12:1-12:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{jansen_et_al:LIPIcs.TIME.2025.12,
author = {Jansen, Arthur and Kuijpers, Bart},
title = {{On the Complexity of the Realisability Problem for Visit Events in Trajectory Sample Databases}},
booktitle = {32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
pages = {12:1--12:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-401-7},
ISSN = {1868-8969},
year = {2025},
volume = {355},
editor = {Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.12},
URN = {urn:nbn:de:0030-drops-244586},
doi = {10.4230/LIPIcs.TIME.2025.12},
annote = {Keywords: Trajectory sample databases, uncertain databases, query languages, complexity}
}
Document
Temporal Ensemble Logic for Integrative Representation of the Entirety of Clinical Trials
Abstract
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.
Cite as
Xiaojin Li, Yan Huang, Rashmie Abeysinghe, Zenan Sun, Hongyu Chen, Pengze Li, Xing He, Shiqiang Tao, Cui Tao, Jiang Bian, Licong Cui, and Guo-Qiang Zhang. Temporal Ensemble Logic for Integrative Representation of the Entirety of Clinical Trials. In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 13:1-13:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{li_et_al:LIPIcs.TIME.2025.13,
author = {Li, Xiaojin and Huang, Yan and Abeysinghe, Rashmie and Sun, Zenan and Chen, Hongyu and Li, Pengze and He, Xing and Tao, Shiqiang and Tao, Cui and Bian, Jiang and Cui, Licong and Zhang, Guo-Qiang},
title = {{Temporal Ensemble Logic for Integrative Representation of the Entirety of Clinical Trials}},
booktitle = {32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
pages = {13:1--13:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-401-7},
ISSN = {1868-8969},
year = {2025},
volume = {355},
editor = {Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.13},
URN = {urn:nbn:de:0030-drops-244595},
doi = {10.4230/LIPIcs.TIME.2025.13},
annote = {Keywords: Temporal ensemble logic, Clinical trials, Logic-based modeling}
}
Document
Short Paper
QualiNet: Acquiring Bird’s Eye View Qualitative Spatial Representation from 2D Images in Automated Vehicle Perception (Short Paper)
Abstract
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.
Cite as
Nassim Belmecheri. QualiNet: Acquiring Bird’s Eye View Qualitative Spatial Representation from 2D Images in Automated Vehicle Perception (Short Paper). In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 14:1-14:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{belmecheri:LIPIcs.TIME.2025.14,
author = {Belmecheri, Nassim},
title = {{QualiNet: Acquiring Bird’s Eye View Qualitative Spatial Representation from 2D Images in Automated Vehicle Perception}},
booktitle = {32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
pages = {14:1--14:6},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-401-7},
ISSN = {1868-8969},
year = {2025},
volume = {355},
editor = {Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.14},
URN = {urn:nbn:de:0030-drops-244608},
doi = {10.4230/LIPIcs.TIME.2025.14},
annote = {Keywords: Qualitative Spatial Representation, Deep Learning, Computer vision, Qualitative Scene Understanding, Spatio-temporal representation and reasoning models (including moving objects tracking)}
}
Document
Short Paper
The Temporal Vadalog System (Short Paper)
Abstract
The recent resurgence of the Datalog language in the Knowledge Representation and Reasoning community has paved the way for a very promising proposal for temporal extension. DatalogMTL (Datalog with Metric Temporal Operators) is a language that offers a good trade-off between computational complexity and expressive power. However, existing implementations are still preliminary or prototypical. In this extended abstract, we give a brief overview of Temporal Vadalog, a system supporting reasoning over DatalogMTL programs built upon an engineered architecture and adopted in production scenarios in the financial setting.
Cite as
Luigi Bellomarini, Livia Blasi, Markus Nissl, and Emanuel Sallinger. The Temporal Vadalog System (Short Paper). In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 15:1-15:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{bellomarini_et_al:LIPIcs.TIME.2025.15,
author = {Bellomarini, Luigi and Blasi, Livia and Nissl, Markus and Sallinger, Emanuel},
title = {{The Temporal Vadalog System}},
booktitle = {32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
pages = {15:1--15:8},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-401-7},
ISSN = {1868-8969},
year = {2025},
volume = {355},
editor = {Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.15},
URN = {urn:nbn:de:0030-drops-244611},
doi = {10.4230/LIPIcs.TIME.2025.15},
annote = {Keywords: temporal reasoning, Datalog, DatalogMTL}
}
Document
Short Paper
Solutions to the Generalised Alibi Query in Moving Object Databases (Short Paper)
Abstract
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 [Kuijpers et al., 2011]. In this paper, we address the generalised alibi query that asks the same question for an arbitrary number 𝗇 ≥ 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.
Cite as
Arthur Jansen and Bart Kuijpers. Solutions to the Generalised Alibi Query in Moving Object Databases (Short Paper). In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 16:1-16:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{jansen_et_al:LIPIcs.TIME.2025.16,
author = {Jansen, Arthur and Kuijpers, Bart},
title = {{Solutions to the Generalised Alibi Query in Moving Object Databases}},
booktitle = {32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
pages = {16:1--16:4},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-401-7},
ISSN = {1868-8969},
year = {2025},
volume = {355},
editor = {Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.16},
URN = {urn:nbn:de:0030-drops-244622},
doi = {10.4230/LIPIcs.TIME.2025.16},
annote = {Keywords: Convex geometry, Semi-algebraic geometry, Space-time prism, Geographic information systems, Quantifier elimination}
}
Document
Short Paper
Visit Probability in Space-Time Prisms for Moving Object Data (Short Paper)
Abstract
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.
Cite as
Arthur Jansen and Bart Kuijpers. Visit Probability in Space-Time Prisms for Moving Object Data (Short Paper). In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 17:1-17:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{jansen_et_al:LIPIcs.TIME.2025.17,
author = {Jansen, Arthur and Kuijpers, Bart},
title = {{Visit Probability in Space-Time Prisms for Moving Object Data}},
booktitle = {32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
pages = {17:1--17:4},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-401-7},
ISSN = {1868-8969},
year = {2025},
volume = {355},
editor = {Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.17},
URN = {urn:nbn:de:0030-drops-244633},
doi = {10.4230/LIPIcs.TIME.2025.17},
annote = {Keywords: Spatio-temporal databases, moving object databases, space-time prisms, probability spaces}
}
Document
Short Paper
Prompting LLMs for the Run-Time Event Calculus (Short Paper)
Abstract
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.
Cite as
Andreas Kouvaras, Periklis Mantenoglou, and Alexander Artikis. Prompting LLMs for the Run-Time Event Calculus (Short Paper). In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 18:1-18:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{kouvaras_et_al:LIPIcs.TIME.2025.18,
author = {Kouvaras, Andreas and Mantenoglou, Periklis and Artikis, Alexander},
title = {{Prompting LLMs for the Run-Time Event Calculus}},
booktitle = {32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
pages = {18:1--18:7},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-401-7},
ISSN = {1868-8969},
year = {2025},
volume = {355},
editor = {Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.18},
URN = {urn:nbn:de:0030-drops-244641},
doi = {10.4230/LIPIcs.TIME.2025.18},
annote = {Keywords: Event Calculus, temporal pattern matching, composite event recognition}
}
Document
Short Paper
Temporal Association Rules from Motifs (Short Paper)
Abstract
A motif is defined as a frequently occurring pattern within a (multivariate) time series. In recent years, various techniques have been developed to mine time series data. However, only a few studies have explored the idea of using motif discovery in temporal association rule mining. Interval-based temporal association rules have been recently defined and studied, along with the temporal version of the known frequent patterns, and therefore, association rule extraction algorithms (such as APRIORI and FP-Growth). In this work, we define a vocabulary of propositional letters wrapping motifs, and show how to extract temporal association rules starting from such a vocabulary. We apply our methodology to time series datasets in the fields of hand signs execution and gait recognition, and we discuss how they capture curious insights within data, keeping a high level of interpretability.
Cite as
Mauro Milella, Giovanni Pagliarini, Guido Sciavicco, and Ionel Eduard Stan. Temporal Association Rules from Motifs (Short Paper). In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 19:1-19:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{milella_et_al:LIPIcs.TIME.2025.19,
author = {Milella, Mauro and Pagliarini, Giovanni and Sciavicco, Guido and Stan, Ionel Eduard},
title = {{Temporal Association Rules from Motifs}},
booktitle = {32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
pages = {19:1--19:7},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-401-7},
ISSN = {1868-8969},
year = {2025},
volume = {355},
editor = {Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.19},
URN = {urn:nbn:de:0030-drops-244653},
doi = {10.4230/LIPIcs.TIME.2025.19},
annote = {Keywords: Motifs, Interval Temporal Logic, Association Rules}
}
Document
Short Paper
Temporal Considerations in DJ Mix Information Retrieval and Generation (Short Paper)
Abstract
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.
Cite as
Alexander Williams, Gregor Meehan, Stefan Lattner, Johan Pauwels, and Mathieu Barthet. Temporal Considerations in DJ Mix Information Retrieval and Generation (Short Paper). In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 20:1-20:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{williams_et_al:LIPIcs.TIME.2025.20,
author = {Williams, Alexander and Meehan, Gregor and Lattner, Stefan and Pauwels, Johan and Barthet, Mathieu},
title = {{Temporal Considerations in DJ Mix Information Retrieval and Generation}},
booktitle = {32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
pages = {20:1--20:8},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-401-7},
ISSN = {1868-8969},
year = {2025},
volume = {355},
editor = {Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.20},
URN = {urn:nbn:de:0030-drops-244662},
doi = {10.4230/LIPIcs.TIME.2025.20},
annote = {Keywords: Music Information Retrieval, Computational Creativity, Recommender Systems, Electronic Dance Music, DJ}
}
Document
Short Paper
A Translation of Probabilistic Event Calculus into Markov Decision Processes (Short Paper)
Abstract
Probabilistic Event Calculus (PEC) is a logical framework for reasoning about actions and their effects in uncertain environments, which enables the representation of probabilistic narratives and computation of temporal projections. The PEC formalism offers significant advantages in interpretability and expressiveness for narrative reasoning. However, it lacks mechanisms for goal-directed reasoning. Our work bridges this gap by developing a formal translation of PEC domains into Markov Decision Processes (MDPs), introducing the concept of "action-taking situations" to preserve PEC’s flexible action semantics. The resulting PEC-MDP formalism enables the extensive collection of algorithms and theoretical tools developed for MDPs to be applied to PEC’s interpretable narrative domains. We demonstrate how the translation supports both temporal reasoning tasks and objective-driven planning, with methods for mapping learned policies back into human-readable PEC representations, maintaining interpretability while extending PEC’s capabilities.
Cite as
Lyris Xu, Fabio Aurelio D'Asaro, and Luke Dickens. A Translation of Probabilistic Event Calculus into Markov Decision Processes (Short Paper). In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 21:1-21:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{xu_et_al:LIPIcs.TIME.2025.21,
author = {Xu, Lyris and D'Asaro, Fabio Aurelio and Dickens, Luke},
title = {{A Translation of Probabilistic Event Calculus into Markov Decision Processes}},
booktitle = {32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
pages = {21:1--21:5},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-401-7},
ISSN = {1868-8969},
year = {2025},
volume = {355},
editor = {Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.21},
URN = {urn:nbn:de:0030-drops-244674},
doi = {10.4230/LIPIcs.TIME.2025.21},
annote = {Keywords: Probabilistic Event Calculus, Markov Decision Processes, Temporal Projection, Narrative Reasoning}
}