In this paper we describe a two-step scheme for approximate model checking of discrete time stochastic hybrid systems. In the first step, the stochastic hybrid system is approximated by a finite state Markov chain. In the second step, the Markov chain is model checked for the desired property. In particular, we consider the probabilistic invariance property and show that, under certain regularity conditions, the invariance probability computed using the approximatingMarkov chain converges to the invariance probability of the original stochastic hybrid system, as the grid used in the approximation gets finer. A bound on the convergence rate is also provided.

A two-step scheme for approximate model checking of stochastic hybrid systems

PRANDINI, MARIA
2011-01-01

Abstract

In this paper we describe a two-step scheme for approximate model checking of discrete time stochastic hybrid systems. In the first step, the stochastic hybrid system is approximated by a finite state Markov chain. In the second step, the Markov chain is model checked for the desired property. In particular, we consider the probabilistic invariance property and show that, under certain regularity conditions, the invariance probability computed using the approximatingMarkov chain converges to the invariance probability of the original stochastic hybrid system, as the grid used in the approximation gets finer. A bound on the convergence rate is also provided.
2011
Proceedings of the 18th IFAC World Congress
978-3-902661-93-7
AUT
File in questo prodotto:
File Dimensione Formato  
printed version.pdf

Accesso riservato

: Post-Print (DRAFT o Author’s Accepted Manuscript-AAM)
Dimensione 160.38 kB
Formato Adobe PDF
160.38 kB Adobe PDF   Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11311/608434
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? ND
social impact