Volume
OASIcs, Volume 146
33rd International Symposium on Temporal Representation and Reasoning (TIME 2026)
-
Part of:
Series:
Open Access Series in Informatics (OASIcs)
Conference: International Symposium on Temporal Representation and Reasoning (TIME)
Event
Editors
Publication Details
- published at: 2026-10-10
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-448-2
Access Numbers
- Detailed Access Statistics available here
-
Total Accesses (updated on a weekly basis)
0Documents
Documents
No documents found matching your filter selection.
Document
Complete Volume
OASIcs, Volume 146, TIME 2026, Complete Volume
Abstract
OASIcs, Volume 146, TIME 2026, Complete Volume
Cite as
33rd International Symposium on Temporal Representation and Reasoning (TIME 2026). Open Access Series in Informatics (OASIcs), Volume 146, pp. 1-264, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Proceedings{orlandini_et_al:OASIcs.TIME.2026,
title = {{OASIcs, Volume 146, TIME 2026, Complete Volume}},
booktitle = {33rd International Symposium on Temporal Representation and Reasoning (TIME 2026)},
pages = {1--264},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-448-2},
ISSN = {2190-6807},
year = {2026},
volume = {146},
editor = {Orlandini, AndreA and Pinchinat, Sophie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TIME.2026},
URN = {urn:nbn:de:0030-drops-280779},
doi = {10.4230/OASIcs.TIME.2026},
annote = {Keywords: OASIcs, Volume 146, TIME 2026, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
33rd International Symposium on Temporal Representation and Reasoning (TIME 2026). Open Access Series in Informatics (OASIcs), Volume 146, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{orlandini_et_al:OASIcs.TIME.2026.0,
author = {Orlandini, AndreA and Pinchinat, Sophie},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {33rd International Symposium on Temporal Representation and Reasoning (TIME 2026)},
pages = {0:i--0:xiv},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-448-2},
ISSN = {2190-6807},
year = {2026},
volume = {146},
editor = {Orlandini, AndreA and Pinchinat, Sophie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TIME.2026.0},
URN = {urn:nbn:de:0030-drops-280768},
doi = {10.4230/OASIcs.TIME.2026.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Revisiting the Expressiveness of Metric Temporal Logic
Abstract
The expressiveness of Metric Temporal Logic (MTL) has been extensively studied throughout the last two decades. In particular, it has been shown that the interval-based semantics of MTL is strictly more expressive than the pointwise one. These results may suggest that enabling the evaluation of formulae at arbitrary time points instead of positions of timed events increases the expressive power of MTL. In this paper, we formally argue otherwise. We demonstrate that under standard models of finite or non-Zeno infinite (action-based) timed executions, the interval-based and the pointwise semantics are incomparable. We then propose a new mixed semantics that embeds both the pointwise and the interval-based ones.
Cite as
Mohammed Aristide Foughali. Revisiting the Expressiveness of Metric Temporal Logic. In 33rd International Symposium on Temporal Representation and Reasoning (TIME 2026). Open Access Series in Informatics (OASIcs), Volume 146, pp. 1:1-1:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{foughali:OASIcs.TIME.2026.1,
author = {Foughali, Mohammed Aristide},
title = {{Revisiting the Expressiveness of Metric Temporal Logic}},
booktitle = {33rd International Symposium on Temporal Representation and Reasoning (TIME 2026)},
pages = {1:1--1:18},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-448-2},
ISSN = {2190-6807},
year = {2026},
volume = {146},
editor = {Orlandini, AndreA and Pinchinat, Sophie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TIME.2026.1},
URN = {urn:nbn:de:0030-drops-276970},
doi = {10.4230/OASIcs.TIME.2026.1},
annote = {Keywords: Timed logics, Metric temporal logic}
}
Document
Core Fragments of Compass Logic
Abstract
Compass Logic is arguably the most intuitive modal spatial logic designed for a point-based ontology, featuring exactly one unary modal operator for each cardinal direction, and interpreted over bi-dimensional structures; it can also be seen as a very natural bi-temporal logic, allowing independent reasoning in terms of future and past in two orthogonal temporal dimensions. As such, Compass Logic finds applications in several areas of modern artificial intelligence, from spatial reasoning to temporal databases. Its introduction is due to Marx and Reynolds in 1999 (inspired by previous work of Venema, 1990), when the authors proved that its satisfiability problem is undecidable regardless of the properties of the underlying structure. More recently, the idea of exploring sub-propositional fragments of unary modal logic emerged, and was applied to point-based and interval-based temporal logic. In the same spirit, in this paper we explore sub-propositional fragments of Compass Logic in the finite/discrete case, and we prove that while its satisfiability problem remains undecidable in very weak conditions, such as for the core fragment, characterized by having only formulas that are conjunctions of binary Horn clauses, it becomes surprisingly decidable for the same core fragment devoid of existential quantifiers.
Cite as
Pietro Casavecchia, Guido Sciavicco, and Leonardo Serrentino. Core Fragments of Compass Logic. In 33rd International Symposium on Temporal Representation and Reasoning (TIME 2026). Open Access Series in Informatics (OASIcs), Volume 146, pp. 2:1-2:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{casavecchia_et_al:OASIcs.TIME.2026.2,
author = {Casavecchia, Pietro and Sciavicco, Guido and Serrentino, Leonardo},
title = {{Core Fragments of Compass Logic}},
booktitle = {33rd International Symposium on Temporal Representation and Reasoning (TIME 2026)},
pages = {2:1--2:16},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-448-2},
ISSN = {2190-6807},
year = {2026},
volume = {146},
editor = {Orlandini, AndreA and Pinchinat, Sophie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TIME.2026.2},
URN = {urn:nbn:de:0030-drops-276985},
doi = {10.4230/OASIcs.TIME.2026.2},
annote = {Keywords: spatial logic, bi-temporal logic, Horn fragment, core fragment, undecidability, decidability}
}
Document
The Σ-Chain Product: A Succinct Model of Automata (De)Composition
Abstract
The cascade product is a fundamental construction in automata theory, enabling hierarchical composition of automata and playing a central role in decomposition results such as the Krohn–Rhodes theorem. However, its use is limited by the exponential size required to represent cascades, which stems from the fact that each component may depend on all preceding ones, leading to exponentially large alphabets.
To address this issue, we introduce the Σ-chain product, a restricted variant in which each component depends only on the input alphabet and the component immediately preceding it. We show that Σ-chains achieve linear-size representations and can be exponentially more succinct than cascades. We prove that Σ-chains and cascades are expressively equivalent even when restricting the components to specific classes of automata, such as permutation-reset automata. As a consequence, we derive that a language is regular if and only if it is recognized by a Σ-chain of permutation-reset automata. Finally, we analyze structural properties of Σ-chains of reset automata, including a relation with well-known subclasses of star-free languages.
Cite as
Roberto Borelli, Davide Bresolin, Luca Geatti, Angelo Montanari, and Matteo Zavatteri. The Σ-Chain Product: A Succinct Model of Automata (De)Composition. In 33rd International Symposium on Temporal Representation and Reasoning (TIME 2026). Open Access Series in Informatics (OASIcs), Volume 146, pp. 3:1-3:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{borelli_et_al:OASIcs.TIME.2026.3,
author = {Borelli, Roberto and Bresolin, Davide and Geatti, Luca and Montanari, Angelo and Zavatteri, Matteo},
title = {{The \Sigma-Chain Product: A Succinct Model of Automata (De)Composition}},
booktitle = {33rd International Symposium on Temporal Representation and Reasoning (TIME 2026)},
pages = {3:1--3:17},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-448-2},
ISSN = {2190-6807},
year = {2026},
volume = {146},
editor = {Orlandini, AndreA and Pinchinat, Sophie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TIME.2026.3},
URN = {urn:nbn:de:0030-drops-276999},
doi = {10.4230/OASIcs.TIME.2026.3},
annote = {Keywords: Automata, Cascade Product, Formal Languages, Krohn-Rhodes Theory}
}
Document
Discrete Linear Ensemble Logic: Decidability, Expressiveness, and Axiomatization
Abstract
We study the discrete point-based fragment of Ensemble Logic EL(ℕ) over the natural numbers, a logic combining displacement φ_u, term-dependent metric modalities ☐_t and ♢_t with respect to an additive term t, Boolean connectives, and first-order quantification over ℕ. Motivated by the need for a unified symbolic representation of biomedical knowledge with temporal, spatial, and multimodal metric content, we develop the foundational discrete theory of the formalism. We give syntax and semantics, and prove a forward embedding of EL(ℕ) (over a finite proposition set 𝒫) into first-order monadic Presburger arithmetic FO(ℕ,<,+;𝒫). This embedding yields the analytical upper bounds, while a reduction from nondeterministic two-counter Turing machines with recurring control states proves that satisfiability is Σ¹₁-complete and validity is dually Π¹₁-complete. Expressively, EL(ℕ) strictly extends the star-free ω-languages and is incomparable with the ω-regular languages: it defines the non-ω-regular counting language {a^m b^m c^m d^m∣ m ≥ 1}⋅Σ^ω, whereas a delimited parity language remains outside the logic by a quantifier-bounding argument combined with classical circuit lower bounds for parity. On the proof-theoretic side, we present a sound Hilbert system ℋ_EL and establish completeness relative to monadic Presburger validity as oracle, noting that completeness relative to plain Presburger arithmetic is impossible. We also prove that the existential fragment ∃EL(ℕ) has NP-complete satisfiability and coNP-complete unsatisfiability. Finally, we show that finite active-domain model-checking has PTIME data complexity and PSPACE-complete combined complexity. Together, these results give a precise decidability, expressiveness, proof-theoretic, and model-checking baseline for subsequent algorithmic applications of Ensemble Logic in biomedicine. This work is a part of the Symbolic Biomedicine program championed by the corresponding author.
Cite as
Manfred Droste and Guo-Qiang Zhang. Discrete Linear Ensemble Logic: Decidability, Expressiveness, and Axiomatization. In 33rd International Symposium on Temporal Representation and Reasoning (TIME 2026). Open Access Series in Informatics (OASIcs), Volume 146, pp. 4:1-4:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{droste_et_al:OASIcs.TIME.2026.4,
author = {Droste, Manfred and Zhang, Guo-Qiang},
title = {{Discrete Linear Ensemble Logic: Decidability, Expressiveness, and Axiomatization}},
booktitle = {33rd International Symposium on Temporal Representation and Reasoning (TIME 2026)},
pages = {4:1--4:18},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-448-2},
ISSN = {2190-6807},
year = {2026},
volume = {146},
editor = {Orlandini, AndreA and Pinchinat, Sophie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TIME.2026.4},
URN = {urn:nbn:de:0030-drops-277009},
doi = {10.4230/OASIcs.TIME.2026.4},
annote = {Keywords: Temporal logic, monadic Presburger arithmetic, descriptive complexity, electronic health records}
}
Document
Social Networks Through Time: Completeness of Temporal Network Logic
Abstract
The framework of Temporal Network Logic (TNL) - first introduced in [Pedersen et al., 2021] and further developed in [Pedersen et al., 2023; Mina Young Pedersen, 2024] - was construed to model how a social network of interacting agents changes through time, with a language that could reflect both agents' actions, such as posting information and following each other, as well as temporal operators. This framework allows, among other things, to detect social bots, by modelling given bot behaviours as logical formulas and checking these formulas against a given model. While such applications were the main focus in [Pedersen et al., 2021; Pedersen et al., 2023; Mina Young Pedersen, 2024], the complete axiomatic system of this language has remained an open problem. In this paper, we focus on new logic-technical results and give a complete axiomatisation for TNL as well as a partial completeness result for its hybrid extension. The proofs are nonstandard and mix techniques from temporal and hybrid logics with "orthogonal" models.
Cite as
Saúl Fernández González, Mina Young Pedersen, and Sonja Smets. Social Networks Through Time: Completeness of Temporal Network Logic. In 33rd International Symposium on Temporal Representation and Reasoning (TIME 2026). Open Access Series in Informatics (OASIcs), Volume 146, pp. 5:1-5:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{fernandezgonzalez_et_al:OASIcs.TIME.2026.5,
author = {Fern\'{a}ndez Gonz\'{a}lez, Sa\'{u}l and Pedersen, Mina Young and Smets, Sonja},
title = {{Social Networks Through Time: Completeness of Temporal Network Logic}},
booktitle = {33rd International Symposium on Temporal Representation and Reasoning (TIME 2026)},
pages = {5:1--5:21},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-448-2},
ISSN = {2190-6807},
year = {2026},
volume = {146},
editor = {Orlandini, AndreA and Pinchinat, Sophie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TIME.2026.5},
URN = {urn:nbn:de:0030-drops-277017},
doi = {10.4230/OASIcs.TIME.2026.5},
annote = {Keywords: temporal logic, completeness, social network logic, hybrid logic, logics for multi-agent systems}
}
Document
Querying Interval-Based Temporal Data with SPARQL
Abstract
We propose an extension of the graph query language SPARQL to support temporal data. The proposal follows the approach of temporal databases, where each tuple is annotated with a finite set of intervals, and joins and other operators implicitly take account of these annotations. We adapt this model to the specifics of SPARQL query evaluation, which is defined in terms of compatibility of partial solution mappings. Furthermore, unlike existing proposals, our model allows predicates over intervals (e.g., Allen’s relations) in temporal atoms of filter expressions, while ensuring that query evaluation remains tractable in data complexity. Our semantics comes in three equivalent flavours, with different levels of abstraction. The basic semantics provides a snapshot view of data (it is, however, applicable only to queries without temporal atoms). In the second semantics, induced by an SPM-semiring, solution mappings are annotated with finite sets of intervals. This semantics covers temporal atoms and coincides with the snapshot semantics when the latter is defined. The third, most concrete semantics is equivalent to the second, but based on single intervals, which naturally leads to an implementation over a triple store or a relational database, with tables featuring columns for interval endpoints. As a proof of concept, we evaluate a database storage prototype and show that it addresses previously identified performance limitations of triple stores for temporal data.
Cite as
Julien Corman, Roman Kontchakov, and Cem Okulmus. Querying Interval-Based Temporal Data with SPARQL. In 33rd International Symposium on Temporal Representation and Reasoning (TIME 2026). Open Access Series in Informatics (OASIcs), Volume 146, pp. 6:1-6:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{corman_et_al:OASIcs.TIME.2026.6,
author = {Corman, Julien and Kontchakov, Roman and Okulmus, Cem},
title = {{Querying Interval-Based Temporal Data with SPARQL}},
booktitle = {33rd International Symposium on Temporal Representation and Reasoning (TIME 2026)},
pages = {6:1--6:21},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-448-2},
ISSN = {2190-6807},
year = {2026},
volume = {146},
editor = {Orlandini, AndreA and Pinchinat, Sophie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TIME.2026.6},
URN = {urn:nbn:de:0030-drops-277029},
doi = {10.4230/OASIcs.TIME.2026.6},
annote = {Keywords: Query languages, SPARQL, interval-based temporal data}
}
Document
A Multi-Scale Process for Mining and Abstracting Environmental Spatio-Temporal Graphs
Abstract
Understanding the continuous evolution of environmental systems increasingly relies on tracking large-scale, heterogeneous data across shifting timelines, commonly structured as temporal multigraphs. While such representations are highly expressive, their temporal density and structural heterogeneity make the automated analysis of long-term transitions particularly challenging. In this paper, we propose a unified process for extracting and abstracting recurrent evolutionary patterns within time-varying multigraphs. The proposed pipeline articulates four successive stages: (1) a spatio-temporal modeling stage based on RCC-8 relations to capture both topological structures and the chronological evolution of geographic entities across consecutive time steps; (2) a frequent pattern mining stage designed to discover recurring temporal sequences within multigraph representations; (3) a pattern matching stage that enables efficient, multi-scale localization of these evolutionary signatures; and (4) a hierarchical abstraction stage relying on super-nodes to produce a compact, condensed representation of the graph’s historical progression. An interactive visual environment is additionally provided as a complementary exploration tool to inspect the timeline outputs of the pipeline. We report on the results obtained from historical graph analyses of CORINE Land Cover data across multiple European cities, demonstrating the process’s capacity to reveal recurrent environmental behaviors and meaningful, time-dependent trajectories of change.
Cite as
Assaad Zeghina, Aurélie Leborgne, Florence Le Ber, and Antoine Vacavant. A Multi-Scale Process for Mining and Abstracting Environmental Spatio-Temporal Graphs. In 33rd International Symposium on Temporal Representation and Reasoning (TIME 2026). Open Access Series in Informatics (OASIcs), Volume 146, pp. 7:1-7:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{zeghina_et_al:OASIcs.TIME.2026.7,
author = {Zeghina, Assaad and Leborgne, Aur\'{e}lie and Le Ber, Florence and Vacavant, Antoine},
title = {{A Multi-Scale Process for Mining and Abstracting Environmental Spatio-Temporal Graphs}},
booktitle = {33rd International Symposium on Temporal Representation and Reasoning (TIME 2026)},
pages = {7:1--7:15},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-448-2},
ISSN = {2190-6807},
year = {2026},
volume = {146},
editor = {Orlandini, AndreA and Pinchinat, Sophie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TIME.2026.7},
URN = {urn:nbn:de:0030-drops-277031},
doi = {10.4230/OASIcs.TIME.2026.7},
annote = {Keywords: Graph Deep Learning, Temporal Graphs, Pattern Mining, Temporal Analysis, Graph Abstraction, Subgraph Matching}
}
Document
The Satisfiability Problem of Temporal-Spatial Logics over Quasi-Temporal Graphs
Abstract
Temporal Graph Neural Networks (TGNN) are used to detect patterns in so-called temporal graphs (TG): graphs in which edges may be added or removed over time. Sälzer et al. suggested to study the expressive power of TGNNs through temporal-spatial logics, specifically the combination of the linear-time temporal logic LTL and modal logic K. In this paper we investigate the computational complexity of the satisfiability problem for this logic and its natural extension in which the LTL part is replaced by a linear-time μ-calculus, reflecting TGNNs' ability to recognise not just star-free (word) languages. We consider their interpretation over a more natural class of models which we call quasi-temporal graphs (QTG), relaxing certain conditions on the temporal evolutions of nodes that are indifferent to the logic. We formalise this by giving an adjusted notion of bisimulation which preserves satisfaction in these logics. It turns out that satisfiability over the class of QTGs is PSPACE-complete for the temporal-spatial logic based on LTL but becomes EXPTIME-complete when based on the μ-calculus. This is in contrast to the situation on words where both logics are PSPACE-complete. We also discuss consequences for the special satisfiability problems over the class of TGs.
Cite as
Eric Alsmann, Martin Lange, and Igor Semezies. The Satisfiability Problem of Temporal-Spatial Logics over Quasi-Temporal Graphs. In 33rd International Symposium on Temporal Representation and Reasoning (TIME 2026). Open Access Series in Informatics (OASIcs), Volume 146, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{alsmann_et_al:OASIcs.TIME.2026.8,
author = {Alsmann, Eric and Lange, Martin and Semezies, Igor},
title = {{The Satisfiability Problem of Temporal-Spatial Logics over Quasi-Temporal Graphs}},
booktitle = {33rd International Symposium on Temporal Representation and Reasoning (TIME 2026)},
pages = {8:1--8:16},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-448-2},
ISSN = {2190-6807},
year = {2026},
volume = {146},
editor = {Orlandini, AndreA and Pinchinat, Sophie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TIME.2026.8},
URN = {urn:nbn:de:0030-drops-277049},
doi = {10.4230/OASIcs.TIME.2026.8},
annote = {Keywords: linear-time temporal logic, modal logic, temporal graphs, computational complexity, automated reasoning}
}
Document
Dynamic Quantitative Skill Distribution in Multi-Agent Temporal Planning as SMT
Abstract
We introduce a new framework for multi-agent temporal planning, based on event-based temporal planning, dynamic team formation and Multi-Robot Task Allocation (MRTA). Unlike existing approaches, team formation is directly integrated into the planning and scheduling process. Then, both the teams and agents' skills may evolve over time. In particular, our framework allows us to address complex and dynamic multi-agent problems, such as cooperative task execution, where heterogeneous agents with qualitative and quantitative skills must cooperate dynamically. We propose an SMT encoding of these team temporal planning problems that utilizes the linear arithmetic theory over the rational numbers, QF-LRA. Next, to demonstrate that our approach is suitable for real-world applications, we present experimental results on disaster response problems.
Cite as
Josselin Guéneron and Frédéric Maris. Dynamic Quantitative Skill Distribution in Multi-Agent Temporal Planning as SMT. In 33rd International Symposium on Temporal Representation and Reasoning (TIME 2026). Open Access Series in Informatics (OASIcs), Volume 146, pp. 9:1-9:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{gueneron_et_al:OASIcs.TIME.2026.9,
author = {Gu\'{e}neron, Josselin and Maris, Fr\'{e}d\'{e}ric},
title = {{Dynamic Quantitative Skill Distribution in Multi-Agent Temporal Planning as SMT}},
booktitle = {33rd International Symposium on Temporal Representation and Reasoning (TIME 2026)},
pages = {9:1--9:20},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-448-2},
ISSN = {2190-6807},
year = {2026},
volume = {146},
editor = {Orlandini, AndreA and Pinchinat, Sophie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TIME.2026.9},
URN = {urn:nbn:de:0030-drops-277052},
doi = {10.4230/OASIcs.TIME.2026.9},
annote = {Keywords: Multi-Agent Temporal Planning, Multi-Agent Task Allocation, SMT-based Planning, Dynamic Team Formation}
}
Document
A Formal Model for Forensically Sound Timestamp Normalization
Abstract
Digital forensic analysts interpret timestamps from digital systems to assess what happened in the past. Since these systems encode time according to different underlying domains, timestamps cannot be interpreted uniformly. To enable cross-system analysis, timestamps must therefore be normalized. In this paper, we propose a formal model for forensically sound timestamp normalization and examine its properties. We show that normalization generally does not guarantee the comparability of normalized timestamps. This means that the temporal order of digitally tracked events cannot always be determined. Furthermore, we illustrate that existing forensic tools do not adhere to the proposed normalization, resulting in violations of forensic soundness in the example discussed.
Cite as
Lorenz Hornung, Carly Bakker, Bouke Timbermont, Roel van Dijk, Harm van Beek, and Natasha Alechina. A Formal Model for Forensically Sound Timestamp Normalization. In 33rd International Symposium on Temporal Representation and Reasoning (TIME 2026). Open Access Series in Informatics (OASIcs), Volume 146, pp. 10:1-10:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{hornung_et_al:OASIcs.TIME.2026.10,
author = {Hornung, Lorenz and Bakker, Carly and Timbermont, Bouke and van Dijk, Roel and van Beek, Harm and Alechina, Natasha},
title = {{A Formal Model for Forensically Sound Timestamp Normalization}},
booktitle = {33rd International Symposium on Temporal Representation and Reasoning (TIME 2026)},
pages = {10:1--10:21},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-448-2},
ISSN = {2190-6807},
year = {2026},
volume = {146},
editor = {Orlandini, AndreA and Pinchinat, Sophie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TIME.2026.10},
URN = {urn:nbn:de:0030-drops-277061},
doi = {10.4230/OASIcs.TIME.2026.10},
annote = {Keywords: Digital Forensics, Formal Model, Timestamp, Normalization}
}
Document
Decidable Reasoning About Time in Finite-Domain Situation Calculus Theories
Abstract
Representing time is crucial for cyber-physical systems and has been studied extensively in the situation calculus. The most commonly used approach represents time by adding a real-valued function time(a) that attaches a time point to each action and consequently to each situation. We show that in this approach, checking whether there is a reachable situation that satisfies a given formula is undecidable, even when the domain contains only finitely many objects. We present an alternative approach based on well-established results from timed automata theory by introducing clocks as real-valued fluents with restricted successor state axioms and comparison operators. With this restriction, we can show that the reachability problem for finite-domain basic action theories is decidable. Finally, we apply our results to Golog program realization by presenting a decidable procedure for determining an action sequence that is a successful execution of a given program.
Cite as
Till Hofmann, Stefan Schupp, and Gerhard Lakemeyer. Decidable Reasoning About Time in Finite-Domain Situation Calculus Theories. In 33rd International Symposium on Temporal Representation and Reasoning (TIME 2026). Open Access Series in Informatics (OASIcs), Volume 146, pp. 11:1-11:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{hofmann_et_al:OASIcs.TIME.2026.11,
author = {Hofmann, Till and Schupp, Stefan and Lakemeyer, Gerhard},
title = {{Decidable Reasoning About Time in Finite-Domain Situation Calculus Theories}},
booktitle = {33rd International Symposium on Temporal Representation and Reasoning (TIME 2026)},
pages = {11:1--11:22},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-448-2},
ISSN = {2190-6807},
year = {2026},
volume = {146},
editor = {Orlandini, AndreA and Pinchinat, Sophie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TIME.2026.11},
URN = {urn:nbn:de:0030-drops-277073},
doi = {10.4230/OASIcs.TIME.2026.11},
annote = {Keywords: Situation Calculus, Golog, timed automata, clocks, dense time, reachability, decidability, region abstraction, program realization}
}
Document
Earth Observation Satellite Constellation Planning with Matheuristics and Metaheuristics Combination
Abstract
A standard problem in the field of Earth observation is the scheduling of the observations of an agile satellite constellation. Given a set of end-user requests over Points Of Interest (POIs), it consists in selecting observations among the candidate ones, attributing each of them to a satellite, and defining the sequence of observations planned for each satellite given operational constraints. The latter are related to the visibility windows available to observe the POIs and the time-dependent maneuvers required to reorient the observation instrument between two POIs. They result in a highly combinatorial problem that must be solved in a restricted amount of time. To solve such a complex problem, we propose an approach that combines matheuristics to filter the observation tasks and metaheuristics to schedule them. Firstly, we solve a Sequential Ordering Problem for each satellite to get a giant tour visiting all the visible POIs. From this giant tour, we exploit a Linear Programming Model to compute the best set of observations under several tour length constraints. Finally, we schedule the selected observations based on a Large Neighborhood Search. This three-step method notoriously improves the solution quality when compared to a baseline scheduling approach.
Cite as
Romain Barrault, Cedric Pralet, Gauthier Picard, and Eric Sawyer. Earth Observation Satellite Constellation Planning with Matheuristics and Metaheuristics Combination. In 33rd International Symposium on Temporal Representation and Reasoning (TIME 2026). Open Access Series in Informatics (OASIcs), Volume 146, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{barrault_et_al:OASIcs.TIME.2026.12,
author = {Barrault, Romain and Pralet, Cedric and Picard, Gauthier and Sawyer, Eric},
title = {{Earth Observation Satellite Constellation Planning with Matheuristics and Metaheuristics Combination}},
booktitle = {33rd International Symposium on Temporal Representation and Reasoning (TIME 2026)},
pages = {12:1--12:17},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-448-2},
ISSN = {2190-6807},
year = {2026},
volume = {146},
editor = {Orlandini, AndreA and Pinchinat, Sophie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TIME.2026.12},
URN = {urn:nbn:de:0030-drops-277089},
doi = {10.4230/OASIcs.TIME.2026.12},
annote = {Keywords: Scheduling, Earth Observation Satellite, Matheuristic, Metaheuristic, Linear Programming}
}
Document
Multi-Agent Path Finding with Tasks Under Time Uncertainty
Abstract
Multi-Agent Path Finding under Time Uncertainty (MAPF-TU) extends classical MAPF by considering uncertain traversal duration. However, existing approaches, such as the Conflict Based Search with Time Uncertainty (CBS_TU) method, assume that uncertainty only arises while agents move between locations, overlooking uncertainty induced by executing tasks. In many real-world applications, agents must not only navigate but also perform tasks of uncertain duration at specific locations, leading to additional temporal dependencies.
In this paper, we introduce Multi-Agent Path Finding with Tasks under Time Uncertainty (MAPF-TTU), a new extension of MAPF-TU in which agents must execute tasks of uncertain duration at intermediate goals. We first analyze the computational complexity of MAPF-TU and MAPF-TTU. We then propose two complementary solution approaches. The first extends CBS_TU to explicitly reason about uncertain task execution during planning. The second transforms an MAPF-TU solution into a Simple Temporal Network with Uncertainty (STNU) and computes a robust execution schedule through Strong Controllability.
Finally, we experimentally evaluate both approaches under varying levels of traversal and task time uncertainty, highlighting the tradeoff between solution quality and scalability.
Cite as
Alexandre Albore, Christophe Grand, Noëlie Ramuzat, and Ajdin Sumic. Multi-Agent Path Finding with Tasks Under Time Uncertainty. In 33rd International Symposium on Temporal Representation and Reasoning (TIME 2026). Open Access Series in Informatics (OASIcs), Volume 146, pp. 13:1-13:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{albore_et_al:OASIcs.TIME.2026.13,
author = {Albore, Alexandre and Grand, Christophe and Ramuzat, No\"{e}lie and Sumic, Ajdin},
title = {{Multi-Agent Path Finding with Tasks Under Time Uncertainty}},
booktitle = {33rd International Symposium on Temporal Representation and Reasoning (TIME 2026)},
pages = {13:1--13:21},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-448-2},
ISSN = {2190-6807},
year = {2026},
volume = {146},
editor = {Orlandini, AndreA and Pinchinat, Sophie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TIME.2026.13},
URN = {urn:nbn:de:0030-drops-277090},
doi = {10.4230/OASIcs.TIME.2026.13},
annote = {Keywords: Multi-Agent Path Finding, Temporal Uncertainty, Conflict Based Search, Simple Temporal Network}
}