Trace Refinement in Labelled Markov Decision Processes

DOI10.1007/978-3-662-49630-5_18zbMATH Open1475.68203arXiv1510.09102OpenAlexW3046661466MaRDI QIDQ2811347FDOQ2811347

Mahsa Shirmohammadi, Nathanaël Fijalkow, Stefan Kiefer

Publication date: 10 June 2016

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Abstract: Given two labelled Markov decision processes (MDPs), the trace-refinement problem asks whether for all strategies of the first MDP there exists a strategy of the second MDP such that the induced labelled Markov chains are trace-equivalent. We show that this problem is decidable in polynomial time if the second MDP is a Markov chain. The algorithm is based on new results on a particular notion of bisimulation between distributions over the states. However, we show that the general trace-refinement problem is undecidable, even if the first MDP is a Markov chain. Decidability of those problems was stated as open in 2008. We further study the decidability and complexity of the trace-refinement problem provided that the strategies are restricted to be memoryless.

Full work available at URL: https://arxiv.org/abs/1510.09102

Mathematics Subject Classification ID

Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.) (60J20) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• Introduction to algorithms
• On the Complexity of Nonnegative Matrix Factorization
• Computing a nonnegative matrix factorization -- provably
• Title not available (Why is that?)
• Title not available (Why is that?)
• Nonnegative ranks, decompositions, and factorizations of nonnegative matrices
• Title not available (Why is that?)
• Undecidable problems for probabilistic automata of fixed dimension
• On the definition of a family of automata
• On the computational complexity and geometry of the first-order theory of the reals. III: Quantifier elimination
• A Polynomial-Time Algorithm for the Equivalence of Probabilistic Automata
• Quantum Markov chains: description of hybrid systems, decidability of equivalence, and model checking linear-time properties
• On the computational complexity and geometry of the first-order theory of the reals. I: Introduction. Preliminaries. The geometry of semi-algebraic sets. The decision problem for the existential theory of the reals
• EQUIVALENCE OF LABELED MARKOV CHAINS
• Probabilistic Bisimulation: Naturally on Distributions
• Stability and Complexity of Minimising Probabilistic Automata
• Reachability in two-clock timed automata is PSPACE-complete
• On path equivalence of nondeterministic finite automata
• Approximate Verification and Enumeration Problems

Cited In (2)

• The complexity of synchronizing Markov decision processes
• Trace relations and logical preservation for continuous-time Markov decision processes

This page was built for publication: Trace Refinement in Labelled Markov Decision Processes

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2811347)