  In this paper, we consider the problem of constructing a finite bisimulation
quotient for a discrete-time switched linear system in a bounded subset of its
state space. Given a set of observations over polytopic subsets of the state
space and a switched linear system with stable subsystems, the proposed
algorithm generates the bisimulation quotient in a finite number of steps with
the aid of sublevel sets of a polyhedral Lyapunov function. Starting from a
sublevel set that includes the origin in its interior, the proposed algorithm
iteratively constructs the bisimulation quotient for any larger sublevel set.
The bisimulation quotient can then be further used for synthesis of the
switching law and system verification with respect to specifications given as
syntactically co-safe Linear Temporal Logic formulas over the observed
polytopic subsets.
