Approximate Model Checking of Stochastic Hybrid Systems
A method for approximate model checking of stochastic hybrid systems with provable approximation guarantees is proposed. We focus on the probabilistic invariance problem for discrete time stochastic hybrid systems and propose a two-step scheme. The stochastic hybrid system is first approximated by a...
| Main Authors: | , , , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
2010
|
| _version_ | 1797100365546520576 |
|---|---|
| author | Abate, A Katoen, J Lygeros, J Prandini, M |
| author_facet | Abate, A Katoen, J Lygeros, J Prandini, M |
| author_sort | Abate, A |
| collection | OXFORD |
| description | A method for approximate model checking of stochastic hybrid systems with provable approximation guarantees is proposed. We focus on the probabilistic invariance problem for discrete time stochastic hybrid systems and propose a two-step scheme. The stochastic hybrid system is first approximated by a finite state Markov chain. The approximating chain is then model checked for probabilistic invariance. Under certain regularity conditions on the transition and reset kernels governing the dynamics of the stochastic hybrid system, the invariance probability computed using the approximating Markov chain is shown to converge 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. The performance of the two-step approximate model checking procedure is assessed on a case study of a multi-room heating system. © 2010 EUCA. |
| first_indexed | 2024-03-07T05:36:25Z |
| format | Journal article |
| id | oxford-uuid:e40beeb4-d752-4c05-beea-63c812b4fe01 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T05:36:25Z |
| publishDate | 2010 |
| record_format | dspace |
| spelling | oxford-uuid:e40beeb4-d752-4c05-beea-63c812b4fe012022-03-27T10:13:42ZApproximate Model Checking of Stochastic Hybrid SystemsJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:e40beeb4-d752-4c05-beea-63c812b4fe01EnglishSymplectic Elements at Oxford2010Abate, AKatoen, JLygeros, JPrandini, MA method for approximate model checking of stochastic hybrid systems with provable approximation guarantees is proposed. We focus on the probabilistic invariance problem for discrete time stochastic hybrid systems and propose a two-step scheme. The stochastic hybrid system is first approximated by a finite state Markov chain. The approximating chain is then model checked for probabilistic invariance. Under certain regularity conditions on the transition and reset kernels governing the dynamics of the stochastic hybrid system, the invariance probability computed using the approximating Markov chain is shown to converge 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. The performance of the two-step approximate model checking procedure is assessed on a case study of a multi-room heating system. © 2010 EUCA. |
| spellingShingle | Abate, A Katoen, J Lygeros, J Prandini, M Approximate Model Checking of Stochastic Hybrid Systems |
| title | Approximate Model Checking of Stochastic Hybrid Systems |
| title_full | Approximate Model Checking of Stochastic Hybrid Systems |
| title_fullStr | Approximate Model Checking of Stochastic Hybrid Systems |
| title_full_unstemmed | Approximate Model Checking of Stochastic Hybrid Systems |
| title_short | Approximate Model Checking of Stochastic Hybrid Systems |
| title_sort | approximate model checking of stochastic hybrid systems |
| work_keys_str_mv | AT abatea approximatemodelcheckingofstochastichybridsystems AT katoenj approximatemodelcheckingofstochastichybridsystems AT lygerosj approximatemodelcheckingofstochastichybridsystems AT prandinim approximatemodelcheckingofstochastichybridsystems |