一句话：提出 ULTIMATE 框架，统一多类随机模型的表示、验证与综合，并处理模型间依赖。
概率模型检测（PMC）可分析离散/连续时间马尔可夫链、马尔可夫决策过程和随机博弈等随机模型，广泛用于验证系统可靠性与性能性质。但许多软件密集型系统需要联合分析多个相互依赖且类型不同的随机模型，现有 PMC 技术无法处理。本文提出工具支持的 ULTIMATE 框架，支持具有复杂模型依赖的异构多模型随机系统的表示、验证与综合。该框架独特地集成了多种 PMC 范式，并以一种处理模型间依赖的新型验证方法为基础，首次统一了概率与非确定性不确定性、离散与连续时间、部分可观测性，以及利用贝叶斯和频率派推断来利用系统及其上下文的领域知识和数据。大量案例研究与实验验证了该框架的通用性与有效性。
Given its ability to analyse stochastic models ranging from discrete and continuous-time Markov chains to Markov decision processes and stochastic games, probabilistic model checking (PMC) is widely used to verify system dependability and performance properties. However, modelling the behaviour of, and verifying these properties for many software-intensive systems requires the joint analysis of multiple interdependent stochastic models of different types, which existing PMC techniques and tools cannot handle. To address this limitation, we introduce a tool-supported UniversaL stochasTIc Modelling, verificAtion and synThEsis (ULTIMATE) framework that supports the representation, verification and synthesis of heterogeneous multi-model stochastic systems with complex model interdependencies. Through its unique integration of multiple PMC paradigms, and underpinned by a novel verification method for handling model interdependencies, ULTIMATE unifies—for the first time—the modelling of probabilistic and nondeterministic uncertainty, discrete and continuous time, partial observability, and the use of both Bayesian and frequentist inference to exploit domain knowledge and data about the modelled system and its context. A comprehensive suite of case studies and experiments confirm the generality and effectiveness of our novel verification framework.