Abstract
Most of the SOS semantics for concurrent systems can be derived by abstracting on the inference rules of a concrete transition system, namely the proved transition system. Besides the standard interleaving semantics we mechanically derive the causal transition system for CCS, whose definition is particularly dificult and paradigmatic. Its rules are shown to coincide with those presented in the literature. Also, the tree of its computations coincide with that obtained by abstracting the computations of the proved transition system.
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
L. Aceto. A static view of localities. Formal Aspects of Computing, 1992.
R.M. Amadio and S. Prasad. Localities and failures. In Proceedings of FST-TCS’94, pages 205–216. Springer-Verlag, 1994.
M. Bernardo, L. Donatiello, and R. Gorrieri. Integrating performance and functional analysis of concurrent systems with EMPA. Technical Report UBLCS-95-14, University of Bologna, Laboratory for Computer Science, 1995.
C. Bodei, P. Degano, and C. Priami. Mobile processes with a distributed environment. In Proceedings of ICALP’96, LNCS 1099, pages 490–501. Springer-Verlag, 1996. To appear in TCS.
C. Bodei and C. Priami. True concurrency via abstract interpretation. In Proceedings of SAS’97, LNCS 1302, pages 202–216, 1997.
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. Buchholz. On a markovian process algebra. Technical report, Informatik IV, University of Dortmund, 1994.
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 Procs. ICCL’94, IEEE, pages 95–112, 1994.
P. Cousot and R. Cousot. Compositional and inductive semantic definitions in fixpoint equational, constraint, closure-condition, rule-based and game-theoretic form. In Proceedings of CAV’95, LNCS 939, pages 293–308, 1995.
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, J.-V. Loddo, and C. Priami. Mobile processes with local clocks. In Proceedings of Workshop on Analysis and Verification of Multiple-Agent Languages, Stockholm, Sweden, 1996.
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. Non interleaving semantics for mobile processes. Extended abstract. In Proceedings of ICALP’95, LNCS 944, pages 660–671. Springer-Verlag, 1995. To appear in TCS.
R. Gorrieri, M. Roccetti, and E. Stancapiano. A theory of processes with durational actions. Theoretical Computer Science, (140), 1994.
N. Götz, U. Herzog, and M. Rettelbach. TIPP-a language for timed processes and performance evaluation. Technical Report 4/92, IMMD VII, University of Erlangen-Nurnberg, 1992.
E. Goubault. Durations for truly concurrent transitions. In Proceedings of ESOP96, LNCS 1058, pages 173–187, 1995.
M. Hennessy and T. Regan. A temporal process algebra. Technical Report 2/90, University of Sussex, 1990.
J. Hillston. The nature of synchronization. In U. Herzog and M. Rettelbach, editors, Proceedings of PAPM’94, University of Erlangen, 1994.
A. Kiehn. Comparing causality and locality based equivalences. Acta Informatica, 31(8):697–718, 1994.
K.G. Larsen and A. Skou. Compositional verification of probabilistic processes. In Proceedings of CONCUR’92, volume 630 of LNCS. Springer-Verlag, 1992.
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.
U. Montanari and M. Pistore. Concurrent semantics for the π-calculus. In Electronic Notes in Computer Science, number 1. Elsevier, 1995.
U. Montanari and D. Yankelevich. A parametric approach to localities. In Proceedings of ICALP’92, LNCS 623, pages 617–628. Springer-Verlag, 1992.
X. Nicollin and J. Sifakis. An overview and synthesis on timed process algebras. In Real Time: Theory in Practice, LNCS 600, pages 526–548. Springer-Verlag, 1991.
C. Priami. Stochastic π-calculus. The Computer Journal, 38(6):578–589, 1995.
C. Priami. Enhanced Operational Semantics for Concurrency. PhD thesis, Dipartimento di Informatica, Università di Pisa, March 1996. Available as Tech. Rep. TD-08/96.
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.
R.J. van Glabbeek, S.A. Smolka, B. Steffen, and C.M.N. Tofts. Reactive, generative and stratified models of probabilistic processes. Information and Computation, 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bodei, C., Degano, P., Priami, C. (1998). Constructing Specific SOS Semantics for Concurrency via Abstract Interpretation. In: Levi, G. (eds) Static Analysis. SAS 1998. Lecture Notes in Computer Science, vol 1503. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49727-7_10
Download citation
DOI: https://doi.org/10.1007/3-540-49727-7_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65014-0
Online ISBN: 978-3-540-49727-1
eBook Packages: Springer Book Archive