Model Checking Succinct and Parametric One-Counter Automata

1. Arnold, A., Niwiński, D.: Rudiments of μ-calculus. Studies in Logic and the Foundations of Mathematics, vol. 146. North-Holland, Amsterdam (2001)

   Book  Google Scholar 

2. Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: Programs with lists are counter automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 517–531. Springer, Heidelberg (2006)

   Chapter  Google Scholar 

3. Bozga, M., Iosif, R., Lakhnech, Y.: Flat parametric counter automata. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 577–588. Springer, Heidelberg (2006)

   Chapter  Google Scholar 

4. Bozga, M., Iosif, R.: On decidability within the arithmetic of addition and divisibility. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 425–439. Springer, Heidelberg (2005)

   Google Scholar 

5. Cai, J.-Y., Furst, M.: PSPACE survives constant-width bottlenecks. International Journal of Foundations of Computer Science 2(1), 67–76 (1991)

   Article  MATH  MathSciNet  Google Scholar 

6. Chitic, C., Rosu, D.: On validation of xml streams using finite state machines. In: Proc. of WebDB, pp. 85–90. ACM, New York (2004)

   Chapter  Google Scholar 

7. Chiu, A., Davida, G., Litow, B.: Division in logspace-uniform \(\rm NC\sp 1\). Theoretical Informatics and Applications. Informatique Théorique et Applications 35(3), 259–275 (2001)

   Article  MATH  MathSciNet  Google Scholar 

8. Comon, H., Jurski, Y.: Multiple counters automata, safety analysis and presburger arithmetic. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, Springer, Heidelberg (1998)

   Chapter  Google Scholar 

9. Demri, S., Gascon, R.: The effects of bounding syntactic resources on Presburger LTL. Journal of Logic and Computation 19(6), 1541–1575 (2009)

   Article  MATH  MathSciNet  Google Scholar 

10. Göller, S., Haase, C., Ouaknine, J., Worrel, J.: Model checking succinct and parametric one-counter automata. Technical report, University of Bremen (2010), http://www.informatik.uni-bremen.de/tdki/research/papers/succ.pdf

11. Göller, S., Lohrey, M.: Branchning-time model checking of one-counter processes. Technical report, arXiv.org (2009), http://arxiv.org/abs/0909.1102

12. Göller, S., Lohrey, M.: Branchning-time model checking of one-counter processes. In: Proc. of STACS, IFIB Schloss Dagstuhl (2010)

    Google Scholar 

13. Haase, C., Kreutzer, S., Ouaknine, J., Worrell, J.: Reachability in parametric one-counter automata (2010) (submitted), http://www.comlab.ox.ac.uk/files/2833/iandc.pdf

14. Hertrampf, U., Lautemann, C., Schwentick, T., Vollmer, H., Wagner, K.W.: On the power of polynomial time bit-reductions. In: Proc. of CoCo, pp. 200–207. IEEE Computer Society Press, Los Alamitos (1993)

    Google Scholar 

15. Ibarra, O.H., Jiang, T., Trân, N., Wang, H.: New decidability results concerning two-way counter machines and applications. In: Lingas, A., Carlsson, S., Karlsson, R. (eds.) ICALP 1993. LNCS, vol. 700, pp. 313–324. Springer, Heidelberg (1993)

    Google Scholar 

16. Ibarra, O.H., Dang, Z.: On the solvability of a class of diophantine equations and applications. Theor. Comput. Sci. 352(1), 342–346 (2006)

    Article  MATH  MathSciNet  Google Scholar 

17. Jančar, P., Kučera, A., Moller, F., Sawa, Z.: DP lower bounds for equivalence-checking and model-checking of one-counter automata. Information Computation 188(1), 1–19 (2004)

    Article  MATH  Google Scholar 

18. Leroux, J., Sutre, G.: Flat counter automata almost everywhere! In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 489–503. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

19. Minsky, M.L.: Recursive unsolvability of Post’s problem of “tag” and other topics in theory of Turing machines. Annals of Mathematics. Second Series 74, 437–455 (1961)

    MathSciNet  Google Scholar 

20. Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)

    MATH  Google Scholar 

21. Serre, O.: Parity games played on transition graphs of one-counter processes. In: Aceto, L., Ingólfsdóttir, A. (eds.) FOSSACS 2006. LNCS, vol. 3921, pp. 337–351. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

22. Vollmer, H.: A generalized quantifier concept in computational complexity theory. Technical report, arXiv.org (1998), http://arxiv.org/abs/cs.CC/9809115

Download references