Computing Maximal Expected Termination Time of Probabilistic Timed Automata

TL;DR

This paper presents a novel acceleration technique for probabilistic timed automata that improves the efficiency of computing maximal expected termination times, especially in systems with high-probability cycles, making analysis more feasible.

Contribution

It introduces the first formal acceleration method for cycles with both timing and probabilistic behaviors in PTAs, reducing complexity and enabling practical model checking.

Findings

Acceleration reduces computational complexity.

Method handles cycles with high probability and timing.

Enables feasible analysis of complex PTAs.

Abstract

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.