Modelling and Simulation of Quantum Teleportation and Dense Coding Using Predicate/Transition-Nets

Reachability analysis is one of the most successful methods used in design and validation of protocols for classical communication, whereas the predicate/transition-net formalism is one of the most appropriate formalisms for reachability analysis oriented modelling. Quantum teleportation and dense coding are non-classical communication protocols that have been widely researched in the field of quantum computing. In this article, we present predicate/transition-net models of these two protocols and use the PROD reachability analysis tool for analysing the models.