Skip to main content
SpringerLink
Log in
Book cover

International Static Analysis Symposium

SAS 1998: Static Analysis pp 168–183Cite as

Constructing Specific SOS Semantics for Concurrency via Abstract Interpretation

Extended Abstract

  • Conference paper
  • First Online:

  • 357 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1503))

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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. L. Aceto. A static view of localities. Formal Aspects of Computing, 1992.

    Google Scholar 

  2. R.M. Amadio and S. Prasad. Localities and failures. In Proceedings of FST-TCS’94, pages 205–216. Springer-Verlag, 1994.

    Google Scholar 

  3. 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.

    Google Scholar 

  4. 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.

    Google Scholar 

  5. C. Bodei and C. Priami. True concurrency via abstract interpretation. In Proceedings of SAS’97, LNCS 1302, pages 202–216, 1997.

    Google Scholar 

  6. M. Boreale and D. Sangiorgi. A fully abstract semantics of causality in the π-calculus. In Proceedings of STACS’95, LNCS. Springer Verlag, 1995.

    Google Scholar 

  7. G. Boudol and I. Castellani. A non-interleaving semantics for CCS based on proved transitions. Fundamenta Informaticae, XI(4):433–452, 1988.

    MathSciNet  Google Scholar 

  8. G. Boudol, I. Castellani, M. Hennessy, and A. Kiehn. A theory of processes with localities. Theoretical Computer Science, 114, 1993.

    Google Scholar 

  9. P. Buchholz. On a markovian process algebra. Technical report, Informatik IV, University of Dortmund, 1994.

    Google Scholar 

  10. P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511–547, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  11. P. Cousot and R. Cousot. Inductive definitions, semantics and abstract interpretation. In Proceedings of POPL’92, pages 83–94, 1992.

    Google Scholar 

  12. 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.

    Google Scholar 

  13. 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.

    Google Scholar 

  14. Ph. Darondeau and P. Degano. Causal trees. In Proceedings of ICALP’89, LNCS 372, pages 234–248. Springer-Verlag, 1989.

    Google Scholar 

  15. 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.

    Google Scholar 

  16. 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.

    Google Scholar 

  17. P. Degano and C. Priami. Proved trees. In Proceedings of ICALP’92, LNCS 623, pages 629–640. Springer-Verlag, 1992.

    Google Scholar 

  18. 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.

    Google Scholar 

  19. R. Gorrieri, M. Roccetti, and E. Stancapiano. A theory of processes with durational actions. Theoretical Computer Science, (140), 1994.

    Google Scholar 

  20. 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.

    Google Scholar 

  21. E. Goubault. Durations for truly concurrent transitions. In Proceedings of ESOP96, LNCS 1058, pages 173–187, 1995.

    Google Scholar 

  22. M. Hennessy and T. Regan. A temporal process algebra. Technical Report 2/90, University of Sussex, 1990.

    Google Scholar 

  23. J. Hillston. The nature of synchronization. In U. Herzog and M. Rettelbach, editors, Proceedings of PAPM’94, University of Erlangen, 1994.

    Google Scholar 

  24. A. Kiehn. Comparing causality and locality based equivalences. Acta Informatica, 31(8):697–718, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  25. K.G. Larsen and A. Skou. Compositional verification of probabilistic processes. In Proceedings of CONCUR’92, volume 630 of LNCS. Springer-Verlag, 1992.

    Google Scholar 

  26. R. Milner. Communication and Concurrency. Prentice-Hall, London, 1989.

    MATH  Google Scholar 

  27. R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes (I and II). Information and Computation, 100(1):1–77, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  28. U. Montanari and M. Pistore. Concurrent semantics for the π-calculus. In Electronic Notes in Computer Science, number 1. Elsevier, 1995.

    Google Scholar 

  29. U. Montanari and D. Yankelevich. A parametric approach to localities. In Proceedings of ICALP’92, LNCS 623, pages 617–628. Springer-Verlag, 1992.

    Google Scholar 

  30. 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.

    Chapter  Google Scholar 

  31. C. Priami. Stochastic π-calculus. The Computer Journal, 38(6):578–589, 1995.

    Article  Google Scholar 

  32. C. Priami. Enhanced Operational Semantics for Concurrency. PhD thesis, Dipartimento di Informatica, Università di Pisa, March 1996. Available as Tech. Rep. TD-08/96.

    Google Scholar 

  33. 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.

    Google Scholar 

  34. 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.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Informatica, Università di Pisa, Corso Italia 40, I-56100, Pisa, Italy

    Chiara Bodei & Pierpaolo Degano

  2. Istituto Policattedra, Università di Verona, Ca’ Vignal 2, Strada Le Grazie 1, I-37134, Verona, Italy

    Corrado Priami

Authors
  1. Chiara Bodei
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pierpaolo Degano
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Corrado Priami
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Università di Pisa, Corso Italia, 40, I-56125, Pisa, Italy

    Giorgio Levi

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation