Finite Uniform Bisimulations for Linear Systems with Finite Input Alphabets
For control theorists working on abstraction of linear systems with finite inputs, this provides theoretical foundations and computational methods for bisimulation-based verification.
The paper derives sufficient conditions for the existence of finite uniform bisimulations for discrete-time linear systems with finite input alphabets, and proposes algorithms to compute them when conditions are met.
We consider a class of systems over finite alphabets, namely discrete-time systems with linear dynamics and a finite input alphabet. We formulate a notion of finite uniform bisimulation, and motivate and propose a notion of regular finite uniform bisimulation. We derive sufficient conditions for the existence of finite uniform bisimulations, and propose and analyze algorithms to compute finite uniform bisimulations when the sufficient conditions are satisfied. We investigate the necessary conditions, and conclude with a set of illustrative examples.