A new approach to proving local cause bisimulation axiomatically

The local cause bisimulation is the behavior equivalence between processes enriched with local cause information. This paper proposes a full abstraction between observation theories of the local cause CCS and π-calculus. And based on the full abstraction, a new, alternative approach, which does not depend on auxiliary operators, to proving axiomatically the local cause bisimulation on finite processes of the local cause CCS is deduced. Although it is not possible to finitely axiomatize the local cause congruence without the help of extra operators.