This paper introduces PRISM 4.0, a major update to the PRISM probabilistic model checker, which adds support for quantitative verification of (priced) probabilistic timed automata (PTAs). PTAs are a natural model for systems with probabilistic, nondeterministic, and real-time characteristics, widely used in embedded controllers, wireless communication protocols, and randomized security protocols. PRISM 4.0 includes several new components: an extensible toolkit for building and refining abstractions of probabilistic models, an explicit-state probabilistic model checking library, a discrete-event simulation engine for statistical model checking, support for generating optimal adversaries/strategies, and a benchmark suite. The paper also provides an overview of the current functionality of PRISM, including the modelling and verification techniques for PTAs, and discusses related tools and the technical details of PRISM's implementation.This paper introduces PRISM 4.0, a major update to the PRISM probabilistic model checker, which adds support for quantitative verification of (priced) probabilistic timed automata (PTAs). PTAs are a natural model for systems with probabilistic, nondeterministic, and real-time characteristics, widely used in embedded controllers, wireless communication protocols, and randomized security protocols. PRISM 4.0 includes several new components: an extensible toolkit for building and refining abstractions of probabilistic models, an explicit-state probabilistic model checking library, a discrete-event simulation engine for statistical model checking, support for generating optimal adversaries/strategies, and a benchmark suite. The paper also provides an overview of the current functionality of PRISM, including the modelling and verification techniques for PTAs, and discusses related tools and the technical details of PRISM's implementation.