Ticket #40 (new defect)

Opened 6 years ago

Error bounds and the numerical model-checking engine

Reported by: ivan.zapreev Owned by: ivan.zapreev
Priority: major Milestone: MRMC future
Component: Core Version: 1.3
Keywords: Cc: nguyen, christinajansen

Description

Error bounds are not properly computed and used! For nested formulas it is not even known how to derive error bounds. For plain steady-state operator it is known but is not done:

  • Since probabilistic results are computed with a certain error bound for the steady-state (long-run) operators of PRCTL, PCTL, CSL and CSRL, we have to check +- error bound bound. WARNING: Here the provided error bound is not quite correct, it is tighter than it should be but at least it is something!
     S{<=>p}[phi], err = get_error_bound()
    
     1. In case of ergodic MC we have to take:
             error_bound = err * | phi |
     2. In case of Non ergodic MC it should be:
             error_bound = \Sum_j (y_j * err +
                          x_ij * err * | phi_j | + err^2 * | phi_j |)
        Where \Sum_j ( (x_ij +- err)*(y_j +- err * | phi_j |) )
        is the way the probability is computed for the state i.
        x_ij  - the probability to reach BSCC_j from state i
        y_j   - the the total steady state probability of phi
                states in BSCC_j
        phi_j - the phi states in BSCC_j 
    
  • Imagine nested Until formulas, on every level there are computational errors. Now what if one one level due to such an error we include a wrong state / exclude a needed state, how does this affect the error bound of the formulas on the outer level?!


We should be able to set an error bound once and then to derive sub error bounds for sub formulas in such a way that the overall error remains the one the user wants. Right now the same error bound is just used everywhere.

Note: See TracTickets for help on using tickets.