pith. sign in

arxiv: 2604.23756 · v1 · submitted 2026-04-26 · 💻 cs.LO

Verification of Quantum Protocols Adopting Physically Admissible Schedulers

Lorenzo Ceragioli , Fabio Gadducci , Giuseppe Lomurno , Gabriele Tedeschi This is my paper

Pith reviewed 2026-05-08 05:05 UTC · model grok-4.3

classification 💻 cs.LO
keywords quantum process calculusphysically admissible schedulersbisimilarityquantum protocolsverificationconcurrencynon-determinism
0
0 comments X

The pith

A process calculus with physically admissible schedulers verifies quantum protocols by aligning bisimilarity with quantum observations.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces lqCCS, a process calculus for modeling quantum communication protocols that include concurrency and non-determinism. It defines a semantics using distributions over states, restricted by physically admissible schedulers to avoid non-deterministic behaviors that do not occur in real quantum systems. This allows for a notion of bisimilarity that correctly equates processes that are indistinguishable in quantum mechanics, such as those acting on mixtures of states. The work shows that this equivalence is a congruence for parallel composition and is decidable for many processes, enabling verification of actual protocols.

Core claim

lqCCS provides a semantics in terms of distributions where physically admissible schedulers constrain probabilistic composition and forbid ill-defined non-deterministic moves. A scheduled version of saturated bisimilarity is defined, and its adequacy is shown by lifting the quantum mechanics result that processes on indistinguishable mixtures are equivalent. An alternative semantics using quantum probability distributions yields a labelled bisimilarity that is a congruence with respect to the parallel operator, enabling compositional reasoning.

What carries the argument

The central object is lqCCS with its distribution semantics constrained by physically admissible schedulers, which select only physically allowed probabilistic resolutions of non-determinism while preserving modeling power for real protocols.

Load-bearing premise

The notion of physically admissible schedulers accurately captures the observational properties of physical quantum systems.

What would settle it

A pair of processes that the bisimilarity considers equivalent but which produce distinguishable outcomes in a real quantum experiment, or the reverse, would falsify the claim.

Figures

Figures reproduced from arXiv: 2604.23756 by Fabio Gadducci, Gabriele Tedeschi, Giuseppe Lomurno, Lorenzo Ceragioli.

Figure 1
Figure 1. Figure 1: The Quantum Coin Flip protocol QCF, modelled using lqCCS. 2.2 Modelling and Analysing the Quantum Coin Flip Protocol To exemplify our approach, we use a non-trivial concrete case, the Quantum Coin Flip protocol [Bennet and Brassard 2014], which is also a basis for implementing the more involved Quantum Byzantine Agreement [Ben-Or and Hassidim 2005]. The objective of the protocol is to randomly select a win… view at source ↗
Figure 2
Figure 2. Figure 2: Two malicious versions of Alice, modelled using lqCCS. view at source ↗
Figure 3
Figure 3. Figure 3: Typing rules for lqCCS are intended to explicitly name the non-deterministic choices that a scheduler can perform when running a process. In the following, we assume that processes come with their associated tags. The visibility of qubits is enforced explicitly through the linear type system in view at source ↗
Figure 4
Figure 4. Figure 4: Rules of lqCCS semantics. quantum state 𝜌 is a density operator in DO (HΣ). The type system is extended to configurations and distributions by considering the qubits of the underlying quantum state. Let Σ𝜌 be the set of qubits appearing in 𝜌. Definition 4.3 (Configuration Typing). Let ⌊︁𝜌, 𝑃}︁ ∈ Conf , with 𝑃 typed and Σ𝑃 ⊆ Σ𝜌 , then we let (Σ𝜌, Σ𝑃 ) ⊢ ⌊︁𝜌, 𝑃}︁. Let Δ ∈ D≤ (Conf ), then we let (Σ, Σ ′ ) ⊢ … view at source ↗
Figure 5
Figure 5. Figure 5: Semantics of the quantum lottery process. view at source ↗
Figure 6
Figure 6. Figure 6: Lifted semantics of the quantum lottery process. view at source ↗
Figure 7
Figure 7. Figure 7: Indistinguishable qubit sources Δ01 and Δ± are distinguished by the context 𝐵[ · ]. • whenever 𝐵[Δ] 𝜏 • Δ ′ , there exists Θ ′ such that 𝐵[Θ] 𝜏 • Θ ′ and Δ ′ R Θ ′ ; • whenever 𝐵[Θ] 𝜏 • Θ ′ , there exists Δ ′ such that 𝐵[Δ] 𝜏 • Δ ′ and Δ ′ R Θ ′ . Let unscheduled saturated bisimilarity, denoted ≃•, be the largest unscheduled saturated bisimulation. We now compare the bisimilarity above with the prescriptio… view at source ↗
Figure 8
Figure 8. Figure 8: Scheduled semantics of the protocol described in view at source ↗
Figure 9
Figure 9. Figure 9: Rules of Density Operator Semantics. We maintain the same notation: we write 𝜖 for the empty distribution associating each element of 𝑆 with the matrix O; we let 𝜌 • 𝑠 be a distribution such that (𝜌 • 𝑠) (𝑠) = 𝜌 and (𝜌 • 𝑠) (𝑠 ′ ) = O if 𝑠 ≠ 𝑠 ′ ; finally, we write Í 𝑖∈𝐼 𝑝𝑖 • 𝔇𝑖 for the distribution such that ( Í 𝑖∈𝐼 𝑝𝑖 • 𝔇𝑖) (𝑠) = Í 𝑖∈𝐼 𝑝𝑖𝔇𝑖(𝑠), with {𝑝𝑖 }𝑖∈𝐼 a finite set of non-negatives reals and Í 𝑖∈𝐼 … view at source ↗
read the original abstract

Reliable verification techniques for quantum communication protocols are of paramount importance, given their high implementation cost and critical contexts of application. Extensions of process calculi have been proposed, together with various notions of behavioural equivalence. However, their standard probabilistic models turn out to introduce some non-deterministic capabilities not aligned with the observational properties of physical quantum systems, leading to bisimilarity notions that distinguish physically equivalent processes. Nonetheless, non-deterministic features are fundamental to account for inputs, environments and adversarial behaviour. To address this issue, we propose lqCCS, a process calculus that integrates concurrency, non-determinism and quantum capabilities. We introduce a novel semantics in terms of distributions, where explicit physically admissible schedulers constrain probabilistic composition and forbid ill-defined non-deterministic moves, while preserving the expressivity needed to model real-world protocols. We investigate a scheduled version of saturated bisimilarity, pairing two processes if no observer can tell them apart, and we verify its adequacy by lifting a known result from quantum mechanics to lqCCS: equivalent processes acting on indistinguishable mixtures of quantum states are correctly recognized as bisimilar. Finally, we give an alternative semantics and a labelled bisimilarity based on a quantum generalization of probability distributions. This characterizes our behavioural equivalence as a congruence with respect to the parallel operator, enabling compositional reasoning without the need to explicitly check all possible contexts. We describe a rich class of lqCCS processes for which equivalence is decidable using standard techniques, and we analyse real-world quantum communication protocols.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 3 minor

Summary. The paper introduces lqCCS, a process calculus integrating concurrency, non-determinism and quantum capabilities. It defines a novel distribution semantics employing physically admissible schedulers that constrain probabilistic composition and eliminate ill-defined non-deterministic transitions while retaining expressivity for protocol modelling. The work studies a scheduled saturated bisimilarity, establishes its adequacy by lifting a standard quantum-mechanics result on indistinguishable mixtures, supplies an alternative labelled semantics based on a quantum generalisation of probability distributions that characterises the equivalence as a congruence for parallel composition, proves decidability for a rich class of processes, and applies the framework to real-world quantum communication protocols.

Significance. If the adequacy and congruence results hold, the contribution is significant for quantum protocol verification. It directly addresses the mismatch between standard probabilistic process models and quantum observational equivalence while preserving the non-determinism required for inputs, environments and adversaries. Notable strengths are the explicit scheduler construction, the lifting argument from quantum mechanics, the labelled-bisimulation characterisation that enables compositional reasoning, the decidability result, and the concrete protocol analysis.

major comments (1)
  1. [Adequacy section (around the lifting argument)] The adequacy theorem (lifting the quantum-mechanics indistinguishability result) is load-bearing for the central claim that scheduled saturated bisimilarity correctly identifies physically equivalent processes. The manuscript should state the precise hypotheses on the schedulers and on the quantum states under which the lifting is valid, and should exhibit at least one concrete pair of processes that are distinguished by ordinary bisimilarity but identified once schedulers are imposed.
minor comments (3)
  1. [Decidability section] The abstract and introduction refer to 'a rich class of lqCCS processes for which equivalence is decidable using standard techniques'; the precise syntactic restrictions defining this class and the decision procedure should be stated explicitly, preferably with a complexity bound.
  2. [Preliminaries and semantics sections] Notation for distributions and scheduler application is introduced without a consolidated table of symbols; adding such a table would improve readability when comparing the two semantics.
  3. [Related work] The paper should include a short comparison table or paragraph contrasting lqCCS schedulers with the treatment of non-determinism in prior quantum process calculi (e.g., qCCS variants).

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the constructive review and the recommendation of minor revision. The comment on the adequacy section is helpful, and we will incorporate the requested clarifications to make the lifting argument more precise and illustrative.

read point-by-point responses

  1. Referee: [Adequacy section (around the lifting argument)] The adequacy theorem (lifting the quantum-mechanics indistinguishability result) is load-bearing for the central claim that scheduled saturated bisimilarity correctly identifies physically equivalent processes. The manuscript should state the precise hypotheses on the schedulers and on the quantum states under which the lifting is valid, and should exhibit at least one concrete pair of processes that are distinguished by ordinary bisimilarity but identified once schedulers are imposed.

    Authors: We agree that explicit hypotheses and a concrete example will strengthen the presentation. In the revised manuscript we will state that the lifting holds for physically admissible schedulers (those whose resolution of non-determinism respects the linearity of quantum operations, the probabilistic outcomes of measurements, and the no-cloning theorem) and for quantum states that are indistinguishable mixtures in the sense of the underlying quantum-mechanics theorem (i.e., states ρ and σ such that Tr(Oρ) = Tr(Oσ) for every observable O). We will also insert a concrete pair of processes: let P perform a non-deterministic choice between two unitaries U1 and U2 on a qubit, while Q performs the same choice but with the roles of U1 and U2 swapped; under ordinary bisimilarity the processes are distinguished by the different transition labels, yet under any admissible scheduler the resulting distributions coincide because the mixtures are physically indistinguishable. This example will be placed immediately after the statement of the adequacy theorem. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation self-contained via external QM fact

full rationale

The paper defines lqCCS, its distribution semantics with physically admissible schedulers, scheduled saturated bisimilarity, and an alternative labelled semantics directly from the core syntax and rules. Adequacy is shown by lifting a standard quantum-mechanics result on indistinguishable mixtures to the new setting; this is an external fact applied after the definitions are given, not a self-referential reduction. Decidability for a subclass follows from standard process-calculus techniques. No equations or claims reduce the central results to fitted parameters, self-definitions, or author-only citations.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 2 invented entities

The central claims rest on the new definition of physically admissible schedulers and the lifting of a quantum mechanics result; these are introduced without external independent evidence beyond the paper itself.

axioms (2)
  • standard math Standard definitions and properties of bisimilarity and process semantics from classical process calculi.
    The paper builds directly on extensions of process calculi and behavioural equivalence notions.
  • domain assumption Observational properties of physical quantum systems for indistinguishable mixtures of quantum states.
    Adequacy is shown by lifting a known result from quantum mechanics to the lqCCS setting.
invented entities (2)
  • lqCCS process calculus no independent evidence
    purpose: Integrates concurrency, non-determinism and quantum capabilities under physically admissible schedulers.
    Newly proposed framework in the paper.
  • physically admissible schedulers no independent evidence
    purpose: Constrain probabilistic composition and forbid ill-defined non-deterministic moves while preserving expressivity.
    Core novel mechanism introduced to align with physical quantum observations.

pith-pipeline@v0.9.0 · 5574 in / 1357 out tokens · 52847 ms · 2026-05-08T05:05:54.367448+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

46 extracted references · 21 canonical work pages

  1. [1]

    doi:10.1006/inco.1998.2740 Miguel E

    A Calculus for Cryptographic Protocols: The Spi Calculus.Information and Computation148, 1 (1999), 1–70. doi:10.1006/inco.1998.2740 Miguel E. Andrés, Catuscia Palamidessi, Peter van Rossum, and Ana Sokolova

    work page doi:10.1006/inco.1998.2740 1999

  2. [2]

    Ebrahim Ardeshir-Larijani, Simon J

    Information Hiding in Probabilistic Concurrent Systems.Theoretical Computer Science412, 28 (2011), 3072–3089. Ebrahim Ardeshir-Larijani, Simon J. Gay, and Rajagopal Nagarajan

    2011

  3. [3]

    Automated Equivalence Checking of Concurrent Quantum Systems.ACM Trans. Comput. Logic19, 4, Article 28 (Nov. 2018), 32 pages. doi:10.1145/3231597 Michael Ben-Or and Avinatan Hassidim

    work page doi:10.1145/3231597 2018

  4. [4]

    InProceedings of the Thirty-Seventh Annual ACM Symposium on Theory of Computing(Baltimore, MD, USA)(STOC ’05)

    Fast quantum byzantine agreement. InProceedings of the Thirty-Seventh Annual ACM Symposium on Theory of Computing(Baltimore, MD, USA)(STOC ’05). Association for Computing Machinery, New York, NY, USA, 481–485. doi:10.1145/1060590.1060662 Charles H. Bennet and Gilles Brassard

    work page doi:10.1145/1060590.1060662

  5. [5]

    Quantum cryptography: Public key distribution and coin tossing,

    Quantum cryptography: Public key distribution and coin tossing.Theoretical Computer Science560 (2014), 7–11. doi:10.1016/j.tcs.2014.05.025 Theoretical Aspects of Quantum Cryptography – celebrating 30 years of BB84. Charles H. Bennett, Gilles Brassard, Claude Crépeau, Richard Jozsa, Asher Peres, and William K. Wootters

    work page doi:10.1016/j.tcs.2014.05.025 2014

  6. [6]

    Teleporting an unknown quantum state via dual classical and E instein-Podolsky-Rosen channels.Physical Review Letters70 (1993), 1895–1899. Issue

    1993

  7. [7]

    Communication via one- and two-particle operators on Einstein-P odolsky-Rosen states.Physical Review Letters69 (1992), 2881–2884. Issue

    1992

  8. [8]

    Filippo Bonchi, Alexandra Silva, and Ana Sokolova

    A General Theory of Barbs, Contexts, and Labels.ACM Transactions on Computational Logic15, 4 (2014), 1–27. Filippo Bonchi, Alexandra Silva, and Ana Sokolova

    2014

  9. [9]

    InCONCUR 2017 (LIPIcs, Vol

    The Power of Convex Algebras. InCONCUR 2017 (LIPIcs, Vol. 85), Roland Meyer, Uwe Nestmann, and Marc Herbstritt (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 23:1–23:18. Gilles Brassard

    2017

  10. [10]

    Quantum Communication Complexity,

    Quantum communication complexity.Foundations of Physics33, 11 (2003), 1593–1616. doi:10.1023/A:1026009100467 Ran Canetti, Ling Cheung, Dilsun Kirli Kaynar, Moses D. Liskov, Nancy A. Lynch, Olivier Pereira, and Roberto Segala

    work page doi:10.1023/a:1026009100467 2003

  11. [11]

    InDISC 2006 (LNCS, Vol

    Time-Bounded Task-PIOAs: A Framework for Analyzing Security Protocols. InDISC 2006 (LNCS, Vol. 4167), Shlomi Dolev (Ed.). Springer, 238–253. Lorenzo Ceragioli, Elena Di Lavore, Giuseppe Lomurno, and Gabriele Tedeschi

    2006

  12. [12]

    2025), 249–269

    A Coalgebraic Model of Quantum Bisimulation.Electronic Proceedings in Theoretical Computer Science429 (Sept. 2025), 249–269. doi:10.4204/eptcs.429.14 Lorenzo Ceragioli, Fabio Gadducci, Giuseppe Lomurno, and Gabriele Tedeschi. 2024a. Effect Semantics for Quantum Process Calculi. InCONCUR 2024 (LIPIcs, Vol. 311), Rupak Majumdar and Alexandra Silva (Eds.). S...

    work page doi:10.4204/eptcs.429.14 2025

  13. [13]

    InFOSSACS 2009 (LNCS, Vol

    Bisimulation for Demonic Schedulers. InFOSSACS 2009 (LNCS, Vol. 5504), Luca de Alfaro (Ed.). Springer, 318–332. Manuscript submitted to ACM Verification of Quantum Protocols Adopting Physically Admissible Schedulers 37 Konstantinos Chatzikokolakis and Catuscia Palamidessi

    2009

  14. [14]

    InCONCUR 2007 (LNCS, Vol

    Making Random Choices Invisible to the Scheduler. InCONCUR 2007 (LNCS, Vol. 4703), Luís Caires and Vasco Thudichum Vasconcelos (Eds.). Springer, 42–58. Timothy A. S. Davidson. 2012.Formal Verification Techniques Using Quantum Process Calculus. Ph. D. Dissertation. University of Warwick. Timothy A. S. Davidson, Simon J. Gay, Hynek Mlnarik, Rajagopal Nagara...

    2007

  15. [15]

    Model Checking for Communicating Quantum Processes.Int. J. Unconv. Comput.8, 1 (2012), 73–98. http://www.oldcitypublishing.com/journals/ijuc-home/ijuc-issue-contents/ijuc-volume-8- number-1-2012/ijuc-8-1-p-73-98/ Yuxin Deng

    2012

  16. [16]

    InCONCUR 2018 (LIPIcs, Vol

    Bisimulations for Probabilistic and Quantum Processes. InCONCUR 2018 (LIPIcs, Vol. 118), Sven Schewe and Lijun Zhang (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2:1–2:14. Yuxin Deng and Yuan Feng

    2018

  17. [17]

    InTCS 2012 (LNCS, Vol

    Open Bisimulation for Quantum Processes. InTCS 2012 (LNCS, Vol. 7604), Jos C. M. Baeten, Thomas Ball, and Frank S. de Boer (Eds.). Springer, 119–133. Yuan Feng, Yuxin Deng, and Mingsheng Ying

    2012

  18. [18]

    doi:10.1145/2579818 Yuan Feng, Runyao Duan, Zhengfeng Ji, and Mingsheng Ying

    Symbolic Bisimulation for Quantum Processes.ACM Transactions on Computational Logic15, 2 (2014), 14:1–14:32. doi:10.1145/2579818 Yuan Feng, Runyao Duan, Zhengfeng Ji, and Mingsheng Ying

    work page doi:10.1145/2579818 2014

  19. [19]

    doi:10.1016/j.ic.2007.08.001 Yuan Feng, Runyao Duan, and Mingsheng Ying

    Probabilistic Bisimulations for Quantum Processes.Information and Computation205, 11 (2007), 1608–1639. doi:10.1016/j.ic.2007.08.001 Yuan Feng, Runyao Duan, and Mingsheng Ying

    work page doi:10.1016/j.ic.2007.08.001 2007

  20. [20]

    Yuan Feng and Mingsheng Ying

    Bisimulation for Quantum Processes.ACM Transactions on Programming Languages and Systems 34, 4 (2012), 17:1–17:43. Yuan Feng and Mingsheng Ying

    2012

  21. [21]

    InCONCUR 2015 (LIPIcs, Vol

    Toward Automatic Verification of Quantum Cryptographic Protocols. InCONCUR 2015 (LIPIcs, Vol. 42), Luca Aceto and David de Frutos-Escrig (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 441–455. Fei Gao, SuJuan Qin, Wei Huang, and QiaoYan Wen

    2015

  22. [22]

    Quantum Private Query: A New Kind of Practical Quantum Cryptographic Protocol.Science China Physics, Mechanics & Astronomy62, 7 (2019), 70301. Simon J. Gay and Rajagopal Nagarajan

    2019

  23. [23]

    InPOPL 2005, Jens Palsberg and Martin Abadi (Eds.)

    Communicating quantum processes. InPOPL 2005, Jens Palsberg and Martin Abadi (Eds.). ACM, 145–157. Simon J. Gay and Rajagopal Nagarajan

    2005

  24. [24]

    doi:10.1017/S0960129506005263 Simon J

    Types and Typechecking for Communicating Quantum Processes.Mathematical Structures in Computer Science16, 3 (2006), 375–406. doi:10.1017/S0960129506005263 Simon J. Gay, Rajagopal Nagarajan, and Nikolaos Papanikolaou

    work page doi:10.1017/s0960129506005263 2006

  25. [25]

    https://api.semanticscholar.org/CorpusID:6622187 Simon J

    Probabilistic Model-Checking of Quantum Protocols.ArXivabs/quant-ph/0504007 (2005). https://api.semanticscholar.org/CorpusID:6622187 Simon J. Gay, Rajagopal Nagarajan, and Nikolaos Papanikolaou

    work page arXiv 2005

  26. [26]

    InComputer Aided Verification, Aarti Gupta and Sharad Malik (Eds.)

    QMC: A Model Checker for Quantum Systems. InComputer Aided Verification, Aarti Gupta and Sharad Malik (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 543–547. Teiko Heinosaari and Mário Ziman. 2011.The Mathematical Language of Quantum Theory: From Uncertainty to Entanglement. Cambridge University Press. Matthew Hennessy

    2011

  27. [27]

    doi:10.1007/BF01642508 Matthew Hennessy

    A Proof System for Communicating Processes with Value-Passing.Formal Aspects of Computing3, 4 (1991), 346–366. doi:10.1007/BF01642508 Matthew Hennessy

    work page doi:10.1007/bf01642508 1991

  28. [28]

    Exploring Probabilistic Bisimulations, Part I.Formal Aspects of Computing24, 4-6 (2012), 749–768. C. A. R. Hoare

    2012

  29. [29]

    ACM21, 8 (Aug

    Communicating sequential processes.Commun. ACM21, 8 (Aug. 1978), 666–677. doi:10.1145/359576.359585 H. J. Kimble

    work page doi:10.1145/359576.359585 1978

  30. [30]

    The quantum internet,

    The Quantum Internet.Nature453, 7198 (2008), 1023–1030. doi:10.1038/nature07127 Takahiro Kubota, Yoshihiko Kakutani, Go Kato, Yasuhito Kawano, and Hideki Sakurada

    work page doi:10.1038/nature07127 2008

  31. [31]

    InFCS 2012, Hamid R

    Application of a Process Calculus to Security Proofs of Quantum Protocols. InFCS 2012, Hamid R. Arabnia, George A. Gravvanis, and Ashu M. G. Solo (Eds.). CSREA Press, 141–147. Takahiro Kubota, Yoshihiko Kakutani, Go Kato, Yasuhito Kawano, and Hideki Sakurada

    2012

  32. [32]

    Marie Lalire

    Semi-Automated Verification of Security Proofs of Quantum Cryptographic Protocols.Journal of Symbolic Computation73 (2016), 192–220. Marie Lalire

    2016

  33. [33]

    Marie Lalire and Philippe Jorrand

    Relations among quantum processes: Bisimilarity and congruence.Mathematical Structures in Computer Science16, 3 (2006), 407–428. Marie Lalire and Philippe Jorrand

    2006

  34. [34]

    CoRRquant-ph/0407005 (2004)

    A Process Algebraic Approach to Concurrent and Distributed Quantum Computation: Operational Semantics. CoRRquant-ph/0407005 (2004). Ivan Lanese, Ugo Dal Lago, and Vikraman Choudhury

    work page arXiv 2004

  35. [35]

    InSoftware Engineering and Formal Methods - 22nd International Conference, SEFM 2024, A veiro, Portugal, November 6-8, 2024, Proceedings (Lecture Notes in Computer Science, Vol

    Towards Quantum Multiparty Session Types. InSoftware Engineering and Formal Methods - 22nd International Conference, SEFM 2024, A veiro, Portugal, November 6-8, 2024, Proceedings (Lecture Notes in Computer Science, Vol. 15280), Alexandre Madeira and Alexander Knapp (Eds.). Springer, 385–403. doi:10.1007/978-3-031-77382-2_22 Kim G. Larsen and Arne Skou

    work page doi:10.1007/978-3-031-77382-2_22 2024

  36. [36]

    doi:10.1016/0890- 5401(91)90030-6 A

    Bisimulation through Probabilistic Testing.Information and Computation94, 1 (1991), 1–28. doi:10.1016/0890- 5401(91)90030-6 A. G. J. MacFarlane, Jonathan P. Dowling, and Gerard J. Milburn

    work page doi:10.1016/0890- 1991

  37. [37]

    doi:10.1098/rsta.2003.1227 arXiv:https://royalsocietypublishing.org/rsta/article-pdf/361/1809/1655/323777/rsta.2003.1227.pdf Robin Milner

    Quantum technology: the second quantum revolution.Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences361, 1809 (06 2003), 1655–1674. doi:10.1098/rsta.2003.1227 arXiv:https://royalsocietypublishing.org/rsta/article-pdf/361/1809/1655/323777/rsta.2003.1227.pdf Robin Milner. 1980.A Calculus of Communicating Syste...

    work page doi:10.1098/rsta.2003.1227 2003

  38. [38]

    Lecture Notes in Computer Science 92, Springer, doi:10.1007/3-540-10235-3

    Springer. doi:10.1007/3-540-10235-3 Michael A. Nielsen and Isaac L. Chuang. 2010.Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press. Damien Pous and Davide Sangiorgi

    work page doi:10.1007/3-540-10235-3 2010

  39. [39]

    doi:10.1088/2058-9565/aa6aca Manuscript submitted to ACM 38 Ceragioli et al

    The European quantum technologies flagship programme.Quantum Science and Technology2, 3 (jun 2017), 030501. doi:10.1088/2058-9565/aa6aca Manuscript submitted to ACM 38 Ceragioli et al. Shraddha Singh, Mina Doosti, Natansh Mathur, Mahshid Delavar, Atul Mantri, Harold Ollivier, and Elham Kashefi

    work page doi:10.1088/2058-9565/aa6aca 2017

  40. [40]

    arXiv:2310.12780 Lei Song, Yuan Feng, and Lijun Zhang

    Towards a Unified Quantum Protocol Framework: Classification, Implementation, and Use Cases. arXiv:2310.12780 Lei Song, Yuan Feng, and Lijun Zhang

    work page arXiv

  41. [41]

    InAAMAS 2015, Gerhard Weiss, Pinar Yolum, Rafael H

    Decentralized Bisimulation for Multiagent Systems. InAAMAS 2015, Gerhard Weiss, Pinar Yolum, Rafael H. Bordini, and Edith Elkind (Eds.). ACM, 209–217. R. J. van Glabbeek

    2015

  42. [42]

    InCONCUR ’90 Theories of Concurrency: Unification and Extension, J

    The linear time - branching time spectrum. InCONCUR ’90 Theories of Concurrency: Unification and Extension, J. C. M. Baeten and J. W. Klop (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 278–297. Marco Vitale. 2022.Verification of Quantum Bit Commitment Protocols using Bisimulation Techniques. Ph. D. Dissertation. https://amslaurea.unibo.it/id/ ep...

    2022

  43. [43]

    Branching bisimulation semantics for quantum processes.Inform. Process. Lett.186 (2024), 106492. doi:10.1016/j.ipl.2024.106492 Peiying Zhang, Ning Chen, Shigen Shen, Shui Yu, Sheng Wu, and Neeraj Kumar

    work page doi:10.1016/j.ipl.2024.106492 2024

  44. [44]

    Future Quantum Communications and Networking: A Review and Vision.IEEE Wireless Communications31, 1 (2024), 141–148. Manuscript submitted to ACM Verification of Quantum Protocols Adopting Physically Admissible Schedulers 39 A Proofs Probability Distributions Lemma A.1.For any Δ,Θ∈ D (𝑆) and relation R ⊆𝑆× D (𝑆) , Δllift(R)Θ if and only if there is a finit...

    2024

  45. [45]

    By linearity of 𝜏 𝑠 and by definition of lc, 𝐵[Θ] 𝜏 𝑠 Í 𝑖∈𝐼 𝑝𝑖 •Θ′ 𝑖 =Θ ′ where |Θ′ | must be less than one andΔ ′ lc(R)Θ ′

    Since Δ𝑖 RΘ 𝑖, for all 𝑖∈𝐼 there exists Θ′ 𝑖 such that 𝐵[Θ 𝑖 ] 𝜏 𝑠 Θ′ 𝑖. By linearity of 𝜏 𝑠 and by definition of lc, 𝐵[Θ] 𝜏 𝑠 Í 𝑖∈𝐼 𝑝𝑖 •Θ′ 𝑖 =Θ ′ where |Θ′ | must be less than one andΔ ′ lc(R)Θ ′. The argument is symmetric for the last condition.□ Manuscript submitted to ACM 46 Ceragioli et al. Lemma C.7 (Bis𝑏-compatible).LetR ⊆ D ≤ (Conf) × D ≤ (Conf).B...

    2011

  46. [46]

    □ Theorem D.8.∼ 𝑝 ⊆ ≃. Proof. It is sufficient to show that ∼𝑝 is a saturated bisimulation up-to lc◦ B. Assume Δ∼ 𝑝 Θ. To see that |Δ| = |Θ| it is sufficient to notice that𝑒𝑛𝑣(Δ)=𝑒𝑛𝑣(Θ), by definition of∼ 𝑝, and that |Δ| =𝑡𝑟(𝑒𝑛𝑣(Δ))for anyΔ. We now show that for all 𝐵[ · ],Δ,Θ,Δ ′, if Δ∼ 𝑝 Θ and 𝐵[Δ] 𝜏 𝑠 Δ′ then Θ′ exists such that 𝐵[Θ] 𝜏 𝑠 Θ′ and Δ′ lc(B...

    2007