Volume
LIPIcs, Volume 147
26th International Symposium on Temporal Representation and Reasoning (TIME 2019)
Event
TIME 2019, October 16-19, 2019, Málaga, SpainEditors
Publication Details
- published at: 2019-10-07
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-127-6
- DBLP: db/conf/time/time2019
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 147, TIME'19, Complete Volume
Abstract
LIPIcs, Volume 147, TIME'19, Complete Volume
Cite as
26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@Proceedings{gamper_et_al:LIPIcs.TIME.2019,
title = {{LIPIcs, Volume 147, TIME'19, Complete Volume}},
booktitle = {26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-127-6},
ISSN = {1868-8969},
year = {2019},
volume = {147},
editor = {Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019},
URN = {urn:nbn:de:0030-drops-113887},
doi = {10.4230/LIPIcs.TIME.2019},
annote = {Keywords: Theory of computation, Logic; Information systems, Temporal data; Computing methodologies, Knowledge representation and reasoning}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{gamper_et_al:LIPIcs.TIME.2019.0,
author = {Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
pages = {0:i--0:xiv},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-127-6},
ISSN = {1868-8969},
year = {2019},
volume = {147},
editor = {Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.0},
URN = {urn:nbn:de:0030-drops-113582},
doi = {10.4230/LIPIcs.TIME.2019.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
Computing the Fourier Transformation over Temporal Data Streams (Invited Talk)
Abstract
In radio astronomy the sky is continuously scanned to collect frequency information about celestial objects. The inverse 2D Fourier transformation is used to generate images of the sky from the collected frequency information. We propose an algorithm that incrementally refines images by processing frequency information as it arrives in a temporal data stream. A direct implementation of the refinement with the discrete Fourier transformation requires O(N^2) complex multiplications to process an element of the stream. We propose a new algorithm that avoids recomputations and only requires O(N) complex multiplications.
Cite as
Michael H. Böhlen and Muhammad Saad. Computing the Fourier Transformation over Temporal Data Streams (Invited Talk). In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 1:1-1:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{bohlen_et_al:LIPIcs.TIME.2019.1,
author = {B\"{o}hlen, Michael H. and Saad, Muhammad},
title = {{Computing the Fourier Transformation over Temporal Data Streams}},
booktitle = {26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
pages = {1:1--1:4},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-127-6},
ISSN = {1868-8969},
year = {2019},
volume = {147},
editor = {Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.1},
URN = {urn:nbn:de:0030-drops-113595},
doi = {10.4230/LIPIcs.TIME.2019.1},
annote = {Keywords: Data streams, Fourier transform, time-varying data}
}
Document
Invited Talk
From Unstructured Data to Narrative Abstractive Summaries (Invited Talk)
Abstract
To provide with easy and optimal access to digital information, narrative summaries must have a coherent and natural structure. Depending on how a summary is produced, a distinction can be made between extractive and abstractive summaries. Using an abstractive summarization approach, the relevant information (e.g., who? what?, when?, where?,...) could be fused together, leading to the generation of one or more new sentences. However, in order to do this it is necessary to obtain and process the temporal information in a text. A very effective way is the generation of timelines starting from multiple documents so that the generation of summaries is supported by the generated timeline, without losing the relevant temporal information of the texts. In this proposal, a enriched timeline is generated automatically, and the process of generating abstractive summaries is presented using this timeline as a basis [Barros et al., 2019]. Finally, potential applications of the automatic timeline generation would be presented, as for example its application to Fake News detection.
Cite as
Estela Saquete Boró. From Unstructured Data to Narrative Abstractive Summaries (Invited Talk). In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 2:1-2:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{saqueteboro:LIPIcs.TIME.2019.2,
author = {Saquete Bor\'{o}, Estela},
title = {{From Unstructured Data to Narrative Abstractive Summaries}},
booktitle = {26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
pages = {2:1--2:4},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-127-6},
ISSN = {1868-8969},
year = {2019},
volume = {147},
editor = {Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.2},
URN = {urn:nbn:de:0030-drops-113608},
doi = {10.4230/LIPIcs.TIME.2019.2},
annote = {Keywords: Narrative summarization, Abstractive summarization, Timeline Generation, Temporal Information Processing, Natural Language Generation}
}
Document
Invited Talk
On the Computation of Nash Equilibria in Games on Graphs (Invited Talk)
Abstract
In this talk, I will show how one can characterize and compute Nash equilibria in multiplayer games played on graphs. I will present in particular a construction, called the suspect game construction, which allows to reduce the computation of Nash equilibria to the computation of winning strategies in a two-player zero-sum game.
Cite as
Patricia Bouyer. On the Computation of Nash Equilibria in Games on Graphs (Invited Talk). In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 3:1-3:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{bouyer:LIPIcs.TIME.2019.3,
author = {Bouyer, Patricia},
title = {{On the Computation of Nash Equilibria in Games on Graphs}},
booktitle = {26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
pages = {3:1--3:3},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-127-6},
ISSN = {1868-8969},
year = {2019},
volume = {147},
editor = {Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.3},
URN = {urn:nbn:de:0030-drops-113616},
doi = {10.4230/LIPIcs.TIME.2019.3},
annote = {Keywords: Multiplayer games, Nash equilibria}
}
Document
A Modal Logic for Subject-Oriented Spatial Reasoning
Abstract
We present a modal logic for representing and reasoning about space seen from the subject’s perspective. The language of our logic comprises modal operators for the relations "in front", "behind", "to the left", and "to the right" of the subject, which introduce the intrinsic frame of reference; and operators for "behind an object", "between the subject and an object", "to the left of an object", and "to the right of an object", employing the relative frame of reference. The language allows us to express nominals, hybrid operators, and a restricted form of distance operators which, as we demonstrate by example, makes the logic interesting for potential applications. We prove that the satisfiability problem in the logic is decidable and in particular PSpace-complete.
Cite as
Przemysław Andrzej Wałęga and Michał Zawidzki. A Modal Logic for Subject-Oriented Spatial Reasoning. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 4:1-4:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{walega_et_al:LIPIcs.TIME.2019.4,
author = {Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej and Zawidzki, Micha{\l}},
title = {{A Modal Logic for Subject-Oriented Spatial Reasoning}},
booktitle = {26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
pages = {4:1--4:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-127-6},
ISSN = {1868-8969},
year = {2019},
volume = {147},
editor = {Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.4},
URN = {urn:nbn:de:0030-drops-113622},
doi = {10.4230/LIPIcs.TIME.2019.4},
annote = {Keywords: spatial logic, modal logic, subject-oriented, computational complexity}
}
Document
Customizing BPMN Diagrams Using Timelines
Abstract
BPMN (Business Process Model and Notation) is widely used standard modeling technique for representing Business Processes by using diagrams, but lacks in some aspects. Representing execution-dependent and time-dependent decisions in BPMN Diagrams may be a daunting challenge [Carlo Combi et al., 2017]. In many cases such constraints are omitted in order to preserve the simplicity and the readability of the process model. However, for purposes such as compliance checking, process mining, and verification, formalizing such constraints could be very useful. In this paper, we propose a novel approach for annotating BPMN Diagrams with Temporal Synchronization Rules borrowed from the timeline-based planning field. We discuss the expressivity of the proposed approach and show that it is able to capture a lot of complex temporally-related constraints without affecting the structure of BPMN diagrams. Finally, we provide a mapping from annotated BPMN diagrams to timeline-based planning problems that allows one to take advantage of the last twenty years of theoretical and practical developments in the field.
Cite as
Carlo Combi, Barbara Oliboni, and Pietro Sala. Customizing BPMN Diagrams Using Timelines. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{combi_et_al:LIPIcs.TIME.2019.5,
author = {Combi, Carlo and Oliboni, Barbara and Sala, Pietro},
title = {{Customizing BPMN Diagrams Using Timelines}},
booktitle = {26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
pages = {5:1--5:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-127-6},
ISSN = {1868-8969},
year = {2019},
volume = {147},
editor = {Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.5},
URN = {urn:nbn:de:0030-drops-113630},
doi = {10.4230/LIPIcs.TIME.2019.5},
annote = {Keywords: Business Processes, BPMN, Timelines, Temporal Constraints}
}
Document
The Second Order Traffic Fine: Temporal Reasoning in European Transport Regulations
Abstract
We argue that European transport regulations can be formalized within the Sigma^1_1 fragment of monadic second order logic, and possibly weaker fragments including linear temporal logic. We consider several articles in the regulation to verify these claims.
Cite as
Ana de Almeida Borges, Juan José Conejero Rodríguez, David Fernández-Duque, Mireia González Bedmar, and Joost J. Joosten. The Second Order Traffic Fine: Temporal Reasoning in European Transport Regulations. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{dealmeidaborges_et_al:LIPIcs.TIME.2019.6,
author = {de Almeida Borges, Ana and Conejero Rodr{\'\i}guez, Juan Jos\'{e} and Fern\'{a}ndez-Duque, David and Gonz\'{a}lez Bedmar, Mireia and Joosten, Joost J.},
title = {{The Second Order Traffic Fine: Temporal Reasoning in European Transport Regulations}},
booktitle = {26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
pages = {6:1--6:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-127-6},
ISSN = {1868-8969},
year = {2019},
volume = {147},
editor = {Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.6},
URN = {urn:nbn:de:0030-drops-113649},
doi = {10.4230/LIPIcs.TIME.2019.6},
annote = {Keywords: linear temporal logic, monadic second order logic, formalized law, transport regulations}
}
Document
Two-Dimensional Rule Language for Querying Sensor Log Data: A Framework and Use Cases
Abstract
Motivated by two industrial use cases that involve detecting events of interest in (asynchronous) time series from sensors in manufacturing rigs and gas turbines, we design an expressive rule language DslD equipped with interval aggregate functions (such as weighted average over a time interval), Allen’s interval relations and various metric constructs. We demonstrate how to model events in the uses cases in terms of DslD programs. We show that answering DslD queries in our use cases can be reduced to evaluating SQL queries. Our experiments with the use cases, carried out on the Apache Spark system, show that such SQL queries scale well on large real-world datasets.
Cite as
Sebastian Brandt, Diego Calvanese, Elem Güzel Kalaycı, Roman Kontchakov, Benjamin Mörzinger, Vladislav Ryzhikov, Guohui Xiao, and Michael Zakharyaschev. Two-Dimensional Rule Language for Querying Sensor Log Data: A Framework and Use Cases. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 7:1-7:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{brandt_et_al:LIPIcs.TIME.2019.7,
author = {Brandt, Sebastian and Calvanese, Diego and Kalayc{\i}, Elem G\"{u}zel and Kontchakov, Roman and M\"{o}rzinger, Benjamin and Ryzhikov, Vladislav and Xiao, Guohui and Zakharyaschev, Michael},
title = {{Two-Dimensional Rule Language for Querying Sensor Log Data: A Framework and Use Cases}},
booktitle = {26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
pages = {7:1--7:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-127-6},
ISSN = {1868-8969},
year = {2019},
volume = {147},
editor = {Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.7},
URN = {urn:nbn:de:0030-drops-113658},
doi = {10.4230/LIPIcs.TIME.2019.7},
annote = {Keywords: Ontology-based data access, temporal logic, sensor log data}
}
Document
Time-Aware Probabilistic Knowledge Graphs
Abstract
The emergence of open information extraction as a tool for constructing and expanding knowledge graphs has aided the growth of temporal data, for instance, YAGO, NELL and Wikidata. While YAGO and Wikidata maintain the valid time of facts, NELL records the time point at which a fact is retrieved from some Web corpora. Collectively, these knowledge graphs (KG) store facts extracted from Wikipedia and other sources. Due to the imprecise nature of the extraction tools that are used to build and expand KG, such as NELL, the facts in the KG are weighted (a confidence value representing the correctness of a fact). Additionally, NELL can be considered as a transaction time KG because every fact is associated with extraction date. On the other hand, YAGO and Wikidata use the valid time model because they maintain facts together with their validity time (temporal scope). In this paper, we propose a bitemporal model (that combines transaction and valid time models) for maintaining and querying bitemporal probabilistic knowledge graphs. We study coalescing and scalability of marginal and MAP inference. Moreover, we show that complexity of reasoning tasks in atemporal probabilistic KG carry over to the bitemporal setting. Finally, we report our evaluation results of the proposed model.
Cite as
Melisachew Wudage Chekol and Heiner Stuckenschmidt. Time-Aware Probabilistic Knowledge Graphs. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{chekol_et_al:LIPIcs.TIME.2019.8,
author = {Chekol, Melisachew Wudage and Stuckenschmidt, Heiner},
title = {{Time-Aware Probabilistic Knowledge Graphs}},
booktitle = {26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
pages = {8:1--8:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-127-6},
ISSN = {1868-8969},
year = {2019},
volume = {147},
editor = {Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.8},
URN = {urn:nbn:de:0030-drops-113662},
doi = {10.4230/LIPIcs.TIME.2019.8},
annote = {Keywords: temporal, probabilistic, knowledge graph, OWL-RL}
}
Document
Qualitative Reasoning and Data Mining
Abstract
In this paper, we introduce a new data mining framework that is based on qualitative reasoning. We consider databases where the item domains are of different types, such as numerical values, time intervals and spatial regions. Then, for the considered tasks, we associate to each item a constraint network in a qualitative formalism representing the relations between all the pairs of objects of the database w.r.t. this item. In this context, the introduced data mining problems consist in discovering qualitative covariations between items. In a sense, our framework can be seen as a generalization of gradual itemset mining. In order to solve the introduced problem, we use a declarative approach based on the satisfiability problem in classical propositional logic (SAT). Indeed, we define SAT encodings where the models represent the desired patterns.
Cite as
Yakoub Salhi. Qualitative Reasoning and Data Mining. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 9:1-9:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{salhi:LIPIcs.TIME.2019.9,
author = {Salhi, Yakoub},
title = {{Qualitative Reasoning and Data Mining}},
booktitle = {26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
pages = {9:1--9:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-127-6},
ISSN = {1868-8969},
year = {2019},
volume = {147},
editor = {Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.9},
URN = {urn:nbn:de:0030-drops-113677},
doi = {10.4230/LIPIcs.TIME.2019.9},
annote = {Keywords: Qualitative Database, Qualitative Pattern Mining, Declarative Approach, SAT Modeling}
}
Document
Recurrent Neural Networks Applied to GNSS Time Series for Denoising and Prediction
Abstract
Global Navigation Satellite Systems (GNSS) are systems that continuously acquire data and provide position time series. Many monitoring applications are based on GNSS data and their efficiency depends on the capability in the time series analysis to characterize the signal content and/or to predict incoming coordinates. In this work we propose a suitable Network Architecture, based on Long Short Term Memory Recurrent Neural Networks, to solve two main tasks in GNSS time series analysis: denoising and prediction. We carry out an analysis on a synthetic time series, then we inspect two real different case studies and evaluate the results. We develop a non-deep network that removes almost the 50% of scattering from real GNSS time series and achieves a coordinate prediction with 1.1 millimeters of Mean Squared Error.
Cite as
Elena Loli Piccolomini, Stefano Gandolfi, Luca Poluzzi, Luca Tavasci, Pasquale Cascarano, and Andrea Pascucci. Recurrent Neural Networks Applied to GNSS Time Series for Denoising and Prediction. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 10:1-10:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{lolipiccolomini_et_al:LIPIcs.TIME.2019.10,
author = {Loli Piccolomini, Elena and Gandolfi, Stefano and Poluzzi, Luca and Tavasci, Luca and Cascarano, Pasquale and Pascucci, Andrea},
title = {{Recurrent Neural Networks Applied to GNSS Time Series for Denoising and Prediction}},
booktitle = {26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
pages = {10:1--10:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-127-6},
ISSN = {1868-8969},
year = {2019},
volume = {147},
editor = {Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.10},
URN = {urn:nbn:de:0030-drops-113687},
doi = {10.4230/LIPIcs.TIME.2019.10},
annote = {Keywords: Deep Neural Networks, Recurrent Neural Networks, Time Series Denoising, Time Series Prediction}
}
Document
From Quantified CTL to QBF
Abstract
QCTL extends the temporal logic CTL with quantifications over atomic propositions. This extension is known to be very expressive: QCTL allows us to express complex properties over Kripke structures (it is as expressive as MSO). Several semantics exist for the quantifications: here, we work with the structure semantics, where the extra propositions label the Kripke structure (and not its execution tree), and the model-checking problem is known to be PSPACE-complete in this framework. We propose a model-checking algorithm for QCTL based on a reduction to QBF. We consider several reduction strategies, and we compare them with a prototype (based on the SMT-solver Z3) on several examples.
Cite as
Akash Hossain and François Laroussinie. From Quantified CTL to QBF. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{hossain_et_al:LIPIcs.TIME.2019.11,
author = {Hossain, Akash and Laroussinie, Fran\c{c}ois},
title = {{From Quantified CTL to QBF}},
booktitle = {26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
pages = {11:1--11:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-127-6},
ISSN = {1868-8969},
year = {2019},
volume = {147},
editor = {Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.11},
URN = {urn:nbn:de:0030-drops-113699},
doi = {10.4230/LIPIcs.TIME.2019.11},
annote = {Keywords: Model-checking, Quantified CTL, QBF solvers, SAT based model-checking}
}
Document
Towards Certified Model Checking for PLTL Using One-Pass Tableaux
Abstract
The standard model checking setup analyses whether the given system specification satisfies a dedicated temporal property of the system, providing a positive answer here or a counter-example. At the same time, it is often useful to have an explicit proof that certifies the satisfiability. This is exactly what the certified model checking (CMC) has been introduced for. The paper argues that one-pass (context-based) tableau for PLTL can be efficiently used in the CMC setting, emphasising the following two advantages of this technique. First, the use of the context in which the eventualities occur, forces them to fulfil as soon as possible. Second, a dual to the tableau sequent calculus can be used to formalise the certificates. The combination of the one-pass tableau and the dual sequent calculus enables us to provide not only counter-examples for unsatisfied properties, but also proofs for satisfied properties that can be checked in a proof assistant. In addition, the construction of the tableau is enriched by an embedded solver, to which we dedicate those (propositional) computational tasks that are costly for the tableaux rules applied solely. The combination of the above techniques is particularly helpful to reason about large (system) specifications.
Cite as
Alex Abuin, Alexander Bolotov, Unai Díaz de Cerio, Montserrat Hermo, and Paqui Lucio. Towards Certified Model Checking for PLTL Using One-Pass Tableaux. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{abuin_et_al:LIPIcs.TIME.2019.12,
author = {Abuin, Alex and Bolotov, Alexander and D{\'\i}az de Cerio, Unai and Hermo, Montserrat and Lucio, Paqui},
title = {{Towards Certified Model Checking for PLTL Using One-Pass Tableaux}},
booktitle = {26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
pages = {12:1--12:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-127-6},
ISSN = {1868-8969},
year = {2019},
volume = {147},
editor = {Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.12},
URN = {urn:nbn:de:0030-drops-113702},
doi = {10.4230/LIPIcs.TIME.2019.12},
annote = {Keywords: Temporal logic, fairness, expressiveness, linear-time, Certified model checking}
}
Document
Minimisation of Models Satisfying CTL Formulas
Abstract
We study the problem of minimisation of a given finite pointed Kripke model satisfying a given CTL formula, with the only objective to preserve the satisfaction of that formula in the resulting reduced model. We consider minimisations of the model with respect both to state-based redundancies and formula-based redundancies in that model. We develop a procedure computing all such minimisations, illustrate it with some examples, and provide some complexity analysis for it.
Cite as
Serenella Cerrito, Amélie David, and Valentin Goranko. Minimisation of Models Satisfying CTL Formulas. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 13:1-13:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{cerrito_et_al:LIPIcs.TIME.2019.13,
author = {Cerrito, Serenella and David, Am\'{e}lie and Goranko, Valentin},
title = {{Minimisation of Models Satisfying CTL Formulas}},
booktitle = {26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
pages = {13:1--13:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-127-6},
ISSN = {1868-8969},
year = {2019},
volume = {147},
editor = {Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.13},
URN = {urn:nbn:de:0030-drops-113718},
doi = {10.4230/LIPIcs.TIME.2019.13},
annote = {Keywords: CTL, model minimisation, bisimulation reduction, tableaux-based reduction}
}
Document
On the Utility of Neighbourhood Singleton-Style Consistencies for Qualitative Constraint-Based Spatial and Temporal Reasoning
Abstract
A singleton-style consistency is a local consistency that verifies if each base relation (atom) of each constraint of a qualitative constraint network (QCN) can serve as a support with respect to the closure of that network under a (naturally) weaker local consistency. This local consistency is essential for tackling fundamental reasoning problems associated with QCNs, such as the satisfiability checking or the minimal labeling problem, but can suffer from redundant constraint checks, especially when those checks occur far from where the pruning usually takes place. In this paper, we propose singleton-style consistencies that are applied just on the neighbourhood of a singleton-checked constraint instead of the whole network. We make a theoretical comparison with existing consistencies and consequently prove some properties of the new ones. In addition, we propose algorithms to enforce our consistencies, as well as parsimonious variants thereof, that are more efficient in practice than the state of the art. We make an experimental evaluation with random and structured QCNs of Interval Algebra in the phase transition region to demonstrate the potential of our approach.
Cite as
Michael Sioutis, Anastasia Paparrizou, and Tomi Janhunen. On the Utility of Neighbourhood Singleton-Style Consistencies for Qualitative Constraint-Based Spatial and Temporal Reasoning. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{sioutis_et_al:LIPIcs.TIME.2019.14,
author = {Sioutis, Michael and Paparrizou, Anastasia and Janhunen, Tomi},
title = {{On the Utility of Neighbourhood Singleton-Style Consistencies for Qualitative Constraint-Based Spatial and Temporal Reasoning}},
booktitle = {26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
pages = {14:1--14:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-127-6},
ISSN = {1868-8969},
year = {2019},
volume = {147},
editor = {Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.14},
URN = {urn:nbn:de:0030-drops-113727},
doi = {10.4230/LIPIcs.TIME.2019.14},
annote = {Keywords: Qualitative constraints, spatial and temporal reasoning, singleton-style consistencies, neighbourhood, minimal labeling problem}
}
Document
A Bounded Domain Property for an Expressive Fragment of First-Order Linear Temporal Logic
Abstract
First-Order Linear Temporal Logic (FOLTL) is well-suited to specify infinite-state systems. However, FOLTL satisfiability is not even semi-decidable, thus preventing automated verification. To address this, a possible track is to constrain specifications to a decidable fragment of FOLTL, but known fragments are too restricted to be usable in practice. In this paper, we exhibit various fragments of increasing scope that provide a pertinent basis for abstract specification of infinite-state systems. We show that these fragments enjoy the Bounded Domain Property (any satisfiable FOLTL formula has a model with a finite, bounded FO domain), which provides a basis for complete, automated verification by reduction to LTL satisfiability. Finally, we present a simple case study illustrating the applicability and limitations of our results.
Cite as
Quentin Peyras, Julien Brunel, and David Chemouil. A Bounded Domain Property for an Expressive Fragment of First-Order Linear Temporal Logic. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{peyras_et_al:LIPIcs.TIME.2019.15,
author = {Peyras, Quentin and Brunel, Julien and Chemouil, David},
title = {{A Bounded Domain Property for an Expressive Fragment of First-Order Linear Temporal Logic}},
booktitle = {26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
pages = {15:1--15:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-127-6},
ISSN = {1868-8969},
year = {2019},
volume = {147},
editor = {Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.15},
URN = {urn:nbn:de:0030-drops-113731},
doi = {10.4230/LIPIcs.TIME.2019.15},
annote = {Keywords: First-Order Linear Temporal Logic, Bounded Domain Property, Finite Domain Property, Decidability}
}
Document
Hybrid SAT-Based Consistency Checking Algorithms for Simple Temporal Networks with Decisions
Abstract
A Simple Temporal Network (STN) consists of time points modeling temporal events and constraints modeling the minimal and maximal temporal distance between them. A Simple Temporal Network with Decisions (STND) extends an STN by adding decision time points to model temporal plans with decisions. A decision time point is a special kind of time point that once executed allows for deciding a truth value for an associated Boolean proposition. Furthermore, STNDs label time points and constraints by conjunctions of literals saying for which scenarios (i.e., complete truth value assignments to the propositions) they are relevant. Thus, an STND models a family of STNs each obtained as a projection of the initial STND onto a scenario. An STND is consistent if there exists a consistent scenario (i.e., a scenario such that the corresponding STN projection is consistent). Recently, a hybrid SAT-based consistency checking algorithm (HSCC) was proposed to check the consistency of an STND. Unfortunately, that approach lacks experimental evaluation and does not allow for the synthesis of all consistent scenarios. In this paper, we propose an incremental HSCC algorithm for STNDs that (i) is faster than the previous one and (ii) allows for the synthesis of all consistent scenarios and related early execution schedules (offline temporal planning). Then, we carry out an experimental evaluation with KAPPA, a tool that we developed for STNDs. Finally, we prove that STNDs and disjunctive temporal networks (DTNs) are equivalent.
Cite as
Matteo Zavatteri, Carlo Combi, Romeo Rizzi, and Luca Viganò. Hybrid SAT-Based Consistency Checking Algorithms for Simple Temporal Networks with Decisions. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{zavatteri_et_al:LIPIcs.TIME.2019.16,
author = {Zavatteri, Matteo and Combi, Carlo and Rizzi, Romeo and Vigan\`{o}, Luca},
title = {{Hybrid SAT-Based Consistency Checking Algorithms for Simple Temporal Networks with Decisions}},
booktitle = {26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
pages = {16:1--16:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-127-6},
ISSN = {1868-8969},
year = {2019},
volume = {147},
editor = {Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.16},
URN = {urn:nbn:de:0030-drops-113748},
doi = {10.4230/LIPIcs.TIME.2019.16},
annote = {Keywords: Simple temporal network with decisions, HSCC algorithms, incremental SAT-solving, disjunctive temporal network, KAPPA}
}
Document
Synthesis of LTL Formulas from Natural Language Texts: State of the Art and Research Directions
Abstract
Linear temporal logic (LTL) is commonly used in model checking tasks; moreover, it is well-suited for the formalization of technical requirements. However, the correct specification and interpretation of temporal logic formulas require a strong mathematical background and can hardly be done by domain experts, who, instead, tend to rely on a natural language description of the intended system behaviour. In such situations, a system that is able to automatically translate English sentences into LTL formulas, and vice versa, would be of great help. While the task of rendering an LTL formula into a more readable English sentence may be carried out in a relatively easy way by properly parsing the formula, the converse is still an open problem, due to the inherent difficulty of interpreting free, natural language texts. Although several partial solutions have been proposed in the past, the literature still lacks a critical assessment of the work done. We address such a shortcoming, presenting the current state of the art for what concerns the English-to-LTL translation problem, and outlining some possible research directions.
Cite as
Andrea Brunello, Angelo Montanari, and Mark Reynolds. Synthesis of LTL Formulas from Natural Language Texts: State of the Art and Research Directions. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 17:1-17:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{brunello_et_al:LIPIcs.TIME.2019.17,
author = {Brunello, Andrea and Montanari, Angelo and Reynolds, Mark},
title = {{Synthesis of LTL Formulas from Natural Language Texts: State of the Art and Research Directions}},
booktitle = {26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
pages = {17:1--17:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-127-6},
ISSN = {1868-8969},
year = {2019},
volume = {147},
editor = {Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.17},
URN = {urn:nbn:de:0030-drops-113756},
doi = {10.4230/LIPIcs.TIME.2019.17},
annote = {Keywords: Evolutionary algorithms, Machine learning, Natural language processing, Semantic parsing, Temporal logic}
}
Document
Complexity Analysis of a Unifying Algorithm for Model Checking Interval Temporal Logic
Abstract
The model-checking (MC) problem of Halpern and Shoham Interval Temporal Logic (HS) has been recently investigated in some papers and is known to be decidable. An intriguing open question concerns the exact complexity of the problem for full HS: it is at least EXPSPACE-hard, while the only known upper bound is non-elementary and is obtained by exploiting an abstract representation of Kripke structure paths called descriptors. In this paper we generalize the approach by providing a uniform framework for model-checking full HS and meaningful (almost maximal) fragments, where a specialized type of descriptor is defined for each fragment. We then devise a general MC alternating algorithm parameterized by the type of descriptor which has a polynomially bounded number of alternations and whose running time is bounded by the length of minimal representatives of descriptors (certificates). We analyze the time complexity of the algorithm and give, by non-trivial arguments, tight bounds on the length of certificates. For two types of descriptors, we obtain exponential upper and lower bounds which lead to an elementary MC algorithm for the related HS fragments. For the other types of descriptors, we provide non-elementary lower bounds. This last result addresses a question left open in some papers regarding the possibility of fixing an elementary upper bound on the size of the descriptors for full HS.
Cite as
Laura Bozzelli, Angelo Montanari, and Adriano Peron. Complexity Analysis of a Unifying Algorithm for Model Checking Interval Temporal Logic. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{bozzelli_et_al:LIPIcs.TIME.2019.18,
author = {Bozzelli, Laura and Montanari, Angelo and Peron, Adriano},
title = {{Complexity Analysis of a Unifying Algorithm for Model Checking Interval Temporal Logic}},
booktitle = {26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
pages = {18:1--18:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-127-6},
ISSN = {1868-8969},
year = {2019},
volume = {147},
editor = {Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.18},
URN = {urn:nbn:de:0030-drops-113768},
doi = {10.4230/LIPIcs.TIME.2019.18},
annote = {Keywords: Interval temporal logic, Model checking, Complexity and succinctness issues}
}
Document
Simplifying Inductive Schemes in Temporal Logic
Abstract
In propositional temporal logic, the combination of the connectives "tomorrow" and "always in the future" require the use of induction tools. In this paper, we present a classification of inductive schemes for propositional linear temporal logic that allows the detection of loops in decision procedures. In the design of automatic theorem provers, these schemes are responsible for the searching of efficient solutions for the detection and management of loops. We study which of these schemes have a good behavior in order to give a set of reduction rules that allow us to compute these schemes efficiently and, therefore, be able to eliminate these loops. These reduction laws can be applied previously and during the execution of any automatic theorem prover. All the reductions introduced in this paper can be considered a part of the process for obtaining a normal form of a given formula.
Cite as
Pablo Cordero, Inmaculada Fortes, Inmaculada P. de Guzmán, and Sixto Sánchez. Simplifying Inductive Schemes in Temporal Logic. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 19:1-19:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{cordero_et_al:LIPIcs.TIME.2019.19,
author = {Cordero, Pablo and Fortes, Inmaculada and de Guzm\'{a}n, Inmaculada P. and S\'{a}nchez, Sixto},
title = {{Simplifying Inductive Schemes in Temporal Logic}},
booktitle = {26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
pages = {19:1--19:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-127-6},
ISSN = {1868-8969},
year = {2019},
volume = {147},
editor = {Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.19},
URN = {urn:nbn:de:0030-drops-113773},
doi = {10.4230/LIPIcs.TIME.2019.19},
annote = {Keywords: Linear Temporal Logic, Inductive Schemes, Loop-check}
}
Document
On Verifying Timed Hyperproperties
Abstract
We study the satisfiability and model-checking problems for timed hyperproperties specified with HyperMTL, a timed extension of HyperLTL. Depending on whether interleaving of events in different traces is allowed, two possible semantics can be defined for timed hyperproperties: synchronous and asynchronous. While the satisfiability problem can be decided similarly as for HyperLTL regardless of the choice of semantics, we show that the model-checking problem for HyperMTL, unless the specification is alternation-free, is undecidable even when very restricted timing constraints are allowed. On the positive side, we show that model checking HyperMTL with quantifier alternations is possible under certain conditions in the synchronous semantics, or when there is a fixed bound on the length of the time domain.
Cite as
Hsi-Ming Ho, Ruoyu Zhou, and Timothy M. Jones. On Verifying Timed Hyperproperties. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
Copy BibTex To Clipboard
@InProceedings{ho_et_al:LIPIcs.TIME.2019.20,
author = {Ho, Hsi-Ming and Zhou, Ruoyu and Jones, Timothy M.},
title = {{On Verifying Timed Hyperproperties}},
booktitle = {26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
pages = {20:1--20:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-127-6},
ISSN = {1868-8969},
year = {2019},
volume = {147},
editor = {Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.20},
URN = {urn:nbn:de:0030-drops-113782},
doi = {10.4230/LIPIcs.TIME.2019.20},
annote = {Keywords: Timed Automata, Temporal Logics, Cybersecurity}
}