TY - JOUR

T1 - p-Safe Analysis of Stochastic Hybrid Processes

AU - Wisniewski, Rafal

AU - Bujorianu, Luminita Manuela

AU - Sloth, Christoffer

PY - 2020/12

Y1 - 2020/12

N2 - We develop a method for determining whether a stochastic system is safe, i.e., whether its trajectories reach unsafe states. Specifically, we define and solve a probabilistic safety problem for Markov processes. Based on the knowledge of the extended generator, we are able to develop an evolution equation, as a system of integral equations, describing the connection between unsafe and initial states. Subsequently, using the moment method, we approximate the infinite-dimensional optimization problem searching for the largest set of safe states by a finite-dimensional polynomial optimization problem. In particular, we address the above safety problem to a special class of stochastic hybrid processes, namely piecewise-deterministic Markov processes. These are characterized by deterministic dynamics and stochastic jumps, where both the time and the destination of the jumps are stochastic. In addition, the jumps can be both spontaneous (in the style of a Poisson process) and forced (governed by guards). In this case, the extended generator of this process and its corresponding martingale problem turn out to be defined on a rather restricted domain. To circumvent this difficulty, we bring the generalized differential formula of this process into the evolution equation and, subsequently, formulate a polynomial optimization.

AB - We develop a method for determining whether a stochastic system is safe, i.e., whether its trajectories reach unsafe states. Specifically, we define and solve a probabilistic safety problem for Markov processes. Based on the knowledge of the extended generator, we are able to develop an evolution equation, as a system of integral equations, describing the connection between unsafe and initial states. Subsequently, using the moment method, we approximate the infinite-dimensional optimization problem searching for the largest set of safe states by a finite-dimensional polynomial optimization problem. In particular, we address the above safety problem to a special class of stochastic hybrid processes, namely piecewise-deterministic Markov processes. These are characterized by deterministic dynamics and stochastic jumps, where both the time and the destination of the jumps are stochastic. In addition, the jumps can be both spontaneous (in the style of a Poisson process) and forced (governed by guards). In this case, the extended generator of this process and its corresponding martingale problem turn out to be defined on a rather restricted domain. To circumvent this difficulty, we bring the generalized differential formula of this process into the evolution equation and, subsequently, formulate a polynomial optimization.

KW - Markov processes

KW - martingale problem

KW - moment method

KW - optimization

KW - safety verification

KW - stochastic hybrid systems

UR - http://www.scopus.com/inward/record.url?scp=85093964010&partnerID=8YFLogxK

U2 - 10.1109/TAC.2020.2972789

DO - 10.1109/TAC.2020.2972789

M3 - Journal article

VL - 65

SP - 5220

EP - 5235

JO - I E E E Transactions on Automatic Control

JF - I E E E Transactions on Automatic Control

SN - 0018-9286

IS - 12

M1 - 8989815

ER -