基于乐观优化的随机系统验证与参数综合
机器学习
2020-12-04 v2 形式语言与自动机理论
摘要
我们提出了一种用于连续状态空间马尔可夫链的形式化验证与参数综合的算法。这类问题涵盖由非线性和黑盒模块定义的各类自主系统与信息物理系统的设计与分析。为解决这些问题,必须针对初始状态与参数的所有选择最大化某些概率目标函数。在本文中,我们明确了使该问题可被视为多臂老虎机问题的前提假设。基于这一新视角,我们提出了一种求解该问题的算法(HOO-MB),该算法谨慎地以适当参数实例化已有的老虎机算法——分层乐观优化(Hierarchical Optimistic Optimization)。由此,我们获得了关于所提方案样本效率的理论后悔界,其依赖于平滑性、近最优维数与批量大小等关键问题参数。批量大小参数使我们能够在算法的样本效率与内存占用之间取得平衡。我们使用工具 HooVer 进行的实验表明,该方法可扩展至实际规模的问题,并且相较于随机系统验证的领先工具 PlasmaLab 通常具有更高的样本效率。具体而言,HooVer 在分析与目标函数具有陡峭斜率的模型时具有明显优势。此外,HooVer 在线性二次调节器(LQR)示例的参数综合中表现出良好的性能。
引用
@article{arxiv.1911.01537,
title = {Verification and Parameter Synthesis for Stochastic Systems using Optimistic Optimization},
author = {Negin Musavi and Dawei Sun and Sayan Mitra and Geir Dullerud and Sanjay Shakkottai},
journal= {arXiv preprint arXiv:1911.01537},
year = {2020}
}
备注
24 pages, 7 figures