ﻻ يوجد ملخص باللغة العربية
Hidden Markov Models, HMMs, 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 HMMs as denotations of probabilistic hidden-state sequential programs: for that, we recast them as `abstract HMMs, 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}^2mathcal{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}^2mathcal{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 HMMs that is dual to the `forwards abstract HMMs - 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.
We put forward a model of action-based randomization mechanisms to analyse quantitative information flow (QIF) under generic leakage functions, and under possibly adaptive adversaries. This model subsumes many of the QIF models proposed so far. Our m
In this paper we propose a complete axiomatization of the bisimilarity distance of Desharnais et al. for the class of finite labelled Markov chains. Our axiomatization is given in the style of a quantitative extension of equational logic recently pro
We provide a computer verified exact monadic functional implementation of the Riemann integral in type theory. Together with previous work by OConnor, this may be seen as the beginning of the realization of Bishops vision to use constructive mathematics as a programming language for exact analysis.
We introduce a syntactic translation of Goedels System T parametrized by a weak notion of a monad, and prove a corresponding fundamental theorem of logical relation. Our translation structurally corresponds to Gentzens negative translation of classic
Markov chain analysis is a key technique in reliability engineering. A practical obstacle is that all probabilities in Markov models need to be known. However, system quantities such as failure rates or packet loss ratios, etc. are often not---or onl