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

Markov decision processes can be viewed as transformers of probabilitydistributions. While this view is useful from a practical standpoint to reasonabout trajectories of distributions, basic reachability and safety problems areknown to be computationally intractable (i.e., Skolem-hard) to solve in suchmodels. Further, we show that even for simple examples of MDPs, strategies forsafety objectives over distributions can require infinite memory andrandomization.  In light of this, we present a novel overapproximation approach to synthesizestrategies in an MDP, such that a safety objective over the distributions ismet. More precisely, we develop a new framework for template-based synthesis ofcertificates as affine distributional and inductive invariants for safetyobjectives in MDPs. We provide two algorithms within this framework. One canonly synthesize memoryless strategies, but has relative completenessguarantees, while the other can synthesize general strategies. The runtimecomplexity of both algorithms is in PSPACE. We implement these algorithms andshow that they can solve several non-trivial examples.

MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives