Symbolic algorithms to calculate steady-state probabilities of a finite state machine

Author

Hachtel, Gary D. ; Macii, Enrico ; Pardo, Abelardo ; Somenzi, Fabio

Author_Institution

Dept. of Electr. & Comput. Eng., Colorado Univ., Boulder, CO, USA

fYear

1994

fDate

28 Feb-3 Mar 1994

Firstpage

214

Lastpage

218

Abstract

In this paper we present two symbolic algorithms to compute the steady-state probabilities for very large finite state machines. These algorithms, based on Algebraic Decision Diagrams (ADD´s)-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 have implemented two solution techniques: one is based on the Gauss-Jacobi iteration, and the other one on simple matrix multiplication, we report the experimental results obtained for problems with over 10⁸ unknowns in irreducible form

Keywords

Markov processes; finite state machines; formal verification; iterative methods; matrix algebra; probabilistic logic; sequential circuits; Chapman-Kolmogorov equations; Gauss-Jacobi iteration; algebraic decision diagrams; finite state machine; finite state spaces; homogeneous discrete-parameter Markov chains; matrix multiplication; sequential circuit synthesis; steady-state probabilities; symbolic algorithms; terminal nodes; Automata; Boolean functions; Circuit synthesis; Data structures; Equations; Gaussian processes; Military computing; Probability; State-space methods; Steady-state;

fLanguage

English

Publisher

ieee

Conference_Titel

European Design and Test Conference, 1994. EDAC, The European Conference on Design Automation. ETC European Test Conference. EUROASIC, The European Event in ASIC Design, Proceedings.

Conference_Location

Paris

Print_ISBN

0-8186-5410-4

Type

conf

DOI

10.1109/EDTC.1994.326875

Filename

326875