Skip to content Skip to navigation
University of Warwick
  • Study
  • |
  • Research
  • |
  • Business
  • |
  • Alumni
  • |
  • News
  • |
  • About

University of Warwick
Publications service & WRAP

Highlight your research

  • WRAP
    • Home
    • Search WRAP
    • Browse by Warwick Author
    • Browse WRAP by Year
    • Browse WRAP by Subject
    • Browse WRAP by Department
    • Browse WRAP by Funder
    • Browse Theses by Department
  • Publications Service
    • Home
    • Search Publications Service
    • Browse by Warwick Author
    • Browse Publications service by Year
    • Browse Publications service by Subject
    • Browse Publications service by Department
    • Browse Publications service by Funder
  • Statistics
  • Help & Advice
University of Warwick

The Library

  • Login

Modd checking probabilistic timed automata with one or two clocks

Tools
- Tools
+ Tools

Jurdzinski, Marcin, Laroussinie, Francois and Sproston, Jeremy (2007) Modd checking probabilistic timed automata with one or two clocks. In: 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Braga, PORTUGAL, MAR 24-APR 01, 2007. Published in: Tools and Algorithms for the Construction and Analysis of Systems, Proceedings, 4424 pp. 170-184.

Full text not available from this repository.

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 it 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 the model-checking problem for the probabilistic timed temporal logic PTCTL is EXPTIME-complete for one clock probabilistic timed automata. However, the corresponding model-checking problem for the subclass of PTCTL which does not permit both (1) punctual timing bounds, which require the occurrence of an event at an exact time point, and (2) comparisons with probability bounds other than 0 or 1, is PTIME-complete.

Item Type: Conference Item (UNSPECIFIED)
Subjects: Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software
Series Name: LECTURE NOTES IN COMPUTER SCIENCE
Journal or Publication Title: Tools and Algorithms for the Construction and Analysis of Systems, Proceedings
Publisher: SPRINGER-VERLAG BERLIN
ISBN: 978-3-540-71208-4
ISSN: 0302-9743
Editor: Grumberg, O and Huth, M
Date: 2007
Volume: 4424
Number of Pages: 15
Page Range: pp. 170-184
Publication Status: Published
Title of Event: 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
Location of Event: Braga, PORTUGAL
Date(s) of Event: MAR 24-APR 01, 2007
URI: http://wrap.warwick.ac.uk/id/eprint/31007

Data sourced from Thomson Reuters' Web of Knowledge

Request changes to a record

Actions (login required)

View Item View Item
twitter

Email us: publications@warwick.ac.uk
Contact Details
About Us