摘要
arXiv:2410.18293v2 宣告类型: 替代
摘要:尽管在概率模型检查方面取得了进展,但验证方法的可扩展性仍然有限。特别是在用中等值实例化参数化马尔可夫决策过程(MDPs)时,状态空间往往变得极其庞大。对于这种巨大的MDPs生成策略超出了现有工具的能力。我们提出了一种基于学习的方法来获得这样的巨大MDPs的合理策略。该方法的思路是使用决策树学习将模型检查小实例得到的最优策略推广到更大的实例。因此,我们的方法绕过了对大规模模型显式状态空间探索的需要,提供了一种解决状态空间爆炸问题的实用方案。我们通过在相关基准集中的定量验证模型进行广泛的实验来证明我们方法的有效性。实验结果表明,即使当模型的规模远远超出最先进的分析工具所能处理的范围时,我们的策略表现良好。