[DKPQ14] Klaus Draeger, Marta Kwiatkowska, David Parker and Hongyang Qu. Local Abstraction Refinement for Probabilistic Timed Programs. Theoretical Computer Science, 538, pages 37-53, Elsevier. June 2014. [pdf] [bib] [Presents new techniques for abstraction refinement on probabilistic timed programs (probabilistic timed automata with data variables), implemented in an extension of PRISM.]
Downloads:  pdf pdf (504 KB)  bib bib
Abstract. 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.