💻 computer science

Multi-Objective Statistical Model Checking using Lightweight Strategy Sampling (extended version)

本文提出了一种针对多目标帕累托查询（multi-objective Pareto queries）的统计模型检测方法，该方法采用轻量级策略采样，具有用于渐近收敛的增量方案以及用于有限时间近似的启发式方法，并已在 Modest 工具集中实现与验证。

原作者： Pedro R. D'Argenio, Arnd Hartmanns, Patrick Wienhöft, Mark van Wijk

发布于 2026-07-02

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Pedro R. D'Argenio, Arnd Hartmanns, Patrick Wienhöft, Mark van Wijk

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下你是一名宇宙飞船的船长。你有两个主要目标：你想收集尽可能多的宝藏（最大化奖励），但同时你也想使用尽可能少的燃料（最小化成本）。

问题在于，这两个目标是相互冲突的。如果你为了获取更多宝藏而飞快行驶，你就会消耗更多燃料。如果你为了节省燃料而飞慢一点，你得到的宝藏就会变少。这里并不存在一条单一的“最佳”路径；相反，存在一条由所有“最佳可能权衡点”组成的曲线。在数学中，这条曲线被称为帕累托前沿（Pareto Front）。

长期以来，计算机科学家一直有一种能够完美找到这条曲线的方法，但那就像是为了寻找建造城堡的最佳位置而去数遍滩涂上的每一粒沙子一样。如果“滩涂”（计算机模型）太大，这种方法就会崩溃或耗时过久。这被称为“状态空间爆炸”。

随后，他们发明了一种更快速的方法，叫做统计模型检测（Statistical Model Checking, SMC）。与其去数每一粒沙子，不如随机抽取几把，测量它们，然后利用统计学来推测整个滩涂的样子。这种方法很快，且适用于巨大的滩涂，但直到现在，它只能检查一个目标（例如，“我能获得多少宝藏？”）。它无法处理这种复杂的“宝藏与燃料”之间的权衡关系。

这篇论文介绍了一种新的方法，利用这种快速的随机采样法来寻找这条“宝藏 vs 燃料”的曲线。以下是他们是如何实现的，我们使用了日常生活的类比：

1. “魔法骰子”策略（轻量级策略采样）

想象你有一个巨大的图书馆，里面记录了你的宇宙飞船所有可能的飞行方式。你无法读完图书馆里的每一本书。相反，你有一个“魔法骰子”（称为哈希函数）。

你通过掷骰子来挑选一个随机的飞行计划（即一个“策略”）。
你在电脑上模拟这个飞行计划，看看它消耗了多少宝藏和燃料。
因为这个骰子是“轻量级”的，你可以挑选数百万个不同的飞行计划，而不需要一台超级计算机来记住它们。你只需要一个微小的笔记（一个 32 位数字）来记录你选了哪一个计划。

2. “置信度方框”

当你模拟一个飞行计划时，你得到的不是一个完美的数字，而是一个带有一定不确定性的估计值。

这可以想象成围绕你的结果画出的一个方框。
方框的中心是你的最佳猜测。
方框的大小代表了你的确定程度。如果你运行 10 次模拟，方框就很小；如果你只运行 1 次，方框就会非常大。
该论文的数学逻辑保证了，如果你画出足够多的方框，真正的最佳结果几乎肯定就隐藏在这些方框之中。

3. 寻找曲线（帕累托前沿）

研究人员尝试了两种主要方法，利用这些方框来寻找最佳权衡曲线：

方法 A：“无尽探索者”（增量采样）
想象你是一名试图绘制山脉地图的徒步旅行者。你不会停下，而是边走边画图。

你不断挑选随机的飞行计划并画出它们的方框。
随着时间的推移，你在真实的范围周围画出了一个“底面”（下近似）和一个“顶面”（上近似）。
随着你的行走，底面和顶面会越来越接近，直到它们完美地勾勒出山脉的轮廓。
代价： 你必须永远走下去，才能得到完美的轮廓。

方法 B：“聪明猎人”（固定预算算法）
想象你只有有限的时间（比如 1 小时）来寻找最佳地点。你不能永远走下去，所以你需要聪明地寻找。论文提出了三种“狩猎策略”：

权重向量精炼（Weight Vector Refinement）： 你选择一个方向（例如，“我更看重宝藏而非燃料”），找到该方向下的最佳点，然后稍微改变方向并再次寻找。你不断精炼你的搜索过程。
固定迭代预算（Fixed Iteration Budget）： 你挑选一组飞行计划，测试它们，扔掉那些看起来很糟糕的计划，然后将剩余的时间分配给剩下的“优胜者”，以便对它们进行更仔细的测试。
固定策略预算（Fixed Strategy Budget）： 与上述方法类似，但你不仅是对优胜者进行更深入的测试，还会同时加入新的随机飞行计划，以确保你不会错过任何隐藏的珍宝。

他们发现了什么？

作者构建了一个工具（名为 modes），并在许多不同的问题上进行了测试，从智能家居的能源调度到深海潜艇的导航。

好消息： 他们的法在那些对于旧有的完美方法来说过于庞大的问题上依然有效。在旧方法需要数小时或直接崩溃的情况下，他们能在几秒钟或几分钟内找到良好的权衡曲线。
“简单”的赢家： 令人惊讶的是，最有效的策略往往是最简单的：只需挑选大量的随机飞行计划，立即扔掉那些明显很差的计划，然后用剩余的时间来测试剩下的计划。你不需要复杂的数学来剔除那些坏计划；仅仅观察原始数据就足够了。
局限性： 由于他们使用的是随机采样，在固定时间内，他们永远无法 100% 确定自己找到了绝对完美的曲线。他们只能说：“我们有 95% 的把握，真实答案就在这个区域内。”然而，对于规模巨大、极其复杂的问题，拥有 95% 的把握比完全无法解决问题要好得多。

总结

这篇论文为解决“鱼与熊掌不可兼得”类问题（例如：速度 vs 安全，或成本 vs 质量）提供了一种处理巨型计算机模型的新方法。他们并没有尝试计算每一种可能性（这对于大型系统来说是不可能的），而是使用一种聪明的随机采样技术，在消耗极少计算机内存的同时，绘制出一张非常准确的最佳权衡路径图。

技术摘要：基于轻量级策略采样的多目标统计模型检测

问题陈述

统计模型检测（SMC）是一种成熟的技术，用于验证具有大规模状态空间的概率系统，在这些系统中，穷举式的概率模型检测（PMC）会因状态空间爆炸而失效。然而，现有的 SMC 方法局限于一次评估单个属性。在许多实际场景中，例如平衡卫星电池消耗与效用，或优化热泵成本与舒适度之间的关系，决策者需要的是帕累托前沿（Pareto front）：即多个通常相互冲突的目标之间的最优权衡集合。

虽然存在多目标 PMC 算法（例如使用线性规划或值迭代），但它们需要对整个状态空间进行探索，这使得它们无法应用于具有数十亿个状态或高维目标空间的模型。此外，现有工具（如 Uppaal Stratego）仅通过词典序（lexicographic ordering）或单维度优化来处理多目标问题，无法捕捉等优先级目标之间的权衡。目前还没有一种 SMC 方法能够在保持 SMC 特有的常数内存占用的同时，计算多目标查询的帕累托前沿。

方法论

本文提出了一种基于**轻量级策略采样（Lightweight Strategy Sampling, LSS）**的首个用于多目标帕累托查询的 SMC 方法。其核心方法论包含以下组件：

1. 轻量级策略采样 (LSS)

为了处理马尔可夫决策过程（MDP）中的非确定性，且不存储每个状态的策略信息，作者使用了 LSS。LSS 不显式存储策略，而是使用一个紧凑的标识符（例如 32 位整数）和一个哈希函数，在模拟过程中确定性地解决非确定性选择。这使得能够以常数内存模拟大量的不同策略，且该内存占用与模型状态空间的大小无关。

2. 帕累托前沿的统计近似

该方法通过采样确定性策略并利用 SMC 进行评估，以获得每个目标的置信区间（CI）。

置信框（Confidence Boxes）： 对于给定的采样策略 $\sigma$ ，SMC 会在其估计的均值向量 $\hat{x}_\sigma$ 周围生成一个 $d$ 维置信框 $B_\sigma$ 。
欠近似与过近似： 这些置信框中“最悲观”顶点的凸包构成了可实现集的候选欠近似（ $\underline{C}$ ）。相反，“最乐观”的顶点则构成了候选过近似（ $\overline{C}$ ）。
多重比较： 为了确保所有置信框以概率 $\gamma$ 同时成立，作者应用了 Bonferroni 校正（联合界/union bound），将误差预算分配到各个策略和维度中。

3. 算法

论文引入了两类算法：

A. 带有收敛性的增量采样
该方案会对策略进行无限次的批次采样。它动态调整每批次的误差预算（使用因子 $f$ ），以确保在极限情况下，欠近似和过近似能够收敛到围绕真实帕累托前沿的同步置信带。在理想 LSS 的条件下，这提供了几乎处处收敛（almost sure convergence）的理论保证。

B. 固定预算采样
考虑到实际应用具有有限的时间限制，本文提出了三种启发式算法，旨在固定模拟预算内找到最佳近似：

权重向量细化 (WVR)： 通过线性标量化目标来适配多目标 PMC 技术。它根据当前近似值与当前近似值之间的距离迭代细化权重向量，并丢弃次优策略。
固定迭代预算 (FIB)： 采样初始策略集，并进行迭代式的模拟运行，在每次迭代中丢弃表现最差的策略，从而将预算集中在有潜力的候选对象上。
固定策略预算 (FSB)： 与 FIB 类似，但它确保最终留存的策略集获得均匀数量的模拟运行，通过采样新策略来替换被丢弃的策略。

策略选择启发式规则：
为了过滤策略，作者定义了几种基于样本均值和置信区间的规则（例如“简单”、“足够远”、“保守地远”）。这些规则决定了某个策略是否因在统计学上具有足够的置信度而被另一个策略所支配，从而被丢弃。

核心贡献

首个多目标 SMC： 本文提出了第一个能够近似 $d$ 个等优先级目标帕累托前沿的 SMC 框架。
常数内存： 该方法保持了 SMC 的主要优势：内存使用量相对于模型状态空间大小是常数，从而能够分析拥有数十亿个状态的模型。
统计保证： 增量方案提供了收敛到真实帕累托前沿周围置信带的理论保证。固定预算算法则提供了具有指定置信水平的统计可靠下界（欠近似）。
实现与评估： 这些技术在 Modest 工具集的 modes 模拟器中实现。作者在来自定量验证和强化学习文献的 40 个基准实例上对该方法进行了评估，并将结果与 PMC 工具 Storm 进行了对比。

实验结果

实验表明，所提出的 SMC 方法可以处理 PMC 工具（如 Storm）因状态空间爆炸或超时而无法处理的实例。

可扩展性： 对于大型模型（例如具有 $2.7 \times 10^9$ 个状态的 fruit_tree，以及具有数亿个状态的 puddle_world 变体），SMC 方法能在数秒到数分钟内成功计算出帕雷托前沿近似，而 PMC 工具则会超时或无法完成。
准确性： 对于可以获得 PMC 结果的小型模型，SMC 近似值通常与真实的帕累托前沿非常接近（例如，乘性 $\epsilon$ 接近 1 的 deep_sea 和 fruit_tree 模型）。然而，准确性存在差异；对于某些模型（如 breakable_bottles），近似值可能离真实前沿较远，这突显了采样的随机性质。
算法性能： 在固定预算算法中，结合“简单”启发式规则、并倾向于使用大量初始策略及较少单策略运行次数的 FSB（固定策略预算）配置，通常在超体积（hypervolume）结果上表现最好。
启发式规则的影响： “简单”规则（仅基于样本均值进行丢弃）通常表现最佳，这表明早期丢弃非潜力策略在测试的基准集中是有益的。

重要性与声明

作者声称这项工作弥合了 SMC 的可扩展性与多目标优化复杂性之间的关键差距。通过利用轻量级策略采样，该方法使得验证大型系统中原本难以处理的权衡问题成为可能。

论文也客观地承认了局限性：

过近似： 虽然增量方案会收敛到置信带，但固定预算算法无法在有限时间内保证获得有效的过近似，因为它们可能会错过最优策略。
策略空间： 该方法假设策略空间是有限的（通过固定大小的标识符）。虽然这在实践中是可行的，但与一般 MDP 中策略的理论无限空间相比是一个局限。
模型类别： 虽然在 MDP 上得到了验证，但只要运行几乎处处终止，该方法可以直接应用于任何支持 LSS 的模型类别，如马尔可夫自动机（Markov automata）和概率定时自动机（probabilistic timed automata）。

这项工作被视为一项基础性工作，为大规模系统中的多目标验证提供了一个实用的工具，而在这些系统中，传统的穷举方法是无法使用的。