Factorisation of finite state machines under strong and observational equivalences
Huajun Qin, Philip Lewis · Formal Aspects of Computing · 1991
Abstract The factorisation problem is to construct the specification of a submoduleXwhen the specifications of the system and all submodules butXare given. It is usually described by the equation where P and X are submodules of system Q, ¦ is a composition operator, and is the equivalence criterion. In this paper we use a finite state machine (FSM) model consistent with CCS and study two factorisation problems:P|||P∼QandP|||P≈Q, where ||| is a derived CCS composition operator, ∼ and ≈ represent strong and observational equivalences. Algorithms are presented and proved correct to find the most general specification of submoduleXforP|||P∼QwithQτ-deterministic and forP|||P≈QwithQdeterministic. Conditions on the submachines of the most general solutions that remain solutions toP|||P∼Q(P|||P≈Q) are given. This paper extends and is based on the work of M. W. Shields.