Employing AI Techniques in Probabilistic Model Checking

Probabilistic model-checking (PMC) is a new frontier in model checking verification, useful for checking randomized algorithms, communications protocols with random components, etc. AI techniques have been incorporated into conventional model-checking, with great success. We wish to see if corresponding successes can be found by applying AI techniques to PMC. In this position paper, we introduce PMC. We present the probabilistic automata and probabilistic bounded LTL used in modeling for PMC. We also introduce some existing tools for PMC. With this background in place, we dis- cuss challenges and opportunities for incorporating AI techniques in PMC, and our current work in the area.