Affiliations: Space Systems Finland Ltd., Kappelitie 6, FI-02200
Espoo, Finland. kimmo.varpaaniemi@kolumbus.fi | Laboratory for Theoretical Computer Science, Helsinki
University of Technology, P.O. Box 5400, FI-02015 TKK, Finland.
leo.ojala@tkk.fi
Note: [] Address for correspondence: Space Systems Finland Ltd.,
Kappelitie 6, FI-02200 Espoo, Finland
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.
