| |
VOLUME 4, ISSUE 3, PAPER 12
|
Model Checking Probabilistic Timed Automata with One or Two Clocks
|
©Marcin Jurdzinski, University or Warwick
©Jeremy Sproston, Università di Torino
©Francois Laroussinie, LSV, ENS Cachan
|
Abstract
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.
|
Publication date: September 26, 2008
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-4(3:12)2008
Hit Counts: 2936 |
 Creative Commons | |
