On probabilistic timed automata

We propose a model of probabilistic timed automaton which substitutes for the non-determinism of an ordinary timed automaton, a new one (directly drawn from Markov decision processes) by means of actions which provide a probabilistic distribution over transitions. Using Buchi acceptance conditions, timed automata can refer timing properties as "during every open time interval of length I at least one message is delivered". A policy is a mechanism which solves the non-determinism by choosing for each finite run an action and the time moment of the next transition step implied by this action. We prove that, given a probabilistic timed automaton A, there exists a Markov (memoryless) policy which maximizes the probability p of the set of accepting runs realized by this policy. This policy as well as the maximal value of p are computable in polytime in the size of the region automaton of W. This result provides an algorithm of model-checking for properties like "there is a policy which realizes a correct behavior of the system with probability at least p". (C) 2002 Elsevier Science B.V. All rights reserved.