1: \begin{thebibliography}{}
2:
3: \bibitem[\protect\citeauthoryear{Bardin, Finkel, Leroux, and Petrucci}{Bardin
4: et~al\mbox{.}}{2003}]{FAST}
5: {\sc Bardin, S.}, {\sc Finkel, A.}, {\sc Leroux, J.}, {\sc and} {\sc Petrucci,
6: L.} 2003.
7: \newblock {FAST}: Fast accelereation of symbolic transition systems.
8: \newblock In {\em Proc.\@ of the 15th International Conference on Computer
9: Aided Verification (CAV'03)}. Lecture Notes in Computer Science, vol. 2725.
10: 118--121.
11:
12: \bibitem[\protect\citeauthoryear{Bartzis and Bultan}{Bartzis and
13: Bultan}{2003}]{Bartzis_Bultan.2003}
14: {\sc Bartzis, C.} {\sc and} {\sc Bultan, T.} 2003.
15: \newblock Efficient symbolic representations for arithmetic constraints in
16: verification.
17: \newblock {\em Int.\@ J.\@ Found.\@ Comput.\@ Sci.\@\/}~{\em 14,\/}~4,
18: 605--624.
19:
20: \bibitem[\protect\citeauthoryear{Berman}{Berman}{1980}]{Berman.1980}
21: {\sc Berman, L.} 1980.
22: \newblock The complexity of logical theories.
23: \newblock {\em Theor. Comput. Sci.\/}~{\em 11}, 71--77.
24:
25: \bibitem[\protect\citeauthoryear{Blumensath and Gr{\"a}del}{Blumensath and
26: Gr{\"a}del}{2000}]{Blumensath_Graedel.2000}
27: {\sc Blumensath, A.} {\sc and} {\sc Gr{\"a}del, E.} 2000.
28: \newblock Automatic structures.
29: \newblock In {\em Proc.\@ of the 15th Annual IEEE Symposium on Logic in
30: Computer Science (LICS'00)}. IEEE Computer Society Press, 51--62.
31:
32: \bibitem[\protect\citeauthoryear{Boigelot}{Boigelot}{1999}]{Boigelot.1999}
33: {\sc Boigelot, B.} 1999.
34: \newblock Symbolic methods for exploring infinite state spaces.
35: \newblock Ph.D. thesis, Facult{\'e} des Sciences Appliqu{\'e}es de
36: l'Universit{\'e} de Li{\`e}ge, Li{\`e}ge, Belgium.
37:
38: \bibitem[\protect\citeauthoryear{Boigelot, Jodogne, and Wolper}{Boigelot
39: et~al\mbox{.}}{2001}]{Boigelot_Jodogne_Wolper.2001}
40: {\sc Boigelot, B.}, {\sc Jodogne, S.}, {\sc and} {\sc Wolper, P.} 2001.
41: \newblock On the use of weak automata for deciding linear arithmetic with
42: integer and real variables.
43: \newblock In {\em Proc.\@ of the 1st International Joint Conference on
44: Automated Reasoning (IJCAR'01)}. Lecture Notes in Computer Science, vol.
45: 2083. 611--625.
46: \newblock To appear in the ACM Transactions on Computational Logic.
47:
48: \bibitem[\protect\citeauthoryear{Boigelot, Rassart, and Wolper}{Boigelot
49: et~al\mbox{.}}{1998}]{Boigelot_Rassart_Wolper.1998}
50: {\sc Boigelot, B.}, {\sc Rassart, S.}, {\sc and} {\sc Wolper, P.} 1998.
51: \newblock On the expressiveness of real and integer arithmetic automata
52: (extended abstract).
53: \newblock In {\em Proc.\@ of the 25th International Colloquium on Automata,
54: Languages and Programming (ICALP'98)}. Lecture Notes in Computer Science,
55: vol. 1443. 152--163.
56:
57: \bibitem[\protect\citeauthoryear{Boudet and Comon}{Boudet and
58: Comon}{1996}]{Boudet_Comon.1996}
59: {\sc Boudet, A.} {\sc and} {\sc Comon, H.} 1996.
60: \newblock Diophantine equations, {Presburger} arithmetic and finite automata.
61: \newblock In {\em Proc.\@ of the 21st International Colloquium on Trees in
62: Algebra and Programming (CAAP'96)}. Lecture Notes in Computer Science, vol.
63: 1059. 30--43.
64:
65: \bibitem[\protect\citeauthoryear{Bruy{\`e}re, Hansel, Michaux, and
66: Villemaire}{Bruy{\`e}re et~al\mbox{.}}{1994}]{Bruyere_etal.1994}
67: {\sc Bruy{\`e}re, V.}, {\sc Hansel, G.}, {\sc Michaux, C.}, {\sc and} {\sc
68: Villemaire, R.} 1994.
69: \newblock Logic and $p$-recognizable sets of integers.
70: \newblock {\em Bull. Belg. Math. Soc.\/}~{\em 1,\/}~2, 191--238.
71:
72: \bibitem[\protect\citeauthoryear{Brzozowski and Leiss}{Brzozowski and
73: Leiss}{1980}]{Brzozowski_Leiss.1980}
74: {\sc Brzozowski, J.~A.} {\sc and} {\sc Leiss, E.~L.} 1980.
75: \newblock On equations for regular languages, finite automata, and sequential
76: networks.
77: \newblock {\em Theor. Comput. Sci.\/}~{\em 10,\/}~1, 19--35.
78:
79: \bibitem[\protect\citeauthoryear{B{\"u}chi}{B{\"u}chi}{1960}]{Buechi.1960}
80: {\sc B{\"u}chi, J.} 1960.
81: \newblock Weak second-order arithmetic and finite automata.
82: \newblock {\em Z.\@ Math.\@ Logik Grundlagen Math.\@\/}~{\em 6}, 66--92.
83:
84: \bibitem[\protect\citeauthoryear{Chandra, Kozen, and Stockmeyer}{Chandra
85: et~al\mbox{.}}{1981}]{Chandra_Kozen_Stockmeyer.1981}
86: {\sc Chandra, A.~K.}, {\sc Kozen, D.}, {\sc and} {\sc Stockmeyer, L.~J.} 1981.
87: \newblock Alternation.
88: \newblock {\em J.\@ ACM\/}~{\em 28,\/}~1, 114--133.
89:
90: \bibitem[\protect\citeauthoryear{Cobham}{Cobham}{1969}]{Cobham.1969}
91: {\sc Cobham, A.} 1969.
92: \newblock On the base-dependence of sets of numbers recognizable by finite
93: automata.
94: \newblock {\em Math.\@ Syst.\@ Theory\/}~{\em 3}, 186--192.
95:
96: \bibitem[\protect\citeauthoryear{Cooper}{Cooper}{1972}]{Cooper.1972}
97: {\sc Cooper, D.} 1972.
98: \newblock Theorem proving in arithmetic without multiplication.
99: \newblock {\em Machine Intelligence\/}~{\em 7}, 91--99.
100:
101: \bibitem[\protect\citeauthoryear{Dixmier}{Dixmier}{1990}]{Dixmier.1990}
102: {\sc Dixmier, J.} 1990.
103: \newblock Proof of a conjecture by {Erd{\"o}s} and {Graham} concerning the
104: problem of {Frobenius}.
105: \newblock {\em J.\@ Number Theory\/}~{\em 34,\/}~2, 198--209.
106:
107: \bibitem[\protect\citeauthoryear{Ferrante and Rackoff}{Ferrante and
108: Rackoff}{1975}]{Ferrante_Rackoff.1975}
109: {\sc Ferrante, J.} {\sc and} {\sc Rackoff, C.~W.} 1975.
110: \newblock A decision procedure for the first order theory of real addition with
111: order.
112: \newblock {\em SIAM J. Comput.\/}~{\em 4,\/}~1, 69--76.
113:
114: \bibitem[\protect\citeauthoryear{Ferrante and Rackoff}{Ferrante and
115: Rackoff}{1979}]{Ferrante_Rackoff.1979}
116: {\sc Ferrante, J.} {\sc and} {\sc Rackoff, C.~W.} 1979.
117: \newblock {\em The Computational Complexity of Logical Theories}. Lecture Notes
118: in Mathematics, vol. 718.
119: \newblock Springer-Verlag.
120:
121: \bibitem[\protect\citeauthoryear{Fischer and Rabin}{Fischer and
122: Rabin}{1974}]{Fischer_Rabin.1974}
123: {\sc Fischer, M.} {\sc and} {\sc Rabin, M.} 1974.
124: \newblock Super-exponential complexity of {Presburger} arithmetic.
125: \newblock In {\em Symposium on Applied Mathematics}. SIAM-AMS Proceedings, vol.
126: {VII}. 27--41.
127:
128: \bibitem[\protect\citeauthoryear{Fischer and Rabin}{Fischer and
129: Rabin}{1998}]{Fischer_Rabin.1998}
130: {\sc Fischer, M.} {\sc and} {\sc Rabin, M.} 1998.
131: \newblock Super-exponential complexity of {Presburger} arithmetic.
132: \newblock In {\em Quantifier elimination and cylindrical algebraic
133: decomposition}, {B.~Caviness} {and} {J.~Johnson}, Eds. Texts and Monographs
134: in Symbolic Computation. Springer-Verlag, 122--135.
135: \newblock Reprint of the article~\cite{Fischer_Rabin.1974}.
136:
137: \bibitem[\protect\citeauthoryear{Ganesh, Berezin, and Dill}{Ganesh
138: et~al\mbox{.}}{2002}]{Ganesh_Berezin_Dill.2002}
139: {\sc Ganesh, V.}, {\sc Berezin, S.}, {\sc and} {\sc Dill, D.~L.} 2002.
140: \newblock Deciding {Presburger} arithmetic by model checking and comparisons
141: with other methods.
142: \newblock In {\em Proc.\@ of the 4th International Conference on Formal Methods
143: in Computer-Aided Design (FMCAD'02)}. Lecture Notes in Computer Science, vol.
144: 2517. 171--186.
145:
146: \bibitem[\protect\citeauthoryear{Gr{\"a}del}{Gr{\"a}del}{1988}]{Graedel.1988}
147: {\sc Gr{\"a}del, E.} 1988.
148: \newblock Subclasses of {Presburger} arithmetic and the polynomial-time
149: hierarchy.
150: \newblock {\em Theor. Comput. Sci.\/}~{\em 56}, 289--301.
151:
152: \bibitem[\protect\citeauthoryear{Khoussainov and Nerode}{Khoussainov and
153: Nerode}{1995}]{Khoussainov_Nerode.1994}
154: {\sc Khoussainov, B.} {\sc and} {\sc Nerode, A.} 1995.
155: \newblock Automatic presentations of structures.
156: \newblock In {\em Proc.\@ of the International Workshop on Logical and
157: Computational Complexity (LCC'94)}. Lecture Notes in Computer Science, vol.
158: 960. 367--392.
159:
160: \bibitem[\protect\citeauthoryear{{LASH}}{{LASH}}{}]{LASH}
161: {\sc {LASH}}.
162: \newblock {T}he {L}i{\`e}ge {A}utomata-based {S}ymbolic {H}andler.
163: \newblock See the web-page
164: \url{http://www.montefiore.ulg.ac.be/~boigelot/research/lash/}.
165:
166: \bibitem[\protect\citeauthoryear{Oppen}{Oppen}{1978}]{Oppen.1978}
167: {\sc Oppen, D.} 1978.
168: \newblock A $2^{2^{2^{pn}}}$ {\!\!\!}upper bound on the complexity of
169: {Presburger} arithmetic.
170: \newblock {\em J.\@ Comput.\@ Syst.\@ Sci.\@\/}~{\em 16}, 323--332.
171:
172: \bibitem[\protect\citeauthoryear{Presburger}{Presburger}{1930}]{Presburger.192%
173: 9}
174: {\sc Presburger, M.} 1930.
175: \newblock {\"U}ber die {V}ollst{\"a}ndigkeit eines gewissen {S}ystems der
176: {A}rithmetik ganzer {Z}ahlen, in welchem die {A}ddition als einzige
177: {O}peration hervortritt.
178: \newblock In {\em Sprawozdanie z I Kongresu metematyk{\'o}w slowia{\'n}skich,
179: Warszawa 1929}. 92--101 and 395.
180:
181: \bibitem[\protect\citeauthoryear{Reddy and Loveland}{Reddy and
182: Loveland}{1978}]{Reddy_Loveland.1978}
183: {\sc Reddy, C.} {\sc and} {\sc Loveland, D.~W.} 1978.
184: \newblock {Presburger} arithmetic with bounded quantifier alternation.
185: \newblock In {\em Proc.\@ of the 10th Annual ACM Symposium on Theory of
186: Computing (STOC'78)}. ACM Press, 320--325.
187:
188: \bibitem[\protect\citeauthoryear{Reinhardt}{Reinhardt}{2002}]{Reinhardt.2002}
189: {\sc Reinhardt, K.} 2002.
190: \newblock The complexity of translating logic to finite automata.
191: \newblock In {\em Automata, Logics, and Infinite Games}, {E.~Gr{\"a}del},
192: {W.~Thomas}, {and} {T.~Wilke}, Eds. Lecture Notes in Computer Science, vol.
193: 2500. Springer-Verlag, Chapter~13, 231--238.
194:
195: \bibitem[\protect\citeauthoryear{Rubin}{Rubin}{2004}]{Rubin.2004}
196: {\sc Rubin, S.} 2004.
197: \newblock Automatic structures.
198: \newblock Ph.D. thesis, University of Auckland, Auckland, New Zealand.
199:
200: \bibitem[\protect\citeauthoryear{Rybina and Voronkov}{Rybina and
201: Voronkov}{2001}]{Rybina_Voronkov.2001}
202: {\sc Rybina, T.} {\sc and} {\sc Voronkov, A.} 2001.
203: \newblock A decision procedure for term algebras with queues.
204: \newblock {\em ACM Trans. On Comp. Logic\/}~{\em 2,\/}~2, 155--181.
205:
206: \bibitem[\protect\citeauthoryear{Rybina and Voronkov}{Rybina and
207: Voronkov}{2003}]{Rybina_Voronkov.2003}
208: {\sc Rybina, T.} {\sc and} {\sc Voronkov, A.} 2003.
209: \newblock Upper bounds for a theory of queues.
210: \newblock In {\em Proc.\@ of the 30th International Colloquium on Automata,
211: Languages and Programming (ICALP'03)}. Lecture Notes in Computer Science,
212: vol. 2719. 714--724.
213:
214: \bibitem[\protect\citeauthoryear{Sch{\"o}ning}{Sch{\"o}ning}{1997}]{Schoening.%
215: 1997}
216: {\sc Sch{\"o}ning, U.} 1997.
217: \newblock Complexity of {Presburger} arithmetic with fixed quantifier
218: dimension.
219: \newblock {\em Theory Comput.\@ Syst.\@\/}~{\em 30,\/}~4, 423--428.
220:
221: \bibitem[\protect\citeauthoryear{Semenov}{Semenov}{1977}]{Semenov.1977}
222: {\sc Semenov, A.} 1977.
223: \newblock Presburgerness of predicates regular in two number systems.
224: \newblock {\em Sib. Math. J.\/}~{\em 18}, 289--300.
225:
226: \bibitem[\protect\citeauthoryear{Shiple, Kukula, and Ranjan}{Shiple
227: et~al\mbox{.}}{1998}]{Ranjan_Shiple_Kukula.1998}
228: {\sc Shiple, T.~R.}, {\sc Kukula, J.~H.}, {\sc and} {\sc Ranjan, R.~K.} 1998.
229: \newblock A comparison of {Presburger} engines for {EFSM} reachability.
230: \newblock In {\em Proc.\@ of the 10th International Conference on Computer
231: Aided Verification (CAV'98)}. Lecture Notes in Computer Science, vol. 1427.
232: 280--292.
233:
234: \bibitem[\protect\citeauthoryear{Skolem}{Skolem}{1931}]{Skolem.1931}
235: {\sc Skolem, T.} 1931.
236: \newblock {\"U}ber einige {S}atzfunktionen in der {A}rithmetik.
237: \newblock In {\em Skrifter utgitt av Det Norske Videnskaps-Akademi i Oslo, I.
238: Matematisk naturvidenskapelig klasse}. Vol.~7. Oslo, 1--28.
239:
240: \bibitem[\protect\citeauthoryear{Skolem}{Skolem}{1970}]{Skolem.1970}
241: {\sc Skolem, T.} 1970.
242: \newblock {\"U}ber einige {S}atzfunktionen in der {A}rithmetik.
243: \newblock In {\em Selected Works in Logic}, {J.~Fenstad}, Ed.
244: Universitetsforlaget, Oslo, 281--306.
245: \newblock Reprint of the article~\cite{Skolem.1931}.
246:
247: \bibitem[\protect\citeauthoryear{Stansifer}{Stansifer}{1984}]{Stansifer.1984}
248: {\sc Stansifer, R.} 1984.
249: \newblock Presburger's article on integer arithmetic: Remarks and translation.
250: \newblock Tech. Rep. TR84-639, Department of Computer Science, Cornell
251: University, Ithaca, NY, USA.
252:
253: \bibitem[\protect\citeauthoryear{Stockmeyer}{Stockmeyer}{1974}]{Stockmeyer.197%
254: 4}
255: {\sc Stockmeyer, L.} 1974.
256: \newblock The complexity of decision problems in automata theory and logic.
257: \newblock Ph.D. thesis, Department of Electrical Engineering, MIT, Boston, MA,
258: USA.
259:
260: \bibitem[\protect\citeauthoryear{Weispfenning}{Weispfenning}{1999}]{Weispfenni%
261: ng.1999}
262: {\sc Weispfenning, V.} 1999.
263: \newblock Mixed real-integer linear quantifier elimination.
264: \newblock In {\em Proc.\@ of the International Symposium on Symbolic and
265: Algebraic Computation (ISSAC'99)}. ACM Press, 129--136.
266:
267: \bibitem[\protect\citeauthoryear{Wolper and Boigelot}{Wolper and
268: Boigelot}{1995}]{Wolper_Boigelot.1995}
269: {\sc Wolper, P.} {\sc and} {\sc Boigelot, B.} 1995.
270: \newblock An automata-theoretic approach to {Presburger} arithmetic constraints
271: (extended abstract).
272: \newblock In {\em Proc.\@ of the 2nd International Symposium on Static Analysis
273: (SAS'95)}. Lecture Notes in Computer Science, vol. 983. 21--32.
274:
275: \bibitem[\protect\citeauthoryear{Wolper and Boigelot}{Wolper and
276: Boigelot}{2000}]{Wolper_Boigelot.2000}
277: {\sc Wolper, P.} {\sc and} {\sc Boigelot, B.} 2000.
278: \newblock On the construction of automata from linear arithmetic constraints.
279: \newblock In {\em Proc.\@ of the 6th International Conference on Tools and
280: Algorithms for Construction and Analysis of Systems (TACAS'00)}. Lecture
281: Notes in Computer Science, vol. 1785. 1--19.
282:
283: \bibitem[\protect\citeauthoryear{Yavuz-Kahveci, Bartzis, and
284: Bultan}{Yavuz-Kahveci et~al\mbox{.}}{2005}]{ALV}
285: {\sc Yavuz-Kahveci, T.}, {\sc Bartzis, C.}, {\sc and} {\sc Bultan, T.} 2005.
286: \newblock Action language verifier, extended.
287: \newblock In {\em Proc.\@ of the 17th International Conference on Computer
288: Aided Verification (CAV'05)}.
289: \newblock Accepted for publication.
290:
291: \end{thebibliography}
292: