28 Search Results for "Penczek, Wojciech"

Volume

LIPIcs, Volume 120

25th International Symposium on Temporal Representation and Reasoning (TIME 2018)

TIME 2018, October 15-17, 2018, Warsaw, Poland

Editors: Natasha Alechina, Kjetil Nørvåg, and Wojciech Penczek

Document
Complete Volume
DOI: 10.4230/LIPIcs.TIME.2018
LIPIcs, Volume 120, TIME'18, Complete Volume

Authors: Natasha Alechina, Kjetil Nørvåg, and Wojciech Penczek

Published in: LIPIcs, Volume 120, 25th International Symposium on Temporal Representation and Reasoning (TIME 2018)

Abstract
LIPIcs, Volume 120, TIME'18, Complete Volume
Cite as

Natasha Alechina, Kjetil Nørvåg, and Wojciech Penczek. LIPIcs, Volume 120, TIME'18, Complete Volume. In 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
DOI: 10.4230/LIPIcs.TIME.2018.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Natasha Alechina, Kjetil Nørvåg, and Wojciech Penczek

Published in: LIPIcs, Volume 120, 25th International Symposium on Temporal Representation and Reasoning (TIME 2018)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

Natasha Alechina, Kjetil Nørvåg, and Wojciech Penczek. Front Matter, Table of Contents, Preface, Conference Organization. In 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
DOI: 10.4230/LIPIcs.TIME.2018.1
On Temporal and Separation Logics (Invited Paper)

Authors: Stéphane Demri

Published in: LIPIcs, Volume 120, 25th International Symposium on Temporal Representation and Reasoning (TIME 2018)

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
DOI: 10.4230/LIPIcs.TIME.2018.2
Database Technology for Processing Temporal Data (Invited Paper)

Authors: Michael H. Böhlen, Anton Dignös, Johann Gamper, and Christian S. Jensen

Published in: LIPIcs, Volume 120, 25th International Symposium on Temporal Representation and Reasoning (TIME 2018)

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
DOI: 10.4230/LIPIcs.TIME.2018.3
Model Checking Strategic Ability - Why, What, and Especially: How? (Invited Paper)

Authors: Wojciech Jamroga

Published in: LIPIcs, Volume 120, 25th International Symposium on Temporal Representation and Reasoning (TIME 2018)

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
DOI: 10.4230/LIPIcs.TIME.2018.4
Predicting the Evolution of Communities with Online Inductive Logic Programming

Authors: George Athanasopoulos, George Paliouras, Dimitrios Vogiatzis, Grigorios Tzortzis, and Nikos Katzouris

Published in: LIPIcs, Volume 120, 25th International Symposium on Temporal Representation and Reasoning (TIME 2018)

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
DOI: 10.4230/LIPIcs.TIME.2018.5
Extending Fairness Expressibility of ECTL+: A Tree-Style One-Pass Tableau Approach

Authors: Alexander Bolotov, Montserrat Hermo, and Paqui Lucio

Published in: LIPIcs, Volume 120, 25th International Symposium on Temporal Representation and Reasoning (TIME 2018)

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
DOI: 10.4230/LIPIcs.TIME.2018.6
Results on Alternating-Time Temporal Logics with Linear Past

Authors: Laura Bozzelli, Aniello Murano, and Loredana Sorrentino

Published in: LIPIcs, Volume 120, 25th International Symposium on Temporal Representation and Reasoning (TIME 2018)

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
DOI: 10.4230/LIPIcs.TIME.2018.7
Extracting Interval Temporal Logic Rules: A First Approach

Authors: Davide Bresolin, Enrico Cominato, Simone Gnani, Emilio Muñoz-Velasco, and Guido Sciavicco

Published in: LIPIcs, Volume 120, 25th International Symposium on Temporal Representation and Reasoning (TIME 2018)

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
DOI: 10.4230/LIPIcs.TIME.2018.8
Faster Dynamic Controllability Checking for Simple Temporal Networks with Uncertainty

Authors: Massimo Cairo, Luke Hunsberger, and Romeo Rizzi

Published in: LIPIcs, Volume 120, 25th International Symposium on Temporal Representation and Reasoning (TIME 2018)

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
DOI: 10.4230/LIPIcs.TIME.2018.9
Extending Conditional Simple Temporal Networks with Partially Shrinkable Uncertainty

Authors: Carlo Combi and Roberto Posenato

Published in: LIPIcs, Volume 120, 25th International Symposium on Temporal Representation and Reasoning (TIME 2018)

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
DOI: 10.4230/LIPIcs.TIME.2018.10
On Restricted Disjunctive Temporal Problems: Faster Algorithms and Tractability Frontier

Authors: Carlo Comin and Romeo Rizzi

Published in: LIPIcs, Volume 120, 25th International Symposium on Temporal Representation and Reasoning (TIME 2018)

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
DOI: 10.4230/LIPIcs.TIME.2018.11
Algebraic Operators for Processing Sets of Temporal Intervals in Relational Databases

Authors: Andreas Dohr, Christiane Engels, and Andreas Behrend

Published in: LIPIcs, Volume 120, 25th International Symposium on Temporal Representation and Reasoning (TIME 2018)

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
DOI: 10.4230/LIPIcs.TIME.2018.12
Deciding the Consistency of Branching Time Interval Networks

Authors: Marco Gavanelli, Alessandro Passantino, and Guido Sciavicco

Published in: LIPIcs, Volume 120, 25th International Symposium on Temporal Representation and Reasoning (TIME 2018)

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}
}
  • Refine by Author
  • 4 Penczek, Wojciech
  • 3 Hunsberger, Luke
  • 3 Posenato, Roberto
  • 2 Alechina, Natasha
  • 2 Nørvåg, Kjetil
  • Show More...

  • Refine by Classification
  • 5 Computing methodologies → Temporal reasoning
  • 5 Theory of computation → Modal and temporal logics
  • 3 Mathematics of computing → Graph algorithms
  • 2 Computing methodologies → Planning under uncertainty
  • 2 Theory of computation → Dynamic graph algorithms
  • Show More...

  • Refine by Keyword
  • 3 Dynamic Controllability
  • 2 Event Calculus
  • 2 Temporal Constraints
  • 2 Temporal Logic
  • 2 branching-time
  • Show More...

  • Refine by Type
  • 27 document
  • 1 volume

  • Refine by Publication Year
  • 26 2018
  • 1 2000
  • 1 2012

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact