About model checking PTAs via interval iteration

8 views

Skip to first unread message

unread,

Mar 15, 2023, 2:55:26 AM3/15/23

to PRISM model checker

Hello, I recently faced a problem.

I selected backwards reachability as PTA model checking method and interval iteration for model checking MDPs, (explicit engine)

but prism gave an error message:

"Precomputations (Prob0 & Prob1) must be enabled for interval iteration."

Reply all

Reply to author

Forward

0 new messages