PRISM 4.0 is a major update to the probabilistic model checker, adding support for quantitative verification of priced probabilistic timed automata (PTAs). These models combine probabilistic, non-deterministic, and real-time features, essential in domains like embedded systems, wireless protocols, and security. PRISM is open-source and includes new components such as an abstraction-refinement toolkit, a probabilistic model checking library, a discrete-event simulation engine, and a benchmark suite. PRISM 4.0 supports PTAs, which are finite-state automata with real-valued clocks and probabilistic transitions. It allows modeling of systems with costs or rewards, enabling analysis of properties like energy consumption. The tool supports various quantitative properties, including probabilities and expected rewards, and offers multiple verification methods like abstraction refinement and statistical model checking. Key features include support for probabilistic timed automata, a uniform modeling language, and a GUI or command-line interface. PRISM also provides optimal adversary generation for non-deterministic models and a benchmark suite for probabilistic model checking. It is available for download and is free and open-source, supporting multiple operating systems. PRISM 4.0 improves scalability and supports a broader range of models, including hybrid systems. It integrates with existing tools and offers enhanced verification techniques, making it a versatile tool for probabilistic real-time systems. The paper also discusses related tools like UPPAAL and mcpta, and highlights PRISM's contributions to the field of probabilistic model checking.PRISM 4.0 is a major update to the probabilistic model checker, adding support for quantitative verification of priced probabilistic timed automata (PTAs). These models combine probabilistic, non-deterministic, and real-time features, essential in domains like embedded systems, wireless protocols, and security. PRISM is open-source and includes new components such as an abstraction-refinement toolkit, a probabilistic model checking library, a discrete-event simulation engine, and a benchmark suite. PRISM 4.0 supports PTAs, which are finite-state automata with real-valued clocks and probabilistic transitions. It allows modeling of systems with costs or rewards, enabling analysis of properties like energy consumption. The tool supports various quantitative properties, including probabilities and expected rewards, and offers multiple verification methods like abstraction refinement and statistical model checking. Key features include support for probabilistic timed automata, a uniform modeling language, and a GUI or command-line interface. PRISM also provides optimal adversary generation for non-deterministic models and a benchmark suite for probabilistic model checking. It is available for download and is free and open-source, supporting multiple operating systems. PRISM 4.0 improves scalability and supports a broader range of models, including hybrid systems. It integrates with existing tools and offers enhanced verification techniques, making it a versatile tool for probabilistic real-time systems. The paper also discusses related tools like UPPAAL and mcpta, and highlights PRISM's contributions to the field of probabilistic model checking.