Groups keyboard shortcuts have been updated

Dismiss

See shortcuts

PRISM model checker developers

Contact owners and managers

1–30 of 91

This group is for developers working on the probabilistic model checker PRISM, extensions of it, or other related tools. We welcome all questions, comments and discussions.

PRISM users with questions or comments should use the "PRISM model checker" forum, also on Google Groups.

0 selected

2/8/24

Documentation for BDDs used in NondetModel and ProbModel

I am trying to understand how the symbolic engine handles MDPs. I found the various BDDs and BDDVars

unread,

Documentation for BDDs used in NondetModel and ProbModel

I am trying to understand how the symbolic engine handles MDPs. I found the various BDDs and BDDVars

2/8/24

8/22/23

Convert non probabilistic models to PRISM models

hi~Perhaps anyone knows if there is open source software can automately convert AADL/Simulnik.. (non

unread,

Convert non probabilistic models to PRISM models

hi~Perhaps anyone knows if there is open source software can automately convert AADL/Simulnik.. (non

8/22/23

shuhao qi, Dave Parker2

8/1/23

Empty .dot for smg model

Hi Shuhao, Thanks for reporting this. There were various bugs in that code. We've been

unread,

Empty .dot for smg model

Hi Shuhao, Thanks for reporting this. There were various bugs in that code. We've been

8/1/23

7/6/23

Dear all, We are pleased to announce that version 4.8 of PRISM has now been released, and is

unread,

Dear all, We are pleased to announce that version 4.8 of PRISM has now been released, and is

7/6/23

Stamina Model Checker, Dave Parker3

6/23/23

Counterintuitive Discrepancy in PRISM Runtimes

Hi, I don't see an immediately obvious cause for this, especially if the model is small enough to

unread,

Counterintuitive Discrepancy in PRISM Runtimes

Hi, I don't see an immediately obvious cause for this, especially if the model is small enough to

6/23/23

2/12/23

Model Checking on Feed Forward (FF) Artificial Neural Network (ANN)

Hello Everyone. How can we apply model checking on FF ANN ? As I searched this is how flow works : -

unread,

Model Checking on Feed Forward (FF) Artificial Neural Network (ANN)

Hello Everyone. How can we apply model checking on FF ANN ? As I searched this is how flow works : -

2/12/23

11/22/22

How PRISM verify CSL properties of an CTMC

Hello everyone, I have recently used the Monte Carlo simulation to verify some properties of CTMC (eg

unread,

How PRISM verify CSL properties of an CTMC

Hello everyone, I have recently used the Monte Carlo simulation to verify some properties of CTMC (eg

11/22/22

8/17/22

Command line prompt does not work

Hello, I installed prism on mac os. I used to run xprism to use prism GUI for model checking, but

unread,

Command line prompt does not work

Hello, I installed prism on mac os. I used to run xprism to use prism GUI for model checking, but

8/17/22

8/15/22

Prism generated adversary for MDP

Hello, I am confused about the prism-generated adversary of the following MDP- mdp module M s:[0..3]

unread,

Prism generated adversary for MDP

Hello, I am confused about the prism-generated adversary of the following MDP- mdp module M s:[0..3]

8/15/22

3/12/22

PRISM API for Python

Hello developers, I am currently developing a program in Python and would like to fetch data from

unread,

PRISM API for Python

Hello developers, I am currently developing a program in Python and would like to fetch data from

3/12/22

Dong Yuanfa, Dave Parker2

11/25/21

Properties Verification of PTA

Hi Dong, We don't support full PTCTL, but for this specific example it is feasible because you

unread,

Properties Verification of PTA

Hi Dong, We don't support full PTCTL, but for this specific example it is feasible because you

11/25/21

Geeta Mahala, Gethin Norman3

5/17/21

RE: Filter Property Specification

Hello Gethin, Thank you so much for reply. I have some more questions : 1. Can we generate counter

unread,

RE: Filter Property Specification

Hello Gethin, Thank you so much for reply. I have some more questions : 1. Can we generate counter

5/17/21

4/6/21

state chart diagram to prism

hello everyone, I am new into prism and wander if it is possible to convert state chart diagram to

unread,

state chart diagram to prism

hello everyone, I am new into prism and wander if it is possible to convert state chart diagram to

4/6/21

3/22/21

Dear all, We are pleased to announce that version 4.7 of PRISM has just been released, and is

unread,

Dear all, We are pleased to announce that version 4.7 of PRISM has just been released, and is

3/22/21

Zhen Zhang, Dave Parker3

4/21/20

No verification results generated when using Gauss-Seidel CTMC model

Dear Dave, Thank you very much for getting back to me. Dr. Gethin Norman responded to my questions

unread,

No verification results generated when using Gauss-Seidel CTMC model

Dear Dave, Thank you very much for getting back to me. Dr. Gethin Norman responded to my questions

4/21/20

Khayyam Salehi, Joachim Klein4

12/31/19

symbolically compute reachability probability of a state in a DTMC

Hi, > Thanks for your response. How can I do this by code? I am writing a > program and I have

unread,

symbolically compute reachability probability of a state in a DTMC

Hi, > Thanks for your response. How can I do this by code? I am writing a > program and I have

12/31/19

lotfi larbaoui, Dave Parker2

9/26/19

How to generate all adversaries of the MDP ?

Hi, We don't actually explicitly generate them all anywhere because there are typically too many

unread,

How to generate all adversaries of the MDP ?

Hi, We don't actually explicitly generate them all anywhere because there are typically too many

9/26/19

Andrew Wells, Joachim Klein2

9/23/19

Symbolic Engine with LTL

Hi Andrew, > I'm curious how PRISM uses the symbolic engine to verify LTL properties > of

unread,

Symbolic Engine with LTL

Hi Andrew, > I'm curious how PRISM uses the symbolic engine to verify LTL properties > of

9/23/19

bensalah...@gmail.com, Dave Parker3

9/19/19

assume-guarantee verification for probabilistic systems

Hello Dave, you have, exactly, answered my question. Best regards, On Thu, Aug 8, 2019 at 10:06 AM

unread,

assume-guarantee verification for probabilistic systems

Hello Dave, you have, exactly, answered my question. Best regards, On Thu, Aug 8, 2019 at 10:06 AM

9/19/19

Andrew Wells, Joachim Klein2

6/14/19

PRISM for co-safe LTL

Hi Andrew, > I'm trying to understand the inner workings of PRISM, especially in > cases

unread,

PRISM for co-safe LTL

Hi Andrew, > I'm trying to understand the inner workings of PRISM, especially in > cases

6/14/19

Zhen Zhang, Dave Parker3

6/6/19

Will there be updates to SBML-to-PRISM Translation?

Dear Dave, Thank you for your prompt reply. I created an biosynthesis pathway from the Sabio-RK

unread,

Will there be updates to SBML-to-PRISM Translation?

Dear Dave, Thank you for your prompt reply. I created an biosynthesis pathway from the Sabio-RK

6/6/19

5/21/19

PRISM 4.5 and PRISM-games 2.1

Dear all, I am pleased to announce that we have recently released new versions of both PRISM and

unread,

PRISM 4.5 and PRISM-games 2.1

Dear all, I am pleased to announce that we have recently released new versions of both PRISM and

5/21/19

Calvin Chau, Dave Parker9

4/16/19

Accessing transition matrix by action

Hello Dave, it worked out, thanks a lot! Best regards Calvin Am Dienstag, 16. April 2019 12:15:22 UTC

unread,

Accessing transition matrix by action

Hello Dave, it worked out, thanks a lot! Best regards Calvin Am Dienstag, 16. April 2019 12:15:22 UTC

4/16/19

Ali A. Noroozi2

3/22/19

Partitioning a list of states

Can anybody help me with this? On Wednesday, March 6, 2019 at 6:14:05 PM UTC+3, Ali A. Noroozi wrote:

unread,

Partitioning a list of states

Can anybody help me with this? On Wednesday, March 6, 2019 at 6:14:05 PM UTC+3, Ali A. Noroozi wrote:

3/22/19

thakur....@aggiemail.usu.edu, Joachim Klein2

2/27/19

Hi Thakur, you are right: There was a bug in FAU model exploration that was fixed after the 4.4

unread,

Hi Thakur, you are right: There was a bug in FAU model exploration that was fixed after the 4.4

2/27/19

Ali A. Noroozi, Joachim Klein4

2/26/19

Finding states that have only one self-loop

Hi Joachim, Yes, this is exactly what I was looking for. Thank you. On Tuesday, February 26, 2019 at

unread,

Finding states that have only one self-loop

Hi Joachim, Yes, this is exactly what I was looking for. Thank you. On Tuesday, February 26, 2019 at

2/26/19

bensalah...@gmail.com, Dave Parker2

11/15/18

Probabilistic Model Checking of Labelled Markov Processes via Finite Approximate Bisimulations

Hi Bensalah, We don't have an implementation of that in PRISM I'm afraid. Best wishes, Dave

unread,

Probabilistic Model Checking of Labelled Markov Processes via Finite Approximate Bisimulations

Hi Bensalah, We don't have an implementation of that in PRISM I'm afraid. Best wishes, Dave

11/15/18

iram....@seecs.edu.pk

11/7/18

pick selective values from the pool values

Hi, Is there a way to pick selective values from pool of values when initializing the range of a

unread,

pick selective values from the pool values

Hi, Is there a way to pick selective values from pool of values when initializing the range of a

11/7/18

iram....@seecs.edu.pk

10/26/18

Local copy of build model

Hi, Does prism save a local copy of the model after it is built? if yes, how can we access it?

unread,

Local copy of build model

Hi, Does prism save a local copy of the model after it is built? if yes, how can we access it?

10/26/18

iram....@seecs.edu.pk

10/14/18

Counter example generation

Hi, can some one guide me, how can we view the counter examples in our model using DTMC and explicit

unread,

Counter example generation

Hi, can some one guide me, how can we view the counter examples in our model using DTMC and explicit

10/14/18

Search

Clear search

Close search

Google apps

Main menu