×

A rewriting strategy to verify observational congruence. (English) Zbl 0702.68074

Summary: We are concerned with the verification of behavioural equivalences for CCS specifications. We consider their axiomatic presentations thus relying on a term rewriting approach to verify the equivalence. In this framework it happens that, while some behavioural equivalences do admit a finit canonical term rewriting system, the completion of observational congruence diverges. We present a complete rewriting strategy for observational congruence that permits to reduce a finite CCS specification to normal form without attempting any completion.

MSC:

68Q42 Grammars and rewriting systems
68Q60 Specification and verification (program logics, model checking, etc.)
03D03 Thue and Post systems, etc.

Software:

REVE
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Bachmair, L.; Dershowitz, N., Completion for rewriting modulo a congruence, Theoret. Comput. Sci., 67, 173-201 (1989) · Zbl 0686.68021
[2] Bachmair, L.; Plaisted, D. A., Termination orderings for associative-commutative rewriting systems, J. Symbolic Comput., 1, 329-349 (1985) · Zbl 0587.68041
[3] De Nicola, R.; Inverardi, P.; Nesi, M., Using the axiomatic presentation of behavioural equivalences for manipulating CCS specifications, (Lecture Notes in Computer Science, 407 (1990), Springer: Springer Berlin), 54-67, Proc. Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, June 12-14, 1989
[4] Gnesi, S.; Inverardi, P.; Nesi, M., A logic-functional approach to the execution of CCS specifications modulo behavioural equivalences, (Concurrency 88, 335 (1988), Springer: Springer Berlin), 181-196, Lecture Notes in Computer Science · Zbl 0663.68040
[5] Hennessy, M.; Milner, R., Algebraic laws for nondeterminism and concurrency, J. ACM, 32, 1, 137-161 (1985) · Zbl 0629.68021
[6] Hermann, M., Crossed term rewriting systems, Res. Rept. 89-R-003 (1989), Centre de Recherche en Informatique de Nancy: Centre de Recherche en Informatique de Nancy Nancy
[7] Hermann, M., Lazy completion of term rewriting systems (1989), Centre de Recherche en Informatique de Nancy: Centre de Recherche en Informatique de Nancy Nancy, (draft)
[8] Huet, G.; Oppen, D. C., Equations and rewrite rules: A survey, (Book, R. V., Formal Language Theory: Perspectives and Open Problems (1980), Academic Press: Academic Press New York), 349-405
[9] Hullot, J. M., A catalogue of canonical term rewriting systems, Tech. Rept. CLS-113 (1980), SRI International: SRI International Menlo Park, CA
[10] Jouannaud, J. P.; Kirchner, H., Completion of a set of rules modulo a set of equations, SIAM J. Comput., 15, 4, 1155-1194 (1986) · Zbl 0665.03005
[11] Kirchner, H., Schematization of infinite sets of rewrite rules. Application to the divergence of completion processes, (Proc. RTA 87, 256 (1987), Springer: Springer Berlin), 80-191, Lecture Notes in Computer Science · Zbl 0657.68026
[12] Lescanne, P., Computer experiments with the REVE term rewriting system generator, Proc. 10th ACM POPL Symposium, 99-108 (1983), Austin, TX
[13] Milner, R., A Calculus of Communicating Systems, Lecture Notes in Computer Science, 92 (1980), Springer: Springer Berlin · Zbl 0452.68027
[14] Milner, R., Lectures on a calculus for communicating systems, (Control Flow and Data Flow: Concepts of Distributed Programming, 14 (1985), Springer: Springer Berlin), 205-228, NATO Advances Science Institutes Series F: Computer and Systems Sciences
[15] Peterson, G. E.; Stickel, M. E., Complete sets of reductions for some equational theories, J. ACM, 28, 2, 233-264 (1981) · Zbl 0479.68092
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.