The expressive power of implicit specifications (Q685409)

We investigate the expressive power of implicit specifications of concurrent systems. That is, we consider specifications \(S\) specifying a system \(P\) not directly, but rather in combination with a given environment. Formally, we shall represent the environment as a \(CCS\) context of the form \((A\mid[\;][\Phi])\setminus L\), where \(A\) is a process expression and \(\mid\), \(\setminus L\) and \([\Phi]\) are the parallel, restriction and renaming operators of \(CCS\), respectively. We investigate the expressive power of the following three types of implicit specifications: (i) \((A\mid P[\Phi])\setminus L\sim B\), where \(\sim\) is strong bisimulation equivalence and \(B\) is a process expression; (ii) \((A\mid P[\Phi])\setminus L\triangleleft S\), where \(S\) is a modal specification and \(\triangleleft\) is refinement between modal specifications (a generalization of bisimulation equivalence); and (iii) \((A\mid P[\Phi])\setminus L\models F\), where \(F\) is a formula of Hennessy-Milner logic extended with a (maximal) recursion construct. The paper offers the following two main results. When \(A\),\(B\) and \(S\) are recursion-free and \(F\) is a Hennessy-Milner logic formula, the expressive powers of all three types of implicit specifications are the same and equal that of Hennessy-Milner logic. When \(A\) and \(S\) are regular, the expressive powers of implicit specifications of type (ii) and (iii) are the same and identical to that of Hennessy-Milner logic extended with (maximal) recursion. Finally, we recall from \textit{K. G. Larsen} and \textit{L. Xinxin} [Lect. Notes Comput. Sci. 443, 526-539 (1990; Zbl 0765.68107)] that the expressive power of implicit specifications does not increase by modelling the environment as other contexts (of CCS or other process calculi).