Computing the steady state probabilities or rewards in a CTMC, i.e. PRISM properties of the form:
Model  Property  PRISM property & description 
Extra parameters 
Notes 
cluster  premium_steady 
S=? [ "premium" ] Longrun 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 
 
Computing the probability of reaching some set of states in a CTMC, i.e. PRISM properties of the form:
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 
 
Computing the expected accumulated reward to reach some set of states in a CTMC, i.e. PRISM properties of the form:
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 
 
Computing the probability of a formula holding for some time bound in a CTMC, i.e. PRISM properties of the form:
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. ...) 
Computing the expected value of a reward at a time instant in a CTMC, i.e. PRISM properties of the form:
Model  Property  PRISM property & description 
Extra parameters 
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. ...) 
Computing the expected accumulated reward up to some time bound in a CTMC, i.e. PRISM properties of the form:
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. ...) 