  This paper presents a compositional framework for the construction of
symbolic models for a network composed of a countably infinite number of
finite-dimensional discrete-time control subsystems. We refer to such a network
as infinite network. The proposed approach is based on the notion of
alternating simulation functions. This notion relates a concrete network to its
symbolic model with guaranteed mismatch bounds between their output behaviors.
We propose a compositional approach to construct a symbolic model for an
infinite network, together with an alternating simulation function, by
composing symbolic models and alternating simulation functions constructed for
subsystems. Assuming that each subsystem is incrementally input-to-state stable
and under some small-gain type conditions, we present an algorithm for orderly
constructing local symbolic models with properly designed quantization
parameters. In this way, the proposed compositional approach can provide us a
guideline for constructing an overall symbolic model with any desired
approximation accuracy. A compositional controller synthesis scheme is also
provided to enforce safety properties on the infinite network in a
decentralized fashion. The effectiveness of our result is illustrated through a
road traffic network consisting of infinitely many road cells.
