eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-10-08
120
0
0
10.4230/LIPIcs.TIME.2018
article
LIPIcs, Volume 120, TIME'18, Complete Volume
Alechina, Natasha
Nørvåg, Kjetil
Penczek, Wojciech
LIPIcs, Volume 120, TIME'18, Complete Volume
https://drops.dagstuhl.de/storage/00lipics/lipics-vol120-time2018/LIPIcs.TIME.2018/LIPIcs.TIME.2018.pdf
Theory of computation, Logic, Information systems, Temporal data, Computing methodologies, Knowledge representation and reasoning
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-10-08
120
0:i
0:xiv
10.4230/LIPIcs.TIME.2018.0
article
Front Matter, Table of Contents, Preface, Conference Organization
Alechina, Natasha
Nørvåg, Kjetil
Penczek, Wojciech
Front Matter, Table of Contents, Preface, Conference Organization
https://drops.dagstuhl.de/storage/00lipics/lipics-vol120-time2018/LIPIcs.TIME.2018.0/LIPIcs.TIME.2018.0.pdf
Front Matter
Table of Contents
Preface
Conference Organization
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-10-08
120
1:1
1:4
10.4230/LIPIcs.TIME.2018.1
article
On Temporal and Separation Logics (Invited Paper)
Demri, Stéphane
1
https://orcid.org/0000-0002-3493-2610
LSV, CNRS, ENS Paris-Saclay, Université Paris-Saclay, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol120-time2018/LIPIcs.TIME.2018.1/LIPIcs.TIME.2018.1.pdf
separation logics
temporal logics
expressive power
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-10-08
120
2:1
2:7
10.4230/LIPIcs.TIME.2018.2
article
Database Technology for Processing Temporal Data (Invited Paper)
Böhlen, Michael H.
1
https://orcid.org/0000-0003-3694-9026
Dignös, Anton
2
https://orcid.org/0000-0002-7621-967X
Gamper, Johann
2
https://orcid.org/0000-0002-7128-507X
Jensen, Christian S.
3
https://orcid.org/0000-0002-9697-7670
University of Zurich, Switzerland
Free University of Bozen-Bolzano, Italy
Aalborg University, Denmark
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol120-time2018/LIPIcs.TIME.2018.2/LIPIcs.TIME.2018.2.pdf
Temporal databases
temporal query processing
sequenced semantics
SQL
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-10-08
120
3:1
3:10
10.4230/LIPIcs.TIME.2018.3
article
Model Checking Strategic Ability - Why, What, and Especially: How? (Invited Paper)
Jamroga, Wojciech
1
Institute of Computer Science, Polish Academy of Sciences, Warsaw, Poland
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol120-time2018/LIPIcs.TIME.2018.3/LIPIcs.TIME.2018.3.pdf
model checking
strategic ability
alternating-time temporal logic
imperfect information games
approximate verification
model reductions
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-10-08
120
4:1
4:20
10.4230/LIPIcs.TIME.2018.4
article
Predicting the Evolution of Communities with Online Inductive Logic Programming
Athanasopoulos, George
1
Paliouras, George
2
Vogiatzis, Dimitrios
3
4
Tzortzis, Grigorios
2
Katzouris, Nikos
2
Department of Informatics and Telecommunications, National and Kapodistrian University of Athens, Athens, Greece
Institute of Informatics and Telecommunications, NCSR "Demokritos", Athens, Greece
The American College of Greece, Deree, Athens, Greece
and, Institute of Informatics and Telecommunications, NCSR "Demokritos", Athens, Greece
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol120-time2018/LIPIcs.TIME.2018.4/LIPIcs.TIME.2018.4.pdf
Social Network Analysis
Community Evolution Prediction
Machine Learning
Inductive Logic Programming
Event Calculus
Online Learning
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-10-08
120
5:1
5:22
10.4230/LIPIcs.TIME.2018.5
article
Extending Fairness Expressibility of ECTL+: A Tree-Style One-Pass Tableau Approach
Bolotov, Alexander
1
Hermo, Montserrat
2
Lucio, Paqui
2
University of Westminster, W1W 6UW, London, UK
University of the Basque Country, P. Manuel de Lardizabal, 1, 20018-San Sebastián, Spain
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol120-time2018/LIPIcs.TIME.2018.5/LIPIcs.TIME.2018.5.pdf
Temporal logic
fairness
tableau
branching-time
one-pass tableau
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-10-08
120
6:1
6:22
10.4230/LIPIcs.TIME.2018.6
article
Results on Alternating-Time Temporal Logics with Linear Past
Bozzelli, Laura
1
Murano, Aniello
1
Sorrentino, Loredana
1
University of Napoli "Federico II", Italy
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol120-time2018/LIPIcs.TIME.2018.6/LIPIcs.TIME.2018.6.pdf
Alternating-time temporal logics
Linear Past
Model Checking
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-10-08
120
7:1
7:15
10.4230/LIPIcs.TIME.2018.7
article
Extracting Interval Temporal Logic Rules: A First Approach
Bresolin, Davide
1
https://orcid.org/0000-0003-2253-9878
Cominato, Enrico
2
Gnani, Simone
3
Muñoz-Velasco, Emilio
4
https://orcid.org/0000-0002-0117-4219
Sciavicco, Guido
3
https://orcid.org/0000-0002-9221-879X
Department of Mathematics, University of Padova, Italy
Department of Mathematics, Computer Science and Physics, University of Udine, Italy
Department of Mathematics and Computer Science, University of Ferrara, Italy
Department of Applied Mathematics, University of Malaga, Spain
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol120-time2018/LIPIcs.TIME.2018.7/LIPIcs.TIME.2018.7.pdf
Interval temporal logic
Horn fragment
Rule extraction
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-10-08
120
8:1
8:16
10.4230/LIPIcs.TIME.2018.8
article
Faster Dynamic Controllability Checking for Simple Temporal Networks with Uncertainty
Cairo, Massimo
1
Hunsberger, Luke
2
Rizzi, Romeo
3
Department of Mathematics, University of Trento, Italy
Computer Science Department, Vassar College, Poughkeepsie, NY USA
Department of Computer Science, University of Verona, Italy
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol120-time2018/LIPIcs.TIME.2018.8/LIPIcs.TIME.2018.8.pdf
Simple Temporal Networks with Uncertainty
Dynamic Controllability
Temporal Planning under Uncertainty
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-10-08
120
9:1
9:16
10.4230/LIPIcs.TIME.2018.9
article
Extending Conditional Simple Temporal Networks with Partially Shrinkable Uncertainty
Combi, Carlo
1
https://orcid.org/0000-0002-4837-4701
Posenato, Roberto
1
https://orcid.org/0000-0003-0944-0419
Department of Computer Science, University of Verona, Verona, Italy
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol120-time2018/LIPIcs.TIME.2018.9/LIPIcs.TIME.2018.9.pdf
Conditional Simple Temporal Networks with Uncertainty
Partial Shrinkable Temporal Constraint
Dynamic Controllability
Temporal Constraints
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-10-08
120
10:1
10:20
10.4230/LIPIcs.TIME.2018.10
article
On Restricted Disjunctive Temporal Problems: Faster Algorithms and Tractability Frontier
Comin, Carlo
1
https://orcid.org/0000-0001-5748-2029
Rizzi, Romeo
1
https://orcid.org/0000-0002-2387-0952
Department of Computer Science, University of Verona, Italy
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol120-time2018/LIPIcs.TIME.2018.10/LIPIcs.TIME.2018.10.pdf
Restricted Disjuctive Temporal Problems
Simple Temporal Networks
Hyper Temporal Networks
Consistency Checking
Single-Source Shortest-Paths
2-SAT
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-10-08
120
11:1
11:16
10.4230/LIPIcs.TIME.2018.11
article
Algebraic Operators for Processing Sets of Temporal Intervals in Relational Databases
Dohr, Andreas
1
Engels, Christiane
1
Behrend, Andreas
1
University of Bonn, Institute of Computer Science III, Germany
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol120-time2018/LIPIcs.TIME.2018.11/LIPIcs.TIME.2018.11.pdf
Temporal Databases
Relational Operators
Situation Calculus
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-10-08
120
12:1
12:15
10.4230/LIPIcs.TIME.2018.12
article
Deciding the Consistency of Branching Time Interval Networks
Gavanelli, Marco
1
https://orcid.org/0000-0001-7433-5899
Passantino, Alessandro
2
Sciavicco, Guido
2
https://orcid.org/0000-0002-9221-879X
Department of Engineering, University of Ferrara, Italy
Department of Mathematics and Computer Science, University of Ferrara, Italy
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol120-time2018/LIPIcs.TIME.2018.12/LIPIcs.TIME.2018.12.pdf
Constraint programming
Consistency
Branching time
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-10-08
120
13:1
13:17
10.4230/LIPIcs.TIME.2018.13
article
A Game-Theoretic Approach to Timeline-Based Planning with Uncertainty
Gigante, Nicola
1
Montanari, Angelo
1
Cialdea Mayer, Marta
2
Orlandini, Andrea
3
Reynolds, Mark
4
University of Udine, Udine, Italy
University of Roma Tre, Rome, Italy
National Research Council, Rome, Italy
The University of Western Australia, Perth, Australia
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol120-time2018/LIPIcs.TIME.2018.13/LIPIcs.TIME.2018.13.pdf
Timeline-based planning with uncertainty
strategic games
decidability
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-10-08
120
14:1
14:17
10.4230/LIPIcs.TIME.2018.14
article
Sound-and-Complete Algorithms for Checking the Dynamic Controllability of Conditional Simple Temporal Networks with Uncertainty
Hunsberger, Luke
1
Posenato, Roberto
2
https://orcid.org/0000-0003-0944-0419
Department of Computer Science, Vassar College, NY, USA
Department of Computer Science, University of Verona, Verona, Italy
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol120-time2018/LIPIcs.TIME.2018.14/LIPIcs.TIME.2018.14.pdf
Temporal Networks
Conditional Simple Temporal Problem with Uncertainty
Dynamic Controllability
Checking Algorithm
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-10-08
120
15:1
15:15
10.4230/LIPIcs.TIME.2018.15
article
Reducing epsilon-DC Checking for Conditional Simple Temporal Networks to DC Checking
Hunsberger, Luke
1
Posenato, Roberto
2
https://orcid.org/0000-0003-0944-0419
Department of Computer Science, Vassar College, NY, USA
Department of Computer Science, University of Verona, Verona, Italy
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol120-time2018/LIPIcs.TIME.2018.15/LIPIcs.TIME.2018.15.pdf
Conditional Simple Temporal Networks
Dynamic Consistency
Temporal Constraints
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-10-08
120
16:1
16:18
10.4230/LIPIcs.TIME.2018.16
article
On the Expressive Power of Hybrid Branching-Time Logics
Kernberger, Daniel
1
Lange, Martin
1
School of Electrical Engineering and Computer Science, University of Kassel, Germany
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol120-time2018/LIPIcs.TIME.2018.16/LIPIcs.TIME.2018.16.pdf
branching-time
mu-calculus
hybrid logics
expressiveness
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-10-08
120
17:1
17:15
10.4230/LIPIcs.TIME.2018.17
article
A Temporal Logic for Modelling Activities of Daily Living
Kließ, Malte S.
1
https://orcid.org/0000-0001-7219-309X
Jonker, Catholijn M.
2
https://orcid.org/0000-0003-4780-7461
van Riemsdijk, M. Birna
1
Interactive Intelligence, Delft University of Technology, Delft, The Netherlands
Interactive Intelligence, Delft University of Technology, Delft, The Netherlands and , Leiden Institute of Advanced Computer Science, Leiden University
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol120-time2018/LIPIcs.TIME.2018.17/LIPIcs.TIME.2018.17.pdf
Temporal Logic
Reasoning
Durative Activities
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-10-08
120
18:1
18:15
10.4230/LIPIcs.TIME.2018.18
article
GSM+T: A Timed Artifact-Centric Process Model
Köpke, Julius
1
https://orcid.org/0000-0002-6678-5731
Eder, Johann
1
https://orcid.org/0000-0001-6050-468X
Su, Jianwen
2
https://orcid.org/0000-0002-4637-1339
Alpen-Adria-Universität, Klagenfurt, Austria
Department of Computer Science, UC Santa Barbara, USA
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol120-time2018/LIPIcs.TIME.2018.18/LIPIcs.TIME.2018.18.pdf
Guard Stage Milestone
GSM
Time Constraints
Controllability
Case Handling
Business Process Modeling
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-10-08
120
19:1
19:13
10.4230/LIPIcs.TIME.2018.19
article
Learning Qualitative Constraint Networks
Mouhoub, Malek
1
https://orcid.org/0000-0001-7381-1064
Al Marri, Hamad
1
Alanazi, Eisa
2
University of Regina 3737 Wascana Parkway, Regina SK S4V 0A2, Canada
Um Al Qura University Aif Road, 21955, Mecca, Makkah Province, Saudi Arabia
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol120-time2018/LIPIcs.TIME.2018.19/LIPIcs.TIME.2018.19.pdf
Temporal Reasoning
Qualitative Constraint Network (QCN)
Constraint Learning
Path Consistency
Constraint Propagation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-10-08
120
20:1
20:17
10.4230/LIPIcs.TIME.2018.20
article
A Stream Reasoning System for Maritime Monitoring
Santipantakis, Georgios M.
1
Vlachou, Akrivi
1
Doulkeridis, Christos
1
Artikis, Alexander
2
Kontopoulos, Ioannis
3
Vouros, George A.
1
University of Piraeus, Karaoli and Dimitriou 80, 18534 Piraeus, Greece
Department of Maritime Studies, University of Piraeus, Greece, Institute of Informatics & Telecommunications, NCSR "Demokritos", Ag. Paraskevi, Greece
Institute of Informatics & Telecommunications, NCSR "Demokritos", Ag. Paraskevi, Greece
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol120-time2018/LIPIcs.TIME.2018.20/LIPIcs.TIME.2018.20.pdf
event pattern matching
Event Calculus
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-10-08
120
21:1
21:19
10.4230/LIPIcs.TIME.2018.21
article
An Empirical Study on Bidirectional Recurrent Neural Networks for Human Motion Recognition
Tanisaro, Pattreeya
1
Heidemann, Gunther
1
Institute of Cognitive Science, University of Osnabrück, Germany
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol120-time2018/LIPIcs.TIME.2018.21/LIPIcs.TIME.2018.21.pdf
Recurrent Neural Networks
Human Motion Classification
Echo State Networks
Motion Capture
Bidirectional Recurrent Neural Networks
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-10-08
120
22:1
22:22
10.4230/LIPIcs.TIME.2018.22
article
Population Based Methods for Optimising Infinite Behaviours of Timed Automata
Tolonen, Lewis
1
French, Tim
1
Reynolds, Mark
1
The University of Western Australia
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol120-time2018/LIPIcs.TIME.2018.22/LIPIcs.TIME.2018.22.pdf
Timed Automata
Heuristic Search
Ant Colony Optimisation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-10-08
120
23:1
23:18
10.4230/LIPIcs.TIME.2018.23
article
Computational Complexity of a Core Fragment of Halpern-Shoham Logic
Walega, Przemyslaw Andrzej
1
University of Oxford, United Kingdom, University of Warsaw, Poland
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol120-time2018/LIPIcs.TIME.2018.23/LIPIcs.TIME.2018.23.pdf
Temporal Logic
Interval Logic
Computational Complexity
Hybrid Logic