Oxford logo
[HK98] M. Huth and M. Kwiatkowska. Comparing CTL and PCTL on Labeled Markov Chains. In Proc. Programming Concepts and Methods (PROCOMET'98), IFIP, Chapman & Hall. February 1998. [ps.gz] [bib]
Downloads:  ps.gz ps.gz (110 KB)  bib bib
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.