Compositionality and bisimulation: A negative result (Q1182130)

We investigate the possibility of giving a temporal semantics to CCS. CCS (Calculus for Communicating Systems) describes the behaviour of processes by means of temporal ordering of events. On CCS terms different equivalence relations can be defined; among them the most commonly used is the bisimulation equivalence [\textit{R. Milner}, A calculus of communication systems. Lect. Notes in Comput. Sci. 92, Berlin etc.: Springer-Verlag (1980; Zbl 0452.68027)]. Our aim is to give the temporal semantics of CCS, fully abstract with respect to bisimulation equivalence, complying with the following requirements; (i) maintaining compositionality; (ii) using a ''standard'' temporal logic, such as the logic \(\hbox{CTL}^*\) [\textit{E. A. Emerson} and \textit{J. Halpern}, ''Sometime'' and ''Not never'' revisited: On branching versus linear time temporal logic, J. ACM 33, 151-178 (1986)]. By ''standard'' temporal logics we mean branching or linear temporal logics as defined usually in the literature, where no operator is added with the explicit purpose of expressing the behaviour of a process language construct. Actually, it turns out that our requirements are indeed too strong and do not allow us to express bisimulation equivalence. In order to show this we start from a subset of CCS -- called Regular CCS, with only the action prefixing, nondeterministic choice, and recursion -- providing for it a compositional branching temporal semantics which is proved fully abstract with respect to the bisimulation semantics. When we take into account Finite CCS (action prefixing, nondeterministic choice and parallel composition), we show that it is impossible to define a compositional temporal semantics, fully abstract with respect to the bisimulation equivalence, using \(\text{CTL}^*\) as the target logic.