A method to bound stationary distributions of large Markov chains resulting
from networks of stochastic automata is presented. It combines the concepts
for bounding the stationary distribution using eigenvector polyhedra with
the exploitation of the specific structure of Markov chains resulting from
stochastic automata networks. The quality of the bounds depends on the
coupling between automata. Three consecutive steps of the method are
presented. In the first step bounds are computed using information about
single automata in isolation. Bounds for single automata are refined in a
second step by considering the environment of an automaton given by the
other automata in the network. In a third step, bounds are further improved
using a disaggregation step. By means of two small examples it is shown
that the method yields tight bounds for loosely coupled automata and that
the approach is extremely efficient compared to other bounding methods, let
alone compared to an exact numerical analysis.