Approximate Bisimulation: A Bridge Between Computer Science and Control Theory
Fifty years ago, control and computing were part of a broader system science. After a long period of separate development within each discipline, embedded and hybrid systems have challenged us to reunite the, now sophisticated theories of continuous control and discrete computing on a broader system theoretic basis. In this paper, we present a framework of system approximation that applies to both discrete and continuous systems. We deﬁne a hierarchy of approximation metrics between two systems that quantify the quality of the approximation, and capture the established notions in computer science as zero sections. The central notions in this framework are that of approximate simulation and bisimulation relations and their functional characterizations called simulation and bisimulation functions and deﬁned by Lyapunov-type inequalities. In particular, these functions can provide computable upper-bounds on the approximation metrics by solving a static game. Our approximation framework will be illustrated by showing some of its applications in various problems such as reachability analysis of continuous systems and hybrid systems, approximation of continuous and hybrid systems by discrete systems, hierarchical control design, and simulation-based approaches to veriﬁcation of continuous and hybrid systems.