Search

• < Previous
• 1
• Next >

---

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 timed automata which have one or two clocks. Firstly, we show that PCTL probabilistic model-checking problems (such as&nbsp;[&hellip;]

---

Probabilistic Timed Automata with One Clock and Initialised Clock-Dependent Probabilities

Jeremy Sproston.

Clock-dependent probabilistic timed automata extend classical timed automata with discrete probabilistic choice, where the probabilities are allowed to depend on the exact values of the clocks. Previous work has shown that the quantitative reachability problem for clock-dependent probabilistic timed&nbsp;[&hellip;]

---