A bisimulation-like algorithm for abstracting control systems A. Wagenmaker and N. Ozay Motivated by the recent interest in abstraction-based correct-by-construction control synthesis, in this paper we propose a new algorithm to construct finite abstractions for “large”, possibly infinite, transition systems. As opposed to the standard bisimulation algorithms that create a partition of the state space, the new algorithm uses overlapping subsets of the state space as the states of the abstraction. We show that the output of the new bisimulation-like algorithm preserves realizability of linear-time properties. Several interesting properties of the algorithm are analyzed. In particular, when a finite bisimulation of the original system exists, the new algorithm is shown to always terminate in a finite number of steps. Moreover, we show with an example that even when the original system does not have a finite bisimulation, the new algorithm can result in a finite transition system whose infinite traces are equivalent to those of the original system. In the second part of the paper, we focus on the application of this algorithm to construct finite abstractions for discrete-time linear control systems and discuss several of its advantages over the standard bisimulation algorithm. Finally, the new algorithm is compared to the existing algorithms with some numerical examples. |