Expressing interesting properties of programs in propositional temporal logic

ABSTRACT

We show that the class of properties of programs expressible in propositional temporal logic can be substantially extended if we assume the programs to be <i>data-independent.</i> Basically, a program is data-independent if its behavior does not depend on the specific data it operates upon. Our results significantly extend the applicability of program verification and synthesis methods based on propositional temporal logic.

REFERENCES

• 1: {AK85} K. R. Apt, D. C. Kozen, "Limits for Automatic Program Verification", IBM Research Report RC11095, 1985.
• 2: K. A. Bartlett , R. A. Scantlebury , P. T. Wilkinson, A note on reliable full-duplex transmission over half-duplex links, Communications of the ACM, v.12 n.5, p.260-261, May 1969 [doi>10.1145/362946.362970]
• 3: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 4: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite state concurrent system using temporal logic specifications: a practical approach, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.117-126, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567080]
• 5: Edmund M. Clarke , Bud Mishra, Automatic Verification of Asynchronous Circuits, Proceedings of the Carnegie Mellon Workshop on Logic of Programs, p.101-115, June 06-08, 1983
• 6: E. Allen Emerson , Joseph Y. Halpern, "Sometimes" and "not never" revisited: on branching versus linear time (preliminary report), Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.127-140, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567081]
• 7: E. Allen Emerson , Chin-Laung Lei, Modalities for model checking (extended abstract): branching time strikes back, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.84-96, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318620]
• 8: Yishai A. Feidman, A decidable propositional probabilistic dynamic logic, Proceedings of the fifteenth annual ACM symposium on Theory of computing, p.298-309, December 1983 [doi>10.1145/800061.808759]
• 9: {F167} R. W. Floyd, "Assigning Meaning to Programs", Proc. Symp. Appl. Math., 19, in <i>Mathematical Aspects of Computer Science,</i> (J. T. Schwartz, ed.), AMS, Providence, 1967, pp. 19--32.
• 10: {FL79} M. Fischer, R. Ladner, "Propositional Dynamic Logic of Regular Programs", <i>J. of Computer and System Sciences,</i> 18(2), 1979, pp. 194--211.
• 11: Dov Gabbay , Amir Pnueli , Saharon Shelah , Jonathan Stavi, On the temporal analysis of fairness, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.163-173, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567462]
• 12: David Harel, First-Order Dynamic Logic, Springer-Verlag New York, Inc., Secaucus, NJ, 1979
• 13: {HKP82} D. Harel, D. Kozen, R. Parikh, "Process Logic: Expressiveness, Decidability, Completeness", <i>Journal of Computer and System Science</i> 25, 2 (1982), pp. 144--170.
• 14: Joseph Y. Halpern , Yoram Moses, Knowledge and common knowledge in a distributed environment, Proceedings of the third annual ACM symposium on Principles of distributed computing, p.50-61, August 27-29, 1984, Vancouver, British Columbia, Canada [doi>10.1145/800222.806735]
• 15: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 16: C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.21 n.8, p.666-677, Aug. 1978 [doi>10.1145/359576.359585]
• 17: {HO83} B. T. Hailpern and S. S. Owicki, "Modular Verification of Computer Communication Protocols", <i>IEEE Trans. on Comm.,</i> Vol. COM-31, No. 1, January, 1983, pp. 56--68.
• 18: Dexter Kozen, A probabilistic PDL, Proceedings of the fifteenth annual ACM symposium on Theory of computing, p.291-297, December 1983 [doi>10.1145/800061.808758]
• 19: Leslie Lamport, "Sometime" is sometimes "not never": on the temporal logic of programs, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-185, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567463]
• 20: Daniel Lehmann, Knowledge, common knowledge and related puzzles (Extended Summary), Proceedings of the third annual ACM symposium on Principles of distributed computing, p.62-67, August 27-29, 1984, Vancouver, British Columbia, Canada [doi>10.1145/800222.806736]
• 21: Orna Lichtenstein , Amir Pnueli, Checking that finite state concurrent programs satisfy their linear specification, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.97-107, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318622]
• 22: Zohar Manna , Pierre Wolper, Synthesis of Communicating Processes from Temporal Logic Specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.1, p.68-93, Jan. 1984 [doi>10.1145/357233.357237]
• 23: {Pn81} A. Pnueli, "The Temporal Logic of Concurrent Programs", <i>Theoretical Computer Science</i> 13(1981), pp. 45--60.
• 24: Amir Pnueli, Linear and Branching Structures in the Semantics and Logics of Reactive Systems, Proceedings of the 12th Colloquium on Automata, Languages and Programming, p.15-32, July 15-19, 1985
• 25: {Pr76} V. R. Pratt, "Semantical Considerations on Floyd-Hoare Logic", <i>Proc. 17th IEEE Symp. on Foundations of Computer Science,</i> Houston, October 1976, pp. 109--121.
• 26: {Pr80} V. R. Pratt, "A Near-Optimal Method for Reasoning about Action", <i>J. Computer and Systems Sciences</i> 20(1980), pp. 231--254.
• 27: {PZ85} A. Pnueli, L. Zuck, "The Gallant Model Checker", to appear.
• 28: {QS82} J. P. Queille, J. Sifakis, <i>"Fairness and Related Properties in Transition Systems",</i> Research Report #292, IMAG, Grenoble, 1982.
• 29: A. P. Sistla , E. M. Clarke, The complexity of propositional linear temporal logics, Journal of the ACM (JACM), v.32 n.3, p.733-749, July 1985 [doi>10.1145/3828.3837]
• 30: A. P. Sistla , E. M. Clarke , N. Francez , Y. Gurevich, Can message buffers be characterized in linear temporal logic?, Proceedings of the first ACM SIGACT-SIGOPS symposium on Principles of distributed computing, p.148-156, August 18-20, 1982, Ottawa, Canada [doi>10.1145/800220.806692]
• 31: {St82} R. S. Streett, "Propositional Dynamic Logic of Looping and Converse", <i>Information and Control</i> 54(1982), pp. 121--141.
• 32: {SWL85} K. Sabnani, P. Wolper, A. Lapone, "An Algorithmic Technique for Protocol Verification", to appear.
• 33: {Va85} M. Vardi, "Automatic Verification of Probabilistic Concurrent Finite-State Programs". <i>Proc. 26th Symp. on Foundations of Computer Science,</i> Portland, to appear.
• 34: Friedrich H. Vogt, Event-Based Temporal Logic Specifications of Services and Protocols, Proceedings of the IFIP WG6.1 Second International Workshop on Protocol Specification, Testing and Verification, p.63-73, May 17-20, 1982
• 35: Moshe Y. Vardi , Pierre Wolper, Yet Another Process Logic (Preliminary Version), Proceedings of the Carnegie Mellon Workshop on Logic of Programs, p.501-512, June 06-08, 1983
• 36: Moshe Y. Vardi , Pierre Wolper, Automata theoretic techniques for modal logics of programs: (Extended abstract), Proceedings of the sixteenth annual ACM symposium on Theory of computing, p.446-456, December 1984 [doi>10.1145/800057.808711]
• 37: {VW85} M. Y. Vardi, P. Wolper, "An Automata-Theoretic Approach to Automatic Program Verification", to appear.
• 38: Pierre Leon Wolper, Synthesis of communicating processes from temporal logic specifications, 1982
• 39: {Wo83} P. Wolper, "Temporal Logic Can Be More Expressive", <i>Information and Control,</i> Vol. 56, Nos. 1--2, 1983, pp. 72--99.
• 40: {WVS83} P. Wolper, M. Y. Vardi, A. P. Sistla, "Reasoning about Infinite Computation Paths", <i>Proc. 24th IEEE Symposium on Foundations of Computer Science,</i> Tucson, 1983, pp. 185--194.