Abstract
Abstract interpretation can be used to formalize the concept of parametricity in the concurrency field. The concrete domain is the proved transition system, whose transitions are labelled by encodings of the parallel structure of processes. Suitable relabelling functions of proved transitions allow us to retrieve many non interleaving models presented in the literature. We prove here that such relabelling functions are indeed abstraction functions in the sense of abstract interpretations, considering causality as a test-bed. They induce Galois connections between the concrete domain and the abstract semantic models. We prove that abstractions preserve non interleaving bisimulations.
Work partially supported by ESPRIT BRA n.8130 - LOMAPS.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
M. Boreale and D. Sangiorgi. A fully abstract semantics of causality in the π-calculus. In Proceedings of STACS'95, LNCS. Springer Verlag, 1995.
G. Boudol and I. Castellani. A non-interleaving semantics for CCS based on proved transitions. Fundamenta Informaticae, XI(4):433–452, 1988.
G. Boudol, I. Castellani, M. Hennessy, and A. Kiehn. A theory of processes with localities. Theoretical Computer Science, 114, 1993.
P. Cousot. Program analysis: the abstract interpretation perspective. ACM Computing Surveys, 28A(4), 1996.
P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511–547, 1992.
P. Cousot and R. Cousot. Inductive definitions, semantics and abstract interpretation. In Proceedings of POPL'92, pages 83–94, 1992.
P. Cousot and R. Cousot. Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages). In Proceedings of ICCL'9l, IEEE, pages 95–112, 1994.
R. Cridlig. Semantic analysis of concurrent ML by abstract model-checking. In B. Steffen, editor, Proceedings of the International Workshop on Verification of Infinite State Systems, Pisa, 1996.
Ph. Darondeau and P. Degano. Causal trees. In Proceedings of ICALP'89, LNCS 372, pages 234–248. Springer-Verlag, 1989.
P. Degano, R. De Nicola, and U. Montanari. Partial ordering derivations for CCS. In Proceedings of FCT, LNCS 199, pages 520–533. Springer-Verlag, 1985.
P. Degano, R. Gorrieri, and S. Vigna. On relating some models of concurrency. In Proceedings of TAPSOFT'93, LNCS 668, pages 15–30. Springer-Verlag, 1993.
P. Degano and C. Priami. Proved trees. In Proceedings of ICALP'92, LNCS 623, pages 629–640. Springer-Verlag, 1992.
P. Degano and C. Priami. Causality for mobile processes. In Proceedings of ICALP'95, LNCS 944, pages 660–671. Springer-Verlag, 1995.
A. Kiehn. Comparing causality and locality based equivalences. Acta Informatica, 31(8):697–718, 1994.
R. Milner. Communication and Concurrency. Prentice-Hall, London, 1989.
R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes (I and II). Information and Computation, 100(1):1–77, 1992.
C. Priami. Interleaving-based partial odering semantics. In Proceedings of Italian Conference on Theoretical Computer Science, pages 264–278, Ravello, November 1995, 1996. World Scientific.
G. Winskel and M. Nielsen. Models for concurrency. In Handbook of Logic in Computer Science. Oxford University Press, 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bodei, C., Priami, C. (1997). True concurrency via abstract interpretation. In: Van Hentenryck, P. (eds) Static Analysis. SAS 1997. Lecture Notes in Computer Science, vol 1302. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0032743
Download citation
DOI: https://doi.org/10.1007/BFb0032743
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63468-3
Online ISBN: 978-3-540-69576-9
eBook Packages: Springer Book Archive