Sciweavers

FORMATS
2003
Springer

Performance Analysis of Probabilistic Timed Automata Using Digital Clocks

13 years 8 months ago
Performance Analysis of Probabilistic Timed Automata Using Digital Clocks
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...
Marta Z. Kwiatkowska, Gethin Norman, David Parker,
Added 06 Jul 2010
Updated 06 Jul 2010
Type Conference
Year 2003
Where FORMATS
Authors Marta Z. Kwiatkowska, Gethin Norman, David Parker, Jeremy Sproston
Comments (0)