Model Checking Functional and Performability Properties of Stochastic Fluid Models
Sat 4 Sep 2004 17:32 BST
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.