Probabilistic model checking aims to prove whether a Markov decision process (MDP) satisfies a temporal logic specification. The underlying methods rely on an often unrealistic assumption that the MDP is precisely known. Consequently, parametric MDPs (pMDPs) extend MDPs with transition probabilities that are functions over unspecified parameters. The parameter synthesis problem is to compute an instantiation of these unspecified parameters such that the resulting MDP satisfies the temporal logic specification. We formulate the parameter synthesis problem as a quadratically constrained quadratic program (QCQP), which is nonconvex and is NP-hard to solve in general. We develop two approaches that iteratively obtain locally optimal solutions. The first approach exploits the so-called convex-concave procedure (CCP), and the second approach utilizes a sequential convex programming (SCP) method. The techniques improve the runtime and scalability by multiple orders of magnitude compared to black-box CCP and SCP by merging ideas from convex optimization and probabilistic model checking. We demonstrate the approaches on a satellite collision avoidance problem with hundreds of thousands of states and tens of thousands of parameters and their scalability on a wide range of commonly used benchmarks.


翻译:概率模型检查旨在证明Markov决定过程(MDP)是否符合时间逻辑规格。基本方法所依据的假设往往是不切实际的,即MDP是众所周知的。因此,参数 MDP(pMDPs)扩展了具有过渡概率的MDPs,而过渡概率则功能高于未指明的参数。参数合成问题是对这些未说明的参数进行即时计算,从而使由此产生的MDP符合时间逻辑规格。我们将参数合成问题作为一个四进制受限制的四进制程序(QCQP)来设计,这是一个非对立的四进制程序(QCQP),并且很难解决一般的NP。我们开发了两种迭代获得当地最佳解决方案的方法。第一种是利用所谓的convex-concave 程序(CCP),第二种是使用顺序组合程序(SCP)方法,以便计算出这些参数的速率,从而使MDP满足时间和SCP的多级,通过黑箱CCP和SCP(QQQQ)来改进运行时间和缩缩度。我们展示了卫星碰撞避免碰撞问题的方法,以千万个共同的参数和千个标准为基准。

0
下载
关闭预览

相关内容

专知会员服务
141+阅读 · 2021年3月17日
专知会员服务
52+阅读 · 2020年9月7日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
Fariz Darari简明《博弈论Game Theory》介绍,35页ppt
专知会员服务
109+阅读 · 2020年5月15日
Stabilizing Transformers for Reinforcement Learning
专知会员服务
58+阅读 · 2019年10月17日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
MIT新书《强化学习与最优控制》
专知会员服务
275+阅读 · 2019年10月9日
LibRec 精选:AutoML for Contextual Bandits
LibRec智能推荐
7+阅读 · 2019年9月19日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
Hierarchical Imitation - Reinforcement Learning
CreateAMind
19+阅读 · 2018年5月25日
Reinforcement Learning: An Introduction 2018第二版 500页
CreateAMind
11+阅读 · 2018年4月27日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
Arxiv
6+阅读 · 2021年6月24日
Arxiv
7+阅读 · 2021年5月25日
Arxiv
5+阅读 · 2018年4月22日
VIP会员
相关VIP内容
专知会员服务
141+阅读 · 2021年3月17日
专知会员服务
52+阅读 · 2020年9月7日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
Fariz Darari简明《博弈论Game Theory》介绍,35页ppt
专知会员服务
109+阅读 · 2020年5月15日
Stabilizing Transformers for Reinforcement Learning
专知会员服务
58+阅读 · 2019年10月17日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
MIT新书《强化学习与最优控制》
专知会员服务
275+阅读 · 2019年10月9日
相关资讯
LibRec 精选:AutoML for Contextual Bandits
LibRec智能推荐
7+阅读 · 2019年9月19日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
Hierarchical Imitation - Reinforcement Learning
CreateAMind
19+阅读 · 2018年5月25日
Reinforcement Learning: An Introduction 2018第二版 500页
CreateAMind
11+阅读 · 2018年4月27日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
Top
微信扫码咨询专知VIP会员