Abstract
Proof systems for weak bisimulation congruences in the finite-control φ-calculus are presented and their completeness proved. This study consists of two major steps: first complete proof systems for guarded recursions arc obtained; then sound laws sufficient to remove any unguarded recursions are formulated. These results lift Milncr's axiomatisatiou for observation congruence in regular pure-CCS to the φ-calculus. The completeness proof relies on the symbolic bisimulation technique.
Cite
CITATION STYLE
Lin, H. (1998). Complete proof systems for observation congruences in finite-control φ-calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1443 LNCS, pp. 443–454). Springer Verlag. https://doi.org/10.1007/bfb0055074
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
