We provide a unifying view of timed models such as timed automata, probabilistic timed automata, and Markov automata. The timed models and their bisimulation semantics are encoded in the framework of uniform labeled transition systems. In this unifying framework, we show that the timed bisimilarities present in the literature can be re-obtained and that a new bisimilarity, of which we exhibit the modal logic characterization, can be introduced for timed models including probabilities. We finally highlight similarities and differences among the models.

Encoding Timed Models as Uniform Labeled Transition Systems

TESEI, Luca
2013-01-01

Abstract

We provide a unifying view of timed models such as timed automata, probabilistic timed automata, and Markov automata. The timed models and their bisimulation semantics are encoded in the framework of uniform labeled transition systems. In this unifying framework, we show that the timed bisimilarities present in the literature can be re-obtained and that a new bisimilarity, of which we exhibit the modal logic characterization, can be introduced for timed models including probabilities. We finally highlight similarities and differences among the models.
2013
9783642407246
9783642407253
273
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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/11581/337189
 Attenzione

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

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