Expressiveness bounds for completeness in trace-based network proof systems

  • Jennifer Widom
  • Prakash Panangaden
Parallelism And Concurrency
Part of the Lecture Notes in Computer Science book series (LNCS, volume 299)


Network proof systems based on first-order specifications over channel traces are incomplete unless reasoning over the interleaving of communication events is permitted. Relatively complete trace-based proof systems using temporal logic have been described, but full temporal logic is more powerful than necessary. Using the interleaving approach, we isolate the expressiveness required of a relatively complete trace logic. A hierarchy of temporal logic subsets is then defined; a certain subset is shown to have necessary and sufficient expressive power for relative completeness.


Temporal Operator Temporal Logic Inference Rule Proof System Expressive Power 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. [AS85]
    B. Alpern and F.B. Schneider. Defining liveness. Information Processing Letters, 21(4):181–185, October 1985.Google Scholar
  2. [BA81]
    J.D. Brock and W.B. Ackerman. Scenarios: a model of non-determinate computation. In Formalization of Programming Concepts, Lecture Notes in Computer Science 107, pages 252–259, Springer-Verlag, Berlin, 1981.Google Scholar
  3. [Bro84]
    S.D. Brookes. A semantics and proof system for communicating processes. In Logics of Programs, Lecture Notes in Computer Science 164, pages 68–85, Springer-Verlag, Berlin, 1984.Google Scholar
  4. [CH81]
    Z.C. Chen and C.A.R. Hoare. Partial correctness of communicating sequential processes. In Proceedings of the IEEE International Conference on Distributed Computing Systems, pages 1–12, Paris, April 1981.Google Scholar
  5. [Coo78]
    S.A. Cook. Soundness and completeness of an axiom system for program verification. SIAM Journal on Computing, 7(1):70–90, February 1978.Google Scholar
  6. [HH83]
    E.C.R. Hehner and C.A.R. Hoare. A more complete model of communicating processes. Theoretical Computer Science, 26:105–120, September 1983.Google Scholar
  7. [Hoa85]
    C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs, New Jersey, 1985.Google Scholar
  8. [Jon85]
    B. Jonsson. A model and proof system for asynchronous networks. In Proceedings of the Fourth ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, pages 49–58, August 1985.Google Scholar
  9. [MC81]
    J. Misra and K.M. Chandy. Proofs of networks of processes. IEEE Transactions on Software Engineering, 7(7):417–426, July 1981.Google Scholar
  10. [MP81]
    Z. Manna and A. Pnueli. Verification of concurrent programs: the temporal framework. In R.S. Boyer and J.S. Moore, editors, The Correctness Problem in Computer Science, pages 215–273, International Lecture Series in Computer Science, Academic Press, London, 1981.Google Scholar
  11. [MP82]
    Z. Manna and A. Pnueli. Verification of concurrent programs: a temporal proof system. In Proceedings of the Fourth School on Advanced Programming, pages 163–255, Amsterdam, June 1982.Google Scholar
  12. [NDGO86]
    V. Nguyen, A. Demers, D. Gries, and S. Owicki. A model and temporal proof system for networks of processes. Distributed Computing, 1(1):7–25, January 1986.Google Scholar
  13. [Ngu85]
    V. Nguyen. The incompleteness of Misra and Chandy's proof systems. Information Processing Letters, 21:93–96, August 1985.Google Scholar
  14. [RU71]
    N. Rescher and A. Urquhart. Temporal Logic. Library of Exact Philosophy, Springer-Verlag, Vienna, 1971.Google Scholar
  15. [Sch67]
    J.R. Schoenfield. Mathematical Logic. Addison-Wesley, Reading, Massachusetts, 1967.Google Scholar
  16. [WGS87]
    J. Widom, D. Gries, and F.B. Schneider. Completeness and incompleteness of trace-based network proof systems. In Proceedings of the Fourteenth ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 27–38, January 1987.Google Scholar
  17. [Wid87]
    J. Widom. Trace-Based Network Proof Systems: Expressiveness and Completeness. PhD thesis, Cornell University, Ithaca, New York, May 1987.Google Scholar
  18. [Wol81]
    P. Wolper. Temporal logic can be more expressive. In Proceedings of the 22nd Annual Symposium on Foundations of Computer Science, pages 340–348, October 1981.Google Scholar
  19. [ZdRvEB85]
    J. Zwiers, W.P. de Roever, and P. van Emde Boas. Compositionality and concurrent networks: soundness and completeness of a proofsystem. In Proceedings of the 12th International Colloquium on Automata, Languages, and Programming, Lecture Notes in Computer Science 194, pages 509–519, Springer-Verlag, Berlin, 1985.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1988

Authors and Affiliations

  • Jennifer Widom
    • 1
  • Prakash Panangaden
    • 1
  1. 1.Computer Science DepartmentCornell UniversityIthacaUSA

Personalised recommendations