24 Search Results for "Gamper, Johann"

Volume

LIPIcs, Volume 147

26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

TIME 2019, October 16-19, 2019, Málaga, Spain

Editors: Johann Gamper, Sophie Pinchinat, and Guido Sciavicco

Document
Complete Volume
DOI: 10.4230/LIPIcs.TIME.2019
LIPIcs, Volume 147, TIME'19, Complete Volume

Authors: Johann Gamper, Sophie Pinchinat, and Guido Sciavicco

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

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.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
DOI: 10.4230/LIPIcs.TIME.2019.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Johann Gamper, Sophie Pinchinat, and Guido Sciavicco

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

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.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
DOI: 10.4230/LIPIcs.TIME.2019.1
Computing the Fourier Transformation over Temporal Data Streams (Invited Talk)

Authors: Michael H. Böhlen and Muhammad Saad

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

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.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
DOI: 10.4230/LIPIcs.TIME.2019.2
From Unstructured Data to Narrative Abstractive Summaries (Invited Talk)

Authors: Estela Saquete Boró

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

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.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
DOI: 10.4230/LIPIcs.TIME.2019.3
On the Computation of Nash Equilibria in Games on Graphs (Invited Talk)

Authors: Patricia Bouyer

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

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.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
DOI: 10.4230/LIPIcs.TIME.2019.4
A Modal Logic for Subject-Oriented Spatial Reasoning

Authors: Przemysław Andrzej Wałęga and Michał Zawidzki

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

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.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
DOI: 10.4230/LIPIcs.TIME.2019.5
Customizing BPMN Diagrams Using Timelines

Authors: Carlo Combi, Barbara Oliboni, and Pietro Sala

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

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.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
DOI: 10.4230/LIPIcs.TIME.2019.6
The Second Order Traffic Fine: Temporal Reasoning in European Transport Regulations

Authors: Ana de Almeida Borges, Juan José Conejero Rodríguez, David Fernández-Duque, Mireia González Bedmar, and Joost J. Joosten

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

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.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
DOI: 10.4230/LIPIcs.TIME.2019.7
Two-Dimensional Rule Language for Querying Sensor Log Data: A Framework and Use Cases

Authors: Sebastian Brandt, Diego Calvanese, Elem Güzel Kalaycı, Roman Kontchakov, Benjamin Mörzinger, Vladislav Ryzhikov, Guohui Xiao, and Michael Zakharyaschev

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

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.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
DOI: 10.4230/LIPIcs.TIME.2019.8
Time-Aware Probabilistic Knowledge Graphs

Authors: Melisachew Wudage Chekol and Heiner Stuckenschmidt

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

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.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
DOI: 10.4230/LIPIcs.TIME.2019.9
Qualitative Reasoning and Data Mining

Authors: Yakoub Salhi

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

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.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
DOI: 10.4230/LIPIcs.TIME.2019.10
Recurrent Neural Networks Applied to GNSS Time Series for Denoising and Prediction

Authors: Elena Loli Piccolomini, Stefano Gandolfi, Luca Poluzzi, Luca Tavasci, Pasquale Cascarano, and Andrea Pascucci

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

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.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
DOI: 10.4230/LIPIcs.TIME.2019.11
From Quantified CTL to QBF

Authors: Akash Hossain and François Laroussinie

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

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.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
DOI: 10.4230/LIPIcs.TIME.2019.12
Towards Certified Model Checking for PLTL Using One-Pass Tableaux

Authors: Alex Abuin, Alexander Bolotov, Unai Díaz de Cerio, Montserrat Hermo, and Paqui Lucio

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

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.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}
}
  • Refine by Author
  • 3 Gamper, Johann
  • 2 Böhlen, Michael H.
  • 2 Combi, Carlo
  • 2 Montanari, Angelo
  • 2 Pinchinat, Sophie
  • Show More...

  • Refine by Classification
  • 7 Theory of computation → Modal and temporal logics
  • 6 Computing methodologies → Temporal reasoning
  • 3 Computing methodologies → Knowledge representation and reasoning
  • 3 Information systems → Temporal data
  • 3 Theory of computation → Logic
  • Show More...

  • Refine by Keyword
  • 2 Temporal logic
  • 1 Abstractive summarization
  • 1 BPMN
  • 1 Bounded Domain Property
  • 1 Business Processes
  • Show More...

  • Refine by Type
  • 23 document
  • 1 volume

  • Refine by Publication Year
  • 23 2019
  • 1 2018

© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact