### Abstract

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.

### License

BSD License

### Topics

- Computer science/Automata and formal languages

### Session Probabilistic_System_Zoo

- Bool_Bounded_Set
- Finitely_Bounded_Set_Counterexample
- Nonempty_Bounded_Set
- Probabilistic_Hierarchy
- Vardi
- Vardi_Counterexample

## Cite

×

Probabilistic_System_Zoo-AFP

    @article{Probabilistic_System_Zoo-AFP,
      author  = {Johannes Hölzl and Andreas Lochbihler and Dmitriy Traytel},
      title   = {A Zoo of Probabilistic Systems},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2015},
      note    = {\url{https://isa-afp.org/entries/Probabilistic_System_Zoo.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 28, 2015 : Isabelle2015