Kiefer, S 
ORCID: 0000-0003-4173-6877 and Tang, Q ORCID: 0000-0002-9265-3011
(2024)
Minimising the Probabilistic Bisimilarity Distance.
In: International Conference on Concurrency Theory, Calgary, Canada.
|
Text
paper.pdf - Author Accepted Manuscript Available under License Creative Commons Attribution. Download (771kB) | Preview |
Abstract
A labelled Markov decision process (MDP) 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 to the verification of probabilistic noninterference in security, we study problems of minimising probabilistic bisimilarity distances of labelled MDPs, in particular, whether there exist strategies such that the probabilistic bisimilarity distance between the induced labelled Markov chains is less than a given rational number, both for memoryless strategies and general strategies. We show that the distance minimisation problem is ∃R-complete for memoryless strategies and undecidable for general strategies. We also study the computational complexity of the qualitative problem about making the distance less than one. This problem is known to be NP-complete for memoryless strategies. We show that it is EXPTIME-complete for general strategies.
| Item Type: | Conference Item (Unspecified) |
|---|---|
| Depositing User: | Symplectic Admin |
| Date Deposited: | 03 Jul 2024 13:27 |
| Last Modified: | 05 Jun 2025 10:05 |
| DOI: | 10.4230/LIPIcs.CONCUR.2024.32 |
| URI: | https://livrepository.liverpool.ac.uk/id/eprint/3182554 |
Altmetric
Altmetric