Local abstraction refinement for probabilistic timed programs

Klaus Dräger, Marta Kwiatkowska, David Parker, Hongyang Qu

Research output: Contribution to journalArticlepeer-review

5 Citations (Scopus)
152 Downloads (Pure)


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.
Original languageEnglish
Pages (from-to)37-53
JournalTheoretical Computer Science
Early online date1 Aug 2013
Publication statusPublished - 12 Jun 2014


  • Probabilistic verification
  • Abstraction refinement


Dive into the research topics of 'Local abstraction refinement for probabilistic timed programs'. Together they form a unique fingerprint.

Cite this