Controller/Orchestrator Synthesis via Filtration
Philippe Balbiani, Fahima Cheikh, Guillaume Feuillade · Electronic Notes in Theoretical Computer Science · 2010
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.