We study automatic methods for establishing P-validity (validity with probability 1) of simple temporal properties over finite-state probabilistic systems. The proposed approach replaces P-validity with validity over a non-probabilistic version of the system, in which probabilistic choices are replaced by non-deterministic choices constrained by compassion (strong fairness) requirements. ``Simple'' properties are temporal properties whose only temporal operators are ‹› (eventually) and its dual [] (always). In general, the appropriate compassion requirements are ``global,'' since they involve global states of the system. Yet, in many cases they can be transformed into ``local'' requirements, which enables their verification by model checkers. We demonstrate our methodology of translating the problem of P-validity into that of verification of a system with local compassion requirement on the ``courteous philosophers'' algorithm of [LR81], a parameterized probabilistic system that is notoriously difficult to verify, and outline a verification of the algorithm that was obtained by the TLV model checker.
Proc. 3rd workshop on Verification, Model Checking, and Abstract Interpretation
Gzipped Postscript
PDF