  The paper addresses the problem of computing maximal expected time to
termination of probabilistic timed automata (PTA) models, under the condition
that the system will, eventually, terminate. This problem can exhibit high
computational complexity, in particular when the automaton under analysis
contains cycles that may be repeated very often (due to very high
probabilities, e.g. p =0.999). Such cycles can degrade the performance of
typical model checking algorithms, as the likelihood of repeating the cycle
converges to zero arbitrarily slowly. We introduce an acceleration technique
that can be applied to improve the execution of such cycles by collapsing their
iterations. The acceleration process of a cyclic PTA consists of several formal
steps necessary to handle the cumulative timing and probability information
that result from successive executions of a cycle. The advantages of
acceleration are twofold. First, it helps to reduce the computational
complexity of the problem without adversely affecting the outcome of the
analysis. Second, it can bring the "worst case execution time" problem of PTAs
within the bounds of feasibility for model checking techniques. To our
knowledge, this is the first work that addresses the problem of accelerating
execution of cycles that exhibit both timing and probabilistic behavior.

Formal Languages and Automata Theory