Kiefer, S and Tang, Q 
ORCID: 0000-0002-9265-3011
(2022)
Strategies for MDP Bisimilarity Equivalence and Inequivalence.
.
|
PDF
LIPIcs-CONCUR-2022-32.pdf - Author Accepted Manuscript Download (1MB) | 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. Motivated by applications to the verification of probabilistic noninterference in security, we study problems whether there exist strategies such that the labelled MDPs become bisimilarity equivalent/inequivalent. We show that the equivalence problem is decidable; in fact, it is EXPTIME-complete and becomes NP-complete if one of the MDPs is a Markov chain. Concerning the inequivalence problem, we show that (1) it is decidable in polynomial time; (2) if there are strategies for inequivalence then there are memoryless strategies for inequivalence; (3) such memoryless strategies can be computed in polynomial time.
| Item Type: | Conference or Workshop Item (Unspecified) |
|---|---|
| Depositing User: | Symplectic Admin |
| Date Deposited: | 12 Oct 2022 11:04 |
| Last Modified: | 18 Jan 2023 20:36 |
| DOI: | 10.4230/LIPIcs.CONCUR.2022.32 |
| URI: | https://livrepository.liverpool.ac.uk/id/eprint/3165428 |
Dimensions
Dimensions
