Symbolic transition graph and its early bisimulation checking algorithms for the pi-calculus

Symbolic transition graph is proposed as an intuitive and compact semantic model for the pi-calculus processes. Various versions (strong/weak, ground/ symbolic) of early operational semantics are given to such graphs. Based on them the corresponding versions of early bisimulation equivalences and obs ervation congruence are defined. The notions of symbolic observation graph and symbolic congruence graph are also introduced, and followed by two theo rems ensuring the elimination of tau-cycles and tau-edges. Finally algorith ms for checking strong/weak early bisimulation equivalences and observation congruence are presented together with their correctness proofs. These res ults fuse and generalize the strong bisimulation checking algorithm for val ue-passing processes and the verification technique for weak bisimulation o f pure-CCS to the finite control pi-calculus.