Contextual transition system for π-calculus

This paper presents a labeled transition system (LTS) for π-calculus that uses contexts of processes rather than actions as labels for transitions. We present a set of rules that derives transitions with contextual labels. We show that the operational semantics defined with the LTS corresponds to the semantics defined with reaction rules. The set of rules does not refer the rules for reaction semantics explicitly unlike existing contextual LTS. The LTS is a base for a structural operational semantics with contextual labels. We present that the bisimulation equivalence based on the contextual LTS is a congruence relation.