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.	-
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 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	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. ...)

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. ...)