Numerous models of probabilistic systems are studied in the literature. Coalgebra has been used to classify them into system types and compare their expressiveness. In this work, we formalize the resulting hierarchy of probabilistic system types in Isabelle/HOL by modeling the semantics of the different systems as codatatypes. This approach yields simple and concise proofs, as bisimilarity coincides with equality for codatatypes. On the way, we develop libraries of bounded sets and discrete probability distributions and integrate them with the facility for (co)datatype definitions.
CITATION STYLE
Hölzl, J., Lochbihler, A., & Traytel, D. (2015). A formalized hierarchy of probabilistic system types: Proof pearl. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9236, pp. 203–220). Springer Verlag. https://doi.org/10.1007/978-3-319-22102-1_13
Mendeley helps you to discover research relevant for your work.