DROPS

Document

DOI: 10.4230/LIPIcs.TIME.2025.3

Metric Linear-Time Temporal Logic with Strict First-Time Semantics

Authors: Eric Alsmann and Martin Lange

Published in: LIPIcs, Volume 355, 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)

Abstract

We introduce strict first-time semantics for the Until operator from linear-time temporal logic which makes assertions not just about some future moment but about the first time in the future that its argument should hold. We investigate Metric Linear-Time Temporal Logic under this interpretation in terms of expressive power, relative succinctness and computational complexity. While the expressiveness does not exceed that of pure LTL, there are properties definable in this logic which can only be expressed in LTL with exponentially larger formulas. Yet, we show that the complexity of the satisfiability problem remains PSPACE-complete which is in contrast to the EXPSPACE-completeness of Metric LTL. The motivation for this logic originates in a study of the expressive power of State Space Models, a recently proposed alternative to the popular transformer architectures in machine learning.

Cite as

Eric Alsmann and Martin Lange. Metric Linear-Time Temporal Logic with Strict First-Time Semantics. In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 3:1-3:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{alsmann_et_al:LIPIcs.TIME.2025.3,
  author =	{Alsmann, Eric and Lange, Martin},
  title =	{{Metric Linear-Time Temporal Logic with Strict First-Time Semantics}},
  booktitle =	{32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
  pages =	{3:1--3:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-401-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{355},
  editor =	{Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.3},
  URN =		{urn:nbn:de:0030-drops-244491},
  doi =		{10.4230/LIPIcs.TIME.2025.3},
  annote =	{Keywords: linear-time temporal logic, metric temporal logic, computational complexity, Streett automata}
}

Document

DOI: 10.4230/LIPIcs.TIME.2024.16

Real-Time Higher-Order Recursion Schemes

Authors: Eric Alsmann and Florian Bruse

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

Abstract

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

Cite as

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

Copy BibTex To Clipboard

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

Search Results

Documents authored by Alsmann, Eric

Metric Linear-Time Temporal Logic with Strict First-Time Semantics

Abstract

Cite as

Real-Time Higher-Order Recursion Schemes

Abstract

Cite as

Thanks for your feedback!

Could not send message