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/

Zendy Plus

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

Zendy Tools

Zendy Open

Markov chains and Markov decision processes (MDPs) are well-establishedprobabilistic models. While finite Markov models are well-understood, analysingtheir infinite counterparts remains a significant challenge. Decisiveness hasproven to be an elegant property for countable Markov chains: it is generalenough to be satisfied by several natural classes of countable Markov chains,and it is a sufficient condition for simple qualitative and approximatequantitative model-checking algorithms to exist.  In contrast, existing works on the formal analysis of countable MDPs usuallyrely on ad hoc techniques tailored to specific classes. We provide here ageneral framework to analyse countable MDPs by extending the notion ofdecisiveness. Compared to Markov chains, MDPs exhibit extra non-determinismthat can be resolved in an adversarial or cooperative way, leading to multiplenatural notions of decisiveness. We show that these notions enable theapproximation of reachability and safety probabilities in countable MDPs usingsimple model-checking procedures.  We then instantiate our generic approach to two concrete classes of modelsinducing countable MDPs: non-deterministic probabilistic lossy channel systemsand partially observable MDPs. This leads to an algorithm to approximatelycompute safety probabilities in each of these classes.

Decisiveness for countable MDPs and insights for NPLCSs and POMDPs