LIPIcs, Volume 318

31st International Symposium on Temporal Representation and Reasoning (TIME 2024)



Thumbnail PDF

Event

TIME 2024, October 28-30, 2024, Montpellier, France

Editors

Pietro Sala
  • University of Verona, Italy
Michael Sioutis
  • LIRMM UMR 5506, Université de Montpellier & CNRS, France
Fusheng Wang
  • Stony Brook University, NY, USA

Publication Details

  • published at: 2024-10-22
  • Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
  • ISBN: 978-3-95977-349-2

Access Numbers

Documents

No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 318, TIME 2024, Complete Volume

Authors: Pietro Sala, Michael Sioutis, and Fusheng Wang


Abstract
LIPIcs, Volume 318, TIME 2024, Complete Volume

Cite as

31st International Symposium on Temporal Representation and Reasoning (TIME 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 318, pp. 1-308, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@Proceedings{sala_et_al:LIPIcs.TIME.2024,
  title =	{{LIPIcs, Volume 318, TIME 2024, Complete Volume}},
  booktitle =	{31st International Symposium on Temporal Representation and Reasoning (TIME 2024)},
  pages =	{1--308},
  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},
  URN =		{urn:nbn:de:0030-drops-220682},
  doi =		{10.4230/LIPIcs.TIME.2024},
  annote =	{Keywords: LIPIcs, Volume 318, TIME 2024, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Pietro Sala, Michael Sioutis, and Fusheng Wang


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

Cite as

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


Copy BibTex To Clipboard

@InProceedings{sala_et_al:LIPIcs.TIME.2024.0,
  author =	{Sala, Pietro and Sioutis, Michael and Wang, Fusheng},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{31st International Symposium on Temporal Representation and Reasoning (TIME 2024)},
  pages =	{0:i--0:xiv},
  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.0},
  URN =		{urn:nbn:de:0030-drops-220672},
  doi =		{10.4230/LIPIcs.TIME.2024.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
A General Logical Approach to Learning from Time Series (Invited Talk)

Authors: Guido Sciavicco


Abstract
Machine learning from multivariate time series is a common task, and countless different approaches to typical learning problems have been proposed in recent years. In this talk, we review some basic ideas towards logic-based learning methods, and we sketch a general framework.

Cite as

Guido Sciavicco. A General Logical Approach to Learning from Time Series (Invited Talk). In 31st International Symposium on Temporal Representation and Reasoning (TIME 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 318, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{sciavicco:LIPIcs.TIME.2024.1,
  author =	{Sciavicco, Guido},
  title =	{{A General Logical Approach to Learning from Time Series}},
  booktitle =	{31st International Symposium on Temporal Representation and Reasoning (TIME 2024)},
  pages =	{1:1--1:2},
  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.1},
  URN =		{urn:nbn:de:0030-drops-212088},
  doi =		{10.4230/LIPIcs.TIME.2024.1},
  annote =	{Keywords: Machine learning, temporal logic, general approach}
}
Document
Invited Talk
Strategic Reasoning Under Imperfect Information with Synchronous Semantics (Invited Talk)

Authors: Sophie Pinchinat


Abstract
Dynamic Epistemic Logic is a modal logic dedicated to specifying epistemic property changes along the dynamic behavior of a multi-agent system. The models that underlie this logic are (epistemic) states together with transitions caused by events, the occurrence of which may modify the current state. We first develop a setting where the entire dynamics of the system starting from an initial state is captured by a single infinite tree, in a way similar to what has been considered for Epistemic Temporal Logic, and second go through the current state-of-the-art regarding strategic reasoning, with a focus on planning problems in this infinite structure.

Cite as

Sophie Pinchinat. Strategic Reasoning Under Imperfect Information with Synchronous Semantics (Invited Talk). In 31st International Symposium on Temporal Representation and Reasoning (TIME 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 318, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{pinchinat:LIPIcs.TIME.2024.2,
  author =	{Pinchinat, Sophie},
  title =	{{Strategic Reasoning Under Imperfect Information with Synchronous Semantics}},
  booktitle =	{31st International Symposium on Temporal Representation and Reasoning (TIME 2024)},
  pages =	{2:1--2:2},
  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.2},
  URN =		{urn:nbn:de:0030-drops-212093},
  doi =		{10.4230/LIPIcs.TIME.2024.2},
  annote =	{Keywords: Strategic reasoning, Imperfect information, chain-MSO, Automatic structures}
}
Document
Invited Talk
Rule-Based Temporal Reasoning: Exploring DatalogMTL (Invited Talk)

Authors: Przemysław Andrzej Wałęga


Abstract
I will introduce DatalogMTL - an extension of Datalog, augmenting it with operators known from metric temporal logic (MTL). DatalogMTL is an expressive language which allows us for complex temporal reasoning over a dense timeline and, at the same time, remains decidable. I will provide an overview of research on DatalogMTL by discussing its computational complexity, syntactic and semantic modifications, practical reasoning approaches, applications, and future research directions.

Cite as

Przemysław Andrzej Wałęga. Rule-Based Temporal Reasoning: Exploring DatalogMTL (Invited Talk). In 31st International Symposium on Temporal Representation and Reasoning (TIME 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 318, pp. 3:1-3:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{walega:LIPIcs.TIME.2024.3,
  author =	{Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
  title =	{{Rule-Based Temporal Reasoning: Exploring DatalogMTL}},
  booktitle =	{31st International Symposium on Temporal Representation and Reasoning (TIME 2024)},
  pages =	{3:1--3:3},
  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.3},
  URN =		{urn:nbn:de:0030-drops-212106},
  doi =		{10.4230/LIPIcs.TIME.2024.3},
  annote =	{Keywords: Temporal Datalog, Temporal Logic Programming, Temporal Reasoning}
}
Document
Agile Controllability of Simple Temporal Networks with Uncertainty and Oracles

Authors: Johann Eder, Roberto Posenato, Carlo Combi, Marco Franceschetti, and Franziska S. Hollauf


Abstract
Simple temporal networks with uncertainty (STNUs) have achieved wide attention and are the basis of many applications requiring the representation of temporal constraints and checking whether they are conflicting. Dynamic controllability is currently the most relaxed notion to check whether a system can be controlled without violating temporal constraints despite uncertainties. However, dynamic controllability assumes that the actual duration of a contingent activity is only known when the end event of this activity takes place. The recently introduced notion of agile controllability considers when this duration is known earlier, leading to a more relaxed notion of temporal feasibility. We extend the definition of STNUs to STNUOs (Simple Temporal Networks with Uncertainty and Oracles) to represent the point in time at which information about a contingent duration is available. We formally define agile controllability as a generalization of dynamic controllability considering the timepoints of information availability. We propose a set of constraint propagation rules for STNUOs leading to an algorithm for checking agile controllability.

Cite as

Johann Eder, Roberto Posenato, Carlo Combi, Marco Franceschetti, and Franziska S. Hollauf. Agile Controllability of Simple Temporal Networks with Uncertainty and Oracles. In 31st International Symposium on Temporal Representation and Reasoning (TIME 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 318, pp. 4:1-4:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{eder_et_al:LIPIcs.TIME.2024.4,
  author =	{Eder, Johann and Posenato, Roberto and Combi, Carlo and Franceschetti, Marco and Hollauf, Franziska S.},
  title =	{{Agile Controllability of Simple Temporal Networks with Uncertainty and Oracles}},
  booktitle =	{31st International Symposium on Temporal Representation and Reasoning (TIME 2024)},
  pages =	{4:1--4:16},
  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.4},
  URN =		{urn:nbn:de:0030-drops-212115},
  doi =		{10.4230/LIPIcs.TIME.2024.4},
  annote =	{Keywords: Temporal constraint networks, contingent durations, agile controllability}
}
Document
Open the Chests: An Environment for Activity Recognition and Sequential Decision Problems Using Temporal Logic

Authors: Ivelina Stoyanova, Nicolas Museux, Sao Mai Nguyen, and David Filliat


Abstract
This article presents Open the Chests, a novel benchmark environment designed for simulating and testing activity recognition and reactive decision-making algorithms. By leveraging temporal logic, Open the Chests offers a dynamic, event-driven simulation platform that illustrates the complexities of real-world systems. The environment contains multiple chests, each representing an activity pattern that an interacting agent must identify and respond to by pressing a corresponding button. The agent must analyze sequences of asynchronous events generated by the environment to recognize these patterns and make informed decisions. With the aim of theoretically grounding the environment, the Activity-Based Markov Decision Process (AB-MDP) is defined, allowing to model the context-dependent interaction with activities. Our goal is to propose a robust tool for the development, testing, and bench-marking of algorithms that is illustrative of realistic scenarios and allows for the isolation of specific complexities in event-driven environments.

Cite as

Ivelina Stoyanova, Nicolas Museux, Sao Mai Nguyen, and David Filliat. Open the Chests: An Environment for Activity Recognition and Sequential Decision Problems Using Temporal Logic. In 31st International Symposium on Temporal Representation and Reasoning (TIME 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 318, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{stoyanova_et_al:LIPIcs.TIME.2024.5,
  author =	{Stoyanova, Ivelina and Museux, Nicolas and Nguyen, Sao Mai and Filliat, David},
  title =	{{Open the Chests: An Environment for Activity Recognition and Sequential Decision Problems Using Temporal Logic}},
  booktitle =	{31st International Symposium on Temporal Representation and Reasoning (TIME 2024)},
  pages =	{5:1--5:19},
  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.5},
  URN =		{urn:nbn:de:0030-drops-212128},
  doi =		{10.4230/LIPIcs.TIME.2024.5},
  annote =	{Keywords: Event-Based Decision Making, Activity Recognition, Temporal Logic, Reinforcement Learning, Dynamic Systems, Complex Event Processing, Benchmark Environment, Real-Time Simulation}
}
Document
Extending the Range of Temporal Specifications of the Run-Time Event Calculus

Authors: Periklis Mantenoglou and Alexander Artikis


Abstract
Composite event recognition (CER) frameworks reason over streams of low-level, symbolic events in order to detect instances of spatio-temporal patterns defining high-level, composite activities. The Event Calculus is a temporal, logical formalism that has been used to define composite activities in CER, while RTEC_{∘} is a formal CER framework that detects composite activities based on their Event Calculus definitions. RTEC_{∘}, however, cannot handle every possible set of Event Calculus definitions for composite activities, limiting the range of CER applications supported by RTEC_{∘}. We propose RTEC_{fl}, an extension of RTEC_{∘} that supports arbitrary composite activity specifications in the Event Calculus. We present the syntax, semantics, reasoning algorithms and time complexity of RTEC_{fl}. Our analysis demonstrates that RTEC_{fl} extends the scope of RTEC_{∘}, supporting every possible set of Event Calculus definitions for composite activities, while maintaining the high reasoning efficiency of RTEC_{∘}.

Cite as

Periklis Mantenoglou and Alexander Artikis. Extending the Range of Temporal Specifications of the Run-Time Event Calculus. In 31st International Symposium on Temporal Representation and Reasoning (TIME 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 318, pp. 6:1-6:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{mantenoglou_et_al:LIPIcs.TIME.2024.6,
  author =	{Mantenoglou, Periklis and Artikis, Alexander},
  title =	{{Extending the Range of Temporal Specifications of the Run-Time Event Calculus}},
  booktitle =	{31st International Symposium on Temporal Representation and Reasoning (TIME 2024)},
  pages =	{6:1--6:14},
  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.6},
  URN =		{urn:nbn:de:0030-drops-212135},
  doi =		{10.4230/LIPIcs.TIME.2024.6},
  annote =	{Keywords: Event Calculus, temporal pattern matching, composite event recognition}
}
Document
Fitting’s Style Many-Valued Interval Temporal Logic Tableau System: Theory and Implementation

Authors: Guillermo Badia, Carles Noguera, Alberto Paparella, Guido Sciavicco, and Ionel Eduard Stan


Abstract
Many-valued logics, often referred to as fuzzy logics, are a fundamental tool for reasoning about uncertainty, and are based on truth value algebras that generalize the Boolean one; the same logic can be interpreted on algebras from different varieties, for different purposes and pose different challenges. Although temporal many-valued logics, that is, the many-valued counterpart of popular temporal logics, have received little attention in the literature, the many-valued generalization of Halpern and Shoham’s interval temporal logic has been recently introduced and studied, and a sound and complete tableau system for it has been presented for the case in which it is interpreted on some finite Heyting algebra. In this paper, we take a step further in this inquiry by exploring a tableau system for Halpern and Shoham’s interval temporal logic interpreted on some finite {FL_{ew}}-algebra, therefore generalizing the Heyting case, and by providing its open-source implementation.

Cite as

Guillermo Badia, Carles Noguera, Alberto Paparella, Guido Sciavicco, and Ionel Eduard Stan. Fitting’s Style Many-Valued Interval Temporal Logic Tableau System: Theory and Implementation. In 31st International Symposium on Temporal Representation and Reasoning (TIME 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 318, pp. 7:1-7:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{badia_et_al:LIPIcs.TIME.2024.7,
  author =	{Badia, Guillermo and Noguera, Carles and Paparella, Alberto and Sciavicco, Guido and Stan, Ionel Eduard},
  title =	{{Fitting’s Style Many-Valued Interval Temporal Logic Tableau System: Theory and Implementation}},
  booktitle =	{31st International Symposium on Temporal Representation and Reasoning (TIME 2024)},
  pages =	{7:1--7:16},
  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.7},
  URN =		{urn:nbn:de:0030-drops-212145},
  doi =		{10.4230/LIPIcs.TIME.2024.7},
  annote =	{Keywords: Interval temporal logic, many-valued logic, tableau system}
}
Document
A More Efficient and Informed Algorithm to Check Weak Controllability of Simple Temporal Networks with Uncertainty

Authors: Ajdin Sumic and Thierry Vidal


Abstract
Simple Temporal Networks with Uncertainty (STNU) are a well-known constraint-based model expressing sets of activities (e.g., a schedule or a plan) related by temporal constraints, each having possible durations in the form of convex intervals. Uncertainty comes from some of these durations being contingent, i.e., the agent executing the plan cannot decide the actual duration at execution time. To check that execution will satisfy all the constraints, three levels of controllability exist: the Strong and Dynamic Controllability (SC/DC) has proven both useful in practice and provable in polynomial time, while Weak Controllability (WC) is co-NP-complete and has been left aside. Moreover, controllability checking algorithms are propagation strategies, which have the usual drawback, in case of failure, to prove unable to locate the contingents that explain the source of non-controllability. This paper has three contributions: (1) it substantiates the usefulness of WC in multi-agent systems (MAS) where another agent controls a contingent, and agents agree just before execution on the durations; (2) it provides a new WC-checking algorithm whose performance in practice depends on the network structure and is faster in loosely connected ones; (3) it provides the failing cycles in the network that explain non-WC.

Cite as

Ajdin Sumic and Thierry Vidal. A More Efficient and Informed Algorithm to Check Weak Controllability of Simple Temporal Networks with Uncertainty. In 31st International Symposium on Temporal Representation and Reasoning (TIME 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 318, pp. 8:1-8:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{sumic_et_al:LIPIcs.TIME.2024.8,
  author =	{Sumic, Ajdin and Vidal, Thierry},
  title =	{{A More Efficient and Informed Algorithm to Check Weak Controllability of Simple Temporal Networks with Uncertainty}},
  booktitle =	{31st International Symposium on Temporal Representation and Reasoning (TIME 2024)},
  pages =	{8:1--8:15},
  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.8},
  URN =		{urn:nbn:de:0030-drops-212151},
  doi =		{10.4230/LIPIcs.TIME.2024.8},
  annote =	{Keywords: Temporal constraints satisfaction, uncertainty, STNU, Controllability checking, Explainable inconsistency, Multi-agent planning}
}
Document
A Faster Algorithm for Finding Negative Cycles in Simple Temporal Networks with Uncertainty

Authors: Luke Hunsberger and Roberto Posenato


Abstract
Temporal constraint networks are data structures for representing and reasoning about time (e.g., temporal constraints among actions in a plan). Finding and computing negative cycles in temporal networks is important for planning and scheduling applications since it is the first step toward resolving inconsistent networks. For Simple Temporal Networks (STNs), the problem reduces to finding simple negative cycles (i.e., no repeat nodes), resulting in numerous efficient algorithms. For Simple Temporal Networks with Uncertainty (STNUs), which accommodate actions with uncertain durations, the situation is more complex because the characteristic of a non-dynamically controllable (non-DC) network is a so-called semi-reducible negative (SRN) cycle, which can have repeat edges and, in the worst case, an exponential number of occurrences of such edges. Algorithms for computing SRN cycles in non-DC STNUs that have been presented so far are based on older, less efficient DC-checking algorithms. In addition, the issue of repeated edges has either been ignored or given scant attention. This paper presents a new, faster algorithm for identifying SRN cycles in non-DC STNUs. Its worst-case time complexity is O(mn + k²n + knlog n), where n is the number of timepoints, m is the number of constraints, and k is the number of actions with uncertain durations. This complexity is the same as that of the fastest DC-checking algorithm for STNUs. It avoids an exponential blow-up by efficiently dealing with repeated structures and outputting a compact representation of the SRN cycle it finds. The space required to compactly store accumulated path information while avoiding redundant storage of repeated edges is O(mk + k²n). An empirical evaluation demonstrates the effectiveness of the new algorithm on an existing benchmark.

Cite as

Luke Hunsberger and Roberto Posenato. A Faster Algorithm for Finding Negative Cycles in Simple Temporal Networks with Uncertainty. In 31st International Symposium on Temporal Representation and Reasoning (TIME 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 318, pp. 9:1-9:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{hunsberger_et_al:LIPIcs.TIME.2024.9,
  author =	{Hunsberger, Luke and Posenato, Roberto},
  title =	{{A Faster Algorithm for Finding Negative Cycles in Simple Temporal Networks with Uncertainty}},
  booktitle =	{31st International Symposium on Temporal Representation and Reasoning (TIME 2024)},
  pages =	{9:1--9:15},
  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.9},
  URN =		{urn:nbn:de:0030-drops-212160},
  doi =		{10.4230/LIPIcs.TIME.2024.9},
  annote =	{Keywords: Temporal constraint networks, overconstrained networks, negative cycles}
}
Document
What Killed the Cat? Towards a Logical Formalization of Curiosity (And Suspense, and Surprise) in Narratives

Authors: Florence Dupin de Saint-Cyr, Anne-Gwenn Bosser, Benjamin Callac, and Eric Maisel


Abstract
We provide a unified framework in which the three emotions at the heart of narrative tension (curiosity, suspense and surprise) are formalized. This framework is built on non-monotonic reasoning which allows us to compactly represent the default behavior of the world and to simulate the affective evolution of an agent receiving a story. After formalizing the notions of awareness, curiosity, surprise and suspense, we explore the properties induced by our definitions and study the computational complexity of detecting them. We finally propose means to evaluate these emotions’ intensity for a given agent listening to a story.

Cite as

Florence Dupin de Saint-Cyr, Anne-Gwenn Bosser, Benjamin Callac, and Eric Maisel. What Killed the Cat? Towards a Logical Formalization of Curiosity (And Suspense, and Surprise) in Narratives. In 31st International Symposium on Temporal Representation and Reasoning (TIME 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 318, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{dupindesaintcyr_et_al:LIPIcs.TIME.2024.10,
  author =	{Dupin de Saint-Cyr, Florence and Bosser, Anne-Gwenn and Callac, Benjamin and Maisel, Eric},
  title =	{{What Killed the Cat? Towards a Logical Formalization of Curiosity (And Suspense, and Surprise) in Narratives}},
  booktitle =	{31st International Symposium on Temporal Representation and Reasoning (TIME 2024)},
  pages =	{10:1--10:16},
  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.10},
  URN =		{urn:nbn:de:0030-drops-212170},
  doi =		{10.4230/LIPIcs.TIME.2024.10},
  annote =	{Keywords: Knowledge Representation, Narration, Cognition}
}
Document
Faster Algorithm for Converting an STNU into Minimal Dispatchable Form

Authors: Luke Hunsberger and Roberto Posenato


Abstract
A Simple Temporal Network with Uncertainty (STNU) is a data structure for representing and reasoning about temporal constraints on activities, including those with uncertain durations. An STNU is dispatchable if it can be flexibly and efficiently executed in real time while guaranteeing that all relevant constraints are satisfied. The number of edges in a dispatchable network affects the computational work that must be done during real-time execution. Recent work presented an O(k n³)-time algorithm for converting a dispatchable STNU into an equivalent dispatchable network having a minimal number of edges, where n is the number of timepoints and k is the number of actions with uncertain durations. This paper presents a modification of that algorithm, making it an order of magnitude faster, down to O(n³). Given that in typical applications k = O(n), this represents an effective order-of-magnitude reduction from O(n⁴) to O(n³).

Cite as

Luke Hunsberger and Roberto Posenato. Faster Algorithm for Converting an STNU into Minimal Dispatchable Form. In 31st International Symposium on Temporal Representation and Reasoning (TIME 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 318, pp. 11:1-11:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{hunsberger_et_al:LIPIcs.TIME.2024.11,
  author =	{Hunsberger, Luke and Posenato, Roberto},
  title =	{{Faster Algorithm for Converting an STNU into Minimal Dispatchable Form}},
  booktitle =	{31st International Symposium on Temporal Representation and Reasoning (TIME 2024)},
  pages =	{11:1--11:14},
  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.11},
  URN =		{urn:nbn:de:0030-drops-212182},
  doi =		{10.4230/LIPIcs.TIME.2024.11},
  annote =	{Keywords: Temporal constraint networks, dispatchable networks}
}
Document
Robust Execution of Probabilistic STNs

Authors: Luke Hunsberger and Roberto Posenato


Abstract
A Probabilistic Simple Temporal Network (PSTN) is a formalism for representing and reasoning about actions subject to temporal constraints, where some action durations may be uncontrollable, modeled using continuous probability density functions. Recent work aims to manage this kind of uncertainty during execution by approximating a PSTN by a Simple Temporal Network with Uncertainty (STNU) (for which well-known execution strategies exist) and using an STNU execution strategy to execute the PSTN, hoping that its probabilistic action durations will not cause any constraint violations. This paper presents significant improvements to the robust execution of PSTNs. Our approach is based on a recent, faster algorithm for finding negative cycles in non-DC STNUs. We also formally prove that many of the constraints included in others' work are unnecessary and that our algorithm can take advantage of a flexible real-time execution algorithm to react to observations of contingent durations that may fall outside the fixed STNU bounds. The paper presents an empirical evaluation of our approach that provides evidence of its effectiveness in robustly executing PSTNs derived from a publicly available benchmark.

Cite as

Luke Hunsberger and Roberto Posenato. Robust Execution of Probabilistic STNs. In 31st International Symposium on Temporal Representation and Reasoning (TIME 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 318, pp. 12:1-12:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{hunsberger_et_al:LIPIcs.TIME.2024.12,
  author =	{Hunsberger, Luke and Posenato, Roberto},
  title =	{{Robust Execution of Probabilistic STNs}},
  booktitle =	{31st International Symposium on Temporal Representation and Reasoning (TIME 2024)},
  pages =	{12:1--12:19},
  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.12},
  URN =		{urn:nbn:de:0030-drops-212197},
  doi =		{10.4230/LIPIcs.TIME.2024.12},
  annote =	{Keywords: Temporal constraint networks, probabilistic durations, dispatchable networks}
}
Document
Introducing Interdependent Simple Temporal Networks with Uncertainty for Multi-Agent Temporal Planning

Authors: Ajdin Sumic, Thierry Vidal, Andrea Micheli, and Alessandro Cimatti


Abstract
Simple Temporal Networks with Uncertainty are a powerful and widely used formalism for representing and reasoning over convex temporal constraints in the presence of uncertainty called contingent constraints. Since their introduction, they have been used in planning and scheduling applications to model situations where the scheduling agent does not control some activity durations or event timings. What needs to be checked is then the controllability of the network, i.e., that there is a valid execution strategy whatever the values of the contingents. This paper considers a new type of multi-agent extension, where, as opposed to previous works, each agent manages its own separate STNU, and the control over activity durations is shared among the agents: what is called here a contract is a mutual constraint controllable for some agent and contingent for others. We will propose a semantically enriched version of STNUs that will be composed into a global Multi-agent Interdependent STNUs model. Then, controllability issues will be revisited, and we will focus on the repair problem, i.e., how to regain failed controllability by shrinking some of the shared contract durations, here in a centralized manner.

Cite as

Ajdin Sumic, Thierry Vidal, Andrea Micheli, and Alessandro Cimatti. Introducing Interdependent Simple Temporal Networks with Uncertainty for Multi-Agent Temporal Planning. In 31st International Symposium on Temporal Representation and Reasoning (TIME 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 318, pp. 13:1-13:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{sumic_et_al:LIPIcs.TIME.2024.13,
  author =	{Sumic, Ajdin and Vidal, Thierry and Micheli, Andrea and Cimatti, Alessandro},
  title =	{{Introducing Interdependent Simple Temporal Networks with Uncertainty for Multi-Agent Temporal Planning}},
  booktitle =	{31st International Symposium on Temporal Representation and Reasoning (TIME 2024)},
  pages =	{13:1--13:14},
  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.13},
  URN =		{urn:nbn:de:0030-drops-212200},
  doi =		{10.4230/LIPIcs.TIME.2024.13},
  annote =	{Keywords: Temporal constraints satisfaction, uncertainty, STNU, Controllability checking, Explainable inconsistency, Multi-agent planning}
}
Document
Learning Temporal Properties from Event Logs via Sequential Analysis

Authors: Francesco Chiariello


Abstract
In this work, we present a novel approach to learning Linear Temporal Logic (LTL) formulae from event logs by leveraging statistical techniques from sequential analysis. In particular, we employ the Sequential Probability Ratio Test (SPRT), using Trace Alignment to quantify the discrepancy between a trace and a candidate LTL formula. We then test the proposed approach in a controlled experimental setting and highlight its advantages, which include robustness to noise and data efficiency.

Cite as

Francesco Chiariello. Learning Temporal Properties from Event Logs via Sequential Analysis. In 31st International Symposium on Temporal Representation and Reasoning (TIME 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 318, pp. 14:1-14:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{chiariello:LIPIcs.TIME.2024.14,
  author =	{Chiariello, Francesco},
  title =	{{Learning Temporal Properties from Event Logs via Sequential Analysis}},
  booktitle =	{31st International Symposium on Temporal Representation and Reasoning (TIME 2024)},
  pages =	{14:1--14:14},
  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.14},
  URN =		{urn:nbn:de:0030-drops-212217},
  doi =		{10.4230/LIPIcs.TIME.2024.14},
  annote =	{Keywords: Process Mining, Declarative Process Discovery, Trace Alignment, Sequential Analysis}
}
Document
A Framework for Assessing Inconsistency in Disjunctive Temporal Problems

Authors: Jean-François Condotta and Yakoub Salhi


Abstract
Inconsistency measures serve to quantify the level of contradiction present within a knowledge base. They can be used for both consistency restoration and information extraction. In this article, we specifically explore inconsistency measures applicable to Disjunctive Temporal Problems (DTPs). We present a framework that extends traditional propositional logic approaches to DTPs, incorporating both new postulates and adaptations of existing ones. We identify and elaborate on various properties that establish relationships among these postulates. Furthermore, we introduce multiple inconsistency measures, adopting both a conventional approach that particularly leverages Minimal Inconsistent Subsets and a DTP-specific strategy based on constraint relaxation. Finally, we show the applicability of the inconsistency measures in DTPs through two real-world applications.

Cite as

Jean-François Condotta and Yakoub Salhi. A Framework for Assessing Inconsistency in Disjunctive Temporal Problems. In 31st International Symposium on Temporal Representation and Reasoning (TIME 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 318, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{condotta_et_al:LIPIcs.TIME.2024.15,
  author =	{Condotta, Jean-Fran\c{c}ois and Salhi, Yakoub},
  title =	{{A Framework for Assessing Inconsistency in Disjunctive Temporal Problems}},
  booktitle =	{31st International Symposium on Temporal Representation and Reasoning (TIME 2024)},
  pages =	{15:1--15:18},
  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.15},
  URN =		{urn:nbn:de:0030-drops-212223},
  doi =		{10.4230/LIPIcs.TIME.2024.15},
  annote =	{Keywords: Disjunctive Temporal Problems, Inconsistency Measures, Temporal Reasoning}
}
Document
Real-Time Higher-Order Recursion Schemes

Authors: Eric Alsmann and Florian Bruse


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
Time Series Anomaly Detection Leveraging MSE Feedback with AutoEncoder and RNN

Authors: Ibrahim Delibasoglu and Fredrik Heintz


Abstract
Anomaly detection in time series data is a critical task in various domains, including finance, healthcare, cybersecurity and industry. Traditional methods, such as time series decomposition, clustering, and density estimation, have provided robust solutions for identifying anomalies that exhibit distinct patterns or significant deviations from normal data distributions. Recent advancements in machine learning and deep learning have further enhanced these capabilities. This paper introduces a novel method for anomaly detection that combines the strengths of autoencoders and recurrent neural networks (RNNs) with an reconstruction error feedback mechanism based on Mean Squared Error. We compare our method against classical techniques and recent approaches like OmniAnomaly, which leverages stochastic recurrent neural networks, and the Anomaly Transformer, which introduces association discrepancy to capture long-range dependencies and DCDetector using contrastive representation learning with multi-scale dual attention. Experimental results demonstrate that our method achieves superior overall performance in terms of precision, recall, and F1 score. The source code is available at http://github.com/mribrahim/AE-FAR

Cite as

Ibrahim Delibasoglu and Fredrik Heintz. Time Series Anomaly Detection Leveraging MSE Feedback with AutoEncoder and RNN. In 31st International Symposium on Temporal Representation and Reasoning (TIME 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 318, pp. 17:1-17:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{delibasoglu_et_al:LIPIcs.TIME.2024.17,
  author =	{Delibasoglu, Ibrahim and Heintz, Fredrik},
  title =	{{Time Series Anomaly Detection Leveraging MSE Feedback with AutoEncoder and RNN}},
  booktitle =	{31st International Symposium on Temporal Representation and Reasoning (TIME 2024)},
  pages =	{17:1--17:12},
  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.17},
  URN =		{urn:nbn:de:0030-drops-212244},
  doi =		{10.4230/LIPIcs.TIME.2024.17},
  annote =	{Keywords: Time series, Anomaly, Neural networks}
}
Document
Full Characterisation of Extended CTL*

Authors: Massimo Benerecetti, Laura Bozzelli, Fabio Mogavero, and Adriano Peron


Abstract
The precise identification of the expressive power of logic languages used in formal methods for specifying and verifying run-time properties of critical systems is a fundamental task and characterisation theorems play a crucial role as model-theoretic tools in this regard. While a clear picture of the expressive power of linear-time temporal logics in terms of word automata and predicate logics has long been established, a complete mapping of the corresponding relationships for branching-time temporal logics has proven to be a more elusive task over the past four decades with few scattered results. Only recently, an automata-theoretic characterisation of both CTL* and its full-ω-regular extension ECTL* has been provided in terms of Symmetric Hesitant Tree Automata (HTA), with and without a suitable counter-freeness restriction on their linear behaviours. These two temporal logics also correspond to the bisimulation-invariant semantic fragments of Monadic Path Logic (MPL) and Monadic Chain Logic (MCL), respectively. Additionally, it has been proven that the counting extensions of CTL* and ECTL*, namely CCTL* and CECTL*, enjoy equivalent graded versions of the HTAs for the corresponding non-counting logics. However, while Moller and Rabinovich have proved CCTL* to be equivalent to full MPL, thus filling the gap for the standard branching-time logic, no similar result has been given for CECTL*. This work completes the picture, by proving the expressive equivalence of CECTL* and full MCL, by means of a composition theorem for the latter logic. This also indirectly establishes the equivalence between HTAs and their first-order extensions HFTAs, as originally introduced by Walukiewicz.

Cite as

Massimo Benerecetti, Laura Bozzelli, Fabio Mogavero, and Adriano Peron. Full Characterisation of Extended CTL*. In 31st International Symposium on Temporal Representation and Reasoning (TIME 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 318, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{benerecetti_et_al:LIPIcs.TIME.2024.18,
  author =	{Benerecetti, Massimo and Bozzelli, Laura and Mogavero, Fabio and Peron, Adriano},
  title =	{{Full Characterisation of Extended CTL*}},
  booktitle =	{31st International Symposium on Temporal Representation and Reasoning (TIME 2024)},
  pages =	{18:1--18:18},
  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.18},
  URN =		{urn:nbn:de:0030-drops-212259},
  doi =		{10.4230/LIPIcs.TIME.2024.18},
  annote =	{Keywords: Branching-Time Temporal Logics, Monadic Chain Logic, Tree Automata}
}
Document
Model Checking Linear Temporal Properties on Polyhedral Systems

Authors: Massimo Benerecetti, Marco Faella, and Fabio Mogavero


Abstract
We study the problem of model checking linear temporal logic formulae on finite trajectories generated by polyhedral differential inclusions, thus enriching the landscape of models where such specifications can be effectively verified. Each model in the class comprises a static and a dynamic component. The static component features a finite set of observables represented by (non-necessarily convex) polyhedra. The dynamic one is given by a convex polyhedron constraining the dynamics of the system, by specifying the possible slopes of the trajectories in each time instant. We devise an exact algorithm that computes a symbolic representation of the region of points that existentially satisfy a given formula φ, i.e., the points from which there exists a trajectory satisfying φ.

Cite as

Massimo Benerecetti, Marco Faella, and Fabio Mogavero. Model Checking Linear Temporal Properties on Polyhedral Systems. In 31st International Symposium on Temporal Representation and Reasoning (TIME 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 318, pp. 19:1-19:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{benerecetti_et_al:LIPIcs.TIME.2024.19,
  author =	{Benerecetti, Massimo and Faella, Marco and Mogavero, Fabio},
  title =	{{Model Checking Linear Temporal Properties on Polyhedral Systems}},
  booktitle =	{31st International Symposium on Temporal Representation and Reasoning (TIME 2024)},
  pages =	{19:1--19:23},
  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.19},
  URN =		{urn:nbn:de:0030-drops-212267},
  doi =		{10.4230/LIPIcs.TIME.2024.19},
  annote =	{Keywords: Model Checking, Real-Time Systems, LTLf, RTLf}
}
Document
FastMinTC+: A Fast and Effective Heuristic for Minimum Timeline Cover on Temporal Networks

Authors: Giorgio Lazzarinetti, Sara Manzoni, Italo Zoppis, and Riccardo Dondi


Abstract
The analysis and summarization of temporal networks are crucial for understanding complex interactions over time, yet pose significant computational challenges. This paper introduces FastMinTC+, an innovative heuristic approach designed to efficiently solve the Minimum Timeline Cover (MinTCover) problem in temporal networks. Our approach focuses on the optimization of activity timelines within temporal networks, aiming to provide both effective and computationally feasible solutions. By employing a low-complexity approach, FastMinTC+ adeptly handles massive temporal graphs, improving upon existing methods. Indeed, comparative evaluations on both synthetic and real-world datasets demonstrate that our algorithm outperforms established benchmarks with remarkable efficiency and accuracy. The results highlight the potential of heuristic approaches in the domain of temporal network analysis and open up new avenues for further research incorporating other computational techniques, for example deep learning, to enhance the adaptability and precision of such heuristics.

Cite as

Giorgio Lazzarinetti, Sara Manzoni, Italo Zoppis, and Riccardo Dondi. FastMinTC+: A Fast and Effective Heuristic for Minimum Timeline Cover on Temporal Networks. In 31st International Symposium on Temporal Representation and Reasoning (TIME 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 318, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{lazzarinetti_et_al:LIPIcs.TIME.2024.20,
  author =	{Lazzarinetti, Giorgio and Manzoni, Sara and Zoppis, Italo and Dondi, Riccardo},
  title =	{{FastMinTC+: A Fast and Effective Heuristic for Minimum Timeline Cover on Temporal Networks}},
  booktitle =	{31st International Symposium on Temporal Representation and Reasoning (TIME 2024)},
  pages =	{20:1--20:18},
  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.20},
  URN =		{urn:nbn:de:0030-drops-212275},
  doi =		{10.4230/LIPIcs.TIME.2024.20},
  annote =	{Keywords: Temporal Networks, Activity Timeline, Timeline Cover, Vertex Cover, Optimization, Heuristic}
}

Filters


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