Timed Automaton to Probabilistic Timed Automaton

[Anitha Murugesan]

Hi, 

  Is there a standard translation from a Timed Automaton (created using tools like UPPAAL) to Probabilistic Timed Automaton to quantitatively reason about a system properties in PRISM? 

Thanks

Anitha.

[Dave Parker]

Hi Anitha,

PRISM does not currently read UPPAAL models I'm afraid. You might be
able to build something with these tools/libraries:

http://opaal-modelchecker.com/
https://launchpad.net/pyuppaal

which are open source and read from UPPAAL models.

You could also look at:

http://www.modestchecker.net/Default.aspx

which has connections to both UPPAAL and PRISM, but I don't know if it
does quite what you want.

Best wishes,

Dave.

> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to prismmodelchec...@googlegroups.com
> <mailto:prismmodelchec...@googlegroups.com>.
> To post to this group, send email to prismmod...@googlegroups.com
> <mailto:prismmod...@googlegroups.com>.
> Visit this group at http://groups.google.com/group/prismmodelchecker.
> For more options, visit https://groups.google.com/d/optout.