Strategies for MDP bisimilarity equivalence and inequivalence

Conference item

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.

Authors: Kiefer, S; Tang, Q

• Publication status: Accepted
• Peer review status: Peer reviewed
• Publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
• Host title: 33rd International Conference on Concurrency Theory (CONCUR 2022)
• Pages: 32:1-32:22
• Series: Leibniz International Proceedings in Informatics (LIPIcs)
• Publication date: 2022-09-06
• Acceptance date: 2022-06-25
• Event title: International Conference on Concurrency Theory (CONCUR)
• Event location: Warsaw
• Event website: https://concur2022.mimuw.edu.pl/
• Event start date: 2022-09-12
• Event end date: 2022-09-16
• DOI: 10.4230/LIPIcs.CONCUR.2022.32
• ISSN: 1868-8969
• ISBN: 978-3-95977-246-4
• Language: English
• Keywords: FFR