Safety Verification of Continuous-Space Pure Jump Markov Processes

Conference item

We study the probabilistic safety verification problem for pure jump Markov processes, a class of models that generalizes continuous-time Markov chains over continuous (uncountable) state spaces. Solutions of these processes are piecewise constant, right-continuous functions from time to states. Their jump (or reset) times are realizations of a Poisson process, characterized by a jump rate function that can be both time- and state-dependent. Upon jumping in time, the new state of the solution process is specified according to a (continuous) stochastic conditional kernel. After providing a full characterization of safety properties of these processes, we describe a formal method to abstract the process as a finite-state discrete-time Markov chain; this approach is formal in that it provides a-priori error bounds on the precision of the abstraction, based on the continuity properties of the stochastic kernel of the process and of its jump rate function. We illustrate the approach on a case study of thermostatically controlled loads.

Authors: Esmaeil Zadeh Soudjani, S; Majumdar, R; Abate, A

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Springer
• Host title: 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
• Publication date: 2016-04-09
• Event location: Eindhoven, The Netherlands
• Event start date: 2016-04-02
• DOI: 10.1007/978-3-662-49674-9_9
• ISSN: 0302-9743