Counting CTL

1. Adler, M., Immerman, N.: An n! lower bound on formula size. ACM Transactions on Computational Logic 4(3), 296–314 (2003)

   Article  MathSciNet  Google Scholar 

2. Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking in dense real-time. Inf. Comput. 104(1), 2–34 (1993)

   Article  MATH  MathSciNet  Google Scholar 

3. Bernholtz, O., Vardi, M., Wolper, P.: An automata-theoretic approach to branching-time model-checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 142–155. Springer, Heidelberg (1994)

   Google Scholar 

4. Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499–513. Springer, Heidelberg (1995)

   Google Scholar 

5. Bouajjani, A., Echahed, R., Habermehl, P.: On the verification problem of nonregular properties for nonregular processes. In: Proc. 10th LICS, pp. 123–133. IEEE Comp. Soc. Press, Los Alamitos (1995)

   Google Scholar 

6. Bouajjani, A., Echahed, R., Habermehl, P.: Verifying infinite state processes with sequential and parallel composition. In: Proc. 22nd POPL, pp. 95–106 (1995)

   Google Scholar 

7. Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)

   Chapter  Google Scholar 

8. Emerson, E.A.: Temporal and modal logic. In: Handbook of Theoretical Computer Science, vol. B, ch. 16, pp. 995–1072. Elsevier, Amsterdam (1990)

   Google Scholar 

9. Emerson, E.A., Mok, A.K., Sistla, A.P., Srinivasan, J.: Quantitative temporal reasoning. Real-Time Systems 4(4), 331–352 (1992)

   Article  Google Scholar 

10. Emerson, E.A., Trefler, R.J.: Generalized quantitative temporal reasoning: An automata-theoretic approach. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214, pp. 189–200. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

11. Emerson, E.A., Trefler, R.J.: Parametric quantitative temporal reasoning. In: Proc. 14th LICS, pp. 336–343. IEEE Comp. Soc. Press, Los Alamitos (1999)

    Google Scholar 

12. Laroussinie, F., Markey, N., Schnoebelen, P.: Model checking CTL ⁺ and FCTL is hard. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol. 2030, pp. 318–331. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

13. Laroussinie, F., Markey, N., Schnoebelen, P.: Efficient timed model checking for discrete-time systems. Theor. Comput. Sci. 353(1-3), 249–271 (2006)

    Article  MATH  MathSciNet  Google Scholar 

14. Laroussinie, F., Schnoebelen, P.: Specification in CTL+Past for verification in CTL. Inf. Comput. 156(1/2), 236–263 (2000)

    Article  MATH  MathSciNet  Google Scholar 

15. Laroussinie, F., Schnoebelen, P., Turuani, M.: On the expressivity and complexity of quantitative branching-time temporal logics. Theor. Comput. Sci. 297(1-3), 297–315 (2003)

    Article  MATH  MathSciNet  Google Scholar 

16. Pnueli, A.: The temporal logic of programs. In: Proc. 18th FOCS, pp. 46–57. IEEE Comp. Soc. Press, Los Alamitos (1977)

    Google Scholar 

17. Queille, J.-P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982)

    Google Scholar 

18. Wilke, T.: CTL⁺ is exponentially more succinct than CTL. In: Pandu Rangan, C., Raman, V., Sarukkai, S. (eds.) FST TCS 1999. LNCS, vol. 1738, pp. 110–121. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

19. Wolper, P.: Temporal logic can be more expressive. Inf. and Control 56(1/2), 72–99 (1983)

    Article  MATH  MathSciNet  Google Scholar 

20. Yang, J., Mok, A.K., Wang, F.: Symbolic model checking for event-driven real-time systems. ACM Transactions on Programming Languages and Systems 19(2), 386–412 (1997)

    Article  Google Scholar 

Download references