Journal
THEORETICAL COMPUTER SCIENCE
Volume 292, Issue 1, Pages 65-84Publisher
ELSEVIER
DOI: 10.1016/S0304-3975(01)00215-8
Keywords
model-checking; Markov decision process; probabilistic timed automata
Categories
Ask authors/readers for more resources
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.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available