A modal characterization of observational congruence on finite terms of CCS

We propose a translation method of finite terms of CCS into formulas of a modal language representing their class of observational congruence. For this purpose, we define a modal language and a function associating with any finite term of CCS a formula of the language, satisfied by the term. Furthermore, this function is such that two terms are congruent if and only if the corresponding formulas are equivalent. The translation method consists in associating with operations on terms (action, +) operations on the corresponding formulas. This work is a first step towards the definition of a modal language with modalities expressing both possibility and inevitability and which is compatible with observational congruence