To the Decision Problem for Branching Time Logic

  • Yuri Gurevich
  • Saharon Shelah


First we describe a certain branching time logic. We borrow this logic from Prior (1967) and call it BTL. It is a propositional logic whose formulas are built from propositional symbols by means of usual boolean connectives and additional unary connectives PAST, FUTURE, NECESSARY.


Decision Problem Binary Tree Complete Tree Theory Tree Time Logic 
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. Gurevich, Y., and Shelah, S., 1984, The Decision Problem for Branching Time Logic, J. Symbolic Logic, to appear.Google Scholar
  2. Prior, A. N., 1967, “Past, Present and Future,” Clarendon Press, Oxford.CrossRefGoogle Scholar

Copyright information

© Springer Science+Business Media New York 1985

Authors and Affiliations

  • Yuri Gurevich
    • 1
  • Saharon Shelah
    • 2
  1. 1.Electrical Engineering and Computer Science DepartmentUniversity of MichiganAnn ArborUSA
  2. 2.Mathematics DepartmentHebrew UniversityJerusalemIsrael

Personalised recommendations