Model Checking Probabilistic Timed Automata with One or Two Clocks

Details Model Checking Probabilistic Timed Automata with One or Two Clocks Model Checking Probabilistic Timed Automata with One or Two Clocks

2008-08-30

arxiv.org/abs/0809.0060v3

LMCS 4 (3:11) 2008

Computer Science

Logic in Computer Science

Scientific paper

10.2168/LMCS-4(3:11)2008

Probabilistic timed automata are an extension of timed automata with discrete probability distributions. We consider model-checking algorithms for the subclasses of probabilistic timed automata which have one or two clocks. Firstly, we show that PCTL probabilistic model-checking problems (such as determining whether a set of target states can be reached with probability at least 0.99 regardless of how nondeterminism is resolved) are PTIME-complete for one-clock probabilistic timed automata, and are EXPTIME-complete for probabilistic timed automata with two clocks. Secondly, we show that, for one-clock probabilistic timed automata, the model-checking problem for the probabilistic timed temporal logic PCTL is EXPTIME-complete. However, the model-checking problem for the subclass of PCTL which does not permit both punctual timing bounds, which require the occurrence of an event at an exact time point, and comparisons with probability bounds other than 0 or 1, is PTIME-complete for one-clock probabilistic timed automata.

Affiliated with

Also associated with

No associations

Rating

Model Checking Probabilistic Timed Automata with One or Two Clocks does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Model Checking Probabilistic Timed Automata with One or Two Clocks, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Model Checking Probabilistic Timed Automata with One or Two Clocks will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-613690