25 Search Results for "Posenato, Roberto"


Volume

LIPIcs, Volume 247

29th International Symposium on Temporal Representation and Reasoning (TIME 2022)

TIME 2022, November 7-9, 2022, Virtual Conference

Editors: Alexander Artikis, Roberto Posenato, and Stefano Tonetta

Document
Extended Abstract
Converting Simple Temporal Networks with Uncertainty into Dispatchable Form - Faster (Extended Abstract)

Authors: Luke Hunsberger and Roberto Posenato

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


Abstract
In many sectors of real-world industry, it is necessary to plan and schedule tasks allocated to agents participating in complex processes. Temporal planning aims to schedule tasks while respecting temporal constraints such as release times, maximum durations, and deadlines, which requires quantitative temporal reasoning. Over the years, several major application developers have highlighted the need for the explicit representation of actions with uncertain durations; efficient algorithms for determining whether plans involving such actions are controllable; and efficient algorithms for converting such plans into forms that enable them to be executed in real time with minimal computation, while preserving maximum flexibility. A Simple Temporal Network with Uncertainty (STNU) is a data structure for reasoning about time constraints on actions that may have uncertain durations. An STNU is a triple (𝒯, 𝒞, ℒ) where 𝒯 is a set of real-valued variables called timepoints, 𝒞 is a set of constraints of the form Y-X ≤ δ, where X, Y ∈ 𝒯 and δ ∈ 𝐑, and ℒ is a set of contingent links of the form (A,x,y,C), where A,C ∈ 𝒯 and 0 < x < y < ∞. A contingent link (A,x,y,C) represents an uncertain duration where A is the activation timepoint, C is the contingent timepoint, and y-x is the uncertainty in the duration C-A. Typically, an executor controls the execution of A, but only observes the execution of C in real time. Although uncontrollable, the duration is guaranteed to satisfy C-A ∈ [x,y]. We let n = |𝒯|, m = |𝒞| and k = |ℒ|. An STNU graph is a pair (𝒯, ℰ), where the timepoints in 𝒯 serve as nodes in the graph, and the edges in ℰ correspond to the constraints in 𝒞 and contingent links in ℒ. For each Y-X ≤ δ in 𝒞, ℰ contains an ordinary edge X-δ->Y. For each (A,x,y,C) ∈ ℒ, ℰ contains a lower-case (LC) edge, A-c:y->C, and an upper-case (UC) edge, C-C:-y->A, representing the respective possibilities that C-A might take its minimum or maximum value. The LO-edges are the LC or ordinary edges; the OU-edges are the ordinary or UC edges. For any STNU, it is important to determine whether it is dynamically controllable (DC) (i.e., whether it is possible, in real time, to schedule its non-contingent timepoints such that all constraints will necessarily be satisfied no matter what durations turn out for the contingent links). Polynomial-time algorithms are available to solve this DC-checking problem. Each uses rules to generate new edges aiming to bypass certain kinds of edges in the STNU graph. Morris' O(n⁴)-time DC-checking algorithm [Paul Morris, 2006] starts from LC edges, propagating forward along OU-edges, looking for opportunities to generate new OU-edges that bypass the LC edges. Morris' O(n³)-time algorithm [Morris, 2014] starts from negative OU-edges, propagating backward along LO-edges, aiming to bypass negative edges with non-negative edges. The O(mn+k²n + knlog n)-time RUL¯ algorithm [Massimo Cairo et al., 2018] starts from UC edges, propagating backward along LO-edges, aiming to bypass UC edges with ordinary edges. After propagating, each algorithm checks for certain kinds of negative cycles to decide DC-vs.-non-DC. However, being DC only asserts the existence of a dynamic scheduler. It is also crucial to be able to execute a DC STNU efficiently in real time. For maximum flexibility and minimal space and time requirements, a dynamic scheduler for an STNU is typically computed incrementally, in real time, so that it can react to observations of contingent executions as they occur. An efficient dynamic scheduler can be realized by first transforming an STNU into an equivalent dispatchable form [Muscettola et al., 1998; Ioannis Tsamardinos et al., 1998]. Then, to execute the dispatchable STNU, it suffices to maintain time-windows for each timepoint and, as each timepoint X is executed, only updating time-windows for neighbors of X in the graph. Dispatchable STNUs are very important in applications that demand quick responses to observations of contingent events. Of the existing DC-checking algorithms, only Morris' O(n³)-time algorithm necessarily generates a dispatchable STNU for DC inputs. This abstract describes a faster, O(mn + kn² + n² log n)-time algorithm for converting DC STNUs into dispatchable form. (The full journal article is available elsewhere [Luke Hunsberger and Roberto Posenato, 2023].) This improvement is significant for applications (e.g., modeling business processes) where networks are typically sparse. For example, if m = O(n log n) and k = O(log n), then our algorithm runs in O(n²log n) ≪ O(n³) time. Our new Fast Dispatch algorithm, FD_STNU, has three phases. The first phase is similar to the RUL¯ DC-checking algorithm, but generates an order-of-magnitude fewer edges overall, while also generating new UC edges that correspond to wait constraints. The second phase is a version of Morris' 2006 algorithm that propagates forward from LC edges, but only along LO-edges, aiming to generate ordinary bypass edges. The third phase focuses on the subgraph of ordinary edges, which comprise a Simple Temporal Network (STN). It uses an existing dispatchability algorithm for STNs [Ioannis Tsamardinos et al., 1998] to convert that ordinary subgraph into a dispatchable STN. After completing the three phases, the STNU is guaranteed to be dispatchable. We provide the source code of a Java implementation of the considered algorithms (Morris, RUL¯, and FD_STNU) [Posenato, 2022] and the benchmarks used to compare their performances.

Cite as

Luke Hunsberger and Roberto Posenato. Converting Simple Temporal Networks with Uncertainty into Dispatchable Form - Faster (Extended Abstract). In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 20:1-20:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{hunsberger_et_al:LIPIcs.TIME.2023.20,
  author =	{Hunsberger, Luke and Posenato, Roberto},
  title =	{{Converting Simple Temporal Networks with Uncertainty into Dispatchable Form - Faster}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{20:1--20:3},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.20},
  URN =		{urn:nbn:de:0030-drops-191104},
  doi =		{10.4230/LIPIcs.TIME.2023.20},
  annote =	{Keywords: Temporal constraint networks, contingent durations, dispatchable network}
}
Document
Complete Volume
LIPIcs, Volume 247, TIME 2022, Complete Volume

Authors: Alexander Artikis, Roberto Posenato, and Stefano Tonetta

Published in: LIPIcs, Volume 247, 29th International Symposium on Temporal Representation and Reasoning (TIME 2022)


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-dev.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

Authors: Alexander Artikis, Roberto Posenato, and Stefano Tonetta

Published in: LIPIcs, Volume 247, 29th International Symposium on Temporal Representation and Reasoning (TIME 2022)


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-dev.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)

Authors: Moshe Y. Vardi

Published in: LIPIcs, Volume 247, 29th International Symposium on Temporal Representation and Reasoning (TIME 2022)


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-dev.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)

Authors: Silvia Miksch

Published in: LIPIcs, Volume 247, 29th International Symposium on Temporal Representation and Reasoning (TIME 2022)


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-dev.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)

Authors: Stijn Vansummeren

Published in: LIPIcs, Volume 247, 29th International Symposium on Temporal Representation and Reasoning (TIME 2022)


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-dev.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

Authors: Isaac Mackey, Raghubir Chimni, and Jianwen Su

Published in: LIPIcs, Volume 247, 29th International Symposium on Temporal Representation and Reasoning (TIME 2022)


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-dev.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

Authors: Florian Bruse, Martin Lange, and Etienne Lozes

Published in: LIPIcs, Volume 247, 29th International Symposium on Temporal Representation and Reasoning (TIME 2022)


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-dev.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

Authors: Victor Roussanaly and Yliès Falcone

Published in: LIPIcs, Volume 247, 29th International Symposium on Temporal Representation and Reasoning (TIME 2022)


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-dev.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

Authors: Thomas Guyet and Nicolas Markey

Published in: LIPIcs, Volume 247, 29th International Symposium on Temporal Representation and Reasoning (TIME 2022)


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-dev.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

Authors: Ashwin Bhaskar and M. Praveen

Published in: LIPIcs, Volume 247, 29th International Symposium on Temporal Representation and Reasoning (TIME 2022)


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-dev.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

Authors: Nicolas Peltier

Published in: LIPIcs, Volume 247, 29th International Symposium on Temporal Representation and Reasoning (TIME 2022)


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-dev.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

Authors: Dimitar P. Guelev

Published in: LIPIcs, Volume 247, 29th International Symposium on Temporal Representation and Reasoning (TIME 2022)


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-dev.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

Authors: Laura Bozzelli and Adriano Peron

Published in: LIPIcs, Volume 247, 29th International Symposium on Temporal Representation and Reasoning (TIME 2022)


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-dev.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}
}
  • Refine by Author
  • 9 Posenato, Roberto
  • 6 Hunsberger, Luke
  • 2 Artikis, Alexander
  • 2 Cairo, Massimo
  • 2 Combi, Carlo
  • Show More...

  • Refine by Classification
  • 7 Theory of computation → Modal and temporal logics
  • 6 Computing methodologies → Temporal reasoning
  • 5 Theory of computation → Logic and verification
  • 4 Theory of computation → Dynamic graph algorithms
  • 3 Mathematics of computing → Graph algorithms
  • Show More...

  • Refine by Keyword
  • 3 Dynamic Consistency
  • 3 Temporal Constraints
  • 2 Conditional Simple Temporal Networks
  • 2 Dynamic Controllability
  • 2 Linear Temporal Logic
  • Show More...

  • Refine by Type
  • 24 document
  • 1 volume

  • Refine by Publication Year
  • 18 2022
  • 3 2018
  • 2 2017
  • 1 2021
  • 1 2023

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