Research output per year
Research output per year
Abstract
This paper presents an algorithm for cost-bounded probabilistic reachability in timed automata extended with prices (on edges and locations) and discrete probabilistic branching. The algorithm determines whether the probability to reach a (set of) goal location(s) within a given price bound (and time bound) can exceed a threshold p in [0,1]. We prove that the algorithm is partially correct and show an example for which termination cannot be guaranteed.
| Original language | English |
|---|---|
| Place of Publication | Enschede |
| Publisher | Centre for Telematics and Information Technology (CTIT) |
| Number of pages | 29 |
| Publication status | Published - Jun 2006 |
Publication series
| Name | CTIT Technical Report Series |
|---|---|
| Publisher | Centre for Telematics and Information Technology, University of Twente |
| No. | 06-26 |
| ISSN (Print) | 1381-3625 |
Fingerprint
Dive into the research topics of 'Probably on time and within budget: on reachability in priced probabilistic timed automata'. Together they form a unique fingerprint.Research output
- 24 Citations
- 1 Conference contribution
-
Probably on time and within budget: On reachability in priced probabilistic timed automata
Berendsen, J., Jansen, D. N. & Katoen, J.-P., Sept 2006, Third International Conference on the Quantitative Evaluation of Systems - (QEST 2006). Los Alamitos, CA: IEEE, p. 311-322 12 p.Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review