Abstract Hidden Markov Models: a monadic account of quantitative information flow

Research output: Contribution to journalArticleResearchpeer-review

Abstract

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 D, and we equip them with a partial order of increasing security. However to encode the monadic type with hiding over some state X we use DX→D2X rather than the conventional X→DX that suffices for Markov models whose state is not hidden. We illustrate the DX→D2X 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.
LanguageEnglish
Article number36
Pages1-50
Number of pages50
JournalLogical Methods in Computer Science
Volume15
Issue number1
DOIs
Publication statusPublished - 29 Mar 2019

Fingerprint

Information Flow
Hidden Markov models
Markov Model
Semantics
Transformer
Entropy
Uncertainty Measure
Compositionality
Denotational Semantics
Haskell
Monads
Partial Order
Joint Distribution
Predicate
Markov Process
Duality
Probability Distribution
Prototype
Mathematical Model
Markov processes

Bibliographical note

Copyright the Author(s). Version archived for private and non-commercial use with the permission of the author/s and according to publisher conditions. For further rights please contact the publisher.

Cite this

@article{48463aa7c76240699a97652cf00b9996,
title = "Abstract Hidden Markov Models: a monadic account of quantitative information flow",
abstract = "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 D, and we equip them with a partial order of increasing security. However to encode the monadic type with hiding over some state X we use DX→D2X rather than the conventional X→DX that suffices for Markov models whose state is not hidden. We illustrate the DX→D2X 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.",
author = "Annabelle McIver and Carroll Morgan and Tahiry Rabehaja",
note = "Copyright the Author(s). Version archived for private and non-commercial use with the permission of the author/s and according to publisher conditions. For further rights please contact the publisher.",
year = "2019",
month = "3",
day = "29",
doi = "10.23638/LMCS-15(1:36)2019",
language = "English",
volume = "15",
pages = "1--50",
journal = "Logical Methods in Computer Science",
issn = "1860-5974",
publisher = "Technischen Universitat Braunschweig",
number = "1",

}

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

In: Logical Methods in Computer Science, Vol. 15, No. 1, 36, 29.03.2019, p. 1-50.

Research output: Contribution to journalArticleResearchpeer-review

TY - JOUR

T1 - Abstract Hidden Markov Models

T2 - Logical Methods in Computer Science

AU - McIver,Annabelle

AU - Morgan,Carroll

AU - Rabehaja,Tahiry

N1 - Copyright the Author(s). Version archived for private and non-commercial use with the permission of the author/s and according to publisher conditions. For further rights please contact the publisher.

PY - 2019/3/29

Y1 - 2019/3/29

N2 - 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 D, and we equip them with a partial order of increasing security. However to encode the monadic type with hiding over some state X we use DX→D2X rather than the conventional X→DX that suffices for Markov models whose state is not hidden. We illustrate the DX→D2X 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.

AB - 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 D, and we equip them with a partial order of increasing security. However to encode the monadic type with hiding over some state X we use DX→D2X rather than the conventional X→DX that suffices for Markov models whose state is not hidden. We illustrate the DX→D2X 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.

U2 - 10.23638/LMCS-15(1:36)2019

DO - 10.23638/LMCS-15(1:36)2019

M3 - Article

VL - 15

SP - 1

EP - 50

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

SN - 1860-5974

IS - 1

M1 - 36

ER -