Compositionality and bisimulation: A negative result
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.
- A calculus of communicating systems
- A logic for the description of non-deterministic programs and their properties
- An action-based framework for veryfying logical and behavioural properties of concurrent systems
- Characterizing finite Kripke structures in propositional temporal logic
- scientific article; zbMATH DE number 3919813 (Why is no real title available?)
- scientific article; zbMATH DE number 3936485 (Why is no real title available?)
- scientific article; zbMATH DE number 4119598 (Why is no real title available?)
- scientific article; zbMATH DE number 869193 (Why is no real title available?)
- Proof systems for satisfiability in Hennessy-Milner logic with recursion
- The temporal semantics of concurrent programs
- “Sometimes” and “not never” revisited
- Finitary logics for some CCS observational bisimulations
- \textsc{ULTraS} at work: compositionality metaresults for bisimulation and trace semantics
- Impossibility Results for the Equational Theory of Timed CCS
- scientific article; zbMATH DE number 4119603 (Why is no real title available?)
- On convergence-sensitive bisimulation and the embedding of CCS in timed CCS
- Towards automatic temporal logic verification of value passing process algebra using abstract interpretation
This page was built for publication: Compositionality and bisimulation: A negative result
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1182130)
