Safety Verification of Piecewise-Deterministic Markov Processes.
HSCC(2016)
摘要
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.
更多查看译文
关键词
Hybrid Systems, Verification, Sum of Squares, piecewise-deterministic Markov processes, Optimisation
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络