PRISM model checker developers

1–30 of 86

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

Feb 12

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 : -

Feb 12

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

Edoardo, Dave Parker3

9/20/18

Using MTBDD Engine with ModelGenerator

Excellent. Many thanks for this Edoardo. I'll look at the PR. Glad it is working well for you.

unread,

Using MTBDD Engine with ModelGenerator

Excellent. Many thanks for this Edoardo. I'll look at the PR. Glad it is working well for you.

9/20/18

Ali A. Noroozi, Joachim Klein2

9/1/18

Findig paths and traces of a dtmc model

Hi, > Given a dtmc model, which is an instance of ProbModel class, how can I > find all paths

unread,

Findig paths and traces of a dtmc model

Hi, > Given a dtmc model, which is an instance of ProbModel class, how can I > find all paths

9/1/18

Ali A. Noroozi, Joachim Klein3

8/21/18

Creating Linux and Windows binaries for a PRISM extension

Thanks Dr. Klein. This will do it. On Monday, August 20, 2018 at 9:52:04 PM UTC+4:30, Joachim Klein

unread,

Creating Linux and Windows binaries for a PRISM extension

Thanks Dr. Klein. This will do it. On Monday, August 20, 2018 at 9:52:04 PM UTC+4:30, Joachim Klein

8/21/18

iram....@seecs.edu.pk, Joachim Klein4

8/10/18

Explicit engine

Hi, > Thank you for your detailed reply. Attached is the log file with 22g > cudd and 8g java

unread,

Explicit engine

Hi, > Thank you for your detailed reply. Attached is the log file with 22g > cudd and 8g java

8/10/18

Ali A. Noroozi, Joachim Klein3

8/9/18

How to extract transition probability from transition matrix MTBDD

Dear Joachim, Yes, it helped. I wanted transitions of reachable states. I was already working on

unread,

How to extract transition probability from transition matrix MTBDD

Dear Joachim, Yes, it helped. I wanted transitions of reachable states. I was already working on

8/9/18

Search

Clear search

Close search

Google apps

Main menu