Probabilistic Timed Automata with Clock-Dependent Probabilities

TL;DR

This paper introduces clock-dependent probabilistic timed automata, a new model where transition probabilities depend linearly on clock values, and analyzes their decidability and approximation methods.

Contribution

It defines a novel class of probabilistic timed automata with clock-dependent probabilities and studies their decidability and approximation techniques.

Findings

Deciding whether the maximum reachability probability exceeds a threshold is undecidable.

Maximum and minimum reachability probabilities can be approximated using region-graph-based methods.

The model captures continuous relationships between time passage and event likelihoods.

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 other hand, 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.