The Complexity of Propositional Linear Temporal Logics in Simple Cases

Basin, 1998, Automata based symbolic reasoning in hardware verification, Formal Methods in System Design, 13, 253, 10.1023/A:1008644009416

Bjørner, N., Browne, A., Chang, E., Colón, M., Kapur, A., Manna, Z., Sipma, H. B., and Uribe, T. E.1996, STeP: Deductive-algorithmic verification of reactive and real-time systems, inProc. 8th Int. Conf. Computer Aided Verification (CAV'96), New Brunswick, NJ, July-Aug., 1996, Lecture Notes in Computer Science, Vol. 1102, pp. 415–418, Springer-Verlag, Berlin.

Browne, 1988, Characterizing finite Kripke structures in propositional temporal logic, Theoret. Comput. Sci., 59, 115, 10.1016/0304-3975(88)90098-9

Bull, 1965, An algebraic study of Diodorean modal systems, J. Symbolic Logic, 30, 58, 10.2307/2270582

Chen, 1993, The computational complexity of satisfiability of temporal Horn formulas in propositional linear-time temporal logic, Inform. Process. Lett., 45, 131, 10.1016/0020-0190(93)90014-Z

Clarke, 1997, Another look at LTL model checking, Formal Methods in System Design, 10, 47, 10.1023/A:1008615614281

Comon, H., and Cortier, V.2000, Flatness is not a weakness, inProc. 14th Int. Workshop Computer Science Logic (CSL'2000), Fischbachau, Germany, Aug. 2000, Lecture Notes in Computer Science, Vol. 1862, pp. 262–276, Springer-Verlag, Berlin.

Cook, S.1971, The complexity of theorem-proving procedures, inProc. 3rd ACM Symp. Theory of Computing (STOC'71), Shaker Heights, OH, May 1971, pp. 151–158.

Dalal, M.1996, An almost quadratic class of satisfiability problems, inProc. 12th European Conf. Artificial Intelligence (ECAI'96), Budapest, Hungary, Aug. 1996, pp. 355–359, Wiley, New York.

Dams, 1999, Flat fragments of CTL and CTL*: Separating the expressive and distinguishing powers, Logic Journal of the IGPL, 7, 55, 10.1093/jigpal/7.1.55

Demri, S.1996, A simple tableau system for the logic of elsewhere, inProc. 5th Int. Workshop on Theorem Proving with Analytical Tableaux and Related Methods (TABLEAUX'96), Terrasini, Palermo, Italy, May 1996, Lecture Notes in Artificial Intelligence, Vol. 1071, pp. 177–192, Springer-Verlag, Berlin.

Demri, S., and Schnoebelen, Ph.1998, The complexity of propositional linear temporal logics in simple cases (extended abstract), inProc. 15th Ann. Symp. Theoretical Aspects of Computer Science (STACS'98), Paris, France, Feb. 1998, Lecture Notes in Computer Science, Vol. 1373, pp. 61–72, Springer-Verlag, Berlin.

Diekert, V., and Gastin, P.1999, An expressively complete temporal logic without past tense operators for Mazurkiewicz traces, inProc. 13th Int. Workshop Computer Science Logic (CSL'99), Madrid, Spain, Sep. 1999, Lecture Notes in Computer Science, Vol. 1683, pp. 188–203, Springer-Verlag, Berlin.

Dixon, C., Fisher, M., and Reynolds, M.2000, Execution and proof in a Horn-clause temporal logic, inAdvances in Temporal LogicH. Barringer, M. Fisher, D. Gabbay, and G. Gough, Eds., Applied Logic Series, Vol. 16, pp. 413–433, Kluwer Academic, Dordrecht.

Donini, 1997, The complexity of concept languages, Inform. and Comput., 134, 1, 10.1006/inco.1997.2625

Emerson, E. A.1990, Temporal and modal logic, inHandbook of Theoretical Computer ScienceJ. van Leeuwen, Ed., Vol. B, Chap. 16, pp. 995–1072, Elsevier, Amsterdam.

Emerson, E. A., Evangelist, M., and Srinivasan, J.1990, On the limits of efficient temporal decidability, inProc. 5th IEEE Symp. Logic in Computer Science (LICS'90), PA, June 1990, pp. 464–475.

Emerson, 1987, Modalities for model checking: Branching time logic strikes back, Sci. Comput. Programming, 8, 275, 10.1016/0167-6423(87)90036-0

Franco, 1998, A perspective on certain polynomial time solvable classes of satisfiability, Discrete Appl. Math.

Goré, 1994, Cut-free sequent and tableau systems for propositional Diodorean modal logics, Studia Logica, 53, 433, 10.1007/BF01057938

Halpern, 1995, The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic, Artificial Intelligence, 75, 361, 10.1016/0004-3702(95)00018-A

Halpern, 1983, The propositional dynamic logic of deterministic, well-structured programs, Theoret. Comput. Sci., 27, 127, 10.1016/0304-3975(83)90097-X

Harel, 1985, Recurring dominos: Making the highly undecidable highly understandable, Ann. Discrete Math., 24, 51

Hemaspaandra, E.2000, The complexity of Poor Man's logic, inProc. 17th Ann. Symp. Theoretical Aspects of Computer Science (STACS'2000), Lille, France, Feb. 2000, Lecture Notes in Computer Science, Vol. 1770, pp. 230–241, Springer-Verlag, Berlin.

Holzmann, 1997, The model checker Spin, IEEE Trans. Software Engineering, 23, 279, 10.1109/32.588521

Jones, 1975, Space-bounded reducibility among combinatorial problems, J. Comput. System Sci., 11, 68, 10.1016/S0022-0000(75)80050-X

Kupferman, O., and Vardi, M. Y.1998, Relating linear and branching model checking, inProc. IFIP Working Conference on Programming Concepts and Methods (PROCOMET'98), Shelter Island, NY, June 1998, pp. 304–326, Chapman & Hall, London.

Lamport, L.1983, What good is temporal logic?inInformation Processing'83. Proc. IFIP 9th World Computer Congress, Sep. 1983, Paris, France, pp. 657–668, North-Holland, Amsterdam.

Laroussinie, F., Markey, N., and Schnoebelen, Ph.2001, Model checking CTL+ and FCTL is hard, inProc. 4th Int. Conf. Foundations of Software Science and Computation Structures (FOSSACS'2001), Genova, Italy, Apr. 2001, Lecture Notes in Computer Science, Vol. 2030, pp. 318–331, Springer-Verlag, Berlin.

Laroussinie, 2000, Specification in CTL+Past for verification in CTL, Inform. and Comput., 156, 236, 10.1006/inco.1999.2817

Lichtenstein, O., and Pnueli, A.1985, Checking that finite state concurrent programs satisfy their linear specification, inProc. 12th ACM Symp. Principles of Programming Languages (POPL'85), New Orleans, LA, Jan. 1985, pp. 97–107.

Lynch., 1977, Log space recognition and translation of parenthesis languages, J. Assoc. Comput. Mach., 24, 583, 10.1145/322033.322037

Manna, Z, and, Pnueli, A. 1992, The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag, Berlin.

Mishra, 1985, Hierarchical verification of asynchronous circuits using temporal logic, Theoret. Comput. Sci., 38, 269, 10.1016/0304-3975(85)90223-3

Ono, 1980, On the size of refutation Kripke models for some linear modal and tense logics, Studia Logica, 39, 325, 10.1007/BF00713542

Papadimitriou, C. H. 1994, Computational Complexity, Addison-Wesley, Reading, MA.

Schobbens, 1999, The logic of “initially” and “next”: Complete axiomatization and complexity, Inform. Process. Lett., 69, 221, 10.1016/S0020-0190(99)00022-8

Segerberg, K. 1971, An Essay in Classical Modal Logic (Three Vols.), Technical Report Filosofiska Studier 13, Uppsala Universitet.

Sistla, 1985, The complexity of propositional linear temporal logics, J. Assoc. Comput. Mach., 32, 733, 10.1145/3828.3837

Spaan, E. 1993, Complexity of Modal Logics, Ph.D. thesis, ILLC, Amsterdam University, Netherlands.

Vardi, M. Y.1994, Nontraditional applications of automata theory, inProc. Int. Symp. Theoretical Aspects of Computer Software (TACS'94), Sendai, Japan, Apr. 1994, Lecture Notes in Computer Science, Vol. 789, pp. 575–597, Springer-Verlag, Berlin.

Wolper, 1983, Temporal logic can be more expressive, Inform. and Control, 56, 72, 10.1016/S0019-9958(83)80051-5

Wolper, P., Vardi, M. Y., and Sistla, A. P.1983, Reasoning about infinite computation paths (extended abstract), inProc. 24th IEEE Symp. Foundations of Computer Science (FOCS'83), Tucson, AZ, Nov. 1983, pp. 185–194.