Volume
LIPIcs, Volume 278
30th International Symposium on Temporal Representation and Reasoning (TIME 2023)
Publication Details
- published at: 2023-09-18
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-298-3
- DBLP: db/conf/time/time2023
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 278, TIME 2023, Complete Volume
Abstract
LIPIcs, Volume 278, TIME 2023, Complete Volume
Cite as
30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 1-254, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Proceedings{artikis_et_al:LIPIcs.TIME.2023,
title = {{LIPIcs, Volume 278, TIME 2023, Complete Volume}},
booktitle = {30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
pages = {1--254},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-298-3},
ISSN = {1868-8969},
year = {2023},
volume = {278},
editor = {Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023},
URN = {urn:nbn:de:0030-drops-190890},
doi = {10.4230/LIPIcs.TIME.2023},
annote = {Keywords: LIPIcs, Volume 278, TIME 2023, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{artikis_et_al:LIPIcs.TIME.2023.0,
author = {Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
pages = {0:i--0:xiv},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-298-3},
ISSN = {1868-8969},
year = {2023},
volume = {278},
editor = {Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.0},
URN = {urn:nbn:de:0030-drops-190907},
doi = {10.4230/LIPIcs.TIME.2023.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
Learning Temporal Logic Formulas from Time-Series Data (Invited Talk)
Abstract
In this talk, we provide an overview of recent advancements in the field of mining formal specifications from time-series data, with a specific focus on learning Signal Temporal Logic (STL) formulae.
Cite as
Laura Nenzi. Learning Temporal Logic Formulas from Time-Series Data (Invited Talk). In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{nenzi:LIPIcs.TIME.2023.1,
author = {Nenzi, Laura},
title = {{Learning Temporal Logic Formulas from Time-Series Data}},
booktitle = {30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
pages = {1:1--1:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-298-3},
ISSN = {1868-8969},
year = {2023},
volume = {278},
editor = {Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.1},
URN = {urn:nbn:de:0030-drops-190917},
doi = {10.4230/LIPIcs.TIME.2023.1},
annote = {Keywords: Temporal Logic, Mining Specifications}
}
Document
LTL over Finite Words Can Be Exponentially More Succinct Than Pure-Past LTL, and vice versa
Abstract
Linear Temporal Logic over finite traces (LTL_𝖿) has proved itself to be an important and effective formalism in formal verification as well as in artificial intelligence. Pure past LTL_𝖿 (pLTL) is the logic obtained from LTL_𝖿 by replacing each (future) temporal operator by a corresponding past one, and is naturally interpreted at the end of a finite trace. It is known that each property definable in LTL_𝖿 is also definable in pLTL, and ǐceversa. However, despite being extensively used in practice, to the best of our knowledge, there is no systematic study of their succinctness.
In this paper, we investigate the succinctness of LTL_𝖿 and pLTL. First, we prove that pLTL can be exponentially more succinct than LTL_𝖿 by showing that there exists a property definable with a pLTL formula of size n such that the size of all LTL_𝖿 formulas defining it is at least exponential in n. Then, we prove that LTL_𝖿 can be exponentially more succinct than pLTL as well. This result shows that, although being expressively equivalent, LTL_𝖿 and pLTL are incomparable when succinctness is concerned. In addition, we study the succinctness of Safety-LTL (the syntactic safety fragment of LTL over infinite traces) with respect to its canonical form G(pLTL), whose formulas are of the form G(α), G being the globally operator and α a pLTL formula. We prove that G(pLTL) can be exponentially more succinct than Safety-LTL, and that the same holds for the dual cosafety fragment.
Cite as
Alessandro Artale, Luca Geatti, Nicola Gigante, Andrea Mazzullo, and Angelo Montanari. LTL over Finite Words Can Be Exponentially More Succinct Than Pure-Past LTL, and vice versa. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 2:1-2:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{artale_et_al:LIPIcs.TIME.2023.2,
author = {Artale, Alessandro and Geatti, Luca and Gigante, Nicola and Mazzullo, Andrea and Montanari, Angelo},
title = {{LTL over Finite Words Can Be Exponentially More Succinct Than Pure-Past LTL, and vice versa}},
booktitle = {30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
pages = {2:1--2:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-298-3},
ISSN = {1868-8969},
year = {2023},
volume = {278},
editor = {Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.2},
URN = {urn:nbn:de:0030-drops-190927},
doi = {10.4230/LIPIcs.TIME.2023.2},
annote = {Keywords: Temporal Logic, Succinctness, LTLf, Finite Traces, Pure past LTL}
}
Document
LSCPM: Communities in Massive Real-World Link Streams by Clique Percolation Method
Abstract
Community detection is a popular approach to understand the organization of interactions in static networks. For that purpose, the Clique Percolation Method (CPM), which involves the percolation of k-cliques, is a well-studied technique that offers several advantages. Besides, studying interactions that occur over time is useful in various contexts, which can be modeled by the link stream formalism. The Dynamic Clique Percolation Method (DCPM) has been proposed for extending CPM to temporal networks.
However, existing implementations are unable to handle massive datasets. We present a novel algorithm that adapts CPM to link streams, which has the advantage that it allows us to speed up the computation time with respect to the existing DCPM method. We evaluate it experimentally on real datasets and show that it scales to massive link streams. For example, it allows to obtain a complete set of communities in under twenty-five minutes for a dataset with thirty million links, what the state of the art fails to achieve even after a week of computation. We further show that our method provides communities similar to DCPM, but slightly more aggregated. We exhibit the relevance of the obtained communities in real world cases, and show that they provide information on the importance of vertices in the link streams.
Cite as
Alexis Baudin, Lionel Tabourier, and Clémence Magnien. LSCPM: Communities in Massive Real-World Link Streams by Clique Percolation Method. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 3:1-3:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{baudin_et_al:LIPIcs.TIME.2023.3,
author = {Baudin, Alexis and Tabourier, Lionel and Magnien, Cl\'{e}mence},
title = {{LSCPM: Communities in Massive Real-World Link Streams by Clique Percolation Method}},
booktitle = {30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
pages = {3:1--3:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-298-3},
ISSN = {1868-8969},
year = {2023},
volume = {278},
editor = {Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.3},
URN = {urn:nbn:de:0030-drops-190932},
doi = {10.4230/LIPIcs.TIME.2023.3},
annote = {Keywords: Temporal network, Link stream, k-clique, Community detection, Clique Percolation Method, Real-world interactions}
}
Document
Discovering Predictive Dependencies on Multi-Temporal Relations
Abstract
In this paper, we propose a methodology for deriving a new kind of approximate temporal functional dependencies, called Approximate Predictive Functional Dependencies (APFDs), based on a three-window framework and on a multi-temporal relational model. Different features are proposed for the Observation Window (OW), where we observe predictive data, for the Waiting Window (WW), and for the Prediction Window (PW), where the predicted event occurs. We then discuss the concept of approximation for such APFDs, introduce two new error measures. We prove that the problem of deriving APFDs is intractable. Moreover, we discuss some preliminary results in deriving APFDs from real clinical data using MIMIC III dataset, related to patients from Intensive Care Units.
Cite as
Beatrice Amico, Carlo Combi, Romeo Rizzi, and Pietro Sala. Discovering Predictive Dependencies on Multi-Temporal Relations. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{amico_et_al:LIPIcs.TIME.2023.4,
author = {Amico, Beatrice and Combi, Carlo and Rizzi, Romeo and Sala, Pietro},
title = {{Discovering Predictive Dependencies on Multi-Temporal Relations}},
booktitle = {30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
pages = {4:1--4:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-298-3},
ISSN = {1868-8969},
year = {2023},
volume = {278},
editor = {Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.4},
URN = {urn:nbn:de:0030-drops-190945},
doi = {10.4230/LIPIcs.TIME.2023.4},
annote = {Keywords: temporal databases, temporal data mining, functional dependencies}
}
Document
Prime Scenarios in Qualitative Spatial and Temporal Reasoning
Abstract
The concept of prime implicant is a fundamental tool in Boolean algebra, which is used in Boolean circuit design and, recently, in explainable AI. This study investigates an analogous concept in qualitative spatial and temporal reasoning, called prime scenario. Specifically, we define a prime scenario of a qualitative constraint network (QCN) as a minimal set of decisions that can uniquely determine solutions of this QCN. We propose in this paper a collection of algorithms designed to address various problems related to prime scenarios. The first three algorithms aim to generate a prime scenario from a scenario of a QCN. The main idea consists in using path consistency to identify the constraints that can be ignored to generate a prime scenario. The next two algorithms focus on generating a set of prime scenarios that cover all the scenarios of the original QCN: The first algorithm examines every branch of the search tree, while the second is based on the use of a SAT encoding. Our last algorithm is concerned with computing a minimum-size prime scenario by using a MaxSAT encoding built from countermodels of the original QCN. We show that this algorithm is particularly useful for measuring the robustness of a QCN. Finally, a preliminary experimental evaluation is performed with instances of Allen’s Interval Algebra to assess the efficiency of our algorithms and, hence, also the difficulty of the newly introduced problems here.
Cite as
Yakoub Salhi and Michael Sioutis. Prime Scenarios in Qualitative Spatial and Temporal Reasoning. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 5:1-5:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{salhi_et_al:LIPIcs.TIME.2023.5,
author = {Salhi, Yakoub and Sioutis, Michael},
title = {{Prime Scenarios in Qualitative Spatial and Temporal Reasoning}},
booktitle = {30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
pages = {5:1--5:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-298-3},
ISSN = {1868-8969},
year = {2023},
volume = {278},
editor = {Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.5},
URN = {urn:nbn:de:0030-drops-190957},
doi = {10.4230/LIPIcs.TIME.2023.5},
annote = {Keywords: Spatial and Temporal Reasoning, Qualitative Constraints, Prime Scenario, Prime Implicant, Robustness Measurement}
}
Document
Bounded-Memory Runtime Enforcement of Timed Properties
Abstract
Runtime Enforcement (RE) is a monitoring technique aimed at correcting possibly incorrect executions w.r.t. a set of formal requirements (properties) of a system. In this paper, we consider enforcement monitoring of real-time properties. Thus, executions are modelled as timed words and specifications as timed automata. Moreover, we consider that the enforcer has the ability to delay events by storing or buffering them into its internal memory (and releasing them when the property is finally satisfied) and suppressing events when no delaying is appropriate. Practically, in an implementation, the internal memory of the enforcer is finite.
In this paper, we propose a new RE paradigm for timed properties, where the memory of the enforcer is bounded/finite, to address practical applications with memory constraints and timed specifications. Bounding the memory presents a number of difficulties, e.g., how to accommodate a timed event into the memory when the memory is full, s.t., regardless of the course of action we choose to handle this situation, the behaviour of the bounded enforcer should not significantly differ from that of the unbounded enforcer. The problem of how to optimally discard events when the buffer is full is significantly more difficult in a timed environment where the progress of time affects the satisfaction or violation of a property. We define the bounded-memory RE problem for timed properties and develop a framework for regular timed properties specified as timed automata. The proposed framework is implemented in Python, and its performance is evaluated. From experiments, we discovered that the enforcer has a reasonable execution time overhead.
Cite as
Saumya Shankar, Srinivas Pinisetty, and Thierry Jéron. Bounded-Memory Runtime Enforcement of Timed Properties. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 6:1-6:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{shankar_et_al:LIPIcs.TIME.2023.6,
author = {Shankar, Saumya and Pinisetty, Srinivas and J\'{e}ron, Thierry},
title = {{Bounded-Memory Runtime Enforcement of Timed Properties}},
booktitle = {30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
pages = {6:1--6:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-298-3},
ISSN = {1868-8969},
year = {2023},
volume = {278},
editor = {Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.6},
URN = {urn:nbn:de:0030-drops-190962},
doi = {10.4230/LIPIcs.TIME.2023.6},
annote = {Keywords: Formal methods, Runtime enforcement, Bounded-memory, Timed automata}
}
Document
More Than 0s and 1s: Metric Quantifiers and Counting over Timed Words
Abstract
We study the expressiveness of the pointwise interpretations (i.e. over timed words) of some predicate and temporal logics with metric and counting features. We show that counting in the unit interval (0, 1) is strictly weaker than counting in (0, b) with arbitrary b ≥ 0; moreover, allowing the latter indeed leads to expressive completeness for the metric predicate logic Q2MLO, recovering the corresponding result for the continuous interpretations (i.e. over signals). Exploiting this connection, we show that in contrast to the continuous case, adding "punctual" predicates into Q2MLO is still insufficient for the full expressive power of the Monadic First-Order Logic of Order and Metric (FO[<,+1]). Finally, we propose a generalisation of the recently proposed Pnueli automata modalities and show that the resulting metric temporal logic is expressively complete for FO[<,+1].
Cite as
Hsi-Ming Ho and Khushraj Madnani. More Than 0s and 1s: Metric Quantifiers and Counting over Timed Words. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 7:1-7:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{ho_et_al:LIPIcs.TIME.2023.7,
author = {Ho, Hsi-Ming and Madnani, Khushraj},
title = {{More Than 0s and 1s: Metric Quantifiers and Counting over Timed Words}},
booktitle = {30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
pages = {7:1--7:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-298-3},
ISSN = {1868-8969},
year = {2023},
volume = {278},
editor = {Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.7},
URN = {urn:nbn:de:0030-drops-190979},
doi = {10.4230/LIPIcs.TIME.2023.7},
annote = {Keywords: Temporal Logic, Expressiveness, Automata}
}
Document
Analyzing Complex Systems with Cascades Using Continuous-Time Bayesian Networks
Abstract
Interacting systems of events may exhibit cascading behavior where events tend to be temporally clustered. While the cascades themselves may be obvious from the data, it is important to understand which states of the system trigger them. For this purpose, we propose a modeling framework based on continuous-time Bayesian networks (CTBNs) to analyze cascading behavior in complex systems. This framework allows us to describe how events propagate through the system and to identify likely sentry states, that is, system states that may lead to imminent cascading behavior. Moreover, CTBNs have a simple graphical representation and provide interpretable outputs, both of which are important when communicating with domain experts. We also develop new methods for knowledge extraction from CTBNs and we apply the proposed methodology to a data set of alarms in a large industrial system.
Cite as
Alessandro Bregoli, Karin Rathsman, Marco Scutari, Fabio Stella, and Søren Wengel Mogensen. Analyzing Complex Systems with Cascades Using Continuous-Time Bayesian Networks. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 8:1-8:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{bregoli_et_al:LIPIcs.TIME.2023.8,
author = {Bregoli, Alessandro and Rathsman, Karin and Scutari, Marco and Stella, Fabio and Mogensen, S{\o}ren Wengel},
title = {{Analyzing Complex Systems with Cascades Using Continuous-Time Bayesian Networks}},
booktitle = {30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
pages = {8:1--8:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-298-3},
ISSN = {1868-8969},
year = {2023},
volume = {278},
editor = {Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.8},
URN = {urn:nbn:de:0030-drops-190980},
doi = {10.4230/LIPIcs.TIME.2023.8},
annote = {Keywords: event model, continuous-time Bayesian network, alarm network, graphical models, event cascade}
}
Document
A Sound and Complete Tableau System for Fuzzy Halpern and Shoham’s Interval Temporal Logic
Abstract
Interval temporal logic plays a critical role in various applications, including planning, scheduling, and formal verification; recently, interval temporal logic has also been successfully applied to learning from temporal data. Halpern and Shoham’s interval temporal logic, in particular, stands out as a very intuitive, yet expressive, interval-based formalism. To address real-world scenarios involving uncertainty and imprecision, Halpern and Shoham’s logic has been recently generalized to the fuzzy (many-valued) case. The resulting language capitalizes on many-valued modal logics, allowing for a range of truth values that reflect multiple expert perspectives, but inherits the bad computational behaviour of its crisp counterpart. In this work, we investigate a sound and complete tableau system for fuzzy Halpern and Shoham’s logic, which, although possibly non-terminating, offers a semi-decision procedure for the finite case.
Cite as
Willem Conradie, Riccardo Monego, Emilio Muñoz-Velasco, Guido Sciavicco, and Ionel Eduard Stan. A Sound and Complete Tableau System for Fuzzy Halpern and Shoham’s Interval Temporal Logic. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 9:1-9:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{conradie_et_al:LIPIcs.TIME.2023.9,
author = {Conradie, Willem and Monego, Riccardo and Mu\~{n}oz-Velasco, Emilio and Sciavicco, Guido and Stan, Ionel Eduard},
title = {{A Sound and Complete Tableau System for Fuzzy Halpern and Shoham’s Interval Temporal Logic}},
booktitle = {30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
pages = {9:1--9:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-298-3},
ISSN = {1868-8969},
year = {2023},
volume = {278},
editor = {Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.9},
URN = {urn:nbn:de:0030-drops-190996},
doi = {10.4230/LIPIcs.TIME.2023.9},
annote = {Keywords: Interval temporal logic, many-valued logic, tableau system}
}
Document
The Calculus of Temporal Influence
Abstract
We present the Calculus of Temporal Influence, a simple logical calculus that allows reasoning about the behaviour of real-valued functions over time by making assertions that bound their values or the values of their derivatives. The motivation for the design of such a proof system comes from the need to provide the background computational machinery for tools that support learning in experimental subjects in secondary-education classrooms. The end goal is a tool that allows school pupils to formalise hypotheses about phenomena in natural sciences, such that their validity with respect to some formal experiment model can be checked automatically. The Calculus of Temporal Influence provides a language for formal statements and the mechanisms for reasoning about valid logical consequences. It extends (and deviates in parts from) previous work introducing the Calculus of (Non-Temporal) Influence by integrating the ability to model temporal effects in such experiments. We show that reasoning in the calculus is sound with respect to a natural formal semantics, that logical consequence is at least semi-decidable, and that one obtains polynomial-time decidability for a natural stratification of the problem.
Cite as
Florian Bruse, Marit Kastaun, Martin Lange, and Sören Möller. The Calculus of Temporal Influence. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{bruse_et_al:LIPIcs.TIME.2023.10,
author = {Bruse, Florian and Kastaun, Marit and Lange, Martin and M\"{o}ller, S\"{o}ren},
title = {{The Calculus of Temporal Influence}},
booktitle = {30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
pages = {10:1--10:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-298-3},
ISSN = {1868-8969},
year = {2023},
volume = {278},
editor = {Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.10},
URN = {urn:nbn:de:0030-drops-191009},
doi = {10.4230/LIPIcs.TIME.2023.10},
annote = {Keywords: temporal reasoning, formal models, continuous functions, polynomial decidability}
}
Document
Detecting Causality in the Presence of Byzantine Processes: The Synchronous Systems Case
Abstract
Detecting causality or the happens before relation between events in a distributed system is a fundamental building block for distributed applications. It was recently proved that this problem cannot be solved in an asynchronous distributed system in the presence of Byzantine processes, irrespective of whether the communication mechanism is via unicasts, multicasts, or broadcasts. In light of this impossibility result, we turn attention to synchronous systems and examine the possibility of solving the causality detection problem in such systems. In this paper, we prove that causality detection between events can be solved in the presence of Byzantine processes in a synchronous distributed system. The positive result holds for unicast, multicast, as well as broadcast modes of communication. We prove the result by providing an algorithm. Our solution uses the Replicated State Machine (RSM) approach and vector clocks.
Cite as
Anshuman Misra and Ajay D. Kshemkalyani. Detecting Causality in the Presence of Byzantine Processes: The Synchronous Systems Case. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 11:1-11:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{misra_et_al:LIPIcs.TIME.2023.11,
author = {Misra, Anshuman and Kshemkalyani, Ajay D.},
title = {{Detecting Causality in the Presence of Byzantine Processes: The Synchronous Systems Case}},
booktitle = {30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
pages = {11:1--11:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-298-3},
ISSN = {1868-8969},
year = {2023},
volume = {278},
editor = {Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.11},
URN = {urn:nbn:de:0030-drops-191017},
doi = {10.4230/LIPIcs.TIME.2023.11},
annote = {Keywords: Byzantine fault-tolerance, causality, happens before, distributed system, message-passing, synchronous system}
}
Document
Embarrassingly Greedy Inconsistency Resolution of Qualitative Constraint Networks
Abstract
In this paper, we deal with inconsistency resolution in qualitative constraint networks (QCN). This type of networks allows one to represent and reason about spatial or temporal information in a natural, human-like manner, e.g., by expressing relations of the form x {is north of ∨ is east of} y. On the other hand, inconsistency resolution involves maximizing the amount of information that is consistent in a knowledge base; in the context of QCNs, this translates to maximizing the number of constraints that can be satisfied, via obtaining a qualitative solution (scenario) of the QCN that ignores/violates as few of the original constraints as possible. To this end, we present two novel approaches: a greedy constraint-based and an optimal Partial MaxSAT-based one, with a focus on the former due to its simplicity. Specifically, the greedy technique consists in adding the constraints of a QCN to a new, initially empty network, one by one, all the while filtering out the ones that fail the satisfiability check. What makes or breaks this technique is the ordering in which the constraints will be processed to saturate the empty QCN, and for that purpose we use many different strategies to form a portfolio-style implementation. The Partial MaxSAT-based approach is powered by Horn theory-based maximal tractable subsets of relations. Finally, we compare the greedy approach with the optimal one, commenting on the trade-off between obtaining repairs that are optimal and obtaining repairs in a manner that is fast, and make our source code available for anyone to use.
Cite as
Michael Sioutis. Embarrassingly Greedy Inconsistency Resolution of Qualitative Constraint Networks. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 12:1-12:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{sioutis:LIPIcs.TIME.2023.12,
author = {Sioutis, Michael},
title = {{Embarrassingly Greedy Inconsistency Resolution of Qualitative Constraint Networks}},
booktitle = {30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
pages = {12:1--12:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-298-3},
ISSN = {1868-8969},
year = {2023},
volume = {278},
editor = {Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.12},
URN = {urn:nbn:de:0030-drops-191020},
doi = {10.4230/LIPIcs.TIME.2023.12},
annote = {Keywords: Spatial and Temporal Reasoning, Qualitative Constraints, Inconsistency Resolution, Maximizing Satisfiability, Greedy Algorithm, Partial MaxSAT Solver}
}
Document
Optimization of Nonsequenced Queries Using Log-Segmented Timestamps
Abstract
In a period-timestamped, relational temporal database, each tuple is timestamped with a period. The timestamp records when the tuple is "alive" in some temporal dimension. Nonsequenced semantics is a query evaluation semantics that involves adding temporal predicates and constructors to a query. We show how to use log-segmented timestamps to improve the efficiency of temporal, nonsequenced queries evaluated using a non-temporal DBMS, i.e., a DBMS that has no special temporal indexes or query evaluation operators. A log-segmented timestamp divides the time-line into segments of known length. Any temporal period can be represented by a small number of such segments. The segments can be appended to a relation as additional columns. The advantage of log-segmented timestamps is that each segment can be indexed using standard database indexes, e.g., a B^+-tree. A query optimizer can use the indexes to generate a lower cost query evaluation plan. This paper shows how to rewrite a query to use the additional columns and evaluates the time cost benefits and space cost disadvantages.
Cite as
Curtis E. Dyreson. Optimization of Nonsequenced Queries Using Log-Segmented Timestamps. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 13:1-13:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{dyreson:LIPIcs.TIME.2023.13,
author = {Dyreson, Curtis E.},
title = {{Optimization of Nonsequenced Queries Using Log-Segmented Timestamps}},
booktitle = {30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
pages = {13:1--13:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-298-3},
ISSN = {1868-8969},
year = {2023},
volume = {278},
editor = {Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.13},
URN = {urn:nbn:de:0030-drops-191036},
doi = {10.4230/LIPIcs.TIME.2023.13},
annote = {Keywords: Temporal databases, nonsequenced semantics, query evaluation, query performance}
}
Document
Extended Abstract
An Event Calculus for Run-Time Reasoning (Extended Abstract)
Abstract
In stream reasoning, the task is to derive high level abstractions of large data streams with minimal latency, as required by contemporary applications. This work presents an Event Calculus-based approach to stream reasoning, highlighting its core features and recent extensions.
Cite as
Periklis Mantenoglou. An Event Calculus for Run-Time Reasoning (Extended Abstract). In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 14:1-14:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{mantenoglou:LIPIcs.TIME.2023.14,
author = {Mantenoglou, Periklis},
title = {{An Event Calculus for Run-Time Reasoning}},
booktitle = {30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
pages = {14:1--14:3},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-298-3},
ISSN = {1868-8969},
year = {2023},
volume = {278},
editor = {Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.14},
URN = {urn:nbn:de:0030-drops-191046},
doi = {10.4230/LIPIcs.TIME.2023.14},
annote = {Keywords: Event Calculus, temporal pattern matching, complex event recognition}
}
Document
Extended Abstract
SSTRESED: Scalable Semantic Trajectory Extraction for Simple Event Detection over Streaming Movement Data (Extended Abstract)
Abstract
We describe SSTRESED, a prototype focused on the real-time, online detection of simple, durative events over streaming movement data. It is the first prototype that establishes a direct connection between semantic trajectory extraction and simple event detection. SSTRESED is highly scalable by incorporating parallel processing in two separate, but connected, training and event detection pipelines implemented on state-of-the-art platforms, directly deployable in cloud environments.
Cite as
Nikos Giatrakos. SSTRESED: Scalable Semantic Trajectory Extraction for Simple Event Detection over Streaming Movement Data (Extended Abstract). In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 15:1-15:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{giatrakos:LIPIcs.TIME.2023.15,
author = {Giatrakos, Nikos},
title = {{SSTRESED: Scalable Semantic Trajectory Extraction for Simple Event Detection over Streaming Movement Data}},
booktitle = {30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
pages = {15:1--15:4},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-298-3},
ISSN = {1868-8969},
year = {2023},
volume = {278},
editor = {Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.15},
URN = {urn:nbn:de:0030-drops-191053},
doi = {10.4230/LIPIcs.TIME.2023.15},
annote = {Keywords: Semantic Trajectory, Event Processing, Data Streams}
}
Document
Extended Abstract
A Decomposition Framework for Inconsistency Handling in Qualitative Spatial and Temporal Reasoning (Extended Abstract)
Abstract
Dealing with inconsistency is a central problem in AI, due to the fact that inconsistency can arise for many reasons in real-world applications, such as context dependency, multi-source information, vagueness, noisy data, etc. Among the approaches that are involved in inconsistency handling, we can mention argumentation, non-monotonic reasoning, and paraconsistency, e.g., see [Philippe Besnard and Anthony Hunter, 2008; Gerhard Brewka et al., 1997; Koji Tanaka et al., 2013]. In the work of [Yakoub Salhi and Michael Sioutis, 2023], we are interested in dealing with inconsistency in the context of Qualitative Spatio-Temporal Reasoning (QSTR) [Ligozat, 2013]. QSTR is an AI framework that aims to mimic, natural, human-like representation and reasoning regarding space and time. This framework is applied to a variety of domains, such as qualitative case-based reasoning and learning [Thiago Pedro Donadon Homem et al., 2020] and visual sensemaking [Jakob Suchan et al., 2021]; the interested reader is referred to [Michael Sioutis and Diedrich Wolter, 2021] for a recent survey.
Motivation. In [Yakoub Salhi and Michael Sioutis, 2023], we study the decomposition of an inconsistent constraint network into consistent subnetworks under, possible, mandatory constraints. To illustrate the interest of such a decomposition, we provide a simple example described in Figure 1. The QCN depicted in the top part of the figure corresponds to a description of an inconsistent plan. Further, we assume that the constraint Task A {before} Task B is mandatory. To handle inconsistency, this plan can be transformed into a decomposition of two consistent plans, depicted in the bottom part of the figure; this decomposition can be used, e.g., to capture the fact that Task C must be performed twice. More generally, network decomposition can be involved in inconsistency handling in several ways: it can be used to identify potential contexts that explain the presence of inconsistent information; it can also be used to restore consistency through a compromise between the components of a decomposition, e.g., by using belief merging [Jean-François Condotta et al., 2010]; in addition, QCN decomposition can be used as the basis for defining inconsistency measures.
Contributions. We summarize the contributions of [Yakoub Salhi and Michael Sioutis, 2023] as follows. First, we propose a theoretical study of a problem that consists in decomposing an inconsistent QCN into a bounded number of consistent QCNs that may satisfy a specified part in the original QCN; intuitively, the required common part corresponds to the constraints that are considered necessary, if any. To this end, we provide upper bounds for the minimum number of components in a decomposition as well as computational complexity results. Secondly, we provide two methods for solving our decomposition problem. The first method corresponds to a greedy constraint-based algorithm, a variant of which involves the use of spanning trees; the basic idea of this variant is that any acyclic constraint graph in QSTR is consistent, and such a graph can be used as a starting point for building consistent components. The second method corresponds to a SAT-based encoding; every model of this encoding is used to construct a valid decomposition. Thirdly, we consider two optimization versions of the initial decomposition problem that focus on minimizing the number of components and maximizing the similarity between components, respectively. The similarity between two QCNs is quantified by the number of common non-universal constraints; the interest in maximizing the similarity lies mainly in the fact that it reduces the number of constraints that allow each component to be distinguished from the rest. Of course, our previous methods are adapted to tackle these optimization versions, too. Additionally, we introduce two inconsistency measures based on QCN decomposition, which can be seen as counterparts of measures for propositional KBs introduced in [Matthias Thimm, 2016; Meriem Ammoura et al., 2017], and show that they satisfy several desired properties in the literature. Finally, we provide implementations of our methods for computing decompositions and experimentally evaluate them using different metrics.
Cite as
Yakoub Salhi and Michael Sioutis. A Decomposition Framework for Inconsistency Handling in Qualitative Spatial and Temporal Reasoning (Extended Abstract). In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 16:1-16:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{salhi_et_al:LIPIcs.TIME.2023.16,
author = {Salhi, Yakoub and Sioutis, Michael},
title = {{A Decomposition Framework for Inconsistency Handling in Qualitative Spatial and Temporal Reasoning}},
booktitle = {30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
pages = {16:1--16:3},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-298-3},
ISSN = {1868-8969},
year = {2023},
volume = {278},
editor = {Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.16},
URN = {urn:nbn:de:0030-drops-191062},
doi = {10.4230/LIPIcs.TIME.2023.16},
annote = {Keywords: Spatial and Temporal Reasoning, Qualitative Constraints, Inconsistency Handling, Decomposition, Inconsistency Measures}
}
Document
Extended Abstract
Answer Set Automata: A Learnable Pattern Specification Framework for Complex Event Recognition (Extended Abstract)
Abstract
Complex Event Recognition (CER) systems detect event occurrences in streaming input using predefined event patterns. Techniques that learn event patterns from data are highly desirable in CER. Since such patterns are typically represented by symbolic automata, we propose a family of such automata where the transition-enabling conditions are defined by Answer Set Programming (ASP) rules, and which, thanks to the strong connections of ASP to symbolic learning, are learnable from data. We present such a learning approach in ASP, capable of jointly learning the structure of an automaton and its transition guards' definitions from building-block predicates, and a scalable, incremental version thereof that progressively revises models learnt from mini-batches using Monte Carlo Tree Search. We evaluate our approach on three CER datasets and empirically demonstrate its efficacy.
Cite as
Nikos Katzouris and Georgios Paliouras. Answer Set Automata: A Learnable Pattern Specification Framework for Complex Event Recognition (Extended Abstract). In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 17:1-17:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{katzouris_et_al:LIPIcs.TIME.2023.17,
author = {Katzouris, Nikos and Paliouras, Georgios},
title = {{Answer Set Automata: A Learnable Pattern Specification Framework for Complex Event Recognition}},
booktitle = {30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
pages = {17:1--17:3},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-298-3},
ISSN = {1868-8969},
year = {2023},
volume = {278},
editor = {Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.17},
URN = {urn:nbn:de:0030-drops-191071},
doi = {10.4230/LIPIcs.TIME.2023.17},
annote = {Keywords: Event Pattern Learning, Answer Set Programming}
}
Document
Extended Abstract
A Benchmark for Early Time-Series Classification (Extended Abstract)
Abstract
The objective of Early Time-Series Classification (ETSC) is to predict the class of incoming time-series by observing the fewest time-points possible. Although many approaches have been proposed in the past, not all techniques are suitable for every problem type. In particular, the characteristics of the input data may impact performance. To aid researchers and developers with deciding which kind of method suits their needs best, we developed a framework that allows the comparison of five existing ETSC algorithms, and also introduce a new method that is based on the selective truncation of time-series principle. To promote results reproducibility and the alignment of algorithm comparisons, we also include a bundle of datasets originating from real-world time-critical applications, and for which the application of ETSC algorithms can be considered quite valuable.
Cite as
Petro-Foti Kamberi, Evgenios Kladis, and Charilaos Akasiadis. A Benchmark for Early Time-Series Classification (Extended Abstract). In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 18:1-18:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{kamberi_et_al:LIPIcs.TIME.2023.18,
author = {Kamberi, Petro-Foti and Kladis, Evgenios and Akasiadis, Charilaos},
title = {{A Benchmark for Early Time-Series Classification}},
booktitle = {30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
pages = {18:1--18:3},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-298-3},
ISSN = {1868-8969},
year = {2023},
volume = {278},
editor = {Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.18},
URN = {urn:nbn:de:0030-drops-191084},
doi = {10.4230/LIPIcs.TIME.2023.18},
annote = {Keywords: Time-series analysis, Classification, Benchmark}
}
Document
Extended Abstract
Time-Aware Robustness of Temporal Graph Neural Networks for Link Prediction (Extended Abstract)
Abstract
We present a first notion of a time-aware robustness property for Temporal Graph Neural Networks (TGNN), a recently popular framework for computing functions over continuous- or discrete-time graphs, motivated by recent work on time-aware attacks on TGNN used for link prediction tasks. Furthermore, we discuss promising verification approaches for the presented or similar safety properties and possible next steps in this direction of research.
Cite as
Marco Sälzer and Silvia Beddar-Wiesing. Time-Aware Robustness of Temporal Graph Neural Networks for Link Prediction (Extended Abstract). In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 19:1-19:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{salzer_et_al:LIPIcs.TIME.2023.19,
author = {S\"{a}lzer, Marco and Beddar-Wiesing, Silvia},
title = {{Time-Aware Robustness of Temporal Graph Neural Networks for Link Prediction}},
booktitle = {30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
pages = {19:1--19:3},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-298-3},
ISSN = {1868-8969},
year = {2023},
volume = {278},
editor = {Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.19},
URN = {urn:nbn:de:0030-drops-191094},
doi = {10.4230/LIPIcs.TIME.2023.19},
annote = {Keywords: graph neural networks, temporal, verification}
}
Document
Extended Abstract
Converting Simple Temporal Networks with Uncertainty into Dispatchable Form - Faster (Extended Abstract)
Abstract
In many sectors of real-world industry, it is necessary to plan and schedule tasks allocated to agents participating in complex processes. Temporal planning aims to schedule tasks while respecting temporal constraints such as release times, maximum durations, and deadlines, which requires quantitative temporal reasoning. Over the years, several major application developers have highlighted the need for the explicit representation of actions with uncertain durations; efficient algorithms for determining whether plans involving such actions are controllable; and efficient algorithms for converting such plans into forms that enable them to be executed in real time with minimal computation, while preserving maximum flexibility.
A Simple Temporal Network with Uncertainty (STNU) is a data structure for reasoning about time constraints on actions that may have uncertain durations. An STNU is a triple (𝒯, 𝒞, ℒ) where 𝒯 is a set of real-valued variables called timepoints, 𝒞 is a set of constraints of the form Y-X ≤ δ, where X, Y ∈ 𝒯 and δ ∈ 𝐑, and ℒ is a set of contingent links of the form (A,x,y,C), where A,C ∈ 𝒯 and 0 < x < y < ∞. A contingent link (A,x,y,C) represents an uncertain duration where A is the activation timepoint, C is the contingent timepoint, and y-x is the uncertainty in the duration C-A. Typically, an executor controls the execution of A, but only observes the execution of C in real time. Although uncontrollable, the duration is guaranteed to satisfy C-A ∈ [x,y]. We let n = |𝒯|, m = |𝒞| and k = |ℒ|.
An STNU graph is a pair (𝒯, ℰ), where the timepoints in 𝒯 serve as nodes in the graph, and the edges in ℰ correspond to the constraints in 𝒞 and contingent links in ℒ. For each Y-X ≤ δ in 𝒞, ℰ contains an ordinary edge X-δ->Y. For each (A,x,y,C) ∈ ℒ, ℰ contains a lower-case (LC) edge, A-c:y->C, and an upper-case (UC) edge, C-C:-y->A, representing the respective possibilities that C-A might take its minimum or maximum value. The LO-edges are the LC or ordinary edges; the OU-edges are the ordinary or UC edges.
For any STNU, it is important to determine whether it is dynamically controllable (DC) (i.e., whether it is possible, in real time, to schedule its non-contingent timepoints such that all constraints will necessarily be satisfied no matter what durations turn out for the contingent links). Polynomial-time algorithms are available to solve this DC-checking problem. Each uses rules to generate new edges aiming to bypass certain kinds of edges in the STNU graph. Morris' O(n⁴)-time DC-checking algorithm [Paul Morris, 2006] starts from LC edges, propagating forward along OU-edges, looking for opportunities to generate new OU-edges that bypass the LC edges. Morris' O(n³)-time algorithm [Morris, 2014] starts from negative OU-edges, propagating backward along LO-edges, aiming to bypass negative edges with non-negative edges. The O(mn+k²n + knlog n)-time RUL¯ algorithm [Massimo Cairo et al., 2018] starts from UC edges, propagating backward along LO-edges, aiming to bypass UC edges with ordinary edges. After propagating, each algorithm checks for certain kinds of negative cycles to decide DC-vs.-non-DC.
However, being DC only asserts the existence of a dynamic scheduler. It is also crucial to be able to execute a DC STNU efficiently in real time. For maximum flexibility and minimal space and time requirements, a dynamic scheduler for an STNU is typically computed incrementally, in real time, so that it can react to observations of contingent executions as they occur. An efficient dynamic scheduler can be realized by first transforming an STNU into an equivalent dispatchable form [Muscettola et al., 1998; Ioannis Tsamardinos et al., 1998]. Then, to execute the dispatchable STNU, it suffices to maintain time-windows for each timepoint and, as each timepoint X is executed, only updating time-windows for neighbors of X in the graph. Dispatchable STNUs are very important in applications that demand quick responses to observations of contingent events.
Of the existing DC-checking algorithms, only Morris' O(n³)-time algorithm necessarily generates a dispatchable STNU for DC inputs. This abstract describes a faster, O(mn + kn² + n² log n)-time algorithm for converting DC STNUs into dispatchable form. (The full journal article is available elsewhere [Luke Hunsberger and Roberto Posenato, 2023].) This improvement is significant for applications (e.g., modeling business processes) where networks are typically sparse. For example, if m = O(n log n) and k = O(log n), then our algorithm runs in O(n²log n) ≪ O(n³) time.
Our new Fast Dispatch algorithm, FD_STNU, has three phases. The first phase is similar to the RUL¯ DC-checking algorithm, but generates an order-of-magnitude fewer edges overall, while also generating new UC edges that correspond to wait constraints. The second phase is a version of Morris' 2006 algorithm that propagates forward from LC edges, but only along LO-edges, aiming to generate ordinary bypass edges. The third phase focuses on the subgraph of ordinary edges, which comprise a Simple Temporal Network (STN). It uses an existing dispatchability algorithm for STNs [Ioannis Tsamardinos et al., 1998] to convert that ordinary subgraph into a dispatchable STN. After completing the three phases, the STNU is guaranteed to be dispatchable.
We provide the source code of a Java implementation of the considered algorithms (Morris, RUL¯, and FD_STNU) [Posenato, 2022] and the benchmarks used to compare their performances.
Cite as
Luke Hunsberger and Roberto Posenato. Converting Simple Temporal Networks with Uncertainty into Dispatchable Form - Faster (Extended Abstract). In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 20:1-20:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{hunsberger_et_al:LIPIcs.TIME.2023.20,
author = {Hunsberger, Luke and Posenato, Roberto},
title = {{Converting Simple Temporal Networks with Uncertainty into Dispatchable Form - Faster}},
booktitle = {30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
pages = {20:1--20:3},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-298-3},
ISSN = {1868-8969},
year = {2023},
volume = {278},
editor = {Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.20},
URN = {urn:nbn:de:0030-drops-191104},
doi = {10.4230/LIPIcs.TIME.2023.20},
annote = {Keywords: Temporal constraint networks, contingent durations, dispatchable network}
}
Document
Extended Abstract
Torwards Infinite-State Verification and Planning with Linear Temporal Logic Modulo Theories (Extended Abstract)
Abstract
In this extended abstract, we discuss about Linear Temporal Logic Modulo Theories over finite traces (LTL_f^MT), a temporal logic that we recently introduced with the goal of providing an equilibrium between generality of the formalism and decidability of the logic. After recalling its distinguishing features, we discuss some future applications.
Cite as
Luca Geatti, Alessandro Gianola, and Nicola Gigante. Torwards Infinite-State Verification and Planning with Linear Temporal Logic Modulo Theories (Extended Abstract). In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 21:1-21:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{geatti_et_al:LIPIcs.TIME.2023.21,
author = {Geatti, Luca and Gianola, Alessandro and Gigante, Nicola},
title = {{Torwards Infinite-State Verification and Planning with Linear Temporal Logic Modulo Theories}},
booktitle = {30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
pages = {21:1--21:3},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-298-3},
ISSN = {1868-8969},
year = {2023},
volume = {278},
editor = {Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.21},
URN = {urn:nbn:de:0030-drops-191110},
doi = {10.4230/LIPIcs.TIME.2023.21},
annote = {Keywords: Linear Temporal Logic, Satisfiability Modulo Theories}
}
Document
Extended Abstract
Qualitative past Timeline-Based Games (Extended Abstract)
Abstract
This extended abstract discusses timeline-based planning, a modeling approach that offers a unique way to model complex systems. Recently, the timeline-based planning framework has been extended to handle general nondeterminism in a game-theoretic setting, resulting in timeline-based games. In this context, the problem of establishing whether a timeline-based game admits a winning strategy and synthesizing such a strategy have been addressed. We propose exploring simpler yet expressive fragments of timeline-based games by leveraging results about the role of past operators in synthesis from temporal logic specifications. The qualitative fragment of timeline-based planning is a good starting point for this exploration. We suggest introducing syntactic restrictions on synchronization rules so that they only constrain the behavior of the system before the current time point, which is expected to lower the complexity of synthesizing timeline-based games to EXPTIME.
Cite as
Renato Acampora, Luca Geatti, Nicola Gigante, and Angelo Montanari. Qualitative past Timeline-Based Games (Extended Abstract). In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 22:1-22:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{acampora_et_al:LIPIcs.TIME.2023.22,
author = {Acampora, Renato and Geatti, Luca and Gigante, Nicola and Montanari, Angelo},
title = {{Qualitative past Timeline-Based Games}},
booktitle = {30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
pages = {22:1--22:3},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-298-3},
ISSN = {1868-8969},
year = {2023},
volume = {278},
editor = {Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.22},
URN = {urn:nbn:de:0030-drops-191125},
doi = {10.4230/LIPIcs.TIME.2023.22},
annote = {Keywords: Automata, Planning, Temporal Reasoning}
}