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

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

Research output: Book/ReportReport

  • 20 Citations

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.
LanguageUndefined
Place of PublicationEnschede
PublisherCentrum voor Telematica en Informatie Technologie
Number of pages29
StatePublished - Jun 2006

Publication series

NameCTIT Technical Report Series
PublisherCentre for Telematics and Information Technology, University of Twente
No.06-26
ISSN (Print)1381-3625

Keywords

  • EWI-2874
  • METIS-238644
  • IR-65646

Cite this

Berendsen, J., Jansen, D. N., & Katoen, J. P. (2006). Probably on time and within budget: on reachability in priced probabilistic timed automata. (CTIT Technical Report Series; No. 06-26). Enschede: Centrum voor Telematica en Informatie Technologie.
Berendsen, J. ; Jansen, D.N. ; Katoen, Joost P./ Probably on time and within budget: on reachability in priced probabilistic timed automata. Enschede : Centrum voor Telematica en Informatie Technologie, 2006. 29 p. (CTIT Technical Report Series; 06-26).
@book{2a87847f424d4e6fa6d6388ceead9738,
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 in [0,1]. We prove that the algorithm is partially correct and show an example for which termination cannot be guaranteed.",
keywords = "EWI-2874, METIS-238644, IR-65646",
author = "J. Berendsen and D.N. Jansen and Katoen, {Joost P.}",
year = "2006",
month = "6",
language = "Undefined",
series = "CTIT Technical Report Series",
publisher = "Centrum voor Telematica en Informatie Technologie",
number = "06-26",

}

Berendsen, J, Jansen, DN & Katoen, JP 2006, Probably on time and within budget: on reachability in priced probabilistic timed automata. CTIT Technical Report Series, no. 06-26, Centrum voor Telematica en Informatie Technologie, Enschede.

Probably on time and within budget: on reachability in priced probabilistic timed automata. / Berendsen, J.; Jansen, D.N.; Katoen, Joost P.

Enschede : Centrum voor Telematica en Informatie Technologie, 2006. 29 p. (CTIT Technical Report Series; No. 06-26).

Research output: Book/ReportReport

TY - BOOK

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.

PY - 2006/6

Y1 - 2006/6

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

KW - EWI-2874

KW - METIS-238644

KW - IR-65646

M3 - Report

T3 - CTIT Technical Report Series

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

PB - Centrum voor Telematica en Informatie Technologie

CY - Enschede

ER -

Berendsen J, Jansen DN, Katoen JP. Probably on time and within budget: on reachability in priced probabilistic timed automata. Enschede: Centrum voor Telematica en Informatie Technologie, 2006. 29 p. (CTIT Technical Report Series; 06-26).