31 Search Results for "Bruse, Florian"

Volume

LIPIcs, Volume 278

30th International Symposium on Temporal Representation and Reasoning (TIME 2023)

TIME 2023, September 25-26, 2023, NCSR Demokritos, Athens, Greece

Editors: Alexander Artikis, Florian Bruse, and Luke Hunsberger

Document
DOI: 10.4230/LIPIcs.TIME.2024.16
Real-Time Higher-Order Recursion Schemes

Authors: Eric Alsmann and Florian Bruse

Published in: LIPIcs, Volume 318, 31st International Symposium on Temporal Representation and Reasoning (TIME 2024)

Abstract
Higher-Order Recursion Schemes (HORS) have long been studied as a tool to model functional programs. Model-checking the tree generated by a HORS of order k against a parity automaton is known to be k-EXPTIME-complete. This paper introduces timed HORS, a real-time version of HORS in the sense of Alur/Dill'90, to be model-checked against a pair of a parity automaton and a timed automaton. We show that adding dense linear time to the notion of recursion schemes adds one exponential to the cost of model-checking, i.e., model-checking a timed HORS of order k can be done in (k+1)-EXPTIME. This is shown by an adaption of the region-graph construction known from the model-checking of timed CTL. We also obtain a hardness result for k = 1, but we strongly conjecture that it holds for all k. This result is obtained by encoding runs of 2-EXPTIME Turing machines into the trees generated by timed HORS.
Cite as

Eric Alsmann and Florian Bruse. Real-Time Higher-Order Recursion Schemes. In 31st International Symposium on Temporal Representation and Reasoning (TIME 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 318, pp. 16:1-16:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{alsmann_et_al:LIPIcs.TIME.2024.16,
  author =	{Alsmann, Eric and Bruse, Florian},
  title =	{{Real-Time Higher-Order Recursion Schemes}},
  booktitle =	{31st International Symposium on Temporal Representation and Reasoning (TIME 2024)},
  pages =	{16:1--16:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-349-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{318},
  editor =	{Sala, Pietro and Sioutis, Michael and Wang, Fusheng},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2024.16},
  URN =		{urn:nbn:de:0030-drops-212236},
  doi =		{10.4230/LIPIcs.TIME.2024.16},
  annote =	{Keywords: Timed Automata, Higher-Order Recursion Schemes, Tree Automata}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.TIME.2023
LIPIcs, Volume 278, TIME 2023, Complete Volume

Authors: Alexander Artikis, Florian Bruse, and Luke Hunsberger

Published in: LIPIcs, Volume 278, 30th International Symposium on Temporal Representation and Reasoning (TIME 2023)

Abstract
LIPIcs, Volume 278, TIME 2023, Complete Volume
Cite as

30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 1-254, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Proceedings{artikis_et_al:LIPIcs.TIME.2023,
  title =	{{LIPIcs, Volume 278, TIME 2023, Complete Volume}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{1--254},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-298-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{278},
  editor =	{Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023},
  URN =		{urn:nbn:de:0030-drops-190890},
  doi =		{10.4230/LIPIcs.TIME.2023},
  annote =	{Keywords: LIPIcs, Volume 278, TIME 2023, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.TIME.2023.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Alexander Artikis, Florian Bruse, and Luke Hunsberger

Published in: LIPIcs, Volume 278, 30th International Symposium on Temporal Representation and Reasoning (TIME 2023)

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

30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{artikis_et_al:LIPIcs.TIME.2023.0,
  author =	{Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{0:i--0:xiv},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-298-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{278},
  editor =	{Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.0},
  URN =		{urn:nbn:de:0030-drops-190907},
  doi =		{10.4230/LIPIcs.TIME.2023.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.TIME.2023.1
Learning Temporal Logic Formulas from Time-Series Data (Invited Talk)

Authors: Laura Nenzi

Published in: LIPIcs, Volume 278, 30th International Symposium on Temporal Representation and Reasoning (TIME 2023)

Abstract
In this talk, we provide an overview of recent advancements in the field of mining formal specifications from time-series data, with a specific focus on learning Signal Temporal Logic (STL) formulae.
Cite as

Laura Nenzi. Learning Temporal Logic Formulas from Time-Series Data (Invited Talk). In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{nenzi:LIPIcs.TIME.2023.1,
  author =	{Nenzi, Laura},
  title =	{{Learning Temporal Logic Formulas from Time-Series Data}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{1:1--1:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-298-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{278},
  editor =	{Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.1},
  URN =		{urn:nbn:de:0030-drops-190917},
  doi =		{10.4230/LIPIcs.TIME.2023.1},
  annote =	{Keywords: Temporal Logic, Mining Specifications}
}
Document
DOI: 10.4230/LIPIcs.TIME.2023.2
LTL over Finite Words Can Be Exponentially More Succinct Than Pure-Past LTL, and vice versa

Authors: Alessandro Artale, Luca Geatti, Nicola Gigante, Andrea Mazzullo, and Angelo Montanari

Published in: LIPIcs, Volume 278, 30th International Symposium on Temporal Representation and Reasoning (TIME 2023)

Abstract
Linear Temporal Logic over finite traces (LTL_𝖿) has proved itself to be an important and effective formalism in formal verification as well as in artificial intelligence. Pure past LTL_𝖿 (pLTL) is the logic obtained from LTL_𝖿 by replacing each (future) temporal operator by a corresponding past one, and is naturally interpreted at the end of a finite trace. It is known that each property definable in LTL_𝖿 is also definable in pLTL, and ǐceversa. However, despite being extensively used in practice, to the best of our knowledge, there is no systematic study of their succinctness. In this paper, we investigate the succinctness of LTL_𝖿 and pLTL. First, we prove that pLTL can be exponentially more succinct than LTL_𝖿 by showing that there exists a property definable with a pLTL formula of size n such that the size of all LTL_𝖿 formulas defining it is at least exponential in n. Then, we prove that LTL_𝖿 can be exponentially more succinct than pLTL as well. This result shows that, although being expressively equivalent, LTL_𝖿 and pLTL are incomparable when succinctness is concerned. In addition, we study the succinctness of Safety-LTL (the syntactic safety fragment of LTL over infinite traces) with respect to its canonical form G(pLTL), whose formulas are of the form G(α), G being the globally operator and α a pLTL formula. We prove that G(pLTL) can be exponentially more succinct than Safety-LTL, and that the same holds for the dual cosafety fragment.
Cite as

Alessandro Artale, Luca Geatti, Nicola Gigante, Andrea Mazzullo, and Angelo Montanari. LTL over Finite Words Can Be Exponentially More Succinct Than Pure-Past LTL, and vice versa. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 2:1-2:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{artale_et_al:LIPIcs.TIME.2023.2,
  author =	{Artale, Alessandro and Geatti, Luca and Gigante, Nicola and Mazzullo, Andrea and Montanari, Angelo},
  title =	{{LTL over Finite Words Can Be Exponentially More Succinct Than Pure-Past LTL, and vice versa}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{2:1--2:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-298-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{278},
  editor =	{Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.2},
  URN =		{urn:nbn:de:0030-drops-190927},
  doi =		{10.4230/LIPIcs.TIME.2023.2},
  annote =	{Keywords: Temporal Logic, Succinctness, LTLf, Finite Traces, Pure past LTL}
}
Document
DOI: 10.4230/LIPIcs.TIME.2023.3
LSCPM: Communities in Massive Real-World Link Streams by Clique Percolation Method

Authors: Alexis Baudin, Lionel Tabourier, and Clémence Magnien

Published in: LIPIcs, Volume 278, 30th International Symposium on Temporal Representation and Reasoning (TIME 2023)

Abstract
Community detection is a popular approach to understand the organization of interactions in static networks. For that purpose, the Clique Percolation Method (CPM), which involves the percolation of k-cliques, is a well-studied technique that offers several advantages. Besides, studying interactions that occur over time is useful in various contexts, which can be modeled by the link stream formalism. The Dynamic Clique Percolation Method (DCPM) has been proposed for extending CPM to temporal networks. However, existing implementations are unable to handle massive datasets. We present a novel algorithm that adapts CPM to link streams, which has the advantage that it allows us to speed up the computation time with respect to the existing DCPM method. We evaluate it experimentally on real datasets and show that it scales to massive link streams. For example, it allows to obtain a complete set of communities in under twenty-five minutes for a dataset with thirty million links, what the state of the art fails to achieve even after a week of computation. We further show that our method provides communities similar to DCPM, but slightly more aggregated. We exhibit the relevance of the obtained communities in real world cases, and show that they provide information on the importance of vertices in the link streams.
Cite as

Alexis Baudin, Lionel Tabourier, and Clémence Magnien. LSCPM: Communities in Massive Real-World Link Streams by Clique Percolation Method. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 3:1-3:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{baudin_et_al:LIPIcs.TIME.2023.3,
  author =	{Baudin, Alexis and Tabourier, Lionel and Magnien, Cl\'{e}mence},
  title =	{{LSCPM: Communities in Massive Real-World Link Streams by Clique Percolation Method}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{3:1--3:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-298-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{278},
  editor =	{Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.3},
  URN =		{urn:nbn:de:0030-drops-190932},
  doi =		{10.4230/LIPIcs.TIME.2023.3},
  annote =	{Keywords: Temporal network, Link stream, k-clique, Community detection, Clique Percolation Method, Real-world interactions}
}
Document
DOI: 10.4230/LIPIcs.TIME.2023.4
Discovering Predictive Dependencies on Multi-Temporal Relations

Authors: Beatrice Amico, Carlo Combi, Romeo Rizzi, and Pietro Sala

Published in: LIPIcs, Volume 278, 30th International Symposium on Temporal Representation and Reasoning (TIME 2023)

Abstract
In this paper, we propose a methodology for deriving a new kind of approximate temporal functional dependencies, called Approximate Predictive Functional Dependencies (APFDs), based on a three-window framework and on a multi-temporal relational model. Different features are proposed for the Observation Window (OW), where we observe predictive data, for the Waiting Window (WW), and for the Prediction Window (PW), where the predicted event occurs. We then discuss the concept of approximation for such APFDs, introduce two new error measures. We prove that the problem of deriving APFDs is intractable. Moreover, we discuss some preliminary results in deriving APFDs from real clinical data using MIMIC III dataset, related to patients from Intensive Care Units.
Cite as

Beatrice Amico, Carlo Combi, Romeo Rizzi, and Pietro Sala. Discovering Predictive Dependencies on Multi-Temporal Relations. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{amico_et_al:LIPIcs.TIME.2023.4,
  author =	{Amico, Beatrice and Combi, Carlo and Rizzi, Romeo and Sala, Pietro},
  title =	{{Discovering Predictive Dependencies on Multi-Temporal Relations}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{4:1--4:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-298-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{278},
  editor =	{Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.4},
  URN =		{urn:nbn:de:0030-drops-190945},
  doi =		{10.4230/LIPIcs.TIME.2023.4},
  annote =	{Keywords: temporal databases, temporal data mining, functional dependencies}
}
Document
DOI: 10.4230/LIPIcs.TIME.2023.5
Prime Scenarios in Qualitative Spatial and Temporal Reasoning

Authors: Yakoub Salhi and Michael Sioutis

Published in: LIPIcs, Volume 278, 30th International Symposium on Temporal Representation and Reasoning (TIME 2023)

Abstract
The concept of prime implicant is a fundamental tool in Boolean algebra, which is used in Boolean circuit design and, recently, in explainable AI. This study investigates an analogous concept in qualitative spatial and temporal reasoning, called prime scenario. Specifically, we define a prime scenario of a qualitative constraint network (QCN) as a minimal set of decisions that can uniquely determine solutions of this QCN. We propose in this paper a collection of algorithms designed to address various problems related to prime scenarios. The first three algorithms aim to generate a prime scenario from a scenario of a QCN. The main idea consists in using path consistency to identify the constraints that can be ignored to generate a prime scenario. The next two algorithms focus on generating a set of prime scenarios that cover all the scenarios of the original QCN: The first algorithm examines every branch of the search tree, while the second is based on the use of a SAT encoding. Our last algorithm is concerned with computing a minimum-size prime scenario by using a MaxSAT encoding built from countermodels of the original QCN. We show that this algorithm is particularly useful for measuring the robustness of a QCN. Finally, a preliminary experimental evaluation is performed with instances of Allen’s Interval Algebra to assess the efficiency of our algorithms and, hence, also the difficulty of the newly introduced problems here.
Cite as

Yakoub Salhi and Michael Sioutis. Prime Scenarios in Qualitative Spatial and Temporal Reasoning. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 5:1-5:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{salhi_et_al:LIPIcs.TIME.2023.5,
  author =	{Salhi, Yakoub and Sioutis, Michael},
  title =	{{Prime Scenarios in Qualitative Spatial and Temporal Reasoning}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{5:1--5:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-298-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{278},
  editor =	{Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.5},
  URN =		{urn:nbn:de:0030-drops-190957},
  doi =		{10.4230/LIPIcs.TIME.2023.5},
  annote =	{Keywords: Spatial and Temporal Reasoning, Qualitative Constraints, Prime Scenario, Prime Implicant, Robustness Measurement}
}
Document
DOI: 10.4230/LIPIcs.TIME.2023.6
Bounded-Memory Runtime Enforcement of Timed Properties

Authors: Saumya Shankar, Srinivas Pinisetty, and Thierry Jéron

Published in: LIPIcs, Volume 278, 30th International Symposium on Temporal Representation and Reasoning (TIME 2023)

Abstract
Runtime Enforcement (RE) is a monitoring technique aimed at correcting possibly incorrect executions w.r.t. a set of formal requirements (properties) of a system. In this paper, we consider enforcement monitoring of real-time properties. Thus, executions are modelled as timed words and specifications as timed automata. Moreover, we consider that the enforcer has the ability to delay events by storing or buffering them into its internal memory (and releasing them when the property is finally satisfied) and suppressing events when no delaying is appropriate. Practically, in an implementation, the internal memory of the enforcer is finite. In this paper, we propose a new RE paradigm for timed properties, where the memory of the enforcer is bounded/finite, to address practical applications with memory constraints and timed specifications. Bounding the memory presents a number of difficulties, e.g., how to accommodate a timed event into the memory when the memory is full, s.t., regardless of the course of action we choose to handle this situation, the behaviour of the bounded enforcer should not significantly differ from that of the unbounded enforcer. The problem of how to optimally discard events when the buffer is full is significantly more difficult in a timed environment where the progress of time affects the satisfaction or violation of a property. We define the bounded-memory RE problem for timed properties and develop a framework for regular timed properties specified as timed automata. The proposed framework is implemented in Python, and its performance is evaluated. From experiments, we discovered that the enforcer has a reasonable execution time overhead.
Cite as

Saumya Shankar, Srinivas Pinisetty, and Thierry Jéron. Bounded-Memory Runtime Enforcement of Timed Properties. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 6:1-6:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{shankar_et_al:LIPIcs.TIME.2023.6,
  author =	{Shankar, Saumya and Pinisetty, Srinivas and J\'{e}ron, Thierry},
  title =	{{Bounded-Memory Runtime Enforcement of Timed Properties}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{6:1--6:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-298-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{278},
  editor =	{Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.6},
  URN =		{urn:nbn:de:0030-drops-190962},
  doi =		{10.4230/LIPIcs.TIME.2023.6},
  annote =	{Keywords: Formal methods, Runtime enforcement, Bounded-memory, Timed automata}
}
Document
DOI: 10.4230/LIPIcs.TIME.2023.7
More Than 0s and 1s: Metric Quantifiers and Counting over Timed Words

Authors: Hsi-Ming Ho and Khushraj Madnani

Published in: LIPIcs, Volume 278, 30th International Symposium on Temporal Representation and Reasoning (TIME 2023)

Abstract
We study the expressiveness of the pointwise interpretations (i.e. over timed words) of some predicate and temporal logics with metric and counting features. We show that counting in the unit interval (0, 1) is strictly weaker than counting in (0, b) with arbitrary b ≥ 0; moreover, allowing the latter indeed leads to expressive completeness for the metric predicate logic Q2MLO, recovering the corresponding result for the continuous interpretations (i.e. over signals). Exploiting this connection, we show that in contrast to the continuous case, adding "punctual" predicates into Q2MLO is still insufficient for the full expressive power of the Monadic First-Order Logic of Order and Metric (FO[<,+1]). Finally, we propose a generalisation of the recently proposed Pnueli automata modalities and show that the resulting metric temporal logic is expressively complete for FO[<,+1].
Cite as

Hsi-Ming Ho and Khushraj Madnani. More Than 0s and 1s: Metric Quantifiers and Counting over Timed Words. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 7:1-7:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{ho_et_al:LIPIcs.TIME.2023.7,
  author =	{Ho, Hsi-Ming and Madnani, Khushraj},
  title =	{{More Than 0s and 1s: Metric Quantifiers and Counting over Timed Words}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{7:1--7:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-298-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{278},
  editor =	{Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.7},
  URN =		{urn:nbn:de:0030-drops-190979},
  doi =		{10.4230/LIPIcs.TIME.2023.7},
  annote =	{Keywords: Temporal Logic, Expressiveness, Automata}
}
Document
DOI: 10.4230/LIPIcs.TIME.2023.8
Analyzing Complex Systems with Cascades Using Continuous-Time Bayesian Networks

Authors: Alessandro Bregoli, Karin Rathsman, Marco Scutari, Fabio Stella, and Søren Wengel Mogensen

Published in: LIPIcs, Volume 278, 30th International Symposium on Temporal Representation and Reasoning (TIME 2023)

Abstract
Interacting systems of events may exhibit cascading behavior where events tend to be temporally clustered. While the cascades themselves may be obvious from the data, it is important to understand which states of the system trigger them. For this purpose, we propose a modeling framework based on continuous-time Bayesian networks (CTBNs) to analyze cascading behavior in complex systems. This framework allows us to describe how events propagate through the system and to identify likely sentry states, that is, system states that may lead to imminent cascading behavior. Moreover, CTBNs have a simple graphical representation and provide interpretable outputs, both of which are important when communicating with domain experts. We also develop new methods for knowledge extraction from CTBNs and we apply the proposed methodology to a data set of alarms in a large industrial system.
Cite as

Alessandro Bregoli, Karin Rathsman, Marco Scutari, Fabio Stella, and Søren Wengel Mogensen. Analyzing Complex Systems with Cascades Using Continuous-Time Bayesian Networks. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 8:1-8:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{bregoli_et_al:LIPIcs.TIME.2023.8,
  author =	{Bregoli, Alessandro and Rathsman, Karin and Scutari, Marco and Stella, Fabio and Mogensen, S{\o}ren Wengel},
  title =	{{Analyzing Complex Systems with Cascades Using Continuous-Time Bayesian Networks}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{8:1--8:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-298-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{278},
  editor =	{Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.8},
  URN =		{urn:nbn:de:0030-drops-190980},
  doi =		{10.4230/LIPIcs.TIME.2023.8},
  annote =	{Keywords: event model, continuous-time Bayesian network, alarm network, graphical models, event cascade}
}
Document
DOI: 10.4230/LIPIcs.TIME.2023.9
A Sound and Complete Tableau System for Fuzzy Halpern and Shoham’s Interval Temporal Logic

Authors: Willem Conradie, Riccardo Monego, Emilio Muñoz-Velasco, Guido Sciavicco, and Ionel Eduard Stan

Published in: LIPIcs, Volume 278, 30th International Symposium on Temporal Representation and Reasoning (TIME 2023)

Abstract
Interval temporal logic plays a critical role in various applications, including planning, scheduling, and formal verification; recently, interval temporal logic has also been successfully applied to learning from temporal data. Halpern and Shoham’s interval temporal logic, in particular, stands out as a very intuitive, yet expressive, interval-based formalism. To address real-world scenarios involving uncertainty and imprecision, Halpern and Shoham’s logic has been recently generalized to the fuzzy (many-valued) case. The resulting language capitalizes on many-valued modal logics, allowing for a range of truth values that reflect multiple expert perspectives, but inherits the bad computational behaviour of its crisp counterpart. In this work, we investigate a sound and complete tableau system for fuzzy Halpern and Shoham’s logic, which, although possibly non-terminating, offers a semi-decision procedure for the finite case.
Cite as

Willem Conradie, Riccardo Monego, Emilio Muñoz-Velasco, Guido Sciavicco, and Ionel Eduard Stan. A Sound and Complete Tableau System for Fuzzy Halpern and Shoham’s Interval Temporal Logic. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 9:1-9:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{conradie_et_al:LIPIcs.TIME.2023.9,
  author =	{Conradie, Willem and Monego, Riccardo and Mu\~{n}oz-Velasco, Emilio and Sciavicco, Guido and Stan, Ionel Eduard},
  title =	{{A Sound and Complete Tableau System for Fuzzy Halpern and Shoham’s Interval Temporal Logic}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{9:1--9:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-298-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{278},
  editor =	{Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.9},
  URN =		{urn:nbn:de:0030-drops-190996},
  doi =		{10.4230/LIPIcs.TIME.2023.9},
  annote =	{Keywords: Interval temporal logic, many-valued logic, tableau system}
}
Document
DOI: 10.4230/LIPIcs.TIME.2023.10
The Calculus of Temporal Influence

Authors: Florian Bruse, Marit Kastaun, Martin Lange, and Sören Möller

Published in: LIPIcs, Volume 278, 30th International Symposium on Temporal Representation and Reasoning (TIME 2023)

Abstract
We present the Calculus of Temporal Influence, a simple logical calculus that allows reasoning about the behaviour of real-valued functions over time by making assertions that bound their values or the values of their derivatives. The motivation for the design of such a proof system comes from the need to provide the background computational machinery for tools that support learning in experimental subjects in secondary-education classrooms. The end goal is a tool that allows school pupils to formalise hypotheses about phenomena in natural sciences, such that their validity with respect to some formal experiment model can be checked automatically. The Calculus of Temporal Influence provides a language for formal statements and the mechanisms for reasoning about valid logical consequences. It extends (and deviates in parts from) previous work introducing the Calculus of (Non-Temporal) Influence by integrating the ability to model temporal effects in such experiments. We show that reasoning in the calculus is sound with respect to a natural formal semantics, that logical consequence is at least semi-decidable, and that one obtains polynomial-time decidability for a natural stratification of the problem.
Cite as

Florian Bruse, Marit Kastaun, Martin Lange, and Sören Möller. The Calculus of Temporal Influence. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{bruse_et_al:LIPIcs.TIME.2023.10,
  author =	{Bruse, Florian and Kastaun, Marit and Lange, Martin and M\"{o}ller, S\"{o}ren},
  title =	{{The Calculus of Temporal Influence}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{10:1--10:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-298-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{278},
  editor =	{Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.10},
  URN =		{urn:nbn:de:0030-drops-191009},
  doi =		{10.4230/LIPIcs.TIME.2023.10},
  annote =	{Keywords: temporal reasoning, formal models, continuous functions, polynomial decidability}
}
Document
DOI: 10.4230/LIPIcs.TIME.2023.11
Detecting Causality in the Presence of Byzantine Processes: The Synchronous Systems Case

Authors: Anshuman Misra and Ajay D. Kshemkalyani

Published in: LIPIcs, Volume 278, 30th International Symposium on Temporal Representation and Reasoning (TIME 2023)

Abstract
Detecting causality or the happens before relation between events in a distributed system is a fundamental building block for distributed applications. It was recently proved that this problem cannot be solved in an asynchronous distributed system in the presence of Byzantine processes, irrespective of whether the communication mechanism is via unicasts, multicasts, or broadcasts. In light of this impossibility result, we turn attention to synchronous systems and examine the possibility of solving the causality detection problem in such systems. In this paper, we prove that causality detection between events can be solved in the presence of Byzantine processes in a synchronous distributed system. The positive result holds for unicast, multicast, as well as broadcast modes of communication. We prove the result by providing an algorithm. Our solution uses the Replicated State Machine (RSM) approach and vector clocks.
Cite as

Anshuman Misra and Ajay D. Kshemkalyani. Detecting Causality in the Presence of Byzantine Processes: The Synchronous Systems Case. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 11:1-11:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{misra_et_al:LIPIcs.TIME.2023.11,
  author =	{Misra, Anshuman and Kshemkalyani, Ajay D.},
  title =	{{Detecting Causality in the Presence of Byzantine Processes: The Synchronous Systems Case}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{11:1--11:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-298-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{278},
  editor =	{Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.11},
  URN =		{urn:nbn:de:0030-drops-191017},
  doi =		{10.4230/LIPIcs.TIME.2023.11},
  annote =	{Keywords: Byzantine fault-tolerance, causality, happens before, distributed system, message-passing, synchronous system}
}
  • Refine by Author
  • 9 Bruse, Florian
  • 6 Lange, Martin
  • 3 Geatti, Luca
  • 3 Gigante, Nicola
  • 3 Hunsberger, Luke
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 5 temporal logic
  • 4 formal specification
  • 3 Qualitative Constraints
  • 3 Spatial and Temporal Reasoning
  • 3 Temporal Logic
  • Show More...

  • Refine by Type
  • 30 document
  • 1 volume

  • Refine by Publication Year
  • 25 2023
  • 3 2021
  • 1 2020
  • 1 2022
  • 1 2024

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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