Weak bisimulation for Probabilistic Timed Automata

We are interested in describing timed systems that exhibit
probabilistic behaviour. To this purpose, we consider a model of
Probabilistic Timed Automata and introduce a concept of weak
bisimulation for these automata, together with an algorithm to
decide it. The weak bisimulation relation is shown to be preserved when either time, or probability are abstracted away. As an application, we use weak bisimulation for Probabilistic Timed Automata to model and analyze a timing attack on the dining cryptographers protocol.