Behavior Trees (BTs) have emerged as a modular and reactive framework for robotic decision-making. However, the lack of a definitive reference for execution semantics limits their applicability in safety-critical systems. This paper contributes a solution by providing a new translation of BTs to Petri Nets (PNs) to enable verification in scenarios where the embedding context of the BT is modeled also as a PN. This ensures that safety and response properties about the overall robotic system can be assessed using state-of-the-art model checkers. Our method takes a BT, translates each node to a so-called PN Template and then composes the templates to obtain a single PN. Additionally, we introduce optimization strategies to reduce the size of the final model, improving computational efficiency while preserving verification accuracy. We report evaluation results on different case studies, including industry-related ones, demonstrating the feasibility and the scalability of our approach.