Automata and Fixpoints for Asynchronous Hyperproperties
summary
Introduces Hμ (a linear-time μ-calculus with named path quantifiers and indexed nexts) and Alternating Asynchronous Parity Automata as concrete tools, proves a correspondence theorem giving effective translations between them over fixed trace assignments, and shows key decision problems (emptiness for AAPA, model checking for Hμ) are highly undecidable — not even arithmetical. Proposes decidable approximations: k-synchronicity (emptiness in EXPSPACE, optimal) and k‑context bounds (decidable but non‑elementary when k is part of input).
AI-written summary · about
chapters (17)
- 0:00Intro
- 0:25Hyperproperties
- 1:38Classical Model Checking
- 2:34State of the Art Logics
- 3:23Motivation for a new Hyperlogic
- 4:25The logic H
- 5:12Examples of Security Properties in Hy
- 6:34Asynchronous Specifications
- 7:35Specifications for Concurrent Programs
- 8:45Alternating Asynchronous Parity Automata
- 10:38Correspondence Theorem
- 12:05Undecidability Results
- 13:18Extended Syntax Tree
- 13:44k-synchronicity
- 15:08Context Bounds
- 17:09Future Work
- 20:04Conclusion
related talks
20mHyper Hoare Logic: (Dis-)Proving Program Hyperproperties
21mDecision and Complexity of Dolev-Yao Hyperproperties
21mHyper Separation Logic
58mAutomating Relational Verification of Infinite-State Programs
34mIs It Even Possible? On the Parallel Composition of Asynchronous MPC Protocols
57mSequential Information Flow
26mNon-Interference Preserving and Optimising Compilation with Hyperproperty Simulations
12mFully Abstract and Robust Compilation and How to Reconcile the Two, Abstractly