## Model Checking Functional and Performability Properties of Stochastic Fluid Models

#### by Tony Garnock-Jones / @leastfixedpoint

Precise model-checking of models with continuous state variables is difficult. DTMCs and CTMCs, discrete and continuous time Markov Chains respectively, while able to optionally model continuous time cannot model a continuous state space, having only a discrete state space. (cf. PEPA) Markovian Reward Models have a strongly limited capability for modelling continuous state — limitations include for instance that the behaviour may not depend on the continuous state variable!

Stochastic Fluid Models do better [could it be applied to the
RKIP/ERK
pathway problem?] at the expense of significantly more difficult
analysis. Only a *very* small number of continuous state
variable can be handled.

*I missed the end — had to leave to see the
stochastic-ambients talk.*