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

J. Berendsen, D.N. Jansen, Joost P. Katoen

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-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 languageUndefined
Title of host publicationQuantitative Evaluation of Systems (QEST)
Place of PublicationLos Alamitos
PublisherIEEE Computer Society
Pages311-322
Number of pages12
ISBN (Print)0-7695-2665-9
DOIs
Publication statusPublished - Sep 2006
Event3rd International Conference on Quantitative Evaluation of SysTems, QEST 2006 - University of California, Riverside, United States
Duration: 11 Sep 200614 Sep 2006
Conference number: 3
http://www.qest.org/qest2006/

Publication series

Name
PublisherIEEE Computer Society Press
Number10

Conference

Conference3rd International Conference on Quantitative Evaluation of SysTems, QEST 2006
Abbreviated titleQEST
CountryUnited States
CityRiverside
Period11/09/0614/09/06
Internet address

Keywords

  • IR-63704
  • METIS-237637
  • EWI-8232

Cite this

Berendsen, J., Jansen, D. N., & Katoen, J. P. (2006). Probably on time and within budget - On reachability in priced probabilistic timed automata. In Quantitative Evaluation of Systems (QEST) (pp. 311-322). [10.1109/QEST.2006.43] Los Alamitos: IEEE Computer Society. https://doi.org/10.1109/QEST.2006.43
Berendsen, J. ; Jansen, D.N. ; Katoen, Joost P. / Probably on time and within budget - On reachability in priced probabilistic timed automata. Quantitative Evaluation of Systems (QEST). Los Alamitos : IEEE Computer Society, 2006. pp. 311-322
@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.",
keywords = "IR-63704, METIS-237637, EWI-8232",
author = "J. Berendsen and D.N. Jansen and Katoen, {Joost P.}",
note = "10.1109/QEST.2006.43",
year = "2006",
month = "9",
doi = "10.1109/QEST.2006.43",
language = "Undefined",
isbn = "0-7695-2665-9",
publisher = "IEEE Computer Society",
number = "10",
pages = "311--322",
booktitle = "Quantitative Evaluation of Systems (QEST)",
address = "United States",

}

Berendsen, J, Jansen, DN & Katoen, JP 2006, Probably on time and within budget - On reachability in priced probabilistic timed automata. in Quantitative Evaluation of Systems (QEST)., 10.1109/QEST.2006.43, IEEE Computer Society, Los Alamitos, pp. 311-322, 3rd International Conference on Quantitative Evaluation of SysTems, QEST 2006, Riverside, 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, J.; Jansen, D.N.; Katoen, Joost P.

Quantitative Evaluation of Systems (QEST). Los Alamitos : IEEE Computer Society, 2006. p. 311-322 10.1109/QEST.2006.43.

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

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

AU - Berendsen, J.

AU - Jansen, D.N.

AU - Katoen, Joost P.

N1 - 10.1109/QEST.2006.43

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.

KW - IR-63704

KW - METIS-237637

KW - EWI-8232

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 - Quantitative Evaluation of Systems (QEST)

PB - IEEE Computer Society

CY - Los Alamitos

ER -

Berendsen J, Jansen DN, Katoen JP. Probably on time and within budget - On reachability in priced probabilistic timed automata. In Quantitative Evaluation of Systems (QEST). Los Alamitos: IEEE Computer Society. 2006. p. 311-322. 10.1109/QEST.2006.43 https://doi.org/10.1109/QEST.2006.43