Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: A Zoo of Probabilistic Systems


view this post on Zulip Email Gateway (Aug 22 2022 at 10:00):

From: Tobias Nipkow <nipkow@in.tum.de>
Johannes Hölzl, Andreas Lochbihler, Dmitriy Traytel

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.

This work is described in detail in the ITP 2015 publication by the authors.

http://afp.sourceforge.net/entries/Probabilistic_System_Zoo.shtml

Enjoy!
smime.p7s


Last updated: Apr 25 2024 at 01:08 UTC