The Library
Model checking probabilistic timed automata with one or two clocks
Tools
Jurdzinski, Marcin, Laroussinie, Francois and Sproston, Jeremy (2008) Model checking probabilistic timed automata with one or two clocks. Logical Methods in Computer Science, Vol.4 (No.3). Article no.12 . doi:10.2168/LMCS-4(3:12)2008 ISSN 1860-5974.
Research output not available from this repository.
Request-a-Copy directly from author or use local Library Get it For Me service.
Official URL: http://dx.doi.org/10.2168/LMCS-4(3:12)2008
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 PTCTL is EXPTIME-complete. However, the model-checking problem for the subclass of PTCTL 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.
Item Type: | Journal Article | ||||
---|---|---|---|---|---|
Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software | ||||
Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | ||||
Journal or Publication Title: | Logical Methods in Computer Science | ||||
Publisher: | International Federation for Computational Logic | ||||
ISSN: | 1860-5974 | ||||
Official Date: | 2008 | ||||
Dates: |
|
||||
Volume: | Vol.4 | ||||
Number: | No.3 | ||||
Number of Pages: | 28 | ||||
Page Range: | Article no.12 | ||||
DOI: | 10.2168/LMCS-4(3:12)2008 | ||||
Status: | Peer Reviewed | ||||
Publication Status: | Published | ||||
Access rights to Published version: | Restricted or Subscription Access | ||||
Funder: | Engineering and Physical Sciences Research Council (EPSRC), QUASIMODO, Seventh Framework Programme (European Commission) (FP7) | ||||
Grant number: | EP/E022030/1 (EPSRC), FP7-ICT, 027513 |
Data sourced from Thomson Reuters' Web of Knowledge
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |