Annabelle McIver ; Carroll Morgan ; Tahiry Rabehaja - Abstract Hidden Markov Models: a monadic account of quantitative information flow

lmcs:3851 - Logical Methods in Computer Science, March 29, 2019, Volume 15, Issue 1 - https://doi.org/10.23638/LMCS-15(1:36)2019
Abstract Hidden Markov Models: a monadic account of quantitative information flowArticle

Authors: Annabelle McIver ; Carroll Morgan ; Tahiry Rabehaja

    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.


    Volume: Volume 15, Issue 1
    Published on: March 29, 2019
    Accepted on: February 7, 2019
    Submitted on: August 9, 2017
    Keywords: Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • Making software more reliable using a new model for entropies of computers' internal state; Funder: Australian Research Council (ARC); Code: DP120101413

    Consultation statistics

    This page has been seen 1239 times.
    This article's PDF has been downloaded 234 times.