arXiv:2502.04530v1 宣告类型: 新 摘要: 传统的概率模型检验通常验证感兴趣的度量的期望值属性。这种限制可能无法捕捉系统运行中显著比例的服务质量，特别是在感兴趣的度量的概率分布由于厚尾行为或多重模态而无法很好地由其期望值表示时。最近受分布强化学习启发的工作使用离散直方图来近似整数奖励分布，但在连续奖励空间中遇到困难，并且在精确度与可扩展性之间存在挑战。我们提出了一种新颖的方法，使用厄朗混合物进行矩匹配，在离散时间马尔可夫链中处理连续和离散奖励分布。通过对矩生成函数进行解析推导高阶矩，我们的方法以理论可保证的误差来近似奖励分布，同时保持真实分布的统计特性。这种详细的分布洞察力使得基于整个奖励分布函数来制定和验证质量属性成为可能，而不仅仅是受限于其期望值。我们提供了一种理论基础来确保近似误差的有界性，并通过实验评估展示了我们方法在实际模型检查问题中的准确性和可扩展性。