Computation for Supremal Simulation-Based Controllable Subautomata

Bisimulation relation as a well known equivalence relation has been successfully applied to computer science and control theory. In our previous work, we proposed the existence of bisimilarity supervisor by introducing simulation-based controllability. As a continuation, this paper deals with the computation for the supremal simulation-based controllable subautomata with respect to given specifications by lattice theory. In order to achieve the supremal solution, two monotone operators, namely simulation operator and controllable operator, are built upon the established complete lattice, and then we set up the inequalities, whose solutions are simulation-based controllable state pairs. In particular, a sufficient condition is provided to guarantee the existence of supremal simulation-based controllable subautomata. Furthermore, an algorithm is presented for the computation of such subautomata.