Computing Maximal Expected Termination Time of Probabilistic Timed Automata

The paper addresses the problem of computing maximal expected 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...More