# PRISM Benchmark Suite - Properties (CTMCs)

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 Extraparameters Notes cluster premium_steady S=? [ "premium" ] Long-run probability that premium QoS will be delivered. - 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 Extraparameters 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 Extraparameters 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 Extraparameters 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

### CTMC instantaneous reward

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

• R=? [ I=T ]
 Model Property PRISM property & description Extraparameters Notes cluster operational R{"percent_op"}=?[ I=T ] Percentage of operational workstations at time T T (time bound: e.g. ...) mapk_cascade activated_T R{"activated"}=?[ I=T ] Expected amount of activated MAPK at time T T (time bound: e.g. ...) tandem customers_T R=?[I=T] Expected number of customers in the network at time T T (time bound: 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 Extraparameters 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. ...)