Three-Valued Abstractions of Markov Chains: Completeness for a Sizeable Fragment of PCTL

Three-valued Markov chains and their PCTL semantics abstract - via probabilistic simulations - labeled Markov chains and their usual PCTL semantics. This abstraction framework is complete for a PCTL formula if all labeled Markov chains that satisfy said formula have a finite-state abstraction that satisfies it in its abstract semantics. We show that not all PCTL formulae are complete for this abstraction framework. But PCTL formulae whose path modalities occur in a suitable combination of negation polarity and threshold type are proved to be complete, were abstractions are bounded, 3-valued unfoldings of their concrete labeled Markov chains. This set of complete PCTL formulae subsumes widely used PCTL patterns.


PDF