1: \begin{abstract}

2: We propose an extension of the zone-based algorithmics for analyzing timed automata to handle systems where timing uncertainty is considered as \emph{probabilistic} rather than \emph{set-theoretic}. We study \emph{duration probabilistic automata} (DPA), expressing \emph{multiple} parallel processes admitting \emph{memoryfull} continuously-distributed  durations. For this model we develop an extension of the zone-based forward reachability algorithm whose successor operator is a \emph{density transformer}, thus providing a solution to verification and performance evaluation problems concerning acyclic DPA (or the bounded-horizon behavior of cyclic DPA). \comment{We also speculate about the convergence of this computation for unbounded horizon.}

3: \comment{From the point of view of stochastic processes, we propose a new computational technique for class of generalized semi-Markov processes.}

4: \end{abstract}