1: \documentclass{llncs}

2: 

3: \usepackage{amsmath}

4: \usepackage{amssymb}

5: \usepackage{stmaryrd}

6: \usepackage{url}

7: \usepackage{enumerate}

8: 

9: %% Keywords.

10: \newcommand*{\kw}[1]{\mathop{\textup{\textbf{#1}}}}

11: \newcommand*{\arrayrange}[2]{\mathop{[{#1}\,.\,.\,{#2}]}}

12: 

13: %% Summaries for theorem-like environments

14: \newcommand{\summary}[1]{\textrm{\textbf{\textup{#1}}}}

15: \newcommand{\coacomment}[1]{\summary{#1}}

16: 

17: \newcommand{\bigO}{\mathop{\mathrm{O}}\nolimits}

18: \newcommand{\bigOmega}{\mathop{\mathrm{\Omega}}\nolimits}

19: \newcommand{\bigTheta}{\mathop{\mathrm{\Theta}}\nolimits}

20: 

21: %% Special letters denoting sets and algebras

22: \providecommand*{\Iset}{\mathbb{I}}            % An unspecified set.

23: \providecommand*{\Nset}{\mathbb{N}}            % Naturals

24: \providecommand*{\Zset}{\mathbb{Z}}            % Integers

25: \providecommand*{\Qset}{\mathbb{Q}}            % Rationals

26: \providecommand*{\Rset}{\mathbb{R}}            % Reals

27: \providecommand*{\nonnegRset}{\mathbb{R}_{\scriptscriptstyle{+}}}

28:                                                % Non-negative reals

29: \providecommand*{\CPset}{\mathbb{CP}}          % Closed polyhedra

30: \providecommand*{\Pset}{\mathbb{P}}            % (NNC) polyhedra

31: 

32: %% Calligraphic alphabet

33: \newcommand*{\cA}{\ensuremath{\mathcal{A}}}

34: \newcommand*{\cB}{\ensuremath{\mathcal{B}}}

35: \newcommand*{\cC}{\ensuremath{\mathcal{C}}}

36: \newcommand*{\cD}{\ensuremath{\mathcal{D}}}

37: \newcommand*{\cE}{\ensuremath{\mathcal{E}}}

38: \newcommand*{\cF}{\ensuremath{\mathcal{F}}}

39: \newcommand*{\cG}{\ensuremath{\mathcal{G}}}

40: \newcommand*{\cH}{\ensuremath{\mathcal{H}}}

41: \newcommand*{\cI}{\ensuremath{\mathcal{I}}}

42: \newcommand*{\cJ}{\ensuremath{\mathcal{J}}}

43: \newcommand*{\cK}{\ensuremath{\mathcal{K}}}

44: \newcommand*{\cL}{\ensuremath{\mathcal{L}}}

45: \newcommand*{\cM}{\ensuremath{\mathcal{M}}}

46: \newcommand*{\cN}{\ensuremath{\mathcal{N}}}

47: \newcommand*{\cO}{\ensuremath{\mathcal{O}}}

48: \newcommand*{\cP}{\ensuremath{\mathcal{P}}}

49: \newcommand*{\cQ}{\ensuremath{\mathcal{Q}}}

50: \newcommand*{\cR}{\ensuremath{\mathcal{R}}}

51: \newcommand*{\cS}{\ensuremath{\mathcal{S}}}

52: \newcommand*{\cT}{\ensuremath{\mathcal{T}}}

53: \newcommand*{\cU}{\ensuremath{\mathcal{U}}}

54: \newcommand*{\cV}{\ensuremath{\mathcal{V}}}

55: \newcommand*{\cW}{\ensuremath{\mathcal{W}}}

56: \newcommand*{\cX}{\ensuremath{\mathcal{X}}}

57: \newcommand*{\cY}{\ensuremath{\mathcal{Y}}}

58: \newcommand*{\cZ}{\ensuremath{\mathcal{Z}}}

59: 

60: %% mathrm alphabet

61: \newcommand*{\rA}{\ensuremath{\mathrm{A}}}

62: \newcommand*{\rB}{\ensuremath{\mathrm{B}}}

63: \newcommand*{\rC}{\ensuremath{\mathrm{C}}}

64: \newcommand*{\rc}{\ensuremath{\mathrm{c}}}

65: \newcommand*{\rD}{\ensuremath{\mathrm{D}}}

66: \newcommand*{\rE}{\ensuremath{\mathrm{E}}}

67: \newcommand*{\re}{\ensuremath{\mathrm{e}}}

68: \newcommand*{\rF}{\ensuremath{\mathrm{F}}}

69: \newcommand*{\rG}{\ensuremath{\mathrm{G}}}

70: \newcommand*{\rH}{\ensuremath{\mathrm{H}}}

71: \newcommand*{\rI}{\ensuremath{\mathrm{I}}}

72: \newcommand*{\rJ}{\ensuremath{\mathrm{J}}}

73: \newcommand*{\rK}{\ensuremath{\mathrm{K}}}

74: \newcommand*{\rL}{\ensuremath{\mathrm{L}}}

75: \newcommand*{\rM}{\ensuremath{\mathrm{M}}}

76: \newcommand*{\rN}{\ensuremath{\mathrm{N}}}

77: \newcommand*{\rO}{\ensuremath{\mathrm{O}}}

78: \newcommand*{\rP}{\ensuremath{\mathrm{P}}}

79: \newcommand*{\rQ}{\ensuremath{\mathrm{Q}}}

80: \newcommand*{\rR}{\ensuremath{\mathrm{R}}}

81: \newcommand*{\rr}{\ensuremath{\mathrm{r}}}

82: \newcommand*{\rS}{\ensuremath{\mathrm{S}}}

83: \newcommand*{\rs}{\ensuremath{\mathrm{s}}}

84: \newcommand*{\rT}{\ensuremath{\mathrm{T}}}

85: \newcommand*{\rt}{\ensuremath{\mathrm{t}}}

86: \newcommand*{\rU}{\ensuremath{\mathrm{U}}}

87: \newcommand*{\rV}{\ensuremath{\mathrm{V}}}

88: \newcommand*{\rW}{\ensuremath{\mathrm{W}}}

89: \newcommand*{\rX}{\ensuremath{\mathrm{X}}}

90: \newcommand*{\rY}{\ensuremath{\mathrm{Y}}}

91: \newcommand*{\rZ}{\ensuremath{\mathrm{Z}}}

92: 

93: %% lower uppercase mathrm (for subscripts to lowercase)

94: \newcommand*{\lowrS}{\text{\raisebox{-.2ex}{\rS}}}

95: \newcommand*{\lowrT}{\text{\raisebox{-.2ex}{\rT}}}

96: 

97: %% Set theory

98: 

99: \renewcommand{\emptyset}{\mathord{\varnothing}}

100: 

101: %% \newcommand*{\wpc}{\mathop{\wp_\mathrm{c}}\nolimits}

102: \newcommand*{\wpf}{\mathop{\wp_\mathrm{f}}\nolimits}

103: \newcommand*{\wpfn}{\mathop{\wp_\mathrm{fn}}\nolimits}

104: 

105: % subset and supset relations

106: \newcommand*{\sseq}{\subseteq}

107: \newcommand*{\sseqf}{\mathrel{\subseteq_\mathrm{f}}}

108: \newcommand*{\sslt}{\subset}

109: \newcommand*{\Sseq}{\supseteq}

110: \newcommand*{\Ssgt}{\supset}

111: \newcommand{\Nsseq}{\nsubseteq}

112: 

113: % square subset and supset relations

114: \newcommand*{\sqsseq}{\sqsubseteq}

115: \newcommand*{\sqsslt}{\sqsubset}

116: \newcommand*{\sqSseq}{\sqsupseteq}

117: \newcommand*{\sqSsgt}{\sqsupset}

118: \newcommand{\Nsqsseq}{\not\sqsubseteq}

119: 

120: \newcommand*{\union}{\cup}

121: \newcommand*{\bigunion}{\bigcup}

122: \newcommand*{\biginters}{\bigcap}

123: \newcommand*{\inters}{\cap}

124: \newcommand*{\setdiff}{\setminus}

125: 

126: \newcommand{\sset}[2]{{\renewcommand{\arraystretch}{1.2}

127:                       \left\{\,#1 \,\left|\,

128:                                \begin{array}{@{}l@{}}#2\end{array}

129:                       \right.   \,\right\}}}

130: 

131: %% Declarators for functions and relations

132: 

133: \newcommand*{\monoarrow}{\mathrel{\buildrel\mathrm{m}\over\longrightarrow}}

134: \newcommand*{\contarrow}{\mathrel{\buildrel\mathrm{c}\over\longrightarrow}}

135: 

136: \newcommand*{\reld}[3]{\mathord{#1}\subseteq#2\times#3}

137: \newcommand*{\fund}[3]{\mathord{#1}\colon#2\rightarrow#3}

138: \newcommand*{\monofund}[3]{\mathord{#1}\colon#2\monoarrow#3}

139: \newcommand*{\contfund}[3]{\mathord{#1}\colon#2\contarrow#3}

140: \newcommand*{\pard}[3]{\mathord{#1}\colon#2\rightarrowtail#3}

141: 

142: %% Logical quantifiers stuff

143: \newcommand{\st}{\mathrel{.}}

144: \newcommand{\itc}{\mathrel{:}}

145: 

146: %% Lambda notation

147: \newcommand{\lambdadot}{\mathbin{.}}

148: 

149: \spnewtheorem*{delayedproof}{Proof}{\bfseries}{\rmfamily}

150: 

151: % Generic widening

152: \newcommand*{\widen}{\mathbin{\nabla}}

153: \newcommand*{\hwiden}{\mathbin{\nabla_\mathrm{s}}}

154: 

155: %% Logic notation

156: \newcommand*{\entails}{\mathrel{\vdash}}

157: \newcommand*{\bigland}{\mathop{\bigwedge}}

158: \newcommand*{\biglor}{\mathop{\bigvee}}

159: \newcommand*{\piff}{\mathrel{\leftrightarrow}}

160: \newcommand*{\pimplies}{\mathrel{\rightarrow}}

161: \newcommand*{\pimplied}{\mathrel{\leftarrow}}

162: 

163: %% Things that hold by definition

164: \newcommand{\defrel}[1]{\mathrel{\buildrel \mathrm{def} \over {#1}}}

165: %\newcommand{\defeq}{\defrel{=}}

166: \newcommand{\defeq}{\mathrel{\mathord{:}\mathord{=}}}

167: \newcommand{\defiff}{\defrel{\Longleftrightarrow}}

168: %\newcommand{\defeq}{=}

169: %\newcommand{\defiff}{\Longleftrightarrow}

170: 

171: %% Domain and co-domain of a function

172: \newcommand*{\dom}{\mathop{\mathrm{dom}}\nolimits}

173: \newcommand*{\cod}{\mathop{\mathrm{cod}}\nolimits}

174: 

175: %% Composition of functions

176: \newcommand*{\compose}{\mathbin{\circ}}

177: 

178: \newcommand*{\coanote}[1]{\footnote{\textbf{For co-authors:} {#1}}}

179: %\newcommand*{\coanote}[1]{}

180: 

181: \newcommand{\card}{\mathop{\#}\nolimits}

182: \newcommand{\cardnf}{\mathop{\#_{\mathrm{nf}}}\nolimits}

183: \newcommand*{\Min}{\inplus}

184: 

185: %% Dimension of a polyhedron

186: \newcommand*{\pdim}{\mathop{\mathrm{dim}}\nolimits}

187: 

188: %% C++

189: \newcommand*{\Cplusplus}{{C\nolinebreak[4]\hspace{-.05em}\raisebox{.4ex}{\tiny\bf ++}}}

190: 

191: %% Assignment

192: 

193: \newcommand*{\takes}{\mathrel{:=}}

194: 

195: \newcommand*{\zero}{\mathbf{0}}

196: \newcommand*{\Vzero}{\cN_\zero}

197: %%\newcommand*{\Vpm}{\cN^\pm}

198: \newcommand*{\Vpm}{\cN}

199: 

200: \newcommand*{\length}[1]{\left\| #1 \right\|}

201: \newcommand{\pathconc}{\mathrel{::}}

202: 

203: \renewcommand*{\bar}[1]{\overline{#1}}

204: \newcommand*{\bari}{\overline{\imath}}

205: \newcommand*{\barj}{\overline{\jmath}}

206: \newcommand*{\barh}{\overline{h}}

207: \newcommand*{\bark}{\overline{k}}

208: \newcommand*{\barz}{\overline{z}}

209: 

210: \newcommand*{\Graphs}{\mathbb{G}}

211: \newcommand*{\ZGraphs}{\mathbb{G}^\Zset}

212: \newcommand*{\QGraphs}{\mathbb{G}^\Qset}

213: \newcommand*{\IGraphs}{\mathbb{G}^\Iset}

214: \newcommand*{\graphleq}{\unlhd}

215: \newcommand*{\graphlt}{\lhd}

216: \newcommand*{\graphglb}{\sqcap}

217: \newcommand*{\biggraphglb}{\bigsqcap}

218: \newcommand*{\graphlub}{\sqcup}

219: \newcommand*{\biggraphlub}{\bigsqcup}

220: \newcommand*{\Octgraphs}{\mathbb{O}}

221: \newcommand*{\ZOctgraphs}{\mathbb{O}^\Zset}

222: \newcommand*{\QOctgraphs}{\mathbb{O}^\Qset}

223: \newcommand*{\IOctgraphs}{\mathbb{O}^\Iset}

224: 

225: \newcommand*{\oct}{\mathop{\mathrm{oct}}\nolimits}

226: \newcommand*{\closure}{\mathop{\mathrm{closure}}\nolimits}

227: \newcommand*{\strongclosure}{\mathop{\text{\rm S-closure}}\nolimits}

228: \newcommand*{\tightclosure}{\mathop{\text{\rm T-closure}}\nolimits}

229: \newcommand*{\evenclosure}{\mathop{\text{\rm e-closure}}\nolimits}

230: 

231: \input prooftree

232: %% Uncomment this for page numbers.

233: \pagestyle{plain}

234: 

235: \begin{document}

236: 

237: \title{An Improved Tight Closure Algorithm\\

238:        for Integer Octagonal Constraints\thanks{This

239: work has been partly supported by MURST project

240: ``AIDA --- Abstract Interpretation: Design and Applications,''

241: and by a Royal Society (UK) International Joint Project (ESEP) award.}}

242: \author{Roberto Bagnara\inst{1}

243: \and Patricia M. Hill\inst{2}

244: \and Enea Zaffanella\inst{1}

245: }

246: \authorrunning{R.~Bagnara,

247:                P.~M.~Hill,

248:                E.~Zaffanella

249: }

250: \tocauthor{Roberto Bagnara (University of Parma),

251:            Patricia M. Hill (University of Leeds),

252:            Enea Zaffanella (University of Parma)

253: }

254: 

255: \institute{

256:     Department of Mathematics,

257:     University of Parma,

258:     Italy \\

259:     \email{\{bagnara,%

260:              zaffanella\}@cs.unipr.it}

261: \and

262:     School of Computing,

263:     University of Leeds,

264:     UK \\

265:     \email{hill@comp.leeds.ac.uk}

266: }

267: 

268: \maketitle

269: 

270: \begin{abstract}

271: Integer octagonal constraints

272: (a.k.a.\ \emph{Unit Two Variables Per Inequality} or

273: \emph{UTVPI integer constraints})

274: constitute an interesting class of constraints

275: for the representation and solution of integer problems

276: in the fields of constraint programming and formal analysis

277: and verification of software and hardware systems,

278: since they couple algorithms having polynomial complexity

279: with a relatively good expressive power.

280: The main algorithms required for the manipulation of such constraints

281: are the satisfiability check and the computation of the inferential

282: closure of a set of constraints.  The latter is called \emph{tight}

283: closure to mark the difference with the (incomplete) closure algorithm

284: that does not exploit the integrality of the variables.

285: In this paper we present and

286: fully justify an $\bigO(n^3)$ algorithm to compute the tight closure

287: of a set of UTVPI integer constraints.

288: \end{abstract}

289: 

290: \section{Introduction}

291: \label{sec:introduction}

292: 

293: \emph{Integer octagonal constraints}, also called

294: \emph{Unit Two Variables Per Inequality (UTVPI) integer constraints}

295: ---that is, constraints of the form $ax + by \leq d$

296: where $a, b \in \{-1, 0, +1\}$, $d \in \Zset$ and the variables $x$ and $y$

297: range over the integers---,

298: constitute an interesting subclass of linear integer constraints

299: admitting polynomial solvability.

300: The place these constraints occupy in the complexity/expressivity spectrum

301: is in fact peculiar.

302: Concerning complexity, relaxing the restriction imposing (at most)

303: two variables per constraint, or relaxing the restriction on coefficients,

304: or relaxing both restrictions make the satisfiability problem NP-complete

305: \cite{JaffarMSY94,Lagarias85b}.

306: Concerning expressivity, integer octagonal constraints can be used

307: for representing

308: and solving many integer problems in the field of constraint programming,

309: such as temporal reasoning and scheduling \cite{JaffarMSY94}.

310: In the field of formal analysis and verification of software and hardware

311: systems, these constraints have been successfully used in a number

312: of applications \cite{BalasundaramK89,BallCLZ04,CousotCFMMMR05,Mine05th}.

313: 

314: When (integer or rational) octagonal constraints are used to build

315: abstract domains\footnote{In \emph{abstract interpretation}

316: theory \cite{CousotC77}, an \emph{abstract domain} is an algebraic structure

317: formalizing  a set of approximate assertions endowed with an entailment

318: (or approximation) relation, plus various operations that correctly approximate

319: the operations of some \emph{concrete domain}, i.e., the domain being

320: abstracted/approximated.}

321: ---such as the \emph{Octagon Abstract Domain} implemented in the library

322: with the same name \cite{Mine06b} or the domain of \emph{octagonal shapes}

323: defined in \cite{BagnaraHMZ05} and implemented in the

324: \emph{Parma Polyhedra Library} \cite{BagnaraHZ06TR}---

325: the most critical operation is not the satisfiability check

326: (although very important in constraint programming)

327: but \emph{closure by entailment}.

328: This is the procedure whereby a set of octagonal constraints

329: is augmented with (a finite representation of) all the

330: octagonal constraints that can be inferred from it.

331: The closure algorithms for rational octagonal constraints are sound

332: but not complete for integer octagonal constraints.

333: The latter require so-called \emph{tight} closure algorithms that

334: fully exploit the integrality of the variables.

335: 

336: In 2005, Lahiri and Musuvathi proposed an $\bigO(n^3)$ algorithm for

337: the satisfiability check of a (non trivially redundant) system of

338: UTVPI integer constraints~\cite{LahiriM05}.  They also sketched

339: (without formal definitions and proofs) a tight closure algorithm with

340: the same worst-case complexity bound.

341: Still in 2005, Min\'e proposed a modification of

342: the strong (i.e., non-tight) closure algorithm for

343: \emph{rational} octagonal constraints

344: and argued that this would provide a good

345: and efficient approximation of tight closure~\cite{Mine01a}.

346: In the same year

347: we showed that the algorithm for computing

348: the strong closure of rational octagonal constraints

349: as described in~\cite{Mine01a}

350: could be simplified with a consequential improvement in its efficiency

351: \cite{BagnaraHMZ05,BagnaraHMZ05TR}.

352: In this paper we show that our result can be extended

353: so as to apply to integer octagonal constraints.

354: This enables us to present and, for the first time, fully justify an

355: $\bigO(n^3)$ algorithm to compute the tight closure of a set of UTVPI

356: integer constraints.

357: 

358: In Section~\ref{sec:preliminaries} we briefly introduce the terminology

359: and notation adopted throughout the paper and we recall a few

360: standard results on weighted graphs.

361: In Section~\ref{sec:octagonal-graph}, we give the definition

362: of rational-weighted octagonal graphs and recall some of the results that

363: were established in~\cite{BagnaraHMZ05,BagnaraHMZ05TR}.

364: In Section~\ref{sec:octagonal-Z-graph}, we extend these results

365: to the case of integer-weighted octagonal graphs.

366: Finally, in Section~\ref{sec:conclusion} we conclude and briefly

367: discuss future work.

368: 

369: \section{Preliminaries}

370: \label{sec:preliminaries}

371: 

372: Let $\Qset_\infty \defeq \Qset \union \{ +\infty \}$ be totally

373: ordered by the extension of `$\mathord{<}$' such that $d < +\infty$ for

374: each $d \in \Qset$.

375: Let $\cN$ be a finite set of \emph{nodes}.

376: A \emph{rational-weighted directed graph} (graph, for short)

377: $G$ in $\cN$ is a pair $(\cN, w)$,

378: where $\fund{w}{\cN \times \cN}{\Qset_\infty}$ is the

379: weight function for $G$.

380: 

381: Let $G = (\cN, w)$ be a graph.

382: A pair $(n_i, n_j) \in \cN \times \cN$ is an \emph{arc} of $G$

383: if $w(n_i,n_j) < +\infty$;

384: the arc is \emph{proper} if $n_i \neq n_j$.

385: %%

386: A \emph{path} $\pi = n_0 \cdots n_p$ in $G$

387: is a non-empty and finite sequence of nodes such that

388: $(n_{i-1}, n_i)$ is an arc of $G$, for all $i = 1$, \dots,~$p$.

389: Each node $n_i$ where  $i = 0$, \dots,~$p$ and

390: each arc $(n_{i-1}, n_i)$ where $i = 1$, \dots,~$p$

391: is said to be \emph{in} the path $\pi$.

392: %%

393: The \emph{length} of the path $\pi$ is the number $p$ of occurrences

394: of arcs in $\pi$ and denoted by $\length{\pi}$;

395: the \emph{weight} of the path $\pi$

396: is $\sum_{i=1}^p w(n_{i-1}, n_i)$ and denoted by $w(\pi)$.

397: %%

398: The path $\pi$ is \emph{simple} if each node occurs at most once in $\pi$.

399: %%

400: The path $\pi$ is \emph{proper} if all the arcs in it are proper.

401: The path $\pi$ is a \emph{proper cycle} if it is a proper path,

402: $n_0 = n_p$ and $p \geq 2$.

403: %%

404: If $\pi_1 = n_0 \cdots n_h$

405: and $\pi_2 = n_h \cdots n_p$ are paths,

406: where $0 \leq h \leq p$,

407: then the path concatenation $\pi = n_0 \cdots n_h \cdots n_p$ of

408: $\pi_1$ and $\pi_2$ is denoted by $\pi_1 \pathconc \pi_2$;

409: if $\pi_1 = n_0 n_1$ (so that $h = 1$),

410: then $\pi_1 \pathconc \pi_2$ will also be denoted by $n_0 \cdot \pi_2$.

411: Note that path concatenation is not the same as sequence concatenation.

412: %%

413: The path $\pi$ is a \emph{zero-cycle}

414: if it is a proper cycle and $w(\pi) = 0$.

415: A graph is \emph{zero-cycle free} if all its proper cycles

416: have strictly positive weights.

417: 

418: A graph $(\cN, w)$ can be interpreted to represent

419: the system of \emph{potential constraints}

420: \[

421:   \cC

422:     \defeq

423:       \bigl\{\,

424:         n_i - n_j \leq w(n_i, n_j)

425:       \bigm|

426:         n_i, n_j \in \cN

427:       \,\bigr\}.

428: \]

429: Hence, the graph $(\cN, w)$ is \emph{consistent}

430: if and only if

431: the system of constraints it represents is satisfiable in $\Qset$,

432: i.e., there exists a rational valuation

433: $\fund{\rho}{\cN}{\Qset}$ such that,

434: for each constraint $(n_i - n_j \leq d) \in \cC$,

435: the relation $\rho(n_i) - \rho(n_j) \leq d$ holds.

436: It is well-known that a graph is consistent

437: if and only if it has no negative weight cycles

438: (see \cite[Section 25.5]{CormenLR90} and \cite{Pratt77}).

439: 

440: The set of consistent graphs in $\cN$ is denoted by $\Graphs$.

441: This set is partially ordered by the relation

442: `$\mathord{\graphleq}$' defined,

443: for all $G_1 = (\cN, w_1)$ and $G_2 = (\cN, w_2)$, by

444: \[

445:   G_1 \graphleq G_2

446:     \quad\iff\quad

447:       \forall i, j \in \cN \itc w_1(i,j) \leq w_2(i,j).

448: \]

449: We write $G \graphlt G'$ when $G \graphleq G'$ and $G \neq G'$.

450: %%

451: When augmented with a bottom element $\bot$ representing inconsistency,

452: this partially ordered set becomes a non-complete lattice

453: \(

454:   \Graphs_\bot

455:     = \bigl\langle

456:         \Graphs \union \{ \bot \},

457:         \graphleq,

458:         \graphglb,

459:         \graphlub

460:       \bigr\rangle

461: \),

462: where `$\mathord{\graphglb}$' and `$\mathord{\graphlub}$'

463: denote the finitary greatest lower bound and least upper bound

464: operators, respectively.

465: 

466: \begin{definition}

467: \label{def:closure}

468: \summary{(Closed graph.)}

469: A consistent graph $G = (\cN, w)$ is \emph{closed}

470: if the following properties hold:

471: \begin{align}

472: \label{rule:zero-weight-self-loops}

473:   \forall i \in \cN

474:     &\itc w(i,i) = 0; \\

475: \label{rule:transitivity}

476:   \forall i,j,k \in \cN

477:     &\itc w(i,j) \leq w(i,k) + w(k,j).

478: \end{align}

479: The \emph{(shortest-path) closure} of a consistent graph $G$ in $\cN$ is

480: \[

481:   \closure(G)

482:     \defeq

483:       \biggraphlub

484:         \bigl\{\,

485:           G' \in \Graphs

486:         \bigm|

487:           \text{$G' \graphleq G$ and $G'$ is closed\/}

488:         \,\bigr\}.

489: \]

490: \end{definition}

491: %%

492: When trivially extended so as to behave as the identity function

493: on the bottom element $\bot$, shortest-path closure is a kernel operator

494: (monotonic, idempotent and reductive) on the lattice $\Graphs_\bot$,

495: therefore providing a canonical form.

496: 

497: The following lemma recalls a well-known result for closed graphs

498: (for a proof, see Lemma~5 in~\cite{BagnaraHMZ05TR}).

499: 

500: \begin{lemma}

501: \label{lem:trans-rule-star}

502: Let $G =(\cN, w) \in \Graphs$ be a closed graph.

503: Then, for any path $\pi = i \cdots j$ in $G$,

504: it holds that $w(i, j) \leq w(\pi)$.

505: \end{lemma}

506: 

507: \section{Rational Octagonal Graphs}

508: \label{sec:octagonal-graph}

509: 

510: We assume in the following that there is a fixed set

511: $\cV = \{ v_0, \ldots, v_{n-1} \}$ of $n$ variables.

512: The octagon abstract domain allows for the manipulation of

513: \emph{octagonal constraints}

514: of the form  $a v_i + b v_j \leq d$, where $a,b \in \{-1,0,+1\}$,

515: $a \neq 0$, $v_i,v_j \in \cV$, $v_i \neq v_j$ and $d \in \Qset$.

516: Octagonal constraints can be encoded using potential constraints

517: by splitting each variable $v_i$ into two forms:

518: a positive form $v_i^+$, interpreted as $+v_i$;

519: and a negative form $v_i^-$, interpreted as $-v_i$.

520: Then any octagonal constraint $a v_i + b v_j \leq d$ can be written

521: as a potential constraint $v - v' \leq d_0$

522: where $v, v' \in \{v_i^+, v_i^-, v_j^+, v_j^-\}$ and $d_0 \in \Qset$.

523: Namely, an octagonal constraint such as $v_i + v_j \leq d$ can be

524: translated into the potential constraint

525: $v_i^+ - v_j^- \leq d$; alternatively, the same octagonal constraint

526: can be translated into $v_j^+ - v_i^- \leq d$.

527: Furthermore, unary (octagonal) constraints such as

528: $v_i \leq d$ and $-v_i \leq d$

529: can be encoded as $v_i^+ - v_i^- \leq 2d$

530: and $v_i^- - v_i^+ \leq 2d$, respectively.

531: 

532: From now on, we assume that the set of nodes

533: is $\Vpm \defeq \{ 0, \ldots, 2n-1 \}$.

534: These will denote the positive and negative forms of the variables in $\cV$:

535: for all $i \in \Vpm$, if $i = 2k$, then

536: $i$ represents the positive form $v_k^+$ and, if $i = 2k+1$, then

537: $i$ represents the negative form $v_k^-$ of the variable $v_k$.

538: To simplify the presentation, for each $i \in \Vpm$,

539: we let $\bari$ denote $i+1$, if $i$ is even,

540: and $i-1$, if $i$ is odd, so that, for all $i \in \Vpm$, we also have

541: $\bari \in \Vpm$ and $\bar{\bari} = i$.

542: Then we can rewrite a potential constraint $v - v' \leq d$

543: where $v \in \{v_k^+, v_k^-\}$

544: and $v' \in \{v_l^+, v_l^-\}$

545: as the potential constraint $i - j \leq d$ in $\Vpm$ where, if

546: $v = v^+_k$, $i = 2k$ and, if $v = v^-_k$, $i = 2k+1$;

547: similarly, if

548: $v' = v^+_l$, $j = 2l$ and, if $v' = v^-_l$, $j = 2l+1$.

549: 

550: It follows from the above translations that

551: any finite system of octagonal constraints,

552: translated to a set of potential constraints in $\Vpm$ as above,

553: can be encoded by a graph $G$ in $\Vpm$.

554: In particular, any finite \emph{satisfiable} system

555: of octagonal constraints can be encoded by a \emph{consistent}

556: graph in $\Vpm$.

557: However, the converse does not hold

558: since in any valuation $\rho$ of an encoding of

559: a set of octagonal constraints

560: we must also have $\rho(i) = -\rho(\bari)$, so that

561: the arcs $(i,j)$ and $(\barj, \bari)$ should have the same weight.

562: %%

563: Therefore, to encode rational octagonal constraints,

564: we restrict attention to consistent graphs over $\Vpm$

565: where the arcs in all such pairs are \emph{coherent}.

566: 

567: \begin{definition}

568: \label{def:octagonal-graph}

569: \summary{(Octagonal graph.)}

570: A (rational) \emph{octagonal graph} is

571: any consistent graph $G =(\Vpm, w)$ that

572: satisfies the coherence assumption:

573: \begin{equation}

574: \label{rule:coherence}

575:   \forall i,j \in \Vpm

576:     \itc w(i,j) = w(\barj, \bari).

577: \end{equation}

578: \end{definition}

579: %%

580: The set $\Octgraphs$ of all octagonal graphs

581: (with the usual addition of the bottom element,

582: representing an unsatisfiable system of constraints)

583: is a sub-lattice of $\Graphs_\bot$, sharing the same

584: least upper bound and greatest lower bound operators.

585: %%

586: Note that, at the implementation level, coherence can be

587: automatically and efficiently enforced by letting arc $(i,j)$

588: and arc $(\barj, \bari)$ share the same representation.

589: 

590: When dealing with octagonal graphs, one has to remember

591: the relation linking the positive and negative forms of variables.

592: A proper closure by entailment procedure

593: should consider, besides transitivity, the following inference rule:

594: \begin{equation}

595: \label{eq:strong-coherence-inference-rule}

596:   \prooftree

597:     i - \bari \leq d_1

598:       \qquad

599:     \barj - j \leq d_2

600:   \justifies

601:     i - j \leq \frac{d_1 + d_2}{2}

602:   \endprooftree

603: \end{equation}

604: Thus, the standard shortest-path closure algorithm is not enough

605: to obtain a canonical form for octagonal graphs.

606: 

607: \begin{definition}

608: \label{def:strong-closure}

609: \summary{(Strongly closed graph.)}

610: An octagonal graph $G = (\Vpm, w)$ is \emph{strongly closed}

611: if it is closed and the following property holds:

612: \begin{equation}

613: \label{rule:strong-coherence}

614:   \forall i,j \in \Vpm

615:     \itc 2 w(i,j) \leq w(i, \bari) + w(\barj, j).

616: \end{equation}

617: The \emph{strong closure} of an octagonal graph $G$ in $\Vpm$ is

618: \[

619:   \strongclosure(G)

620:     \defeq

621:       \biggraphlub

622:         \bigl\{\,

623:           G' \in \Octgraphs

624:         \bigm|

625:           \text{$G' \graphleq G$ and $G'$ is strongly closed\/}

626:         \,\bigr\}.

627: \]

628: \end{definition}

629: %%

630: When trivially extended to the bottom element,

631: strong closure is a kernel operator on the lattice of octagonal graphs.

632: 

633: A modified closure procedure is defined in~\cite{Mine01b},

634: yielding strongly closed octagonal graphs.

635: A significant efficiency improvement can be obtained thanks to

636: the following theorem

637: (for a proof, see Theorem~2 in~\cite{BagnaraHMZ05TR}).

638: 

639: \begin{theorem}

640: \label{thm:one-step-strong-closure}

641: Let $G = (\Vpm, w)$ be a closed octagonal graph.

642: Consider the graph $G_\rS = (\Vpm, w_\lowrS)$,

643: where $w_\lowrS$ is defined, for each $i,j \in \Vpm$, by

644: \[

645:   w_\lowrS(i, j)

646:     \defeq

647:       \min

648:         \biggl\{

649:           w(i, j),

650:           \frac{w(i, \bari)}{2} + \frac{w(\barj, j)}{2}

651:         \biggr\}.

652: \]

653: Then $G_\rS = \strongclosure(G)$.

654: \end{theorem}

655: %%

656: Intuitively, the theorem states that strong closure can be obtained

657: by application of any shortest-path closure algorithm

658: followed by a \emph{single} local propagation step using the

659: constraint inference rule~\eqref{eq:strong-coherence-inference-rule}.

660: In contrast, in the strong closure algorithm of~\cite{Mine01b},

661: the outermost iterations of (a variant of) the Floyd-Warshall

662: shortest-path algorithm are interleaved with $n$ applications

663: of the inference rule~\eqref{eq:strong-coherence-inference-rule},

664: leading to a more complex and less efficient implementation.

665: 

666: 

667: \section{Integer Octagonal Graphs}

668: \label{sec:octagonal-Z-graph}

669: We now consider the case of integer octagonal constraints, i.e.,

670: octagonal constraints where the bounds are all integral and the variables

671: are only allowed to take integral values.

672: These can be encoded by suitably restricting the codomain of the

673: weight function of octagonal graphs.

674: 

675: \begin{definition}

676: \label{def:integer-octagonal-graph}

677: \summary{(Integer octagonal graph.)}

678: An \emph{integer octagonal graph} is an octagonal graph $G = (\Vpm, w)$

679: having an integral weight function:

680: \[

681:   \forall i,j \in \Vpm \itc w(i,j) \in \Zset \union \{+\infty\}.

682: \]

683: \end{definition}

684: 

685: As an integer octagonal graph is also a rational octagonal graph,

686: the constraint system it encodes

687: will be satisfiable when interpreted to take values in $\Qset$.

688: However, when interpreted to take values in $\Zset$,

689: this system may be unsatisfiable

690: since the arcs encoding unary constraints can have an odd weight;

691: we say that an octagonal graph is \emph{$\Zset$-consistent}

692: if its encoded integer constraint system is satisfiable.

693: For the same reason, the strong closure of an integer octagonal graph does

694: not provide a canonical form for the integer constraint system it encodes

695: and we need to consider the following \emph{tightening} inference rule:

696: %%

697: \begin{equation}

698: \label{eq:tightening-inference-rule}

699:   \prooftree

700:     i - \bari \leq d

701:   \justifies

702:     i - \bari \leq 2 \lfloor d/2 \rfloor

703:   \endprooftree.

704: \end{equation}

705: 

706: \begin{definition}

707: \label{def:tight-closure}

708: \summary{(Tightly closed graph.)}

709: An octagonal graph $G = (\Vpm, w)$ is \emph{tightly closed}

710: if it is a strongly closed integer octagonal graph

711: and the following property holds:

712: \begin{equation}

713: \label{rule:tight-coherence}

714:   \forall i \in \Vpm

715:     \itc \mathord{\text{$w(i, \bari)$ is even}}.

716: \end{equation}

717: The \emph{tight closure} of an octagonal graph $G$ in $\Vpm$ is

718: \[

719:   \tightclosure(G)

720:     \defeq

721:       \biggraphlub

722:         \bigl\{\,

723:           G' \in \Octgraphs

724:         \bigm|

725:           \text{$G' \graphleq G$ and $G'$ is tightly closed\/}

726:         \,\bigr\}.

727: \]

728: \end{definition}

729: 

730: By property \eqref{rule:tight-coherence},

731: any tightly closed integer octagonal graph

732: will encode a satisfiable integer constraint system

733: and is therefore $\Zset$-consistent.

734: Moreover, since the encoding of any satisfiable integer constraint system

735: will result in a $\Zset$-consistent integer octagonal graph $G$

736: that satisfies property \eqref{rule:tight-coherence},

737: its tight closure $\tightclosure(G)$ will also be $\Zset$-consistent.

738: This means that, if $G$ is \emph{not} $\Zset$-consistent,

739: then $\tightclosure(G) = \biggraphlub \emptyset = \bot$;

740: that is, the tight closure operator computes

741: either a tightly closed graph or the bottom element.

742: Therefore, tight closure is a kernel operator on the lattice of

743: octagonal graphs, as was the case for strong closure.

744: 

745: An incremental closure procedure for obtaining the tight closure of an

746: octagonal graph was defined in~\cite{JaffarMSY94} and improved

747: in~\cite{HarveyS97}.

748: The algorithm, which is also presented and discussed

749: in~\cite[Section~4.3.5]{Mine05th}, maintains the tight closure

750: of a system of octagonal constraints by performing at most

751: $\bigO(n^2)$ operations each time a new constraint is added:

752: thus, for $m$ constraints, the worst case complexity is $\bigO(m n^2)$.

753: In particular, for the case of a dense system of octagonal constraints

754: where $m \in \bigO(n^2)$, the worst case complexity is $\bigO(n^4)$.

755: 

756: The following theorem shows that a more efficient tight closure algorithm

757: can be obtained by a simple modification to the improved strong closure

758: algorithm of Theorem~\ref{thm:one-step-strong-closure}.

759: Basically,

760: inference rule~\eqref{eq:tightening-inference-rule}

761: must be applied to ensure property \eqref{rule:tight-coherence}

762: holds before applying

763: inference rule~\eqref{eq:strong-coherence-inference-rule}.

764: 

765: \begin{theorem}

766: \label{thm:one-step-tight-closure}

767: Let $G = (\Vpm, w)$ be a closed integer octagonal graph.

768: Consider the graph $G_\rT = (\Vpm, w_\lowrT)$,

769: where $w_\lowrT$ is defined, for each $i,j \in \Vpm$, by

770: \[

771:   w_\lowrT(i, j)

772:     \defeq

773:       \min

774:         \biggl\{

775:           w(i, j),

776:           \Bigl\lfloor \frac{w(i, \bari)}{2} \Bigr\rfloor

777:             + \Bigl\lfloor \frac{w(\barj, j)}{2} \Bigr\rfloor

778:         \biggr\}.

779: \]

780: Then, if $G_\rT$ is an octagonal graph, $G_\rT = \tightclosure(G)$.

781: \end{theorem}

782: 

783: \begin{figure}

784: \begin{align*}

785: & \kw{procedure} \;

786:     \texttt{tight\_closure\_if\_consistent}

787:       (\kw{var} \; w\arrayrange{0}{2n-1}\arrayrange{0}{2n-1}) \\

788: & \qquad

789:   \{ \text{ Classical Floyd-Warshall: $\bigO(n^3)$ } \} \\

790: & \qquad

791:     \kw{for} \; k := 0 \; \kw{to} \; 2n-1 \; \kw{do} \\

792: & \qquad\qquad

793:     \kw{for} \; i := 0 \; \kw{to} \; 2n-1 \; \kw{do} \\

794: & \qquad\qquad\qquad

795:       \kw{for} \; j := 0 \; \kw{to} \; 2n-1 \; \kw{do} \\

796: & \qquad\qquad\qquad\qquad

797:         w[i,j] := \min\bigl(

798:                         w[i,j],

799:                         w[i,k] + w[k,j]

800:                       \bigr); \\

801: & \qquad

802:   \{ \text{ Tight coherence: $\bigO(n^2)$ } \} \\

803: & \qquad

804:   \kw{for} \; i := 0 \; \kw{to} \; 2n-1 \; \kw{do} \\

805: & \qquad\qquad

806:     \kw{for} \; j := 0 \; \kw{to} \; 2n-1 \; \kw{do} \\

807: & \qquad\qquad\qquad

808:       w[i,j] := \min\Bigl(

809:                       w[i,j],

810:                       \mathrm{floor}\bigl(w[i,\bari]/2\bigr)

811:                         + \mathrm{floor}\bigl(w[\barj,j]/2\bigr)

812:                     \Bigr);

813: \end{align*}

814: \caption{A $\bigO(n^3)$ tight closure algorithm for $\Zset$-consistent

815: integer octagonal graphs}

816: \label{fig:consistent-tight-closure}

817: \end{figure}

818: Figure~\ref{fig:consistent-tight-closure}

819: shows the pseudo-code for a $\bigO(n^3)$ tight closure algorithm

820: based on Theorem~\ref{thm:one-step-tight-closure} and

821: on the classical Floyd-Warshall shortest-path closure algorithm.

822: Note that the pseudo-code in Figure~\ref{fig:consistent-tight-closure}

823: assumes that the data structure recording the weight function $w$,

824: here denoted to be similar to a bidimensional array,

825: automatically implements the coherence assumption for octagonal graphs

826: (i.e., property~\eqref{rule:coherence}

827: of Definition~\ref{def:octagonal-graph}).

828: 

829: In the case of sparse graphs, a better complexity bound can be

830: obtained by modifying the code in Figure~\ref{fig:consistent-tight-closure}

831: so as to compute the shortest path closure

832: using Johnson's algorithm~\cite{CormenLR90}:

833: the worst case complexity of such an implementation will be

834: $\bigO(n^2 \log n + mn)$,

835: which significantly improves upon the $\bigO(mn^2)$

836: worst case complexity of~\cite{HarveyS97,JaffarMSY94}

837: when, e.g., $m \in \bigTheta(n)$.

838: %%

839: However, as observed elsewhere~\cite{Mine05th,VenetB04},

840: some of the targeted applications (e.g., static analysis)

841: typically require the computation of graphs that are dense,

842: so that the Floyd-Warshall algorithm is often a better choice

843: from a practical perspective.

844: 

845: It is possible to define an incremental variant of the tight closure

846: algorithm in Figure~\ref{fig:consistent-tight-closure}, which is simply

847: based on the corresponding incremental version of the Floyd-Warshall

848: shortest path closure algorithm. In such a case, we obtain the same

849: worst case complexity of~\cite{HarveyS97,JaffarMSY94}.

850: 

851: 

852: The proof of Theorem~\ref{thm:one-step-tight-closure}

853: relies on a few auxiliary lemmas.

854: %%

855: The first two were also used in~\cite{BagnaraHMZ05TR}

856: for the formal proof of Theorem~\ref{thm:one-step-strong-closure} above

857: (for their detailed proofs, see Lemmas~9 and 10 in~\cite{BagnaraHMZ05TR}).

858: 

859: \begin{lemma}

860: \label{lem:ijarc-octagonal->closed}

861: Let $G =(\Vpm, w)$ be an octagonal graph,

862: $G^\star = (\Vpm, w^\star) \defeq \closure(G)$

863: and $(z_1, z_2)$ be an arc in $G^\star$.

864: Then there exists a simple path

865: $\pi = z_1 \cdots z_2$ in $G$ such that

866: $w^\star(z_1, z_2) = w(\pi)$.

867: \end{lemma}

868: 

869: \begin{lemma}

870: \label{lem:closed->1-step-strong-coherence}

871: Let $G =(\Vpm, w)$ be a closed octagonal graph and

872: $i, j \in \Vpm$ be such that $i \neq \barj$ and

873: $2 w(i, j) \geq w(i, \bari) + w(\barj, j)$.

874: %

875: Let $G_\rs^\star = (\Vpm, w_\rs^\star) \defeq \closure(G_\rs)$

876: where $G_\rs \defeq (\Vpm, w_\rs)$ and, for each $h_1, h_2 \in \Vpm$,

877: \begin{align*}

878:   w_\rs(h_1, h_2)

879:     &\defeq

880:       \begin{cases}

881:         \bigl(w(i, \bari) + w(\barj, j)\bigr)/2,

882:           &\text{if \(

883:                       (h_1, h_2)

884:                         \in \bigl\{ (i, j), (\barj, \bari) \bigr\}

885:                     \);} \\

886:         w(h_1, h_2),

887:           &\text{otherwise.}

888:       \end{cases}

889: \end{align*}

890: Let also $z_1, z_2 \in \Vpm$.

891: Then one or both of the following hold:

892: \begin{align*}

893:   w_\rs^\star(z_1, z_2)

894:     &= w(z_1, z_2); \\

895:   2 w_\rs^\star(z_1, z_2)

896:     &\geq w(z_1, \barz_1) + w(\barz_2, z_2).

897: \end{align*}

898: \end{lemma}

899: %%

900: Informally, Lemma~\ref{lem:closed->1-step-strong-coherence}

901: states that if inference rule~\eqref{eq:strong-coherence-inference-rule}

902: is applied

903: to a closed octagonal graph, then the resulting graph

904:  can be closed just by making further

905: applications of inference rule~\eqref{eq:strong-coherence-inference-rule}.

906: %%

907: Note that, if $G$ is an integer octagonal graph

908: and property \eqref{rule:tight-coherence} holds,

909: then the derived graph $G_\rs$ will also be an integer octagonal graph.

910: %%

911: We now state a new lemma for integer octagonal graphs showing that when

912: inference rule~\eqref{eq:tightening-inference-rule} is applied we

913: obtain a similar conclusion to that for

914: Lemma~\ref{lem:closed->1-step-strong-coherence}.

915: 

916: \begin{lemma}

917: \label{lem:closed->1-step-tight-coherence}

918: Let $G =(\Vpm, w)$ be a closed integer octagonal graph

919: and $i \in \Vpm$.

920: %

921: Let $G_\rt^\star \defeq \closure(G_\rt)$

922: where $G_\rt \defeq (\Vpm, w_\rt)$ is an octagonal graph

923: and, for each $h_1, h_2 \in \Vpm$,

924: \begin{align}

925: \label{eq:closed->1-step-tight-coherence:os-def}

926:   w_\rt(h_1, h_2)

927:     &\defeq

928:       \begin{cases}

929:         w(i, \bari) -1,

930:           &\text{if $(h_1, h_2) = (i, \bari)$;} \\

931:         w(h_1, h_2),

932:           &\text{otherwise.}

933:       \end{cases}

934: \end{align}

935: Let $G_\rt^\star = (\Vpm, w_\rt^\star)$

936: and $z_1, z_2 \in \Vpm$.

937: Then one or both of the following hold:

938: \begin{align}

939: \label{eq:closed->1-step-tight-coherence:simple-eq}

940:   w_\rt^\star(z_1, z_2)

941:     &= w(z_1, z_2), \\

942: \label{eq:closed->1-step-tight-coherence:tight-coherence-ineq}

943:   w_\rt^\star(z_1, z_2)

944:     &\geq

945:       \Bigl\lfloor \frac{w(z_1, \barz_1)}{2} \Bigr\rfloor

946:         + \Bigl\lfloor \frac{w(\barz_2, z_2)}{2} \Bigr\rfloor.

947: \end{align}

948: \end{lemma}

949: \begin{proof}

950: By hypothesis and Definition~\ref{def:closure},

951: $G_\rt^\star \graphleq G_\rt \graphleq G$.

952: %%

953: If $(z_1, z_2)$ is not an arc in $G_\rt^\star$,

954: then $w_\rt^\star(z_1, z_2) = +\infty$;

955: thus, as $G_\rt^\star \graphleq G$, we also have

956: $w(z_1, z_2) = +\infty$

957: and hence property~\eqref{eq:closed->1-step-tight-coherence:simple-eq} holds.

958: %%

959: Suppose now that $(z_1, z_2)$ is an arc in $G_\rt^\star$.

960: Then we can apply Lemma~\ref{lem:ijarc-octagonal->closed},

961: so that there exists a simple path

962: $\pi = z_1 \cdots z_2$ in $G_\rt$ such that

963: $w_\rt^\star(z_1, z_2) = w_\rt(\pi)$.

964: 

965: Suppose first that $w_\rt(\pi) = w(\pi)$.

966: Then, as $G$ is closed,

967: by Lemma~\ref{lem:trans-rule-star} we obtain

968: $w(\pi) \geq w(z_1, z_2)$

969: so that $w_\rt^\star(z_1, z_2) \geq w(z_1, z_2)$.

970: However $G_\rt^\star \graphleq G$ so that

971: $w_\rt^\star(z_1, z_2) \leq w(z_1, z_2)$ and therefore

972: property~\eqref{eq:closed->1-step-tight-coherence:simple-eq} holds.

973: 

974: 

975: Secondly, suppose that $w_\rt(\pi) \neq w(\pi)$.

976: %

977: Then, by Equation~\eqref{eq:closed->1-step-tight-coherence:os-def},

978: $(i, \bari)$ must be an arc in $\pi$, so that

979: \begin{equation}

980: \label{eq:closed->1-step-tight-coherence:only-ij}

981:   \pi = \pi_1 \pathconc (i \, \bari) \pathconc \pi_2,

982: \end{equation}

983: where

984: $\pi_1 = z_1 \cdots i$,

985: $\pi_2 = j \cdots z_2$

986: are simple paths in $G_\rt$ that do not contain the arc $(i, \bari)$.

987: Therefore,

988: by Equation~\eqref{eq:closed->1-step-tight-coherence:os-def},

989: we have $w_\rt(\pi_1) = w(\pi_1)$, $w_\rt(\pi_2) = w(\pi_2)$.

990: 

991: Consider~\eqref{eq:closed->1-step-tight-coherence:only-ij} and let%

992: \footnote{%

993: If $\pi = j_0 \cdots j_p$ is a path in a graph in $\Vpm$,

994: then $\bar{\pi}$ denotes the path $\barj_p \cdots \barj_0$.}

995: \begin{align*}

996:   \pi_1' &= \pi_1 \pathconc (i \, \bari) \pathconc \bar{\pi}_1,

997:   &\pi_2' &= \bar{\pi}_2 \pathconc (i \, \bari) \pathconc \pi_2. \\

998: \intertext{%

999: As $G$ is an octagonal graph, we have

1000: $w(\pi_1) = w(\bar{\pi}_1)$

1001: and $w(\pi_2) = w(\bar{\pi}_2)$ so that

1002: }

1003:   w(\pi_1') &= 2 w(\pi_1) + w(i, \bari),

1004:   &w(\pi_2') &= 2 w(\pi_2) + w(i, \bari).\\

1005: \intertext{%

1006: As $G$ is closed, by Lemma~\ref{lem:trans-rule-star},

1007: }

1008:   w(\pi_1') &\geq w(z_1, \barz_1),

1009:   &w(\pi_2') &\geq w(\barz_2, z_2)

1010: \intertext{%

1011: so that

1012: }

1013:   w(\pi_1) + \frac{w(i, \bari)}{2}

1014:     &\geq

1015:       \frac{w(z_1, \barz_1)}{2},

1016:   &w(\pi_2) + \frac{w(i, \bari)}{2}

1017:     &\geq

1018:       \frac{w(\barz_2, z_2)}{2}.

1019: \end{align*}

1020: Therefore

1021: \begin{align*}

1022:   w_\rt(\pi)

1023:     &= w_\rt(\pi_1) + w_\rt(i, \bari) + w_\rt(\pi_2) \\

1024:     &= w(\pi_1) + \frac{w(i, \bari) - 1}{2}

1025:          + w(\pi_2) + \frac{w(i, \bari) - 1}{2} \\

1026:     &\geq

1027:       \frac{w(z_1, \barz_1)}{2} - \frac{1}{2}

1028:         + \frac{w(\barz_2, z_2)}{2} - \frac{1}{2} \\

1029:     &\geq

1030:       \Bigl\lfloor \frac{w(z_1, \barz_1)}{2} \Bigr\rfloor

1031:         + \Bigl\lfloor \frac{w(\barz_2, z_2)}{2} \Bigr\rfloor.

1032: \end{align*}

1033: Hence, as $w_\rt^\star(z_1, z_2) = w_\rt(\pi)$, we obtain

1034: property~\eqref{eq:closed->1-step-tight-coherence:tight-coherence-ineq},

1035: as required.

1036: \qed

1037: \end{proof}

1038: 

1039: The next result, uses Lemmas~\ref{lem:closed->1-step-strong-coherence}

1040: and~\ref{lem:closed->1-step-tight-coherence} to derive a property relating the weight

1041: functions for a closed integer octagonal graph and its tight closure.

1042: 

1043: \begin{lemma}

1044: \label{lem:ijarc-closed->tightclosed}

1045: Let $G =(\Vpm, w)$ be a closed integer octagonal graph

1046: such that $G^\rT = (\Vpm, w^\rT) \defeq \tightclosure(G)$

1047: is an octagonal graph and let $z_1, z_2 \in \Vpm$.

1048: Then one or both of the following hold:

1049: \begin{align}

1050: \label{eq:ijarc-closed->tightclosed:simple-eq}

1051:   w^\rT(z_1, z_2)

1052:     &= w(z_1, z_2); \\

1053: \label{eq:ijarc-closed->tightclosed:tight-coherence-eq}

1054:   w^\rT(z_1, z_2)

1055:     &= \Bigl\lfloor \frac{w(z_1, \barz_1)}{2} \Bigr\rfloor

1056:          + \Bigl\lfloor \frac{w(\barz_2, z_2)}{2} \Bigr\rfloor.

1057: \end{align}

1058: \end{lemma}

1059: \begin{proof}

1060: The proof is by contraposition; thus we assume that

1061: neither~\eqref{eq:ijarc-closed->tightclosed:simple-eq}

1062: nor~\eqref{eq:ijarc-closed->tightclosed:tight-coherence-eq} hold.

1063: Without loss of generality,

1064: let the graph $G$ be $\mathord{\graphleq}$-minimal in the set

1065: of all closed integer octagonal graphs such that $\tightclosure(G) = G^\rT$

1066: and for which neither~\eqref{eq:ijarc-closed->tightclosed:simple-eq}

1067: nor~\eqref{eq:ijarc-closed->tightclosed:tight-coherence-eq} hold.

1068: Clearly the negation of~\eqref{eq:ijarc-closed->tightclosed:simple-eq}

1069: implies that $G \neq G^\rT$, so that $G^\rT \graphlt G$.

1070: 

1071: As $G$ is closed but not tightly closed,

1072: by Definitions~\ref{def:strong-closure} and~\ref{def:tight-closure},

1073: it follows that there exist $i,j \in \Vpm$ such that either

1074: \begin{enumerate}[(i)]

1075: \item

1076: \label{item:ijarc-closed->tightclosed:tight-coherence}

1077: $i = \barj$ and $w(i, \bari)$ is odd; or

1078: \item

1079: \label{item:ijarc-closed->tightclosed:strong-coherence}

1080: property \eqref{rule:tight-coherence} holds and

1081: $2 w(i, j) > w(i, \bari) + w(\barj, j)$.

1082: \end{enumerate}

1083: Consider graph $G_1 = (\Vpm, w_1)$

1084: where the weight function $w_1$ is defined,

1085: for all $h_1,h_2 \in \Vpm$, by

1086: \begin{equation*}

1087:   w_1(h_1, h_2)

1088:     \defeq

1089:       \begin{cases}

1090:         \Bigl\lfloor \frac{w(i, \bari)}{2} \Bigr\rfloor

1091:           + \Bigl\lfloor \frac{w(\barj, j)}{2} \Bigr\rfloor,

1092:           &\text{if \(

1093:                       (h_1, h_2)

1094:                         \in \bigl\{ (i, j), (\barj, \bari) \bigr\}

1095:                     \);} \\

1096:         w(h_1, h_2),

1097:           &\text{otherwise.}

1098:       \end{cases}

1099: \end{equation*}

1100: %%

1101: 

1102: Let $G_1^\star = \closure(G_1)$.

1103: By Definitions~\ref{def:closure},~\ref{def:strong-closure}

1104: and~\ref{def:tight-closure},

1105: \begin{equation}

1106: \label{eq:ijarc-closed->tightclosed:graph-relations}

1107: G^\rT \graphleq G_1^\star \graphleq G_1 \graphlt G.

1108: \end{equation}

1109: Thus $\tightclosure(G_1^\star) = G^\rT$ so that,

1110: by the minimality assumption on $G$,

1111: one or both of the following hold:

1112: \begin{align}

1113: \label{eq:ijarc-closed->tightclosed:simple-eq-osc}

1114:   w^\rT(z_1, z_2) &= w_1^\star(z_1, z_2);\\

1115: \label{eq:ijarc-closed->tightclosed:tight-coherence-eq-osc}

1116:   w^\rT(z_1, z_2)

1117:     &= \Bigl\lfloor \frac{w_1^\star(z_1, \barz_1)}{2} \Bigr\rfloor

1118:          + \Bigl\lfloor \frac{w_1^\star(\barz_2, z_2)}{2} \Bigr\rfloor.

1119: \end{align}

1120: 

1121: As $G^\rT \neq \bot$,

1122: by \eqref{eq:ijarc-closed->tightclosed:graph-relations}, $G_1$ is consistent.

1123: Therefore, by construction, $G_1$ is an integer octagonal graph.

1124: If property~(\ref{item:ijarc-closed->tightclosed:tight-coherence})

1125: holds for $i,j$, then  Lemma~\ref{lem:closed->1-step-tight-coherence}

1126: can be applied and,

1127: if property~(\ref{item:ijarc-closed->tightclosed:strong-coherence})

1128: holds for $i,j$,

1129: then  Lemma~\ref{lem:closed->1-step-strong-coherence} can be applied

1130: and also,

1131: since property \eqref{rule:tight-coherence} holds,

1132: both $w_1(z_1, \barz_1)$ and $w(\barz_2, z_2)$ are even.

1133: Hence, letting $G_1^\star \defeq (\Vpm, w_1^\star)$,

1134: one or both of the following hold:

1135: \begin{align}

1136: \label{eq:ijarc-closed->tightclosed:simple-eq-osc-2}

1137:   w_1^\star(z_1, z_2)

1138:     &= w(z_1, z_2); \\

1139: \label{eq:ijarc-closed->tightclosed:tight-coherence-eq-osc-2}

1140:   w_1^\star(z_1, z_2)

1141:     &\geq

1142:       \Bigl\lfloor \frac{w(z_1, \barz_1)}{2} \Bigr\rfloor

1143:         + \Bigl\lfloor \frac{w(\barz_2, z_2)}{2} \Bigr\rfloor. \\

1144: \intertext{%

1145: Again by Lemmas~\ref{lem:closed->1-step-strong-coherence}

1146: and~\ref{lem:closed->1-step-tight-coherence},

1147: }

1148: \notag

1149:   w_1^\star(z_1, \barz_1)

1150:     &\geq

1151:       2 \Bigl\lfloor \frac{w(z_1, \barz_1)}{2} \Bigr\rfloor, \\

1152: \notag

1153:   w_1^\star(\barz_2, z_2)

1154:     &\geq

1155:       2 \Bigl\lfloor \frac{w(\barz_2, z_2)}{2} \Bigr\rfloor;

1156: \end{align}

1157: since the lower bounds for $w_1^\star(z_1, \barz_1)$

1158: and $w_1^\star(\barz_2, z_2)$ are even integers, we obtain

1159: \begin{equation}

1160: \label{eq:ijarc-closed->tightclosed:tight-coherence-eq-osc-3}

1161:   \Bigl\lfloor \frac{w_1^\star(z_1, \barz_1)}{2} \Bigr\rfloor

1162:     + \Bigl\lfloor \frac{w_1^\star(\barz_2, z_2)}{2} \Bigr\rfloor

1163:     \geq

1164:       \Bigl\lfloor \frac{w(z_1, \barz_1)}{2} \Bigr\rfloor

1165:         + \Bigl\lfloor \frac{w(\barz_2, z_2)}{2} \Bigr\rfloor.

1166: \end{equation}

1167: 

1168: Suppose first that~\eqref{eq:ijarc-closed->tightclosed:simple-eq-osc}

1169: and~\eqref{eq:ijarc-closed->tightclosed:simple-eq-osc-2} hold.

1170: Then by transitivity

1171: we obtain~\eqref{eq:ijarc-closed->tightclosed:simple-eq},

1172: contradicting the contrapositive assumption for $G$.

1173: 

1174: If~\eqref{eq:ijarc-closed->tightclosed:simple-eq-osc}

1175: and~\eqref{eq:ijarc-closed->tightclosed:tight-coherence-eq-osc-2} hold,

1176: then it follows

1177: \begin{equation}

1178: \label{eq:ijarc-closed->tightclosed:tight-coherence-eq-osc-4}

1179:   w^\rT(z_1, z_2)

1180:     \geq

1181:       \Bigl\lfloor \frac{w(z_1, \barz_1)}{2} \Bigr\rfloor

1182:         + \Bigl\lfloor \frac{w(\barz_2, z_2)}{2} \Bigr\rfloor.

1183: \end{equation}

1184: On the other hand,

1185: if~\eqref{eq:ijarc-closed->tightclosed:tight-coherence-eq-osc} holds,

1186: then, by~\eqref{eq:ijarc-closed->tightclosed:tight-coherence-eq-osc-3},

1187: we obtain again

1188: property~\eqref{eq:ijarc-closed->tightclosed:tight-coherence-eq-osc-4}.

1189: %%

1190: However, by Definition~\ref{def:tight-closure}

1191: we also have

1192: \begin{align*}

1193:   w^\rT(z_1, z_2)

1194:     &\leq

1195:       \Bigl\lfloor \frac{w(z_1, \barz_1)}{2} \Bigr\rfloor

1196:         + \Bigl\lfloor \frac{w(\barz_2, z_2)}{2} \Bigr\rfloor.

1197: \end{align*}

1198: By combining this inequality

1199: with~\eqref{eq:ijarc-closed->tightclosed:tight-coherence-eq-osc-4}

1200: we obtain~\eqref{eq:ijarc-closed->tightclosed:tight-coherence-eq},

1201: contradicting the contrapositive assumption for $G$.

1202: \qed

1203: \end{proof}

1204: 

1205: \begin{delayedproof}[of Theorem~\ref{thm:one-step-tight-closure}]

1206: Let $G^\rT \defeq \tightclosure(G)$.

1207: By definition of $G_\rT$,

1208: $G_\rT \graphleq G$ so that

1209: $\tightclosure(G_\rT) \graphleq G^\rT$.

1210: As $G_\rT$ is an octagonal graph, $G_\rT$ is consistent,

1211: and hence $G^\rT \neq \bot$;

1212: let $G^\rT = (\Vpm, w^\rT)$.

1213: Letting $i, j \in \Vpm$,

1214: to prove the result we need to show that

1215: $w^\rT(i, j) = w_\lowrT(i, j)$.

1216: Let

1217: \(

1218:   k_{ij}

1219:     \defeq

1220:       \bigl\lfloor w(i, \bari)/2 \bigr\rfloor

1221:         + \bigl\lfloor w(\barj, j)/2 \bigr\rfloor

1222: \).

1223: 

1224: By Definitions~\ref{def:closure},

1225: \ref{def:strong-closure} and~\ref{def:tight-closure},

1226: it follows that both properties

1227: $w^\rT(i, j) \leq w(i, j)$ and

1228: $w^\rT(i, j) \leq k_{ij}$ hold

1229: so that, by definition of $w_\lowrT$, we have

1230: $w^\rT(i, j) \leq w_\lowrT(i, j)$.

1231: %%

1232: By Lemma~\ref{lem:ijarc-closed->tightclosed}, $w^\rT(i, j) = w(i, j)$

1233: and/or

1234: $w^\rT(i, j) = k_{ij}$.

1235: Therefore since, by definition,

1236: $w_\lowrT(i, j) = \min \bigl\{ w(i, j), k_{ij} \bigr\}$,

1237: we obtain $w_\lowrT(i, j) \leq w^\rT(i, j)$.

1238: \qed

1239: \end{delayedproof}

1240: 

1241: It follows from the statement of

1242: Theorem~\ref{thm:one-step-tight-closure}

1243: that an implementation based on it

1244: also needs to check the consistency of $G_\rT$.

1245: In principle, one could apply again a

1246: shortest-path closure procedure so as to check whether

1247: $G_\rT$ contains some negative weight cycles.

1248: Fortunately, a much more efficient solution is obtained

1249: by the following result.

1250: 

1251: \begin{theorem}

1252: \label{thm:even-closure-consistency-condition}

1253: Let $G = (\Vpm, w)$ be a closed integer octagonal graph.

1254: Consider the graphs $G_\rt = (\Vpm, w_\rt)$

1255: and $G_\rT = (\Vpm, w_\lowrT)$

1256: where, for each $i, j \in \Vpm$,

1257: \begin{align}

1258: \label{eq:even-closure-consistency-condition:tightening-rule}

1259:   w_\rt(i, j)

1260:     &\defeq

1261:       \begin{cases}

1262:         2 \lfloor w(i, j)/2 \rfloor,

1263:           &\text{if $j = \bari$;} \\

1264:         w(i, j),

1265:           &\text{otherwise;}

1266:       \end{cases}\\

1267: \label{eq:even-closure-consistency-condition:strong-coherence-rule}

1268:   w_\lowrT(i, j)

1269:     &\defeq

1270:       \min

1271:         \biggl\{

1272:           w(i, j),

1273:           \Bigl\lfloor \frac{w(i, \bari)}{2} \Bigr\rfloor

1274:             + \Bigl\lfloor \frac{w(\barj, j)}{2} \Bigr\rfloor

1275:         \biggr\}.

1276: \end{align}

1277: Suppose that, for all $i \in \Vpm$, $w_\rt(i, \bari) + w_\rt(\bari, i) \geq 0$.

1278: Then $G_\rT$ is an octagonal graph.

1279: \end{theorem}

1280: 

1281: This result is a corollary of the following result

1282: proved in~\cite[Lemma 4]{LahiriM05}.

1283: \begin{lemma}

1284: \label{lem:LahiriM05-lemma-4}

1285: Let $G =(\Vpm, w)$ be an integer octagonal graph with no negative

1286: weight cycles and

1287: $G_\rt = (\Vpm, w_\rt)$, where $w_\rt$ satisfies

1288: \eqref{eq:even-closure-consistency-condition:tightening-rule},

1289: have a negative weight cycle.

1290: Then there exists $i,\bari \in \Vpm$ and a cycle

1291: $\pi = (i \cdot \pi_1 \cdot \bari) \pathconc (\bari  \cdot\pi_2 \cdot i)$

1292: in $G$ such that $w(\pi) = 0$ and the weight of the shortest path in

1293: $G$ from $i$ to $\bari$ is odd.

1294: \end{lemma}

1295: 

1296: \begin{delayedproof}[of Theorem~\ref{thm:even-closure-consistency-condition}]

1297: The proof is by contradiction; suppose $G_\rT$ is not an octagonal

1298: graph; then by Definitions~\ref{def:closure}, \ref{def:strong-closure}

1299: and~\ref{def:tight-closure}, $G_\rT$ is inconsistent.

1300: We show that $G_\rt$ is also inconsistent.

1301: Again, we assume to the contrary that $G_\rt$ is consistent

1302: and derive a contradiction.

1303: Let $i,j \in \Vpm$.

1304: By~\eqref{eq:even-closure-consistency-condition:tightening-rule},

1305: we have $w_\rt(i,j) \leq w(i,j)$

1306: and $w_\rt(i, \bari)/2 + w_\rt(\barj, j)/2 = k_{ij}$,

1307: where

1308: \(

1309:   k_{ij}

1310:     \defeq

1311:       \bigl\lfloor w(i, \bari)/2 \bigr\rfloor

1312:         + \bigl\lfloor w(\barj, j)/2 \bigr\rfloor

1313: \).

1314: Letting $\strongclosure(G_\rt) = (\Vpm, w^\rS_\rt)$,

1315: we have, by Definition~\ref{def:strong-closure},

1316: $w^\rS_\rt(i,j) \leq w_\rt(i, j)$

1317: and

1318: \(

1319:   w^\rS_\rt(i,j)

1320:     \leq

1321:       w_\rt(i, \bari)/2 + w_\rt(\barj, j)/2.

1322: \)

1323: Thus

1324: \(

1325:   w^\rS_\rt(i,j) \leq \min\bigl(w(i,j), k_{ij}\bigr).

1326: \)

1327: As this holds for all $i,j \in \Vpm$,

1328: by~\eqref{eq:even-closure-consistency-condition:strong-coherence-rule},

1329: $\strongclosure(G_\rt) \graphleq G_\rT$,

1330: contradicting the assumption that $G_\rt$ was consistent.

1331: Hence $G_\rt$ is inconsistent and

1332: therefore contains a negative weight cycle.

1333: 

1334: By Lemma \ref{lem:LahiriM05-lemma-4},

1335: there exists $i,\bari \in \Vpm$ and a cycle

1336: $\pi = (i \cdot \pi_1 \cdot \bari) \pathconc (\bari  \cdot\pi_2 \cdot i)$

1337: in $G$ such that $w(\pi) = 0$ and the weight of the shortest path in

1338: $G$ from $i$ to $\bari$ is odd.

1339: As $G$ is closed, $w(i, \bari) \leq w(i \cdot \pi_1 \cdot \bari)$

1340: and $w(\bari, i) \leq w(\bari \cdot \pi_2 \cdot i)$.

1341: Thus $w(i,\bari) + w(\bari, i) \leq w(\pi) = 0$.

1342: Moreover, $(i \bari)$ is a path

1343: and hence the shortest path from $i$ to $\bari$

1344: so that $w(i \bari)$ is odd; hence,

1345: by~\eqref{eq:even-closure-consistency-condition:tightening-rule},

1346: $w(i, \bari) = w_\rt(i, \bari) + 1$ and $w(\bari, i) \geq w_\rt(\bari, i)$.

1347: Therefore $w_\rt(i,\bari) + w_\rt(\bari, i) < 0$.

1348: \qed

1349: \end{delayedproof}

1350: 

1351: \begin{figure}

1352: \begin{align*}

1353: & \kw{function} \;

1354:     \texttt{tight\_closure}

1355:       (\kw{var} \; w\arrayrange{0}{2n-1}\arrayrange{0}{2n-1}) : \kw{bool} \\

1356: & \qquad

1357:   \{ \text{ Initialization: $\bigO(n)$ } \} \\

1358: & \qquad

1359:     \kw{for} \; i := 0 \; \kw{to} \; 2n-1 \; \kw{do} \; w[i,i] := 0; \\

1360: & \qquad

1361:   \{ \text{ Classical Floyd-Warshall: $\bigO(n^3)$ } \} \\

1362: & \qquad

1363:     \kw{for} \; k := 0 \; \kw{to} \; 2n-1 \; \kw{do} \\

1364: & \qquad\qquad

1365:     \kw{for} \; i := 0 \; \kw{to} \; 2n-1 \; \kw{do} \\

1366: & \qquad\qquad\qquad

1367:       \kw{for} \; j := 0 \; \kw{to} \; 2n-1 \; \kw{do} \\

1368: & \qquad\qquad\qquad\qquad

1369:         w[i,j] := \min\bigl(

1370:                         w[i,j],

1371:                         w[i,k] + w[k,j]

1372:                       \bigr); \\

1373: & \qquad

1374:   \{ \text{ Check for $\Qset$-consistency: $\bigO(n)$ } \} \\

1375: & \qquad

1376:     \kw{for} \; i := 0 \; \kw{to} \; 2n-2 \; \kw{step} \; 2 \; \kw{do} \\

1377: & \qquad\qquad

1378:       \kw{if} \; w[i,i] < 0 \; \kw{return} \; \mathrm{false}; \\

1379: & \qquad

1380:   \{ \text{ Tightening: $\bigO(n)$ } \} \\

1381: & \qquad

1382:   \kw{for} \; i := 0 \; \kw{to} \; 2n-1 \; \kw{do} \\

1383: & \qquad\qquad

1384:     w[i,\bari] := \mathrm{floor}\bigl( w[i,\bari] / 2 \bigr); \\

1385: & \qquad

1386:   \{ \text{ Check for $\Zset$-consistency: $\bigO(n)$ } \} \\

1387: & \qquad

1388:     \kw{for} \; i := 0 \; \kw{to} \; 2n-2 \; \kw{step} \; 2 \; \kw{do} \\

1389: & \qquad\qquad

1390:       \kw{if} \; w[i,\bari] + w[\bari,i] < 0

1391:         \; \kw{return} \; \mathrm{false}; \\

1392: & \qquad

1393:   \{ \text{ Strong coherence: $\bigO(n^2)$ } \} \\

1394: & \qquad

1395:   \kw{for} \; i := 0 \; \kw{to} \; 2n-1 \; \kw{do} \\

1396: & \qquad\qquad

1397:     \kw{for} \; j := 0 \; \kw{to} \; 2n-1 \; \kw{do} \\

1398: & \qquad\qquad\qquad

1399:       w[i,j] := \min\bigl(

1400:                       w[i,j],

1401:                       w[i,\bari]/2 + w[\barj,j]/2

1402:                     \bigr); \\

1403: & \qquad

1404:   \kw{return} \; \mathrm{true};

1405: \end{align*}

1406: \caption{A $\bigO(n^3)$ tight closure algorithm for integer coherent graphs}

1407: \label{fig:tight-closure}

1408: \end{figure}

1409: The combination of the results stated in

1410: Theorems~\ref{thm:one-step-tight-closure}

1411: and~\ref{thm:even-closure-consistency-condition}

1412: (together with the well known result for rational consistency)

1413: leads to an $\bigO(n^3)$ tight closure algorithm,

1414: such as that given by the pseudo-code in Figure~\ref{fig:tight-closure},

1415: that

1416: computes the tight closure of any (possibly inconsistent)

1417: coherent integer-weighted graph

1418: returning the Boolean value `$\mathrm{true}$'

1419: if and only if the input graph is $\Zset$-consistent.

1420: 

1421: 

1422: \section{Conclusion and Future Work}

1423: \label{sec:conclusion}

1424: 

1425: We have presented and fully justified an $\bigO(n^3)$ algorithm

1426: that computes the tight closure of a set of integer octagonal

1427: constraints.

1428: The algorithm ---which is based on the extension to integer-weighted

1429: octagonal graphs of the one we proposed for rational-weighted

1430: octagonal graphs~\cite{BagnaraHMZ05,BagnaraHMZ05TR}--- and its

1431: proof of correctness means the issue about

1432: the possibility of computing the tight closure at a computational

1433: cost that is asymptotically not worse than the cost of computing

1434: all-pairs shortest paths is finally closed.

1435: 

1436: In the field of hardware and software verification, the integrality

1437: constraint that distinguishes integer-weighted from rational-weighted

1438: octagonal graphs can be seen as an abstraction of the more general

1439: imposition of a set of congruence relations.  Such a set can be encoded

1440: by an element of a suitable abstract domain such as the non-relational

1441: congruence domain of \cite{Granger89}

1442: (that is, of the form $x = a \pmod b$),

1443: the  weakly relational \emph{zone-congruence} domain of \cite{Mine02}

1444: (that is, also allowing the form $x - y = a \pmod b$),

1445: the linear congruence domain of \cite{Granger91},

1446: and the more general fully relational \emph{rational grids} domain developed

1447: in~\cite{BagnaraDHMZ07}.

1448: The combination of such domains with the abstract domain

1449: proposed in \cite{BagnaraHMZ05,BagnaraHMZ05TR}

1450: is likely to provide an interesting complexity-precision trade-off.

1451: Future work includes investigating such a combination,

1452: exploiting the ideas presented in this paper.

1453: 

1454: %\bibliographystyle{plain}

1455: %\bibliography{ppl,mybib}

1456: \newcommand{\noopsort}[1]{}\hyphenation{ Ba-gna-ra Bie-li-ko-va Bruy-noo-ghe

1457:   Common-Loops DeMich-iel Dober-kat Di-par-ti-men-to Er-vier Fa-la-schi

1458:   Fell-eisen Gam-ma Gem-Stone Glan-ville Gold-in Goos-sens Graph-Trace

1459:   Grim-shaw Her-men-e-gil-do Hoeks-ma Hor-o-witz Kam-i-ko Kenn-e-dy Kess-ler

1460:   Lisp-edit Lu-ba-chev-sky Ma-te-ma-ti-ca Nich-o-las Obern-dorf Ohsen-doth

1461:   Par-log Para-sight Pega-Sys Pren-tice Pu-ru-sho-tha-man Ra-guid-eau Rich-ard

1462:   Roe-ver Ros-en-krantz Ru-dolph SIG-OA SIG-PLAN SIG-SOFT SMALL-TALK Schee-vel

1463:   Schlotz-hauer Schwartz-bach Sieg-fried Small-talk Spring-er Stroh-meier

1464:   Thing-Lab Zhong-xiu Zac-ca-gni-ni Zaf-fa-nel-la Zo-lo }

1465: \begin{thebibliography}{10}

1466: 

1467: \bibitem{BagnaraDHMZ07}

1468: R.~Bagnara, K.~Dobson, P.~M. Hill, M.~Mundell, and E.~Zaffanella.

1469: \newblock Grids: A domain for analyzing the distribution of numerical values.

1470: \newblock In G.~Puebla, editor, {\em Logic-based Program Synthesis and

1471:   Transformation, 16th International Symposium}, volume 4407 of {\em Lecture

1472:   Notes in Computer Science}, pages 219--235, Venice, Italy, 2007.

1473:   Springer-Verlag, Berlin.

1474: 

1475: \bibitem{BagnaraHMZ05}

1476: R.~Bagnara, P.~M. Hill, E.~Mazzi, and E.~Zaffanella.

1477: \newblock Widening operators for weakly-relational numeric abstractions.

1478: \newblock In C.~Hankin and I.~Siveroni, editors, {\em Static Analysis:

1479:   Proceedings of the 12th International Symposium}, volume 3672 of {\em Lecture

1480:   Notes in Computer Science}, pages 3--18, London, UK, 2005. Springer-Verlag,

1481:   Berlin.

1482: 

1483: \bibitem{BagnaraHMZ05TR}

1484: R.~Bagnara, P.~M. Hill, E.~Mazzi, and E.~Zaffanella.

1485: \newblock Widening operators for weakly-relational numeric abstractions.

1486: \newblock Quaderno 399, Dipartimento di Matematica, Universit\`a di Parma,

1487:   Italy, 2005.

1488: \newblock Available at \url{http://www.cs.unipr.it/Publications/}.

1489: 

1490: \bibitem{BagnaraHZ06TR}

1491: R.~Bagnara, P.~M. Hill, and E.~Zaffanella.

1492: \newblock The {Parma Polyhedra Library}: Toward a complete set of numerical

1493:   abstractions for the analysis and verification of hardware and software

1494:   systems.

1495: \newblock Quaderno 457, Dipartimento di Matematica, Universit\`a di Parma,

1496:   Italy, 2006.

1497: \newblock Available at \url{http://www.cs.unipr.it/Publications/}. Also

1498:   published as {\tt arXiv:cs.MS/0612085}, available from

1499:   \url{http://arxiv.org/}.

1500: 

1501: \bibitem{BalasundaramK89}

1502: V.~Balasundaram and K.~Kennedy.

1503: \newblock A technique for summarizing data access and its use in parallelism

1504:   enhancing transformations.

1505: \newblock In B.~Knobe, editor, {\em Proceedings of the ACM SIGPLAN'89

1506:   Conference on Programming Language Design and Implementation (PLDI)}, volume

1507:   24(7) of {\em ACM SIGPLAN Notices}, pages 41--53, Portland, Oregon, USA,

1508:   1989. ACM Press.

1509: 

1510: \bibitem{BallCLZ04}

1511: T.~Ball, B.~Cook, S.~K. Lahiri, and L.~Zhang.

1512: \newblock {Zapato}: Automatic theorem proving for predicate abstraction

1513:   refinement.

1514: \newblock In R.~Alur and D.~Peled, editors, {\em Computer Aided Verification:

1515:   Proceedings of the 16th International Conference}, volume 3114 of {\em

1516:   Lecture Notes in Computer Science}, pages 457--461, Boston, MA, USA, 2004.

1517:   Springer-Verlag, Berlin.

1518: 

1519: \bibitem{CormenLR90}

1520: T.~H. Cormen, T.~E. Leiserson, and R.~L. Rivest.

1521: \newblock {\em Introduction to Algorithms}.

1522: \newblock The MIT Press, Cambridge, MA, 1990.

1523: 

1524: \bibitem{CousotC77}

1525: P.~Cousot and R.~Cousot.

1526: \newblock Abstract interpretation: A unified lattice model for static analysis

1527:   of programs by construction or approximation of fixpoints.

1528: \newblock In {\em Proceedings of the Fourth Annual ACM Symposium on Principles

1529:   of Programming Languages}, pages 238--252, New York, 1977. ACM Press.

1530: 

1531: \bibitem{CousotCFMMMR05}

1532: P.~Cousot, R.~Cousot, J.~Feret, L.~Mauborgne, A.~Min\'e, D.~Monniaux, and

1533:   X.~Rival.

1534: \newblock The {ASTR\'EE} analyzer.

1535: \newblock In M.~Sagiv, editor, {\em Programming Languages and Systems,

1536:   Proceedings of the 14th European Symposium on Programming}, volume 3444 of

1537:   {\em Lecture Notes in Computer Science}, pages 21--30, Edinburgh, UK, 2005.

1538:   Springer-Verlag, Berlin.

1539: 

1540: \bibitem{Granger89}

1541: P.~Granger.

1542: \newblock Static analysis of arithmetical congruences.

1543: \newblock {\em International Journal of Computer Mathematics}, 30:165--190,

1544:   1989.

1545: 

1546: \bibitem{Granger91}

1547: P.~Granger.

1548: \newblock Static analysis of linear congruence equalities among variables of a

1549:   program.

1550: \newblock In S.~Abramsky and T.~S.~E. Maibaum, editors, {\em TAPSOFT'91:

1551:   Proceedings of the International Joint Conference on Theory and Practice of

1552:   Software Development, Volume 1: Colloquium on Trees in Algebra and

1553:   Programming (CAAP'91)}, volume 493 of {\em Lecture Notes in Computer

1554:   Science}, pages 169--192, Brighton, UK, 1991. Springer-Verlag, Berlin.

1555: 

1556: \bibitem{HarveyS97}

1557: W.~Harvey and P.~J. Stuckey.

1558: \newblock A unit two variable per inequality integer constraint solver for

1559:   constraint logic programming.

1560: \newblock In M.~Patel, editor, {\em ACSC'97: Proceedings of the 20th

1561:   Australasian Computer Science Conference}, volume~19, pages 102--111.

1562:   Australian Computer Science Communications, 1997.

1563: 

1564: \bibitem{JaffarMSY94}

1565: J.~Jaffar, M.~J. Maher, P.~J. Stuckey, and R.~H.~C. Yap.

1566: \newblock Beyond finite domains.

1567: \newblock In A.~Borning, editor, {\em Principles and Practice of Constraint

1568:   Programming: Proceedings of the Second International Workshop}, volume 874 of

1569:   {\em Lecture Notes in Computer Science}, pages 86--94, Rosario, Orcas Island,

1570:   Washington, USA, 1994. Springer-Verlag, Berlin.

1571: 

1572: \bibitem{Lagarias85b}

1573: J.~C. Lagarias.

1574: \newblock The computational complexity of simultaneous {Diophantine}

1575:   approximation problems.

1576: \newblock {\em SIAM Journal on Computing}, 14(1):196--209, 1985.

1577: 

1578: \bibitem{LahiriM05}

1579: S.~K. Lahiri and M.~Musuvathi.

1580: \newblock An efficient decision procedure for {UTVPI} constraints.

1581: \newblock In B.~Gramlich, editor, {\em Frontiers of Combining Systems:

1582:   Proceedings of the 5th International Workshop, FroCoS 2005}, volume 3717 of

1583:   {\em Lecture Notes in Artificial Intelligence}, pages 168--183, Vienna,

1584:   Austria, 2005. Springer-Verlag, Berlin.

1585: 

1586: \bibitem{Mine01a}

1587: A.~Min\'e.

1588: \newblock A new numerical abstract domain based on difference-bound matrices.

1589: \newblock In O.~Danvy and A.~Filinski, editors, {\em Proceedings of the 2nd

1590:   Symposium on Programs as Data Objects (PADO 2001)}, volume 2053 of {\em

1591:   Lecture Notes in Computer Science}, pages 155--172, Aarhus, Denmark, 2001.

1592:   Springer-Verlag, Berlin.

1593: 

1594: \bibitem{Mine01b}

1595: A.~Min\'e.

1596: \newblock The octagon abstract domain.

1597: \newblock In {\em Proceedings of the Eighth Working Conference on Reverse

1598:   Engineering (WCRE'01)}, pages 310--319, Stuttgart, Germany, 2001. IEEE

1599:   Computer Society Press.

1600: 

1601: \bibitem{Mine02}

1602: A.~Min\'e.

1603: \newblock A few graph-based relational numerical abstract domains.

1604: \newblock In M.~V. Hermenegildo and G.~Puebla, editors, {\em Static Analysis:

1605:   Proceedings of the 9th International Symposium}, volume 2477 of {\em Lecture

1606:   Notes in Computer Science}, pages 117--132, Madrid, Spain, 2002.

1607:   Springer-Verlag, Berlin.

1608: 

1609: \bibitem{Mine05th}

1610: A.~Min\'e.

1611: \newblock {\em Weakly Relational Numerical Abstract Domains}.

1612: \newblock PhD thesis, \'Ecole Polytechnique, Paris, France, March 2005.

1613: 

1614: \bibitem{Mine06b}

1615: A.~Min{\'e}.

1616: \newblock The octagon abstract domain.

1617: \newblock {\em Higher-Order and Symbolic Computation}, 19(1):31--100, 2006.

1618: 

1619: \bibitem{NelsonO77}

1620: G.~Nelson and D.~C. Oppen.

1621: \newblock Fast decision algorithms based on {Union} and {Find}.

1622: \newblock In {\em Proceedings of the 18th Annual Symposium on Foundations of

1623:   Computer Science (FOCS'77)}, pages 114--119, Providence, RI, USA, 1977. IEEE

1624:   Computer Society Press.

1625: \newblock The journal version of this paper is \cite{NelsonO80}.

1626: 

1627: \bibitem{NelsonO80}

1628: G.~Nelson and D.~C. Oppen.

1629: \newblock Fast decision procedures based on congruence closure.

1630: \newblock {\em Journal of the ACM}, 27(2):356--364, 1980.

1631: \newblock An earlier version of this paper is \cite{NelsonO77}.

1632: 

1633: \bibitem{Pratt77}

1634: V.~R. Pratt.

1635: \newblock Two easy theories whose combination is hard.

1636: \newblock Memo sent to Nelson and Oppen concerning a preprint of their paper

1637:   \cite{NelsonO77}, September 1977.

1638: 

1639: \bibitem{VenetB04}

1640: A.~Venet and G.~Brat.

1641: \newblock Precise and efficient static array bound checking for large embedded

1642:   {C} programs.

1643: \newblock In {\em Proceedings of the ACM SIGPLAN 2004 Conference on Programming

1644:   Language Design and Implementation (PLDI'04)}, pages 231--242, Washington,

1645:   DC, USA, 2004. ACM Press.

1646: 

1647: \end{thebibliography}

1648: 

1649: \end{document}

1650: