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