Probabilistic systems are often modeled as factored Markov decision processes (MDPs), where the states are composed out of the local states of components and each transition involves only a small subset of the components. To exploit the concurrency that arises naturally in such systems, we formulate, as a first step, a restricted class of factored MDPs called Causally Deterministic Factored MDPs (CMDPs, for short). We use this model to port several basic notions from concurrency theory to the framework of factored MDPs. In particular, we provide a concurrent semantics for CMDPs based on the classical notion of event structures. Then using this semantics, we show that local reachability properties of CMDPs can be computed efficiently using a greedy strategy. Finally, we implement our ideas in a prototype and apply it to four models, confirming the potential for substantial improvements over state-of-the-art methods.

This is joint work with S. Akshay and Tobias Meggendorfer.