A small model theorem for bisimilarity control under partial observation

In our prior work on control under complete observation of a nondeterministic system to satisfy bisimilarity with a nondeterministic specification by C. Zhou et al. (2004), we established a "small model theorem" showing that a control-compatible (Σ_u-compatible for short) supervisor exists if and only if it exists over a certain finite state space, namely the power set of Cartesian product of system and specification state spaces. In this paper, we show that the small model theorem remains valid even when there is partial observation of events so that a supervisor must be both control and observation compatible ((Σ_u, M)-compatible for short). The result proves the decidability of bisimilarity enforcing control under partial observation for general nondeterministic systems and nondeterministic specification.