Abstract
Preorders are often used as a semantic tool in various fields of computer science. Examples in this direction are the preorder semantics defined for process algebra formalisms, such as testing preorders and bisimulation preorders. Preorders turn out to be useful when modelling divergence or partial specification. In this paper we present some results on the possibility of associating to a preorder theory, presented via a set of equality axioms and ordering ones, an equivalent rewriting relation which, together with a proof strategy, allows the decidability of the preorder relation. Our approach has been developed in the framework of a project whose main goal is to develop a verification system for process algebra formalisms based on equational reasoning.
Work partially supported by “PF Sistemi Informatici e Calcolo Parallelo” of CNR
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Aceto L., Hennessy M. ‘Termination, Deadlock and Divergence', Journal of ACM, Jan. 1992.
Bachmair, L., Dershowitz, N. 'Commutation, Transformation, and Termination’ in Proceedings of the 8th CADE, LNCS 230, (1986), 52–60.
Bachmair, L., Dershowitz, N. ‘Completion for Rewriting modulo a Congruence', in Theoretical Computer Science, North-Holland, (1989), 67, 173–201.
Bachmair, L., Ganzinger, H. ‘Ordering Chaining for Total Orderings’ in Proceedings of the 12th CADE, LNCS 814, (1994).
Bergstra, J.A., Klop, J.W. ‘Process Algebra for Synchronous Communication', in Information and Control, 60, No. 1/3, (1984), 109–137.
Camilleri, A., Inverardi, P., Nesi, M. ‘Combining Interaction and Automation in Process Algebra Verification', LNCS 494, Springer-Verlag, (1991).
De Nicola, R., Hennessy, M. ‘Testing Equivalences for Processes', in Theoretical Computer Science, North-Holland, 34, (1984), 83–133.
De Nicola, R., Inverardi, P., Nesi, M. 'Using the Axiomatic Presentation of Behavioural Equivalences for Manipulating CCS Specifications', in Proc. Workshop on Automatic Verification Methods for Finite State Systems, LNCS 407, (1990), 54–67.
Dershowitz N., Jouannaud J.-P., ‘Rewrite Systems', in Handbook of Theo. Computer Science, Vol. B: Formal Models and Semantics, J. van Leeuwen (ed.), North-Holland, 1990, pp. 243–320.
Hoare, C.A.R. ‘Communicating Sequential Processes', Prentice Hall Int., London, (1985).
Huet, G., ‘Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems', in Journal of ACM, Vol. 27, n. 4, Oct. 1980, pp.797–821.
Hussmann, H. ‘Nondeterministic Algebraic Specifications', PhD Thesis, University of Passau, English Literal Translation as TUM-19104, March 1991.
Inverardi P., Leggio, T., ‘Rewriting Preorders', I.E.I. IR B4-3 January, 1993.
Inverardi, P., Nesi, M., ‘A Rewriting Strategy to Verify Observational Congruence', Information Processing Letters, 1990, Vol. 35, pp. 191–199.
Inverardi, P., Nesi, M. ‘Deciding Observational Congruence of Finite-State CCS Expressions by Rewriting', I.E.I. IR n B4-10, (revised 1993), to appear in Theoretical Computer Science, North-Holland, (1995).
Jouannaud, J.P., Kirchner, H. ‘Completion of a Set of Rules modulo a Set of Equations’ in, SIAM J. Comput., Vol.15, No.4, (1986), 1155–1194.
Klop J.W., de Vrijer R.C., ‘Term Rewriting Systems', Cambridge University Press, forthcoming.
Levy, J., Augusti', J. ‘Bi-rewriting, a Term Rewriting Technique for Monotonic Order Relations’ in Proceedings of the 5th RTA, LNCS 690, (1993).
Leggio, T. ‘Riscrittura di preordini' Tesi di Laurea in Scienze dell'Informazione, Universita’ di Pisa, February 1992.
Meseguer, J. ‘Conditioned Rewriting Logic as a Unified Model of Concurrency', in Theoretical Computer Science Vol. 96, N. 1, 1992, North-Holland.
Milner, R. ‘Communication and Concurrency', Prentice Hall, (1989).
Peterson, G.E., Stickel, M.E. ‘Complete Sets of Reductions for Some Equational Theories', in Journal of ACM, Vol.28, No.2, (1981), 233–264.
D.J.Walker. ‘Bisimulation and Divergence', in Information and Computation 85, (1990), 202–242.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Inverardi, P. (1995). Rewriting for preorder relations. In: Dershowitz, N., Lindenstrauss, N. (eds) Conditional and Typed Rewriting Systems. CTRS 1994. Lecture Notes in Computer Science, vol 968. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60381-6_13
Download citation
DOI: https://doi.org/10.1007/3-540-60381-6_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60381-8
Online ISBN: 978-3-540-45513-4
eBook Packages: Springer Book Archive