Effect Semantics for Quantum Protocols
summary
Proposes a semantics that replaces state-based probabilistic LTS with effect distributions and effect LTS that record measurement effects (matrices ≤ I) so one finite effect LTS yields all input-instantiated probabilistic LTS. Proves equivalence: two processes are bisimilar in the Heisenberg-style semantics iff every instantiated probabilistic LTS is bisimilar, enabling algorithmic verification instead of infinitely many checks. Identifies two bisimilarities and advocates large-scope bisimilarity for quantum indistinguishability; congruence and nondeterminism preservation remain work in progress.
AI-written summary · about
chapters (7)
- 0:00Quantum protocol semantics intro
- 2:23Probabilistic bisimulation limits
- 4:37Effect semantics for quantum systems
- 8:12Effect transition systems
- 12:31Basic quantum protocol semantics
- 15:41Heisenberg-style semantics correctness
- 16:42Future work and verification
related talks
23mQuantum Information Effects
14mDenotational semantics for stabiliser quantum programs
22mLocal Reasoning about Probabilistic Behaviour for Classical-Quantum Programs
20mA Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantu
22mA Semantics for Quantum Loops
24mSemantics for Variational Quantum Programming
21mInteractive Proofs for Synthesizing Quantum States and Unitaries
30mOn incorrectness logic for Quantum programs