Improving efficiency of implicit Markov chain state classification

Current efficient symbolic methods to classify the states of a Markov chain into transient and recurrent classes use an iterative approach, where each iteration begins by selecting a "seed" state. In this paper we present heuristics to reduce the number of iterations required. Our core contribution is the use of shortest distance information to select the seed state. Our approach uses multiway decision diagrams to represent sets of states and edge-valued decision diagrams to represent distance information. Experimental results indicate that the distance heuristics can be quite effective, often minimizing the required number of iterations.