Flat Parametric Counter Automata

• Autorzy: Bozga M. , Iosif R. , Lakhnech Y.
• Języki publikacji: EN

Abstrakty

EN

In this paper we study the reachability problem for parametric flat counter automata, in relation with the satisfiability problem of three fragments of integer arithmetic. The equivalence between non-parametric flat counter automata and Presburger arithmetic has been established previously by Comon and Jurski. We simplify their proof by introducing finite state automata defined over alphabets of a special kind of graphs (zigzags). This framework allows one to express also the reachability problem for parametric automata with one control loop as the satisfiability of a 1-parametric linear Diophantine systems. The latter problem is shown to be decidable, using a number-theoretic argument. In general, the reachability problem for parametric flat counter automata with more than one loops is shown to be undecidable, by reduction from Hilbert's Tenth Problem. Finally, we study the relation between flat counter automata, integer arithmetic, and another important class of computational devices, namely the 2-way reversal bounded counter machines.

Słowa kluczowe

EN

counter machines; reachability problems; diophantine systems

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2009
• Tom: Vol. 91, nr 2
• Strony: 275--303
• Opis fizyczny: Bibliogr. 22 poz., wykr.

Twórcy

autor

Bozga M.

autor

Iosif R.

autor

Lakhnech Y.

• Verimag, CNRS, Universit´e de Grenoble 2 Avenue de Vignate, 38610, Gieres, France,

Bibliografia

• [1] Annichini, A., Bouajjani, A., M. Sighireanu: TreX: A Tool for Reachability Analysis of Complex Systems, Proc.CAV, 2102, Springer, 2001.
• [2] Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: Fast Accelereation of Symbolic Transition systems, Proc. TACAS, 2725, Springer, 2004.
• [3] Boigelot, B.: On Iterating Linear Transformations over Recognizable Sets of Integers, TCS, 309(2), 2003, 413-468.
• [4] Church, A.: An unsolvable problem of elementary number theory, American Journal of Mathematics, 58, 1936, 345 - 363.
• [5] Comon, H., Jurski, Y.: Multiple Counters Automata, Safety Analysis and Presburger Arithmetic, Proc. CAV, 1427, Springer, 1998.
• [6] Dasdan, A., Irani, S., Gupta, R. K.: Efficient Algorithms for Optimum Cycle Mean and Optimum Cost to Time Ratio Problems, Design Automation Conference, 1999.
• [7] Finkel, A., Leroux, J.: How to compose Presburger-accelerations: Applications to broadcast protocols, Proc. FST&TCS, 2556, Springer, 2002.
• [8] Ginsburg, S., Spanier, E. H.: Semigroups, Presburger Formulas and Languages, Pacific Journal of Mathematics, 16(2), 1966, 285-296.
• [9] Gődel, K.: Über formal unentscheidbare Sätze der PrincipiaMathematica und verwandter Systeme I, Monatshefte für Mathematik und Physik, 38, 1931, 173 - 198.
• [10] Gurari, E. M., Ibarra, O. H.: Two-way CounterMachines and Diophantine Equations, Journal of the Association for Computing Machinery, 29(3), July 1982, 863-873.
• [11] Hilbert, D.: Mathematische Probleme. Vortrag, gehalten auf dem internationalen Mathematiker-Kongress zu Paris, Nachrichten von der Kőnigliche Gesellschaft der Wissenschaften zu Gőttingen, 1900.
• [12] Ibarra, O. H.: Reversal-BoundedMulticounter Machines and Their Decision Problems, Journal of the Association for Computing Machinery, 25(1), January 1978, 116 - 133.
• [13] Ibarra, O. H., Dang, Z.: On the Solvability of a Class of Diophantine Equations and Applications, Theoretical Computer Science, 352, 2006, 342 - 346.
• [14] Ibarra, O. H., Jiang, T., Tran, N., Wang, H.: New Decidability Results Concerning Two-way Counter Machines, SIAM J. Comput., 24(1), February 1995, 123-137.
• [15] Leroux, J., Sutre, G.: On flatness for 2-dimensional vector addition systems with states, Proc. CONCUR, 3170, Springer, 2004.
• [16] Matiyasevich, Y.: Enumerable Sets are Diophantine, Journal of Sovietic Mathematics, 11, 1970, 354 - 358.
• [17] Matiyasevich, Y.: Personal communication, 2005.
• [18] Minsky, M.: Computation: Finite and Infinite Machines, Prentice-Hall, 1967.
• [19] Pottier, L.: Solutionsminimales des systemes diophantiens lineaires: bornes et algorithmes, Technical Report 1292, INRIA Sophia Antipolis, 1990.
• [20] Presburger, M.: über die Vollstandigkeit eines gewissen Systems der Arithmetik, Comptes rendus du I Congrés des Pays Slaves, Warsaw 1929.
• [21] Rosser, B.: Extensions of some theorems of Gődel and Church, The Journal of Symbolic Logic, 1, 1936, 87 - 91.
• [22] Wolper, P., Boigelot, B.: Verifying Systemswith Infinite but Regular State Spaces, Proc. CAV, 1427, Springer, 1998.