www.prismmodelchecker.org
[WK05] F. Wang and M. Kwiatkowska. An MTBDD-based implementation of forward reachability for probabilistic timed automata. In Proc. 3rd International Symposium on Automated Technology for Verification and Analysis (ATVA'05), volume 3707 of Lecture Notes in Computer Science, pages 385-399, Springer. October 2005. [ps.gz] [pdf] [bib]
Downloads:  ps.gz ps.gz (994 KB)  pdf pdf (238 KB)  bib bib
Notes: The original publication is available at www.springerlink.com.
Abstract. Multi-Terminal Binary Decision Diagrams (MTBDDs) have been successfully applied in symbolic model checking of probabilistic systems. In this paper we propose an encoding method for Probabilistic Timed Automata (PTA) based on MTBDDs. The timing information is encoded via placeholders stored in the MTBDDs that are independent of how the timing information is represented. Using the Colorado University Decision Diagrams (CUDD) package, an experimental model checker is implemented, which supports probabilistic reachability model checking via the forward algorithm. We use Difference Bound Matrices (DBMs) and Difference Decision Diagrams (DDDs) for representing timing infor- mation and present experimental results on three case studies. Our key contribution is a general placeholder encoding method for Probabilis- tic Timed Automata and an experimental MTBDD-based model checker which has been partly integrated with PRISM. This is the first symbolic implementation of the forward probabilistic reachability algorithm.

Publications