Probably on Time and within BudgetOn Reachability in Priced Probabilistic Timed Automata

	This Article
	Subscribers, please Login Purchase article: $19 PDF RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Jasper Berendsen Articles by David N. Jansen Articles by Joost-Pieter Katoen

Third International Conference on the Quantitative Evaluation of Systems - (QEST'06)

Riverside, California

September 11-September 14

ISBN: 0-7695-2665-9

	ASCII Text	x
	Jasper Berendsen, David N. Jansen, Joost-Pieter Katoen, "Probably on Time and within BudgetOn Reachability in Priced Probabilistic Timed Automata," Quantitative Evaluation of Systems, International Conference on, pp. 311-322, Third International Conference on the Quantitative Evaluation of Systems - (QEST'06), 2006.

	BibTex	x
	@article{ 10.1109/QEST.2006.43, author = {Jasper Berendsen and David N. Jansen and Joost-Pieter Katoen}, title = {Probably on Time and within BudgetOn Reachability in Priced Probabilistic Timed Automata}, journal ={Quantitative Evaluation of Systems, International Conference on}, volume = {0}, year = {2006}, isbn = {0-7695-2665-9}, pages = {311-322}, doi = {http://doi.ieeecomputersociety.org/10.1109/QEST.2006.43}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Quantitative Evaluation of Systems, International Conference on TI - Probably on Time and within BudgetOn Reachability in Priced Probabilistic Timed Automata SN - 0-7695-2665-9 SP311 EP322 A1 - Jasper Berendsen, A1 - David N. Jansen, A1 - Joost-Pieter Katoen, PY - 2006 KW - null VL - 0 JA - Quantitative Evaluation of Systems, International Conference on ER -

Jasper Berendsen, University of Twente, Netherlands

David N. Jansen, University of Twente, Netherlands

Joost-Pieter Katoen, RWTH Aachen Software Modeling and Verification Group Aachen, Germany

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/QEST.2006.43

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.

Citation:

Jasper Berendsen, David N. Jansen, Joost-Pieter Katoen, "Probably on Time and within BudgetOn Reachability in Priced Probabilistic Timed Automata," qest, pp.311-322, Third International Conference on the Quantitative Evaluation of Systems - (QEST'06), 2006

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.