Probabilistic Analysis of Large Finite State Machines

Regarding nite state machines as Markov chains facilitates the application of probabilistic methods to very large logic synthesis and formal verication problems. Recently, we have shown how symbolic algorithms based on Algebraic Decision Diagrams may be used to calculate the steadystate probabilities of nite state machines with more than 108 states. These algorithms treated machines with state graphs composed of a single terminal strongly connected component. In this paper we consider the most general case of systems which can be modeled as state machines with arbitrary transition structures. The proposed approach exploits structural information to decompose and simplify the state graph of the machine.

• Type: Conference
• Year: 1994
• Where: DAC
• Authors: Gary D. Hachtel, Enrico Macii, Abelardo Pardo, Fabio Somenzi
• Keywords: Computer Architecture, DAC 1994, Formal Veri Cation, Nite State Machines, State Graph