A Parametric Analysis of the State Explosion Problem in Model Checking

1. K. A. Abrahamson, R. G. Downey, and M. R. Fellows. Fixed-parameter tractability and completeness IV: On completeness for W[P] and PSPACE analogs. Annals of Pure and Applied Logic, 73(3):235–276, 1995.

   Article  MATH  MathSciNet  Google Scholar 

2. H. R. Andersen. Verification of Temporal Properties of Concurrent Systems. PhD thesis, Aarhus University, Denmark, June 1993.

   Google Scholar 

3. H. L. Bodlaender, R. G. Downey, M. R. Fellows, and H. T. Wareham. The parameterized complexity of sequence alignment and consensus. Theoretical Computer Science, 147(1–2):31–54, 1995.

   Article  MATH  MathSciNet  Google Scholar 

4. J. Bradfield and C. Stirling. Modal logics and mu-calculi: an introduction. In Handbook of Process Algebra, ch 4, pp 293–330. Elsevier Science, 2001.

   Google Scholar 

5. Liming Cai, Jianer Chen, R. G. Downey, and M. R. Fellows. On the parameterized complexity of short computation and factorization. Archive for Mathematical Logic, 36(4/5):321–337, 1997.

   Article  MATH  MathSciNet  Google Scholar 

6. M. Cesati. The Turing way to the parameterized intractability, September 2001. Submitted.

   Google Scholar 

7. E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 1999.

   Google Scholar 

8. R. G. Downey and M. R. Fellows. Parameterized Complexity. Springer, 1999.

   Google Scholar 

9. S. Demri, F. Laroussinie, and Ph. Schnoebelen. A parametric analysis of the state explosion problem in model checking. Research Report LSV-01-4, Lab. Specification and Verification, ENS de Cachan, France, Apr. 2001.

   Google Scholar 

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

    MathSciNet  Google Scholar 

11. J. Esparza. Decidability and complexity of Petri net problems — an introduction. In Advances in Petri Nets 1998, LNCS 1491, pp 374–428. Springer, 1998.

    Google Scholar 

12. R. J. van Glabbeek. The linear time — branching time spectrum I. In Handbook of Process Algebra, ch 1, pp 3–99. Elsevier Science, 2001.

    Google Scholar 

13. M. Grohe. Descriptive and parameterized complexity. In Computer Science Logic (CSL’99), LNCS 1683, pp 14–31. Springer, 1999.

    Chapter  Google Scholar 

14. M. Grohe, T. Schwentick, and L. Segoufin. When is the evaluation of conjunctive queries tractable? In 33rd ACM Symp. Theory of Computing (STOC’01), pp 657–666, 2001.

    Google Scholar 

15. D. Harel, O. Kupferman, and M. Y. Vardi. On the complexity of verifying concurrent transition systems. In Concurrency Theory (CONCUR’97), LNCS 1243, pp 258–272. Springer, 1997.

    Google Scholar 

16. L. Jategaonkar and A. R. Meyer. Deciding true concurrency equivalences on safe, finite nets. Theoretical Computer Science, 154(1):107–143, 1996.

    Article  MATH  MathSciNet  Google Scholar 

17. T. Kasai, A. Adachi, and S. Iwata. Classes of pebble games and complete problems. SIAM J. Comput., 8(4):574–586, 1979.

    Article  MATH  MathSciNet  Google Scholar 

18. P. C. Kanellakis and S. A. Smolka. CCS expressions, finite state processes and three problems of equivalence. Information and Computation, 86(1):43–68, 1990.

    Article  MATH  MathSciNet  Google Scholar 

19. O. Kupferman, M. Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. J. ACM, 47(2):312–360, 2000.

    Article  MATH  MathSciNet  Google Scholar 

20. O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In 12th ACM Symp. Principles of Programming Languages (POPL’85), pp 97–107, 1985.

    Google Scholar 

21. F. Laroussinie and Ph. Schnoebelen. The state explosion problem from trace to bisimulation equivalence. In Found. Software Science & Computation Structures (FOSSACS’2000), LNCS 1784, pp 192–207. Springer, 2000.

    Chapter  Google Scholar 

22. C. H. Papadimitriou and M. Yannakakis. On the complexity of database queries. J. Computer and System Sciences, 58(3):407–427, 1999.

    Article  MATH  MathSciNet  Google Scholar 

23. A. Rabinovich. Complexity of equivalence problems for concurrent systems of finite agents. Information and Computation, 139(2):111–129, 1997.

    Article  MATH  MathSciNet  Google Scholar 

24. A. Rabinovich. Symbolic model checking for μ-calculus requires exponential time. Theoretical Computer Science, 243(1–2):467–475, 2000.

    Article  MATH  MathSciNet  Google Scholar 

25. A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logics. J. ACM, 32(3):733–749, 1985.

    Article  MATH  MathSciNet  Google Scholar 

26. Z. Sawa and P. Jančar. P-hardness of equivalence testing on finite-state processes. In Current Trends in Theory and Practice of Informatics (SOFSEM’ 01), LNCS 2234, pp 326–335. Springer, 2001.

    Google Scholar 

27. H. T. Wareham. The parameterized complexity of intersection and composition operations on sets of finite-state automata. In Implementation & Application of Automata (CIAA’2000), LNCS 2088, pp 302–310. Springer, 2001.

    Chapter  Google Scholar 

Download references