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 is 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.

R. Lanotte, A. Maggiolo-Schettini, A. Troina (2010). Weak Bisimulation for Probabilistic Timed Automata. THEORETICAL COMPUTER SCIENCE, 411(50), 4291-4322 [10.1016/j.tcs.2010.09.003].

Weak Bisimulation for Probabilistic Timed Automata

TROINA, ANGELO
2010

Abstract

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 is 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.
2010
R. Lanotte, A. Maggiolo-Schettini, A. Troina (2010). Weak Bisimulation for Probabilistic Timed Automata. THEORETICAL COMPUTER SCIENCE, 411(50), 4291-4322 [10.1016/j.tcs.2010.09.003].
R. Lanotte; A. Maggiolo-Schettini; A. Troina
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/581027
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 7
  • ???jsp.display-item.citation.isi??? 5
social impact