Abstract.
We interpret modal muÂcalculus formulas in a nonÂstandard way as expectations over labeled Markov chains. In this semantics fixedÂpoints are computed in an iterative incremental/decremental fashion. This provides the foundation for a symbolic model checking algorithm for CTL over labeled Markov chains using MultiÂTerminal Binary Decision Diagrams, where expectations of untilÂformulas are calculated via suitable fixedÂpoint approximations. We compare this nonÂstandard semantics of CTL to the standard one for the probabilis tic logic PCTL by specifying a translation phi -> phib of the positive existential fragment CTL+ of CTL into PCTL, where PCTL probability thresholds are supplied by the nonÂstandard semantics. Finally, we show soundness of our nonÂstandard semantics of CTL+ with respect to the one for PCTL in the following sense: if our semantics computes a positive evidence for phi at state s then s satisfies the translated PCTL formula phib.
|