Abstract
We propose a methodology for the analysis of open systems based on process calculi and bisimilarity. Open systems are seen as coordinators (i.e. terms with place-holders), that evolve when suitable components (i.e. closed terms) fill in their place-holders. The distinguishing feature of our approach is the definition of a symbolic operational semantics for coordinators that exploits spatial/modal formulae as labels of transitions and avoids the universal closure of coordinators w.r.t. all components. Two kinds of bisimilarities are then defined, called strict and large, which differ in the way formulae are compared. Strict bisimilarity implies large bisimilarity which, in turn, implies the one based on universal closure. Moreover, for process calculi in suitable formats, we show how the symbolic semantics can be defined constructively, using unification. Our approach is illustrated on a toy process calculus with CCS-like communication within ambients.
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
M. Abadi and M. P. Fiore. Computing symbolic models for verifying cryptographic protocols. In Proc. 14th IEEE Computer Security Foundations Workshop, pp. 160–173. IEEE, 2001.
R. Allen and D. Garlan. A Formal Basis for Architectural Connectors. ACM TOSEM, 6(3), pp. 213–249, 1997.
L. F. Andrade, J. L. Fiadeiro, J. Gouveia, G. Koutsoukos and M. Wermelinger. Coordination for Orchestration. In Coordination Models and Languages, 5th Int. Conference COORDINATION. Lect. Notes in Comput. Sci. 2315 pp. 5–13. Springer 2002.
F. Baader and W. Snyder. Unification theory. In Handbook of Automated Reasoning. Elsevier Science, 2000.
M. Boreale. Symbolic trace analysis of cryptographic protocols. In Proc. ICALP’01, Lect. Notes in Comput. Sci. 2076, pp. 667–681. Springer, 2001.
R. Bruni, D. de Frutos-Escrig, N. Martí-Oliet, and U. Montanari. Bisimilarity congruences for open terms and term graphs via tile logic. In Proc. CONCUR 2000, Lect. Notes in Comput. Sci. 1877, pp. 259–274. Springer, 2000.
R. Bruni, U. Montanari, and F. Rossi. An interactive semantics of logic programming. Theory and Practice of Logic Programming, 1(6):647–690, 2001.
L. Caires. A Model for Declarative Programming and Specification with Concurrency and Mobility. PhD thesis, Departamento de Informática, Universidade Nova de Lisboa, 1999.
L. Caires and L. Cardelli. A spatial logic for concurrency (part I). In Proc. TACS 2001, Lect. Notes in Comput. Sci. 2215, pp. 1–37. Springer, 2001.
L. Caires and L. Cardelli. A spatial logic for concurrency (part II). In Proc. CONCUR 2002. Lect. Notes in Comput. Sci., Springer, 2002. To appear.
L. Cardelli and A. D. Gordon. Anytime, anywhere. modal logics for mobile ambients. In Proc. POPL 2000, pp. 365–377. ACM, 2000.
L. Cardelli and A. D. Gordon. Mobile ambients. In Proc. FoSSaCS’98, Lect. Notes in Comput. Sci. 1378, pp. 140–155. Springer, 1998.
E. M. Clarke, S. Jha, and W. Marrero. Using state space exploration and a natural deduction style message derivation engine to verify security protocols. In Proc. PROCOMET’98. Chapmann & Hall, 1998.
R. De Simone. Higher level synchronizing devices in MEIJE-SCCS. TCS, 37:245–267, 1985.
J. L. Fiadeiro, T. Maibaum, N. Martí-Oliet, J. Meseguer, and I. Pita. Towards a verification logic for rewriting logic. In Proc. WADT’99, LNCS 1827, pp. 438–458. Springer, 2000.
F. Gadducci and U. Montanari. The tile model. In Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press, 2000.
M. Hennessy and H. Lin. Symbolic bisimulations. Theoret. Comp. Sci., 138:353–389, 1995.
A. Herold and J. Siekmann. Unification in abelian semi-groups. Journal of Automated Reasoning, 3(3):247–283, 1987.
K. G. Larsen and L. Xinxin. Compositionality through an operational semantics of contexts. In Proc. ICALP’90, Lect. Notes in Comput. Sci. 443, pp. 526–539. Springer, 1990.
J. J. Leifer and R. Milner. Deriving bisimulation congruences for reactive systems. In Proc. CONCUR 2000, Lect. Notes in Comput. Sci. 1877, pp. 243–258. Springer, 2000.
R. Milner. A Calculus of Communicating Systems, LNCS 92. Springer, 1980.
U. Montanari and V. Sassone. Dynamic congruence vs. progressing bisimulation for CCS. Fundamenta Informaticae, 16:171–196, 1992.
G. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Aarhus University, Computer Science Department, 1981.
A. Rensink. Bisimilarity of open terms. Inform. and Comput., 156(1–2):345–385, 2000.
P. Sewell. From rewrite rules to bisimulation congruences. In Proc. CONCUR’98, Lect. Notes in Comput. Sci. 1466, pp. 269–284. Springer, 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baldan, P., Bracciali, A., Bruni, R. (2002). Bisimulation by Unification* . In: Kirchner, H., Ringeissen, C. (eds) Algebraic Methodology and Software Technology. AMAST 2002. Lecture Notes in Computer Science, vol 2422. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45719-4_18
Download citation
DOI: https://doi.org/10.1007/3-540-45719-4_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44144-1
Online ISBN: 978-3-540-45719-0
eBook Packages: Springer Book Archive