Markov Chains and Markov Decision Processes in Isabelle/HOL
Markov Chains and Markov Decision Processes in Isabelle/HOL
复制标题
Isabelle/HOL 中的马尔可夫链和马尔可夫决策过程
DOI：
10.1007/s10817-016-9401-5
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Johannes Hölzl
中科院分区：
文献类型：
--
作者：
Johannes Hölzl
本文提出了一个广泛的形式化的马尔可夫链（MC）和马尔可夫决策过程（MDP），离散时间和（可能是无限的）离散状态空间。该形式化方法从共代数的角度对表示MC的变迁系统进行了研究，并构造了它们的迹空间。在这些迹空间的公平性，可达性和平稳分布等性质的形式化。与MC类似，MDP被表示为具有迹空间构造的转换系统。这些迹空间提供了对所有可能的非确定性决策的最大和最小期望。作为应用程序，我们提供了一个有限的可达性问题的证明，我们涉及的概率守卫命令语言的指称语义和操作语义。我们的形式化的一个显着特点是秩序理论和coalgebraic查看我们的概念：我们认为过渡系统的coalgebras，我们认为痕迹coinductive流，我们提供迭代计算规则的期望，我们定义了许多属性的痕迹最小或最大的不动点。
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.
登录
查看更多内容
马尔可夫链的交互式验证：两个分布式协议案例研究
DOI：
10.4204/eptcs.103.2
发表时间：
2012
期刊：
影响因子：
--
作者：
Johannes Hölzl;Tobias Nipkow
通讯作者：
Tobias Nipkow
DOI：
10.1007/s10817-017-9404-x
发表时间：
2017
期刊：
Journal of Automated Reasoning
影响因子：
--
作者：
Jeremy Avigad;Johannes Hölzl;Luke Serafin
通讯作者：
Luke Serafin
DOI：
10.1007/978-3-319-43144-4_30
发表时间：
2016
期刊：
影响因子：
--
作者：
Johannes Hölzl
通讯作者：
Johannes Hölzl
DOI：
--
发表时间：
2002
期刊：
影响因子：
--
作者：
B. Davey;H. Priestley
通讯作者：
H. Priestley
HOL 中分类马尔可夫链的形式化推理
影响因子：
--
作者：
Liya Liu;O. Hasan;Vincent Aravantinos;S. Tahar
通讯作者：
S. Tahar