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

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

    Research output: Book/ReportReportProfessional

    20 Citations (Scopus)
    23 Downloads (Pure)

    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 languageUndefined
    Place of PublicationEnschede
    PublisherCentrum voor Telematica en Informatie Technologie
    Number of pages29
    Publication statusPublished - 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/ReportReportProfessional

    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).