Skip to main content

A complete proof system for SCCS with modal assertions

Extended abstract

  • Conference paper
  • First Online:
Foundations of Software Technology and Theoretical Computer Science (FSTTCS 1985)

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

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

Access this chapter

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Aczel, P., An introduction to inductive definitions. In the handbook of Mathematical Logic, Ed. Barwise, J., North-Holland (1983).

    Google Scholar 

  2. Brookes, S. D., On the axiomatic treatment of concurrency. In the proceedings of the joint US-UK seminar on the semantics of concurrency, July 1984, Carnegie-Mellon University, Pittsburgh, Springer-Verlag Lecture Notes in Comp. Sc. 197 (1984).

    Google Scholar 

  3. Barringer H., Kuiper R. and Pnueli A., Now you may compose temporal logic specifications. In the proceedings of STOC 84 (1984).

    Google Scholar 

  4. de Nicola, R. and Hennessy, M.C.B., Testing Equivalences for Processes, Lecture Notes in Comp. Sc. vol. 154 (1983) and in Theoretical Computer Science (1984).

    Google Scholar 

  5. Golson, W.G., Denotational models based on synchronously communicating processes: refusal, acceptance, safety. In the proceedings of the joint US-UK seminar on the semantics of concurrency, July 1984, Carnegie-Mellon University, Pittsburgh, Springer-Verlag Lecture Notes in Comp. Sc. 197 (1984).

    Google Scholar 

  6. Graf, S., and Sifakis, J., A logic for the specification and proof of controllable processes of CCS. Advanced Seminar on logics and models for verification and specification of concurrent systems, La Colle-sur-Loup, France, to appear in Springer-Verlag Lecture Notes in Comp. Sc. (1984).

    Google Scholar 

  7. Hoare, C.A.R., A model for communicating sequential processes. Monograph of the Programming Research Group, Oxford University (1981).

    Google Scholar 

  8. Hoare, C.A.R., Brookes, S.D., and Roscoe, A.W., A Theory of Communicating Processes, Technical Report PRG-16, Programming Research Group, University of Oxford (1981); appears also in JACM (1984).

    Google Scholar 

  9. Hennessy, M.C.B. and Milner, R., On observing nondeterminism and concurrency, Springer LNCS Vol. 85. (1979).

    Google Scholar 

  10. Hennessy, M.C.B. and Plotkin, G.D., A term model for CCS. Springer Lecture Notes in Comp. Sc., vol. 88 (1980).

    Google Scholar 

  11. Larsen, K. and Winskel, G., Using Information Systems to solve Recursive Domain Equations Effectively. Springer Lecture Notes in Comp. Sc., vol. 173 (1984). A full version appears as report No 51 of the Computer Laboratory, University of Cambridge.

    Google Scholar 

  12. Milner, R., A Calculus of Communicating Systems. Springer Lecture Notes in Comp. Sc. vol. 92 (1980).

    Google Scholar 

  13. Milner, R., A modal characterisation of observable machine-behaviour. Springer Lecture Notes in Comp. Sc. vol. 112 (1981).

    Google Scholar 

  14. Milner, R., Calculi for synchrony and asynchrony, Theoretical Computer Science, pp.267–310 (1983).

    Google Scholar 

  15. Olderog, E., and Hoare, C.A.R., Specification-oriented semantics for communicating processes. ICALP 83, Springer Lecture Notes in Comp. Sc. vol. 154 (1983).

    Google Scholar 

  16. Plotkin, G. D., Some comments on Robin's “A modal characterisation of observable machine-behaviour”. Handwritten notes, Comp. Sc. Dept., University of Edinburgh (1983).

    Google Scholar 

  17. Park, D., Concurrency and automata on infinite sequences. Springer Lecture Notes in Comp. Sc. vol. 104 (1981).

    Google Scholar 

  18. Scott, D. S., Domains for Denotational Semantics. ICALP 1982.

    Google Scholar 

  19. Scott, D. S., Lectures on a mathematical theory of computation. Oxford University Computing Laboratory Technical Monograph PRG-19 (1981).

    Google Scholar 

  20. Smyth, M.B., Power domains and predicate transformers: a topological view. Proc. of ICALP 83, Springer Lecture Notes in Comp. Sc. vol. 154 (1983).

    Google Scholar 

  21. Stirling, C., A complete modal proof system for a subset of SCCS. Research report, Dept. of Comp. Sci., Edinburgh University (1984).

    Google Scholar 

  22. Stirling, C., A proof theoretic characterisation of observational equivalence. Research report, Dept. of Comp. Sci., Edinburgh University, CSR-132-83 (1983). A version also appears in the proceedings of the Bangalore conference, India (1983) and is to appear in Theoretical Computer Science.

    Google Scholar 

  23. Stirling, C., A Complete Intuitionistic Hennessy-Milner Logic. Handwritten note, Comp. Sc. Dept, University of Edinburgh (Sep. 84).

    Google Scholar 

  24. Winskel, G., On the composition and decomposition of assertions. In the proceedings of the joint US-UK seminar on the semantics of concurrency, July 1984, Carnegie-Mellon University, Pittsburgh, Springer-Verlag Lecture Notes in Comp. Sc. 197, and appears as a report of the Computer Laboratory, University of Cambridge (1984).

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

S. N. Maheshwari

Rights and permissions

Reprints and permissions

Copyright information

© 1985 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Winskel, G. (1985). A complete proof system for SCCS with modal assertions. In: Maheshwari, S.N. (eds) Foundations of Software Technology and Theoretical Computer Science. FSTTCS 1985. Lecture Notes in Computer Science, vol 206. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16042-6_22

Download citation

  • DOI: https://doi.org/10.1007/3-540-16042-6_22

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-16042-7

  • Online ISBN: 978-3-540-39722-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics