Probably on time and within budget: On reachability in priced probabilistic timed automata

Jasper Berendsen; David N. Jansen; Joost-Pieter Katoen

doi:10.1109/QEST.2006.43

Probably on time and within budget: On reachability in priced probabilistic timed automata

Jasper Berendsen, David N. Jansen, Joost-Pieter Katoen

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

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 e¸ [0, 1]. We prove that the algorithm is partially correct and show an example for which termination cannot be guaranteed.

Original language	English
Title of host publication	Third International Conference on the Quantitative Evaluation of Systems - (QEST 2006)
Place of Publication	Los Alamitos, CA
Publisher	IEEE
Pages	311-322
Number of pages	12
ISBN (Print)	0-7695-2665-9
DOIs	https://doi.org/10.1109/QEST.2006.43
Publication status	Published - Sept 2006
Event	3rd International Conference on Quantitative Evaluation of SysTems, QEST 2006 - University of California, Riverside, United States Duration: 11 Sept 2006 → 14 Sept 2006 Conference number: 3 http://www.qest.org/qest2006/

Conference

Conference	3rd International Conference on Quantitative Evaluation of SysTems, QEST 2006
Abbreviated title	QEST
Country/Territory	United States
City	Riverside
Period	11/09/06 → 14/09/06
Internet address	http://www.qest.org/qest2006/

Access to Document

10.1109/QEST.2006.43

1 Report

Probably on time and within budget: on reachability in priced probabilistic timed automata
Berendsen, J., Jansen, D. N. & Katoen, J.-P., Jun 2006, Enschede: Centre for Telematics and Information Technology (CTIT). 29 p. (CTIT Technical Report Series; no. 06-26)
Research output: Book/Report › Report › Professional

Open Access
File

Cite this

@inproceedings{e8c542f087ef4d55af21721685955a89,

title = "Probably on time and within budget: On reachability in priced probabilistic timed automata",

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 e¸ [0, 1]. We prove that the algorithm is partially correct and show an example for which termination cannot be guaranteed.",

author = "Jasper Berendsen and Jansen, {David N.} and Joost-Pieter Katoen",

year = "2006",

month = sep,

doi = "10.1109/QEST.2006.43",

language = "English",

isbn = "0-7695-2665-9",

pages = "311--322",

booktitle = "Third International Conference on the Quantitative Evaluation of Systems - (QEST 2006)",

publisher = "IEEE",

address = "United States",

note = "3rd International Conference on Quantitative Evaluation of SysTems, QEST 2006, QEST ; Conference date: 11-09-2006 Through 14-09-2006",

url = "http://www.qest.org/qest2006/",

}

Berendsen, J, Jansen, DN & Katoen, J-P 2006, Probably on time and within budget: On reachability in priced probabilistic timed automata. in Third International Conference on the Quantitative Evaluation of Systems - (QEST 2006). IEEE, Los Alamitos, CA, pp. 311-322, 3rd International Conference on Quantitative Evaluation of SysTems, QEST 2006, Riverside, California, United States, 11/09/06. https://doi.org/10.1109/QEST.2006.43

Probably on time and within budget: On reachability in priced probabilistic timed automata. / Berendsen, Jasper; Jansen, David N.; Katoen, Joost-Pieter.
Third International Conference on the Quantitative Evaluation of Systems - (QEST 2006). Los Alamitos, CA: IEEE, 2006. p. 311-322.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Probably on time and within budget

T2 - 3rd International Conference on Quantitative Evaluation of SysTems, QEST 2006

AU - Berendsen, Jasper

AU - Jansen, David N.

AU - Katoen, Joost-Pieter

N1 - Conference code: 3

PY - 2006/9

Y1 - 2006/9

N2 - 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 e¸ [0, 1]. We prove that the algorithm is partially correct and show an example for which termination cannot be guaranteed.

AB - 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 e¸ [0, 1]. We prove that the algorithm is partially correct and show an example for which termination cannot be guaranteed.

U2 - 10.1109/QEST.2006.43

DO - 10.1109/QEST.2006.43

M3 - Conference contribution

SN - 0-7695-2665-9

SP - 311

EP - 322

BT - Third International Conference on the Quantitative Evaluation of Systems - (QEST 2006)

PB - IEEE

CY - Los Alamitos, CA

Y2 - 11 September 2006 through 14 September 2006

ER -

Probably on time and within budget: On reachability in priced probabilistic timed automata

Abstract

Conference

Access to Document

Fingerprint

Research output

Probably on time and within budget: on reachability in priced probabilistic timed automata

Cite this