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 (253 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.