Volume
LIPIcs, Volume 178
27th International Symposium on Temporal Representation and Reasoning (TIME 2020)
Event
TIME 2020, September 23-25, 2020, Bozen-Bolzano, ItalyEditors
Publication Details
- published at: 2020-09-15
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-167-2
- DBLP: db/conf/time/time2020
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 178, TIME 2020, Complete Volume
Abstract
LIPIcs, Volume 178, TIME 2020, Complete Volume
Cite as
27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 1-292, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@Proceedings{munozvelasco_et_al:LIPIcs.TIME.2020,
title = {{LIPIcs, Volume 178, TIME 2020, Complete Volume}},
booktitle = {27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
pages = {1--292},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-167-2},
ISSN = {1868-8969},
year = {2020},
volume = {178},
editor = {Mu\~{n}oz-Velasco, Emilio and Ozaki, Ana and Theobald, Martin},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020},
URN = {urn:nbn:de:0030-drops-129670},
doi = {10.4230/LIPIcs.TIME.2020},
annote = {Keywords: LIPIcs, Volume 178, TIME 2020, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{munozvelasco_et_al:LIPIcs.TIME.2020.0,
author = {Mu\~{n}oz-Velasco, Emilio and Ozaki, Ana and Theobald, Martin},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
pages = {0:i--0:xiv},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-167-2},
ISSN = {1868-8969},
year = {2020},
volume = {178},
editor = {Mu\~{n}oz-Velasco, Emilio and Ozaki, Ana and Theobald, Martin},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020.0},
URN = {urn:nbn:de:0030-drops-129688},
doi = {10.4230/LIPIcs.TIME.2020.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
Verifying Autonomous Robots: Challenges and Reflections (Invited Talk)
Abstract
Autonomous robots such as robot assistants, healthcare robots, industrial robots, autonomous vehicles etc. are being developed to carry out a range of tasks in different environments. The robots need to be able to act autonomously, choosing between a range of activities. They may be operating close to or in collaboration with humans, or in environments hazardous to humans where the robot is hard to reach if it malfunctions. We need to ensure that such robots are reliable, safe and trustworthy. In this talk I will discuss experiences from several projects in developing and applying verification techniques to autonomous robotic systems. In particular we consider: a robot assistant in a domestic house, a robot co-worker for a cooperative manufacturing task, multiple robot systems and robots operating in hazardous environments.
Cite as
Clare Dixon. Verifying Autonomous Robots: Challenges and Reflections (Invited Talk). In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 1:1-1:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{dixon:LIPIcs.TIME.2020.1,
author = {Dixon, Clare},
title = {{Verifying Autonomous Robots: Challenges and Reflections}},
booktitle = {27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
pages = {1:1--1:4},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-167-2},
ISSN = {1868-8969},
year = {2020},
volume = {178},
editor = {Mu\~{n}oz-Velasco, Emilio and Ozaki, Ana and Theobald, Martin},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020.1},
URN = {urn:nbn:de:0030-drops-129697},
doi = {10.4230/LIPIcs.TIME.2020.1},
annote = {Keywords: Verification, Autonomous Robots}
}
Document
Invited Talk
Temporal Modalities in Answer Set Programming (Invited Talk)
Abstract
Based on the answer set (or stable model) semantics for logic programs, Answer Set Programming (ASP) has become one of the most successful paradigms for practical Knowledge Representation and problem solving. Although ASP is naturally equipped for solving static combinatorial problems up to NP complexity (or ΣP2 in the disjunctive case) its
application to temporal scenarios has been frequent since its very beginning, partly due to its early use for reasoning about actions and change. Temporal problems normally suppose an extra challenge for ASP for several reasons. On the one hand, they normally raise the complexity (in the case of classical planning, for instance, it becomes PSPACE-complete), although this is usually accounted for by making repeated calls to an ASP solver. On the other hand, temporal scenarios also pose a representational challenge, since the basic ASP language does not support temporal expressions. To fill this representational gap, a temporal extension of ASP called Temporal Equilibrium Logic (TEL) was proposed in and extensively studied later. This formalism constitutes a modal, linear-time extension of Equilibrium Logic which, in its turn, is a complete logical characterisation of (standard) ASP based on the intermediate logic of Here-and-There (HT). As a result, TEL is an expressive non-monotonic modal logic that shares the syntax of Linear-Time Temporal Logic (LTL) but interprets temporal formulas under a non-monotonic semantics that properly extends stable models.
Cite as
Pedro Cabalar. Temporal Modalities in Answer Set Programming (Invited Talk). In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 2:1-2:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{cabalar:LIPIcs.TIME.2020.2,
author = {Cabalar, Pedro},
title = {{Temporal Modalities in Answer Set Programming}},
booktitle = {27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
pages = {2:1--2:5},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-167-2},
ISSN = {1868-8969},
year = {2020},
volume = {178},
editor = {Mu\~{n}oz-Velasco, Emilio and Ozaki, Ana and Theobald, Martin},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020.2},
URN = {urn:nbn:de:0030-drops-129707},
doi = {10.4230/LIPIcs.TIME.2020.2},
annote = {Keywords: Logic Programming, Temporal Logic, Answer Set Programming, Modal Logic}
}
Document
Invited Talk
Time and Business Process Management: Problems, Achievements, Challenges (Invited Talk)
Abstract
Processes have been successfully introduced for modeling dynamic phenomena in many areas like business, production, health care, etc. Many of these applications require to adequately deal with temporal aspects. Process models need to express temporal durations, temporal constraints like allowed time between events, and deadlines. For checking the correctness of process definitions with temporal constraints, different notions and algorithms have been developed. Schedules for the execution of processes can be computed and proactive time management supports process managers to avoid time failures during the execution of a process. We present an overview of the problems and the requirements for treating time in business processes and the solutions achieved by applying results and techniques of research in temporal representation and reasoning. We reflect where expectations have not yet been met and sketch challenges in temporal representation and reasoning for addressing advanced requirements of the management of business processes.
Cite as
Johann Eder and Marco Franceschetti. Time and Business Process Management: Problems, Achievements, Challenges (Invited Talk). In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 3:1-3:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{eder_et_al:LIPIcs.TIME.2020.3,
author = {Eder, Johann and Franceschetti, Marco},
title = {{Time and Business Process Management: Problems, Achievements, Challenges}},
booktitle = {27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
pages = {3:1--3:8},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-167-2},
ISSN = {1868-8969},
year = {2020},
volume = {178},
editor = {Mu\~{n}oz-Velasco, Emilio and Ozaki, Ana and Theobald, Martin},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020.3},
URN = {urn:nbn:de:0030-drops-129716},
doi = {10.4230/LIPIcs.TIME.2020.3},
annote = {Keywords: Business Process management, Temporal constraints, Scheduling, Process Evolution, Probabilistic Controllability}
}
Document
Negotiating Temporal Commitments in Cross-Organizational Business Processes
Abstract
Cross-organizational business processes emerge from the cooperation of intra-organizational business processes through exchange of messages. The involved parties agree on communication protocols, which contain in particular temporal constraints: as obligations on one hand, and as guarantees on the other hand. These constraints form also requirements for the design of the hidden implementation of the processes and are the basis for control decisions for each party. We present a comprehensive methodology for modeling the temporal aspects of cross-organizational business processes, checking dynamic controllability of such processes, and supporting the negotiation of temporal commitments. We do so by computing the consequences of temporal constraints in choreographies, and by computing the weakest preconditions for the dynamic controllability of a participating process.
Cite as
Marco Franceschetti and Johann Eder. Negotiating Temporal Commitments in Cross-Organizational Business Processes. In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 4:1-4:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{franceschetti_et_al:LIPIcs.TIME.2020.4,
author = {Franceschetti, Marco and Eder, Johann},
title = {{Negotiating Temporal Commitments in Cross-Organizational Business Processes}},
booktitle = {27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
pages = {4:1--4:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-167-2},
ISSN = {1868-8969},
year = {2020},
volume = {178},
editor = {Mu\~{n}oz-Velasco, Emilio and Ozaki, Ana and Theobald, Martin},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020.4},
URN = {urn:nbn:de:0030-drops-129729},
doi = {10.4230/LIPIcs.TIME.2020.4},
annote = {Keywords: Cross-organizational processes, Temporal parameters, Range negotiation}
}
Document
The Horn Fragment of Branching Algebra
Abstract
Branching Algebra is the natural branching-time generalization of Allen’s Interval Algebra. As in the linear case, the consistency problem for Branching Algebra is NP-hard. Being relatively new, however, not much is known about the computational behaviour of the consistency problem of its sub-algebras, except in the case of the recently found subset of convex branching relations, for which the consistency of a network can be tested via path consistency and it is therefore deterministic polynomial. In this paper, following Nebel and Bürckert, we define the Horn fragment of Branching Algebra, and prove that it is a sub-algebra of the latter, being closed under inverse, intersection, and composition, that it strictly contains both the convex fragment of Branching Algebra and the Horn fragment of Interval Algebra, and that its consistency problem can be decided via path consistency. Finally, we experimentally prove that the Horn fragment of Branching Algebra can be used as an heuristic for checking the consistency of a generic network with a considerable improvement over the convex subset.
Cite as
Alessandro Bertagnon, Marco Gavanelli, Alessandro Passantino, Guido Sciavicco, and Stefano Trevisani. The Horn Fragment of Branching Algebra. In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{bertagnon_et_al:LIPIcs.TIME.2020.5,
author = {Bertagnon, Alessandro and Gavanelli, Marco and Passantino, Alessandro and Sciavicco, Guido and Trevisani, Stefano},
title = {{The Horn Fragment of Branching Algebra}},
booktitle = {27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
pages = {5:1--5:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-167-2},
ISSN = {1868-8969},
year = {2020},
volume = {178},
editor = {Mu\~{n}oz-Velasco, Emilio and Ozaki, Ana and Theobald, Martin},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020.5},
URN = {urn:nbn:de:0030-drops-129736},
doi = {10.4230/LIPIcs.TIME.2020.5},
annote = {Keywords: Constraint programming, Consistency, Branching time, Horn Fragment}
}
Document
Temporal Logic with Recursion
Abstract
We introduce extensions of the standard temporal logics CTL and LTL with a recursion operator that takes propositional arguments. Unlike other proposals for modal fixpoint logics of high expressive power, we obtain logics that retain some of the appealing pragmatic advantages of CTL and LTL, yet have expressive power beyond that of the modal μ-calculus or MSO. We advocate these logics by showing how the recursion operator can be used to express interesting non-regular properties. We also study decidability and complexity issues of the standard decision problems.
Cite as
Florian Bruse and Martin Lange. Temporal Logic with Recursion. In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 6:1-6:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{bruse_et_al:LIPIcs.TIME.2020.6,
author = {Bruse, Florian and Lange, Martin},
title = {{Temporal Logic with Recursion}},
booktitle = {27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
pages = {6:1--6:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-167-2},
ISSN = {1868-8969},
year = {2020},
volume = {178},
editor = {Mu\~{n}oz-Velasco, Emilio and Ozaki, Ana and Theobald, Martin},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020.6},
URN = {urn:nbn:de:0030-drops-129748},
doi = {10.4230/LIPIcs.TIME.2020.6},
annote = {Keywords: formal specification, temporal logic, expressive power}
}
Document
Parametric Model Checking Continuous-Time Markov Chains
Abstract
CSL is a well-known temporal logic for specifying properties of real-time stochastic systems, such as continuous-time Markov chains. We introduce PCSL, an extension of CSL that allows using existentially quantified parameters in timing constraints, and investigate its expressiveness and decidability over properties of continuous-time Markov chains. Assuming Schanuel’s Conjecture, we prove the decidability of model checking the one-parameter fragment of PCSL on continuous-time Markov chains. Technically, the central problem we solve (relying on Schanuel’s Conjecture) is to decide positivity of real-valued exponential polynomial functions on bounded intervals. A second contribution is to give a reduction of the Positivity Problem for matrix exponentials to the PCSL model checking problem, suggesting that it will be difficult to give an unconditional proof of the decidability of model checking PCSL.
Cite as
Catalin-Andrei Ilie and James Ben Worrell. Parametric Model Checking Continuous-Time Markov Chains. In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{ilie_et_al:LIPIcs.TIME.2020.7,
author = {Ilie, Catalin-Andrei and Worrell, James Ben},
title = {{Parametric Model Checking Continuous-Time Markov Chains}},
booktitle = {27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
pages = {7:1--7:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-167-2},
ISSN = {1868-8969},
year = {2020},
volume = {178},
editor = {Mu\~{n}oz-Velasco, Emilio and Ozaki, Ana and Theobald, Martin},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020.7},
URN = {urn:nbn:de:0030-drops-129752},
doi = {10.4230/LIPIcs.TIME.2020.7},
annote = {Keywords: Probabilistic Continuous Stochastic Logic, Continuous-time Markov Chains, model checking, Schanuel’s Conjecture, positivity problem}
}
Document
Universal Solutions in Temporal Data Exchange
Abstract
During the past fifteen years, data exchange has been explored in depth and in a variety of different settings. Even though temporal databases constitute a mature area of research studied over several decades, the investigation of temporal data exchange was initiated only very recently. We analyze the properties of universal solutions in temporal data exchange with emphasis on the relationship between universal solutions in the context of concrete time and universal solutions in the context of abstract time. We show that challenges arise even in the setting in which the data exchange specifications involve a single temporal variable. After this, we identify settings, including data exchange settings that involve multiple temporal variables, in which these challenges can be overcome.
Cite as
Zehui Cheng and Phokion G. Kolaitis. Universal Solutions in Temporal Data Exchange. In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{cheng_et_al:LIPIcs.TIME.2020.8,
author = {Cheng, Zehui and Kolaitis, Phokion G.},
title = {{Universal Solutions in Temporal Data Exchange}},
booktitle = {27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
pages = {8:1--8:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-167-2},
ISSN = {1868-8969},
year = {2020},
volume = {178},
editor = {Mu\~{n}oz-Velasco, Emilio and Ozaki, Ana and Theobald, Martin},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020.8},
URN = {urn:nbn:de:0030-drops-129763},
doi = {10.4230/LIPIcs.TIME.2020.8},
annote = {Keywords: temporal databases, database dependencies, data exchange, universal solutions, abstract time, concrete time, Allen’s relations}
}
Document
Knowledge Extraction with Interval Temporal Logic Decision Trees
Abstract
Multivariate temporal, or time, series classification is, in a way, the temporal generalization of (numeric) classification, as every instance is described by multiple time series instead of multiple values. Symbolic classification is the machine learning strategy to extract explicit knowledge from a data set, and the problem of symbolic classification of multivariate temporal series requires the design, implementation, and test of ad-hoc machine learning algorithms, such as, for example, algorithms for the extraction of temporal versions of decision trees. One of the most well-known algorithms for decision tree extraction from categorical data is Quinlan’s ID3, which was later extended to deal with numerical attributes, resulting in an algorithm known as C4.5, and implemented in many open-sources data mining libraries, including the so-called Weka, which features an implementation of C4.5 called J48. ID3 was recently generalized to deal with temporal data in form of timelines, which can be seen as discrete (categorical) versions of multivariate time series, and such a generalization, based on the interval temporal logic HS, is known as Temporal ID3. In this paper we introduce Temporal C4.5, that allows the extraction of temporal decision trees from undiscretized multivariate time series, describe its implementation, called Temporal J48, and discuss the outcome of a set of experiments with the latter on a collection of public data sets, comparing the results with those obtained by other, classical, multivariate time series classification methods.
Cite as
Guido Sciavicco and Ionel Eduard Stan. Knowledge Extraction with Interval Temporal Logic Decision Trees. In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{sciavicco_et_al:LIPIcs.TIME.2020.9,
author = {Sciavicco, Guido and Stan, Ionel Eduard},
title = {{Knowledge Extraction with Interval Temporal Logic Decision Trees}},
booktitle = {27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
pages = {9:1--9:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-167-2},
ISSN = {1868-8969},
year = {2020},
volume = {178},
editor = {Mu\~{n}oz-Velasco, Emilio and Ozaki, Ana and Theobald, Martin},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020.9},
URN = {urn:nbn:de:0030-drops-129776},
doi = {10.4230/LIPIcs.TIME.2020.9},
annote = {Keywords: Interval Temporal Logic, Decision Trees, Explainable AI, Time series}
}
Document
Window-Slicing Techniques Extended to Spanning-Event Streams
Abstract
Streaming systems often use slices to share computation costs among overlapping windows. However they are limited to instantaneous events where only one point represents the event. Here, we extend streams to events that come with a duration, denoted as spanning events. After a short review of the new constraints ensued by event lifespan in a temporal sliding-window context, we propose a new structure for dealing with slices in such an environment, and prove that our technique is both correct and effective to deal with such spanning events.
Cite as
Aurélie Suzanne, Guillaume Raschia, José Martinez, and Damien Tassetti. Window-Slicing Techniques Extended to Spanning-Event Streams. In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 10:1-10:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{suzanne_et_al:LIPIcs.TIME.2020.10,
author = {Suzanne, Aur\'{e}lie and Raschia, Guillaume and Martinez, Jos\'{e} and Tassetti, Damien},
title = {{Window-Slicing Techniques Extended to Spanning-Event Streams}},
booktitle = {27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
pages = {10:1--10:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-167-2},
ISSN = {1868-8969},
year = {2020},
volume = {178},
editor = {Mu\~{n}oz-Velasco, Emilio and Ozaki, Ana and Theobald, Martin},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020.10},
URN = {urn:nbn:de:0030-drops-129783},
doi = {10.4230/LIPIcs.TIME.2020.10},
annote = {Keywords: Data Stream, Spanning-events, Temporal Aggregates, Sliding Windows}
}
Document
Mining Significant Temporal Networks Is Polynomial
Abstract
A Conditional Simple Temporal Network with Uncertainty and Decisions (CSTNUD) is a formalism that tackles controllable and uncontrollable durations as well as controllable and uncontrollable choices simultaneously. In the classic top-down model-based engineering approach, a designer builds a CSTNUD to model, validate and execute some temporal plan of interest. Instead, in this paper, we investigate the bottom-up approach by providing a deterministic polynomial time algorithm to mine a CSTNUD from a set of execution traces (i.e., a log). This paper paves the way for the design of controllable temporal networks mined from traces that also contain information on uncontrollable events.
Cite as
Guido Sciavicco, Matteo Zavatteri, and Tiziano Villa. Mining Significant Temporal Networks Is Polynomial. In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 11:1-11:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{sciavicco_et_al:LIPIcs.TIME.2020.11,
author = {Sciavicco, Guido and Zavatteri, Matteo and Villa, Tiziano},
title = {{Mining Significant Temporal Networks Is Polynomial}},
booktitle = {27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
pages = {11:1--11:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-167-2},
ISSN = {1868-8969},
year = {2020},
volume = {178},
editor = {Mu\~{n}oz-Velasco, Emilio and Ozaki, Ana and Theobald, Martin},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020.11},
URN = {urn:nbn:de:0030-drops-129792},
doi = {10.4230/LIPIcs.TIME.2020.11},
annote = {Keywords: Mining temporal constraints, cstnud, uncertainty, significant temporal network}
}
Document
Dynamic Branching in Qualitative Constraint Networks via Counting Local Models
Abstract
We introduce and evaluate dynamic branching strategies for solving Qualitative Constraint Networks (QCNs), which are networks that are mostly used to represent and reason about spatial and temporal information via the use of simple qualitative relations, e.g., a constraint can be "Task A is scheduled after or during Task C". In qualitative constraint-based reasoning, the state-of-the-art approach to tackle a given QCN consists in employing a backtracking algorithm, where the branching decisions during search are governed by the restrictiveness of the possible relations for a given constraint (e.g., after can be more restrictive than during). In the literature, that restrictiveness is defined a priori by means of static weights that are precomputed and associated with the relations of a given calculus, without any regard to the particulars of a given network instance of that calculus, such as its structure. In this paper, we address this limitation by proposing heuristics that dynamically associate a weight with a relation, based on the count of local models (or local scenarios) that the relation is involved with in a given QCN; these models are local in that they focus on triples of variables instead of the entire QCN. Therefore, our approach is adaptive and seeks to make branching decisions that preserve most of the solutions by determining what proportion of local solutions agree with that decision. Experimental results with a random and a structured dataset of QCNs of Interval Algebra show that it is possible to achieve up to 5 times better performance for structured instances, whilst maintaining non-negligible gains of around 20% for random ones.
Cite as
Michael Sioutis and Diedrich Wolter. Dynamic Branching in Qualitative Constraint Networks via Counting Local Models. In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 12:1-12:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{sioutis_et_al:LIPIcs.TIME.2020.12,
author = {Sioutis, Michael and Wolter, Diedrich},
title = {{Dynamic Branching in Qualitative Constraint Networks via Counting Local Models}},
booktitle = {27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
pages = {12:1--12:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-167-2},
ISSN = {1868-8969},
year = {2020},
volume = {178},
editor = {Mu\~{n}oz-Velasco, Emilio and Ozaki, Ana and Theobald, Martin},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020.12},
URN = {urn:nbn:de:0030-drops-129802},
doi = {10.4230/LIPIcs.TIME.2020.12},
annote = {Keywords: Qualitative constraints, spatial and temporal reasoning, counting local models, dynamic branching, adaptive algorithm}
}
Document
Non-Simultaneity as a Design Constraint
Abstract
Whether one or multiple hardware execution units are activated (i.e. CPU cores), invalid resource sharing, notably due to simultaneous accesses, proves to be problematic as it can yield to unexpected runtime behaviors with negative implications such as security or safety issues. The growing interest for off-the-shelf multi-core architectures in sensitive applications motivates the need for safe resources sharing. If critical sections are a well-known solution from imperative and non-temporized programming models, they fail to provide safety guarantees. By leveraging the time-triggered programming model, this paper aims at enforcing that identified critical windows of computations can never be simultaneously executed. We achieve this result by determining, before an application is compiled, the exact dates during which a task accesses a shared resource, which enables the off-line validation of non-simultaneity constraints.
Cite as
Jean Guyomarc'h, François Guerret, Bilal El Mejjati, Emmanuel Ohayon, Bastien Vincke, and Alain Mérigot. Non-Simultaneity as a Design Constraint. In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 13:1-13:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{guyomarch_et_al:LIPIcs.TIME.2020.13,
author = {Guyomarc'h, Jean and Guerret, Fran\c{c}ois and El Mejjati, Bilal and Ohayon, Emmanuel and Vincke, Bastien and M\'{e}rigot, Alain},
title = {{Non-Simultaneity as a Design Constraint}},
booktitle = {27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
pages = {13:1--13:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-167-2},
ISSN = {1868-8969},
year = {2020},
volume = {178},
editor = {Mu\~{n}oz-Velasco, Emilio and Ozaki, Ana and Theobald, Martin},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020.13},
URN = {urn:nbn:de:0030-drops-129819},
doi = {10.4230/LIPIcs.TIME.2020.13},
annote = {Keywords: Temporal reasoning, Temporal constraints, Specification and verification of systems}
}
Document
One-Pass Context-Based Tableaux Systems for CTL and ECTL
Abstract
When building tableau for temporal logic formulae, applying a two-pass construction, we first check the validity of the given tableaux input by creating a tableau graph, and then, in the second "pass", we check if all the eventualities are satisfied. In one-pass tableaux checking the validity of the input does not require these auxiliary constructions. This paper continues the development of one-pass tableau method for temporal logics introducing tree-style one-pass tableau systems for Computation Tree Logic (CTL) and shows how this can be extended to capture Extended CTL (ECTL). A distinctive feature here is the utilisation, for the core tableau construction, of the concept of a context of an eventuality which forces its earliest fulfilment. Relevant algorithms for obtaining a systematic tableau for these branching-time logics are also defined. We prove the soundness and completeness of the method. With these developments of a tree-shaped one-pass tableau for CTL and ECTL, we have formalisms which are well suited for the automation and are amenable for the implementation, and for the formulation of dual sequent calculi. This brings us one step closer to the application of one-pass context-based tableaux in certified model checking for a variety of CTL-type branching-time logics.
Cite as
Alex Abuin, Alexander Bolotov, Montserrat Hermo, and Paqui Lucio. One-Pass Context-Based Tableaux Systems for CTL and ECTL. In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{abuin_et_al:LIPIcs.TIME.2020.14,
author = {Abuin, Alex and Bolotov, Alexander and Hermo, Montserrat and Lucio, Paqui},
title = {{One-Pass Context-Based Tableaux Systems for CTL and ECTL}},
booktitle = {27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
pages = {14:1--14:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-167-2},
ISSN = {1868-8969},
year = {2020},
volume = {178},
editor = {Mu\~{n}oz-Velasco, Emilio and Ozaki, Ana and Theobald, Martin},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020.14},
URN = {urn:nbn:de:0030-drops-129824},
doi = {10.4230/LIPIcs.TIME.2020.14},
annote = {Keywords: Temporal logic, fairness, expressiveness, branching-time}
}
Document
TESL: A Model with Metric Time for Modeling and Simulation
Abstract
Real-time and distributed systems are increasingly finding their way into critical embedded systems. On one side, computations need to be achieved within specific time constraints. On the other side, computations may be spread among various units which are not necessarily sharing a global clock. Our study is focused on a specification language - named TESL - used for coordinating concurrent models with timed constraints. We explore various questions related to time when modeling systems, and aim at showing that TESL can be introduced as a reasonable balance of expressiveness and decidability to tackle issues in complex systems. This paper introduces (1) an overview of the TESL language and its main properties (polychrony, stutter-invariance, coinduction for simulation), (2) extensions to the language and their applications.
Cite as
Hai Nguyen Van, Frédéric Boulanger, and Burkhart Wolff. TESL: A Model with Metric Time for Modeling and Simulation. In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 15:1-15:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{nguyenvan_et_al:LIPIcs.TIME.2020.15,
author = {Nguyen Van, Hai and Boulanger, Fr\'{e}d\'{e}ric and Wolff, Burkhart},
title = {{TESL: A Model with Metric Time for Modeling and Simulation}},
booktitle = {27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
pages = {15:1--15:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-167-2},
ISSN = {1868-8969},
year = {2020},
volume = {178},
editor = {Mu\~{n}oz-Velasco, Emilio and Ozaki, Ana and Theobald, Martin},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020.15},
URN = {urn:nbn:de:0030-drops-129837},
doi = {10.4230/LIPIcs.TIME.2020.15},
annote = {Keywords: Timed Systems, Semantics, Models, Simulation}
}
Document
Complexity of Qualitative Timeline-Based Planning
Abstract
The timeline-based approach to automated planning was originally developed in the context of space missions. In this approach, problem domains are expressed as systems consisting of independent but interacting components whose behaviors over time, the timelines, are governed by a set of temporal constraints, called synchronization rules. Although timeline-based system descriptions have been successfully used in practice for decades, the research on the theoretical aspects only started recently. In the last few years, some interesting results have been shown concerning both its expressive power and the computational complexity of the related planning problem. In particular, the general problem has been proved to be EXPSPACE-complete. Given the applicability of the approach in many practical scenarios, it is thus natural to ask whether computationally simpler but still expressive fragments can be identified. In this paper, we study the timeline-based planning problem with the restriction that only qualitative synchronization rules, i.e., rules without explicit time bounds in the constraints, are allowed. We show that the problem becomes PSPACE-complete.
Cite as
Dario Della Monica, Nicola Gigante, Salvatore La Torre, and Angelo Montanari. Complexity of Qualitative Timeline-Based Planning. In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 16:1-16:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{dellamonica_et_al:LIPIcs.TIME.2020.16,
author = {Della Monica, Dario and Gigante, Nicola and La Torre, Salvatore and Montanari, Angelo},
title = {{Complexity of Qualitative Timeline-Based Planning}},
booktitle = {27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
pages = {16:1--16:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-167-2},
ISSN = {1868-8969},
year = {2020},
volume = {178},
editor = {Mu\~{n}oz-Velasco, Emilio and Ozaki, Ana and Theobald, Martin},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020.16},
URN = {urn:nbn:de:0030-drops-129847},
doi = {10.4230/LIPIcs.TIME.2020.16},
annote = {Keywords: Timeline-based planning, qualitative temporal constraints, complexity}
}
Document
A Note on C² Interpreted over Finite Data-Words
Abstract
We consider the satisfiability problem for the two-variable fragment of first-order logic extended with counting quantifiers, interpreted over finite words with data, denoted here with C²[≤ , succ, ∼, π_bin]. In our scenario, we allow for using arbitrary many uninterpreted binary predicates from π_bin, two navigational predicates ≤ and succ over word positions as well as a data-equality predicate ∼. We prove that the obtained logic is undecidable, which contrasts with the decidability of the logic without counting by Montanari, Pazzaglia and Sala [Angelo Montanari et al., 2016]. We supplement our results with decidability for several sub-fragments of C²[≤ , succ, ∼, π_bin], e.g. without binary predicates, without successor succ, or under the assumption that the total number of positions carrying the same data value in a data-word is bounded by an a priori given constant.
Cite as
Bartosz Bednarczyk and Piotr Witkowski. A Note on C² Interpreted over Finite Data-Words. In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 17:1-17:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{bednarczyk_et_al:LIPIcs.TIME.2020.17,
author = {Bednarczyk, Bartosz and Witkowski, Piotr},
title = {{A Note on C² Interpreted over Finite Data-Words}},
booktitle = {27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
pages = {17:1--17:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-167-2},
ISSN = {1868-8969},
year = {2020},
volume = {178},
editor = {Mu\~{n}oz-Velasco, Emilio and Ozaki, Ana and Theobald, Martin},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020.17},
URN = {urn:nbn:de:0030-drops-129850},
doi = {10.4230/LIPIcs.TIME.2020.17},
annote = {Keywords: Two-variable logic, data-words, VASS, decidability, undecidability, counting}
}
Document
Stab-Forests: Dynamic Data Structures for Efficient Temporal Query Processing
Abstract
Many sources of data have temporal start and end attributes or are created in a time-ordered manner. Hence, it is only natural to consider joining datasets based on these temporal attributes. To do so efficiently, several internal-memory temporal join algorithms have recently been proposed. Unfortunately, these join algorithms are designed to join entire datasets and cannot efficiently join skewed datasets in which only few events participate in the join result.
To support high-performance internal-memory temporal joins of skewed datasets, we propose the skip-join algorithm, which operates on stab-forests. The stab-forest is a novel dynamic data structure for indexing temporal data that allows efficient updates when events are appended in a time-based order. Our stab-forests efficiently support not only traditional temporal stab-queries, but also more general multi-stab-queries. We conducted an experimental evaluation to compare the skip-join algorithm with state-of-the-art techniques using real-world datasets. We observed that the skip-join algorithm outperforms other techniques by an order of magnitude when joining skewed datasets and delivers comparable performance to other techniques on non-skewed datasets.
Cite as
Jelle Hellings and Yuqing Wu. Stab-Forests: Dynamic Data Structures for Efficient Temporal Query Processing. In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 18:1-18:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{hellings_et_al:LIPIcs.TIME.2020.18,
author = {Hellings, Jelle and Wu, Yuqing},
title = {{Stab-Forests: Dynamic Data Structures for Efficient Temporal Query Processing}},
booktitle = {27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
pages = {18:1--18:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-167-2},
ISSN = {1868-8969},
year = {2020},
volume = {178},
editor = {Mu\~{n}oz-Velasco, Emilio and Ozaki, Ana and Theobald, Martin},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020.18},
URN = {urn:nbn:de:0030-drops-129869},
doi = {10.4230/LIPIcs.TIME.2020.18},
annote = {Keywords: Cache-friendly temporal joins, temporal data, skewed data, stab-queries, temporal indices}
}
Document
On the Decidability of a Fragment of preferential LTL
Abstract
Linear Temporal Logic (LTL) has found extensive applications in Computer Science and Artificial Intelligence, notably as a formal framework for representing and verifying computer systems that vary over time. Non-monotonic reasoning, on the other hand, allows us to formalize and reason with exceptions and the dynamics of information. The goal of this paper is therefore to enrich temporal formalisms with non-monotonic reasoning features. We do so by investigating a preferential semantics for defeasible LTL along the lines of that extensively studied by Kraus et al. in the propositional case and recently extended to modal and description logics. The main contribution of the paper is a decidability result for a meaningful fragment of preferential LTL that can serve as the basis for further exploration of defeasibility in temporal formalisms.
Cite as
Anasse Chafik, Fahima Cheikh-Alili, Jean-François Condotta, and Ivan Varzinczak. On the Decidability of a Fragment of preferential LTL. In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{chafik_et_al:LIPIcs.TIME.2020.19,
author = {Chafik, Anasse and Cheikh-Alili, Fahima and Condotta, Jean-Fran\c{c}ois and Varzinczak, Ivan},
title = {{On the Decidability of a Fragment of preferential LTL}},
booktitle = {27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
pages = {19:1--19:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-167-2},
ISSN = {1868-8969},
year = {2020},
volume = {178},
editor = {Mu\~{n}oz-Velasco, Emilio and Ozaki, Ana and Theobald, Martin},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020.19},
URN = {urn:nbn:de:0030-drops-129871},
doi = {10.4230/LIPIcs.TIME.2020.19},
annote = {Keywords: Knowledge Representation, non-monotonic reasoning, temporal logic}
}