Approximate Bisimulations for Constrained Linear Systems

In this paper, inspired by exact notions of bi-simulation equivalence for discrete-event and continuous-time systems, we establish approximate bi-simulation equivalence for linear systems with internal but bounded disturbances. This is achieved by developing a theory of approximation for transition systems with observation metrics, which require that the distance between system observations is and remains arbitrarily close in the presence of nondeterministic evolution. Our notion of approximate bisimulation naturally reduces to exact bisimulation when the distance between the observations is zero. Approximate bisimulation relations are then characterized by a class of Lyapunov-like functions which are called bisimulation functions. For the class of linear systems with constrained disturbances, we obtain computable characterizations of bisimulation functions in terms of linear matrix inequalities, set inclusions, and optimal values of static games. We illustrate our framework in the context of safety verification.