Dov Gabbay
Amir Pnueli
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.
- {FL} - Fischer, M. J. and R. L. Ladner: "Propositional Modal Logic of Programs", Proc. of the 9th ACM Symp. on the Theory of Computing, Boulder, Col. May (1977). Google Scholar
Digital Library
- {G1} - Gabbay, D.: "Axiomatization of Logic of Programs", Manuscript, Nov. (1977).Google Scholar
- {G2} - Gabbay, D.: "The Separation Property of tense Logics", Manuscript, Sept. (1979).Google Scholar
- {GR} - Gries, D.: "A Proof of Correctness of Reim's Semaphore Implementation of the with-when statement", Technical Report TR 77-314, Cornell University, Ithaca, N.Y. Google ScholarDigital Library
- {K1} - Kamp, H. W.: "Tense Logic and the Theory of Linear Order", Ph.D. Thesis University of California, Los Angeles 1968.Google Scholar
- {K2} - Kamp H. W.: Completeness Results in Temporal Logic", Preprint (1978).Google Scholar
- {KR} - Krablin, L.: "A Temporal Analysis of Fairness," M.Sc. Thesis, University of Pennsylvania (1979)Google Scholar
- {L1} - Lamport, L: "Proving the Correctness of Multiprocess Programs", IEEE Trans. Software Engineering, SE-3, 7 (March 1977) pp. 125-132.Google ScholarDigital Library
- {L2} - Lamport, L.: "Proving The Correctness of Multiprocess Programs", ACM TOPLAS, Vol. 1, No. 1 (July (1979) pp. 84-97. Google ScholarDigital Library
- {MP} - Manna, Z., Pnueli, A.: "The Modal Logic of Programs", Int. Conference in Automata, Languages and Programming, Graz (July 1979). Google ScholarDigital Library
- {MY} - Myers, T. J. and A. Pnueli: "The Temporal Situation Until Now", Technical Note, University of Pennsylvania (1979).Google Scholar
- {P1} - Pnueli, A.: "The Temporal Logic of Programs", 19th Annual Symp. on Foundations of Computer Science, Providence, R.I. Google ScholarDigital Library
- {P2} - Pnueli, A.: "The Temporal Semantics of Concurrent Programs", Int. Symp. Semantics of Concurrent Computation, Evian, July 1979. Google ScholarDigital Library
- {SS} - Shelah, S., J. Stavi: "Expressive Completeness for Temporal Logic", Forthcoming.Google Scholar
- On the temporal analysis of fairness
Recommendations
Constructive linear-time temporal logic: Proof systems and Kripke semantics
In this paper we study a version of constructive linear-time temporal logic (LTL) with the ''next'' temporal operator. The logic is originally due to Davies, who has shown that the proof system of the logic corresponds to a type system for binding-time ...
A Paraconsistent Linear-time Temporal Logic
Inconsistency-tolerant reasoning and paraconsistent logic are of growing importance not only in Knowledge Representation, AI and other areas of Computer Science, but also in Philosophical Logic. In this paper, a new logic, paraconsistent linear-time ...
Comments