Zoo Probabilistic Systems
swMATH ID: | 28541 |
Software Authors: | Hölzl, Johannes; Lochbihler, Andreas; Traytel, Dmitriy |
Description: | Isabelle Zoo of Probabilistic Systems: Numerous models of probabilistic systems are studied in the literature. Coalgebra has been used to classify them into system types and compare their expressiveness. We formalize the resulting hierarchy of probabilistic system types by modeling the semantics of the different systems as codatatypes. This approach yields simple and concise proofs, as bisimilarity coincides with equality for codatatypes. |
Homepage: | https://www.isa-afp.org/entries/Probabilistic_System_Zoo.html |
Dependencies: | Isabelle |
Related Software: | Isabelle/HOL; Lifting; Transfer; Locales; HOL; Isabelle; Archive Formal Proofs; EasyCrypt; Autoref; F*; pGCL; AmiCo; Probabilistic_While; MFMC_Countable; Density Compiler; CoSP; Coq; Lean; Edmonds-Karp; Nuprl |
Cited in: | 9 Documents |
Standard Articles
1 Publication describing the Software, including 1 Publication in zbMATH | Year |
---|---|
A formalized hierarchy of probabilistic system types. Proof pearl. Zbl 1465.68199 Hölzl, Johannes; Lochbihler, Andreas; Traytel, Dmitriy |
2015
|
all
top 5
Cited by 13 Authors
Cited in 2 Serials
5 | Journal of Automated Reasoning |
1 | Journal of Cryptology |
all
top 5