HyperLTL satisfiability is highly undecidable, HyperCTL^* is even harder

DOI10.46298/LMCS-21(1:3)2025MaRDI QIDQ7034355zbMATH OpenFDO

Authors Marie Fortin, Louwe B. Kuijer, Patrick Totzke, Martin Zimmermann

Publication date 31 January 2025

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.46298/LMCS-21(1:3)2025

zbMATH Keywords

analytical hierarchyHyperCTL*HyperLTLsatisfiability

Mathematics Subject Classification ID

Temporal logic (03B44) Undecidability and degrees of sets of sentences (03D35) Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites work

• A combinatorial approach to the theory of ω-automata
• A remark on the expressivity of asynchronous TeamLTL and HyperLTL
• A temporal logic for asynchronous hyperproperties
• Algorithms for model checking HyperLTL and HyperCTL^*
• Asynchronous extensions of hyperLTL
• AutoHyper: explicit-state model checking for HyperLTL
• Bounded model checking for asynchronous hyperproperties
• Classifying regular events in symbolic logic
• Deciding hyperproperties combined with functional specifications
• Dot-depth of star-free events
• Expressiveness and decidability of temporal logics for asynchronous hyperproperties
• Finite-word hyperlanguages
• First-order definable languages
• scientific article; zbMATH DE number 6851935 (Why is no real title available?)
• HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems
• HyperLTL Satisfiability Is Σ₁¹-Complete, HyperCTL* Satisfiability Is Σ₁²-Complete.
• Hypernode automata
• HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties
• Model checking algorithms for hyperproperties (invited paper)
• On the complexity of linear temporal logic with team semantics
• On the expressive power of TeamLTL and first-order team logic over hyperproperties
• Probabilistic Hyperproperties of Markov Decision Processes
• Probabilistic Hyperproperties with Nondeterminism
• Realizing \(\omega\)-regular hyperproperties
• Recurring Dominoes: Making the Highly Undecidable Highly Understandable
• Recursion-theoretic hierarchies
• Rewriting-based runtime verification for alternation-free HyperLTL
• Runtime enforcement of hyperproperties
• Second-order hyperproperties
• Set semantics for asynchronous TeamLTL: expressivity and complexity
• Software Verification of Hyperproperties Beyond k-Safety
• Synthesis from hyperproperties
• Team semantics for the specification and verification of hyperproperties
• The first-order logic of hyperproperties
• The Keys to Decidable HyperLTL Satisfiability: Small Models or Very Simple Formulas
• Über eine Schlußweise aus dem Endlichen ins Unendliche.
• “Sometimes” and “not never” revisited

Cited in

(3)

• The complexity of second-order HyperLTL
• The complexity of HyperQPTL
• Complexity of model checking second-order hyperproperties on finite structures

This page was built for publication: HyperLTL satisfiability is highly undecidable, \(\mathrm{HyperCTL}^*\) is even harder

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7034355)