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 Büchi acceptance conditions,...

Full description

Saved in:
Bibliographic Details
Published in:Theoretical computer science 2003-01, Vol.292 (1), p.65-84
Main Author: Beauquier, Danièle
Format: Article
Language:English
Subjects:
Applied sciences
Automata. Abstract machines. Turing machines
Computer science
control theory
systems
Exact sciences and technology
Markov decision process
Model-checking
Probabilistic timed automata
Theoretical computing
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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 Büchi acceptance conditions, timed automata can refer timing properties as “during every open time interval of length 1 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 A . 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”.
ISSN:0304-3975
1879-2294
DOI:10.1016/S0304-3975(01)00215-8