Markovian Analysis of Large Finite State Machines

G. D. Hachtel and E. Macii and A. Pardo and F. Somenzi

IEEE Transactions on Computer-Aided Design, Vol. 15, Num. 12, Dec. 1996, pp. 1479-1493

Abstract

Regarding finite state machines as Markov chains facilitates the application of probabilistic methods to very large logic synthesis and formal verification problems. In this paper we present symbolic algorithms to compute the steady-state probabilities for very large finite state machines (up to 1027 states). These algorithms, based on Algebraic Decision Diagrams (ADDs) --- an extension of BDDs that allows arbitrary values to be associated with the terminal nodes of the diagrams --- determine the steady-state probabilities by regarding finite state machines as homogeneous, discrete-parameter Markov chains with finite state spaces, and by solving the corresponding Chapman-Kolmogorov equations. We first consider finite state machines with state graphs composed of a single terminal strongly connected component; for this type of systems we have implemented two solution techniques: One is based on the Gauss-Jacobi iteration, the other one is based on simple matrix multiplication. Then we extend our treatment to the most general case of systems which can be modeled as finite state machines with arbitrary transition structures; here our approach exploits structural information to decompose and simplify the state graph of the machine. We report experimental results obtained for problems on which traditional methods fail.

Click here to download the compressed postscript version.

BibTeX Entry

@Article{Hachte96,
  author =       {G. D. Hachtel and E. Macii and A. Pardo and F. Somenzi},
  title =        {Markovian Analysis of Large Finite State Machines},
  journal =      {{IEEE} Transactions on Computer-Aided Design},
  year =         1996,
  volume =       15,
  number =       12,
  month =        dec,
  pages =        {1479-1493}
}
Return to the home page