Skip to main content
SpringerLink
Log in

Linear and branching structures in the semantics and logics of reactive systems

  • Conference paper
  • First Online:
Automata, Languages and Programming (ICALP 1985)

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

Included in the following conference series:

Abstract

In this presentation we reviewed the dichotomy between branching and linear views of reactive systems as they are reflected in three different approaches to the formalization of reactive systems. Hopefully we succeeded in convincing the reader that these views are distinct and represent different attitudes to the desired level of abstractness in the semantics of reactive systems. The branching view is always more detailed than the linear view, and the important question that should be left open for the user of the approach, is whether this additional detail is necessary for his application.

In this presentation we only considered the branching vs. linear dichotomy in the treatment of nondeterminism. A very similar dichotomy exists in the treatment of concurrency itself, namely between the partial order (hence acyclic graph) representation of causality and concurrency and its linearization by all the total orders consistent with this partial order. We suggest a similar study for the identification of the elements captured in the partial order which are lost in the linearization.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Apt, K.R., Francez, N., DeRoever, W.P. A Proof System for Communicating Sequential Processes, TOPLAS 2, 3 (1980) 359–385.

    Article  Google Scholar 

  2. de Bakker, J.W., Bergstra, J.A., Klop, J.W., Meyer, J.J.C. Linear Time and Branching Time Semantics for Recursion with Merge, 10th ICALP, LNCS 154 (1983) 39–51.

    Google Scholar 

  3. Brookes, S.D., Hoare, C.A.R., Roscoe, A.W. A Theory of Communicating Sequential Processes, JACM 31 (1984) 560–569.

    Article  Google Scholar 

  4. Barringer, H., Kuiper, R., Pnueli, A. Now You May Compose Temporal Logic Specifications, 16th ACM Symposium on Theory of Computing (1984) 51–63.

    Google Scholar 

  5. Barringer, H., Kuiper, R., Pnueli, A. A Compositional Temporal Approach to a CSP-like Language, Proc. of IFIP Conference, the Role of Abstract Models in Information Processing, Vienna (1985).

    Google Scholar 

  6. Ben Ari, M., Manna, Z., Pnueli, A. The Temporal Logic of Branching Time, Acta Informatica 20 (1983) 207–226.

    Article  Google Scholar 

  7. Brookes, S.D. A Semantics and Proof System for Communicating Processes, 2nd Conference on Logics of Programs, Springer Verlag LNCS 164 (1983) 68–85.

    Google Scholar 

  8. Brookes, S.D. On the Relationship of CCS and CSP, 10th ICALP, Springer Verlag LNCS 154 (1983) 83–96.

    Google Scholar 

  9. Brookes, S.D., Rounds, W.C. Behavioral Equivalence Relations Induced by Programming Logics, 10th ICALP, Springer Verlag LNCS 154 (1983) 97–108.

    Google Scholar 

  10. Clarke, E.M., Emerson, E.A. Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic, Proc. of an IBM Workshop on Logics of Programs, LNCS 131 (1981) 52–71.

    Google Scholar 

  11. De Nicola A Complete Set of Axioms for a Theory of Communicating Sequential Processes, Foundations of Computation Theory, Springer Verlag LNCS 158 (1983) 115–126.

    Google Scholar 

  12. Emerson, E.A., Halpern, J.Y. 'sometimes’ and ‘Not Never’ Revisited: On Branching Versus Linear Time, 10th ACM Symposium on Principles of Programming Languages (1983).

    Google Scholar 

  13. Francez, N., Hoare, C.A.R., Lehmann, D., DeRoever, W.P. Semantics of Non-Determinism, Concurrency and Communication, JCSS 19 3 (1979).

    Google Scholar 

  14. Floyd, R. W. Assigning Meanings to Programs, Proc. Symposium on Applied Mathematics, AMS, 19 (1967).

    Google Scholar 

  15. Francez, N., Lehmann, D., Pnueli, A. A Linear History Semantics for Languages for Distributed Programming, Theoretical Computer Science 32 (1984) 25–46.

    Article  Google Scholar 

  16. Gabbay, D., Pnueli, A., Stavi, J., Shelah, S. On the Temporal Analysis of Fairness, 7th ACM Symposium on Principles of Programming Languages (1980) 163–173.

    Google Scholar 

  17. Graf, S., Sifakis, J. A Modal Characterization of Observational Congruence on Finite Terms of CCS, 11th ICALP, LNCS 172 (1984).

    Google Scholar 

  18. Graf, S., Sifakis, J. A Logic for the Specification and Proof of Controllable Processes of CCS, Proceedings Advanced Institute on Logics and Models for Verification and Specification of Concurrent Systems, La Colle Surs Loupe (1984).

    Google Scholar 

  19. Graf, S., Sifakis, J. A Logic for the Description of Non-Deterministic Programs and Their Properties, IMAG, Grenoble (1985).

    Google Scholar 

  20. Hoare, D. Statecharts: An Axiomatic Approach to Computer Programming, CACM 12, 10 (1969).

    Google Scholar 

  21. Harel, D. Statecharts: A Visual Approach to Complex Systems, Technical Report CS84-05, Weizmann Institute of Science.

    Google Scholar 

  22. Hennesy, M., Milner R. Algebraic Laws for Nondeterminism and Concurrency, JACM 32 1 (1985) 137–161.

    Article  Google Scholar 

  23. Harel, D., Pnueli, A. On the Development of Reactive Systems, Proceeding Advanced Institute on Logics and Models for Verification and Specification of Concurrent Systems. La Colle Sur Loupe (Oct. 84).

    Google Scholar 

  24. Hennesy, M., Plotkin, G. A Term Model for CCS, 9th Conference on Mathematical Foundations of Computer Science, LNCS 88 (1980) 261–274.

    Google Scholar 

  25. Kozen, D. Results on the Propositional μ-calculus, 9th ICALP, LNCS 140 (1982) 340–359.

    Google Scholar 

  26. Lamport, L. “Sometimes” is Sometimes “Not Never”, 7th ACM Symposium on Principles of Programming Languages (1980) 174–185.

    Google Scholar 

  27. Milner, R. Fully Abstract Models of Typed λ-calculi, Theoretical Computer Science (1977).

    Google Scholar 

  28. Milner, R. A. Calculus of Communicating Systems, LNCS 92 (1980).

    Google Scholar 

  29. Milner, R. A Calculi for Synchrony and Asynchrony, Theoretical Computer Science 25, 3 (1983) 267–310.

    Article  Google Scholar 

  30. de Nicola, R., Hennesy, M.C.B. Testing Equivalences for Processes, 10th ICALP, LNCS 154 (1983).

    Google Scholar 

  31. Owicki, S., Gries, D. An Axiomatic Proof Technique for Parallel Programs, Acta Informatica 6 (1976).

    Google Scholar 

  32. Olderog, E.R., Hoare, C.A.R. Specification Oriented Semantics for Communicating Processes, 10th ICALP, LNCS 154 (1983) 561–572.

    Google Scholar 

  33. Plotkin, G.D. A Powerdomain Construction, SIAM Journal on Computing 5, 3 (1976) 452–487.

    Article  Google Scholar 

  34. Pnueli, A. The Temporal Semantics of Concurrent Programs, Theoretical Computer Science, 13 (1981) 45–60.

    Article  Google Scholar 

  35. Pnueli, A. In Transition from Global to Modular Temporal Reasoning about Programs, Proc. Advanced Institute on Logics and Models for Verification and Specification of Concurrent Systems, La Colle Sur Loupe Springer Verlag (Oct. 84).

    Google Scholar 

  36. Queille, J.P., Sifakis, J. Fairness and Related Properties in Transition Systems—A Temporal Logic to deal with Fairness, Acta Informatica 19 (1983) 195–220.

    Article  Google Scholar 

  37. Rounds, W.C., Brookes, S.D. Possible Futures, Acceptances, Refusals and Communicating Processes, 22nd IEEE Symposium Foundations of Computer Science (1981) 140–149.

    Google Scholar 

  38. Smyth, M. Powerdomains, JCSS 16, 1 (1978).

    Google Scholar 

  39. Stirling, C. A Complete Modal Proof for a Subset of SCCS, Mathematical Foundations of Software Development, Springer Verlag, LNCS 185 (1985) 251–266.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Applied Mathematics, The Weizmann Institute of Science, 76100, Rehovot, Israel

    Amir Pnueli

Authors
  1. Amir Pnueli
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Wilfried Brauer

Rights and permissions

Reprints and permissions

Copyright information

© 1985 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Pnueli, A. (1985). Linear and branching structures in the semantics and logics of reactive systems. In: Brauer, W. (eds) Automata, Languages and Programming. ICALP 1985. Lecture Notes in Computer Science, vol 194. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0015727

Download citation

  • DOI: https://doi.org/10.1007/BFb0015727

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-39557-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation