一句话:用 Giry 单子与抽象 HMM 为隐藏状态概率程序建立信息流语义、安全序与不确定性变换。
隐马尔可夫模型(HMM)描述状态隐藏但会泄漏信息的马尔可夫过程,通常表示为三路联合概率分布。本文把 HMM 重构为抽象 HMM,作为概率隐藏状态序列程序在 Giry 单子中的指称,并用 D X → D² X 而非传统 X → D X 来编码隐藏状态,同时赋予其递增安全性的偏序。作者用一个小型 Haskell 原型展示该构造,提出推广现有概率熵的不确定性测度,分析其解析性质及与安全序的交互,并给出与正向抽象 HMM 对偶的后向不确定性变换语义。最后指出统计数据库的 Dalenius 期望本质上是组合性问题,并给出处理思路。
Hidden Markov Models, HMM's, are mathematical models of Markov processes with state that is hidden, but from which information can leak. They are typically represented as 3-way joint-probability distributions. We use HMM's as denotations of probabilistic hidden-state sequential programs: for that, we recast them as `abstract' HMM's, computations in the Giry monad $\mathbb{D}$, and we equip them with a partial order of increasing security. However to encode the monadic type with hiding over some state $\mathcal{X}$ we use $\mathbb{D}\mathcal{X}\to \mathbb{D}^2\mathcal{X}$ rather than the conventional $\mathcal{X}{\to}\mathbb{D}\mathcal{X}$ that suffices for Markov models whose state is not hidden. We illustrate the $\mathbb{D}\mathcal{X}\to \mathbb{D}^2\mathcal{X}$ construction with a small Haskell prototype. We then present uncertainty measures as a generalisation of the extant diversity of probabilistic entropies, with characteristic analytic properties for them, and show how the new entropies interact with the order of increasing security. Furthermore, we give a `backwards' uncertainty-transformer semantics for HMM's that is dual to the `forwards' abstract HMM's - it is an analogue of the duality between forwards, relational semantics and backwards, predicate-transformer semantics for imperative programs with demonic choice. Finally, we argue that, from this new denotational-semantic viewpoint, one can see that the Dalenius desideratum for statistical databases is actually an issue in compositionality. We propose a means for taking it into account.
@article{paperbot809,
title = {Abstract Hidden Markov Models: a monadic account of quantitative information flow},
author = {Annabelle McIver and Carroll Morgan and Tahiry Rabehaja},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 1},
year = {2019},
doi = {10.23638/lmcs-15(1:36)2019}
}