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

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

    Research output: Book/ReportReportProfessional

    22 Citations (Scopus)
    28 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 languageEnglish
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    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

    Fingerprint Dive into the research topics of 'Probably on time and within budget: on reachability in priced probabilistic timed automata'. Together they form a unique fingerprint.

    Cite this