Markov Chains and Markov Decision Processes in Isabelle/HOL

作者：Hoelzl Johannes

来源：Journal of Automated Reasoning, 2017, 59(3): 345-387.

DOI：10.1007/s10817-016-9401-5

• Markov chains
• Markov decision processes
• Probabilistic guarded command language
• Probabilistic model checking
• Isabelle/HOL

This paper presents an extensive formalization of Markov chains (MCs) and Markov decision processes (MDPs), with discrete time and (possibly infinite) discrete state-spaces. The formalization takes a coalgebraic view on the transition systems representing MCs and constructs their trace spaces. On these trace spaces properties like fairness, reachability, and stationary distributions are formalized. Similar to MCs, MDPs are represented as transition systems with a construction for trace spaces. These trace spaces provide maximal and minimal expectation over all possible non-deterministic decisions. As applications we provide a certifier for finite reachability problems and we relate the denotational semantics and operational semantics of the probabilistic guarded command language. A distinctive feature of our formalization is the order-theoretic and coalgebraic view on our concepts: we view transition systems as coalgebras, we view traces as coinductive streams, we provide iterative computation rules for expectations, and we define many properties on traces as least or greatest fixed points.

• 出版日期2017-10