Safety Verification of Piecewise-Deterministic Markov Processes
Safety Verification of Piecewise-Deterministic Markov Processes
复制标题
DOI：
10.1145/2883817.2883836
复制
发表时间：
2016-04
期刊：
影响因子：
--
通讯作者：
R. Wisniewski;Christoffer Sloth;Manuela L. Bujorianu;Nir Piterman
中科院分区：
文献类型：
--
作者：
R. Wisniewski;Christoffer Sloth;Manuela L. Bujorianu;Nir Piterman
研究了分段确定马尔可夫过程的安全性问题。这些系统具有确定性动力学和随机跳跃，其中跳跃的时间和目的地都是随机的。具体而言，我们解决了p-安全问题，在那里我们确定的初始状态的概率达到指定的不安全状态的集合是最多1 -p。基于知识的PADER的完整的发电机，我们能够开发一个系统的偏微分方程描述不安全和初始状态之间的连接。然后，我们表明，通过使用矩量法，我们可以翻译的无穷维优化问题，寻找最大的一组p-安全状态的有限维多项式优化问题。我们已经在GloptiPoly上实现了这种技术，并展示了如何将其应用于数值示例。
We consider the safety problem of piecewise-deterministic Markov processes (PDMP). These are systems that have deterministic dynamics and stochastic jumps, where both the time and the destination of the jumps are stochastic. Specifically, we solve a p-safety problem, where we identify the set of initial states from which the probability to reach designated unsafe states is at most 1 - p. Based on the knowledge of the full generator of the PDMP, we are able to develop a system of partial differential equations describing the connection between unsafe and initial states. We then show that by using the moment method, we can translate the infinite-dimensional optimisation problem searching for the largest set of p-safe states to a finite dimensional polynomial optimisation problem. We have implemented this technique on top of GloptiPoly and show how to apply it to a numerical example.