English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

In the design of probabilistic timed systems, bounded requirements concerningbehaviour that occurs within a given time, energy, or more generally costbudget are of central importance. Traditionally, such requirements have beenmodel-checked via a reduction to the unbounded case by unfolding the modelaccording to the cost bound. This exacerbates the state space explosion problemand significantly increases runtime. In this paper, we present three newalgorithms to model-check time- and cost-bounded properties for Markov decisionprocesses and probabilistic timed automata that avoid unfolding. They are basedon a modified value iteration process, on an enumeration of schedulers, and onstate elimination techniques. We can now obtain results for any cost bound on asingle state space no larger than for the corresponding unbounded orexpected-value property. In particular, we can naturally compute the cumulativedistribution function at no overhead. We evaluate the applicability and comparethe performance of our new algorithms and their implementation on a number ofcase studies from the literature.

Efficient Algorithms for Time- and Cost-Bounded Probabilistic Model Checking