Weak bisimulation for probabilistic timed automata and applications to security
Ruggero Lanotte, A. Maggiolo‐Schettini, Angelo Troina · 2003
We are interested in describing timed systems that exhibit probabilistic behaviors. To this purpose, we define a model of probabilistic timed automata and give a concept of weak bisimulation together with an algorithm to decide it. We use this model for describing and analyzing a probabilistic non-repudiation protocol in a timed setting.