Reachability in succinct and parametric one-counter automata. (English) Zbl 1254.68134
Bravetti, Mario (ed.) et al., CONCUR 2009 – concurrency theory. 20th international conference, CONCUR 2009, Bologna, Italy, September 1–4, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-04080-1/pbk). Lecture Notes in Computer Science 5710, 369-383 (2009).
Summary: One-counter automata are a fundamental and widely-studied class of infinite-state systems. In this paper we consider one-counter automata with counter updates encoded in binary-which we refer to as the succinct encoding. It is easily seen that the reachability problem for this class of machines is in PSpace and is NP-hard. One of the main results of this paper is to show that this problem is in fact in NP, and is thus NP-complete.
We also consider parametric one-counter automata, in which counter updates be integer-valued parameters. The reachability problem asks whether there are values for the parameters such that a final state can be reached from an initial state. Our second main result shows decidability of the reachability problem for parametric one-counter automata by reduction to existential Presburger arithmetic with divisibility.
For the entire collection see [Zbl 1173.68003].
We also consider parametric one-counter automata, in which counter updates be integer-valued parameters. The reachability problem asks whether there are values for the parameters such that a final state can be reached from an initial state. Our second main result shows decidability of the reachability problem for parametric one-counter automata by reduction to existential Presburger arithmetic with divisibility.
For the entire collection see [Zbl 1173.68003].
MSC:
| 68Q45 | Formal languages and automata |
| 68Q17 | Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) |
References:
| [1] | Abdulla, P.A., Cerans, K.: Simulation is decidable for one-counter nets. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 253–268. Springer, Heidelberg (1998) · Zbl 0940.68055 · doi:10.1007/BFb0055627 |
| [2] | Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: Proc. STOC 1993, pp. 592–601. ACM, New York (1993) · Zbl 1310.68139 |
| [3] | 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) · Zbl 1188.68181 · doi:10.1007/11817963_47 |
| [4] | 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) · Zbl 1134.68028 · doi:10.1007/11787006_49 |
| [5] | 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) · Zbl 0911.03006 · doi:10.1007/BFb0028751 |
| [6] | Cormen, T., Leiserson, C., Rivest, R.: Introduction to algorithms. MIT Press and McGraw-Hill (1990) · Zbl 1158.68538 |
| [7] | Demri, S.: Logiques pour la spécification et vérification. Mémoire d’habilitation, Université Paris 7 (2007) |
| [8] | Demri, S., Gascon, R.: The effects of bounding syntactic resources on Presburger LTL. In: Proc. TIME 2007. IEEE Computer Society Press, Los Alamitos (2007) · Zbl 1193.03033 |
| [9] | Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman & Co., New York (1979) · Zbl 0411.68039 |
| [10] | Ibarra, O.H., Dang, Z.: On two-way finite automata with monotonic counters and quadratic diophantine equations. Theor. Comput. Sci. 312(2-3), 359–378 (2004) · Zbl 1084.68062 · doi:10.1016/j.tcs.2003.10.027 |
| [11] | Ibarra, O.H., Dang, Z.: On the solvability of a class of diophantine equations and applications. Theor. Comput. Sci. 352(1), 342–346 (2006) · Zbl 1120.11017 · doi:10.1016/j.tcs.2005.12.001 |
| [12] | 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) · doi:10.1007/3-540-56939-1_82 |
| [13] | 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) · Zbl 1078.68087 · doi:10.1016/S0890-5401(03)00171-8 |
| [14] | Kučera, A.: Efficient verification algorithms for one-counter processes. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, p. 317. Springer, Heidelberg (2000) · Zbl 0973.68163 · doi:10.1007/3-540-45022-X_28 |
| [15] | Lafourcade, P., Lugiez, D., Treinen, R.: Intruder deduction for AC-like equational theories with homomorphisms. In: Research Report LSV-04-16. LSV, ENS de Cachan (2004) · Zbl 1078.68034 |
| [16] | 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) · Zbl 1170.68519 · doi:10.1007/11562948_36 |
| [17] | Lipshitz, L.: The diophantine problem for addition and divisibility. Transaction of the American Mathematical Society 235, 271–283 (1976) · Zbl 0374.02025 · doi:10.1090/S0002-9947-1978-0469886-1 |
| [18] | Mayr, E.W.: An algorithm for the general petri net reachability problem. In: Proc. STOC 1981, pp. 238–246. ACM, New York (1981) |
| [19] | Minsky, M.: Recursive unsolvability of post’s problem of ”tag” and other topics in theory of turing machines. Annals of Math. 74(3) (1961) · Zbl 0105.00802 · doi:10.2307/1970290 |
| [20] | Xie, G., Dang, Z., Ibarra, O.H.: A solvable class of quadratic diophantine equations with applications to verification of infinite-state systems. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 668–680. Springer, Heidelberg (2003) · Zbl 1039.68077 · doi:10.1007/3-540-45061-0_53 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
