Dear Dave,
Thank you very much for getting back to me. Dr. Gethin Norman responded to my questions shortly after I posted them, too. Unfortunately, I do not have an estimate of the state size of this model. Actually, it turned out that this model was converted from an SBML model without applying the reaction-based quasi-steady-state abstraction. We have regenerated one with this abstraction, and have been able to use PRISM to model check CSL properties.
There is another interesting problem for us to explore further. Our approach is to use our STAMINA tool (
https://github.com/fluentverification/stamina) to truncate the explicit state space, and then send it to PRISM to perform CTMC analysis. STAMINA generated 2,826,140 states (1 initial) and 18,538,724 transitions on the non-abstracted model. Our observation is that the Gauss-Seidel and power methods take long time (15+ hours) to do the CTMC analysis. The machine we used has a 24-core 3.5 GHz processor and 132 GB memory. The computer was stuck at 100% CPU and less than 20% memory usage for almost the entire duration of the CTMC analysis. It did not terminate due to insufficient memory after 15+ hours, either. But it was hard to pinpoint the issue because STAMINA calls PRISM.
Now STAMINA has the ability to save the state space to a file, we can decouple STAMINA's state generation from PRISM's CTMC analysis and hopefully get better diagnostic information. I will keep you updated on what we find.