Abstract Hidden Markov Models: a monadic account of quantitative information flow
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:...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2019-03-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/3851/pdf |
| _version_ | 1797268592046112768 |
|---|---|
| author | Annabelle McIver Carroll Morgan Tahiry Rabehaja |
| author_facet | Annabelle McIver Carroll Morgan Tahiry Rabehaja |
| author_sort | Annabelle McIver |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:34:55Z |
| format | Article |
| id | doaj.art-d7c385d3b33b4485ba84a65c73b4b875 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:34:55Z |
| publishDate | 2019-03-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-d7c385d3b33b4485ba84a65c73b4b8752024-03-08T10:27:57ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742019-03-01Volume 15, Issue 110.23638/LMCS-15(1:36)20193851Abstract Hidden Markov Models: a monadic account of quantitative information flowAnnabelle McIverCarroll MorganTahiry RabehajaHidden 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.https://lmcs.episciences.org/3851/pdfcomputer science - logic in computer science |
| spellingShingle | Annabelle McIver Carroll Morgan Tahiry Rabehaja Abstract Hidden Markov Models: a monadic account of quantitative information flow Logical Methods in Computer Science computer science - logic in computer science |
| title | Abstract Hidden Markov Models: a monadic account of quantitative information flow |
| title_full | Abstract Hidden Markov Models: a monadic account of quantitative information flow |
| title_fullStr | Abstract Hidden Markov Models: a monadic account of quantitative information flow |
| title_full_unstemmed | Abstract Hidden Markov Models: a monadic account of quantitative information flow |
| title_short | Abstract Hidden Markov Models: a monadic account of quantitative information flow |
| title_sort | abstract hidden markov models a monadic account of quantitative information flow |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/3851/pdf |
| work_keys_str_mv | AT annabellemciver abstracthiddenmarkovmodelsamonadicaccountofquantitativeinformationflow AT carrollmorgan abstracthiddenmarkovmodelsamonadicaccountofquantitativeinformationflow AT tahiryrabehaja abstracthiddenmarkovmodelsamonadicaccountofquantitativeinformationflow |