2026-07-20T14:46:33Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13290 2024-03-06T10:52:02Z ddc:004 open_access

Comparing Labelled Markov Decision Processes Kiefer, Stefan Tang, Qiyi Markov decision processes Markov chains Behavioural metrics A labelled Markov decision process is a labelled Markov chain with nondeterminism, i.e., together with a strategy a labelled MDP induces a labelled Markov chain. The model is related to interval Markov chains. Motivated by applications of equivalence checking for the verification of anonymity, we study the algorithmic comparison of two labelled MDPs, in particular, whether there exist strategies such that the MDPs become equivalent/inequivalent, both in terms of trace equivalence and in terms of probabilistic bisimilarity. We provide the first polynomial-time algorithms for computing memoryless strategies to make the two labelled MDPs inequivalent if such strategies exist. We also study the computational complexity of qualitative problems about making the total variation distance and the probabilistic bisimilarity distance less than one or equal to one. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Stefan Kiefer and Qiyi Tang 2020 Is Part Of LIPIcs, Volume 182, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2020.49 urn:nbn:de:0030-drops-132903 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.49 eng https://creativecommons.org/licenses/by/3.0/legalcode