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 Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Partial order reduction has been used to alleviate the state explosion problem in model checkers for nondeterministic systems. The method relies on exploring only a fragment of the full state space of a program that is enough to assess the validity of a property. In this paper, we discuss partial order reduction for probabilistic programs represented as Markov decision processes. The technique we propose preserves probabilistic quantification of reachability properties and is based on partial order reduction techniques for (nonprobabilistic) branching temporal logic. We also show that techniques for (nonprobabilistic) linear temporal logics are not correct for probabilistic reachability and that in turn our method is not sufficient for probabilistic CTL. We conjecture that our reduction technique also preserves maximum and minimum probabilities of next-free LTL properties.

Partial order reduction on concurrent probabilistic programs