Abstract
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/transitionnet models of these two protocols and use the PROD reachability analysis tool for analysing the models.
Get full access to this article
View all access options for this article.