IPTA edition of PRISM

Interval Probabilistic Timed Automata (IPTA) are a recently introduced model for probabilistic real-time behavior with uncertainties. The current development version of the PRISM model checker already supports Probabilistic Timed Automata (PTA). To support also the probability intervals used in IPTA, we extended the syntax of the PRISM specification language and adapted its probabilistic reachability checker. Our IPTA edition of PRISM is available for download here:  prism-ipta.tar_.gz (88 downloads) . For an IPTA example, check out the ipta directory in the examples. If you have any questions or suggestions don't hesitate to contact me.

This entry was posted in Verification Tools. Bookmark the permalink.

Comments are closed.