Approximate equivalence and synchronization of metric transition systems

In this paper, we consider metric transition systems which are transition systems equipped with metrics for observation and synchronization labels. The existence of metrics leads to the introduction of two new concepts, (i) approximate (bi)simulation of transition systems and (ii) approximate synchronization of transition systems. We show that the notion of approximate (bi)simulation can be thought of as a generalization or relaxation of the earlier work by Girard and Pappas. We demonstrate the link between reachability verification and approximate (bi)simulation, and we also provide a characterization of (bi)simulation relations using a tool similar to the (bi)simulation function. Approximate synchronization can be thought of as a generalization of synchronization of transition systems in the usual sense. In fact, the usual synchronization and interleaving synchronization are two special cases of the notion of approximate synchronization developed in this paper. Furthermore, we present a result on the compositional properties of the approximate (bi)simulation with respect to the approximate synchronization. In addition to the theoretical presentation of approximate bisimulation and synchronization, we also discuss the application of this framework in analyzing control systems over digital communication networks.