Skip to main content

On axiomatic defintion of max-model of concurrency

  • Conference paper
  • First Online:
  • 141 Accesses

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

Abstract

The thesis we present in this paper states that for every concurrent program π there exists a set of modal formulas, also called the axioms Ax(π), such that a) the structure of admissible parallel executions of the program π is a Kripke model of the set Ax(π) and, b) any Kripke model of the axioms Ax(π) is an extension of the structure of all admissible distributed (i.e. parallel) executions of the program π.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Apt K.R., Francez N., de Roever W.P., A Proof System for Communicating Sequential Processes, ACM TOPLAS, vol.2,No.3 (1980), 361–385

    Article  Google Scholar 

  2. Best E., Devillers R., Concurrent Behaviour: Sequences, Processes and Programming Languages, GMD-Studien No.99 (1985)

    Google Scholar 

  3. Enjalbert P., Michel M., Many-sorted Temporal Logic for Multiprocesses Systems, Proc. MFCS'84 (Chytil M. and Koubek V. eds) in LNCS 176, 1984, 273–282

    Google Scholar 

  4. Floyd R.W., Assigning Meanings to Programs, Proc.AMS (1967)

    Google Scholar 

  5. Hoare C.A.R., Communicating Sequential Processes, CACM 21 (1978), 666–677

    Google Scholar 

  6. Kripke S., Semantical analysis of modal logic II. The theory of Models, Amsterdam North-Holland 1965

    Google Scholar 

  7. Lamport L., Schneider F., The "Hoare Logic" of CSP and All That, TOPLAS 6 (1984), 281–295

    Article  Google Scholar 

  8. Mirkowska G., Salwicki A., Algorithmic Logic, Warsaw, PWN-Reidel Publ. (1987)

    Google Scholar 

  9. Owicki S., Gries D., An Axiomatic Proof Technique for Parallel Programs, Acta Informatica 6 (1976), 319–340

    Article  Google Scholar 

  10. Salwicki A., Muldner T., On Algorithmic Properties of Concurrent Programs, in Logics of programs, Zurich 1979 (E.Engeler ed.) LNCS 125 (1981) Springer-Verlag, 169–197

    Google Scholar 

  11. de Roever W.P., The quest for compositionality — a survey of assertionbased Proof Systems for Concurrent Programs, Part I: Concurrency Based on Shared Variables, Proc. of the IFIP Working Conf. 1985 "The Role of Abstract Models in Computer Science" (E. J.Neuhold ed.) North-Holland

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Marisa Venturini Zilli

Rights and permissions

Reprints and permissions

Copyright information

© 1987 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Mirkowska, G., Salwicki, A. (1987). On axiomatic defintion of max-model of concurrency. In: Zilli, M.V. (eds) Mathematical Models for the Semantics of Parallelism. Lecture Notes in Computer Science, vol 280. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-18419-8_16

Download citation

  • DOI: https://doi.org/10.1007/3-540-18419-8_16

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-18419-5

  • Online ISBN: 978-3-540-47960-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics