www.prismmodelchecker.org

PRISM Benchmark Suite - Properties (CTMCs)

CTMC steady-state

Computing the steady state probabilities or rewards in a CTMC, i.e. PRISM properties of the form:

  • S=? [ ... ]
  • R=? [ S ]
Model Property PRISM property
& description
Extra
parameters
Notes
cluster premium_steady S=? [ "premium" ]
Long-run probability that premium QoS will be delivered.
-
erlangen avail_ss S=? [ "avail" ]
Long-run probability that the mainframe is available.
-
erlangen thru_hi_ss R{"thru_high"}=? [ S ]
Long-run expected throughout of high priority jobs.
-
fms productivity R{"productivity"}=? [ S ]
Expected productivity of the system
-
kanban throughput R{"throughput"}=? [ S ]
Expected throughput of the system
-
polling s1 S=? [ s1=1 & !(s=1 & a=1) ]
Probability that in the long run station 1 is awaiting service
-
tandem customers R=?[S]
Long run expected customers in the network
-

CTMC quantitative reachability

Computing the probability of reaching some set of states in a CTMC, i.e. PRISM properties of the form:

  • P=? [ F ... ]
  • P=? [ ... U ... ]

Quantitative properties only (i.e. the probability is not 0/1 for at least some states).

Model Property PRISM property
& description
Extra
parameters
Notes
embedded actuators P=? [ !"down" U "fail_actuators" ]
Probability of actuator failure occurring first
-
embedded io P=? [ !"down" U "fail_io" ]
Probability of I/O failure occurring first occurring first
-
embedded main P=? [ !"down" U "fail_main" ]
Probability of main processor failure occurring first
-
embedded sensors P=? [ !"down" U "fail_sensors" ]
Probability of sensor failure occurring first
-
polling s1_before_s2 P=? [ !(s=2 & a=1) U (s=1 & a=1) ]
Probability that station 1 is served before station 2
-

CTMC expected reachability

Computing the expected accumulated reward to reach some set of states in a CTMC, i.e. PRISM properties of the form:

  • R=? [ F ... ]
Model Property PRISM property
& description
Extra
parameters
Notes
embedded danger_time R{"danger"}=? [ F "down" ]
Expected time spent in "danger" before "down"
-
embedded up_time R{"up"}=? [ F "down" ]
Expected time spent in "up" before "down"
-
mapk_cascade activated_time R{"time"}=?[F kpp=N ]
Expected time until all MAPK are activated at the same time instant
-

CTMC time-bounded reachability

Computing the probability of a formula holding for some time bound in a CTMC, i.e. PRISM properties of the form:

  • P=? [ F<=T ... ], P=? [ F[T1,T2] ... ], P=? [ F>=T ... ]
  • P=? [ ... U<=T ... ], P=? [ ... U[T1,T2] ... ], P=? [ ... U>=T ... ],
Model Property PRISM property
& description
Extra
parameters
Notes
cluster qos1 P=? [ F<=T !"minimum" ]
Probability the QoS drops below minimum quality within T time units
T (time bound: e.g. ...)
cluster qos2 P=? [ true U[T,T] !"minimum" ]
Probability of facing insufficient QoS after T time units
T (time bound: e.g. ...)
cluster qos3 P=? [ "minimum" U<=T "premium" {"minimum"}{min} ]
Probability of going from minimum QoS to premium QoS within T time units without violating the minimum QoS constraint along the way
T (time bound: e.g. ...)
cluster qos4 P=? [ !"minimum" U>=T "minimum" ]
Probability that it takes more than T time units to recover from insufficient QoS
T (time bound: e.g. ...)
embedded failure_T P=? [ true U<=(T*3600) "down" ]
Probability of any failure occurring within T hours
T (time bound: e.g. ...)
embedded actuators_T P=? [ !"down" U<=(T*3600) "fail_actuators" ]
Probability of actuator failure occurring first (within T hours)
T (time bound: e.g. ...)
embedded io_T P=? [ !"down" U<=(T*3600) "fail_io" ]
Probability of I/O failure occurring first occurring first (within T hours)
T (time bound: e.g. ...)
embedded main_T P=? [ !"down" U<=(T*3600) "fail_main" ]
Probability of main processor failure occurring first within (T hours)
T (time bound: e.g. ...)
embedded sensors_T P=? [ !"down" U<=(T*3600) "fail_sensors" ]
Probability of sensor failure occurring first within (T hours)
T (time bound: e.g. ...)
polling station1_polled P=?[ F<=T (s=1 & a=0) ]
Probability that station 1 will be polled within T time units
T (time bound: e.g. ...)
tandem network P=? [ F<=T sc=c & sm=c & ph=2 ]
Probability network becomes full in T time units
T (time bound: e.g. ...)
tandem first_queue P=? [ F<=T sc=c ]
Probability first queue becomes full in T time units
T (time bound: e.g. ...)
tandem second_queue P=? [ sm=c U<=T sm<c ]
Probability of leaving a situation where the second queue is entirely populated within T time units
T (time bound: e.g. ...)

CTMC transient

Computing the probability or expected value of a reward at a time instant in a CTMC, i.e. PRISM properties of the form:

  • P=? [ F=T ]
  • R=? [ I=T ]
Model Property PRISM property
& description
Extra
parameters
Notes
cluster operational R{"percent_op"}=? [ I=T ]
Percentage of operational workstations at time T
T (time instant: e.g. ...)
erlangen avail_tr P=? [ F=T "avail" ]
Probability that the mainframe is available at time T
T (time instant: e.g. ...)
erlangen thru_hi_tr R{"thru_high"}=? [ I=T ]
Expected throughout of high priority jobs at time point T
T (time instant: e.g. ...)
mapk_cascade activated_T R{"activated"}=?[ I=T ]
Expected amount of activated MAPK at time T
T (time instant: e.g. ...)
tandem customers_T R=? [ I=T ]
Expected number of customers in the network at time T
T (time instant: e.g. ...)

CTMC cumulative (time-bounded) reward

Computing the expected accumulated reward up to some time bound in a CTMC, i.e. PRISM properties of the form:

  • R=? [ C<=T ]
Model Property PRISM property
& description
Extra
parameters
Notes
cluster below_min R{"time_not_min"}=? [ C<=T ]
Expected time the system spends below minimum QoS until time T
T (time bound: e.g. ...)
cluster repairs R{"num_repairs"}=? [ C<=T ]
Expected number of repairs by time T
T (time bound: e.g. ...)
embedded danger_T R{"danger"}=? [ C<=(T*3600) ]
Expected time spent in "danger" by time T (hours)
T (time bound: e.g. ...)
embedded down_T R{"down"}=? [ C<=(T*3600) ]
Expected time spent in "down" by time T (hours)
T (time bound: e.g. ...)
embedded up_T R{"up"}=? [ C<=(T*3600) ]
Expected time spent in "up" by time T (hours)
T (time bound: e.g. ...)
mapk_cascade reactions R{"reactions"}=? [ C<=T ]
Expected number of reactions between MAPK and MAPKK by time T
T (time bound: e.g. ...)
polling waiting R{"waiting"}=?[C<=T]
Expected time station 1 is waiting to be served by time T
T (time bound: e.g. ...)
polling served R{"served"}=?[C<=T]
Expected number of times station1 is served by time T
T (time bound: e.g. ...)

Benchmarks