Abstract
We consider the compatibility checking problem for a simple fragment of CCS, called BCCSP[12], using equational unification techniques. Two high-level specifications given as two process algebraic terms with free variables are said to be compatible modulo some equivalence relation if a substitution on the free variables can make the resulting terms equivalent modulo that relation. We formulate this compatibility (modulo an equivalence relation) checking problems as unification problems in the equational theory of the the corresponding equivalence relation. We use van Glabbeek's equational axiomatizations [12] for some interesting process algebraic relations. Specifically, we consider equational axiomatizations for bisimulation equivalence and trace equivalence and establish complexity lower bounds and upper bounds for the corresponding unification and matching problems. We also show some special cases for which efficient algorithmic solutions exist.
P. Narendran was supported in part by the NSF grant CCR-9404930 and S. Shukla was partially supported by the NSF grant CCR-94-06611.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
A. Aiken and D. Kozen and M. Vardi and E. Wimmers. The Complexity of Set Constraints. Proceedings of Computer Science Logic, (E. Börger, Y. Gurevich and K. Meinke, eds.) 1993, 1–17.
F. Baader and K.U. Schulz. Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures. J. of Symbolic Computation, 21:211–243, 1996.
J.C.M. Baeten and W.P. Weijland. Process Algebra. Cambridge Tracts in Theoretical Computer Science, Vol. 18, Cambridge University Press, Cambridge, England.
J. Doner. Tree acceptors and some of their applications. Journal of Computer and System Sciences 4(3):406–451, 1970.
W. Dowling and J. Gallier. Linear-time algorithms for testing the satisfiability of propositional Horn formulae. Journal of Logic Programming, 1(3):267–284, 1984.
Q. Guo. Nilpotence, Bisimulation and the Unification Workbench. PhD thesis, State University of New York at Albany, 1997.
M. Hennessy. Algebraic Theory of Processes. Foundations of Computing Series, The MIT Press, 1988.
R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989. SU Fisher Research 511/24.
P. Narendran. Unification modulo ACI + 1 + 0. Fundamenta Informaticae 25 (1):49–57, 1996.
M.O. Rabin. Weakly definable relations and special automata. In: Mathematical Logic and Foundations of Set Theory (Y. Bar-Hillel, ed.), North-Holland, 1970, 1–23.
W. Thomas. Automata on infinite objects. Handbook of Theoretical Computer Science (J. van Leeuwen, ed.), Elsevier Science Publishers, 1990, 133–191.
R.J. van Glabbeek. The linear time—branching time spectrum. Technical Report CS-R9029, Computer Science Department, CWI, Centre for Mathematics and Computer Science, Netherlands, 1990.
R.J. van Glabbeek and Peter Weijland. Branching Time and Abstraction in Bisimulation Semantics. Journal of the ACM 43 (3), May 1996, 555–600.
Author information
Authors and Affiliations
Corresponding authors
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag
About this paper
Cite this paper
Guo, Q., Narendran, P., Shukla, S.K. (1998). Unification and matching in process algebras. In: Nipkow, T. (eds) Rewriting Techniques and Applications. RTA 1998. Lecture Notes in Computer Science, vol 1379. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0052363
Download citation
DOI: https://doi.org/10.1007/BFb0052363
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64301-2
Online ISBN: 978-3-540-69721-3
eBook Packages: Springer Book Archive