PV2 ⊧ Rubicontranslates properties from PRISM to Dice

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

Application domain/field

• Finite horizon reachability properties
• Probabilistic model checking
• Markov chains
• Probabilistic inference

Type of tool

Transpiler?

Expected input

• Program/model
• Property

Format:

• Program: PRISM language
• Property: Passed as an argument, PRISM's specification language

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