A Decision Method for Linear Temporal Logic

  • Ana R. Cavalli
  • Luis FariÑas Del Cerro
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 170)


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.


Temporal Logic Linear Temporal Logic Decision Method Conjunctive Normal Form Modal Formula 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [BM]
    BEN-ARI M.-Complexity of proofs and models in programming logics. Ph D., Tel-Aviv University, May 1981.Google Scholar
  2. [CR]
    CARNAP R.-Modalities and quantification. JSL Vol. 11, 1946, pp. 33–64.MathSciNetzbMATHGoogle Scholar
  3. [CHL]
    CHANG C., LEE R.-Symbolical logic and mechanical theorem proving. Academic Press, New-York, 1973.Google Scholar
  4. [FC]
    FARIÑAS DEL CERRO L.-A simple deduction method for modal logic. Information Processing Letters, Vol. 14, n∘2, 1982Google Scholar
  5. [FL]
    FARIÑAS DEL CERRO L., LAUTH E.-Raisonnement temporel: une méthode de déduction. Rapport Université Paul Sabatier, Toulouse, 1983.Google Scholar
  6. [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
  7. [LE]
    LEMMON E.-An introduction to modal logic. Amer. Phil. Quaterly Monograph Series, 1977.Google Scholar
  8. [MZ]
    MANNA Z.-Verification of sequential programs: Temporal axiomatization, Report NoSTAN-CS-81-877, Stanford University, 1981.Google Scholar
  9. [RJ]
    ROBINSON J.-A machine oriented logic based on the resolution principle. J. ACM, 12, 1965, pp. 23–41.MathSciNetCrossRefzbMATHGoogle Scholar
  10. [CE]
    CLARKE E., EMERSON E.-Design and synthesis of synchronization skeletons using branching time temporal logic, 1981.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • Ana R. Cavalli
    • 1
  • Luis FariÑas Del Cerro
    • 2
  1. 1.LITPUniversité Paris VIIParis Cedex 05France
  2. 2.LSIUniversité Paul SabatierToulouse CedexFrance

Personalised recommendations