A Decision Method for Linear Temporal Logic
In this paper we define a new decision method for propositional temporal logic of programs. Temporal logic appears to be an appropriate tool to prove some properties of programs such as invariance or eventually because in this logic we define operators that enable us to represent properties that are valid during all the development of the program or over some parts of the program.
The decision method that we define is an extension of classical resolution to temporal operators.
We give an example of a mutual exclusion problem and we show, using resolution method, that it verifies a liveness property.
KeywordsTemporal Logic Linear Temporal Logic Decision Method Conjunctive Normal Form Modal Formula
Unable to display preview. Download preview PDF.
- [BM]BEN-ARI M.-Complexity of proofs and models in programming logics. Ph D., Tel-Aviv University, May 1981.Google Scholar
- [CHL]CHANG C., LEE R.-Symbolical logic and mechanical theorem proving. Academic Press, New-York, 1973.Google Scholar
- [FC]FARIÑAS DEL CERRO L.-A simple deduction method for modal logic. Information Processing Letters, Vol. 14, n∘2, 1982Google Scholar
- [FL]FARIÑAS DEL CERRO L., LAUTH E.-Raisonnement temporel: une méthode de déduction. Rapport Université Paul Sabatier, Toulouse, 1983.Google Scholar
- [GPSS]GABBAY D., PNUELI A., SHEALAH S., STAVI J.-Temporal Analysis of Fairness. Seventh ACM Symposium on Principles of Programming Languages. Las Vegas, NV, Janvier 1980.Google Scholar
- [LE]LEMMON E.-An introduction to modal logic. Amer. Phil. Quaterly Monograph Series, 1977.Google Scholar
- [MZ]MANNA Z.-Verification of sequential programs: Temporal axiomatization, Report NoSTAN-CS-81-877, Stanford University, 1981.Google Scholar
- [CE]CLARKE E., EMERSON E.-Design and synthesis of synchronization skeletons using branching time temporal logic, 1981.Google Scholar