This paper presents the use of P systems and π-calculus to model interacting molecular entities and how they are translated into a probabilistic and symbolic model checker called PRISM.