Finitary logics for some CCS observational bisimulations (Q1198052)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Finitary logics for some CCS observational bisimulations |
scientific article |
Statements
Finitary logics for some CCS observational bisimulations (English)
0 references
16 January 1993
0 references
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.
0 references
concurrences
0 references
formal semantics
0 references
finitary modal logic
0 references
observational bisimulations
0 references
CCS
0 references