Metric Interval Temporal Logic ( \(\textsf {MITL} \) ) is a popular formalism for specifying properties of reactive systems with timing constraints. Existing approaches to using \(\textsf {MITL} \) in verification tasks, however, have notable drawbacks: they either support only limited fragments of the logic (the future only fragment \(\textsf {MITL} [\textsf{Fut}]\) ) or allow for only incomplete verification. This paper introduces \(\textsc {MightyPPL} \) , a new tool for translating formulae in Metric Interval Temporal Logic with Past and Pnueli modalities ( \(\textsf {MITPPL} \) ) over the pointwise semantics into timed automata, enabling satisfiability and model checking of this expressive specification logic over both finite and infinite timed words. \(\textsc {MightyPPL} \) optimises performance via specialised constructions for simple cases, a novel symbolic transition encoding, and a symmetry reduction technique that yields an exponential improvement in reachable discrete states. The tool generates language-equivalent automata compatible with back-ends such as Uppaal, TChecker, and LTSmin. Our evaluation demonstrates that \(\textsc {MightyPPL} \) significantly outperforms the state-of-the-art tool \(\textsc {MightyL} \) on future-only fragments and across various benchmarks.