Local abstraction refinement for probabilistic timed programs
We consider models of programs that incorporate probability, dense real-time and data. We present a new abstraction refinement method for computing minimum and maximum reachability probabilities for such models. Our approach uses strictly local refinement steps to reduce both the size of abstraction...
| Main Authors: | , , , |
|---|---|
| Format: | Journal article |
| Published: |
Elsevier
2013
|
| _version_ | 1826302520876597248 |
|---|---|
| author | Dräger, K Kwiatkowska, M Parker, D Qu, H |
| author_facet | Dräger, K Kwiatkowska, M Parker, D Qu, H |
| author_sort | Dräger, K |
| collection | OXFORD |
| description | We consider models of programs that incorporate probability, dense real-time and data. We present a new abstraction refinement method for computing minimum and maximum reachability probabilities for such models. Our approach uses strictly local refinement steps to reduce both the size of abstractions generated and the complexity of operations needed, in comparison to previous approaches of this kind. We implement the techniques and evaluate them on a selection of large case studies, including some infinite-state probabilistic real-time models, demonstrating improvements over existing tools in several cases. |
| first_indexed | 2024-03-07T05:48:49Z |
| format | Journal article |
| id | oxford-uuid:e821293c-2794-4fb9-9dbd-448ddcadd558 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T05:48:49Z |
| publishDate | 2013 |
| publisher | Elsevier |
| record_format | dspace |
| spelling | oxford-uuid:e821293c-2794-4fb9-9dbd-448ddcadd5582022-03-27T10:44:28ZLocal abstraction refinement for probabilistic timed programsJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:e821293c-2794-4fb9-9dbd-448ddcadd558Symplectic Elements at OxfordElsevier2013Dräger, KKwiatkowska, MParker, DQu, HWe consider models of programs that incorporate probability, dense real-time and data. We present a new abstraction refinement method for computing minimum and maximum reachability probabilities for such models. Our approach uses strictly local refinement steps to reduce both the size of abstractions generated and the complexity of operations needed, in comparison to previous approaches of this kind. We implement the techniques and evaluate them on a selection of large case studies, including some infinite-state probabilistic real-time models, demonstrating improvements over existing tools in several cases. |
| spellingShingle | Dräger, K Kwiatkowska, M Parker, D Qu, H Local abstraction refinement for probabilistic timed programs |
| title | Local abstraction refinement for probabilistic timed programs |
| title_full | Local abstraction refinement for probabilistic timed programs |
| title_fullStr | Local abstraction refinement for probabilistic timed programs |
| title_full_unstemmed | Local abstraction refinement for probabilistic timed programs |
| title_short | Local abstraction refinement for probabilistic timed programs |
| title_sort | local abstraction refinement for probabilistic timed programs |
| work_keys_str_mv | AT dragerk localabstractionrefinementforprobabilistictimedprograms AT kwiatkowskam localabstractionrefinementforprobabilistictimedprograms AT parkerd localabstractionrefinementforprobabilistictimedprograms AT quh localabstractionrefinementforprobabilistictimedprograms |