2 Search Results for "Sandström, Max"

Document
DOI: 10.4230/LIPIcs.CSL.2025.10
The Complexity of Second-Order HyperLTL

Authors: Hadar Frenkel and Martin Zimmermann

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
We determine the complexity of second-order HyperLTL satisfiability, finite-state satisfiability, and model-checking: All three are equivalent to truth in third-order arithmetic. We also consider two fragments of second-order HyperLTL that have been introduced with the aim to facilitate effective model-checking by restricting the sets one can quantify over. The first one restricts second-order quantification to smallest/largest sets that satisfy a guard while the second one restricts second-order quantification further to least fixed points of (first-order) HyperLTL definable functions. All three problems for the first fragment are still equivalent to truth in third-order arithmetic while satisfiability for the second fragment is Σ₁¹-complete, i.e., only as hard as for (first-order) HyperLTL and therefore much less complex. Finally, finite-state satisfiability and model-checking are in Σ₂² and are Σ₁¹-hard, and thus also less complex than for full second-order HyperLTL.
Cite as

Hadar Frenkel and Martin Zimmermann. The Complexity of Second-Order HyperLTL. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 10:1-10:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{frenkel_et_al:LIPIcs.CSL.2025.10,
  author =	{Frenkel, Hadar and Zimmermann, Martin},
  title =	{{The Complexity of Second-Order HyperLTL}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{10:1--10:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.10},
  URN =		{urn:nbn:de:0030-drops-227679},
  doi =		{10.4230/LIPIcs.CSL.2025.10},
  annote =	{Keywords: HyperLTL, Satisfiability, Model-checking}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2023.60
Set Semantics for Asynchronous TeamLTL: Expressivity and Complexity

Authors: Juha Kontinen, Max Sandström, and Jonni Virtema

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)

Abstract
We introduce and develop a set-based semantics for asynchronous TeamLTL. We consider two canonical logics in this setting: the extensions of TeamLTL by the Boolean disjunction and by the Boolean negation. We relate the new semantics with the original semantics based on multisets and establish one of the first positive complexity theoretic results in the temporal team semantics setting. In particular we show that both logics enjoy normal forms that can be utilised to obtain results related to expressivity and complexity (decidability) of the new logics.
Cite as

Juha Kontinen, Max Sandström, and Jonni Virtema. Set Semantics for Asynchronous TeamLTL: Expressivity and Complexity. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 60:1-60:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{kontinen_et_al:LIPIcs.MFCS.2023.60,
  author =	{Kontinen, Juha and Sandstr\"{o}m, Max and Virtema, Jonni},
  title =	{{Set Semantics for Asynchronous TeamLTL: Expressivity and Complexity}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{60:1--60:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.60},
  URN =		{urn:nbn:de:0030-drops-185949},
  doi =		{10.4230/LIPIcs.MFCS.2023.60},
  annote =	{Keywords: Hyperproperties, Linear Temporal Logic, Team Semantics}
}
  • Refine by Type
  • 2 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2023

  • Refine by Author
  • 1 Frenkel, Hadar
  • 1 Kontinen, Juha
  • 1 Sandström, Max
  • 1 Virtema, Jonni
  • 1 Zimmermann, Martin

  • Refine by Series/Journal
  • 2 LIPIcs

  • Refine by Classification
  • 2 Theory of computation → Logic and verification
  • 1 Theory of computation → Verification by model checking

  • Refine by Keyword
  • 1 HyperLTL
  • 1 Hyperproperties
  • 1 Linear Temporal Logic
  • 1 Model-checking
  • 1 Satisfiability
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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