Finitary logics for some CCS observational bisimulations (Q1198052)

This paper proves that observational bisimulations for CCS which satisfy certain conditions have a finitary associated modal logic. The conditions involve information on the amount of top-level parallelism of states. This result may add fuel to the interleaving-versus-true-concurrency debate, since it suggests that the ability to observe internal structure of states (which is what distinguishes noninterleaving semantics from interleaving semantics) can lead not only to semantics which are more expressive, but also to semantics which are in some way simpler - their associated modal logics are finitary. Some cases of the result (for instance, Strong Equivalence [\textit{R. Milner}, Communication and concurrency, Prentice Hall, New York (1989; Zbl 0683.68008)] and Pomset Bisimulation Equivalence [\textit{G. Boudal} and \textit{I. Castellani}, Theor. Comput. Sci. 59, No. 1/2, 25-84 (1988; Zbl 0678.68078)] were already known, due to Lemma 1, which was proved in [\textit{M. Hennessy} and \textit{R. Milner}, J. Assoc. Comput. Mach. 32, 137-161 (1985; Zbl 0629.68021)] and is generalized here.