Volume
LIPIcs, Volume 247
29th International Symposium on Temporal Representation and Reasoning (TIME 2022)
Event
TIME 2022, November 7-9, 2022, Virtual ConferenceEditors
Publication Details
- published at: 2022-10-29
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-262-4
- DBLP: db/conf/time/time2022
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 247, TIME 2022, Complete Volume
Abstract
LIPIcs, Volume 247, TIME 2022, Complete Volume
Cite as
29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 1-222, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Proceedings{artikis_et_al:LIPIcs.TIME.2022,
title = {{LIPIcs, Volume 247, TIME 2022, Complete Volume}},
booktitle = {29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
pages = {1--222},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-262-4},
ISSN = {1868-8969},
year = {2022},
volume = {247},
editor = {Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2022},
URN = {urn:nbn:de:0030-drops-172469},
doi = {10.4230/LIPIcs.TIME.2022},
annote = {Keywords: LIPIcs, Volume 247, TIME 2022, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{artikis_et_al:LIPIcs.TIME.2022.0,
author = {Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
pages = {0:i--0:xiv},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-262-4},
ISSN = {1868-8969},
year = {2022},
volume = {247},
editor = {Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2022.0},
URN = {urn:nbn:de:0030-drops-172473},
doi = {10.4230/LIPIcs.TIME.2022.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
Linear Temporal Logic: From Infinite to Finite Horizon (Invited Talk)
Abstract
Linear Temporal Logic (LTL), proposed in 1977 by Amir Pnueli for reasoning about ongoing programs, was defined over infinite traces. The motivation for this was the desire to model arbitrarily long computations. While this approach has been highly successful in the context of model checking, it has been less successful in the context of reactive synthesis, due to the chalenging algorithmics of infinite-horizon temporal synthesis. In this talk we show that focusing on finite-horizon temporal synthesis offers enough algorithmic advantages to compensate for the loss in expressiveness. In fact, finite-horizon reasonings is useful even in the context of infinite-horizon applications.
Cite as
Moshe Y. Vardi. Linear Temporal Logic: From Infinite to Finite Horizon (Invited Talk). In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{vardi:LIPIcs.TIME.2022.1,
author = {Vardi, Moshe Y.},
title = {{Linear Temporal Logic: From Infinite to Finite Horizon}},
booktitle = {29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
pages = {1:1--1:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-262-4},
ISSN = {1868-8969},
year = {2022},
volume = {247},
editor = {Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2022.1},
URN = {urn:nbn:de:0030-drops-172481},
doi = {10.4230/LIPIcs.TIME.2022.1},
annote = {Keywords: Temporal Logic}
}
Document
Invited Talk
Visual Analytics Meets Temporal Reasoning: Challenges and Opportunities (Invited Talk)
Abstract
Visual Analytics as the science of analytical reasoning facilitated by interactive visual interfaces aims to enable the exploration and the understanding of large, heterogeneous, and complex data sets.
Time is an important data dimension with distinct characteristics.
Intertwining Visual Analytics with time and temporal reasoning introduces outstanding challenges and opportunities, which I will illustrate in this talk.
Cite as
Silvia Miksch. Visual Analytics Meets Temporal Reasoning: Challenges and Opportunities (Invited Talk). In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{miksch:LIPIcs.TIME.2022.2,
author = {Miksch, Silvia},
title = {{Visual Analytics Meets Temporal Reasoning: Challenges and Opportunities}},
booktitle = {29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
pages = {2:1--2:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-262-4},
ISSN = {1868-8969},
year = {2022},
volume = {247},
editor = {Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2022.2},
URN = {urn:nbn:de:0030-drops-172490},
doi = {10.4230/LIPIcs.TIME.2022.2},
annote = {Keywords: Visual Analytics, Visualization, Time}
}
Document
Invited Talk
Getting to the CORE of Complex Event Recognition (Invited Talk)
Abstract
In this talk, I will give an overview of our recent work on complex event recognition.
Cite as
Stijn Vansummeren. Getting to the CORE of Complex Event Recognition (Invited Talk). In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{vansummeren:LIPIcs.TIME.2022.3,
author = {Vansummeren, Stijn},
title = {{Getting to the CORE of Complex Event Recognition}},
booktitle = {29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
pages = {3:1--3:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-262-4},
ISSN = {1868-8969},
year = {2022},
volume = {247},
editor = {Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2022.3},
URN = {urn:nbn:de:0030-drops-172503},
doi = {10.4230/LIPIcs.TIME.2022.3},
annote = {Keywords: Complex Event Recognition, automata, enumeration-based query processing}
}
Document
Early Detection of Temporal Constraint Violations
Abstract
Software systems rely on events for logging, system coordination, handling unexpected situations, and more. Monitoring events at runtime can ensure that a business service system complies with policies, regulations, and business rules. Notably, detecting violations of rules as early as possible is much desired as it allows the system to reclaim resources from erring service enactments. We formalize a model for events and a logic-based rule language to specify temporal and data constraints. The primary goal of this paper is to develop techniques for detecting each rule violation as soon as it becomes inevitable. We further develop optimization techniques to reduce monitoring overhead. Finally, we implement a monitoring algorithm and experimentally evaluate it to demonstrate our approach to early violation detection is beneficial and effective for processing service enactments.
Cite as
Isaac Mackey, Raghubir Chimni, and Jianwen Su. Early Detection of Temporal Constraint Violations. In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 4:1-4:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{mackey_et_al:LIPIcs.TIME.2022.4,
author = {Mackey, Isaac and Chimni, Raghubir and Su, Jianwen},
title = {{Early Detection of Temporal Constraint Violations}},
booktitle = {29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
pages = {4:1--4:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-262-4},
ISSN = {1868-8969},
year = {2022},
volume = {247},
editor = {Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2022.4},
URN = {urn:nbn:de:0030-drops-172519},
doi = {10.4230/LIPIcs.TIME.2022.4},
annote = {Keywords: temporal constraints, monitoring, events, early violation detection}
}
Document
The Tail-Recursive Fragment of Timed Recursive CTL
Abstract
Timed Recursive CTL (TRCTL) was recently proposed as a merger of two extensions of the well-known branching-time logic CTL: Timed CTL on one hand is interpreted over real-time systems like timed automata, and Recursive CTL (RecCTL) on the other hand obtains high expressiveness through the introduction of a recursion operator. Model checking for the resulting logic is known to be 2-EXPTIME-complete.
The aim of this paper is to investigate the possibility to obtain a fragment of lower complexity without losing too much expressive power. It is obtained by a syntactic property called "tail-recursiveness" that restricts the way that recursive formulas can be built. This restriction is known to decrease the complexity of model checking by half an exponential in the untimed setting. We show that this also works in the real-time world: model checking for the tail-recursive fragment of TRCTL is EXPSPACE-complete. The upper bound is obtained by a standard untiming construction via region graphs, and rests on the known complexity of tail-recursive fragments of higher-order modal logics. The lower bound is established by a reduction from a suitable tiling problem.
Cite as
Florian Bruse, Martin Lange, and Etienne Lozes. The Tail-Recursive Fragment of Timed Recursive CTL. In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{bruse_et_al:LIPIcs.TIME.2022.5,
author = {Bruse, Florian and Lange, Martin and Lozes, Etienne},
title = {{The Tail-Recursive Fragment of Timed Recursive CTL}},
booktitle = {29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
pages = {5:1--5:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-262-4},
ISSN = {1868-8969},
year = {2022},
volume = {247},
editor = {Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2022.5},
URN = {urn:nbn:de:0030-drops-172527},
doi = {10.4230/LIPIcs.TIME.2022.5},
annote = {Keywords: formal specification, temporal logic, real-time systems}
}
Document
Decentralised Runtime Verification of Timed Regular Expressions
Abstract
Ensuring the correctness of distributed cyber-physical systems can be done at runtime by monitoring properties over their behaviour. In a decentralised setting, such behaviour consists of multiple local traces, each offering an incomplete view of the system events to the local monitors, as opposed to the standard centralised setting with a unique global trace. We introduce the first monitoring framework for timed properties described by timed regular expressions over a distributed network of monitors. First, we define functions to rewrite expressions according to partial knowledge for both the centralised and decentralised cases. Then, we define decentralised algorithms for monitors to evaluate properties using these functions, as well as proofs of soundness and eventual completeness of said algorithms. Finally, we implement and evaluate our framework on synthetic timed regular expressions, giving insights on the cost of the centralised and decentralised settings and when to best use each of them.
Cite as
Victor Roussanaly and Yliès Falcone. Decentralised Runtime Verification of Timed Regular Expressions. In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{roussanaly_et_al:LIPIcs.TIME.2022.6,
author = {Roussanaly, Victor and Falcone, Yli\`{e}s},
title = {{Decentralised Runtime Verification of Timed Regular Expressions}},
booktitle = {29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
pages = {6:1--6:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-262-4},
ISSN = {1868-8969},
year = {2022},
volume = {247},
editor = {Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2022.6},
URN = {urn:nbn:de:0030-drops-172532},
doi = {10.4230/LIPIcs.TIME.2022.6},
annote = {Keywords: Timed expressions, Timed properties, Monitoring, Runtime verification, Decentralized systems, Asynchronous communication}
}
Document
Logical Forms of Chronicles
Abstract
A chronicle is a temporal model introduced by Dousson et al. for situation recognition. In short, a chronicle consists of a set of events and a set of real-valued temporal constraints on the delays between pairs of events. This work investigates the relationship between chronicles and classical temporal-model formalisms, namely TPTL and MTL. More specifically, we answer the following question: is it possible to find an equivalent formula in such formalisms for any chronicle? This question arises from the observation that a single chronicle captures complex temporal behaviours, without imposing a particular order of the events in time.
For our purpose, we introduce the subclass of linear chronicles, which set the order of occurrence of the events to be recognized in a temporal sequence. Our first result is that any chronicle can be expressed as a disjunction of linear chronicles. Our second result is that any linear chronicle has an equivalent TPTL formula. Using existing expressiveness results between TPTL and MTL, we show that some chronicles have no equivalent in MTL. This confirms that the model of chronicle has interesting properties for situation recognition.
Cite as
Thomas Guyet and Nicolas Markey. Logical Forms of Chronicles. In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 7:1-7:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{guyet_et_al:LIPIcs.TIME.2022.7,
author = {Guyet, Thomas and Markey, Nicolas},
title = {{Logical Forms of Chronicles}},
booktitle = {29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
pages = {7:1--7:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-262-4},
ISSN = {1868-8969},
year = {2022},
volume = {247},
editor = {Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2022.7},
URN = {urn:nbn:de:0030-drops-172542},
doi = {10.4230/LIPIcs.TIME.2022.7},
annote = {Keywords: temporal logics, temporal models}
}
Document
Realizability Problem for Constraint LTL
Abstract
Constraint linear-time temporal logic (CLTL) is an extension of LTL that is interpreted on sequences of valuations of variables over an infinite domain. The atomic formulas are interpreted as constraints on the valuations. The atomic formulas can constrain valuations over a range of positions along a sequence, with the range being bounded by a parameter depending on the formula. The satisfiability and model checking problems for CLTL have been studied by Demri and D’Souza. We consider the realizability problem for CLTL. The set of variables is partitioned into two parts, with each part controlled by a player. Players take turns to choose valuations for their variables, generating a sequence of valuations. The winning condition is specified by a CLTL formula - the first player wins if the sequence of valuations satisfies the specified formula. We study the decidability of checking whether the first player has a winning strategy in the realizability game for a given CLTL formula. We prove that it is decidable in the case where the domain satisfies the completion property, a property introduced by Balbiani and Condotta in the context of satisfiability. We prove that it is undecidable over (ℤ, < , =), the domain of integers with order and equality. We prove that over (ℤ, < , =), it is decidable if the atomic constraints in the formula can only constrain the current valuations of variables belonging to the second player, but there are no such restrictions for the variables belonging to the first player. We call this single-sided games.
Cite as
Ashwin Bhaskar and M. Praveen. Realizability Problem for Constraint LTL. In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{bhaskar_et_al:LIPIcs.TIME.2022.8,
author = {Bhaskar, Ashwin and Praveen, M.},
title = {{Realizability Problem for Constraint LTL}},
booktitle = {29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
pages = {8:1--8:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-262-4},
ISSN = {1868-8969},
year = {2022},
volume = {247},
editor = {Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2022.8},
URN = {urn:nbn:de:0030-drops-172556},
doi = {10.4230/LIPIcs.TIME.2022.8},
annote = {Keywords: Realizability, constraint LTL, Strategy trees, Tree automata}
}
Document
Reasoning on Dynamic Transformations of Symbolic Heaps
Abstract
Building on previous results concerning the decidability of the satisfiability and entailment problems for separation logic formulas with inductively defined predicates, we devise a proof procedure to reason on dynamic transformations of memory heaps. The initial state of the system is described by a separation logic formula of some particular form, its evolution is modeled by a finite transition system and the expected property is given as a linear temporal logic formula built over assertions in separation logic.
Cite as
Nicolas Peltier. Reasoning on Dynamic Transformations of Symbolic Heaps. In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 9:1-9:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{peltier:LIPIcs.TIME.2022.9,
author = {Peltier, Nicolas},
title = {{Reasoning on Dynamic Transformations of Symbolic Heaps}},
booktitle = {29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
pages = {9:1--9:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-262-4},
ISSN = {1868-8969},
year = {2022},
volume = {247},
editor = {Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2022.9},
URN = {urn:nbn:de:0030-drops-172566},
doi = {10.4230/LIPIcs.TIME.2022.9},
annote = {Keywords: Separation Logic, Symbolic Heaps, Linear Temporal Logic}
}
Document
Gabbay Separation for the Duration Calculus
Abstract
Gabbay’s separation theorem about linear temporal logic with past has proved to be one of the most useful theoretical results in temporal logic. In particular it enables a concise proof of Kamp’s seminal expressive completeness theorem for LTL. In 2000, Alexander Rabinovich established an expressive completeness result for a subset of the Duration Calculus (DC), a real-time interval temporal logic. DC is based on the chop binary modality, which restricts access to subintervals of the reference time interval, and is therefore regarded as introspective. The considered subset of DC is known as the ⌈P⌉-subset in the literature. Neighbourhood Logic (NL), a system closely related to {DC}, is based on the neighbourhood modalities, also written ⟨A⟩ and ⟨ ̄A⟩ in the notation stemming from Allen’s system of interval relations. These modalities are expanding as they allow writing future and past formulas to impose conditions outside the reference interval. This setting makes temporal separation relevant: is expressive power ultimately affected, if past constructs are not allowed in the scope of future ones, or vice versa? In this paper we establish an analogue of Gabbay’s separation theorem for the ⌈P⌉-subset of the extension of DC by the neighbourhood modalities, and the ⌈P⌉-subset of the extension of DC by the neighbourhood modalities and chop-based analogue of Kleene star. We show that the result applies if the weak chop inverses, a pair binary expanding modalities, are given the role of the neighbourhood modalities, by virtue of the inter-expressibility between them and the neighbourhood modalities in the presence of chop.
Cite as
Dimitar P. Guelev. Gabbay Separation for the Duration Calculus. In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 10:1-10:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{guelev:LIPIcs.TIME.2022.10,
author = {Guelev, Dimitar P.},
title = {{Gabbay Separation for the Duration Calculus}},
booktitle = {29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
pages = {10:1--10:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-262-4},
ISSN = {1868-8969},
year = {2022},
volume = {247},
editor = {Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2022.10},
URN = {urn:nbn:de:0030-drops-172578},
doi = {10.4230/LIPIcs.TIME.2022.10},
annote = {Keywords: Gabbay separation, Neighbourhood Logic, Duration Calculus, expanding modalities}
}
Document
A Quantitative Extension of Interval Temporal Logic over Infinite Words
Abstract
Model checking (MC) for Halpern and Shoham’s interval temporal logic HS has been recently investigated in a systematic way, and it is known to be decidable under three distinct semantics (state-based, trace-based and tree-based semantics), all of them assuming homogeneity in the propositional valuation. Here, we focus on the trace-based semantics, where the main semantic entities are the infinite execution paths (traces) of the given Kripke structure. We introduce a quantitative extension of HS over traces, called Difference HS (DHS), allowing one to express timing constraints on the difference among interval lengths (durations). We show that MC and satisfiability of full DHS are in general undecidable, so, we investigate the decidability border for these problems by considering natural syntactical fragments of DHS. In particular, we identify a maximal decidable fragment DHS_{simple} of DHS proving in addition that the considered problems for this fragment are at least 2Expspace-hard. Moreover, by exploiting new results on linear-time hybrid logics, we show that for an equally expressive fragment of DHS_{simple}, the problems are Expspace-complete. Finally, we provide a characterization of HS over traces by means of the one-variable fragment of a novel hybrid logic.
Cite as
Laura Bozzelli and Adriano Peron. A Quantitative Extension of Interval Temporal Logic over Infinite Words. In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 11:1-11:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{bozzelli_et_al:LIPIcs.TIME.2022.11,
author = {Bozzelli, Laura and Peron, Adriano},
title = {{A Quantitative Extension of Interval Temporal Logic over Infinite Words}},
booktitle = {29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
pages = {11:1--11:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-262-4},
ISSN = {1868-8969},
year = {2022},
volume = {247},
editor = {Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2022.11},
URN = {urn:nbn:de:0030-drops-172585},
doi = {10.4230/LIPIcs.TIME.2022.11},
annote = {Keywords: Interval temporal logic, Homogeneity Assumption, Quantitative Constraints, Model checking, Decision Procedures, Complexity issues, Linear-time Hybrid Logics}
}
Document
A Neuro-Symbolic Approach for Real-World Event Recognition from Weak Supervision
Abstract
Events are structured entities involving different components (e.g, the participants, their roles etc.) and their relations. Structured events are typically defined in terms of (a subset of) simpler, atomic events and a set of temporal relation between them. Temporal Event Detection (TED) is the task of detecting structured and atomic events within data streams, most often text or video sequences, and has numerous applications, from video surveillance to sports analytics. Existing deep learning approaches solve TED task by implicitly learning the temporal correlations among events from data. As consequence, these approaches often fail in ensuring a consistent prediction in terms of the relationship between structured and atomic events. On the other hand, neuro-symbolic approaches have shown their capability to constrain the output of the neural networks to be consistent with respect to the background knowledge of the domain. In this paper, we propose a neuro-symbolic approach for TED in a real world scenario involving sports activities. We show how by incorporating simple knowledge involving the relative order of atomic events and constraints on their duration, the approach substantially outperforms a fully neural solution in terms of recognition accuracy, when little or even no supervision is available on the atomic events.
Cite as
Gianluca Apriceno, Andrea Passerini, and Luciano Serafini. A Neuro-Symbolic Approach for Real-World Event Recognition from Weak Supervision. In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 12:1-12:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{apriceno_et_al:LIPIcs.TIME.2022.12,
author = {Apriceno, Gianluca and Passerini, Andrea and Serafini, Luciano},
title = {{A Neuro-Symbolic Approach for Real-World Event Recognition from Weak Supervision}},
booktitle = {29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
pages = {12:1--12:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-262-4},
ISSN = {1868-8969},
year = {2022},
volume = {247},
editor = {Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2022.12},
URN = {urn:nbn:de:0030-drops-172594},
doi = {10.4230/LIPIcs.TIME.2022.12},
annote = {Keywords: structured events, temporal event detection, neuro-symbolic integration}
}
Document
Neural-Symbolic Temporal Decision Trees for Multivariate Time Series Classification
Abstract
Multivariate time series classification is a widely known problem, and its applications are ubiquitous. Due to their strong generalization capability, neural networks have been proven to be very powerful for the task, but their applicability is often limited by their intrinsic black-box nature. Recently, temporal decision trees have been shown to be a serious alternative to neural networks for the same task in terms of classification performances, while attaining higher levels of transparency and interpretability. In this work, we propose an initial approach to neural-symbolic temporal decision trees, that is, an hybrid method that leverages on both the ability of neural networks of capturing temporal patterns and the flexibility of temporal decision trees of taking decisions on intervals based on (possibly, externally computed) temporal features. While based on a proof-of-concept implementation, in our experiments on public datasets, neural-symbolic temporal decision trees show promising results.
Cite as
Giovanni Pagliarini, Simone Scaboro, Giuseppe Serra, Guido Sciavicco, and Ionel Eduard Stan. Neural-Symbolic Temporal Decision Trees for Multivariate Time Series Classification. In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 13:1-13:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{pagliarini_et_al:LIPIcs.TIME.2022.13,
author = {Pagliarini, Giovanni and Scaboro, Simone and Serra, Giuseppe and Sciavicco, Guido and Stan, Ionel Eduard},
title = {{Neural-Symbolic Temporal Decision Trees for Multivariate Time Series Classification}},
booktitle = {29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
pages = {13:1--13:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-262-4},
ISSN = {1868-8969},
year = {2022},
volume = {247},
editor = {Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2022.13},
URN = {urn:nbn:de:0030-drops-172607},
doi = {10.4230/LIPIcs.TIME.2022.13},
annote = {Keywords: Machine learning, neural-symbolic, temporal logic, hybrid temporal decision trees}
}
Document
Taming Strategy Logic: Non-Recurrent Fragments
Abstract
Strategy Logic (SL for short) is one of the prominent languages for reasoning about the strategic abilities of agents in a multi-agent setting. This logic extends LTL with first-order quantifiers over the agent strategies and encompasses other formalisms, such as ATL* and CTL*. The model-checking problem for SL and several of its fragments have been extensively studied. On the other hand, the picture is much less clear on the satisfiability front, where the problem is undecidable for the full logic. In this work, we study two fragments of One-Goal SL, where the nesting of sentences within temporal operators is constrained. We show that the satisfiability problem for these logics, and for the corresponding fragments of ATL* and CTL*, is ExpSpace and PSpace-Complete, respectively.
Cite as
Massimo Benerecetti, Fabio Mogavero, and Adriano Peron. Taming Strategy Logic: Non-Recurrent Fragments. In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 14:1-14:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{benerecetti_et_al:LIPIcs.TIME.2022.14,
author = {Benerecetti, Massimo and Mogavero, Fabio and Peron, Adriano},
title = {{Taming Strategy Logic: Non-Recurrent Fragments}},
booktitle = {29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
pages = {14:1--14:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-262-4},
ISSN = {1868-8969},
year = {2022},
volume = {247},
editor = {Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2022.14},
URN = {urn:nbn:de:0030-drops-172611},
doi = {10.4230/LIPIcs.TIME.2022.14},
annote = {Keywords: Strategic Reasoning, Multi-Agent Systems, Temporal Logics, Satisfiability}
}
Document
Giving Instructions in Linear Temporal Logic
Abstract
Our aim is to develop a formal semantics for giving instructions to taskable agents, to investigate the complexity of decision problems relating to these semantics, and to explore the issues that these semantics raise. In the setting we consider, agents are given instructions in the form of Linear Temporal Logic (LTL) formulae; the intuitive interpretation of such an instruction is that the agent should act in such a way as to ensure the formula is satisfied. At the same time, agents are assumed to have inviolable and immutable background safety requirements, also specified as LTL formulae. Finally, the actions performed by an agent are assumed to have costs, and agents must act within a limited budget. For this setting, we present a range of interpretations of an instruction to achieve an LTL task Υ, intuitively ranging from "try to do this but only if you can do so with everything else remaining unchanged" up to "drop everything and get this done." For each case we present a formal pre-/post-condition semantics, and investigate the computational issues that they raise.
Cite as
Julian Gutierrez, Sarit Kraus, Giuseppe Perelli, and Michael Wooldridge. Giving Instructions in Linear Temporal Logic. In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 15:1-15:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{gutierrez_et_al:LIPIcs.TIME.2022.15,
author = {Gutierrez, Julian and Kraus, Sarit and Perelli, Giuseppe and Wooldridge, Michael},
title = {{Giving Instructions in Linear Temporal Logic}},
booktitle = {29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
pages = {15:1--15:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-262-4},
ISSN = {1868-8969},
year = {2022},
volume = {247},
editor = {Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2022.15},
URN = {urn:nbn:de:0030-drops-172622},
doi = {10.4230/LIPIcs.TIME.2022.15},
annote = {Keywords: Linear Temporal Logic, Synthesis, Game theory, Multi-Agent Systems}
}