Controller/Orchestrator Synthesis via Filtration

The present paper is interested in the following decision problems: (1) given finite frames F, F′, determine if there exists a frame F″ such that F and F′⊗F″, the synchronous product of F′ and F″, are bisimilar; (2) given finite frames F, F′, determine if there exists a frame F″ such that F and F′⊕F″, the asynchronous product of F′ and F″, are bisimilar. It shows that variants of the filtration method are adequate for solving them.