A Formalized Hierarchy of Probabilistic System Types Proof Pearl

被引：12

作者：

Hoelzl, Johannes ^{[1
]}

Lochbihler, Andreas ^{[2
]}

Traytel, Dmitriy ^{[1
]}

机构：

[1] Tech Univ Munich, Fak Informat, Munich, Germany

[2] Swiss Fed Inst Technol, Inst Informat Secur, Dept Comp Sci, Zurich, Switzerland

来源：

INTERACTIVE THEOREM PROVING | 2015年 / 9236卷

关键词：

BISIMULATION;

D O I：

10.1007/978-3-319-22102-1_13

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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.

引用

页码：203 / 220

页数：18

共 26 条

[1]

[Anonymous], 2001, Handbook of Process Algebra, DOI DOI 10.1016/B978-044482830-9/50029-1

[2] Proofs of randomized algorithms in COQ [J].

Audebaud, Philippe ;

Paulin-Mohring, Christine .

SCIENCE OF COMPUTER PROGRAMMING, 2009, 74 (08) :568-589

[3] A hierarchy of probabilistic system types [J].

Bartels, F ;

Sokolova, A ;

de Vink, E .

THEORETICAL COMPUTER SCIENCE, 2004, 327 (1-2) :3-22

[4] Probabilistic Relational Verification for Cryptographic Implementations [J].

Barthe, Gilles ;

Fournet, Cedric ;

Gregoire, Benjamin ;

Strub, Pierre-Yves ;

Swamy, Nikhil ;

Zanella-Beguelin, Santiago .

ACM SIGPLAN NOTICES, 2014, 49 (01) :193-205

[5]

Blanchette Jasmin Christian, 2014, Interactive Theorem Proving. 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014. Proceedings: LNCS 8558, P93, DOI 10.1007/978-3-319-08970-6_7

[6]

[7] Witnessing (Co)datatypes [J].

Blanchette, Jasmin Christian ;

Popescu, Andrei ;

Traytel, Dmitriy .

PROGRAMMING LANGUAGES AND SYSTEMS, 2015, 9032 :359-382

[8] Bisimulation for probabilistic transition systems: a coalgebraic approach [J].

de Vink, EP ;

Rutten, JJMM .

THEORETICAL COMPUTER SCIENCE, 1999, 221 (1-2) :271-293

[9]

Deng Y., 2014, SEMANTICS PROBABILIS

[10] A Verified Compiler for Probability Density Functions [J].

Eberl, Manuel ;

Hoelzl, Johannes ;

Nipkow, Tobias .

PROGRAMMING LANGUAGES AND SYSTEMS, 2015, 9032 :80-104

← 1 2 3 →