PV2 Rubicontranslates properties from PRISM to Dice

Tool that transpiles PRISM to Dice (probabilistic programming language).

Application domain/field

Type of tool

Transpiler?

Expected input

Format:

Expected output

Dice file. Rubicon can also be used to invoke Dice directly. It will then also provide logging output and the resulting probability on the last line.

Internals

Rubicon is used to model check finite-horizon Markov Chains. First it translates Discrete-time Markov Chains (DTMCs) in the PRISM language to the Dice language. Then it runs inference with Dice.

Comments

License: GPL v3.0
Model checking

Links

Last commit date

10 June 2021

Related papers

https://doi.org/10.1007/978-3-030-81688-9_27 (CAV '21)

Last publication date

15 July 2021

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.