1: %%\documentclass[doublespacing]{elsart}

2: \documentclass[envcountsame,envcountchap]{svmono}

3: \usepackage{amsmath}

4: \usepackage{amssymb}

5: \usepackage{euscript}

6: \usepackage[latin1]{inputenc}

7: %%\usepackage{showkeys}

8: %%\usepackage{multirow}

9: %\usepackage[all]{xy}

10: %%\usepackage{stmaryrd}

11: %%\usepackage{tabularx}

12: %%\usepackage{verbatim}

13: %%\usepackage{ifthen}

14: \usepackage{pstricks,pst-plot}%,pstcol}

15: \usepackage{gastex}

16: \usepackage{url}

17: \usepackage{xspace}

18: %%\usepackage{multicol}

19: %%\usepackage[bottom]{footmisc} 

20: \usepackage{makeidx} 

21: %%\usepackage{showidx}

22: \usepackage{multind}

23: 

24: \makeindex{Gen}

25: \makeindex{Not}

26: 

27: 

28: 

29: 

30: 

31: 

32: \newcommand{\monoid}{\EuScript{M}}

33: \newcommand{\Nat}{\mathbb{N}}

34: \newcommand{\Real}{\mathbb{R}}

35: \newcommand{\Natomega}{\mathbb{N}_\omega}

36: \newcommand{\Q}{\mathbb{Q}}

37: \newcommand{\Z}{\mathbb{Z}}

38: \renewcommand{\D}{\EuScript{L}}

39: \newcommand{\M}{\EuScript{M}}

40: \newcommand{\N}{\EuScript{N}}

41: \renewcommand{\E}{\EuScript{E}}

42: \newcommand{\V}{\EuScript{V}}

43: \newcommand{\F}{\EuScript{F}}

44: \newcommand{\Y}{\EuScript{Y}}

45: \newcommand{\U}{\EuScript{U}}

46: \newcommand{\G}{\textbf{G}}

47: \renewcommand{\I}{\EuScript{I}}

48: \newcommand{\X}{\EuScript{X}}

49: \newcommand{\Gra}{\textbf{G}}

50: \newcommand{\C}{\EuScript{C}}

51: \newcommand{\RF}{\EuScript{RF}}

52: \newcommand{\Lan}{\EuScript{L}}

53: \newcommand{\Pa}{\EuScript{P}}

54: \newcommand{\LS}{\textbf{\textit{L}}}

55: \newcommand{\base}{b}

56: \newcommand{\Base}{B}

57: \newcommand{\cycle}{\textbf{CYCLE }}

58: \newcommand{\flatl}{\textbf{FLAT }}

59: \newcommand{\rat}{\textbf{RAT }}

60: \newcommand{\system}{\EuScript{S}}

61: \newcommand{\Hrond}{\EuScript{H}}

62: \renewcommand{\H}{\Hrond}

63: \newcommand{\partiefinie}{\EuScript{P}_f}

64: \newcommand{\x}{{\bf x}}

65: 

66: \newcommand{\classe}{\EuScript{C}}

67: \newcommand{\A}{\EuScript{A}}

68: 

69: \newcommand{\class}{\classe}

70: 

71: \renewcommand{\S}{\mathcal{S}}

72: 

73: \newcommand{\automaton}{\EuScript{A}}

74: \newcommand{\counterautomaton}{\EuScript{C}}

75: 

76: \newcommand{\T}{\EuScript{T}}

77: 

78: \newcommand{\setpath}{\EuScript{P}}

79: \newcommand{\basis}{\EuScript{B}}

80: \newcommand{\matriceset}{\EuScript{M}}

81: \newcommand{\generator}{\EuScript{G}}

82: \newcommand{\element}{\textbf{e}}

83: \newcommand{\unit}{\textbf{e}}

84: \newcommand{\closure}{\mathrm{closure}}

85: \newcommand{\binary}{\mathrm{binary}}

86: \newcommand{\used}{\mathrm{used}}

87: \newcommand{\supp}{\mathrm{supp}}

88: \newcommand{\size}{\mathrm{size}}

89: \newcommand{\length}{\mathrm{length}}

90: \newcommand{\nstates}{\mathrm{nstates}}

91: \newcommand{\gran}{\mathrm{gran}}

92: \newcommand{\aff}{\mathrm{aff}}

93: \newcommand{\vecspace}{\mathrm{vec}}

94: 

95: \newcommand{\bound}[2]{\textrm{bound}_{#1}(#2)}

96: 

97: \renewcommand{\vec}[1]{\overrightarrow{#1}}

98: \newcommand{\saff}{\mathrm{saff}}

99: \newcommand{\vecsaff}{\vec{\mathrm{saff}}}

100: \newcommand{\comp}{\mathrm{comp}}

101: \newcommand{\veccomp}{\vec{\mathrm{comp}}}

102: 

103: 

104: \newcommand{\Max}{\mathit{Max}}

105: \renewcommand{\min}{\mathrm{min}}

106: \newcommand{\crochet}[1]{\left\llbracket#1\right\rrbracket}

107: \newcommand{\abst}{\mathrm{abst}}

108: 

109: \newcommand{\bool}{\mathrm{Bool}}

110: 

111: \newcommand{\finiteset}[2]{\{#1,\ldots,#2\}}

112: \newcommand{\cardinal}[1]{|#1|}

113: \newcommand{\relation}{\mathcal{R}}

114: \newcommand{\pre}{\mathrm{Pre}}

115: \newcommand{\post}{\mathrm{Post}}

116: \newcommand{\partie}{\mathcal{P}}

117: \newcommand{\moins}{\backslash}

118: \newcommand{\difference}[2]{#1\moins#2}

119: \newcommand{\scalar}[2]{\left<#1,#2\right>}

120: 

121: 

122: 

123: \newcommand{\trex}{\textsc{TreX}\xspace}

124: \newcommand{\fast}{\textsc{Fast}\xspace}

125: \newcommand{\lash}{\textsc{Lash}\xspace}

126: \newcommand{\babylon}{\textsc{Babylon}\xspace}

127: \newcommand{\brain}{\textsc{Brain}\xspace}

128: \newcommand{\cslalv}{\textsc{CSL-ALV}\xspace}

129: \newcommand{\mona}{\textsc{Mona}\xspace}

130: \newcommand{\fmona}{\textsc{FMona}\xspace}

131: \newcommand{\omegatool}{\textsc{Omega}\xspace}

132: \newcommand{\lcs}{\textsc{Lcs}\xspace}

133: 

134: 

135: \newcommand{\norm}[2]{\left|\left|#2\right|\right|_{#1}}

136: 

137: 

138: \newcommand{\fo}[1]{\textrm{FO}\left(#1\right)}

139: 

140: 

141: \renewcommand{\gcd}[2]{\textrm{gcd}(#1,#2)}

142: 

143: 

144: \newcommand{\ind}{\rule{0.6cm}{0cm}}

145: 

146: \renewcommand{\P}{\EuScript{P}}

147: 

148: \newcommand{\group}{\textrm{group}}

149: \newcommand{\inv}{\textrm{inv}}

150: \newcommand{\serial}{\textrm{serialized}}

151: \newcommand{\sautomaton}{\textbf{A}}

152: \newcommand{\sgraph}{\textbf{G}}

153: 

154: 

155: \begin{document}

156: 

157: \author{Jérôme Leroux}

158: \title{Least Significant Digit First\\ Presburger Automata}

159: %%\subtitle{DRAFT. Please do not distribute, but contact the author for a version}  

160: \maketitle

161: 

162: \frontmatter%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

163: 

164: \include{dedic}

165: \include{pref}

166: 

167: \tableofcontents

168: \mainmatter

169: %%\index{test}

170: 

171: %%\include{chapter}

172: 

173: 

174: 

175: 

176: 

177: 

178: %% \ead{leroux@labri.fr}

179: %%  \begin{abstract}

180: %%    Since 1969 \cite{C-MST69,S-SMJ77}, we know that any Presburger-definable set \cite{P-PCM29} (a set of integer vectors satisfying a formula in the first-order additive theory of the integers) can be represented by a state-based symmbolic representation, called in this paper Finite Digit Vector Automata (FDVA). Efficient algorithms for manipulating these sets have been recently developed \cite{WB-ICALP00,BC-CAAP96}. However, the problem of deciding if a FDVA represents such a set, is a well-known hard problem first solved by Muchnik in 1991 \cite{M-PREPRINT91,M-TCS03, BHMV-BMS94} with a \emph{quadruply-exponential time} algorithm. In this paper, we show how to determine in \emph{polynomial time} whether a FDVA represents a Presburger-definable set, and we provide in this positive case a \emph{polynomial time} algorithm that constructs a Presburger-formula that defines the same set.

181: %%  \end{abstract}

182: %%  \begin{keyword}

183: %%    Presburger \sep Semi-linear \sep Arithmetic \sep Logic \sep Automaton

184: %%  \end{keyword}

185: 

186: %%\end{frontmatter}

187: 

188: 

189: \input{chapter.introduction}

190: \input{chapter.notations}

191: 

192: %%\index{notation}{test}

193: 

194: \part{Logic and Automata}

195: \input{chapter.DVA}

196: \input{chapter.modifyingDVA}

197: \input{chapter.expressiveness}

198: \input{chapter.examplesFDVA}

199: \input{chapter.reduction}

200: 

201: \part{Geometry}

202: \input{chapter.linearsets}

203: \input{chapter.semilinearsets}

204: \input{chapter.degenerate}

205: \input{chapter.polyhedrons}

206: \input{chapter.presburgerdecomposition}

207: 

208: \part{From Automata to Presburger Formulas}

209: \input{chapter.stronglyconnected}

210: \input{chapter.geometricalextraction}

211: \input{chapter.finalalgorithm}

212: 

213: 

214: %%\cleardoublepage

215: %%\input{section.untransient}

216: %%\cleardoublepage

217: %%\input{section.detectablepatterns}

218: %%\cleardoublepage

219: %%\input{section.terminal}

220: %%\cleardoublepage

221: 

222: %%\input{section.semiaffinehull}

223: %%\cleardoublepage

224: %%\input{section.invariantcomputation}

225: %%\cleardoublepage

226: %%\input{section.boundary}

227: %%\cleardoublepage

228: 

229: %%\input{section.algorithmfinal}

230: %%\cleardoublepage

231: 

232: 

233: \backmatter%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

234: %%\chapter{L'histoire}

235: %%

236: \begin{thebibliography}{BHMV94}

237: 

238: \bibitem[BC96]{BC-CAAP96}

239: Alexandre Boudet and Hubert Comon.

240: \newblock Diophantine equations, {Presburger} arithmetic and finite automata.

241: \newblock In {\em Proc.\ 21st Int.\ Coll.\ on Trees in Algebra and Programming

242:   (CAAP'96), Link{\"o}ping, Sweden, Apr.\ 1996}, volume 1059 of {\em Lecture

243:   Notes in Computer Science}, pages 30--43. Springer, 1996.

244: 

245: \bibitem[Ber77]{B-FOCS77}

246: Leonard Berman.

247: \newblock Precise bounds for {Presburger} arithmetic and the reals with

248:   addition: Preliminary report.

249: \newblock In {\em Proc.\ 18th IEEE Symp.\ Foundations of Computer Science

250:   (FOCS'77), Providence, RI, USA, Oct.-Nov.\ 1977}, pages 95--99, Providence,

251:   Rhode Island, 31 October--2 November 1977. IEEE.

252: 

253: \bibitem[BFL04]{BFL-TACAS04}

254: Sébastien Bardin, Alain Finkel, and J\'er\^ome Leroux.

255: \newblock Faster acceleration of counter automata.

256: \newblock In {\em Proc.\ 10th Int.\ Conf.\ Tools and Algorithms for the

257:   Construction and Analysis of Systems (TACAS'2004) Barcelona, Spain, Mar.\

258:   2004}, volume 2988 of {\em Lecture Notes in Computer Science}, pages

259:   576--590. Springer, 2004.

260: 

261: \bibitem[BFLP03]{BFLP-CAV03}

262: S\'ebastien Bardin, Alain Finkel, J\'er\^ome Leroux, and Laure Petrucci.

263: \newblock {FAST}: {F}ast {A}cceleration of {S}ymbolic {T}ransition systems.

264: \newblock In {\em Proc.\ 15th Int.\ Conf.\ Computer Aided Verification

265:   (CAV'2003), Boulder, CO, USA, July 2003}, volume 2725 of {\em Lecture Notes

266:   in Computer Science}, pages 118--121. Springer, 2003.

267: 

268: \bibitem[BGP99]{BGP-TOPLAS99}

269: Tevfik Bultan, Richard Gerber, and William Pugh.

270: \newblock Model-checking concurrent systems with unbounded integer variables:

271:   symbolic representations, approximations, and experimental results.

272: \newblock {\em ACM Transactions on Programming Languages and Systems},

273:   21(4):747--789, 1999.

274: 

275: \bibitem[BHMV94]{BHMV-BMS94}

276: Véronique Bruy{\`e}re, Georges Hansel, Christian Michaux, and Roger Villemaire.

277: \newblock Logic and $p$-recognizable sets of integers.

278: \newblock {\em Bull.\ Belg.\ Math.\ Soc.}, 1(2):191--238, March 1994.

279: 

280: \bibitem[Fas]{FAST}

281: \textsc{Fast} homepage.

282: \newblock \url{http://www.lsv.ens-cachan.fr/fast/}.

283: 

284: \bibitem[FO97]{FO-CONCUR97}

285: Laurent Fribourg and Hans Ols\'en.

286: \newblock Proving safety properties of infinite state systems by compilation

287:   into {Presburger} arithmetic.

288: \newblock In {\em Proc.\ 8th Int.\ Conf.\ Concurrency Theory (CONCUR'97),

289:   Warsaw, Poland, Jul.\ 1997}, volume 1243 of {\em Lecture Notes in Computer

290:   Science}, pages 213--227. Springer, 1997.

291: 

292: \bibitem[Fri00]{F-WFLP00}

293: Laurent Fribourg.

294: \newblock {Petri} nets, flat languages and linear arithmetic. {Invited

295:   lecture}.

296: \newblock In M.~Alpuente, editor, {\em Proc.\ 9th Int.\ Workshop.\ on

297:   Functional and Logic Programming (WFLP'2000), Benicassim, Spain, Sept.\

298:   2000}, pages 344--365, 2000.

299: \newblock Proceedings published as Ref.\ 2000.2039, Universidad Polit\'{e}cnica

300:   de Valencia, Spain.

301: 

302: \bibitem[GBD02]{GBD-FMCAD02}

303: Vijay Ganesh, Sergey Berezin, and David~L. Dill.

304: \newblock Deciding presburger arithmetic by model checking and comparisons with

305:   other methods.

306: \newblock In {\em Proc.\ 4th Int.\ Conf.\ Formal Methods in Computer Aided

307:   Design (FMCAD'02), Portland, OR, USA, nov.\ 2002}, volume 2517 of {\em

308:   Lecture Notes in Computer Science}, pages 171--186. Springer, 2002.

309: 

310: \bibitem[GS66]{GS-PACIF66}

311: Seymour Ginsburg and Edwin~H. Spanier.

312: \newblock Semigroups, {P}resburger formulas and languages.

313: \newblock {\em Pacific J.\ Math.}, 16(2):285--296, 1966.

314: 

315: \bibitem[Kla04]{K-LICS04}

316: Felix Klaedtke.

317: \newblock On the automata size for presburger arithmetic.

318: \newblock In {\em Proc. 19th Annual IEEE Symposium on Logic in Computer Science

319:   (LICS'04), Turku, Finland July 2004}, pages 110--119. IEEE Comp.\ Soc.\

320:   Press, 2004.

321: 

322: \bibitem[KMS02]{KMS-IJFCS02}

323: Nils Klarlund, A.~Møller, and M.~I. Schwartzbach.

324: \newblock {MONA} implementation secrets.

325: \newblock {\em Int.\ J.\ of Foundations Computer Science}, 13(4):571--586,

326:   2002.

327: 

328: \bibitem[Las]{LASH}

329: \textsc{Lash} homepage.

330: \newblock \url{http://www.montefiore.ulg.ac.be/~boigelot/research/lash/}.

331: 

332: \bibitem[Lat04]{L-LICS04}

333: Louis Latour.

334: \newblock From automata to formulas: Convex integer polyhedra.

335: \newblock In {\em Proc. 19th Annual IEEE Symposium on Logic in Computer Science

336:   (LICS'04), Turku, Finland July 2004}, pages 120--129. IEEE Comp.\ Soc.\

337:   Press, 2004.

338: 

339: \bibitem[Ler03]{L-THESE03}

340: J\'er\^ome Leroux.

341: \newblock {\em Algorithmique de la vérification des systèmes à compteurs.

342:   Approximation et accélération. Implémentation de l'outil Fast}.

343: \newblock PhD thesis, Ecole Normale Supérieure de Cachan, Laboratoire

344:   Sp\'ecification et V\'erification. CNRS UMR 8643, décembre 2003.

345: 

346: \bibitem[Ler04]{L-INFINITY03}

347: J\'er\^ome Leroux.

348: \newblock The affine hull of a binary automaton is computable in polynomial

349:   time.

350: \newblock In {\em Proc. 5th Int. Workshop on Verification of Infinite State

351:   Systems (INFINITY 2003), Marseille, France, Sep. 2003}, volume~98 of {\em

352:   Electronic Notes in Theor.\ Comp.\ Sci.}, pages 89--104. Elsevier Science,

353:   2004.

354: 

355: \bibitem[Lug04]{L-CIAA04}

356: Denis Lugiez.

357: \newblock From automata to semilinear sets: a solution for polyhedra and even

358:   more general sets.

359: \newblock In {\em Proc.\ 9th. Int. Conf. on Implementation and Application of

360:   Automata (CIAA'04), Queen's University, Kingston, Ontario, Canada, Jul.\

361:   2004}, volume 3317 of {\em Lecture Notes in Computer Science}, pages

362:   321--322. Springer, 2004.

363: 

364: \bibitem[Muc91]{M-PREPRINT91}

365: A.~Muchnik.

366: \newblock Definable criterion for definability in presburger arithmetic and its

367:   applications.

368: \newblock (in russian), preprint, Institute of new technologies, 1991.

369: 

370: \bibitem[Ome]{OMEGA}

371: \textsc{Omega} homepage.

372: \newblock \url{http://www.cs.umd.edu/projects/omega/}.

373: 

374: \bibitem[Pre29]{P-PCM29}

375: M.~Presburger.

376: \newblock Uber die volstandigkeit eines gewissen systems der arithmetik ganzer

377:   zahlen, in welchem die addition als einzige operation hervortritt.

378: \newblock In {\em C. R. 1er congres des Mathematiciens des pays slaves,

379:   Varsovie}, pages 92--101, 1929.

380: 

381: \bibitem[RV02]{RV-AMAST02}

382: Tatiana Rybina and Andrei Voronkov.

383: \newblock Brain: Backward reachability analysis with integers.

384: \newblock In {\em Proc.\ 9th Int.\ Conf.\ Algebraic Methodology and Software

385:   Technology (AMAST'2002), Saint-Gilles-les-Bains, Reunion Island, France,

386:   Sep.\ 2002}, volume 2422 of {\em Lecture Notes in Computer Science}, pages

387:   489--494. Springer, 2002.

388: 

389: \bibitem[Sch87]{S-87}

390: Alexander Schrijver.

391: \newblock {\em Theory of Linear and Integer Programming}.

392: \newblock John Wiley and Sons, New York, 1987.

393: 

394: \bibitem[Tau92]{T-92-maths}

395: Patrice Tauvel.

396: \newblock {\em Math\'ematiques g\'en\'erales pour l'agr\'egation}.

397: \newblock MASSON, Paris Milan Barcelone Bonn, 1992.

398: 

399: \bibitem[WB95]{WB-SAS95}

400: Pierre Wolper and Bernard Boigelot.

401: \newblock An automata-theoretic approach to {Presburger} arithmetic

402:   constraints.

403: \newblock In {\em Proc.\ 2nd Int.\ Symp.\ Static Analysis (SAS'95), Glasgow,

404:   UK, Sep.\ 1995}, volume 983 of {\em Lecture Notes in Computer Science}, pages

405:   21--32. Springer, 1995.

406: 

407: \bibitem[WB00]{WB-ICALP00}

408: Pierre Wolper and Bernard Boigelot.

409: \newblock On the construction of automata from linear arithmetic constraints.

410: \newblock In {\em Proc.\ 6th Int.\ Conf.\ Tools and Algorithms for the

411:   Construction and Analysis of Systems (TACAS'2000), Berlin, Germany,

412:   Mar.-Apr.\ 2000}, volume 1785 of {\em Lecture Notes in Computer Science},

413:   pages 1--19. Springer, 2000.

414: 

415: \end{thebibliography}

416: 

417: %%\bibliography{biblio-these}

418: %%\bibliographystyle{alpha}

419: \printindex{Gen}{Index}

420: \printindex{Not}{Notations}

421: 

422: 

423: %%\cleardoublepage

424: %%\printindex

425: \end{document}

426: %%%%%%%%%%%\input{section.modularspace}

427: %%%%%%%%%%%\cleardoublepage

428: