×

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

5 Lochbihler, Andreas
2 Hölzl, Johannes
1 Avigad, Jeremy
1 Basin, David A.
1 Echenim, Mnacho
1 Guiol, Hervé
1 Hudon, Simon
1 Matichuk, Daniel
1 Murray, Toby
1 Peltier, Nicolas
1 Sefidgar, S. Reza
1 Traytel, Dmitry
1 Wenzel, Makarius

Cited in 2 Serials

5 Journal of Automated Reasoning
1 Journal of Cryptology
all top 5

Cited in 6 Fields

9 Computer science (68-XX)
2 Probability theory and stochastic processes (60-XX)
2 Game theory, economics, finance, and other social and behavioral sciences (91-XX)
2 Information and communication theory, circuits (94-XX)
1 Combinatorics (05-XX)
1 Operations research, mathematical programming (90-XX)

Citations by Year