On existence and construction of finite uniform bisimulations for linear systems with finite input alphabets

In this paper, we consider a class of discrete-time systems with linear dynamics and a finite input alphabet. We begin by motivating and proposing two notions of finite bisimulation that we refer to as `finite uniform bisimulation´, and `regular finite uniform bisimulation´. We derive a sufficient condition for the existence of finite uniform bisimulations, and we investigate necessary conditions. We also present an algorithm to compute finite uniform bisimulations when the sufficient condition is satisfied. We conclude with an illustrative example showing how to construct deterministic finite state machine models of the underlying system when these finite uniform bisimulations exist.