Model Checking Probabilistic Timed Automata with One or Two Clocks

Marcin Jurdzinski, Francois Laroussinie, Jeremy Sproston

Probabilistic timed automata are an extension of timed automata with discrete probability distributions. We consider model-checking algorithms for the subclasses of probabilistic t…