iDTMC: Pmin=? gives larger probability value than Pmax=?

[mcl...@seas.upenn.edu]

Dear All,

I am using PRSIM to compute ranges of probabilities on an iDTMC using Pmin=? and Pmax=? properties. But for one of my models PRISM returns a larger probability for the Pmin=? property than the Pmax=? property (0.307 v. 0.191). I've observed this behavior on a range of initial conditions for this model. I've pasted the PRISM log to the bottom of this message.

What could be causing this?

Thanks,

Matthew

PRISM
=====

Version: 4.8.1
Date: Tue Mar 19 11:27:10 EDT 2024
Hostname: ash01
Memory limits: cudd=1g, java(heap)=16g
Command line: prism GTbaselineModelDataPerBin10.prism ../../aebsProps.props -const 'initPos=400,initSpeed=20' -javamaxmem 16g

Parsing model file "GTbaselineModelDataPerBin10.prism"...

Type:        IDTMC
Modules:     LECMarkovChain
Variables:   carPos carSpeed s seqflag contRegion

Parsing properties file "../../aebsProps.props"...

2 properties:
(1) Pmin=? [ F (carPos<=carPosThresh) ]
(2) Pmax=? [ F (carPos<=carPosThresh) ]

---------------------------------------------------------------------

Model checking: Pmin=? [ F (carPos<=carPosThresh) ]
Model constants: initPos=400,initSpeed=20

Warning: Switching to explicit engine to allow model checking of interval model.

Building model...
Model constants: initPos=400,initSpeed=20

Computing reachable states... 1445 3027 4614 6076 7487 8926 10414 11974 12948 states
Reachable states exploration and model construction done in 25.833 secs.
Sorting reachable states list...

Time for model construction: 25.917 seconds.

Warning: Deadlocks detected and fixed in 478 states

Type:        IDTMC
States:      12948 (1 initial)
Transitions: 18799

Starting probabilistic reachability...
Calculating predecessor relation for interval discrete-time Markov chain...  done (0.008 seconds)
Starting Prob0...
Prob0 took 0.014 seconds.
Starting Prob1...
Prob1 took 0.005 seconds.
target=10488, yes=12209, no=139, maybe=600
Starting value iteration (min)...
Value iteration (min, with Gauss-Seidel) took 25 iterations, 22500 multiplications and 0.015 seconds.
Probabilistic reachability took 0.018 seconds.

Value in the initial state: 0.3066986762704398

Time for model checking: 0.074 seconds.

Result: 0.3066986762704398 (+/- 2.9262772418107085E-6 estimated; rel err 9.541212493628063E-6)

---------------------------------------------------------------------

Model checking: Pmax=? [ F (carPos<=carPosThresh) ]
Model constants: initPos=400,initSpeed=20

Warning: Switching to explicit engine to allow model checking of interval model.

Starting probabilistic reachability...
Starting Prob0...
Prob0 took 0.003 seconds.
Starting Prob1...
Prob1 took 0.004 seconds.
target=10488, yes=12209, no=139, maybe=600
Starting value iteration (max)...
Value iteration (max, with Gauss-Seidel) took 27 iterations, 24300 multiplications and 0.015 seconds.
Probabilistic reachability took 0.015 seconds.

Value in the initial state: 0.1905079430218461

Time for model checking: 0.037 seconds.

Result: 0.1905079430218461 (+/- 4.3158563069566074E-7 estimated; rel err 2.2654469091935425E-6)

---------------------------------------------------------------------

Note: There were 3 warnings during computation.

[Dave Parker]

Hi Matthew,

Thanks for this. It indeed seems wrong. Would you be able to send me the
model (off list) so that I can take a look?

Best wishes,

Dave

> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to prismmodelchec...@googlegroups.com
> <mailto:prismmodelchec...@googlegroups.com>.
> To view this discussion on the web, visit
> https://groups.google.com/d/msgid/prismmodelchecker/5671760f-b853-46da-a960-2c2f4647c76fn%40googlegroups.com <https://groups.google.com/d/msgid/prismmodelchecker/5671760f-b853-46da-a960-2c2f4647c76fn%40googlegroups.com?utm_medium=email&utm_source=footer>.