Computation for supremal simulation-based controllable and strong observable subautomata

In our previous work, we proposed simulation-based controllability and simulation-based observability as properties of the specification to guarantee the existence of a bisimilarity supervisor. However, a given specification may not satisfy these conditions. Then, a natural question is how to compute a feasible sub-specification. To answer this question, this paper investigates the computation of supremal simulation-based controllable and strong observable subautomata by using lattice theory. First, three monotone operators-simulation operator, controllable operator and strong observable operator are constructed upon a complete lattice. Based on these operators, inequalities are then formulated, whose solution is a simulation-based controllable and strong observable set. In particular, a sufficient condition is presented to guarantee the existence of a supremal simulation-based controllable and strong observable subautomaton. When such an existence condition holds, an algorithm is further proposed to compute the supremal simulation-based controllable and strong observable automaton.