Probabilistic Timed Automata with Clock-Dependent Probabilities

Issue title: Special Issue on the 11th International Workshop on Reachability Problems (RP 2017)

Guest editors: Matthew Hague and Igor Potapov

Article type: Research Article

Authors: Sproston, Jeremy^{; *}

Affiliations: Dipartimento di Informatica, University of Turin, Italy. [email protected]

Correspondence: [*] Address for correspondence: Dipartimento di Informatica, Università degli Studi di Torino, Corso Svizzera 185, 10149 Torino, Italy

Abstract: Probabilistic timed automata are classical timed automata extended with discrete probability distributions over edges. We introduce clock-dependent probabilistic timed automata, a variant of probabilistic timed automata in which transition probabilities can depend linearly on clock values. Clock-dependent probabilistic timed automata allow the modelling of a continuous relationship between time passage and the likelihood of system events. We show that the problem of deciding whether the maximum probability of reaching a certain location is above a threshold is undecidable for clock-dependent probabilistic timed automata. On the positive side, we show that the maximum and minimum probability of reaching a certain location in clock-dependent probabilistic timed automata can be approximated using a region-graph-based approach.

Keywords: Probabilistic model checking, timed automata

DOI: 10.3233/FI-2021-2000

Journal: Fundamenta Informaticae, vol. 178, no. 1-2, pp. 101-138, 2021