Volume
LIPIcs, Volume 120
25th International Symposium on Temporal Representation and Reasoning (TIME 2018)
Event
TIME 2018, October 15-17, 2018, Warsaw, PolandEditors
Publication Details
- published at: 2018-10-08
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-089-7
- DBLP: db/conf/time/time2018
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 120, TIME'18, Complete Volume
Abstract
LIPIcs, Volume 120, TIME'18, Complete Volume
Cite as
25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@Proceedings{alechina_et_al:LIPIcs.TIME.2018,
title = {{LIPIcs, Volume 120, TIME'18, Complete Volume}},
booktitle = {25th International Symposium on Temporal Representation and Reasoning (TIME 2018)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-089-7},
ISSN = {1868-8969},
year = {2018},
volume = {120},
editor = {Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018},
URN = {urn:nbn:de:0030-drops-98443},
doi = {10.4230/LIPIcs.TIME.2018},
annote = {Keywords: Theory of computation, Logic, Information systems, Temporal data, Computing methodologies, Knowledge representation and reasoning}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{alechina_et_al:LIPIcs.TIME.2018.0,
author = {Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {25th International Symposium on Temporal Representation and Reasoning (TIME 2018)},
pages = {0:i--0:xiv},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-089-7},
ISSN = {1868-8969},
year = {2018},
volume = {120},
editor = {Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018.0},
URN = {urn:nbn:de:0030-drops-97654},
doi = {10.4230/LIPIcs.TIME.2018.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Paper
On Temporal and Separation Logics (Invited Paper)
Abstract
There exist many success stories about the introduction of logics designed for the formal verification of computer systems. Obviously, the introduction of temporal logics to computer science has been a major step in the development of model-checking techniques. More recently, separation logics extend Hoare logic for reasoning about programs with dynamic data structures, leading to many contributions on theory, tools and applications. In this talk, we illustrate how several features of separation logics, for instance the key concept of separation, are related to similar notions in temporal logics. We provide formal correspondences (when possible) and present an overview of related works from the literature. This is also the opportunity to present bridges between well-known temporal logics and more recent separation logics.
Cite as
Stéphane Demri. On Temporal and Separation Logics (Invited Paper). In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 1:1-1:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{demri:LIPIcs.TIME.2018.1,
author = {Demri, St\'{e}phane},
title = {{On Temporal and Separation Logics}},
booktitle = {25th International Symposium on Temporal Representation and Reasoning (TIME 2018)},
pages = {1:1--1:4},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-089-7},
ISSN = {1868-8969},
year = {2018},
volume = {120},
editor = {Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018.1},
URN = {urn:nbn:de:0030-drops-97662},
doi = {10.4230/LIPIcs.TIME.2018.1},
annote = {Keywords: separation logics, temporal logics, expressive power}
}
Document
Invited Paper
Database Technology for Processing Temporal Data (Invited Paper)
Abstract
Despite the ubiquity of temporal data and considerable research on processing such data, database systems largely remain designed for processing the current state of some modeled reality. More recently, we have seen an increasing interest in processing historical or temporal data. The SQL:2011 standard introduced some temporal features, and commercial database management systems have started to offer temporal functionalities in a step-by-step manner. There has also been a proposal for a more fundamental and comprehensive solution for sequenced temporal queries, which allows a tight integration into relational database systems, thereby taking advantage of existing query optimization and evaluation technologies. New challenges for processing temporal data arise with multiple dimensions of time and the increasing amounts of data, including time series data that represent a special kind of temporal data.
Cite as
Michael H. Böhlen, Anton Dignös, Johann Gamper, and Christian S. Jensen. Database Technology for Processing Temporal Data (Invited Paper). In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 2:1-2:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{bohlen_et_al:LIPIcs.TIME.2018.2,
author = {B\"{o}hlen, Michael H. and Dign\"{o}s, Anton and Gamper, Johann and Jensen, Christian S.},
title = {{Database Technology for Processing Temporal Data}},
booktitle = {25th International Symposium on Temporal Representation and Reasoning (TIME 2018)},
pages = {2:1--2:7},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-089-7},
ISSN = {1868-8969},
year = {2018},
volume = {120},
editor = {Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018.2},
URN = {urn:nbn:de:0030-drops-97674},
doi = {10.4230/LIPIcs.TIME.2018.2},
annote = {Keywords: Temporal databases, temporal query processing, sequenced semantics, SQL}
}
Document
Invited Paper
Model Checking Strategic Ability - Why, What, and Especially: How? (Invited Paper)
Abstract
Automated verification of discrete-state systems has been a hot topic in computer science for over 35 years. Model checking of temporal and strategic properties is one of the most prominent and most successful approaches here. In this talk, I present a brief introduction to the topic, and mention some relevant properties that one might like to verify this way. Then, I describe some recent results on approximate model checking and model reductions, which can be applied to facilitate verification of notoriously hard cases.
Cite as
Wojciech Jamroga. Model Checking Strategic Ability - Why, What, and Especially: How? (Invited Paper). In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 3:1-3:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{jamroga:LIPIcs.TIME.2018.3,
author = {Jamroga, Wojciech},
title = {{Model Checking Strategic Ability - Why, What, and Especially: How?}},
booktitle = {25th International Symposium on Temporal Representation and Reasoning (TIME 2018)},
pages = {3:1--3:10},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-089-7},
ISSN = {1868-8969},
year = {2018},
volume = {120},
editor = {Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018.3},
URN = {urn:nbn:de:0030-drops-97681},
doi = {10.4230/LIPIcs.TIME.2018.3},
annote = {Keywords: model checking, strategic ability, alternating-time temporal logic, imperfect information games, approximate verification, model reductions}
}
Document
Predicting the Evolution of Communities with Online Inductive Logic Programming
Abstract
In the recent years research on dynamic social network has increased, which is also due to the availability of data sets from streaming media. Modeling a network's dynamic behaviour can be performed at the level of communities, which represent their mesoscale structure. Communities arise as a result of user to user interaction. In the current work we aim to predict the evolution of communities, i.e. to predict their future form. While this problem has been studied in the past as a supervised learning problem with a variety of classifiers, the problem is that the "knowledge" of a classifier is opaque and consequently incomprehensible to a human. Thus we have employed first order logic, and in particular the event calculus to represent the communities and their evolution. We addressed the problem of predicting the evolution as an online Inductive Logic Programming problem (ILP), where the issue is to learn first order logical clauses that associate evolutionary events, and particular Growth, Shrinkage, Continuation and Dissolution to lower level events. The lower level events are features that represent the structural and temporal characteristics of communities. Experiments have been performed on a real life data set form the Mathematics StackExchange forum, with the OLED framework for ILP. In doing so we have produced clauses that model both short term and long term correlations.
Cite as
George Athanasopoulos, George Paliouras, Dimitrios Vogiatzis, Grigorios Tzortzis, and Nikos Katzouris. Predicting the Evolution of Communities with Online Inductive Logic Programming. In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 4:1-4:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{athanasopoulos_et_al:LIPIcs.TIME.2018.4,
author = {Athanasopoulos, George and Paliouras, George and Vogiatzis, Dimitrios and Tzortzis, Grigorios and Katzouris, Nikos},
title = {{Predicting the Evolution of Communities with Online Inductive Logic Programming}},
booktitle = {25th International Symposium on Temporal Representation and Reasoning (TIME 2018)},
pages = {4:1--4:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-089-7},
ISSN = {1868-8969},
year = {2018},
volume = {120},
editor = {Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018.4},
URN = {urn:nbn:de:0030-drops-97691},
doi = {10.4230/LIPIcs.TIME.2018.4},
annote = {Keywords: Social Network Analysis, Community Evolution Prediction, Machine Learning, Inductive Logic Programming, Event Calculus, Online Learning}
}
Document
Extending Fairness Expressibility of ECTL+: A Tree-Style One-Pass Tableau Approach
Abstract
Temporal logic has become essential for various areas in computer science, most notably for the specification and verification of hardware and software systems. For the specification purposes rich temporal languages are required that, in particular, can express fairness constraints. For linear-time logics which deal with fairness in the linear-time setting, one-pass and two-pass tableau methods have been developed. In the repository of the CTL-type branching-time setting, the well-known logics ECTL and ECTL^+ were developed to explicitly deal with fairness. However, due to the syntactical restrictions, these logics can only express restricted versions of fairness. The logic CTL^*, often considered as "the full branching-time logic" overcomes these restrictions on expressing fairness. However, this logic itself, is extremely challenging for the application of verification techniques, and the tableau technique, in particular. For example, there is no one-pass tableau construction for this logic, while it is known that one-pass tableau has an additional benefit enabling the formulation of dual sequent calculi that are often treated as more "natural" being more friendly for human understanding. Based on these two considerations, the following problem arises - are there logics that have richer expressiveness than ECTL^+ yet "simpler" than CTL^* for which a one-pass tableau can be developed? In this paper we give a solution to this problem. We present a tree-style one-pass tableau for a sub-logic of CTL^* that we call ECTL^#, which is more expressive than ECTL^+ allowing the formulation of a new range of fairness constraints with "until" operator. The presentation of the tableau construction is accompanied by an algorithm for constructing a systematic tableau, for any given input of admissible branching-time formulae. We prove the termination, soundness and completeness of the method. As tree-shaped one-pass tableaux are well suited for the automation and are amenable for the implementation and for the formulation of sequent calculi, our results also open a prospect of relevant developments of the automation and implementation of the tableau method for ECTL^#, and of a dual sequent calculi.
Cite as
Alexander Bolotov, Montserrat Hermo, and Paqui Lucio. Extending Fairness Expressibility of ECTL+: A Tree-Style One-Pass Tableau Approach. In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 5:1-5:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{bolotov_et_al:LIPIcs.TIME.2018.5,
author = {Bolotov, Alexander and Hermo, Montserrat and Lucio, Paqui},
title = {{Extending Fairness Expressibility of ECTL+: A Tree-Style One-Pass Tableau Approach}},
booktitle = {25th International Symposium on Temporal Representation and Reasoning (TIME 2018)},
pages = {5:1--5:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-089-7},
ISSN = {1868-8969},
year = {2018},
volume = {120},
editor = {Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018.5},
URN = {urn:nbn:de:0030-drops-97704},
doi = {10.4230/LIPIcs.TIME.2018.5},
annote = {Keywords: Temporal logic, fairness, tableau, branching-time, one-pass tableau}
}
Document
Results on Alternating-Time Temporal Logics with Linear Past
Abstract
We investigate the succinctness gap between two known equally-expressive and different linear-past extensions of standard CTL^* (resp., ATL^*). We establish by formal non-trivial arguments that the "memoryful" linear-past extension (the history leading to the current state is taken into account) can be exponentially more succinct than the standard "local" linear-past extension (the history leading to the current state is forgotten). As a second contribution, we consider the ATL-like fragment, denoted ATL_{lp}, of the known "memoryful" linear-past extension of ATL^{*}. We show that ATL_{lp} is strictly more expressive than ATL, and interestingly, it can be exponentially more succinct than the more expressive logic ATL^{*}. Moreover, we prove that both satisfiability and model-checking for the logic ATL_{lp} are Exptime-complete.
Cite as
Laura Bozzelli, Aniello Murano, and Loredana Sorrentino. Results on Alternating-Time Temporal Logics with Linear Past. In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 6:1-6:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{bozzelli_et_al:LIPIcs.TIME.2018.6,
author = {Bozzelli, Laura and Murano, Aniello and Sorrentino, Loredana},
title = {{Results on Alternating-Time Temporal Logics with Linear Past}},
booktitle = {25th International Symposium on Temporal Representation and Reasoning (TIME 2018)},
pages = {6:1--6:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-089-7},
ISSN = {1868-8969},
year = {2018},
volume = {120},
editor = {Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018.6},
URN = {urn:nbn:de:0030-drops-97714},
doi = {10.4230/LIPIcs.TIME.2018.6},
annote = {Keywords: Alternating-time temporal logics, Linear Past, Model Checking}
}
Document
Extracting Interval Temporal Logic Rules: A First Approach
Abstract
Discovering association rules is a classical data mining task with a wide range of applications that include the medical, the financial, and the planning domains, among others. Modern rule extraction algorithms focus on static rules, typically expressed in the language of Horn propositional logic, as opposed to temporal ones, which have received less attention in the literature. Since in many application domains temporal information is stored in form of intervals, extracting interval-based temporal rules seems the natural choice. In this paper we extend the well-known algorithm APRIORI for rule extraction to discover interval temporal rules written in the Horn fragment of Halpern and Shoham's interval temporal logic.
Cite as
Davide Bresolin, Enrico Cominato, Simone Gnani, Emilio Muñoz-Velasco, and Guido Sciavicco. Extracting Interval Temporal Logic Rules: A First Approach. In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 7:1-7:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{bresolin_et_al:LIPIcs.TIME.2018.7,
author = {Bresolin, Davide and Cominato, Enrico and Gnani, Simone and Mu\~{n}oz-Velasco, Emilio and Sciavicco, Guido},
title = {{Extracting Interval Temporal Logic Rules: A First Approach}},
booktitle = {25th International Symposium on Temporal Representation and Reasoning (TIME 2018)},
pages = {7:1--7:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-089-7},
ISSN = {1868-8969},
year = {2018},
volume = {120},
editor = {Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018.7},
URN = {urn:nbn:de:0030-drops-97728},
doi = {10.4230/LIPIcs.TIME.2018.7},
annote = {Keywords: Interval temporal logic, Horn fragment, Rule extraction}
}
Document
Faster Dynamic Controllability Checking for Simple Temporal Networks with Uncertainty
Abstract
Simple Temporal Networks (STNs) are a well-studied model for representing and reasoning about time. An STN comprises a set of real-valued variables called time-points, together with a set of binary constraints, each of the form Y <= X+w. The problem of finding a feasible schedule (i.e., an assignment of real numbers to time-points such that all of the constraints are satisfied) is equivalent to the Single Source Shortest Path problem (SSSP) in the STN graph.
Simple Temporal Networks with Uncertainty (STNUs) augment STNs to include contingent links that can be used, for example, to represent actions with uncertain durations. The duration of a contingent link is not controlled by the planner, but is instead controlled by a (possibly adversarial) environment. Each contingent link has the form, <A,l,u,C>, where 0 < l <= u < infty. Once the planner executes the activation time-point A, the environment must execute the contingent time-point C at some time A+Delta, where Delta in [l,u]. Crucially, the planner does not know the value of Delta in advance, but only discovers it when C executes. An STNU is dynamically controllable (DC) if there is a strategy that the planner can use to execute all of the non-contingent time-points, such that all of the constraints are guaranteed to be satisfied no matter which durations the environment chooses for the contingent links. The strategy can be dynamic in that it can react in real time to the contingent durations it observes. Recently, an upper bound of O(N^3) was given for the DC-checking problem for STNUs, where N is the number of time-points.
This paper introduces a new algorithm, called the RUL^- algorithm, for solving the DC-checking problem for STNUs that improves on the O(N^3) bound. The worst-case complexity of the RUL^- algorithm is O(MN+K^2N+KN log N), where N is the number of time-points, M is the number of constraints, and K is the number of contingent time-points. If M is O(N^2), then the complexity reduces to O(N^3); however, in sparse graphs the complexity can be much less. For example, if M is O(N log N), and K is O(sqrt{N}), then the complexity of the RUL^- algorithm reduces to O(N^2 log N).
The RUL^- algorithm begins by using the Bellman-Ford algorithm to compute a potential function. It then performs at most 2K rounds of computations, interleaving novel applications of Dijkstra's algorithm to (1) generate new edges and (2) update the potential function in response to those new edges. The constraint-propagation/edge-generation rules used by the RUL^- algorithm are distinguished from related work in two ways. First, they only generate unlabeled edges. Second, their applicability conditions are more restrictive. As a result, the RUL^- algorithm requires only O(K) rounds of Dijkstra's algorithm, instead of the O(N) rounds required by other approaches. The paper proves that the RUL^- algorithm is sound and complete for the DC-checking problem for STNUs.
Cite as
Massimo Cairo, Luke Hunsberger, and Romeo Rizzi. Faster Dynamic Controllability Checking for Simple Temporal Networks with Uncertainty. In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{cairo_et_al:LIPIcs.TIME.2018.8,
author = {Cairo, Massimo and Hunsberger, Luke and Rizzi, Romeo},
title = {{Faster Dynamic Controllability Checking for Simple Temporal Networks with Uncertainty}},
booktitle = {25th International Symposium on Temporal Representation and Reasoning (TIME 2018)},
pages = {8:1--8:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-089-7},
ISSN = {1868-8969},
year = {2018},
volume = {120},
editor = {Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018.8},
URN = {urn:nbn:de:0030-drops-97734},
doi = {10.4230/LIPIcs.TIME.2018.8},
annote = {Keywords: Simple Temporal Networks with Uncertainty, Dynamic Controllability, Temporal Planning under Uncertainty}
}
Document
Extending Conditional Simple Temporal Networks with Partially Shrinkable Uncertainty
Abstract
The proper handling of temporal constraints is crucial in many domains. As a particular challenge, temporal constraints must be also handled when different specific situations happen (conditional constraints) and when some event occurrences can be only observed at run time (contingent constraints). In this paper we introduce Conditional Simple Temporal Networks with Partially Shrinkable Uncertainty (CSTNPSUs), in which contingent constraints are made more flexible (guarded constraints) and they are also specified as conditional constraints. It turns out that guarded constraints require the ability to reason on both kinds of constraints in a seamless way. In particular, we discuss CSTNPSU features through a motivating example and, then, we introduce the concept of controllability for such networks and the related sound checking algorithm.
Cite as
Carlo Combi and Roberto Posenato. Extending Conditional Simple Temporal Networks with Partially Shrinkable Uncertainty. In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{combi_et_al:LIPIcs.TIME.2018.9,
author = {Combi, Carlo and Posenato, Roberto},
title = {{Extending Conditional Simple Temporal Networks with Partially Shrinkable Uncertainty}},
booktitle = {25th International Symposium on Temporal Representation and Reasoning (TIME 2018)},
pages = {9:1--9:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-089-7},
ISSN = {1868-8969},
year = {2018},
volume = {120},
editor = {Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018.9},
URN = {urn:nbn:de:0030-drops-97740},
doi = {10.4230/LIPIcs.TIME.2018.9},
annote = {Keywords: Conditional Simple Temporal Networks with Uncertainty, Partial Shrinkable Temporal Constraint, Dynamic Controllability, Temporal Constraints}
}
Document
On Restricted Disjunctive Temporal Problems: Faster Algorithms and Tractability Frontier
Abstract
In 2005 T.K.S. Kumar studied the Restricted Disjunctive Temporal Problem (RDTP), a restricted but very expressive class of Disjunctive Temporal Problems (DTPs). An RDTP comes with a finite set of temporal variables, and a finite set of temporal constraints each of which can be either one of the following three types: (t_1) two-variable linear-difference simple constraint; (t_2) single-variable disjunction of many interval constraints; (t_3) two-variable disjunction of two interval constraints only. Kumar showed that RDTPs are solvable in deterministic strongly polynomial time by reducing them to the Connected Row-Convex (CRC) constraints satisfaction problem, also devising a faster randomized algorithm. Instead, the most general form of DTPs allows for multi-variable disjunctions of many interval constraints and it is NP-complete.
This work offers a deeper comprehension on the tractability of RDTPs, leading to an elementary deterministic strongly polynomial time algorithm for them, significantly improving the asymptotic running times of all the previous deterministic and randomized solutions. The result is obtained by reducing RDTPs to the Single-Source Shortest Paths (SSSP) and the 2-SAT problem (jointly), instead of reducing to CRCs. In passing, we obtain a faster (quadratic time) algorithm for RDTPs having only {t_1, t_2}-constraints and no t_3-constraint. As a second main contribution, we study the tractability frontier of solving RDTPs blended with Hyper Temporal Networks (HyTNs), a disjunctive strict generalization of Simple Temporal Networks (STNs) based on hypergraphs: we prove that solving temporal problems having only t_2-constraints and either only multi-tail or only multi-head hyperarc-constraints lies in NP cap co-NP and admits deterministic pseudo-polynomial time algorithms; on the other hand, problems having only t_3-constraints and either only multi-tail or only multi-head hyperarc-constraints turns out strongly NP-complete.
Cite as
Carlo Comin and Romeo Rizzi. On Restricted Disjunctive Temporal Problems: Faster Algorithms and Tractability Frontier. In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 10:1-10:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{comin_et_al:LIPIcs.TIME.2018.10,
author = {Comin, Carlo and Rizzi, Romeo},
title = {{On Restricted Disjunctive Temporal Problems: Faster Algorithms and Tractability Frontier}},
booktitle = {25th International Symposium on Temporal Representation and Reasoning (TIME 2018)},
pages = {10:1--10:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-089-7},
ISSN = {1868-8969},
year = {2018},
volume = {120},
editor = {Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018.10},
URN = {urn:nbn:de:0030-drops-97751},
doi = {10.4230/LIPIcs.TIME.2018.10},
annote = {Keywords: Restricted Disjuctive Temporal Problems, Simple Temporal Networks, Hyper Temporal Networks, Consistency Checking, Single-Source Shortest-Paths, 2-SAT}
}
Document
Algebraic Operators for Processing Sets of Temporal Intervals in Relational Databases
Abstract
The efficient management of temporal data has become increasingly important for many database applications. Most commercial systems already allow the management of temporal data but the operational support for processing this data is still rather limited. One particular reason is that many extension proposals typically require considerable modifications of the underlying database engine. In this paper, we propose a lightweight solution where temporal operators are realized using a library of user-defined functions. This way the complexity of temporal queries can be drastically reduced leading to more readable and less error-prone code without touching the database system. Our experiments show that the proposed operators significantly outperform temporal queries formulated in pure SQL. In addition, we investigate the possibility to incorporate algebraic optimization strategies directly into our operator definitions which allow for further performance improvements.
Cite as
Andreas Dohr, Christiane Engels, and Andreas Behrend. Algebraic Operators for Processing Sets of Temporal Intervals in Relational Databases. In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 11:1-11:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{dohr_et_al:LIPIcs.TIME.2018.11,
author = {Dohr, Andreas and Engels, Christiane and Behrend, Andreas},
title = {{Algebraic Operators for Processing Sets of Temporal Intervals in Relational Databases}},
booktitle = {25th International Symposium on Temporal Representation and Reasoning (TIME 2018)},
pages = {11:1--11:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-089-7},
ISSN = {1868-8969},
year = {2018},
volume = {120},
editor = {Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018.11},
URN = {urn:nbn:de:0030-drops-97769},
doi = {10.4230/LIPIcs.TIME.2018.11},
annote = {Keywords: Temporal Databases, Relational Operators, Situation Calculus}
}
Document
Deciding the Consistency of Branching Time Interval Networks
Abstract
Allen's Interval Algebra (IA) is one of the most prominent formalisms in the area of qualitative temporal reasoning; however, its applications are naturally restricted to linear flows of time. When dealing with nonlinear time, Allen's algebra can be extended in several ways, and, as suggested by Ragni and Wölfl [M. Ragni and S. Wölfl, 2004], a possible solution consists in defining the Branching Algebra (BA) as a set of 19 basic relations (13 basic linear relations plus 6 new basic nonlinear ones) in such a way that each basic relation between two intervals is completely defined by the relative position of the endpoints on a tree-like partial order. While the problem of deciding the consistency of a network of IA-constraints is well-studied, and every subset of the IA has been classified with respect to the tractability of its consistency problem, the fragments of the BA have received less attention. In this paper, we first define the notion of convex BA-relation, and, then, we prove that the consistency of a network of convex BA-relations can be decided via path consistency, and is therefore a polynomial problem. This is the first non-trivial tractable fragment of the BA; given the clear parallel with the linear case, our contribution poses the bases for a deeper study of fragments of BA towards their complete classification.
Cite as
Marco Gavanelli, Alessandro Passantino, and Guido Sciavicco. Deciding the Consistency of Branching Time Interval Networks. In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 12:1-12:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{gavanelli_et_al:LIPIcs.TIME.2018.12,
author = {Gavanelli, Marco and Passantino, Alessandro and Sciavicco, Guido},
title = {{Deciding the Consistency of Branching Time Interval Networks}},
booktitle = {25th International Symposium on Temporal Representation and Reasoning (TIME 2018)},
pages = {12:1--12:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-089-7},
ISSN = {1868-8969},
year = {2018},
volume = {120},
editor = {Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018.12},
URN = {urn:nbn:de:0030-drops-97779},
doi = {10.4230/LIPIcs.TIME.2018.12},
annote = {Keywords: Constraint programming, Consistency, Branching time}
}
Document
A Game-Theoretic Approach to Timeline-Based Planning with Uncertainty
Abstract
In timeline-based planning, domains are described as sets of independent, but interacting, components, whose behaviour over time (the set of timelines) is governed by a set of temporal constraints. A distinguishing feature of timeline-based planning systems is the ability to integrate planning with execution by synthesising control strategies for flexible plans. However, flexible plans can only represent temporal uncertainty, while more complex forms of nondeterminism are needed to deal with a wider range of realistic problems. In this paper, we propose a novel game-theoretic approach to timeline-based planning problems, generalising the state of the art while uniformly handling temporal uncertainty and nondeterminism. We define a general concept of timeline-based game and we show that the notion of winning strategy for these games is strictly more general than that of control strategy for dynamically controllable flexible plans. Moreover, we show that the problem of establishing the existence of such winning strategies is decidable using a doubly exponential amount of space.
Cite as
Nicola Gigante, Angelo Montanari, Marta Cialdea Mayer, Andrea Orlandini, and Mark Reynolds. A Game-Theoretic Approach to Timeline-Based Planning with Uncertainty. In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{gigante_et_al:LIPIcs.TIME.2018.13,
author = {Gigante, Nicola and Montanari, Angelo and Cialdea Mayer, Marta and Orlandini, Andrea and Reynolds, Mark},
title = {{A Game-Theoretic Approach to Timeline-Based Planning with Uncertainty}},
booktitle = {25th International Symposium on Temporal Representation and Reasoning (TIME 2018)},
pages = {13:1--13:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-089-7},
ISSN = {1868-8969},
year = {2018},
volume = {120},
editor = {Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018.13},
URN = {urn:nbn:de:0030-drops-97786},
doi = {10.4230/LIPIcs.TIME.2018.13},
annote = {Keywords: Timeline-based planning with uncertainty, strategic games, decidability}
}
Document
Sound-and-Complete Algorithms for Checking the Dynamic Controllability of Conditional Simple Temporal Networks with Uncertainty
Abstract
A Conditional Simple Temporal Network with Uncertainty (CSTNU) is a data structure for representing and reasoning about time. CSTNUs incorporate observation time-points from Conditional Simple Temporal Networks (CSTNs) and contingent links from Simple Temporal Networks with Uncertainty (STNUs). A CSTNU is dynamically controllable (DC) if there exists a strategy for executing its time-points that guarantees the satisfaction of all relevant constraints no matter how the uncertainty associated with its observation time-points and contingent links is resolved in real time. This paper presents the first sound-and-complete DC-checking algorithms for CSTNUs that are based on the propagation of labeled constraints and demonstrates their practicality.
Cite as
Luke Hunsberger and Roberto Posenato. Sound-and-Complete Algorithms for Checking the Dynamic Controllability of Conditional Simple Temporal Networks with Uncertainty. In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{hunsberger_et_al:LIPIcs.TIME.2018.14,
author = {Hunsberger, Luke and Posenato, Roberto},
title = {{Sound-and-Complete Algorithms for Checking the Dynamic Controllability of Conditional Simple Temporal Networks with Uncertainty}},
booktitle = {25th International Symposium on Temporal Representation and Reasoning (TIME 2018)},
pages = {14:1--14:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-089-7},
ISSN = {1868-8969},
year = {2018},
volume = {120},
editor = {Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018.14},
URN = {urn:nbn:de:0030-drops-97795},
doi = {10.4230/LIPIcs.TIME.2018.14},
annote = {Keywords: Temporal Networks, Conditional Simple Temporal Problem with Uncertainty, Dynamic Controllability, Checking Algorithm}
}
Document
Reducing epsilon-DC Checking for Conditional Simple Temporal Networks to DC Checking
Abstract
Recent work on Conditional Simple Temporal Networks (CSTNs) has introduced the problem of checking the dynamic consistency (DC) property for the case where the reaction time of an execution strategy to observations is bounded below by some fixed epsilon > 0, the so-called epsilon-DC-checking problem. This paper proves that the epsilon-DC-checking problem for CSTNs can be reduced to the standard DC-checking problem for CSTNs - without incurring any computational cost. Given any CSTN S with k observation time-points, the paper defines a new CSTN S_0 that is the same as S, except that for each observation time-point P? in S: (i) P? is demoted to a non-observation time-point in S_0; and (ii) a new observation time-point P_0?, constrained to occur exactly epsilon units after P?, is inserted into S_0. The paper proves that S is epsilon-DC if and only if S_0 is (standard) DC, and that the application of the epsilon-DC-checking constraint-propagation rules to S is equivalent to the application of the corresponding (standard) DC-checking constraint-propagation rules to S_0. Two versions of these results are presented that differ only in whether a dynamic strategy for S_0 can react instantaneously to observations, or only after some arbitrarily small, positive delay. Finally, the paper demonstrates empirically that building S_0 and DC-checking it incurs no computational cost as the sizes of the instances increase.
Cite as
Luke Hunsberger and Roberto Posenato. Reducing epsilon-DC Checking for Conditional Simple Temporal Networks to DC Checking. In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 15:1-15:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{hunsberger_et_al:LIPIcs.TIME.2018.15,
author = {Hunsberger, Luke and Posenato, Roberto},
title = {{Reducing epsilon-DC Checking for Conditional Simple Temporal Networks to DC Checking}},
booktitle = {25th International Symposium on Temporal Representation and Reasoning (TIME 2018)},
pages = {15:1--15:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-089-7},
ISSN = {1868-8969},
year = {2018},
volume = {120},
editor = {Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018.15},
URN = {urn:nbn:de:0030-drops-97808},
doi = {10.4230/LIPIcs.TIME.2018.15},
annote = {Keywords: Conditional Simple Temporal Networks, Dynamic Consistency, Temporal Constraints}
}
Document
On the Expressive Power of Hybrid Branching-Time Logics
Abstract
Hybrid branching-time logics are a powerful extension of branching-time logics like CTL, CTL^* or even the modal mu-calculus through the addition of binders, jumps and variable tests. Their expressiveness is not restricted by bisimulation-invariance anymore. Hence, they do not retain the tree model property, and the finite model property is equally lost. Their satisfiability problems are typically undecidable, their model checking problems (on finite models) are decidable with complexities ranging from polynomial to non-elementary time. In this paper we study the expressive power of such hybrid branching-time logics beyond some earlier results about their invariance under hybrid bisimulations. In particular, we aim to extend the hierarchy of non-hybrid branching-time logics CTL, CTL^+, CTL^* and the modal mu-calculus to their hybrid extensions. We show that most separation results can be transferred to the hybrid world, even though the required techniques become a bit more involved. We also present some collapse results for restricted classes of models that are especially worth investigating, namely linear, tree-shaped and finite models.
Cite as
Daniel Kernberger and Martin Lange. On the Expressive Power of Hybrid Branching-Time Logics. In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{kernberger_et_al:LIPIcs.TIME.2018.16,
author = {Kernberger, Daniel and Lange, Martin},
title = {{On the Expressive Power of Hybrid Branching-Time Logics}},
booktitle = {25th International Symposium on Temporal Representation and Reasoning (TIME 2018)},
pages = {16:1--16:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-089-7},
ISSN = {1868-8969},
year = {2018},
volume = {120},
editor = {Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018.16},
URN = {urn:nbn:de:0030-drops-97816},
doi = {10.4230/LIPIcs.TIME.2018.16},
annote = {Keywords: branching-time, mu-calculus, hybrid logics, expressiveness}
}
Document
A Temporal Logic for Modelling Activities of Daily Living
Abstract
Behaviour support technology is aimed at assisting people in organizing their Activities of Daily Living (ADLs). Numerous frameworks have been developed for activity recognition and for generating specific types of support actions, such as reminders. The main goal of our research is to develop a generic formal framework for representing and reasoning about ADLs and their temporal relations. This framework should facilitate modelling and reasoning about 1) durative activities, 2) relations between higher-level activities and subactivities, 3) activity instances, and 4) activity duration. In this paper we present a temporal logic as an extension of the logic TPTL for specification of real-time systems. Our logic TPTL_{bih} is defined over Behaviour Identification Hierarchies (BIHs) for representing ADL structure and typical activity duration. To model execution of ADLs, states of the temporal traces in TPTL_{bih} comprise information about the start, stop and current execution of activities. We provide a number of constraints on these traces that we stipulate are desired for the accurate representation of ADL execution, and investigate corresponding validities in the logic. To evaluate the expressivity of the logic, we give a formal definition for the notion of Coherence for (complex) activities, by which we mean that an activity is done without interruption and in a timely fashion. We show that the definition is satisfiable in our framework. In this way the logic forms the basis for a generic monitoring and reasoning framework for ADLs.
Cite as
Malte S. Kließ, Catholijn M. Jonker, and M. Birna van Riemsdijk. A Temporal Logic for Modelling Activities of Daily Living. In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 17:1-17:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{klie_et_al:LIPIcs.TIME.2018.17,
author = {Klie{\ss}, Malte S. and Jonker, Catholijn M. and van Riemsdijk, M. Birna},
title = {{A Temporal Logic for Modelling Activities of Daily Living}},
booktitle = {25th International Symposium on Temporal Representation and Reasoning (TIME 2018)},
pages = {17:1--17:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-089-7},
ISSN = {1868-8969},
year = {2018},
volume = {120},
editor = {Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018.17},
URN = {urn:nbn:de:0030-drops-97822},
doi = {10.4230/LIPIcs.TIME.2018.17},
annote = {Keywords: Temporal Logic, Reasoning, Durative Activities}
}
Document
GSM+T: A Timed Artifact-Centric Process Model
Abstract
We introduce an extension to the declarative and artifact-centric Guard Stage Milestone (GSM) process modeling language to represent temporal aspects (duration, deadlines, lower- and upper-bound constraints), define the correctness of executions of GSM processes with respect to temporal constraints, check controllability of processes, compute execution plans respecting temporal constraints, and provide a translation method allowing to execute controllable GSM+T processes on standard GSM Engines.
Cite as
Julius Köpke, Johann Eder, and Jianwen Su. GSM+T: A Timed Artifact-Centric Process Model. In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 18:1-18:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{kopke_et_al:LIPIcs.TIME.2018.18,
author = {K\"{o}pke, Julius and Eder, Johann and Su, Jianwen},
title = {{GSM+T: A Timed Artifact-Centric Process Model}},
booktitle = {25th International Symposium on Temporal Representation and Reasoning (TIME 2018)},
pages = {18:1--18:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-089-7},
ISSN = {1868-8969},
year = {2018},
volume = {120},
editor = {Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018.18},
URN = {urn:nbn:de:0030-drops-97835},
doi = {10.4230/LIPIcs.TIME.2018.18},
annote = {Keywords: Guard Stage Milestone, GSM, Time Constraints, Controllability, Case Handling, Business Process Modeling}
}
Document
Learning Qualitative Constraint Networks
Abstract
Temporal and spatial reasoning is a fundamental task in artificial intelligence and its related areas including scheduling, planning and Geographic Information Systems (GIS). In these applications, we often deal with incomplete and qualitative information. In this regard, the symbolic representation of time and space using Qualitative Constraint Networks (QCNs) is therefore substantial.
We propose a new algorithm for learning a QCN from a non expert. The learning process includes different cases where querying the user is an essential task. Here, membership queries are asked in order to elicit temporal or spatial relationships between pairs of temporal or spatial entities. During this acquisition process, constraint propagation through Path Consistency (PC) is performed in order to reduce the number of membership queries needed to reach the target QCN. We use the learning theory machinery to prove some limits on learning path consistent QCNs from queries. The time performances of our algorithm have been experimentally evaluated using different scenarios.
Cite as
Malek Mouhoub, Hamad Al Marri, and Eisa Alanazi. Learning Qualitative Constraint Networks. In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 19:1-19:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{mouhoub_et_al:LIPIcs.TIME.2018.19,
author = {Mouhoub, Malek and Al Marri, Hamad and Alanazi, Eisa},
title = {{Learning Qualitative Constraint Networks}},
booktitle = {25th International Symposium on Temporal Representation and Reasoning (TIME 2018)},
pages = {19:1--19:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-089-7},
ISSN = {1868-8969},
year = {2018},
volume = {120},
editor = {Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018.19},
URN = {urn:nbn:de:0030-drops-97849},
doi = {10.4230/LIPIcs.TIME.2018.19},
annote = {Keywords: Temporal Reasoning, Qualitative Constraint Network (QCN), Constraint Learning, Path Consistency, Constraint Propagation}
}
Document
A Stream Reasoning System for Maritime Monitoring
Abstract
We present a stream reasoning system for monitoring vessel activity in large geographical areas. The system ingests a compressed vessel position stream, and performs online spatio-temporal link discovery to calculate proximity relations between vessels, and topological relations between vessel and static areas. Capitalizing on the discovered relations, a complex activity recognition engine, based on the Event Calculus, performs continuous pattern matching to detect various types of dangerous, suspicious and potentially illegal vessel activity. We evaluate the performance of the system by means of real datasets including kinematic messages from vessels, and demonstrate the effects of the highly efficient spatio-temporal link discovery on performance.
Cite as
Georgios M. Santipantakis, Akrivi Vlachou, Christos Doulkeridis, Alexander Artikis, Ioannis Kontopoulos, and George A. Vouros. A Stream Reasoning System for Maritime Monitoring. In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 20:1-20:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{santipantakis_et_al:LIPIcs.TIME.2018.20,
author = {Santipantakis, Georgios M. and Vlachou, Akrivi and Doulkeridis, Christos and Artikis, Alexander and Kontopoulos, Ioannis and Vouros, George A.},
title = {{A Stream Reasoning System for Maritime Monitoring}},
booktitle = {25th International Symposium on Temporal Representation and Reasoning (TIME 2018)},
pages = {20:1--20:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-089-7},
ISSN = {1868-8969},
year = {2018},
volume = {120},
editor = {Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018.20},
URN = {urn:nbn:de:0030-drops-97858},
doi = {10.4230/LIPIcs.TIME.2018.20},
annote = {Keywords: event pattern matching, Event Calculus}
}
Document
An Empirical Study on Bidirectional Recurrent Neural Networks for Human Motion Recognition
Abstract
The deep recurrent neural networks (RNNs) and their associated gated neurons, such as Long Short-Term Memory (LSTM) have demonstrated a continued and growing success rates with researches in various sequential data processing applications, especially when applied to speech recognition and language modeling. Despite this, amongst current researches, there are limited studies on the deep RNNs architectures and their effects being applied to other application domains. In this paper, we evaluated the different strategies available to construct bidirectional recurrent neural networks (BRNNs) applying Gated Recurrent Units (GRUs), as well as investigating a reservoir computing RNNs, i.e., Echo state networks (ESN) and a few other conventional machine learning techniques for skeleton-based human motion recognition. The evaluation of tasks focuses on the generalization of different approaches by employing arbitrary untrained viewpoints, combined together with previously unseen subjects. Moreover, we extended the test by lowering the subsampling frame rates to examine the robustness of the algorithms being employed against the varying of movement speed.
Cite as
Pattreeya Tanisaro and Gunther Heidemann. An Empirical Study on Bidirectional Recurrent Neural Networks for Human Motion Recognition. In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 21:1-21:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{tanisaro_et_al:LIPIcs.TIME.2018.21,
author = {Tanisaro, Pattreeya and Heidemann, Gunther},
title = {{An Empirical Study on Bidirectional Recurrent Neural Networks for Human Motion Recognition}},
booktitle = {25th International Symposium on Temporal Representation and Reasoning (TIME 2018)},
pages = {21:1--21:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-089-7},
ISSN = {1868-8969},
year = {2018},
volume = {120},
editor = {Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018.21},
URN = {urn:nbn:de:0030-drops-97865},
doi = {10.4230/LIPIcs.TIME.2018.21},
annote = {Keywords: Recurrent Neural Networks, Human Motion Classification, Echo State Networks, Motion Capture, Bidirectional Recurrent Neural Networks}
}
Document
Population Based Methods for Optimising Infinite Behaviours of Timed Automata
Abstract
Timed automata are powerful models for the analysis of real time systems. The optimal infinite scheduling problem for double-priced timed automata is concerned with finding infinite runs of a system whose long term cost to reward ratio is minimal. Due to the state-space explosion occurring when discretising a timed automaton, exact computation of the optimal infinite ratio is infeasible. This paper describes the implementation and evaluation of ant colony optimisation for approximating the optimal schedule for a given double-priced timed automaton. The application of ant colony optimisation to the corner-point abstraction of the automaton proved generally less effective than a random method. The best found optimisation method was obtained by formulating the choice of time delays in a cycle of the automaton as a linear program and utilizing ant colony optimisation in order to determine a sequence of profitable discrete transitions comprising an infinite behaviour.
Cite as
Lewis Tolonen, Tim French, and Mark Reynolds. Population Based Methods for Optimising Infinite Behaviours of Timed Automata. In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 22:1-22:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{tolonen_et_al:LIPIcs.TIME.2018.22,
author = {Tolonen, Lewis and French, Tim and Reynolds, Mark},
title = {{Population Based Methods for Optimising Infinite Behaviours of Timed Automata}},
booktitle = {25th International Symposium on Temporal Representation and Reasoning (TIME 2018)},
pages = {22:1--22:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-089-7},
ISSN = {1868-8969},
year = {2018},
volume = {120},
editor = {Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018.22},
URN = {urn:nbn:de:0030-drops-97875},
doi = {10.4230/LIPIcs.TIME.2018.22},
annote = {Keywords: Timed Automata, Heuristic Search, Ant Colony Optimisation}
}
Document
Computational Complexity of a Core Fragment of Halpern-Shoham Logic
Abstract
Halpern-Shoham logic (HS) is a highly expressive interval temporal logic but the satisfiability problem of its formulas is undecidable. The main goal in the research area is to introduce fragments of the logic which are of low computational complexity and of expressive power high enough for practical applications. Recently introduced syntactical restrictions imposed on formulas and semantical constraints put on models gave rise to tractable HS fragments for which prototypical real-world applications have already been proposed. One of such fragments is obtained by forbidding diamond modal operators and limiting formulas to the core form, i.e., the Horn form with at most one literal in the antecedent. The fragment was known to be NL-hard and in P but no tight results were known. In the paper we prove its P-completeness in the case where punctual intervals are allowed and the timeline is dense.
Importantly, the fragment is not referential, i.e., it does not allow us to express nominals (which label intervals) and satisfaction operators (which enables us to refer to intervals by their labels). We show that by adding nominals and satisfaction operators to the fragment we reach NP-completeness whenever the timeline is dense or the interpretation of modal operators is weakened (excluding the case when punctual intervals are disallowed and the timeline is discrete). Moreover, we prove that in the case of language containing nominals but not satisfaction operators, the fragment is still NP-complete over dense timelines.
Cite as
Przemyslaw Andrzej Walega. Computational Complexity of a Core Fragment of Halpern-Shoham Logic. In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@InProceedings{walega:LIPIcs.TIME.2018.23,
author = {Walega, Przemyslaw Andrzej},
title = {{Computational Complexity of a Core Fragment of Halpern-Shoham Logic}},
booktitle = {25th International Symposium on Temporal Representation and Reasoning (TIME 2018)},
pages = {23:1--23:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-089-7},
ISSN = {1868-8969},
year = {2018},
volume = {120},
editor = {Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018.23},
URN = {urn:nbn:de:0030-drops-97880},
doi = {10.4230/LIPIcs.TIME.2018.23},
annote = {Keywords: Temporal Logic, Interval Logic, Computational Complexity, Hybrid Logic}
}