On the temporal analysis of fairness

ABSTRACT

The use of the temporal logic formalism for program reasoning is reviewed. Several aspects of responsiveness and fairness are analyzed, leading to the need for an additional temporal operator: the 'until' operator -U. Some general questions involving the 'until' operator are then discussed. It is shown that with the addition of this operator the temporal language becomes expressively complete. Then, two deductive systems DX and DUX are proved to be complete for the languages without and with the new operator respectively.

REFERENCES

• 1: Michael J. Fischer , Richard E. Ladner, Propositional modal logic of programs, Proceedings of the ninth annual ACM symposium on Theory of computing, p.286-294, May 04-04, 1977, Boulder, Colorado, United States [doi>10.1145/800105.803418]
• 2: {G1} - Gabbay, D.: "Axiomatization of Logic of Programs", Manuscript, Nov. (1977).
• 3: {G2} - Gabbay, D.: "The Separation Property of tense Logics", Manuscript, Sept. (1979).
• 4: David Gries, A Proof Correctness of Rem''s Semaphore Implementation of the With-When Statement, Cornell University, Ithaca, NY, 1977
• 5: {K1} - Kamp, H. W.: "Tense Logic and the Theory of Linear Order", Ph.D. Thesis University of California, Los Angeles 1968.
• 6: {K2} - Kamp H. W.: Completeness Results in Temporal Logic", Preprint (1978).
• 7: {KR} - Krablin, L.: "A Temporal Analysis of Fairness," M.Sc. Thesis, University of Pennsylvania (1979)
• 8: {L1} - Lamport, L: "Proving the Correctness of Multiprocess Programs", IEEE Trans. Software Engineering, SE-3, 7 (March 1977) pp. 125-132.
• 9: Leslie Lamport, A New Approach to Proving the Correctness of Multiprocess Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.1, p.84-97, July 1979 [doi>10.1145/357062.357068]
• 10: Zohar Manna , Amir Pnueli, The Modal Logic of Programs, Proceedings of the 6th Colloquium, on Automata, Languages and Programming, p.385-409, July 16-20, 1979
• 11: {MY} - Myers, T. J. and A. Pnueli: "The Temporal Situation Until Now", Technical Note, University of Pennsylvania (1979).
• 12: {P1} - Pnueli, A.: "The Temporal Logic of Programs", 19th Annual Symp. on Foundations of Computer Science, Providence, R.I.
• 13: Amir Pnueli, The Temporal Semantics of Concurrent Programs, Proceedings of the International Sympoisum on Semantics of Concurrent Computation, p.1-20, July 02-04, 1979
• 14: {SS} - Shelah, S., J. Stavi: "Expressive Completeness for Temporal Logic", Forthcoming.