  Bisimulation relation has been successfully applied to computer science and
control theory. In our previous work, simulation-based controllability and
simulation-based observability are proposed, under which the existence of
bisimilarity supervisor is guaranteed. However, a given specification automaton
may not satisfy these conditions, and a natural question is how to compute a
maximum permissive subspecification. This paper aims to answer this question
and investigate the computation of the supremal simulation-based controllable
and strong observable subautomata with respect to given specifications by the
lattice theory. In order to achieve the supremal solution, three monotone
operators, namely simulation operator, controllable operator and strong
observable operator, are proposed upon the established complete lattice. Then,
inequalities based on these operators are formulated, whose solution is the
simulation-based controllable and strong observable set. In particular, a
sufficient condition is presented to guarantee the existence of the supremal
simulation-based controllable and strong observable subautomata. Furthermore,
an algorithm is proposed to compute such subautomata.
