Skip to Main Content (Press Enter)

Logo UNITO
  • ×
  • Home
  • Pubblicazioni
  • Progetti
  • Persone
  • Competenze
  • Settori
  • Strutture
  • Terza Missione

UNI-FIND
Logo UNITO

|

UNI-FIND

unito.it
  • ×
  • Home
  • Pubblicazioni
  • Progetti
  • Persone
  • Competenze
  • Settori
  • Strutture
  • Terza Missione
  1. Pubblicazioni

Performance Analysis of Probabilistic Timed Automata using Digital Clocks

Articolo
Data di Pubblicazione:
2003
Abstract:
Probabilistic timed automata, a variant of timed automata extended with discrete probability distributions, is a specification formalism suitable for describing both nondeterministic and probabilistic aspects of real-time systems, and is amenable to model checking against probabilistic timed temporal logic properties. In the case of classical (non-probabilistic) timed automata, it has been shown that for a large class of real-time verification problems correctness can be established using an integer-time model, inducing a notion of digital clocks, as opposed to the standard dense model of time. Based on these results, we address the question of under what conditions digital clocks are sufficient for the performance analysis of probabilistic timed automata. We extend previous results concerning the integer-time semantics of an important subclass of probabilistic timed automata to consider the computation of expected costs or rewards. We illustrate this approach through the analysis of the dynamic configuration protocol for IPv4 link-local addresses.
Tipologia CRIS:
03A-Articolo su Rivista
Elenco autori:
M. KWIATKOWSKA; G. NORMAN G; P. PARKER; J. SPROSTON
Autori di Ateneo:
SPROSTON Jeremy James
Link alla scheda completa:
https://iris.unito.it/handle/2318/115845
Pubblicato in:
LECTURE NOTES IN COMPUTER SCIENCE
Journal
LECTURE NOTES IN COMPUTER SCIENCE
Series
  • Utilizzo dei cookie

Realizzato con VIVO | Designed by Cineca | 25.6.1.0