Volume
LIPIcs, Volume 90
24th International Symposium on Temporal Representation and Reasoning (TIME 2017)
Event
TIME 2017, October 16-18, 2017, Mons, BelgiumEditors
Publication Details
- published at: 2017-09-25
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-052-1
- DBLP: db/conf/time/time2017
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 90, TIME'17, Complete Volume
Abstract
LIPIcs, Volume 90, TIME'17, Complete Volume
Cite as
24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@Proceedings{schewe_et_al:LIPIcs.TIME.2017,
title = {{LIPIcs, Volume 90, TIME'17, Complete Volume}},
booktitle = {24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-052-1},
ISSN = {1868-8969},
year = {2017},
volume = {90},
editor = {Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017},
URN = {urn:nbn:de:0030-drops-80233},
doi = {10.4230/LIPIcs.TIME.2017},
annote = {Keywords: Distributed Systems, Design Tools and Techniques, Software/Program Verification, Security and Protection, Models of Computation, Specifying and Verifying and Reasoning about Programs, Mathematical Logic, \lbrackNumerical Linear Algebra\rbrack Linear Systems, Graph Theory}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Organization, List of Authors
Abstract
Front Matter, Table of Contents, Preface, Organization, List of Authors
Cite as
24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{schewe_et_al:LIPIcs.TIME.2017.0,
author = {Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
title = {{Front Matter, Table of Contents, Preface, Organization, List of Authors}},
booktitle = {24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
pages = {0:i--0:xiv},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-052-1},
ISSN = {1868-8969},
year = {2017},
volume = {90},
editor = {Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.0},
URN = {urn:nbn:de:0030-drops-79117},
doi = {10.4230/LIPIcs.TIME.2017.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Organization, List of Authors}
}
Document
Invited Talk
Ontology-Mediated Query Answering over Temporal Data: A Survey (Invited Talk)
Abstract
We discuss the use of various temporal knowledge representation formalisms for ontology-mediated query answering over temporal data. In particular, we analyse ontology and query languages based on the linear temporal logic LTL, the multi-dimensional Halpern-Shoham interval temporal logic HS_n, as well as the metric temporal logic MTL. Our main focus is on the data complexity of answering temporal ontology-mediated queries and their rewritability into standard first-order and datalog queries.
Cite as
Alessandro Artale, Roman Kontchakov, Alisa Kovtunova, Vladislav Ryzhikov, Frank Wolter, and Michael Zakharyaschev. Ontology-Mediated Query Answering over Temporal Data: A Survey (Invited Talk). In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 1:1-1:37, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{artale_et_al:LIPIcs.TIME.2017.1,
author = {Artale, Alessandro and Kontchakov, Roman and Kovtunova, Alisa and Ryzhikov, Vladislav and Wolter, Frank and Zakharyaschev, Michael},
title = {{Ontology-Mediated Query Answering over Temporal Data: A Survey}},
booktitle = {24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
pages = {1:1--1:37},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-052-1},
ISSN = {1868-8969},
year = {2017},
volume = {90},
editor = {Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.1},
URN = {urn:nbn:de:0030-drops-79338},
doi = {10.4230/LIPIcs.TIME.2017.1},
annote = {Keywords: Description Logic, Temporal Logic, Ontology Mediated Query Answering, Data Complexity}
}
Document
Invited Talk
Advances in Quantitative Analysis of Free-Choice Workflow Petri Nets (Invited Talk)
Abstract
We survey recent results on the development of efficient algorithms for the quantitative analysis of business processes modeled as workflow Petri nets. The algorithms can be applied to any workflow net, but have polynomial runtime in the free-choice case.
Cite as
Javier Esparza. Advances in Quantitative Analysis of Free-Choice Workflow Petri Nets (Invited Talk). In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 2:1-2:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{esparza:LIPIcs.TIME.2017.2,
author = {Esparza, Javier},
title = {{Advances in Quantitative Analysis of Free-Choice Workflow Petri Nets}},
booktitle = {24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
pages = {2:1--2:6},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-052-1},
ISSN = {1868-8969},
year = {2017},
volume = {90},
editor = {Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.2},
URN = {urn:nbn:de:0030-drops-79266},
doi = {10.4230/LIPIcs.TIME.2017.2},
annote = {Keywords: Free-choice Petri Nets, concurrency theory, quantitative verification}
}
Document
Invited Talk
Plan and Program Synthesis: A New Look at Some Old Problems (Invited Talk)
Abstract
The proliferation of programmable devices, personal assistants, and autonomous systems presents fundamental challenges to the deployment of safe, predictable systems that can work together, interact seamlessly with humans, and that are taskable and instructable by people who may not know how to program. In this talk, we will revisit the classical problem of program synthesis through the lens of AI automated planning. We will present recent advances in AI automated planning principles and computational methods that support the synthesis of plans with goals and preferences specified in Linear Temporal Logic and Regular Expressions. Moving from automated planning in deterministic domains to planning in nondeterministic domains, we will explore the pathway to synthesizing programs that are taskable and instructable by exploiting state-of-the-art AI planning technology.
Cite as
Sheila A. McIlraith. Plan and Program Synthesis: A New Look at Some Old Problems (Invited Talk). In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{mcilraith:LIPIcs.TIME.2017.3,
author = {McIlraith, Sheila A.},
title = {{Plan and Program Synthesis: A New Look at Some Old Problems}},
booktitle = {24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
pages = {3:1--3:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-052-1},
ISSN = {1868-8969},
year = {2017},
volume = {90},
editor = {Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.3},
URN = {urn:nbn:de:0030-drops-79343},
doi = {10.4230/LIPIcs.TIME.2017.3},
annote = {Keywords: planning, program synthesis, linear temporal logic, regular expressions}
}
Document
Possible and Certain Answers for Queries over Order-Incomplete Data
Abstract
To combine and query ordered data from multiple sources, one needs to handle uncertainty about the possible orderings. Examples of such "order-incomplete" data include integrated event sequences such as log entries; lists of properties (e.g., hotels and restaurants) ranked by an unknown function reflecting relevance or customer ratings; and documents edited concurrently with an uncertain order on edits. This paper introduces a query language for order-incomplete data, based on the positive relational algebra with order-aware accumulation. We use partial orders to represent order-incomplete data, and study possible and certain answers for queries in this context. We show that these problems are respectively NP-complete and coNP-complete, but identify many tractable cases depending on the query operators or input partial orders.
Cite as
Antoine Amarilli, Mouhamadou Lamine Ba, Daniel Deutch, and Pierre Senellart. Possible and Certain Answers for Queries over Order-Incomplete Data. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{amarilli_et_al:LIPIcs.TIME.2017.4,
author = {Amarilli, Antoine and Ba, Mouhamadou Lamine and Deutch, Daniel and Senellart, Pierre},
title = {{Possible and Certain Answers for Queries over Order-Incomplete Data}},
booktitle = {24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
pages = {4:1--4:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-052-1},
ISSN = {1868-8969},
year = {2017},
volume = {90},
editor = {Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.4},
URN = {urn:nbn:de:0030-drops-79311},
doi = {10.4230/LIPIcs.TIME.2017.4},
annote = {Keywords: certain answer, possible answer, partial order, uncertain data}
}
Document
Constraint Identification Using Modified Hoare Logic on Hybrid Models of Gene Networks
Abstract
We present a new hybrid Hoare logic dedicated for a class of linear hybrid automata well suited to model gene regulatory networks. These automata rely on Thomas' discrete framework in which qualitative parameters have been replaced by continuous parameters called celerities. The identification of these parameters remains one of the keypoints of the modelling process, and is difficult especially because the modelling framework is based on a continuous time. We introduce Hoare triples which handle biological traces and pre/post-conditions. Observed chronometrical biological traces play the role of an imperative program for classical Hoare logic and our hybrid Hoare logic, defined by inference rules, is proved to be sound. Furthermore, we present a weakest precondition calculus (a la Dijkstra) which leads to constraints on dynamical parameters. Finally, we illustrate our "constraints generator" with a simplified circadian clock model describing the rhythmicity of cells in mammals on a 24-hour period.
Cite as
Jonathan Behaegel, Jean-Paul Comet, and Maxime Folschette. Constraint Identification Using Modified Hoare Logic on Hybrid Models of Gene Networks. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 5:1-5:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{behaegel_et_al:LIPIcs.TIME.2017.5,
author = {Behaegel, Jonathan and Comet, Jean-Paul and Folschette, Maxime},
title = {{Constraint Identification Using Modified Hoare Logic on Hybrid Models of Gene Networks}},
booktitle = {24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
pages = {5:1--5:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-052-1},
ISSN = {1868-8969},
year = {2017},
volume = {90},
editor = {Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.5},
URN = {urn:nbn:de:0030-drops-79203},
doi = {10.4230/LIPIcs.TIME.2017.5},
annote = {Keywords: Hoare logic, weakest precondition, linear hybrid automata, constraint synthesis, gene networks}
}
Document
Hierarchical Cost-Parity Games
Abstract
Cost-parity games are a fundamental tool in system design for the analysis of reactive and distributed systems that recently have received a lot of attention from the formal methods research community. They allow to reason about the time delay on the requests granted by systems, with a bounded consumption of resources, in their executions.
In this paper, we contribute to research on Cost-parity games by combining them with hierarchical systems, a successful method for the succinct representation of models. We show that determining the winner of a Hierarchical Cost-parity Game is PSpace-Complete, thus matching the complexity of the proper special case of Hierarchical Parity Games. This shows that reasoning about temporal delay can be addressed at a free cost in terms of complexity.
Cite as
Laura Bozzelli, Aniello Murano, Giuseppe Perelli, and Loredana Sorrentino. Hierarchical Cost-Parity Games. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{bozzelli_et_al:LIPIcs.TIME.2017.6,
author = {Bozzelli, Laura and Murano, Aniello and Perelli, Giuseppe and Sorrentino, Loredana},
title = {{Hierarchical Cost-Parity Games}},
booktitle = {24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
pages = {6:1--6:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-052-1},
ISSN = {1868-8969},
year = {2017},
volume = {90},
editor = {Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.6},
URN = {urn:nbn:de:0030-drops-79175},
doi = {10.4230/LIPIcs.TIME.2017.6},
annote = {Keywords: Parity Games, Cost-Parity Games, Hierarchical Systems, System Verification}
}
Document
Timed-Automata-Based Verification of MITL over Signals
Abstract
It has been argued that the most suitable semantic model for real-time formalisms is the non-negative real line (signals), i.e. the continuous semantics, which naturally captures the continuous evolution of system states. Existing tools like UPPAAL are, however, based on omega-sequences with timestamps (timed words), i.e. the pointwise semantics. Furthermore, the support for logic formalisms is very limited in these tools. In this article, we amend these issues by a compositional translation from Metric Temporal Interval Logic (MITL) to signal automata. Combined with an emptiness-preserving encoding of signal automata into timed automata, we obtain a practical automata-based approach to MITL model-checking over signals. We implement the translation in our tool MightyL and report on case studies using LTSmin as the back-end.
Cite as
Thomas Brihaye, Gilles Geeraerts, Hsi-Ming Ho, and Benjamin Monmege. Timed-Automata-Based Verification of MITL over Signals. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{brihaye_et_al:LIPIcs.TIME.2017.7,
author = {Brihaye, Thomas and Geeraerts, Gilles and Ho, Hsi-Ming and Monmege, Benjamin},
title = {{Timed-Automata-Based Verification of MITL over Signals}},
booktitle = {24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
pages = {7:1--7:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-052-1},
ISSN = {1868-8969},
year = {2017},
volume = {90},
editor = {Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.7},
URN = {urn:nbn:de:0030-drops-79126},
doi = {10.4230/LIPIcs.TIME.2017.7},
annote = {Keywords: real-time temporal logic, timed automata, real-time systems}
}
Document
Dynamic Controllability Made Simple
Abstract
Simple Temporal Networks with Uncertainty (STNUs) are a well-studied model for representing temporal constraints, where some intervals (contingent links) have an unknown but bounded duration, discovered only during execution. An STNU is dynamically controllable (DC) if there exists a strategy to execute its time-points satisfying all the constraints, regardless of the actual duration of contingent links revealed during execution.
In this work we present a new system of constraint propagation rules for STNUs, which is sound-and-complete for DC checking. Our system comprises just three rules which, differently from the ones proposed in all previous works, only generate unconditioned constraints. In particular, after applying our sound rules, the network remains an STNU in all respects. Moreover, our completeness proof is short and non-algorithmic, based on the explicit construction of a valid execution strategy. This is a substantial simplification of the theory which underlies all the polynomial-time algorithms for DC-checking.
Our analysis also shows: (1) the existence of late execution strategies for STNUs, (2) the equivalence of several variants of the notion of DC, (3) the existence of a fast algorithm for real-time execution of STNUs, which runs in O(KN) total time in a network with K contingent links and N time points, considerably improving the previous O(N^3)-time bound.
Cite as
Massimo Cairo and Romeo Rizzi. Dynamic Controllability Made Simple. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{cairo_et_al:LIPIcs.TIME.2017.8,
author = {Cairo, Massimo and Rizzi, Romeo},
title = {{Dynamic Controllability Made Simple}},
booktitle = {24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
pages = {8:1--8:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-052-1},
ISSN = {1868-8969},
year = {2017},
volume = {90},
editor = {Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.8},
URN = {urn:nbn:de:0030-drops-79136},
doi = {10.4230/LIPIcs.TIME.2017.8},
annote = {Keywords: Simple Temporal Network with Uncertainty, Dynamic controllability}
}
Document
Incorporating Decision Nodes into Conditional Simple Temporal Networks
Abstract
A Conditional Simple Temporal Network (CSTN) augments a Simple Temporal Network (STN) to include special time-points, called observation time-points. In a CSTN, the agent executing the network controls the execution of every time-point. However, each observation time-point has a unique propositional letter associated with it and, when the agent executes that time-point, the environment assigns a truth value to the corresponding letter. Thus, the agent observes but, does not control the assignment of truth values. A CSTN is dynamically consistent (DC) if there exists a strategy for executing its time-points such that all relevant constraints will be satisfied no matter which truth values the environment assigns to the propositional letters.
Alternatively, in a Labeled Simple Temporal Network (Labeled STN) - also called a Temporal Plan with Choice - the agent executing the network controls the assignment of values to the so-called choice variables. Furthermore, the agent can make those assignments at any time. For this reason, a Labeled STN is equivalent to a Disjunctive Temporal Network.
This paper incorporates both of the above extensions by augmenting a CSTN to include not only observation time-points but also decision time-points. A decision time-point is like an observation time-point in that it has an associated propositional letter whose value is determined when the decision time-point is executed. It differs in that the agent - not the environment - selects that value. The resulting network is called a CSTN with Decisions (CSTND). This paper shows that a CSTND generalizes both CSTNs and Labeled STNs, and proves that the problem of determining whether any given CSTND is dynamically consistent is PSPACE-complete. It also presents algorithms that address two sub-classes of CSTNDs:
(1) those that contain only decision time-points; and (2) those in which all decisions are made before execution begins.
Cite as
Massimo Cairo, Carlo Combi, Carlo Comin, Luke Hunsberger, Roberto Posenato, Romeo Rizzi, and Matteo Zavatteri. Incorporating Decision Nodes into Conditional Simple Temporal Networks. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{cairo_et_al:LIPIcs.TIME.2017.9,
author = {Cairo, Massimo and Combi, Carlo and Comin, Carlo and Hunsberger, Luke and Posenato, Roberto and Rizzi, Romeo and Zavatteri, Matteo},
title = {{Incorporating Decision Nodes into Conditional Simple Temporal Networks}},
booktitle = {24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
pages = {9:1--9:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-052-1},
ISSN = {1868-8969},
year = {2017},
volume = {90},
editor = {Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.9},
URN = {urn:nbn:de:0030-drops-79155},
doi = {10.4230/LIPIcs.TIME.2017.9},
annote = {Keywords: Conditional Simple Temporal Networks with Decisions, Dynamic Consistency, SAT Solver, Hyper Temporal Networks, PSPACE}
}
Document
A Streamlined Model of Conditional Simple Temporal Networks - Semantics and Equivalence Results
Abstract
A Conditional Simple Temporal Network (CSTN) augments a Simple Temporal Network to include a new kind of time-points, called observation time-points. The execution of an observation time-point generates information in real time, specifically, the truth value of a propositional letter. In addition, time-points and temporal constraints may be labeled by conjunctions of (positive or negative) propositional letters. A CSTN is called dynamically consistent (DC) if there exists a dynamic strategy for executing its time-points such that no matter how the observations turn out during execution, the time-points whose labels are consistent with those observations have all been executed, and the constraints whose labels are consistent with those observations have all been satisfied. The strategy is dynamic in that its execution decisions may react to observations.
The original formulation of CSTNs included propositional labels only on time-points, but the DC-checking algorithm was impractical because it was based on a conversion of the semantic constraints into an exponentially-sized Disjunctive Temporal Network. Later work added propositional labels to temporal constraints, and yielded a sound-and-complete propagation-based DC-checking algorithm, empirically demonstrated to be practical across a variety of CSTNs.
This paper introduces a streamlined version of a CSTN in which propositional labels may appear on constraints, but not on time-points. This change simplifies the definition of the DC property, as well as the propagation rules for the DC-checking algorithm. It also simplifies the proofs of the soundness and completeness of those rules.
This paper provides two translations from traditional CSTNs to streamlined CSTNs. Each translation preserves the DC property and, for any DC network, ensures that any dynamic execution strategy for that network can be extended to a strategy for its streamlined counterpart.
Finally, this paper presents an empirical comparison of two versions of the DC-checking algorithm: the original version and a simplified version for streamlined CSTNs. The comparison is based on CSTN benchmarks from earlier work. For small-sized CSTNs, the original version shows the best performance, but the performance difference between the two versions decreases as the number of time-points in the CSTN increases. We conclude that the simplified algorithm is a practical alternative for checking the dynamic consistency of CSTNs.
Cite as
Massimo Cairo, Luke Hunsberger, Roberto Posenato, and Romeo Rizzi. A Streamlined Model of Conditional Simple Temporal Networks - Semantics and Equivalence Results. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{cairo_et_al:LIPIcs.TIME.2017.10,
author = {Cairo, Massimo and Hunsberger, Luke and Posenato, Roberto and Rizzi, Romeo},
title = {{A Streamlined Model of Conditional Simple Temporal Networks - Semantics and Equivalence Results}},
booktitle = {24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
pages = {10:1--10:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-052-1},
ISSN = {1868-8969},
year = {2017},
volume = {90},
editor = {Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.10},
URN = {urn:nbn:de:0030-drops-79145},
doi = {10.4230/LIPIcs.TIME.2017.10},
annote = {Keywords: Conditional Simple Temporal Networks, Dynamic Consistency, Temporal Constraints}
}
Document
Evaluation of Temporal Datasets via Interval Temporal Logic Model Checking
Abstract
The problem of temporal dataset evaluation consists in establishing to what extent a set of temporal data (histories) complies with a given temporal condition. It presents a strong resemblance with the problem of model checking enhanced with the ability of rating the compliance degree of a model against a formula. In this paper, we solve the temporal dataset evaluation problem by suitably combining the outcomes of model checking an interval temporal logic formula against sets of histories (finite interval models), possibly taking into account domain-dependent measures/criteria, like, for instance, sensitivity, specificity, and accuracy. From a technical point of view, the main contribution of the paper is a (deterministic) polynomial time algorithm for interval temporal logic model checking over finite interval models. To the best of our knowledge, this is the first application of a (truly) interval temporal logic model checking in the area of temporal databases and data mining rather than in the formal verification setting.
Cite as
Dario Della Monica, David de Frutos-Escrig, Angelo Montanari, Aniello Murano, and Guido Sciavicco. Evaluation of Temporal Datasets via Interval Temporal Logic Model Checking. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 11:1-11:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{dellamonica_et_al:LIPIcs.TIME.2017.11,
author = {Della Monica, Dario and de Frutos-Escrig, David and Montanari, Angelo and Murano, Aniello and Sciavicco, Guido},
title = {{Evaluation of Temporal Datasets via Interval Temporal Logic Model Checking}},
booktitle = {24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
pages = {11:1--11:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-052-1},
ISSN = {1868-8969},
year = {2017},
volume = {90},
editor = {Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.11},
URN = {urn:nbn:de:0030-drops-79280},
doi = {10.4230/LIPIcs.TIME.2017.11},
annote = {Keywords: Dataset Evaluation, Temporal Databases, Model Checking, Interval Temporal Logics}
}
Document
Time Expressions Recognition with Word Vectors and Neural Networks
Abstract
This work re-examines the widely addressed problem of the recognition and interpretation of time expressions, and suggests an approach based on distributed representations and artificial neural networks. Artificial neural networks allow us to build highly generic models, but the large variety of hyperparameters makes it difficult to determine the best configuration. In this work we study the behavior of different models by varying the number of layers, sizes and normalization techniques. We also analyze the behavior of distributed representations in the temporal domain, where we find interesting properties regarding order and granularity. The experiments were conducted mainly for Spanish, although this does not affect the approach, given its generic nature. This work aims to be a starting point towards processing temporality in texts via word vectors and neural networks, without the need of any kind of feature engineering.
Cite as
Mathias Etcheverry and Dina Wonsever. Time Expressions Recognition with Word Vectors and Neural Networks. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{etcheverry_et_al:LIPIcs.TIME.2017.12,
author = {Etcheverry, Mathias and Wonsever, Dina},
title = {{Time Expressions Recognition with Word Vectors and Neural Networks}},
booktitle = {24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
pages = {12:1--12:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-052-1},
ISSN = {1868-8969},
year = {2017},
volume = {90},
editor = {Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.12},
URN = {urn:nbn:de:0030-drops-79253},
doi = {10.4230/LIPIcs.TIME.2017.12},
annote = {Keywords: Natural Language Processing, Time Expressions, Word Embeddings, Neural Networks}
}
Document
Models and Algorithms for Chronology
Abstract
The last decades have seen the rise of many fundamental chronological debates in Old World archaeology, with far-reaching historical implications. Yet, outside of radiocarbon dating - where Bayesian formal tools and models are applied - these chronological debates are still relying on non-formal models, and dates are mostly derived by hand, without the use of mathematical or computational tools, albeit the large number of complex constraints to be taken into account. This article presents formal models and algorithms for encoding archaeologically-relevant chronological constraints, computing optimal chronologies in an automated way, and automatically checking for chronological properties of a given model.
Cite as
Gilles Geeraerts, Eythan Levy, and Frédéric Pluquet. Models and Algorithms for Chronology. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{geeraerts_et_al:LIPIcs.TIME.2017.13,
author = {Geeraerts, Gilles and Levy, Eythan and Pluquet, Fr\'{e}d\'{e}ric},
title = {{Models and Algorithms for Chronology}},
booktitle = {24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
pages = {13:1--13:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-052-1},
ISSN = {1868-8969},
year = {2017},
volume = {90},
editor = {Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.13},
URN = {urn:nbn:de:0030-drops-79294},
doi = {10.4230/LIPIcs.TIME.2017.13},
annote = {Keywords: Chronology, Algorithms, Archaeology, Formal methods}
}
Document
CTL with Finitely Bounded Semantics
Abstract
We consider a variation of the branching time logic CTL with non-standard, "finitely bounded" semantics (FBS). FBS is naturally defined as game-theoretic semantics where the proponent of truth of an eventuality must commit to a time limit (number of transition steps) within which the formula should become true on all (resp. some) paths starting from the state where the formula is evaluated. The resulting version CTL(FB) of CTL differs essentially from the standard one as it no longer has the finite model property.
We develop two tableaux systems for CTL(FB). The first one deals with infinite sets of formulae, whereas the second one deals with finite sets of formulae in a slightly extended language allowing explicit indication of time limits in formulae. We prove soundness and completeness of both systems and also show that the latter tableaux system provides an EXPTIME decision procedure for it and thus prove EXPTIME-completeness of the satisfiability problem.
Cite as
Valentin Goranko, Antti Kuusisto, and Raine Rönnholm. CTL with Finitely Bounded Semantics. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{goranko_et_al:LIPIcs.TIME.2017.14,
author = {Goranko, Valentin and Kuusisto, Antti and R\"{o}nnholm, Raine},
title = {{CTL with Finitely Bounded Semantics}},
booktitle = {24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
pages = {14:1--14:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-052-1},
ISSN = {1868-8969},
year = {2017},
volume = {90},
editor = {Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.14},
URN = {urn:nbn:de:0030-drops-79325},
doi = {10.4230/LIPIcs.TIME.2017.14},
annote = {Keywords: CTL, finitely bounded semantics, tableaux, decidability}
}
Document
A Relational Algebra for Streaming Tables Living in a Temporal Database World
Abstract
The recently introduced streaming table concept, a fully native representation of streaming data inside a DBMS, enabled modern data-intensive applications with one-time queries (OTQs) and continuous queries (CQs) capabilities on both streaming and standard relational tables. In this paper, we fully acknowledge the temporal nature of streaming tables and we propose to go one step further and integrate them in a temporal DBMS context, where time management is native. Our aim is to break the traditional barrier between the streaming and the temporal worlds, offering complete interoperability between streams and temporal data. To this end, we present a continuous temporal algebra supporting both OTQs and CQs seamlessly on streaming, standard and temporal relational tables. We further show how the transition from continuous to one-time semantics can be managed by defining suitable translation rules, which can also be used as a basis for the implementation of the proposed continuous algebra in a temporal DBMS.
Cite as
Fabio Grandi, Federica Mandreoli, Riccardo Martoglia, and Wilma Penzo. A Relational Algebra for Streaming Tables Living in a Temporal Database World. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{grandi_et_al:LIPIcs.TIME.2017.15,
author = {Grandi, Fabio and Mandreoli, Federica and Martoglia, Riccardo and Penzo, Wilma},
title = {{A Relational Algebra for Streaming Tables Living in a Temporal Database World}},
booktitle = {24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
pages = {15:1--15:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-052-1},
ISSN = {1868-8969},
year = {2017},
volume = {90},
editor = {Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.15},
URN = {urn:nbn:de:0030-drops-79185},
doi = {10.4230/LIPIcs.TIME.2017.15},
annote = {Keywords: Continuous queries, Data streams, Relational algebra, Temporal DB}
}
Document
The Time Ontology of Allen's Interval Algebra
Abstract
Allen's interval algebra is a set of thirteen jointly exhaustive and pairwise disjoint binary relations representing temporal relationships between pairs of timeintervals. Despite widespread use, there is still the question of which time ontology actually underlies Allen's algebra. Early work specified a first-order ontology that can interpret Allen's interval algebra; in this paper, we identify the first-order ontology that is logically synonymous with Allen's interval algebra, so that there is a one-to-one correspondence between models of the ontology and solutions to temporal constraints that are specified using the temporal relations. We further prove a representation theorem for the ontology, thus characterizing its models up to isomorphism.
Cite as
Michael Grüninger and Zhuojun Li. The Time Ontology of Allen's Interval Algebra. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 16:1-16:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{gruninger_et_al:LIPIcs.TIME.2017.16,
author = {Gr\"{u}ninger, Michael and Li, Zhuojun},
title = {{The Time Ontology of Allen's Interval Algebra}},
booktitle = {24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
pages = {16:1--16:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-052-1},
ISSN = {1868-8969},
year = {2017},
volume = {90},
editor = {Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.16},
URN = {urn:nbn:de:0030-drops-79271},
doi = {10.4230/LIPIcs.TIME.2017.16},
annote = {Keywords: time ontology, intervals, composition table, first-order logic, synonymy}
}
Document
The Fully Hybrid mu-Calculus
Abstract
We consider the hybridisation of the mu-calculus through the addition of nominals, binder and jump. Especially the use of the binder differentiates our approach from earlier hybridisations of the mu-calculus and also results in a more involved formal semantics. We then investigate the model checking problem and obtain ExpTime-completeness for the full logic and the same complexity as the modal mu-calculus for a fixed number of variables. We also show that this logic is invariant under hybrid bisimulation and use this result to show that - contrary to the non-hybrid case - the hybrid extension of the full branching time logic CTL* is not a fragment of the fully hybrid mu-calculus.
Cite as
Daniel Kernberger and Martin Lange. The Fully Hybrid mu-Calculus. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 17:1-17:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{kernberger_et_al:LIPIcs.TIME.2017.17,
author = {Kernberger, Daniel and Lange, Martin},
title = {{The Fully Hybrid mu-Calculus}},
booktitle = {24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
pages = {17:1--17:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-052-1},
ISSN = {1868-8969},
year = {2017},
volume = {90},
editor = {Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.17},
URN = {urn:nbn:de:0030-drops-79244},
doi = {10.4230/LIPIcs.TIME.2017.17},
annote = {Keywords: mu-calculus, hybrid logics, model checking, bisimulation invariance}
}
Document
Similarity Search for Spatial Trajectories Using Online Lower Bounding DTW and Presorting Strategies
Abstract
Similarity search with respect to time series has received much attention from research and industry in the last decade. Dynamic time warping is one of the most widely used distance measures in this context. This is due to the simplicity of its definition and the surprising quality of dynamic time warping for time series classification. However, dynamic time warping is not well-behaving with respect to many dimensionality reduction techniques as it does not fulfill the triangle inequality. Additionally, most research on dynamic time warping has been performed with one-dimensional time series or in multivariate cases of varying dimensions. With this paper, we propose three extensions to LB_Rotation for two-dimensional time series (trajectories). We simplify LB_Rotation and adapt it to the online and data streaming case and show how to tune the pruning ratio in similarity search by using presorting strategies based on simple summaries of trajectories. Finally, we provide a thorough valuation of these aspects on a large variety of datasets of spatial trajectories.
Cite as
Marie Kiermeier and Martin Werner. Similarity Search for Spatial Trajectories Using Online Lower Bounding DTW and Presorting Strategies. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 18:1-18:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{kiermeier_et_al:LIPIcs.TIME.2017.18,
author = {Kiermeier, Marie and Werner, Martin},
title = {{Similarity Search for Spatial Trajectories Using Online Lower Bounding DTW and Presorting Strategies}},
booktitle = {24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
pages = {18:1--18:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-052-1},
ISSN = {1868-8969},
year = {2017},
volume = {90},
editor = {Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.18},
URN = {urn:nbn:de:0030-drops-79190},
doi = {10.4230/LIPIcs.TIME.2017.18},
annote = {Keywords: Trajectory Computing, Similarity Search, Dynamic Time Warping, Lower Bounds, k Nearest Neighbor Search, Spatial Presorting}
}
Document
Collective Singleton-Based Consistency for Qualitative Constraint Networks
Abstract
Partial singleton closure under weak composition, or partial singleton (weak) path-consistency for short, is essential for approximating satisfiability of qualitative constraints networks. Briefly put, partial singleton path-consistency ensures that each base relation of each of the constraints of a qualitative constraint network can define a singleton relation in the corresponding partial closure of that network under weak composition, or in its corresponding partially (weak) path-consistent subnetwork for short. In particular, partial singleton path-consistency has been shown to play a crucial role in tackling the minimal labeling problem of a qualitative constraint network, which is the problem of finding the strongest implied constraints of that network. In this paper, we propose a stronger local consistency that couples partial singleton path-consistency with the idea of collectively deleting certain unfeasible base relations by exploiting singleton checks. We then propose an efficient algorithm for enforcing this consistency that, given a qualitative constraint network, performs fewer constraint checks than the respective algorithm for enforcing partial singleton path-consistency in that network. We formally prove certain properties of our new local consistency, and motivate its usefulness through demonstrative examples and a preliminary experimental evaluation with qualitative constraint networks of Interval Algebra.
Cite as
Michael Sioutis, Anastasia Paparrizou, and Jean-François Condotta. Collective Singleton-Based Consistency for Qualitative Constraint Networks. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 19:1-19:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{sioutis_et_al:LIPIcs.TIME.2017.19,
author = {Sioutis, Michael and Paparrizou, Anastasia and Condotta, Jean-Fran\c{c}ois},
title = {{Collective Singleton-Based Consistency for Qualitative Constraint Networks}},
booktitle = {24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
pages = {19:1--19:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-052-1},
ISSN = {1868-8969},
year = {2017},
volume = {90},
editor = {Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.19},
URN = {urn:nbn:de:0030-drops-79237},
doi = {10.4230/LIPIcs.TIME.2017.19},
annote = {Keywords: Qualitative constraint network, qualitative spatial and temporal reasoning, partial singleton path-consistency, local consistency, minimal labeling pr}
}
Document
Dynamic Purpose Decomposition of Mobility Flows Based on Geographical Data
Abstract
Spatial and temporal decomposition of aggregated mobility flows is nowadays a commonly addressed issue, but a trip-purpose decomposition of mobility flows is a more challenging topic, which requires more sensitive analysis such as heterogeneous data fusion. In this paper, we study the relation between land use and mobility purposes. We propose a model that dynamically decomposes mobility flows into six mobility purposes. To this end, we use a national transportation database that surveyed more than 35,000 individuals and a national ground description database that identifies six distinct ground types. Based on these two types of data, we dynamically solve several overdetermined systems of linear equations from a training set and we infer the travel purposes. Our experimental results demonstrate that our model effectively predicts the purposes of mobility from the land use. Furthermore, our model shows great results compared with a reference supervised learning decomposition.
Cite as
Etienne Thuillier, Laurent Moalic, and Alexandre Caminada. Dynamic Purpose Decomposition of Mobility Flows Based on Geographical Data. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 20:1-20:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{thuillier_et_al:LIPIcs.TIME.2017.20,
author = {Thuillier, Etienne and Moalic, Laurent and Caminada, Alexandre},
title = {{Dynamic Purpose Decomposition of Mobility Flows Based on Geographical Data}},
booktitle = {24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
pages = {20:1--20:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-052-1},
ISSN = {1868-8969},
year = {2017},
volume = {90},
editor = {Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.20},
URN = {urn:nbn:de:0030-drops-79221},
doi = {10.4230/LIPIcs.TIME.2017.20},
annote = {Keywords: Human mobility, Purpose decomposition, Information extraction, Linear model}
}
Document
Time Dependent Policy-Based Access Control
Abstract
Access control policies are essential to determine who is allowed to access data in a system without compromising the data's security. However, applications inside a distributed environment may require those policies to be dependent on the actual content of the data, the flow of information, while also on other attributes of the environment such as the time.
In this paper, we use systems of Timed Automata to model distributed systems and we present a logic in which one can express time-dependent policies for access control. We show how a fragment of our logic can be reduced to a logic that current model checkers for Timed Automata such as UPPAAL can handle and we present a translator that performs this reduction. We then use our translator and UPPAAL to enforce time-dependent policy-based access control on an example application from the aerospace industry.
Cite as
Panagiotis Vasilikos, Flemming Nielson, and Hanne Riis Nielson. Time Dependent Policy-Based Access Control. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 21:1-21:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{vasilikos_et_al:LIPIcs.TIME.2017.21,
author = {Vasilikos, Panagiotis and Nielson, Flemming and Nielson, Hanne Riis},
title = {{Time Dependent Policy-Based Access Control}},
booktitle = {24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
pages = {21:1--21:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-052-1},
ISSN = {1868-8969},
year = {2017},
volume = {90},
editor = {Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.21},
URN = {urn:nbn:de:0030-drops-79219},
doi = {10.4230/LIPIcs.TIME.2017.21},
annote = {Keywords: Access Control, Timed Automata, Time-Dependent Policies, UPPAAL}
}
Document
On Expressiveness of Halpern-Shoham Logic and its Horn Fragments
Abstract
Abstract: Halpern and Shoham's modal logic of time intervals (HS in short) is an elegant and highly influential propositional interval-based logic. Its Horn fragments and their hybrid extensions have been recently intensively studied and successfully applied in real-world use cases. Detailed investigation of their decidability and computational complexity has been conducted, however, there has been significantly less research on their expressive power. In this paper we make a step towards filling this gap. We (1) show what time structures are definable in the language of HS, and (2) determine which HS fragments are capable of expressing: hybrid machinery, i.e., nominals and satisfaction operators, and somewhere, difference, and everywhere modal operators. These results enable us to classify HS Horn fragments according to their expressive power and to gain insight in the interplay between their decidability/computational complexity and expressiveness.
Cite as
Przemyslaw Andrzej Walega. On Expressiveness of Halpern-Shoham Logic and its Horn Fragments. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{walega:LIPIcs.TIME.2017.22,
author = {Walega, Przemyslaw Andrzej},
title = {{On Expressiveness of Halpern-Shoham Logic and its Horn Fragments}},
booktitle = {24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
pages = {22:1--22:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-052-1},
ISSN = {1868-8969},
year = {2017},
volume = {90},
editor = {Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.22},
URN = {urn:nbn:de:0030-drops-79307},
doi = {10.4230/LIPIcs.TIME.2017.22},
annote = {Keywords: Temporal Logic, Interval Logic, Expressiveness, Hybrid Logic}
}
Document
Conditional Simple Temporal Networks with Uncertainty and Decisions
Abstract
A conditional simple temporal network with uncertainty (CSTNU) is a framework able to model temporal plans subject to both conditional constraints and uncertain durations. The combination of these two characteristics represents the uncontrollable part of the network. That is, before the network starts executing, we do not know completely which time points and constraints will be taken into consideration nor how long the uncertain durations will last. Dynamic controllability (DC) implies the existence of a strategy scheduling the time points of the network in real time depending on how the uncontrollable part behaves. Despite all this, CSTNUs fail to model temporal plans in which a few conditional constraints are under control and may therefore influence (or be influenced by) the uncontrollable part. To bridge this gap, this paper proposes conditional simple temporal networks with uncertainty and decisions (CSTNUDs) which introduce decision time points into the specification in order to operate on this conditional part under control. We model the dynamic controllability checking (DC-checking) of a CSTNUD as a two-player game in which each player makes his moves in his turn at a specific time instant. We give an encoding into timed game automata for a sound and complete DC-checking. We also synthesize memoryless execution strategies for CSTNUDs proved to be DC. The proposed approach is fully automated.
Cite as
Matteo Zavatteri. Conditional Simple Temporal Networks with Uncertainty and Decisions. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 23:1-23:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{zavatteri:LIPIcs.TIME.2017.23,
author = {Zavatteri, Matteo},
title = {{Conditional Simple Temporal Networks with Uncertainty and Decisions}},
booktitle = {24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
pages = {23:1--23:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-052-1},
ISSN = {1868-8969},
year = {2017},
volume = {90},
editor = {Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.23},
URN = {urn:nbn:de:0030-drops-79169},
doi = {10.4230/LIPIcs.TIME.2017.23},
annote = {Keywords: cstnud, dynamic controllability, timed game automata, controller synthesis, advanced temporal planning under uncertainty}
}