Volume
LIPIcs, Volume 206
28th International Symposium on Temporal Representation and Reasoning (TIME 2021)
Event
TIME 2021, September 27-29, 2021, Klagenfurt, AustriaEditors
Publication Details
- published at: 2021-09-16
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-206-8
- DBLP: db/conf/time/time2021
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 206, TIME 2021, Complete Volume
Abstract
LIPIcs, Volume 206, TIME 2021, Complete Volume
Cite as
28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 1-244, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@Proceedings{combi_et_al:LIPIcs.TIME.2021,
title = {{LIPIcs, Volume 206, TIME 2021, Complete Volume}},
booktitle = {28th International Symposium on Temporal Representation and Reasoning (TIME 2021)},
pages = {1--244},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-206-8},
ISSN = {1868-8969},
year = {2021},
volume = {206},
editor = {Combi, Carlo and Eder, Johann and Reynolds, Mark},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2021},
URN = {urn:nbn:de:0030-drops-147755},
doi = {10.4230/LIPIcs.TIME.2021},
annote = {Keywords: LIPIcs, Volume 206, TIME 2021, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{combi_et_al:LIPIcs.TIME.2021.0,
author = {Combi, Carlo and Eder, Johann and Reynolds, Mark},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {28th International Symposium on Temporal Representation and Reasoning (TIME 2021)},
pages = {0:i--0:xiv},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-206-8},
ISSN = {1868-8969},
year = {2021},
volume = {206},
editor = {Combi, Carlo and Eder, Johann and Reynolds, Mark},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2021.0},
URN = {urn:nbn:de:0030-drops-147761},
doi = {10.4230/LIPIcs.TIME.2021.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
Simple Temporal Networks: A Practical Foundation for Temporal Representation and Reasoning (Invited Talk)
Abstract
Since Simple Temporal Networks (STNs) were first introduced in 1991, there have been numerous theoretic and algorithmic advances that have made them practical for a wide variety of applications. However, the presentation of most of the important advances have been scattered across numerous conference papers and journal articles. As a result, it is too easy for even experienced researchers to be unaware of results that could positively impact their work. In this talk we review the most important results about STNs for researchers in Artificial Intelligence who are interested in incorporating the management of time and temporal constraints into their projects.
Cite as
Luke Hunsberger and Roberto Posenato. Simple Temporal Networks: A Practical Foundation for Temporal Representation and Reasoning (Invited Talk). In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 1:1-1:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{hunsberger_et_al:LIPIcs.TIME.2021.1,
author = {Hunsberger, Luke and Posenato, Roberto},
title = {{Simple Temporal Networks: A Practical Foundation for Temporal Representation and Reasoning}},
booktitle = {28th International Symposium on Temporal Representation and Reasoning (TIME 2021)},
pages = {1:1--1:5},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-206-8},
ISSN = {1868-8969},
year = {2021},
volume = {206},
editor = {Combi, Carlo and Eder, Johann and Reynolds, Mark},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2021.1},
URN = {urn:nbn:de:0030-drops-147770},
doi = {10.4230/LIPIcs.TIME.2021.1},
annote = {Keywords: Simple Temporal Networks, Consistency Checking, Restoring Consistency, Dispatchability, Temporal Decoupling Problem}
}
Document
Invited Talk
Extreme-Scale Model-Based Time Series Management with ModelarDB (Invited Talk)
Abstract
To monitor critical industrial devices such as wind turbines, high quality sensors sampled at a high frequency are increasingly used. Current technology does not handle these extreme-scale time series well [Søren Kejser Jensen et al., 2017], so only simple aggregates are traditionally stored, removing outliers and fluctuations that could indicate problems. As a remedy, we present a model-based approach for managing extreme-scale time series that approximates the time series values using mathematical functions (models) and stores only model coefficients rather than data values. Compression is done both for individual time series and for correlated groups of time series. The keynote will present concepts, techniques, and algorithms from model-based time series management and our implementation of these in the open source Time Series Management System (TSMS) ModelarDB[Søren Kejser Jensen et al., 2018; Søren Kejser Jensen et al., 2019; Søren Kejser Jensen et al., 2021] . Furthermore, it will present our experimental evaluation of ModelarDB on extreme-scale real-world time series, which shows that that compared to widely used Big Data formats, ModelarDB provides up to 14× faster ingestion due to high compression, 113× better compression due to its adaptability, 573× faster aggregatation by using models, and close to linear scale-out scalability. ModelarDB is being commercialized by the spin-out company ModelarData.
Cite as
Torben Bach Pedersen. Extreme-Scale Model-Based Time Series Management with ModelarDB (Invited Talk). In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{pedersen:LIPIcs.TIME.2021.2,
author = {Pedersen, Torben Bach},
title = {{Extreme-Scale Model-Based Time Series Management with ModelarDB}},
booktitle = {28th International Symposium on Temporal Representation and Reasoning (TIME 2021)},
pages = {2:1--2:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-206-8},
ISSN = {1868-8969},
year = {2021},
volume = {206},
editor = {Combi, Carlo and Eder, Johann and Reynolds, Mark},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2021.2},
URN = {urn:nbn:de:0030-drops-147785},
doi = {10.4230/LIPIcs.TIME.2021.2},
annote = {Keywords: Model-based storage, approximate query processing, time series management, extreme-scale data}
}
Document
Invited Talk
Kernel Machines in Time (Invited Talk)
Abstract
Kernel machines is a powerful class of models in machine learning with solid foundations and many existing application fields. The scope of this talk is kernel machines in time with a main focus on least squares support vector machines, and other related methods such as kernel principal component analysis and kernel spectral clustering. For dynamical systems modelling different possible input-output and state space model structures will be discussed. Applications will be shown on electricity load forecasting and temperature prediction in weather forecasting. Approximate closed-form solutions can be given to ordinary and partial differential equations. Kernel spectral clustering applications to identifying customer profiles, pollution modelling and detecting topological changes in time-series of bridges will be shown. Finally, new synergies between kernel machines and deep learning will be presented, leading for example to generative kernel machines, with new insights on disentangled representations, explainability and latent space exploration. Application of these models will be illustrated on out-of-distribution detection of time-series data.
Cite as
Johan Suykens. Kernel Machines in Time (Invited Talk). In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{suykens:LIPIcs.TIME.2021.3,
author = {Suykens, Johan},
title = {{Kernel Machines in Time}},
booktitle = {28th International Symposium on Temporal Representation and Reasoning (TIME 2021)},
pages = {3:1--3:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-206-8},
ISSN = {1868-8969},
year = {2021},
volume = {206},
editor = {Combi, Carlo and Eder, Johann and Reynolds, Mark},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2021.3},
URN = {urn:nbn:de:0030-drops-147791},
doi = {10.4230/LIPIcs.TIME.2021.3},
annote = {Keywords: SVM, Time series analysis}
}
Document
Panel Description
Temporal Big Data Analytics: New Frontiers for Big Data Analytics Research (Panel Description)
Abstract
Big data analytics is an emerging research area with many sophisticated contributions in the actual literature. Big data analytics aims at discovering actionable knowledge from large amounts of big data repositories, based on several approaches that integrate foundations of a wide spectrum of disciplines, ranging from data mining to machine learning and artificial intelligence. Among the concrete innovative topics of big data analytics, temporal big data analytics covers a first-class role and it is attracting the attention of larger and larger communities of academic and industrial researchers. Basically, temporal big data analytics aims at modeling, capturing and analyzing temporal aspects of big data during analytics phase, including specialized tasks such as big data versioning over time, building temporal relations among ad-hoc big data structures (such as nodes of big graphs) and temporal queries over big data. It is worth to notice that temporal big data analytics research is characterized by several open challenges, which range from foundations, including temporal big data representation and processing, to applications, including smart cities and bio-informatics tools. Inspired by these considerations, this paper focuses on models, paradigms, techniques and future challenges of temporal big data analytics, by reporting on state-of-the-art results as well as emerging trends, with also criticisms on future work that we should expect from the community.
Cite as
Alfredo Cuzzocrea. Temporal Big Data Analytics: New Frontiers for Big Data Analytics Research (Panel Description). In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 4:1-4:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{cuzzocrea:LIPIcs.TIME.2021.4,
author = {Cuzzocrea, Alfredo},
title = {{Temporal Big Data Analytics: New Frontiers for Big Data Analytics Research}},
booktitle = {28th International Symposium on Temporal Representation and Reasoning (TIME 2021)},
pages = {4:1--4:7},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-206-8},
ISSN = {1868-8969},
year = {2021},
volume = {206},
editor = {Combi, Carlo and Eder, Johann and Reynolds, Mark},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2021.4},
URN = {urn:nbn:de:0030-drops-147804},
doi = {10.4230/LIPIcs.TIME.2021.4},
annote = {Keywords: Big Data Analytics, Big Data Management, Temporal Big Data Analytics, Temporal Big Data Management}
}
Document
Model Checking of Stream Processing Pipelines
Abstract
Event stream processing (ESP) is the application of a computation to a set of input sequences of arbitrary data objects, called "events", in order to produce other sequences of data objects. In recent years, a large number of ESP systems have been developed; however, none of them is easily amenable to a formal verification of properties on their execution. In this paper, we show how stream processing pipelines built with an existing ESP library called BeepBeep 3 can be exported as a Kripke structure for the NuXmv model checker. This makes it possible to formally verify properties on these pipelines, and opens the way to the use of such pipelines directly within a model checker as an extension of its specification language.
Cite as
Alexis Bédard and Sylvain Hallé. Model Checking of Stream Processing Pipelines. In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{bedard_et_al:LIPIcs.TIME.2021.5,
author = {B\'{e}dard, Alexis and Hall\'{e}, Sylvain},
title = {{Model Checking of Stream Processing Pipelines}},
booktitle = {28th International Symposium on Temporal Representation and Reasoning (TIME 2021)},
pages = {5:1--5:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-206-8},
ISSN = {1868-8969},
year = {2021},
volume = {206},
editor = {Combi, Carlo and Eder, Johann and Reynolds, Mark},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2021.5},
URN = {urn:nbn:de:0030-drops-147819},
doi = {10.4230/LIPIcs.TIME.2021.5},
annote = {Keywords: stream processing, model checking}
}
Document
Investigation of Database Models for Evolving Graphs
Abstract
We deal with the efficient implementation of storage models for time-varying graphs. To this end, we present an improved approach for the HiNode vertex-centric model based on MongoDB. This approach, apart from its inherent space optimality, exhibits significant improvements in global query execution times, which is the most challenging query type for entity-centric approaches. Not only significant speedups are achieved but more expensive queries can be executed as well, when compared to an implementation based on Cassandra due to the capability to exploit indices to a larger extent and benefit from in-database query processing.
Cite as
Alexandros Spitalas, Anastasios Gounaris, Kostas Tsichlas, and Andreas Kosmatopoulos. Investigation of Database Models for Evolving Graphs. In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 6:1-6:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{spitalas_et_al:LIPIcs.TIME.2021.6,
author = {Spitalas, Alexandros and Gounaris, Anastasios and Tsichlas, Kostas and Kosmatopoulos, Andreas},
title = {{Investigation of Database Models for Evolving Graphs}},
booktitle = {28th International Symposium on Temporal Representation and Reasoning (TIME 2021)},
pages = {6:1--6:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-206-8},
ISSN = {1868-8969},
year = {2021},
volume = {206},
editor = {Combi, Carlo and Eder, Johann and Reynolds, Mark},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2021.6},
URN = {urn:nbn:de:0030-drops-147821},
doi = {10.4230/LIPIcs.TIME.2021.6},
annote = {Keywords: Temporal Graphs, Indexing}
}
Document
Interval Temporal Random Forests with an Application to COVID-19 Diagnosis
Abstract
Symbolic learning is the logic-based approach to machine learning. The mission of symbolic learning is to provide algorithms and methodologies to extract logical information from data and express it in an interpretable way. In the context of temporal data, interval temporal logic has been recently proposed as a suitable tool for symbolic learning, specifically via the design of an interval temporal logic decision tree extraction algorithm. Building on it, we study here its natural generalization to interval temporal random forests, mimicking the corresponding schema at the propositional level. Interval temporal random forests turn out to be a very performing multivariate time series classification method, which, despite the introduction of a functional component, are still logically interpretable to some extent. We apply this method to the problem of diagnosing COVID-19 based on the time series that emerge from cough and breath recording of positive versus negative subjects. Our experiment show that our models achieve very high accuracies and sensitivities, often superior to those achieved by classical methods on the same data. Although other recent approaches to the same problem (based on different and more numerous data) show even better statistical results, our solution is the first logic-based, interpretable, and explainable one.
Cite as
Federico Manzella, Giovanni Pagliarini, Guido Sciavicco, and Ionel Eduard Stan. Interval Temporal Random Forests with an Application to COVID-19 Diagnosis. In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{manzella_et_al:LIPIcs.TIME.2021.7,
author = {Manzella, Federico and Pagliarini, Giovanni and Sciavicco, Guido and Stan, Ionel Eduard},
title = {{Interval Temporal Random Forests with an Application to COVID-19 Diagnosis}},
booktitle = {28th International Symposium on Temporal Representation and Reasoning (TIME 2021)},
pages = {7:1--7:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-206-8},
ISSN = {1868-8969},
year = {2021},
volume = {206},
editor = {Combi, Carlo and Eder, Johann and Reynolds, Mark},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2021.7},
URN = {urn:nbn:de:0030-drops-147837},
doi = {10.4230/LIPIcs.TIME.2021.7},
annote = {Keywords: Interval temporal logic, decision trees, random forests, sound-based diagnosis}
}
Document
Past Matters: Supporting LTL+Past in the BLACK Satisfiability Checker
Abstract
LTL+Past is the extension of Linear Temporal Logic (LTL) supporting past temporal operators. The addition of the past does not add expressive power, but does increase the usability of the language both in formal verification and in artificial intelligence, e.g., in the context of multi-agent systems. In this paper, we add the support of past operators to BLACK, a satisfiability checker for LTL based on a SAT encoding of a tree-shaped tableau system. We implement two ways of supporting the past in the tool. The first one is an equisatisfiable translation that removes the past operators, obtaining a future-only formula that can be solved with the original LTL engine. The second one extends the SAT encoding of the underlying tableau to directly support the tableau rules that deal with past operators. We describe both approaches and experimentally compare the two between themselves and with the νXmv model checker, obtaining promising results.
Cite as
Luca Geatti, Nicola Gigante, Angelo Montanari, and Gabriele Venturato. Past Matters: Supporting LTL+Past in the BLACK Satisfiability Checker. In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{geatti_et_al:LIPIcs.TIME.2021.8,
author = {Geatti, Luca and Gigante, Nicola and Montanari, Angelo and Venturato, Gabriele},
title = {{Past Matters: Supporting LTL+Past in the BLACK Satisfiability Checker}},
booktitle = {28th International Symposium on Temporal Representation and Reasoning (TIME 2021)},
pages = {8:1--8:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-206-8},
ISSN = {1868-8969},
year = {2021},
volume = {206},
editor = {Combi, Carlo and Eder, Johann and Reynolds, Mark},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2021.8},
URN = {urn:nbn:de:0030-drops-147846},
doi = {10.4230/LIPIcs.TIME.2021.8},
annote = {Keywords: SAT, LTL, LTL+Past, Tableaux}
}
Document
Pspace-Completeness of the Temporal Logic of Sub-Intervals and Suffixes
Abstract
In this paper, we establish Pspace-completeness of the finite satisfiability and model checking problems for the fragment of Halpern and Shoham interval logic with modality ⟨E⟩, for the "suffix" relation on pairs of intervals, and modality ⟨D⟩, for the "sub-interval" relation, under the homogeneity assumption. The result significantly improves the Expspace upper bound recently established for the same fragment, and proves the rather surprising fact that the complexity of the considered problems does not change when we add either the modality for suffixes (⟨E⟩) or, symmetrically, the modality for prefixes (⟨B⟩) to the logic of sub-intervals (featuring only ⟨D⟩).
Cite as
Laura Bozzelli, Angelo Montanari, Adriano Peron, and Pietro Sala. Pspace-Completeness of the Temporal Logic of Sub-Intervals and Suffixes. In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{bozzelli_et_al:LIPIcs.TIME.2021.9,
author = {Bozzelli, Laura and Montanari, Angelo and Peron, Adriano and Sala, Pietro},
title = {{Pspace-Completeness of the Temporal Logic of Sub-Intervals and Suffixes}},
booktitle = {28th International Symposium on Temporal Representation and Reasoning (TIME 2021)},
pages = {9:1--9:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-206-8},
ISSN = {1868-8969},
year = {2021},
volume = {206},
editor = {Combi, Carlo and Eder, Johann and Reynolds, Mark},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2021.9},
URN = {urn:nbn:de:0030-drops-147853},
doi = {10.4230/LIPIcs.TIME.2021.9},
annote = {Keywords: Interval temporal logic, Satisfiability, Model checking}
}
Document
Deciding FO-Rewritability of Ontology-Mediated Queries in Linear Temporal Logic
Abstract
Our concern is the problem of determining the data complexity of answering an ontology-mediated query (OMQ) given in linear temporal logic LTL over (ℤ, <) and deciding whether it is rewritable to an FO(<)-query, possibly with extra predicates. First, we observe that, in line with the circuit complexity and FO-definability of regular languages, OMQ answering in AC⁰, ACC⁰ and NC¹ coincides with FO(<,≡)-rewritability using unary predicates x ≡ 0 (mod n), FO(<,MOD)-rewritability, and FO(RPR)-rewritability using relational primitive recursion, respectively. We then show that deciding FO(<)-, FO(<,≡)- and FO(<,MOD)-rewritability of LTL OMQs is ExpSpace-complete, and that these problems become PSpace-complete for OMQs with a linear Horn ontology and an atomic query, and also a positive query in the cases of FO(<)- and FO(<,≡)-rewritability. Further, we consider FO(<)-rewritability of OMQs with a binary-clause ontology and identify OMQ classes, for which deciding it is PSpace-, Π₂^p- and coNP-complete.
Cite as
Vladislav Ryzhikov, Yury Savateev, and Michael Zakharyaschev. Deciding FO-Rewritability of Ontology-Mediated Queries in Linear Temporal Logic. In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 10:1-10:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{ryzhikov_et_al:LIPIcs.TIME.2021.10,
author = {Ryzhikov, Vladislav and Savateev, Yury and Zakharyaschev, Michael},
title = {{Deciding FO-Rewritability of Ontology-Mediated Queries in Linear Temporal Logic}},
booktitle = {28th International Symposium on Temporal Representation and Reasoning (TIME 2021)},
pages = {10:1--10:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-206-8},
ISSN = {1868-8969},
year = {2021},
volume = {206},
editor = {Combi, Carlo and Eder, Johann and Reynolds, Mark},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2021.10},
URN = {urn:nbn:de:0030-drops-147867},
doi = {10.4230/LIPIcs.TIME.2021.10},
annote = {Keywords: Linear temporal logic, ontology-mediated query, first-order rewritability}
}
Document
A Neuro-Symbolic Approach to Structured Event Recognition
Abstract
Events are structured entities with multiple components: the event type, the participants with their roles, the outcome, the sub-events etc. A fully end-to-end approach for event recognition from raw data sequence, therefore, should also solve a number of simpler tasks like recognizing the objects involved in the events and their roles, the outcome of the events as well as the sub-events. Ontological knowledge about event structure, specified in logic languages, could be very useful to solve the aforementioned challenges. However, the majority of successful approaches in event recognition from raw data are based on purely neural approaches (mainly recurrent neural networks), with limited, if any, support for background knowledge. These approaches typically require large training sets with detailed annotations at the different levels in which recognition can be decomposed (e.g., video annotated with object bounding boxes, object roles, events and sub-events). In this paper, we propose a neuro-symbolic approach for structured event recognition from raw data that uses "shallow" annotation on the high-level events and exploits background knowledge to propagate this supervision to simpler tasks such as object classification. We develop a prototype of the approach and compare it with a purely neural solution based on recurrent neural networks, showing the higher capability of solving both the event recognition task and the simpler task of object classification, as well as the ability to generalize to events with unseen outcomes.
Cite as
Gianluca Apriceno, Andrea Passerini, and Luciano Serafini. A Neuro-Symbolic Approach to Structured Event Recognition. In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 11:1-11:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{apriceno_et_al:LIPIcs.TIME.2021.11,
author = {Apriceno, Gianluca and Passerini, Andrea and Serafini, Luciano},
title = {{A Neuro-Symbolic Approach to Structured Event Recognition}},
booktitle = {28th International Symposium on Temporal Representation and Reasoning (TIME 2021)},
pages = {11:1--11:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-206-8},
ISSN = {1868-8969},
year = {2021},
volume = {206},
editor = {Combi, Carlo and Eder, Johann and Reynolds, Mark},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2021.11},
URN = {urn:nbn:de:0030-drops-147876},
doi = {10.4230/LIPIcs.TIME.2021.11},
annote = {Keywords: Event recognition, learning and reasoning, neuro-symbolic integration}
}
Document
Model Checking Timed Recursive CTL
Abstract
We introduce Timed Recursive CTL, a merger of two extensions of the well-known branching-time logic CTL: Timed CTL is interpreted over real-time systems like timed automata; Recursive CTL introduces a powerful recursion operator which takes the expressiveness of this logic CTL well beyond that of regular properties. The result is an expressive logic for real-time properties. We show that its model checking problem is decidable over timed automata, namely 2-EXPTIME-complete.
Cite as
Florian Bruse and Martin Lange. Model Checking Timed Recursive CTL. In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 12:1-12:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{bruse_et_al:LIPIcs.TIME.2021.12,
author = {Bruse, Florian and Lange, Martin},
title = {{Model Checking Timed Recursive CTL}},
booktitle = {28th International Symposium on Temporal Representation and Reasoning (TIME 2021)},
pages = {12:1--12:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-206-8},
ISSN = {1868-8969},
year = {2021},
volume = {206},
editor = {Combi, Carlo and Eder, Johann and Reynolds, Mark},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2021.12},
URN = {urn:nbn:de:0030-drops-147880},
doi = {10.4230/LIPIcs.TIME.2021.12},
annote = {Keywords: formal specification, temporal logic, real-time systems}
}
Document
Efficient Anytime Computation and Execution of Decoupled Robustness Envelopes for Temporal Plans
Abstract
One of the major limitations for the employment of model-based planning and scheduling in practical applications is the need of costly re-planning when an incongruence between the observed reality and the formal model is encountered during execution. Robustness Envelopes characterize the set of possible contingencies that a plan is able to address without re-planning, but their exact computation is expensive; furthermore, general robustness envelopes are not amenable for efficient execution.
In this paper, we present a novel, anytime algorithm to approximate Robustness Envelopes, making them scalable and executable. This is proven by an experimental analysis showing the efficiency of the algorithm, and by a concrete case study where the execution of robustness envelopes significantly reduces the number of re-plannings.
Cite as
Michael Cashmore, Alessandro Cimatti, Daniele Magazzeni, Andrea Micheli, and Parisa Zehtabi. Efficient Anytime Computation and Execution of Decoupled Robustness Envelopes for Temporal Plans. In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 13:1-13:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{cashmore_et_al:LIPIcs.TIME.2021.13,
author = {Cashmore, Michael and Cimatti, Alessandro and Magazzeni, Daniele and Micheli, Andrea and Zehtabi, Parisa},
title = {{Efficient Anytime Computation and Execution of Decoupled Robustness Envelopes for Temporal Plans}},
booktitle = {28th International Symposium on Temporal Representation and Reasoning (TIME 2021)},
pages = {13:1--13:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-206-8},
ISSN = {1868-8969},
year = {2021},
volume = {206},
editor = {Combi, Carlo and Eder, Johann and Reynolds, Mark},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2021.13},
URN = {urn:nbn:de:0030-drops-147895},
doi = {10.4230/LIPIcs.TIME.2021.13},
annote = {Keywords: Temporal Planning, Robustness Envelopes}
}
Document
Achieving a Sequenced, Relational Query Language with 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. Sequenced semantics is a special semantics for evaluating a query in a temporal database. The semantics stipulates that the query must, in effect, be evaluated simultaneously in each time instant using the tuples alive at that instant. Previous research has proposed changes to the query evaluation engine to support sequenced semantics. In this paper we show how to achieve sequenced semantics without modifying a query evaluation engine. Our technique has two pillars. First we use log-segmented timestamps to record a tuple’s lifetime. 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. Second, by taking advantage of the properties of log-segmented timestamps, we translate a sequenced relational algebra query to a non-temporal relational algebra query, using the operations already present in an unmodified, non-temporal query evaluation engine. The primary contribution of this paper is how to implement sequenced semantics using log-segmented timestamped tuples in a generic DBMS, which, to the best of our knowledge, has not been previously shown.
Cite as
Curtis E. Dyreson and M. A. Manazir Ahsan. Achieving a Sequenced, Relational Query Language with Log-Segmented Timestamps. In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 14:1-14:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{dyreson_et_al:LIPIcs.TIME.2021.14,
author = {Dyreson, Curtis E. and Ahsan, M. A. Manazir},
title = {{Achieving a Sequenced, Relational Query Language with Log-Segmented Timestamps}},
booktitle = {28th International Symposium on Temporal Representation and Reasoning (TIME 2021)},
pages = {14:1--14:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-206-8},
ISSN = {1868-8969},
year = {2021},
volume = {206},
editor = {Combi, Carlo and Eder, Johann and Reynolds, Mark},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2021.14},
URN = {urn:nbn:de:0030-drops-147900},
doi = {10.4230/LIPIcs.TIME.2021.14},
annote = {Keywords: Temporal databases, sequenced semantics, query evaluation, relational algebra}
}
Document
Olisipo: A Probabilistic Approach to the Adaptable Execution of Deterministic Temporal Plans
Abstract
The robust execution of a temporal plan in a perturbed environment is a problem that remains to be solved. Perturbed environments, such as the real world, are non-deterministic and filled with uncertainty. Hence, the execution of a temporal plan presents several challenges and the employed solution often consists of replanning when the execution fails. In this paper, we propose a novel algorithm, named Olisipo, which aims to maximise the probability of a successful execution of a temporal plan in perturbed environments. To achieve this, a probabilistic model is used in the execution of the plan, instead of in the building of the plan. This approach enables Olisipo to dynamically adapt the plan to changes in the environment. In addition to this, the execution of the plan is also adapted to the probability of successfully executing each action. Olisipo was compared to a simple dispatcher and it was shown that it consistently had a higher probability of successfully reaching a goal state in uncertain environments, performed fewer replans and also executed fewer actions. Hence, Olisipo offers a substantial improvement in performance for disturbed environments.
Cite as
Tomás Ribeiro, Oscar Lima, Michael Cashmore, Andrea Micheli, and Rodrigo Ventura. Olisipo: A Probabilistic Approach to the Adaptable Execution of Deterministic Temporal Plans. In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 15:1-15:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{ribeiro_et_al:LIPIcs.TIME.2021.15,
author = {Ribeiro, Tom\'{a}s and Lima, Oscar and Cashmore, Michael and Micheli, Andrea and Ventura, Rodrigo},
title = {{Olisipo: A Probabilistic Approach to the Adaptable Execution of Deterministic Temporal Plans}},
booktitle = {28th International Symposium on Temporal Representation and Reasoning (TIME 2021)},
pages = {15:1--15:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-206-8},
ISSN = {1868-8969},
year = {2021},
volume = {206},
editor = {Combi, Carlo and Eder, Johann and Reynolds, Mark},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2021.15},
URN = {urn:nbn:de:0030-drops-147913},
doi = {10.4230/LIPIcs.TIME.2021.15},
annote = {Keywords: Temporal Planning, Temporal Plan Execution, Robotics}
}
Document
A One-Pass Tree-Shaped Tableau for Defeasible LTL
Abstract
Defeasible Linear Temporal Logic is a defeasible temporal formalism for representing and verifying exception-tolerant systems. It is based on Linear Temporal Logic (LTL) and builds on the preferential approach of Kraus et al. for non-monotonic reasoning, which allows us to formalize and reason with exceptions. In this paper, we tackle the satisfiability checking problem for defeasible LTL. One of the methods for satisfiability checking in LTL is the one-pass tree shaped analytic tableau proposed by Reynolds. We adapt his tableau to defeasible LTL by integrating the preferential semantics to the method. The novelty of this work is in showing how the preferential semantics works in a tableau method for defeasible linear temporal logic. We introduce a sound and complete tableau method for a fragment that can serve as the basis for further exploring tableau methods for this logic.
Cite as
Anasse Chafik, Fahima Cheikh-Alili, Jean-François Condotta, and Ivan Varzinczak. A One-Pass Tree-Shaped Tableau for Defeasible LTL. In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{chafik_et_al:LIPIcs.TIME.2021.16,
author = {Chafik, Anasse and Cheikh-Alili, Fahima and Condotta, Jean-Fran\c{c}ois and Varzinczak, Ivan},
title = {{A One-Pass Tree-Shaped Tableau for Defeasible LTL}},
booktitle = {28th International Symposium on Temporal Representation and Reasoning (TIME 2021)},
pages = {16:1--16:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-206-8},
ISSN = {1868-8969},
year = {2021},
volume = {206},
editor = {Combi, Carlo and Eder, Johann and Reynolds, Mark},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2021.16},
URN = {urn:nbn:de:0030-drops-147924},
doi = {10.4230/LIPIcs.TIME.2021.16},
annote = {Keywords: Temporal logic, Non-monotonic reasoning, Tableau Calculi}
}
Document
1½-Player Stochastic StopWatch Games
Abstract
Stochastic timed games (STGs), introduced by Bouyer and Forejt, generalize continuous-time Markov chains and timed automata. Depending on the number of players - 2, 1, or 0 - subclasses of stochastic timed games are classified as 2½-player, 1½-player, and ½-player games where the ½ symbolizes the presence of the stochastic player. The qualitative and quantitative reachability problem for STGs was studied in [Patricia Bouyer and Vojtech Forejt, 2009] and [S. Akshay et al., 2016]. In this paper, we introduce stochastic stopwatch games (SSG), an extension of (STG) from clocks to stopwatches. We focus on 1½-player SSGs and prove that with two variables which can be either a clock or a stopwatch, qualitative reachability is decidable, whereas, if we increase the number of variables to three, with at least one stopwatch, the problem becomes undecidable.
Cite as
Sparsa Roychowdhury. 1½-Player Stochastic StopWatch Games. In 28th International Symposium on Temporal Representation and Reasoning (TIME 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 206, pp. 17:1-17:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{roychowdhury:LIPIcs.TIME.2021.17,
author = {Roychowdhury, Sparsa},
title = {{1½-Player Stochastic StopWatch Games}},
booktitle = {28th International Symposium on Temporal Representation and Reasoning (TIME 2021)},
pages = {17:1--17:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-206-8},
ISSN = {1868-8969},
year = {2021},
volume = {206},
editor = {Combi, Carlo and Eder, Johann and Reynolds, Mark},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2021.17},
URN = {urn:nbn:de:0030-drops-147934},
doi = {10.4230/LIPIcs.TIME.2021.17},
annote = {Keywords: Timed Automata, Stopwatches, Stochastic Timed Games}
}