Abstractions of constrained linear systems

Simulation relations are powerful abstraction techniques in computer science that reduce the complexity of analysis and design of labeled transition systems. In this paper, we define and characterize simulation relations for discrete-time linear systems in the presence of state and input constraints. Given a discrete-time linear system and the associated constraints, we consider a control-abstract embedding into a transition system. We then establish necessary and sufficient conditions for one constrained linear system to simulate the transitions of the other. Checking the simulation conditions is formulated as a linear programming problem, which can be efficiently solved for systems of large dimensions. We provide an example where our approach is applied to the hybrid model of the electronic throttle control (ETC) system.