A complete proof system for HyperLTL

DOI10.1007/978-3-032-32589-1_23MaRDI QIDQ7411179zbMATH OpenFDO

Authors Naijun Zhan, Wen Tang, Dimitar P. Guelev

Publication date 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-032-32589-1_23

zbMATH Keywords

first-order logicHyperLTLinteractive theorem provingproof systemsatisfiability

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A Cut-Free and Invariant-Free Sequent Calculus for PLTL
• A model existence theorem in infinitary propositional modal logic
• A strongly complete axiomatization of intuitionistic temporal logic
• A temporal logic for asynchronous hyperproperties
• Asynchronous extensions of hyperLTL
• Beyond 2-safety: asymmetric product programs for relational program verification
• Defining liveness
• Flavors of sequential information flow
• scientific article; zbMATH DE number 1670495 (Why is no real title available?)
• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 6851935 (Why is no real title available?)
• scientific article; zbMATH DE number 1903365 (Why is no real title available?)
• scientific article; zbMATH DE number 7730626 (Why is no real title available?)
• scientific article; zbMATH DE number 7799630 (Why is no real title available?)
• Model Checking Information Flow in Reactive Systems
• Model Checking on Trees with Path Equivalences
• Model checking quantitative hyperproperties
• Monitoring hyperproperties
• Preserving Secrecy Under Refinement
• Probabilistic Hyperproperties of Markov Decision Processes
• Probabilistic Hyperproperties with Nondeterminism
• Propositional Dynamic Logic for Hyperproperties
• Propositional temporal logics: decidability and completeness
• Results on the propositional \(\mu\)-calculus
• Synthesizing reactive systems from hyperproperties
• Team semantics for the specification and verification of hyperproperties
• The complementation problem for Büchi automata with applications to temporal logic
• The complexity of propositional linear temporal logics
• The first-order logic of hyperproperties
• The hierarchy of hyperlogics
• Verifying hyperliveness
• “Sometimes” and “not never” revisited

This page was built for publication: A complete proof system for HyperLTL

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