Qualitative and quantitative model checking of distributed probabilistic timed actors