We consider continuous time stochastic hybrid systems with no resets and continuous dynamics described by linear stochastic differential equations -- models also known as switching diffusions. We show that for this class of models reachability (and dually, safety) properties can be studied on an abstraction defined in terms of a discrete time and finite space Markov chain (DTMC), with provable error bounds. The technical contribution of the paper is a characterization of the uniform convergence of the time discretization of such stochastic processes with respect to safety properties. This allows us to newly provide a complete and sound numerical procedure for reachability and safety computation over switching diffusions.
Reachability Computation for Switching Diffusions: Finite Abstractions with Certifiable and Tuneable Precision
BORTOLUSSI, LUCA;
2017-01-01
Abstract
We consider continuous time stochastic hybrid systems with no resets and continuous dynamics described by linear stochastic differential equations -- models also known as switching diffusions. We show that for this class of models reachability (and dually, safety) properties can be studied on an abstraction defined in terms of a discrete time and finite space Markov chain (DTMC), with provable error bounds. The technical contribution of the paper is a characterization of the uniform convergence of the time discretization of such stochastic processes with respect to safety properties. This allows us to newly provide a complete and sound numerical procedure for reachability and safety computation over switching diffusions.File | Dimensione | Formato | |
---|---|---|---|
p55-laurenti.pdf
Accesso chiuso
Tipologia:
Documento in Versione Editoriale
Licenza:
Digital Rights Management non definito
Dimensione
1.04 MB
Formato
Adobe PDF
|
1.04 MB | Adobe PDF | Visualizza/Apri Richiedi una copia |
p55-laurenti.pdf
Open Access dal 01/05/2018
Tipologia:
Bozza finale post-referaggio (post-print)
Licenza:
Digital Rights Management non definito
Dimensione
1.04 MB
Formato
Adobe PDF
|
1.04 MB | Adobe PDF | Visualizza/Apri |
frontmatter1--compressed.pdf
Accesso chiuso
Tipologia:
Documento in Versione Editoriale
Licenza:
Digital Rights Management non definito
Dimensione
572.8 kB
Formato
Adobe PDF
|
572.8 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.