Hello,
We have been developing approximation techniques to analyze infinite-state continuous Markov chain models. When verifying the results generated by our method against Fast Adaptive Uniformization, we got inconsistent results. I am using attached infinite state model(model.prism) and property 'P=? [ true U[0,800] ((LacI<20)&(TetR>40)) ]'.
Verification result:
Version: 4.4
Date: Wed Feb 27 11:37:34 MST 2019
Hostname: xx
Memory limits: cudd=1g, java(heap)=4.4g
Command line: prism -javamaxmem 5g -transientmethod fau -fauepsilon 1e-9 model.prism -pf 'P=? [ true U[0,800] ((LacI<20)&(TetR>40)) ]'
Parsing model file "model.prism"...
1 property:
(1) P=? [ true U[0,800] ((LacI<20)&(TetR>40)) ]
Type: CTMC
Modules: TetR_def LacI_def
Variables: TetR LacI
---------------------------------------------------------------------
Model checking: P=? [ true U[0,800] ((LacI<20)&(TetR>40)) ]
Starting transient probability computation using fast adaptive uniformisation...
Total probability lost is : 1.4664550684884148E-9
Maximal number of states stored during analysis : 367
Model checking completed in 0.099 secs.
Result (probability): 0.0
The actual probability value for this property is "0.7255". Is there anything I am missing while using the FAU method?
Thanks for the help!
Sincerely,
Thakur Neupane