The complexity of propositional linear temporal logics

ABSTRACT

We consider the complexity of satisfiability and determination of truth in a particular finite structure for different propositional linear temporal logics. We show that both the above problems are NP-complete for the logic with F operator and are PSPACE-complete for the logics with F,X, with U, with U,S,X, and Wolper's extended logic with regular operators [Wo81].

REFERENCES

• 1: Mordechai Ben-Ari , Zohar Manna , Amir Pnueli, The temporal logic of branching time, Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.164-176, January 26-28, 1981, Williamsburg, Virginia [doi>10.1145/567532.567551]
• 2: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 3: M. Fisher, R. Ladner, "Propositional Dynamic Logic of Regular Programs," JCSS, 18(2), 1979.
• 4: Dov Gabbay , Amir Pnueli , Saharon Shelah , Jonathan Stavi, On the temporal analysis of fairness, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.163-173, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567462]
• 5: J. Y. Halpern and J. H. Reif, "The Propositional Dynamic Logic of Deterministic, Well-Structured Programs," 22nd Annual Symposium on Foundations of Computer Science, Nashville, TN, Oct. 1981.
• 6: R. Ladner, "The Computational Complexity of Provability in Systems of Modal Propositional Logic," SIAM J. Comp. 6, 467-480 (A9.Z).
• 7: Z. Manna, A. Pnueli, "Verification of Con-Current Programs," The Correctness Problem in Computer Science, International Lecture Series in Computer Science, Academic Press, London, 1981.
• 8: A. Pnueli, "The Temporal Logic of Programs," Proceedings of the Eighteenth Symposium on Foundations of Computer Science, Providence, RI, Nov. 1977.
• 9: P. Wolper, "Temporal Logic Can Be More Expressive," Proceedings of 22nd Symposium on Foundations of Computer Science, Nashville, TN, Oct. 1981.