1: \documentclass[acmtocl]{acmtrans2m}
2:
3:
4: \usepackage{enumerate}
5:
6: \usepackage{amsmath}
7: \usepackage{amssymb}
8: \usepackage[mathscr]{eucal}
9:
10: \usepackage{graphics}
11:
12: \usepackage{xspace}
13:
14:
15: \input{prelude}
16:
17: \newtheorem{theorem}{Theorem}[section]
18: \newtheorem{conjecture}[theorem]{Conjecture}
19: \newtheorem{corollary}[theorem]{Corollary}
20: \newtheorem{proposition}[theorem]{Proposition}
21: \newtheorem{lemma}[theorem]{Lemma}
22: \newtheorem{fact}[theorem]{Fact}
23: \newdef{algorithm}[theorem]{Algorithm}
24: \newdef{definition}[theorem]{Definition}
25: \newdef{remark}[theorem]{Remark}
26: \newdef{example}[theorem]{Example}
27:
28:
29: \newcommand{\ignore}[1]{}
30:
31: \markboth{Felix Klaedtke}{Bounds on the Automata Size for Presburger
32: Arithmetic}
33:
34: \title{Bounds on the Automata Size for Presburger Arithmetic}
35: %\title{On the Automata Size for Presburger Arithmetic}
36:
37: \author{FELIX KLAEDTKE\\ETH Zurich}
38:
39: \begin{abstract}
40: Automata provide a decision procedure for Presburger arithmetic.
41: However, until now only crude lower and upper bounds were known on
42: the sizes of the automata produced by this approach. In this paper,
43: we prove an upper bound on the the number of states of the minimal
44: deterministic automaton for a Presburger arithmetic formula. This
45: bound depends on the length of the formula and the quantifiers
46: occurring in the formula. The upper bound is established by
47: comparing the automata for Presburger arithmetic formulas with the
48: formulas produced by a quantifier elimination method. We also show
49: that our bound is tight, even for nondeterministic automata.
50: Moreover, we provide optimal automata constructions for linear
51: equations and inequations.
52: \end{abstract}
53:
54: \category{F.1.1}{Computation by Abstract Devices}{Models of
55: Computation}[automata]
56: %%
57: \category{F.4.1}{Mathematical Logic and Formal Languages}{Mathematical
58: Logic}[computational logic]
59:
60: \terms{Algorithms, Theory}
61:
62: \keywords{Automata-based Decision Procedures, Presburger Arithmetic,
63: Quantifier Elimination, Complexity}
64:
65: \begin{document}
66:
67: \begin{bottomstuff}
68: This work was partially supported by the German Research Council
69: (DFG) and the Swiss National Science Foundation (SNF).
70:
71: A preliminary version of this paper appeared at the 19th Annual IEEE
72: Symposium on Logic in Computer Science (LICS'04).
73:
74: Author's address: Felix Klaedtke, ETH Zurich, Department of Computer Science,
75: Haldeneggsteig 4/Weinbergstra\ss{}e, 8092 Zurich, Switzerland.
76: \end{bottomstuff}
77:
78: \maketitle
79:
80: \section{Introduction}
81: \label{INTRO}
82:
83: Presburger arithmetic (PA) is the first-order theory with addition and
84: the ordering relation over the integers. A number of decision
85: problems can be expressed in it, such as solvability of systems of
86: linear Diophantine equations, integer programming, and various
87: problems in system verification. The decidability of PA was
88: established around 1930 independently by
89: Presburger~\citeyear{Presburger.1929,Stansifer.1984} and
90: Skolem~\citeyear{Skolem.1931,Skolem.1970} using the method of
91: quantifier elimination\@.
92:
93: Due to the applicability of PA in various domains, its complexity and
94: the complexity of decision problems for fragments of it have been
95: investigated intensively. For example, Fischer and
96: Rabin~~\citeyear{Fischer_Rabin.1974,Fischer_Rabin.1998} gave a double
97: exponential nondeterministic time lower bound on any decision
98: procedure for PA. Later,~\citeN{Berman.1980} showed that the decision
99: problem for PA is complete in the complexity class
100: $\mathit{LATIME}(2^{2^{\BigOh(n)}})$, \ie, the class of problems
101: solvable by alternating Turing machines in time $2^{2^{\BigOh(n)}}$
102: with a linear number of alternations. The upper bound for PA is
103: established by a result from~\citeN{Ferrante_Rackoff.1979} showing
104: that quantified variables need only to range over a restricted finite
105: domain of integers. \citeN{Graedel.1988} and~\citeN{Schoening.1997}
106: investigated the complexity of decision problems of fragments of PA\@.
107:
108: The complexity of different decision procedures for PA has also been
109: studied, \eg, in
110: \cite{Oppen.1978,Reddy_Loveland.1978,Ferrante_Rackoff.1975,Ferrante_Rackoff.1979}\@.
111: For instance, \citeN{Oppen.1978} showed that Cooper's quantifier
112: elimination decision procedure for PA~\cite{Cooper.1972} has a triple
113: exponential worst case complexity in deterministic time.
114: \citeN{Reddy_Loveland.1978} improved Cooper's quantifier elimination
115: and used it for obtaining space and deterministic time upper bounds
116: for checking the satisfiability of PA formulas in which the number of
117: quantifier alternations is bounded.
118:
119:
120:
121: Another approach for deciding PA or fragments of it that has recently
122: become popular is to use automata; a point that was already made
123: by~\citeN{Buechi.1960}\@. The idea is simple: Integers are represented
124: as words, \eg, using the $2$'s complement representation, and the word
125: automaton (WA) for a formula accepts precisely the words that
126: represent the integers making the formula true. The WA can be
127: recursively constructed from the formula, where automata constructions
128: handle the logical connectives and quantifiers.
129: %%
130: This automata-based approach for PA led to deep theoretical insights,
131: \eg, the languages that are regular in any base are exactly the sets
132: definable in PA~\cite{Cobham.1969,Semenov.1977,Bruyere_etal.1994}\@.
133: %%
134: More recently, the use of automata has been proposed for mechanizing
135: decision procedures for PA and for manipulating sets definable in
136: PA~\cite{Boudet_Comon.1996,Wolper_Boigelot.1995}\@.
137: %%
138: Roughly speaking, this applied use of WAs for PA is similar to the use
139: of binary decision diagrams (BDDs) for propositional logic.
140: %%
141: For example, the automata library LASH~\cite{LASH} provides tool
142: support for manipulating PA definable sets using automata to
143: represented these sets, and it has been successfully used to verify
144: systems with variables ranging over the integers. Other model
145: checkers that use WAs for computing the potential infinite sets of
146: reachable states of systems with integer variables are, \eg,
147: FAST~\cite{FAST} and ALV~\cite{ALV}\@.
148:
149:
150:
151:
152: A crude complexity analysis of automata-based decision procedures for
153: PA leads to a non-elementary worst case complexity. Namely, for every
154: quantifier alternation there is a potential exponential blow-up.
155: However, experimental
156: comparisons~\cite{Ranjan_Shiple_Kukula.1998,Bartzis_Bultan.2003,Ganesh_Berezin_Dill.2002}
157: illustrate that automata-based decision procedures for PA often
158: perform well in comparison with other methods.
159: %%
160: In~\cite{Boudet_Comon.1996}, the authors claimed that the minimal
161: deterministic WA for a PA formula has at most a triple exponential
162: number of states in the length of the formula. Unfortunately, as
163: explained by~\citeN{Wolper_Boigelot.2000}, the argument used
164: in~\cite{Boudet_Comon.1996} to substantiate this claim is incorrect.
165: \citeN{Wolper_Boigelot.2000} gave an argument why there must be an
166: elementary upper bound on the size of the minimal deterministic WA for
167: a PA formula. However, their argumentation is rather sketchy and only
168: indicates that there has to be an elementary upper bound.
169: %\footnote{Appendix~\ref{app:WB_argument} contains a detailed
170: % discussion of Wolper and Boigelot's argumentation.}
171:
172: In this paper, we rigorously prove an upper bound on the size of the
173: minimal deterministic WA for PA formulas and thus, answer a long open
174: question. Namely, for a PA formula in prenex normal form, we show that
175: the minimal deterministic WA has at most $2^{n^{(b+1)^{a+4}}}$ states,
176: where $n$ is the formula length, $a$ is the number of quantifier
177: alternations, and $b$ is the maximal length of the quantifier blocks.
178: A similar upper bound holds for arbitrary PA formulas.
179: %%
180: This bound on the automata size for PA
181: contrasts with the upper bound on the automata size for the monadic
182: second-order logic WS1S, or even WS1S with the ordering relation
183: ``$<$'' as a primitive but without quantification over monadic
184: second-order variables. There, the number of states of the minimal WA
185: for a formula can be non-elementary larger than the formula's
186: length~\cite{Stockmeyer.1974,Reinhardt.2002}\@.
187: %
188: In order to establish the upper bound on the automata size for PA, we
189: give a detailed analysis of the deterministic WAs for formulas by
190: comparing the constructed WAs with the quantifier-free formulas
191: produced by using Reddy and Loveland's quantifier elimination method.
192: From this analysis, we obtain the upper bound on the size of the
193: minimal deterministic WA for PA formulas.
194:
195: We also show that the upper bound on the size of deterministic WAs for
196: formulas is tight. In fact, we show a stronger result. Namely, we give
197: a family of Presburger arithmetic formulas for which even a
198: nondeterministic WA must have at least triple exponentially many
199: states.
200:
201: Furthermore, we investigate the automata constructed from atomic
202: formulas. Specific algorithms for constructing WAs for linear
203: (in)equa\-tions have been developed
204: in~\cite{Boudet_Comon.1996,Boigelot.1999,Wolper_Boigelot.2000,Bartzis_Bultan.2003,Ganesh_Berezin_Dill.2002}\@.
205: We give upper and lower bounds on the automata size for linear
206: (in)equations and we improve the automata constructions
207: in~\cite{Boigelot.1999,Wolper_Boigelot.2000,Ganesh_Berezin_Dill.2002}
208: for linear (in)equations. We prove that our automata constructions are
209: optimal in the sense that the constructed deterministic WAs are
210: minimal.
211:
212:
213: We proceed as follows. In~\S\ref{PRELIM}, we give background.
214: In~\S\ref{AUTO}, we investigate the WAs for quantifier-free formulas.
215: In~\S\ref{BOUND}, we prove the upper bound on the size of the minimal
216: deterministic WA for PA formulas and in~\S\ref{WORST}, we give a worst
217: case example. Finally, in~\S\ref{CONCL}, we draw conclusions.
218: %Appendix~\ref{app:proof_details} contains additional proof details.
219:
220:
221: \section{Preliminaries}
222: \label{PRELIM}
223:
224:
225: \subsection{Presburger Arithmetic}
226:
227: \emph{Presburger arithmetic} (PA) is the first-order logic over the
228: structure $\frakZ:=(\Int,<,+)$\@. We use standard notation. For
229: instance, we write $\frakZ\models\varphi[a_1,\dots,a_r]$ for a formula
230: $\varphi(x_1,\dots,x_r)$ and $a_1,\dots,a_r\in\Int$ if $\varphi$ is
231: true in $\frakZ$ when the variable $x_i$ is interpreted as the integer
232: $a_i$, for $1\leq i\leq r$\@. Analogously, $t[a_1,\dots,a_r]$ denotes
233: the integer when the $x_i$s are interpreted as the $a_i$s in the term
234: $t(x_1,\dots,x_r)$\@. For a formula $\varphi(x_1,\dots,x_r)$, we
235: define $\Zrepresents{\varphi}:=
236: \set{(a_1,\dots,a_r)\in\Int^r}{\frakZ\models\varphi[a_1,\dots,a_r]}$\@.
237:
238:
239: \subsubsection{Extended Logical Language}
240:
241: We extend the logical language of PA by (i)~constants for the integers
242: $0$ and $1$, (ii)~the unary operation ``$-$'' for integer negation,
243: and (iii)~the unary predicates ``$d\divides$'' for the relation
244: ``divisible by $d$,'' for each $d\geq 2$\@. These constructs are
245: definable in PA, \eg, the formula $\exists x(x+\dots+x\EQ t)$ defines
246: $d\divides t$, where $x$ occurs $d$ times in the term $x+\dots+x$ and
247: $x$ does not appear in the term $t$\@.
248: %
249: The reason for the extended logical language, where~(i),~(ii),~and
250: (iii)~are treated as primitives, is that it admits quantifier
251: elimination, \ie, for a formula $\exists x\varphi(x,\overline{y})$,
252: where $\varphi$ is quantifier-free, we can construct a logically
253: equivalent quantifier-free formula $\psi(\overline{y})$\@.
254:
255: Additionally, we allow the relation symbols $\leq,>,\geq$, and $\not=$
256: with their standard meanings.
257: %
258: In the following, we assume that terms and formulas are defined in
259: terms of the extended logical language for PA\@.
260: %%
261: We denote by $\pa$ the set of all Presburger arithmetic formulas over
262: the extended logical language and $\qf$ denotes the set of
263: quantifier-free formulas.
264:
265: For convenience, we use standard symbols when writing terms.
266: %
267: For instance, $c$ stands for $1+\dots+1$ (repeated $c$ times) if
268: $c>0$, and $-(1+\dots+1)$ if $c<0$\@. We call the term $c$ a
269: \emph{constant} and identify the term $c$ with the integer that it
270: represents. Analogously, we write $k\CDOT x$ for $x+\dots+x$
271: (repeated $k$ times) if $k>0$, and $-(x+\dots+x)$ if $k<0$\@.
272: Moreover, if $k=0$ then $k\CDOT x$ abbreviates $x+(-x)$\@. We say
273: that $k$ is a \emph{coefficient}.
274: %
275: For a term $t$ and $k\in\Int$, $k\cdot t$ denotes the term where the
276: constant and the coefficients in $t$ are multiplied by $k$\@.
277:
278: A term $t$ is \emph{homogeneous} if it is either $0$ or of the form
279: $k_1\CDOT x_1+\dots+k_r\CDOT x_r$, for some $r\geq 1$, where the
280: variables $x_1,\dots,x_r$ are pairwise distinct and
281: $k_1,\dots,k_r\in\Int\setminus\{0\}$\@.
282: %%
283: The \emph{normalized form} of $t_1\ZAECKZAECK t_2$, with
284: $\zaeckzaeck\in\{=,\not=,<,\leq,>,\geq\}$, is the logically equivalent
285: (in)equa\-tion $t\ZAECKZAECK c$, where summands of the form $k\CDOT x$
286: in $t_1$ and $t_2$ are collected on the left-hand side $t$ and
287: constants in $t_1$ and $t_2$ are collected on the right-hand side $c$
288: according to standard calculation rules. The \emph{normalized form} of
289: $d\divides t$ is the formula $d\divides t'+c$, where $c\in\Int$ is the
290: sum of the constants in $t$ and $t'$ is the homogeneous term in which
291: the coefficients of the summands of the form $k\CDOT x$ in $t$ are
292: collected.
293: %%
294: We use $\Atoms(\varphi)$ to denote the set of atomic formulas
295: occurring in $\varphi\in\pa$ in their normalized forms.
296:
297:
298: \subsubsection{Formula Length}
299:
300: The \emph{length of a formula} is the number of letters used in
301: writing the formula. Note that the length of a formula depends
302: significantly on how we define the length of coefficients and
303: constants. For instance, $x\EQ 10\CDOT y$ contains $6$ letters,
304: namely, $x$, $\EQ$, $1$, $0$, $\CDOT$, and $y$\@. The ``expanded
305: version'' has $2+19$ letters since $10\CDOT y$ abbreviates the term
306: $y+y+y+y+y+y+y+y+y+y$\@. We use the same definition of the length of
307: a formula as
308: in~\cite{Oppen.1978,Fischer_Rabin.1974,Reddy_Loveland.1978}\@. In
309: particular, the length of a coefficient or constant is the number of
310: letters of the expanded version.
311: %%
312: However, it is possible to express $k\CDOT x$ by a formula of length
313: $\BigOh(\log\abs{k})$\@. The idea is illustrated by $x\EQ 10\CDOT y$:
314: the formula is logically equivalent to $\exists z(x\EQ z+z\AND\exists
315: x(z\EQ x+x+y\AND x\EQ y+y))$\@. Note that we only need a fixed number
316: of variables for any $k$ (see~\cite{Fischer_Rabin.1974})\@. For the
317: sake of uniformity, we define the length of the formula $d\divides t$
318: as the length of the term $t$ plus $d+1$\@. Again, there is a
319: logically equivalent formula of length $\BigOh(\log d)$ plus the length
320: of $t$\@. For the results in this paper it does not matter if we
321: define the length of an integer $k$ as $\BigOh(\log\abs{k})$ or as
322: $\BigOh(\abs{k})$\@.
323:
324:
325: \subsubsection{Nesting of Quantifiers}
326:
327: \newcommand{\qn}{\operatorname{qn}}
328: \newcommand{\qa}{\operatorname{qa}}
329: \newcommand{\qbl}{\operatorname{qbl}}
330:
331:
332: It is well-known that we obtain coarse complexity bounds for checking
333: satisfiability if we only take into account the formula length. We
334: obtain more precise complexity bounds when we additionally for account
335: the number of quantifiers and the number of quantifier alternations.
336:
337: The \emph{quantifier number} of $\varphi\in\pa$ is the number of
338: quantifiers occurring in $\varphi$, \ie,
339: \begin{equation*}
340: \qn(\varphi):=\begin{cases}
341: \qn(\psi) & \text{if $\varphi=\neg\psi$,}
342: \\
343: \qn(\psi_1)+\qn(\psi_2) & \text{if $\varphi=\psi_1\oplus\psi_2$
344: with $\oplus\in\{\wedge,\vee,\rightarrow,\leftrightarrow\}$,}
345: \\
346: 1+\qn(\psi) & \text{if $\varphi=Qx\psi$ with
347: $Q\in\{\exists,\forall\}$,}
348: \\
349: 0 & \text{otherwise.}
350: \end{cases}
351: \end{equation*}
352: For a quantifier $Q\in\{\exists,\forall\}$, $\overline{Q}$ denotes its
353: dual, \ie, $\overline{Q}:=\forall$ if $Q=\exists$, and
354: $\overline{Q}:=\exists$ if $Q=\forall$\@.
355: %%
356: The number of \emph{quantifier alternations} of $\varphi\in\pa$ is
357: \begin{equation*}
358: \qa(\varphi):=
359: \min\{\qa_{\exists}(\varphi),\qa_{\forall}(\varphi)\}
360: \,,
361: \end{equation*}
362: where
363: \begin{equation*}
364: \qa_Q(\varphi):=\begin{cases}
365: \qa_{\overline{Q}}(\psi) & \text{if $\varphi=\neg\psi$,}
366: \\
367: \max\{\qa_Q(\psi_1),\qa_Q(\psi_2)\} & \text{if
368: $\varphi=\psi_1\oplus\psi_2$ with $\oplus\in\{\vee,\wedge\}$,}
369: \\
370: \qa_Q(\neg\psi_1\vee\psi_2)
371: &\text{if $\varphi=\psi_1\rightarrow\psi_2$,}
372: \\
373: \qa_Q((\psi_1\rightarrow\psi_2)\wedge(\psi_2\rightarrow\psi_1))
374: & \text{if $\varphi=\psi_1\leftrightarrow\psi_2$,}
375: \\
376: 1+\qa_{\overline{Q}}(\psi) & \text{if $\varphi=\overline{Q}x\psi$,}
377: \\
378: \max\{1,\qa_Q(\psi)\} & \text{if $\varphi=Qx\psi$,}
379: \\
380: 0 & \text{otherwise,}
381: \end{cases}
382: \end{equation*}
383: for $Q\in\{\exists,\forall\}$\@.
384:
385: %A formula $\varphi$ is in \emph{prenex normal form} if it has the form
386: %$Q_1 x_1\dots Q_r x_r \psi$, where
387: %$Q_1,\dots,Q_r\in\{\exists,\forall\}$ and $\psi_0\in\qf$\@.
388:
389:
390: \subsection{Automata over Finite Words}
391:
392: The set of all words over an alphabet $\Sigma$ is denoted by
393: $\Sigma^*$, $\Sigma^+$ denotes the set of all non-empty words over
394: $\Sigma^*$, and $\lambda$ denotes the \emph{empty word}. The
395: \emph{length of the word} $w\in\Sigma^*$ is denoted by $\length{w}$\@.
396:
397: A \emph{deterministic word automaton} (DWA) is a tuple
398: $\autA=(Q,\Sigma,\delta,q_{\rmI},F)$, where $Q$ is a finite set of
399: states, $\Sigma$ is a finite alphabet,
400: $\delta:Q\times\Sigma\rightarrow Q$ is the transition function,
401: $q_{\rmI}\in Q$ is the initial state, and $F\subseteq Q$ is the set of
402: accepting states. The \emph{size} of $\autA$ is the cardinality of
403: $Q$\@. The \emph{language} of $\autA$ is
404: $L(\autA):=\set{w\in\Sigma^*}{\widehat{\delta}(q_{\rmI},w)\in F}$,
405: where $\widehat{\delta}(q,\lambda):=q$ and
406: $\widehat{\delta}(q,wb):=\delta(\widehat{\delta}(q,w),b)$, for $q\in
407: Q$, $b\in\Sigma$, and $w\in\Sigma^*$\@.
408: %%
409: A state $q\in Q$ is \emph{reachable} from $p\in Q$ if there is a word
410: $w\in\Sigma^*$ such that $\widehat{\delta}(p,w)=q$\@.
411:
412:
413: Let $\autA=(Q,\Sigma,\delta,q_{\rmI},F)$ be a DWA, where we assume
414: that every state is reachable from $q_{\rmI}$\@. Note that the states
415: that are not reachable from $q_{\rmI}$ have no affect on the language
416: of the DWA and can be eliminated.
417: %%
418: The states $p,q\in Q$ are \emph{equivalent}, $p\sim_{\autA} q$ for
419: short, if for all $w\in\Sigma^*$, we have that
420: $\widehat{\delta}(p,w)\in F$ iff $\widehat{\delta}(q,w)\in F$\@. We
421: omit the subscript in the relation $\sim_{\autA}$ if $\autA$ is clear
422: from the context.
423: %%
424: Note that $\mathbin{\sim}\subseteq Q\times Q$ is an equivalence
425: relation. We denote the equivalence class of $q\in Q$ by
426: $\widetilde{q}$\@.
427: %%
428: Since we assume that all states are reachable from $q_{\rmI}$, the
429: states $p,q\in Q$ can be merged iff $p\sim q$\@. We obtain the DWA
430: $\widetilde{\autA}:=(\set{\widetilde{q}}{q\in
431: Q},\Sigma,\widetilde{\delta},
432: \widetilde{q_{\rmI}},\set{\widetilde{q}}{q\in F})$ with
433: $\widetilde{\delta}(\widetilde{q},b):= \widetilde{\delta(q,b)}$, for
434: $q\in Q$ and $b\in\Sigma$\@. We have that
435: $L(\widetilde{\autA})=L(\autA)$ and $\widetilde{\autA}$ is
436: \emph{minimal}, \ie, for every DWA $\autB$ with $L(\autB)=L(\autA)$,
437: either $\autB$ has more states than $\widetilde{\autA}$ or $\autB$ is
438: isomorphic to $\widetilde{\autA}$\@.
439:
440:
441: %-------------------------------------------------------------------------
442: \section{Automata Constructions}
443: \label{AUTO}
444:
445: In this section, we investigate the automata for quantifier-free PA
446: formulas. In~\S\ref{subsec:encoding}, we define how DWAs recognize
447: sets of integers, in~\S\ref{subsec:(in)equations}, we provide optimal
448: automata constructions for linear (in)equa\-tions,
449: in~\S\ref{subsec:divisibility}, we give an automata construction for
450: the divisibility relation, and finally, in~\S\ref{subsec:qf_formulas},
451: we give an upper bound on the size of the minimal DWA for a
452: quantifier-free formula.
453:
454:
455: \subsection{Representing Sets of Integers with Automata}
456: \label{subsec:encoding}
457:
458: We use an idea that goes back at least to
459: B{\"u}chi~\citeyear{Buechi.1960} for using automata to recognize
460: tuples of numbers by mapping words to tuples of numbers. There are
461: many possibilities to represent integers as words. We use an encoding
462: similar to~\cite{Boigelot.1999,Wolper_Boigelot.2000}, which is based
463: on the $\varrho$'s complement representation of integers, where
464: $\varrho\geq 2$ and the most significant bit is the first digit.
465: %Other representations are discussed in~\S\ref{CONCL}\@.
466: %%
467: For the remainder of the
468: paper, we fix $\varrho\geq 2$ and let $\Sigma$ be the alphabet
469: $\{0,\dots,\varrho-1\}$\@.
470: \begin{definition}
471: For $b_{n-1}\dots b_0\in\Sigma^*$, we define $\tonats{b_{n-1}\dots
472: b_0}:=\sum_{0\leq i<n} \varrho^i b_i$\@. We generalize this
473: encoding to integers as follows. For $b_nb_{n-1}\dots
474: b_0\in\Sigma^+$, we define
475: \begin{equation*}
476: \toints{b_nb_{n-1}\dots b_0}:=
477: \tonats{b_{n-1}\dots b_0}
478: -
479: \begin{cases}
480: 0 & \text{if $b_n=0$,}
481: \\
482: \varrho^{n} & \text{if $b_n\not=0$\@.}
483: \end{cases}
484: \end{equation*}
485: We call the first letter $b_n$ the \emph{sign letter}, since it
486: determines whether the word represents a positive or a negative
487: number.
488: \end{definition}
489: %%
490: Note that the empty word $\lambda$ does not represent an integer.
491: This requirement saves us from considering some special cases in
492: \S\ref{subsubsec:opt_inequations} and
493: \S\ref{subsubsec:opt_inequations} where we optimize the automata
494: constructions for (in)equations. However, for the natural numbers, it
495: holds that $\tonats{\lambda}=0$\@. Furthermore, note that the
496: encoding of an integer is not unique.
497: %%
498: First, we have that $\toints{bu}=\toints{bcu}$, where $b,c\in\Sigma$
499: and $u\in\Sigma^*$ with $c=0$ if $b=0$ and $c=\varrho-1$, otherwise.
500: %%
501: Second, it holds that $\toints{bu}=\toints{b'u}$, for all
502: $u\in\Sigma^*$ and $b,b'\in\Sigma\setminus\{0\}$, \ie, the sign letter
503: $b\not=0$ can be replaced by any other letter $b'\not=0$\@. The
504: motivation for allowing any letter to be the sign letter is that we do
505: not have to deal with words in $\Sigma^+$ that do not represent an
506: integer. This eliminates case distinctions of the automata
507: constructions in the next subsections.
508:
509:
510: We extend the encoding to tuples of natural numbers and integers as
511: follows: A word
512: $w:=\overline{b}_{n-1}\dots\overline{b}_0\in(\Sigma^r)^*$
513: \emph{represents} the tuple $\overline{a}:=(a_1,\dots,a_r)\in\Nat^r$
514: of integers, where the $i$th ``track'' of the word $w$ encodes the
515: natural number $a_i$\@. That is, for all $1\leq i\leq r$, we have that
516: $a_i=\toints{b_{n-1,i}\dots b_{0,i}}$, where
517: $\overline{b}_j=(b_{j,1},\dots,b_{j,r})$ for $0\leq j<n$\@.
518: %%
519: The encoding of an integer tuple
520: $\overline{z}=(z_1,\dots,z_r)\in\Int^r$ is defined analogously for a
521: word
522: $w=\overline{b}_n\overline{b}_{n-1}\dots\overline{b}_0\in(\Sigma^r)^+$\@.
523: The first letter $\overline{b}_n$ of $w$ is the \emph{sign letter}
524: since it determines the signs of the integers $z_1,\dots,z_r$\@. We
525: define $\sigma(\overline{b}_n):=(c_1,\dots,c_r)$, where $c_i=0$ if the
526: $i$th coordinate of $\overline{b}_n$ is $0$ and $c_i=-1$, otherwise,
527: for each $1\leq i\leq r$\@.
528: %%
529: We abuse notation and write $\tonats{w}$ to denote the tuple
530: $\overline{a}\in\Nat^r$ and $\toints{w}$ to denote the integer tuple
531: $\overline{z}$\@.
532:
533: Moreover, we write $\towordsnats{\overline{a}}$ for the shortest word
534: in $(\Sigma^r)^*$ that represents $\overline{a}\in\Nat^r$\@. Note that
535: $\towordsnats{\overline{a}}$ is well-defined since (1)~there is a word
536: $w\in(\Sigma^r)^*$ with $\toints{w}=\overline{a}$, and (2)~if
537: $\tonats{v}=\tonats{v'}$ for $v,v'\in(\Sigma^r)^*$, then $v$ and $v'$
538: have a common suffix $u\in(\Sigma^r)^*$ with
539: $\tonats{u}=\tonats{v}$\@.
540: %%
541: Similar to $\towordsnats{\overline{a}}$ for $\overline{a}\in\Nat^r$,
542: we define $\towordsints{\overline{z}}$, for $\overline{z}\in\Int^r$,
543: as the shortest word $w\in(\Sigma^r)^+$ with $\overline{z}=\toints{w}$
544: and the first letter of $w$ is in $\{0,\varrho-1\}^r$\@.
545:
546:
547: \begin{definition}
548: Let $U\subseteq\Int^r$\@. The language $L\subseteq (\Sigma^r)^*$
549: \emph{represents} $U$ if $L=\set{w\in(\Sigma^r)^+}{\toints{w}\in
550: U}$\@.
551: %%
552: A DWA $\autA$ \emph{represents} $U$ if $L(\autA)$ represents $U$\@.
553: \end{definition}
554: Note that by this definition not every language over $\Sigma^r$
555: represents a set of tuples of integers, and not every DWA with
556: alphabet $\Sigma^r$ represents a subset of $\Int^r$\@.
557: %
558: %The language $L\subseteq(\Sigma^r)^*$ encodes a subset of $\Int^r$ iff
559: %$L$ satisfies the two properties: (1)~$\overline{b}u\in
560: %L\Leftrightarrow\overline{b}\overline{b}u\in L$, for all
561: %$u\in(\Sigma^r)^*$ and $\overline{b}\in\Sigma^r$, and (2)~$L$ contains
562: %only words that represent an integer tuple, \ie, $\lambda\not\in L$
563: %and for all $\overline{b}u\in L$ with $u\in(\Sigma^r)^*$ it holds that
564: %$\overline{b}\in\{0,\varrho-1\}^r$\@.
565: \begin{example}
566: The set of pairs $(x,y)\in\Int^2$ where $y$ equals $2x$ is
567: represented by the DWA depicted in
568: Figure~\ref{fig:ex_representing_integers} by using the base
569: $\varrho=2$ for representing integers as words, \ie, the alphabet of
570: the DWA is $\{0,1\}^2$\@. In the figure, we use abbreviations like
571: $(0,\textrm{--})$ to denote the letters $(0,0)$ and $(0,1)$\@.
572: \begin{figure}[t]
573: \centering
574: \includegraphics{images/ex_representing_integers-scaled}
575: %%epsffit 0 0 180 180 ex_representing_integers.eps ex_representing_integers-scaled.eps
576: \caption{DWA over the alphabet $\{0,1\}^2$ representing the set
577: $\set{(x,y)\in\Int^2}{y=2x}$\@.
578: \label{fig:ex_representing_integers}}
579: \end{figure}
580: \end{example}
581:
582:
583:
584:
585:
586: \subsection{Linear Equations and Inequations}
587: \label{subsec:(in)equations}
588:
589: In this subsection, we first recall the automata constructions given
590: in~\cite{Boigelot_Rassart_Wolper.1998,Boigelot.1999,Wolper_Boigelot.2000,Ganesh_Berezin_Dill.2002}
591: for linear (in)equa\-tions. Then, we improve these constructions such
592: that they are optimal, \ie, the constructed DWAs are minimal. Assume
593: that the (in)equa\-tion $t\ZAECKZAECK c$ is given in normalized form,
594: \ie, $t(x_1,\dots,x_r)$ is a homogeneous term,
595: $\zaeckzaeck\in\{=,\not=,<,\leq,>,\geq\}$, and $c\in\Int$\@.
596:
597:
598: First, we make the following observation for a word $u\in(\Sigma^r)^*$
599: and $\overline{b}\in\Sigma^r$\@. If $u\not=\lambda$ then
600: $\toints{u\overline{b}}=\varrho\toints{u}+\overline{b}$\@. For
601: $u=\lambda$, we have that
602: $\toints{\overline{b}}=\sigma(\overline{b})$\@.
603: %%
604: Given this, it is relatively straightforward to obtain an analog of a
605: DWA with \emph{infinitely} many states for $t\ZAECKZAECK c$\@. The set
606: of states is $\{q_{\rmI}\}\cup\Int$, where $q_{\rmI}$ is the initial
607: state. Note that we identify integers with states. The idea is to
608: keep track of the value of $t$ as successive bits are read. Thus,
609: except for the special initial state, a state in $\Int$ represents the
610: current value of $t$\@.
611: Lemma~\ref{lem:automaton_infinite_(in)equation} below justifies this
612: intuition. The transition function
613: $\eta:(\{q_{\rmI}\}\cup\Int)\times\Sigma^r\rightarrow(\{q_{\rmI}\}\cup\Int)$
614: is defined as follows for a letter $\overline{b}\in\Sigma^r$\@. For
615: the initial state, we define
616: $\eta(q_{\rmI},\overline{b}):=t[\sigma(\overline{b})]$\@. For
617: $q\in\Int$, we define $\eta(q,\overline{b}):= \varrho
618: q+t[\overline{b}]$\@.
619: \begin{lemma}
620: \label{lem:automaton_infinite_(in)equation}
621: For $u\in(\Sigma^r)^*$ of length $n\geq 0$ we have that
622: \begin{enumerate}[(a)]
623: \item $\widehat{\eta}(q,u)= \varrho^{n}q+t\bigl[\tonats{u}\bigr]$,
624: for $q\in\Int$, and
625: \item $\widehat{\eta}(q_{\rmI},\overline{b}u)=
626: t\bigl[\toints{\overline{b}u}\bigr]$, for
627: $\overline{b}\in\Sigma^r$\@.
628: \end{enumerate}
629: \end{lemma}
630: \begin{proof}
631: (a)~is easily proved by induction over $n$, and (b)~follows from~(a)
632: and the definition of $\eta$\@.
633: \end{proof}
634:
635: Later we make use of the following lemma, which translates the
636: question whether $q\in\Int$ is reachable from $p\in\Int$ via
637: $\widehat{\eta}$ to a number-theoretic problem.
638: \begin{lemma}
639: \label{lem:reachability_question}
640: Let $p,q\in\Int$\@. There are $N,a_1,\dots,a_r\geq 0$ such that
641: $N\geq\lceil\log_{\varrho}(1+\max\{a_1,\dots,a_r\})\rceil$ and
642: $\varrho^N p+t[a_1,\dots,a_r]=q$ iff there is a word
643: $w\in(\Sigma^r)^*$ such that $\widehat{\eta}(p,w)=q$\@.
644: \end{lemma}
645: \begin{proof}
646: ($\Rightarrow$)\
647: %%
648: Assume that $\towordsnats{a_1,\dots,a_r}$ has length $\ell$\@. Note
649: that $\ell\leq N$\@. This follows from the fact that for every
650: $a\in\Nat$, there is a word $u\in\Sigma^*$ of length
651: $\lceil\log_{\varrho}(1+a)\rceil$ such that $\tonats{u}=a$\@. By
652: Lemma~\ref{lem:automaton_infinite_(in)equation}(a), we have that
653: \begin{equation*}
654: \widehat{\eta}
655: \bigl(p,\overline{0}^{N-\ell}\towordsnats{a_1,\dots,a_r}\bigr)
656: =\varrho^N p+t[a_1,\dots,a_r]=q
657: \,.
658: \end{equation*}
659:
660: \vspace{\topsep}
661: \noindent
662: ($\Leftarrow)$\
663: %%
664: Assume that $\widehat{\eta}(p,w)=q$, for some $w\in(\Sigma^r)^*$\@.
665: Let $N$ be the length of $w$\@. We have that $N\geq
666: {\lceil\log_{\varrho}(1+a)\rceil}$, where $a$ is the largest number
667: in the tuple $\tonats{w}$\@.
668: %Note that for every $a\in\Nat$, there
669: %is a word $u\in\Sigma^*$ of length $\lceil\log_{\varrho}(1+a)\rceil$
670: %such that $\tonats{u}=a$\@.
671: %%
672: It follows from Lemma~\ref{lem:automaton_infinite_(in)equation}(a)
673: that $\widehat{\eta}(p,w)=\varrho^N p+t[\tonats{w}]$\@.
674: \end{proof}
675:
676: The automata constructions
677: in~\cite{Wolper_Boigelot.2000,Ganesh_Berezin_Dill.2002} are based on
678: the observation that the states $q,q'\in\Int$ can be merged if,
679: intuitively speaking, $q$ and $q'$ are both small or both large.
680: Here, the meaning of ``small'' and ``large'' depends on the
681: coefficients of $t$ and on the constant $c$\@. More precisely, we say
682: that $q\in\Int$ is \emph{small} if $q<\min\{c,-\normpos{t}\}$, and
683: \emph{large} if $q>\max\{c,\normneg{t}\}$, where
684: \begin{equation*}
685: \normneg{t}:=
686: \sum_{\substack{1\leq j\leq r\\\text{and }k_j<0}} \abs{k_j}
687: \qquad\text{and}\qquad
688: \normpos{t}:=
689: \sum_{\substack{1\leq j\leq r\\\text{and }k_j>0}} k_j
690: \end{equation*}
691: assuming that $t$ is of the form $k_1\CDOT x_1+\dots+k_r\CDOT x_r$\@.
692: %%Moreover, let $\norm{t}:=\normneg{t}+\normpos{t}$\@.
693: %
694: Note that from a small value we can only obtain smaller values and
695: from a large value we can only obtain larger values by $\eta$, \ie,
696: for all $\overline{b}\in\Sigma^r$, if $q>\normneg{t}$ then
697: $\eta(q,\overline{b})=\varrho q+t[\overline{b}]>q$, and if
698: $q<-\normpos{t}$ then $\eta(q,\overline{b})=\varrho
699: q+t[\overline{b}]<q$\@.
700: %
701: A difference between the constructions in~\cite{Wolper_Boigelot.2000}
702: and~\cite{Ganesh_Berezin_Dill.2002} are the bounds that determine the
703: meaning of ``small'' and ``large''.
704:
705: For $m<n$, we define $\autA^{t\ZAECKZAECK
706: c}_{(m,n)}:=(Q,\Sigma^r,\delta,q_{\rmI},F)$, where
707: $Q:=\{q_{\rmI}\}\cup\set{q\in\Int}{m\leq q\leq n}$ and
708: \begin{equation*}
709: \delta(q,\overline{b}):=\begin{cases}
710: m & \text{if $\eta(q,\overline{b})\leq m$,}\\
711: n & \text{if $\eta(q,\overline{b})\geq n$,}\\
712: \eta(q,\overline{b}) & \text{otherwise,}
713: \end{cases}
714: \end{equation*}
715: for $q\in Q$ and $\overline{b}\in\Sigma^r$\@. Moreover, let
716: $F:=\set{q\in Q\cap\Int}{q\zaeckzaeck c}$\@.
717: \begin{lemma}
718: \label{fact:bound_automata_(in)equation}
719: The DWA $\autA^{t\ZAECKZAECK c}_{(m,n)}$ represents
720: $\Zrepresents{t\ZAECKZAECK c}$ if $m$ is small and $n$ is large.
721: Moreover, $\autA^{t\ZAECKZAECK c}_{(m,n)}$ has $2+n-m$ states.
722: \end{lemma}
723: \begin{proof}
724: The fact that $\autA^{t\ZAECKZAECK c}_{(m,n)}$ represents
725: $\Zrepresents{t\ZAECKZAECK c}$ follows from
726: Lemma~\ref{lem:automaton_infinite_(in)equation}, and
727: $\autA^{t\ZAECKZAECK c}_{(m,n)}$ has $2+n-m$ states by definition.
728: \end{proof}
729:
730: In the following, we optimize the constructions such that the produced
731: DWA for an (in)equa\-tion is minimal. Moreover, we give a lower bound
732: on the minimal DWA for an (in)equa\-tion. However, these results are
733: not needed for the upper bound on the minimal DWA for a PA formula.
734: %%
735: In the remainder of this subsection, let $\autA^{t\ZAECKZAECK
736: c}_{(m,n)}= (Q,\Sigma^r,\delta,q_{\rmI},F)$ for the (in)equa\-tion
737: $t\ZAECKZAECK c$ with $m=\max\set{q\in\Int}{q\text{ is small}} $ and
738: $n=\min\set{q\in\Int}{q\text{ is large}}$\@. We restrict ourselves to
739: the cases where $\zaeckzaeck\in\{=,<,>\}$\@.
740: %
741: The cases with $\zaeckzaeck\in\{\not=,\leq,\geq\}$ reduce to the cases
742: for $=$, $<$, $>$ and complementation of DWAs, since $t\NOTEQ c$ is
743: logically equivalent to $\NEG t\EQ c$, $t\LEQ c$ is logically
744: equivalent to $\NEG t\GREATER c$, and $t\GEQ c$ is logically
745: equivalent to $\NEG t\LESS c$\@. Note that complementation of a DWA
746: can be done by flipping accepting and non-accepting states. After
747: complementation we have to make the initial state of the DWA
748: non-accepting since the empty word does not represent any integer
749: tuple. The resulting DWA is minimal iff the original DWA is minimal.
750:
751:
752: \subsubsection{Eliminating Unreachable States}
753:
754: An obvious optimization is to eliminate the states in $Q\cap\Int$ that
755: are not a multiple of the greatest common divisor of the absolute
756: values of the coefficients in the term $t$, since they are not
757: reachable from the initial state $q_{\rmI}$\@. We define the
758: \emph{greatest common divisor} of the term $t(x_1,\dots,x_r)$ as
759: $\gcd(t):=\gcd(\abs{k_1},\dots,\abs{k_r})$, where $k_i$ is the
760: coefficient of the variable $x_i$, for $1\leq i\leq r$\@.
761: \begin{lemma}
762: \label{lem:reachable}
763: The state $q\in Q\cap\Int$ is reachable from the initial state
764: $q_{\rmI}$ iff $q$ is a multiple of $\gcd(t)$\@.
765: \end{lemma}
766: \begin{proof}
767: ($\Rightarrow$)\ %
768: This direction is easy to prove by induction on the length of
769: $w\in(\Sigma^r)^*$ with $\widehat{\delta}(q_{\rmI},w)\in\Int$: for
770: all $\overline{b}\in\Sigma^r$, it holds that (i)
771: $\delta(q_{\rmI},\overline{b})=t[\sigma(\overline{b})]$ is a
772: multiple of $\gcd(t)$, and (ii) if
773: $\widehat{\delta}(q_{\rmI},w)\in\Int$ is a multiple of $\gcd(t)$
774: then $\varrho\widehat{\delta}(q_{\rmI},w) + t[\overline{b}]$ is a
775: multiple of $\gcd(t)$\@.
776:
777: \vspace{\topsep}
778: \noindent
779: ($\Leftarrow$)\ %
780: Assume that $q$ is a multiple of $\gcd(t)$\@. There are
781: $v_1,\dots,v_r\in\Int$ such that $t[v_1,\dots,v_r]=q$\@. With
782: Lemma~\ref{lem:automaton_infinite_(in)equation}(b) we conclude that
783: $\widehat{\delta}\bigl(q_{\rmI},\towordsints{v_1,\dots,v_r}\bigr)=
784: t[v_1,\dots,v_r]$\@.
785: \end{proof}
786:
787: Alternatively, instead of filtering out the states $q\in\Int$ that are
788: not a multiple of $\gcd(t)$ we can rewrite the (in)equa\-tion
789: $t\ZAECKZAECK c$ to the logically equivalent atomic formula $\alpha$
790: and then construct the DWA for $\alpha$, where $\alpha$ is defined as
791: \begin{equation*}
792: \alpha:=\begin{cases}
793: t'\ZAECKZAECK \bigl\lceil \frac{c}{\gcd(t)}\bigr\rceil
794: & \text{if $\zaeckzaeck$ is $<$,}
795: \\
796: t'\ZAECKZAECK\bigl\lfloor \frac{c}{\gcd(t)}\bigr\rfloor &
797: \text{if $\zaeckzaeck$ is $>$,}
798: \\
799: t'\ZAECKZAECK\frac{c}{\gcd(t)} & \text{if $\zaeckzaeck$ is $=$
800: and $c$ is a multiple of $\gcd(t)$,}
801: \\
802: 1<0 & \text{otherwise,}
803: \end{cases}
804: \end{equation*}
805: where the coefficients in $t'$ are the coefficients of $t$ divided
806: by $\gcd(t)$\@.
807: %%
808: In the remainder of this subsection we assume that $\gcd(t)=1$\@.
809:
810:
811: \subsubsection{Optimal Construction for Inequations}
812: \label{subsubsec:opt_inequations}
813:
814: In the following, we assume that the inequation is of the form
815: $t\GREATER c$, with $c\geq 0$\@. The cases where $\zaeckzaeck$ is $<$
816: or $c\geq 0$ are analogous. The following example illustrates that
817: many states of $\autA^{t\GREATER c}_{(m,n)}$ can be merged if $c$ is
818: significantly larger than $\normneg{t}$\@.
819: \begin{example}
820: \label{ex:minimal_inequation}
821: The automata construction described above for the inequation
822: $x-y\GREATER 32$ produces a DWA with the set of states
823: $Q=\{q_{\rmI},-2,-1,0,\dots,32,33\}$; but the minimal DWA (see
824: Figure~\ref{fig:minimal_automaton_inequation}) for $x-y>32$ has only
825: $13$ states when we choose the base $\varrho=2$\@.
826: \begin{figure}[t]
827: \centering
828: \includegraphics{images/minimal_automaton_inequation-scaled}
829: \caption{Minimal DWA over the alphabet $\{0,1\}^2$ for the inequation
830: $x-y>32$\@.
831: \label{fig:minimal_automaton_inequation}}
832: \end{figure}
833:
834: The reason for this gap is that several states can be merged.
835: %%
836: First, we merge the states $-2$ and $-1$ since from both states only
837: non-accepting states are reachable.
838: %%
839: Second, we can merge the states in $Q':=\set{q\in
840: Q\cap\Int}{2q+a-b>c, \text{ for all $a,b\in\{0,1\}$}}=
841: \{17,\dots,32\}$ to a single state since all states in $Q'$ are
842: non-accepting and all their transitions go to state $33$\@. The
843: state $16$ cannot be merged with any other state since if we read
844: the letter $(1,0)$, we end up in the accepting state $33$, and if we
845: read the letters $(0,0)$, $(1,1)$, or $(0,1)$ we end up in the
846: non-accepting states $32$ or $31$\@. The states in $\{9,\dots,15\}$
847: can again be merged to a single state since with every transition we
848: reach a state in $Q'$\@. Analogously, we can merge the states in
849: $\{5,6,7\}$\@.
850: \end{example}
851:
852: In the following, we determine the equivalent states in
853: $\autA^{t\GREATER c}_{(m,n)}$. Note that from
854: Lemma~\ref{lem:reachable} it follows that all states are reachable
855: from $q_{\rmI}$ since we assume that $\gcd(t)=1$\@. We use the
856: notation $[d,d')$ for the set $\{d,\dots,d'-1\}$ if $d,d'\in\Int$, and
857: if $d\in\Int$ and $d'=\infty$ then $[d,d'):=\set{z\in\Int}{z\geq
858: d}$\@.
859: %%
860: In order to identify the equivalent states, we define the following
861: strictly monotonically decreasing sequence $d_0>d_1>\dots>d_{\ell}$,
862: for some $\ell\geq 1$\@. Let $d_0:=\infty$ and
863: $d_1:=\max\{c+1,\normneg{t}\}$\@. Assume that $d_0>d_1>\dots>d_i$ are
864: already defined, for some $i\geq 1$\@.
865: \begin{itemize}
866: \item If $d_i=\normneg{t}$ then we are done, \ie, $\ell=i$\@.
867: \item If $d_i>\normneg{t}$ then let $d_{i+1}<d_i$ be the smallest
868: integer greater than $\normneg{t}-1$ such that for all
869: $\overline{b}\in\Sigma^r$, there is an index $j$ with $1\leq j\leq
870: i$ and
871: \begin{equation}
872: \label{eqn:interval}
873: \varrho d_{i+1}+t[\overline{b}],\,\,
874: \varrho (d_i-1)+t[\overline{b}]
875: \,\in\,[d_j,d_{j-1})
876: \,.
877: \end{equation}
878: Note that $d_{i+1}$ is well-defined since $d_i-1$
879: satisfies~(\ref{eqn:interval}), for all
880: $\overline{b}\in\Sigma^r$\@.
881: \end{itemize}
882:
883: The following lemma characterizes the equivalent states. In
884: particular, it shows that we can merge the states in
885: $R:=\{-\normpos{t}, \normpos{t}-1\}$, and for each $i\leq i\leq\ell$,
886: the states in $[d_i,d_{i-1})$ can be collapsed to one state.
887: \begin{lemma}
888: \label{lem:equivalent_states}
889: For all $p,q\in Q$, it holds that $p\sim q$ iff $p=q$ or $p,q\in R$
890: or $p,q\in[d_i,d_{i-1})$, for $1\leq i\leq\ell$\@.
891: \end{lemma}
892: \begin{proof}
893: ($\Leftarrow$)\ %
894: If $p=q$ then it is obvious that $p\sim q$\@. If $p,q\in R$ then we
895: also have that $p\sim q$, since both states are non-accepting and
896: all transitions from these states either go to $-\normpos{t}$ or to
897: $-\normpos{t}-1$\@.
898: %
899: It remains to prove that for $1\leq i\leq\ell$, if
900: $p,q\in[d_i,d_{i-1})$ then $p\sim q$\@. We prove this claim by
901: induction over $i$\@. For $i=1$, there is nothing to prove, since
902: $[d_1,d_0)\cap Q$ is a singleton. For the induction step, assume
903: that $i>1$ and let $p,q\in[d_i,d_{i-1})$\@. Without loss of
904: generality we assume that $p\leq q$\@. By the definition of the
905: transition function $\delta$ and the sequence
906: $d_0>d_1>\dots>d_{\ell}$, we have that
907: \begin{equation*}
908: \varrho d_i+t[\overline{b}]\leq
909: \delta(p,\overline{b})\leq
910: \delta(q,\overline{b})\leq
911: \varrho (d_{i-1}-1)+t[\overline{b}]
912: \,,
913: \end{equation*}
914: for all $\overline{b}\in\Sigma^r$\@. Since there is a $1\leq j<i$
915: with $\varrho d_i+t[\overline{b}], \varrho
916: d_{i-1}+t[\overline{b}]\in[d_j,d_{j-1})$ we conclude that
917: $\delta(p,\overline{b}),\delta(q,\overline{b})\in[d_j,d_{j-1})$\@.
918: The claim now follows from the induction hypothesis.
919:
920: \vspace{\topsep}
921: \noindent
922: ($\Rightarrow$)\ %
923: We prove the claim by contraposition, \ie, $p\not\sim q$ is implied
924: by the three conditions (i)~$p\not=q$, (ii)~$p\in R\Rightarrow
925: q\not\in R$, and (iii)~for all $1\leq i\leq \ell$, $p\in
926: [d_i,d_{i-1})\Rightarrow q\not\in [d_i,d_{i-1})$\@.
927: %%
928: Assume $p\not=q$\@. It suffices to distinguish the following three
929: cases.
930:
931: \newdef{case1}{Case}
932: \begin{case1}[{\rm\!\!: $p\in R$ and $q\not\in R$}]
933: Since we can reach an accepting state from $q$, we have that
934: $p\not\sim q$\@.
935: \end{case1}
936:
937: \begin{case1}[{\rm\!\!: $p\in[d_i,d_{i-1})$ and
938: $q\not\in[d_i,d_{i-1})$, for some $1\leq i\leq\ell$}]
939: It is straightforward to prove by induction
940: over $i$ that $p\not\sim q$\@.
941: \end{case1}
942:
943: \begin{case1}[{\rm\!\!: $p\not\in R\cup\bigcup_{1\leq
944: i\leq\ell}[d_i,d_{i-1})$}]
945: Note that the conditions~(ii) and~(iii) are satisfied. We have
946: that either $p=q_{\rmI}$ or $p\in S$, where $S:=\set{s\in
947: Q\cap\Int}{-\normpos{t}<s<\normneg{t}}$\@.
948:
949: If $p=q_{\rmI}$ and $q\in R$ then we conclude similar to Case~1
950: that $p\not\sim q$\@.
951: %%
952: Assume that $p=q_{\rmI}$ and $q\not\in R$\@. Let
953: $\overline{b}\in\Sigma^r$ be the letter that has a $0$ in its
954: $i$th coordinate iff the $i$th coefficient of $t$ is negative, and
955: otherwise the $i$th coordinate is $\varrho-1$\@. It holds that
956: $q_{\rmI}\not\sim q$, since
957: $\delta(q_{\rmI},\overline{b})=-t[\overline{b}]\in R$ and
958: $\delta(q,\overline{b})=\varrho q+\varrho\normpos{t}\geq q$\@.
959: From Case~1, it follows that $p\not\sim q$\@.
960:
961: Assume that $p\in S$\@. Note that for every $s\in S$ there is a
962: $\overline{b}\in\Sigma^r$ such that $\delta(s,\overline{b})\in
963: S$\@. It follows that for every $n\geq 0$ there is a word
964: $u\in(\Sigma^r)^*$ of length $n$ such that
965: $\widehat{\delta}(p,u)\in S$\@. We conclude that there is a word
966: $u\in(\Sigma^r)^*$ such that $\widehat{\delta}(p,u)\in S$ and
967: $\widehat{\delta}(q,u)\in R \cup\bigcup_{1\leq
968: i\leq\ell}[d_i,d_{i-1})$, since
969: $\delta(s,\overline{b})-\delta(s',\overline{b})=\varrho(s-s')$,
970: for all $s,s'\in S$ and all $\overline{b}\in\Sigma^r$\@.
971: Analogously to the Cases~1 and~2 we conclude that $p\not\sim q$\@.
972: \qed
973: \end{case1}
974: \end{proof}
975:
976: From Lemma~\ref{lem:equivalent_states}, it follows that the minimal
977: DWA representing $\Zrepresents{t\GREATER c}$ has at least
978: $\normneg{t}+\normpos{t}$ states. Note that this is in contrast to
979: the number of symbols we need to write the inequation $t\GREATER c$ if
980: coefficients are represented as binary numbers. For instance, we need
981: $22+7$ letters for $1025\cdot x-1024\cdot y\GREATER 0$, since each of
982: the two coefficients can be represented with $11$ digits. The same
983: lower bound on the minimal DWA size holds for $t\LESS c$\@. In the
984: following, we show that a similar lower bound holds for equations.
985:
986:
987:
988: \subsubsection{Optimal Construction for Equations}
989: \label{subsubsec:opt_equations}
990:
991: For an equation $t\EQ c$, we can collapse the states in $\autA^{t\EQ
992: c}_{(m,n)}$ from which we cannot reach the accepting state $c\in Q$
993: to a single non-accepting state.
994: %Additionally, if $t\EQ c$ is one of
995: %the equations $x_1\EQ 0$, $-x_1\EQ 0$, $x_1-x_2\EQ 0$, or $-x_1+x_2\EQ
996: %0$ we can merge the states $q_{\rmI}$ and $0$\@.
997: These optimizations produce the minimal DWA for $t\EQ c$\@. For
998: instance, the case for $p\in Q\cap\Int$ is proved as follows. Assume
999: that we can reach the state $c$ from $p\in Q\cap\Int$, \ie, there is a
1000: $u\in(\Sigma^r)^*$, with $\widehat{\delta}(p,u)=c$\@. Any other
1001: states $q\in Q\cap\Int$ with $q\not=p$ from which we can reach $c$
1002: cannot be merged with $p$, since
1003: \begin{equation*}
1004: c
1005: =
1006: \widehat{\delta}(p,u)
1007: \,\overset{\textup{Lemma~\ref{lem:automaton_infinite_(in)equation}(a)}}{=}\,
1008: \varrho^{\length{u}} p+t\bigl[\tonats{u}\bigr]\not=
1009: \varrho^{\length{u}} q+t\bigl[\tonats{u}\bigr]
1010: \,\overset{\textup{Lemma~\ref{lem:automaton_infinite_(in)equation}(a)}}{=}\,
1011: \widehat{\delta}(q,u)
1012: \,.
1013: \end{equation*}
1014: The other cases are proved similarly.
1015:
1016:
1017: A lower bound for the minimal DWA representing $\Zrepresents{t\EQ c}$
1018: is based on the following lemma about the states of the DWA
1019: $\autA^{t\ZAECKZAECK c}_{(m,n)}=(Q,\Sigma^r,\delta,q_{\rmI},F)$, where
1020: $\zaeckzaeck\in\{=,\not=,<,\leq,>,\geq\}$\@. Let $S:=\set{s\in
1021: Q\cap\Int}{-\normpos{t}<s<\normneg{t}}$ and $[n]:=\{0,\dots,n-1\}$,
1022: for $n\geq 0$\@.
1023: \begin{lemma}
1024: \label{lem:S}
1025: Every $q\in Q\cap\Int$ is reachable from every $p\in S$\@.
1026: \end{lemma}
1027: \begin{proof}
1028: We need a result from number theory. Let $\gamma>0$ and let
1029: $c_1,\dots,c_{\gamma}$ be integers with $0<c_1<\dots<c_{\gamma}$ and
1030: $\gcd(c_1,\dots,c_{\gamma})=1$\@. The \emph{Frobenius number}
1031: $G(c_1,\dots,c_{\gamma})$ is the greatest integer $z$ for which the
1032: linear equation $c_1\cdot x_1+\dots+c_{\gamma}\cdot x_{\gamma}\EQ z$
1033: has \emph{no} solution in the natural numbers. For $\gamma=1$, it
1034: trivially holds that $G(c_1)=-1$\@. For $\gamma>1$, the upper bound
1035: $G(c_1,\dots,c_{\gamma})\leq\frac{c_{\gamma}^2}{\gamma-1}$ was
1036: proved by~\citeN{Dixmier.1990}\@. It is straightforward to show that
1037: for all $\gamma>0$,
1038: \begin{equation}
1039: \label{eqn:Frobenius}
1040: G(c_1,\dots,c_{\gamma})
1041: <
1042: \varrho^{c_1+\dots+c_{\gamma}}-(c_1+\dots+c_{\gamma})
1043: \,.
1044: \end{equation}
1045:
1046: In the following, we will prove the lemma, \ie, for $p\in S$ and
1047: $q\in Q\cap\Int$ there is a word $u\in(\Sigma^r)^*$ such that
1048: $\widehat{\delta}(p,u)=q$\@. Note that if $r=0$ and $r=1$ then
1049: $S=\emptyset$ and the claim is trivially true. Assume that $r\geq
1050: 2$\@. By Lemma~\ref{lem:reachability_question}, it suffices to show
1051: that the equation
1052: \begin{equation}
1053: \label{eqn:claim}
1054: \varrho^Np+t(x_1,\dots,x_r)=q
1055: \end{equation}
1056: has a solution $a_1,\dots,a_r\geq 0$ with
1057: $N\geq\lceil\log_{\varrho}(1+\max\{a_1,\dots,a_r\})\rceil$\@. We
1058: distinguish four cases depending on $p$ and $q$\@.
1059:
1060: \newdef{case2}{Case}
1061: \begin{case2}[{\rm\!\!: $p=0$}]
1062: Equation~(\ref{eqn:claim}) simplifies to
1063: \begin{equation}
1064: \label{eqn:case_0}
1065: t(x_1,\dots,x_r)=q
1066: \,.
1067: \end{equation}
1068: There are positive and negative coefficients in $t$, since $p\in
1069: S$\@. It follows that equation~(\ref{eqn:case_0}) has infinitely
1070: many solutions in the natural numbers. Recall that we assume that
1071: $\gcd(t)=1$\@. In particular, there are $a_1,\dots,a_r\geq 0$
1072: with $\varrho^Np+t[a_1,\dots,a_r]=q$, for some appropriate large
1073: enough $N$\@.
1074: \end{case2}
1075:
1076: \begin{case2}[{\rm\!\!: $p>0$ and $q\geq 0$}]
1077: %%Assume that $t$ is of the form $k_1\CDOT x_1+\dots+k_r\CDOT x_r$
1078: %%with $k_i\not=0$, for all $1\leq i\leq r$\@.
1079: %%Let $i_1,\dots,i_{\mu}$ be the indices of the positive
1080: %%coefficients, \ie, $k_{i_{\xi}}>0$, for all $1\leq\xi\leq\mu$, and
1081: %%let $j_1,\dots,j_{\nu}$ be the indices of the negative
1082: %%coefficients, \ie, $k_{i_{\xi}}<0$, for all $1\leq\xi\leq\nu$\@.
1083: %%
1084: Let $k_{i_1},\dots,k_{i_{\mu}}$ be the positive coefficients in
1085: $t$, and let $k_{j_1},\dots,k_{j_{\nu}}$ be the negative
1086: coefficients in $t$\@.
1087: %%
1088: Let $N$ be the size of the DWA $\autA^{t\ZAECKZAECK c}_{(m,n)}$,
1089: \ie, $N=3+\max\{|c|,\normpos{t}\}+\max\{c,\normneg{t}\}$\@. We
1090: rewrite equation~(\ref{eqn:claim}) to
1091: \begin{equation}
1092: \label{eqn:case_++}
1093: \varrho^Np-q+
1094: t_1(x_{i_1},\dots, x_{i_{\mu}})
1095: %%k_{i_1}\cdot x_{i_1}+\dots+k_{i_{\mu}}\cdot x_{i_{\mu}}
1096: =
1097: t_2(x_{j_1},\dots, x_{j_{\nu}})
1098: %%|k_{j_1}|\cdot x_{j_1}+\dots+|k_{j_{\nu}}|\cdot x_{j_{\nu}}
1099: \,,
1100: \end{equation}
1101: where $t_1$ is the term $k_{i_1}\CDOT
1102: x_{i_1}+\dots+k_{i_{\mu}}\CDOT x_{i_{\mu}}$, and $t_2$ is the term
1103: $|k_{j_1}|\cdot x_{j_1}+\dots+|k_{j_{\nu}}|\cdot x_{j_{\nu}}$\@.
1104: Note that $\varrho^Np-q\geq0$ since $p>0$ and $\varrho^N\geq q$\@.
1105: Let $D:=\gcd(|k_{j_1}|,\dots,|k_{j_{\nu}}|)$\@. In order to show
1106: the existence of a solution $a_1,\dots,a_r\in[\varrho^N]$ of
1107: equation~(\ref{eqn:case_++}), we proceed in two steps:
1108: \begin{itemize}
1109: \item[\bf Step 1:] There are $a_{i_1},\dots,a_{i_{\mu}}\in[D]$ such
1110: that
1111: \begin{equation*}
1112: D
1113: \DIVIDES
1114: \varrho^Np-q+t_1[a_{i_1},\dots,a_{i_{\mu}}]
1115: %%p\varrho^Np-q+k_{i_1}a_{i_1}+\dots+k_{i_{\mu}}a_{i_{\mu}}
1116: \,.
1117: \end{equation*}
1118: \item[\bf Step 2:] There are $a_{j_1},\dots,a_{j_{\nu}}\in[\varrho^N]$ such
1119: that
1120: \begin{equation*}
1121: \varrho^Np-q+t_1[a_{i_1},\dots,a_{i_{\mu}}]
1122: %%\varrho^Np-q+k_{i_1}a_{i_1}+\dots+k_{i_{\mu}}a_{i_{\mu}}
1123: =
1124: t_2[a_{j_1},\dots,a_{j_{\nu}}]
1125: %%|k_{j_1}|a_{j_1}+\dots+|k_{j_{\nu}}|a_{j_{\nu}}
1126: \,.
1127: \end{equation*}
1128: \end{itemize}
1129:
1130: \vspace{\topsep}
1131: \noindent
1132: \textbf{Proof of Step~1:}
1133: %%
1134: If $\mu=0$ then there is nothing to prove. Assume that $\mu>0$\@.
1135: There are $K,R\geq 0$ such that $\varrho^Np-q=DK+R$ with $R<D$\@.
1136: It suffices to show that there are $a_{i_1},\dots,a_{i_{\mu}}$
1137: with $0\leq a_{i_1},\dots,a_{i_{\mu}}<D$, and $K'\geq 0$, such
1138: that $DK'=R+t_1[a_{i_1},\dots,a_{i_{\mu}}]$, since then
1139: \begin{equation*}
1140: \begin{array}{@{}l@{\,}c@{\,}l@{}}
1141: \varrho^Np-q+
1142: t_1[a_{i_1},\dots,a_{i_{\mu}}]
1143: %%k_{i_1}a_{i_1}+\dots+k_{i_{\mu}}a_{i_{\mu}}
1144: &=&
1145: DK+R + t_1[a_{i_1},\dots,a_{i_{\mu}}]
1146: %%k_{i_1}a_{i_1}+\dots+k_{i_{\mu}}a_{i_{\mu}}
1147: =
1148: DK +DK'
1149: \\
1150: &=&
1151: D(K+K')
1152: \,,
1153: \end{array}
1154: \end{equation*}
1155: and thus, $D\divides \varrho^Np-q+t_1[a_{i_1},\dots,a_{i_{\mu}}]$\@.
1156:
1157: First, assume the existence of $a_{i_1},\dots,a_{i_{\mu}}\geq 0$
1158: with $D\divides R+t_1[a_{i_1},\dots,a_{i_{\mu}}]$, where
1159: $a_{i_{\xi}}\geq D$, for some $1\leq\xi\leq\mu$\@. To simplify
1160: matters, we assume without loss of generality that $\xi=1$\@.
1161: There is an $a\geq 0$ with $a_{i_1}=D+a$\@.
1162: %%
1163: Further, assume that there is no $b<a_{i_1}$ with $D\divides
1164: R+t_1[b,a_{i_2},\dots,a_{i_{\mu}}]$\@. For some $K'\geq 0$, we
1165: have that
1166: \begin{equation*}
1167: DK'
1168: \!=\!
1169: R + t_1[a_{i_1},\dots,a_{i_{\mu}}]
1170: \!=\!
1171: R+Dk_{i_1}\!+ t_1[a,a_{i_2},\dots,a_{i_{\mu}}]
1172: \,.
1173: \end{equation*}
1174: Therefore, $D(K'-k_{i_1}) = R + t_1[a,a_{i_2},\dots,a_{i_{\mu}}]$,
1175: \ie, $D\divides R + t_1[a, a_{i_2},\dots,a_{i_{\mu}}]$\@. This
1176: contradicts the minimality of $D+a$\@.
1177:
1178: It remains to show the existence of $a_{i_1},\dots,a_{i_{\mu}}\geq
1179: 0$ with $D\divides R+t_1[a_{i_1},\dots,a_{i_{\mu}}]$\@. The
1180: existence reduces to the problem of whether the equation
1181: \begin{equation*}
1182: D\CDOT y-k_{i_1}\CDOT x_{i_1}-\dots-k_{i_{\mu}}\CDOT x_{i_{\mu}}
1183: =
1184: R
1185: \end{equation*}
1186: has a solution in the natural numbers. This is the case since
1187: $\gcd(D,k_{i_1},\dots,k_{i_{\mu}})=1$, by assumption.
1188:
1189: \vspace{\topsep}
1190: \noindent
1191: \textbf{Proof of Step~2:}
1192: %%
1193: Assume that there are $\gamma\geq 1$ distinct coefficients in
1194: $t_2$ of equation~(\ref{eqn:case_++})\@. Without loss of
1195: generality, assume that $0<|k_{j_1}|<\dots<|k_{j_{\gamma}}|$\@.
1196: %%
1197: Let $W:=\frac{\varrho^Np-q+t_1[a_{i_1},\dots,a_{i_{\mu}}]}{D}$
1198: and
1199: $\ell_{\xi}:=\frac{|k_{j_{\xi}}|}{D}$, for $1\leq\xi\leq\nu$\@.
1200: Note that $\ell_1<\dots<\ell_{\gamma}$ and that
1201: $\gcd(\ell_1,\dots,\ell_{\gamma})=1$\@.
1202: %%
1203: Equation~(\ref{eqn:case_++}) simplifies with the $a_i$s from
1204: Step~$1$ to
1205: \begin{equation}
1206: \label{eqn:case_++_simplified}
1207: W
1208: =
1209: \ell_1\cdot x_{j_1}+\dots+\ell_{\nu}\cdot x_{j_{\nu}}
1210: \,.
1211: \end{equation}
1212: An upper bound on $W$ is
1213: \begin{equation}
1214: \label{eqn:upper_bound_W}
1215: \begin{array}{@{}l@{\,}c@{\,}l@{}}
1216: W
1217: &\leq&
1218: \frac{\varrho^Np-q+(\varrho-1)\normpos{t}}{D}
1219: \leq
1220: \frac{\varrho^N(\normneg{t}-1)+(\varrho-1)\normpos{t}}{D}
1221: \\
1222: &=&
1223: \frac{\varrho^N\normneg{t}}{D}-
1224: \frac{\varrho^N}{D}+
1225: \frac{(\varrho-1)\normpos{t}}{D}
1226: \end{array}
1227: \end{equation}
1228: and a lower bound on $W$ is
1229: \begin{equation*}
1230: \begin{array}{@{}l@{\,}c@{\,}l@{}}
1231: W
1232: &\geq&
1233: \frac{\varrho^N-q}{D}
1234: \geq
1235: \frac{\varrho^N-\max\{c,\normneg{t}\}}{D}
1236: \geq
1237: \frac{\varrho^{D(\ell_1+\dots+\ell_{\nu})}-D(\ell_1+\dots+\ell_{\nu})}{D}
1238: \\[3pt]
1239: &\geq&
1240: \varrho^{\ell_1+\dots+\ell_{\gamma}}-(\ell_1+\dots+\ell_{\gamma})
1241: \,.
1242: \end{array}
1243: \end{equation*}
1244:
1245: From the lower bound on $W$ and the upper bound on Frobenius
1246: numbers~(\ref{eqn:Frobenius}), it follows that
1247: equation~(\ref{eqn:case_++_simplified}) has a solution in the
1248: natural numbers. Let $\kappa\geq 0$ be maximal such that there
1249: are $a_1,\dots,a_{\gamma}\geq 0$ with
1250: \begin{equation}
1251: \label{eqn:solution_W}
1252: W
1253: =
1254: \ell_1a_1+\dots+\ell_{\gamma}a_{\gamma}+\kappa L
1255: \,,
1256: \end{equation}
1257: where $L:=\frac{\normneg{t}}{D}$\@. By contradiction, we obtain
1258: that $a_1,\dots,a_{\gamma}<L$: Assume that there is a $\xi$,
1259: $1\leq\xi\leq\gamma$ with $a_{\xi}=L+a$, for some $a\geq 0$\@.
1260: Without loss of generality, assume that $\xi=1$\@. This
1261: contradicts the assumption that $\kappa$ is maximal:
1262: \begin{equation*}
1263: \begin{array}{@{}l@{\,}c@{\,}l@{}}
1264: W
1265: &=&
1266: \kappa L + \ell_1(L+a) + \ell_2a_2+\dots+\ell_{\gamma}a_{\gamma}
1267: \\
1268: &=&
1269: (\kappa+\ell_1)L + \ell_1a + \ell_2a_2+\dots+\ell_{\gamma}a_{\gamma}
1270: \,.
1271: \end{array}
1272: \end{equation*}
1273:
1274: From $\kappa$ and $a_1,\dots,a_{\gamma}$, we obtain a solution for
1275: equation~(\ref{eqn:case_++_simplified}) in the natural numbers,
1276: namely
1277: \begin{equation*}
1278: \begin{array}{@{}l@{\,}c@{\,}l@{}}
1279: W
1280: &=&
1281: \kappa L+\ell_1a_1+\dots+\ell_{\gamma}a_{\gamma}
1282: \\
1283: &=&
1284: \kappa (\ell_1+\dots+\ell_{\nu}) +
1285: \ell_1a_1+\dots+\ell_{\gamma}a_{\gamma}
1286: \\
1287: &=&
1288: \ell_1(\kappa+a_1)+\dots+\ell_{\gamma}(\kappa+a_{\gamma})+
1289: \ell_{\gamma+1}\kappa+\dots+\ell_{\nu}\kappa
1290: \,.
1291: \end{array}
1292: \end{equation*}
1293:
1294: It suffices to show that $\kappa<
1295: \varrho^N-\max\{a_1,\dots,a_{\gamma}\}$\@. An upper bound on
1296: $\kappa$ is
1297: \begin{equation*}
1298: \begin{array}{@{}l@{\,}c@{\,}l@{}}
1299: \kappa
1300: &\overset{(\ref{eqn:solution_W})}{=}&
1301: \frac{W-(\ell_1a_1+\dots+\ell_{\gamma}a_{\gamma})}{L}
1302: \\
1303: &\leq&
1304: \frac{W}{L}-\frac{\max\{a_1,\dots,a_{\gamma}\}}{L}
1305: \\
1306: &\overset{(\ref{eqn:upper_bound_W})}{\leq}&
1307: % \frac{p\varrho^N-q+(\varrho-1)\normpos{t}}{DL}-\frac{\max\{a_1,\dots,a_{\gamma}\}}{L}
1308: % \\[3pt]
1309: % &\leq&
1310: \frac{\varrho^N\normneg{t}}{DL}-
1311: \frac{\varrho^N}{DL}+
1312: \frac{(\varrho-1)\normpos{t}}{DL}-
1313: \frac{\max\{a_1,\dots,a_{\gamma}\}}{L}
1314: \\[3pt]
1315: &\leq&
1316: \varrho^N-\frac{\varrho^N}{DL}+
1317: \frac{(\varrho-1)\normpos{t}-\max\{a_1,\dots,a_{\gamma}\}}{L}
1318: \,.
1319: \end{array}
1320: \end{equation*}
1321: It remains to check whether the inequality
1322: \begin{equation*}
1323: \begin{array}{@{}l@{}}
1324: \varrho^N-\frac{\varrho^N}{DL}+\frac{(\varrho-1)\normpos{t}-\max\{a_1,\dots,a_{\gamma}\}}{L}
1325: <
1326: \varrho^N-\max\{a_1,\dots,a_{\gamma}\}
1327: \end{array}
1328: \end{equation*}
1329: is valid. The previous inequality simplifies to
1330: \begin{equation*}
1331: \begin{array}{@{}c@{}}
1332: \frac{(\varrho-1)\normpos{t}+\max\{a_1,\dots,a_{\gamma}\}(L-1)}{L}
1333: <
1334: \frac{\varrho^N}{DL}
1335: \,.
1336: \end{array}
1337: \end{equation*}
1338: Multiplying with the common denominator $DL$, the inequality
1339: simplifies further to
1340: \begin{equation*}
1341: D(\varrho-1)\normpos{t}+D\max\{a_1,\dots,a_{\gamma}\}(L-1)
1342: <
1343: \varrho^N
1344: \,.
1345: \end{equation*}
1346: Since $\max\{a_1,\dots,a_{\gamma}\}\leq L-1$ and
1347: $N\geq\normneg{t}+\normpos{t}=DL+\normpos{t}$, it suffices to show
1348: the validity of the inequality
1349: \begin{equation}
1350: \label{eqn:case_++_final_inequality}
1351: D(\varrho-1)\normpos{t}+D(L-1)^2
1352: <
1353: \varrho^{DL+\normpos{t}}
1354: \,.
1355: \end{equation}
1356: It is straightforward to show that the
1357: inequality~(\ref{eqn:case_++_final_inequality}) is true for all
1358: $D,L\geq 1$ and $\normpos{t}\geq 0$\@.
1359: \end{case2}
1360:
1361: \begin{case2}[{\rm\!\!: $p<0$ and $q\leq 0$}]
1362: % This case is symmetric to Case~2\@. Note that there is at least
1363: % one positive coefficient in $t$ since $p<0$\@.
1364: %
1365: It suffices to prove that there is a solution
1366: $a_1,\dots,a_r\in[\varrho^N]$ for the equation
1367: \begin{equation*}
1368: \label{eqn:case_--}
1369: t_1(x_{i_1},\dots,x_{i_{\mu}})
1370: %%k_{i_1}\cdot x_{i_1}+\dots+k_{i_{\mu}}\cdot x_{i_{\mu}}
1371: =
1372: \varrho^N|p|-|q|+
1373: t_2(x_{j_1},\dots,x_{j_{\nu}})
1374: %%|k_{j_1}|\cdot x_{j_1}+\dots+|k_{j_{\mu}}|\cdot x_{j_{\nu}}
1375: \,,
1376: \end{equation*}
1377: where $t_1$ and $t_2$ are defined as in Case~2\@. This equation is
1378: similar to equation~(\ref{eqn:case_++}) except $t_1$ and $t_2$ are
1379: swapped. We can use a similar argumentation as in Case~2 for showing
1380: the existence of $a_1,\dots,a_r\in[\varrho^N]$\@.
1381: \end{case2}
1382:
1383: \begin{case2}[{\rm\!\!: $p>0$ and $q<0$}]
1384: This case can be solved with Case~1 and Case~2\@. Since $p>0$ and
1385: $q<0$, we have that $0\in S$\@. By Case~2, the state $0$ is
1386: reachable from $p$, and by Case~1, $q$ is reachable from state
1387: $0$\@.
1388: \end{case2}
1389:
1390: \begin{case2}[{\rm\!\!: $p<0$ and $q>0$}]
1391: Analogously, this case can be solved by Case~3 and Case~1\@.
1392: \qed
1393: \end{case2}
1394: \end{proof}
1395:
1396: With Lemma~\ref{lem:S} at hand, it is straightforward to prove for
1397: $\autA^{t\ZAECKZAECK c}_{(m,n)}$ that $p\sim q$ iff $p=q$, for all
1398: $p,q\in S$\@. Therefore, we have that the minimal automaton
1399: representing $\Zrepresents{t\EQ c}$ has at least $|S|$ states.
1400:
1401: Another consequence of Lemma~\ref{lem:S} is that $S$ is a strongly
1402: connected component in $\autA^{t\ZAECKZAECK c}_{(m,n)}$: By
1403: Lemma~\ref{lem:S}, every state $q\in S$ is reachable from every $p\in
1404: S$, and it is easy to show that the initial state $q_{\rmI}$ is not
1405: reachable from a state in $S$ and that a state in $S$ cannot be
1406: reached from any state that is not in $S\cup\{q_{\rmI}\}$\@.
1407:
1408:
1409:
1410: %%%
1411: \subsection{Divisibility Relation}
1412: \label{subsec:divisibility}
1413:
1414: In this subsection, we give an upper bound of the size of the minimal
1415: DWA for a formula $d\divides t+c$, where $d\geq 2$, $t(x_1,\dots,x_r)$
1416: is a homogeneous term, and $c\in\Int$\@.
1417:
1418: Let $\autA^{d\divides t+c}$ be the DWA with the set of states
1419: $Q:=\{q_{\rmI},0,1,\dots,d-1\}$\@. A state $q\in Q\cap\Int$ has an
1420: intuitive interpretation: if we reach the state $q$ with a word $w\in
1421: (\Sigma^r)^*$ then the remainder of the division of $t[\toints{w}]$ by
1422: $d$ equals $q$\@. We denote by $\remainder(q,d)$ the remainder of
1423: $q\in\Int$ divided by $d$\@. Let $\autA^{d\divides
1424: t+c}:=(Q,\Sigma^r,\delta,q_{\rmI},F)$ with
1425: \begin{equation*}
1426: \delta(q,\overline{b}):=
1427: \begin{cases}
1428: \remainder\bigl(t[\sigma(\overline{b})],d\bigr) &
1429: \text{if $q=q_{\rmI}$,} \\
1430: \remainder\bigl(\varrho q+t[\overline{b}],d\bigr)&
1431: \text{otherwise,}
1432: \end{cases}
1433: \end{equation*}
1434: for $q\in Q$ and $\overline{b}\in\Sigma^r$, and $F:=\set{q\in
1435: Q\cap\Int}{d\divides q+c}$\@. Note that there is exactly one $q\in
1436: Q\cap\Int$ with $d\divides q+c$\@.
1437:
1438:
1439: The correctness of our construction follows from two facts:
1440: \begin{enumerate}[(a)]
1441: \item \label{enum:divides_remainder}%
1442: For $n\in\Int$, $d\divides n+c$ iff
1443: $d\divides\remainder(n,d)+c$\@.
1444: \item \label{enum:transition_function_remainder}%
1445: For $w\in(\Sigma^r)^+$,
1446: $\widehat{\delta}(q_{\rmI},w)=\remainder\bigl(t[\toints{w}],d\bigr)$\@.
1447: \end{enumerate}
1448: The proof of~(\ref{enum:divides_remainder}) is straightforward. There
1449: are $p,q\in\Int$ such that $pd+q=n$ and $0\leq q<d$\@. Note that
1450: $q=\remainder(n,d)$\@. By definition, $d\divides n+c$ iff there is a
1451: $k\in\Int$ with $dk=n+c=pd+q+c$\@. The equality can be rewritten to
1452: $d(k-p)=q+c$, \ie, $d\divides \remainder(n,d)+c$\@.
1453:
1454: We prove~(\ref{enum:transition_function_remainder}) by induction over
1455: the length of $w$\@. For the base case, let
1456: $w=\overline{b}\in\Sigma^r$\@. Since we represent integers using
1457: $\varrho$'s complement, we have that
1458: $t[\toints{\overline{b}}]=t[\sigma(\overline{b})]$\@. By definition,
1459: $\widehat{\delta}(q_{\rmI},\overline{b})=
1460: \remainder\bigl(t[\toints{\overline{b}}],d\bigr)$\@.
1461: %%
1462: For the step case, assume
1463: $\widehat{\delta}(q_{\rmI},w)=\remainder\bigl(t[\toints{w}],d\bigr)$
1464: and let $\overline{b}\in\Sigma^r$\@.
1465: %%
1466: There are $p,q\in\Int$ with $t[\toints{w}]=pd+q$ and $0\leq q<d$\@.
1467: Note that $q=\remainder\bigl(t[\toints{w}],d\bigr)$ and
1468: $t[\toints{w\overline{b}}]=\varrho
1469: t[\toints{w}]+t[\overline{b}]=\varrho pd+\varrho q+t[\overline{b}]$\@.
1470: We have that
1471: \begin{equation*}
1472: \begin{array}{@{}l@{\,}c@{\,}l@{}}
1473: \remainder\bigl(t[\toints{w\overline{b}}],d\bigr)
1474: &=&
1475: \remainder(\varrho pd+\varrho q+t[\overline{b}],d)
1476: \\
1477: &=&
1478: \remainder(\varrho q+t[\overline{b}],d)=
1479: \delta(q,\overline{b})
1480: \\
1481: &\overset{\textup{IH}}{=}&
1482: \delta(\widehat{\delta}(q_{\rmI},w),\overline{b})
1483: =\widehat{\delta}(q_{\rmI},w\overline{b})
1484: \,.
1485: \end{array}
1486: \end{equation*}
1487: \begin{lemma}
1488: \label{fact:bound_automata_divisibiliy}
1489: The DWA $\autA^{d\divides t+c}$ represents $\Zrepresents{d\divides
1490: t+c}$ and has $d+1$ states.
1491: \end{lemma}
1492:
1493: An optimization of the construction is to filter out the states that
1494: are not a multiple of $\gcd(\gcd(t),d)$\@. These states are not
1495: reachable from the initial state since $\remainder(t[\overline{a}],d)$
1496: is a multiple of $\gcd(\gcd(t),d)$, for every
1497: $\overline{a}\in\Int^r$\@.
1498: %Additionally, we can merge states from
1499: %which we cannot reach an accepting state.
1500:
1501:
1502: %%%
1503: \subsection{Quantifier-free Formulas}
1504: \label{subsec:qf_formulas}
1505:
1506: In this subsection, we give an upper bound on the size of the minimal
1507: DWA for a quantifier-free PA formula. This upper bound depends on the
1508: maximal absolute value of the constants occurring in the
1509: (in)equa\-tions of the formula, the homogeneous terms, and the
1510: divisibility relations. The upper bound does \emph{not} depend on the
1511: Boolean combination of the atomic formulas.
1512: %
1513: This is not obvious since Boolean connectives are handled by the
1514: product construction if we construct the DWA recursively over the
1515: structure of the quantifier-free formula. The size of the resultant
1516: DWA using the product construction is in the worst case the product of
1517: the number of states of the two DWAs.
1518: %
1519: %Note that we allow the connective $\leftrightarrow$\@. Eliminating
1520: %$\leftrightarrow$ can lead to exponentially larger formulas.
1521:
1522: Let $\sfT$ be a finite nonempty set of homogeneous terms and let
1523: $\sfD$ be a finite set of atomic formulas of the form $d\divides t$,
1524: where $d\geq 1$ and $t$ is a homogeneous term. Moreover, let
1525: $\ell>\max\set{\normpos{t}}{t\in \sfT}\cup\set{\normneg{t}}{t\in
1526: \sfT}$ and $\ell'>\max\set{d}{d\divides t\in\sfD}$\@.
1527: \begin{theorem}
1528: \label{thm:bound_qf_formula}
1529: Let $\psi$ be a Boolean combination of atomic formulas $t\ZAECKZAECK
1530: c$ and $d\divides t+c'$, with $t\in\sfT$, $d\divides t\in\sfD$,
1531: $-\ell<c<\ell$, $c'\in\Int$, and
1532: $\zaeckzaeck\in\{=,\not=,<,\leq,>,\geq\}$\@. The size of the minimal
1533: DWA for $\psi$ is at most $(2+2\ell)^{|\sfT|}\cdot
1534: \ell'^{|\sfD|}$\@.
1535: \end{theorem}
1536: \begin{proof}
1537: Without loss of generality, we assume that the variables occurring
1538: in terms in $T$ are $y_1,\dots,y_r$\@.
1539: %
1540: Let $\autC$ be the product automaton of all the
1541: $\autA_{(-\ell,\ell)}^{t\EQ 0}$s and $\autA^{d\divides t}$s, for
1542: $t\in\sfT$ and $d\divides t\in\sfD$\@. To simplify notation we omit
1543: the subscripts $(-\ell,\ell)$ and we assume that
1544: $\sfT=\{t_1,\dots,t_m\}$ and $\sfD=\{d_1\divides
1545: t_1,\dots,d_n\divides t_n\}$\@.
1546: %
1547: Note that the states of $\autC$ are tuples
1548: $(p_1,\dots,p_m,q_1,\dots,q_n)$, where $p_i$ is a state of
1549: $\autA^{t_i\EQ 0}$ and $q_j$ is a state of $\autA^{d_j\divides
1550: t_j}$\@. By Lemma~\ref{fact:bound_automata_(in)equation},
1551: $\autA^{t_i\EQ 0}$ has $2+2\ell$ states, and by
1552: Lemma~\ref{fact:bound_automata_divisibiliy}, $\autA^{d_j\divides
1553: t_j}$ has $1+d_j\leq \ell'$ states.
1554: %
1555: %%Without loss of generality,
1556: %%we assume that all states of $\autC$ are reachable from the
1557: %%$\autC$'s initial state. Note that the initial state of
1558: %%$\autA^{t_i\EQ 0}$ or $\autA^{d_j\divides t_i}$ has no incoming
1559: %%transitions.
1560: %
1561: It follows that the size of $\autC$ is at most
1562: \begin{equation*}
1563: \prod_{t\in\sf T}(2+2\ell)\cdot
1564: \prod_{d\divides t\in\sfD} (1+d)
1565: \leq
1566: (2+2\ell)^{|\sfT|}\cdot
1567: \ell'^{|\sfD|}
1568: \,.
1569: \end{equation*}
1570:
1571: It remains to define the set of accepting states of $\autC$
1572: according to $\psi$\@.
1573: %We identify an initial state of
1574: %$\autA^{t_i\EQ 0}$ or $\autA^{d_j\divides t_i}$ with the integer
1575: %$0$\@.
1576: %
1577: We define the DWA $\autD$ as $\autC$ except the set $E$ of accepting
1578: states is defined as follows. A state
1579: $q=(p_1,\dots,p_m,q_1,\dots,q_n)\in\Int^{m+n}$
1580: of $\autD$ is in $E$ iff $\frakZ\models\psi_q$, where $\psi_q$ is
1581: the formula obtained by substituting
1582: \begin{itemize}
1583: \item the integer $p_i$ for the term $t_i$ in the atomic
1584: formulas of the form $t_i\ZAECKZAECK c$, and
1585: \item the integer $q_j$ for the term $t_j$ in the atomic formulas of
1586: the form $d_j\divides t_j+c$\@.
1587: \end{itemize}
1588: Note that $\psi_q$ is either true or not in $\frakZ$ since it is a
1589: sentence.
1590:
1591: It remains to prove that $\autD$ represents $\Zrepresents{\psi}$\@.
1592: Let $w\in(\Sigma^r)^+$ be a word representing
1593: $\overline{a}\in\Int^r$\@.
1594: %%
1595: For a term $t\in\sfT$, the value $t[\overline{a}]$ can be replaced
1596: by $\ell$ if $t[\overline{a}]\geq \ell$ and by $-\ell$ if
1597: $t[\overline{a}]\leq -\ell$ in every atomic formula of the form
1598: $t\ZAECKZAECK c$ without changing its truth value since
1599: $-\ell<c<\ell$\@. This modified value corresponds to the state
1600: reached by $\autA^{t\EQ 0}$ after reading the word $w$\@.
1601: %%
1602: For an atomic formula of the form $d\divides t+c$, with $d\divides
1603: t\in\sfD$, we can replace $t[\overline{a}]+c$ by
1604: $\remainder(t[\overline{a}]+c,d)$ without changing the truth value.
1605: This adjusted value corresponds to the state reached by
1606: $\autA^{d\divides t}$ after reading the word $w$\@.
1607: %%
1608: From the definition of $E$, it follows that $w\in L(\autD)$ iff
1609: $\frakZ\models\psi[\overline{a}]$\@.
1610: \end{proof}
1611:
1612:
1613: %-------------------------------------------------------------------------
1614: \section{An Upper Bound on the Automata Size}
1615: \label{BOUND}
1616:
1617: In this section, we give an upper bound on the size of the minimal DWA
1618: for PA formulas. We obtain this bound by examining the
1619: quantifier-free formulas constructed by applying Reddy and Loveland's
1620: quantifier elimination method~\cite{Reddy_Loveland.1978}, which
1621: improves Cooper's quantifier elimination method~\cite{Cooper.1972}\@.
1622: We use Reddy and Loveland's quantifier elimination method since the
1623: produced formulas are ``small'' with respect to the following
1624: parameters on which the upper bound of the minimal DWA in
1625: Theorem~\ref{thm:bound_qf_formula} depends.
1626: \begin{definition}
1627: For $\varphi\in\pa$, we define
1628: \begin{align*}
1629: \Terms(\varphi)&:=
1630: \set{t}{t\ZAECKZAECK c\in\Atoms(\varphi)}
1631: \,,
1632: \\
1633: \Divs(\varphi)&:=
1634: \set{d\divides t}{d\divides t+c\in\Atoms(\varphi)}
1635: \,,
1636: \\
1637: \intertext{and}
1638: \maxCoef(\varphi)&:=
1639: \max\{1\}\cup
1640: \set{\abs{k}}{\text{$k$ is a } \text{coefficient
1641: in $t\ZAECKZAECK c\in\Atoms(\varphi)$}}
1642: \,,
1643: \\
1644: \maxConst(\varphi)&:=
1645: \max\{1\}\cup
1646: \set{\abs{c}}{t\ZAECKZAECK c\in\Atoms(\varphi)}
1647: \,,
1648: \\
1649: \maxDiv(\varphi)&:=
1650: \max\{1\}\cup\set{d}{d\divides t+c\in\Atoms(\varphi)}
1651: \,.
1652: \end{align*}
1653: \end{definition}
1654:
1655: \subsection{Eliminating a Quantifier}
1656:
1657: For the sake of completeness, we briefly recall Reddy and Loveland's
1658: quantifier elimination method. Consider the formula $\exists x\varphi$
1659: with $\varphi(x,\overline{y})\in\qf$\@.
1660: %%
1661: The construction of $\psi(\overline{y})\in\qf$ proceeds in 2 steps.
1662:
1663: \vspace{\topsep}
1664: \noindent
1665: \textbf{Step 1:} First, eliminate the connectives $\rightarrow$ and
1666: $\leftrightarrow$ in $\varphi$ using standard rules, \eg, a subformula
1667: $\chi\IMPL\chi'$ is replaced by $\NEG\chi\OR\chi'$\@.
1668: %
1669: Second, push all negation symbols in $\varphi$ inward (using
1670: De\,Morgan's laws, etc.\@) until they only occur directly in front
1671: of the atomic formulas.
1672: %
1673: Third, rewrite all atomic formulas and negated atomic formulas in
1674: which $x$ occurs such that they are all of one of the forms
1675: \begin{gather}
1676: \tag{A}
1677: \label{eqn:atom_typeA}
1678: k\CDOT x\LESS t(y_1,\dots,y_n)
1679: \,,
1680: \\
1681: \tag{B}
1682: \label{eqn:atom_typeB}
1683: t(y_1,\dots,y_n)\LESS k\CDOT x
1684: \,,
1685: \\
1686: \intertext{or}
1687: \tag{C}
1688: \label{eqn:atom_typeC}
1689: d\DIVIDES t(x,y_1,\dots,y_n)
1690: \end{gather}
1691: with $k>0$\@.
1692: %
1693: For instance, the negated inequation $\NEG 2\CDOT x+9\CDOT y\LESS 5$
1694: is rewritten to $-9\CDOT y+5-1\LESS 2\CDOT x$, and the negated
1695: equation $\NEG 2\CDOT x+9\CDOT y\EQ 5$ is replaced by the disjunction
1696: $-9\CDOT y+5\LESS 2\CDOT x\OR 2\CDOT x\LESS -9\CDOT y+5$\@.
1697: %
1698: Let $\varphi'(x,\overline{y})$ be the resulting formula.
1699:
1700: \vspace{\topsep}
1701: \noindent
1702: \textbf{Step 2:} Let $\psi_{-\infty}$ be the formula where all the
1703: atomic formulas of type~(\ref{eqn:atom_typeA}) in $\varphi'$ are
1704: replaced by ``true'', \ie, $0\LESS1$, and all atomic formulas of
1705: type~(\ref{eqn:atom_typeB}) are replaced by ``false'', \ie,
1706: $1\LESS0$\@. We assume in the following, without loss of generality,
1707: that $0\LESS1$ and $1\LESS0$ do not occur as proper subformulas. Note
1708: that by propositional reasoning, we can always eliminate such
1709: subformulas, \eg, $\alpha\AND 0\LESS1$ can be simplified to $\alpha$\@.
1710: %
1711: Let $\sfB$ be the set of the atomic formulas in $\varphi'$ of
1712: type~(\ref{eqn:atom_typeB}), and let $\lcm(x,\varphi)$ be the least
1713: common multiple of the $d$s in the atomic formulas of
1714: type~(\ref{eqn:atom_typeC}) and of the coefficients of the variable
1715: $x$ in the atomic formulas of type~(\ref{eqn:atom_typeB})\@. Let
1716: $\psi$ be the formula
1717: \begin{equation*}
1718: \bigvee_{1\leq j\leq \lcm(x,\varphi)}\psi_{-\infty}[j/x]
1719: \,\,
1720: \OR
1721: \bigvee_{1\leq j\leq \lcm(x,\varphi)\ }
1722: \bigvee_{t+c\LESS k\cdot x\in\sfB}
1723: \bigl(
1724: k\!\DIVIDES\! t+c+j\AND\varphi'[t+c+j/k\cdot x]
1725: \bigr)
1726: \,,
1727: \end{equation*}
1728: where $\varphi'[t+c+j/k\cdot x]$ means that every atomic formula
1729: $\alpha$ in $\varphi'$ in which $x$ occurs is first multiplied by $k$
1730: and then $k\cdot x$ is substituted by $t+c+j$\@. Formally, for an
1731: atomic formula $\alpha$, a term $t$, and $k\in\Int\setminus\{0\}$, we
1732: define
1733: \begin{equation*}
1734: \alpha[t/k\cdot x]:=
1735: \begin{cases}
1736: k'\cdot t \LESS k\cdot t' &
1737: \text{if $\alpha=k'\cdot x\LESS t'$,}
1738: \\
1739: k\cdot t' \LESS k'\cdot t &
1740: \text{if $\alpha=t'\LESS k'\cdot x$,}
1741: \\
1742: kd\divides k'\cdot t+k\cdot t' &
1743: \text{if $\alpha=d\divides k'\cdot x + t'$,}
1744: \\
1745: \alpha & \text{otherwise.}
1746: \end{cases}
1747: \end{equation*}
1748:
1749: %We call the subformulas $\psi_{-\infty}[j/x]$ and
1750: %$\big(k\!\DIVIDES\!t+c+j\AND\varphi'[t+c+j/k\cdot x]\big)$ of $\psi$
1751: %\emph{generated witnesses} for $x$ in $\varphi$\@.
1752:
1753: \begin{fact}
1754: The formula $\psi$ is logically equivalent to $\exists x\varphi$\@.
1755: \end{fact}
1756:
1757: \subsection{Analysis}
1758:
1759: We can construct from an arbitrary formula a logically equivalent
1760: quantifier-free formula by successively replacing subformulas of the
1761: form $Qx\varphi$, where $\varphi\in\qf$ and $Q\in\{\exists,\forall\}$,
1762: with the logically equivalent quantifier-free formulas that are
1763: produced by the quantifier elimination method.
1764: %%
1765: \citeN{Oppen.1978} analyzed the length of the formulas that are
1766: produced by iteratively applying Cooper's quantifier elimination
1767: method. Oppen proved a triple exponential upper bound on the formula
1768: length by relating the growth in the number of atomic formulas, the
1769: maximum of the absolute values of constants and coefficients appearing
1770: in these atomic formulas, and the number of distinct coefficients and
1771: divisibility predicates that may appear.
1772: %%
1773: Similar analysis of improved versions of Cooper's quantifier
1774: elimination method are in~\cite{Reddy_Loveland.1978,Graedel.1988}\@.
1775:
1776:
1777: \citeN{Reddy_Loveland.1978} observed that they obtain shorter formulas
1778: when pushing quantifiers inward before applying their quantifier
1779: elimination method. For example, using the quantifier elimination
1780: method to eliminate the quantified variable $x_2$ in $\exists
1781: x_1\exists x_2\varphi$ with $\varphi\in\qf$, we obtain a formula of
1782: the form $\exists x_1(\varphi_1\OR\dots\OR\varphi_n)$\@. Instead of
1783: applying the quantifier elimination method to $\exists
1784: x_1(\varphi_1\OR\dots\OR\varphi_n)$, rewriting the formula first to
1785: $(\exists x_1\varphi_1)\OR\dots\OR(\exists x_1\varphi_n)$ and then
1786: applying the quantifier elimination method to each of the disjuncts
1787: separately produces shorter formulas due to the following reasons.
1788: First, we avoid using $\lcm(x_1,\varphi_1\OR\dots\OR\varphi_n)$ in
1789: Step~2 of the quantifier elimination method; instead we determine
1790: $\lcm(x_1,\varphi_i)$, for each disjunct $\varphi_i$ separately.
1791: Second, we use an inequation $k\cdot x_1\LESS t$ of
1792: type~(\ref{eqn:atom_typeB}) occurring in a disjunct $\varphi_i$ only
1793: for eliminating $x_1$ in $\varphi_i$\@. We do not use this inequation
1794: $k\cdot x_1\LESS t$ for eliminating $x_1$ in disjuncts $\varphi_j$ in
1795: which the inequation $k\cdot x_1\LESS t$ does not occur.
1796: %%
1797: However, if the variable $x_1$ is universally quantified, then we
1798: cannot push the quantifier inward. Note that in order to apply the
1799: quantifier elimination method, we have to rewrite the formula $\forall
1800: x_1(\varphi_1\OR\dots\OR\varphi_n)$ to $\neg\exists
1801: x_1(\neg(\varphi_1\OR\dots\OR\varphi_n))$\@. To eliminate $x_1$, we
1802: have to use in Step~2 $\lcm(x_1,\neg(\varphi_1\OR\dots\OR\varphi_n))$
1803: and the set $\sfB$ of the inequations of type~(\ref{eqn:atom_typeB})
1804: occurring in the formula produced by Step~1 normalizing
1805: $\neg(\varphi_1\OR\dots\OR\varphi_n)$\@.
1806:
1807:
1808: Reddy and Loveland analyzed the quantifier-free formulas produced by
1809: successively applying their quantifier elimination method to formulas
1810: in prenex normal form. We refine and extend their analysis to
1811: arbitrary formulas.
1812: %%
1813: However, before launching into the analysis, we need the following
1814: definitions. For $\varphi\in\pa$, we define
1815: \begin{align*}
1816: \Terms_+(\varphi)&:=
1817: \set{t\in\Terms(\varphi)}
1818: {\text{in $t$ there occurs a variable that is bound in $\varphi$}}
1819: \\
1820: \intertext{and}
1821: \Divs_+(\varphi)&:=
1822: \set{d\divides t\in\Divs(\varphi)}
1823: {\text{in $t$ there occurs a variable that is bound in $\varphi$}}
1824: \,.
1825: \end{align*}
1826: Furthermore, let
1827: $\Terms_-(\varphi):=\Terms(\varphi)\setminus\Terms_+(\varphi)$ and
1828: $\Divs_-(\varphi):=\Divs(\varphi)\setminus\Divs_+(\varphi)$\@.
1829:
1830: \begin{lemma}
1831: \label{lem:qe_bounds}
1832: For every $\varphi\in\pa$ of the form $Q x_1\dots Q x_s\vartheta$,
1833: with $Q\in\{\exists,\forall\}$ and $\vartheta\in\qf$, there is a
1834: logically equivalent $\psi\in\qf$ such that
1835: \begin{align*}
1836: |\Terms(\psi)\setminus\Terms_-(\varphi)|
1837: &\leq
1838: |\Terms_+(\varphi)|^{s+1}
1839: \,,\\
1840: |\Divs(\psi)\setminus\Divs_-(\varphi)|
1841: &\leq
1842: \big(|\Terms_+(\varphi)|+1\big)^s\cdot
1843: \big(|\Divs_+(\varphi)|+s\big)
1844: \,,\\
1845: \intertext{and}
1846: \maxCoef(\psi)
1847: &<
1848: a^{2^{2s}}
1849: \,,\\
1850: \maxDiv(\psi)
1851: &<
1852: a^{2^{2s}}
1853: \,,\\
1854: \maxConst(\psi)
1855: &<
1856: ba^{2^{2s}
1857: (|\Terms_+(\varphi)|+|\Divs_+(\varphi)|+s)}
1858: \,,
1859: \end{align*}
1860: where $a>\max\{2,\maxCoef(\varphi),\maxDiv(\varphi)\}$ and
1861: $b>\max\{2,\maxConst(\varphi)\}$\@.
1862: \end{lemma}
1863: \begin{proof}
1864: We first describe how we construct the quantifier-free formula
1865: $\psi$, where we assume that $Q=\exists$\@. For $Q=\forall$, we
1866: rewrite $\varphi$ to $\neg\exists x_1\dots\exists x_s\neg\vartheta$
1867: and eliminate the quantified variables in $\exists x_1\dots\exists
1868: x_s\neg\vartheta$ as described below.
1869:
1870: By a preprocessing step we rewrite $\vartheta$ to negation norm form
1871: (\ie, we eliminate the connectives $\rightarrow$ and
1872: $\leftrightarrow$, and we push the negation symbols inward such that
1873: the connective $\neg$ only occurs directly in front of atomic
1874: formulas) and we rewrite (in)equations so that we only have
1875: inequations of the form $t\LESS t'$ or $t\GREATER t'$ and no
1876: negation occurs in front of an inequation. For instance, $t\LEQ t'$
1877: is rewritten to $t\LESS t'+1$ and $\neg t\LEQ t'$ is rewritten to
1878: $t\GREATER t'$\@. Let $\vartheta_0$ be the formula that we obtain
1879: by the rewriting.
1880: %%
1881: The only parameter that is changed by this rewriting is the maximal
1882: absolute value of a constant, which increases by at most $1$\@.
1883: %%
1884: Observe that this special form of a formula is preserved when we
1885: apply the quantifier elimination method: In Step~1 we only rewrite
1886: the inequations such that they are of type~(\ref{eqn:atom_typeA})
1887: or~(\ref{eqn:atom_typeB})\@. Such rewriting does not alter the
1888: parameters. Step~2 also preserves this special form.
1889:
1890: After the preprocessing step, we construct the quantifier-free
1891: formula $\psi$ iteratively in $s$ steps by constructing intermediate
1892: formulas $\varphi_0,\dots,\varphi_s$, where $\psi$ will be
1893: $\varphi_s$. Let $\varphi_0:=\exists x_1\dots\exists
1894: x_s\vartheta_0$\@.
1895: %%
1896: In the $\ell$th step we eliminate the variable $x_{s-\ell+1}$, where
1897: $1\leq \ell\leq s$\@. This is done as follows. Assume that
1898: $\varphi_{\ell-1}=\exists x_1\dots\exists
1899: x_{s-\ell+1}\vartheta_{\ell-1}$, where $\vartheta_{\ell-1}=
1900: \vartheta_{\ell-1,1}\OR\dots\OR\vartheta_{\ell-1,n_{\ell-1}}$\@.
1901: %%
1902: We push the existential quantification of $x_{s-\ell+1}$ inward in
1903: $\vartheta_{\ell-1}$ as far as possible\@. For every $1\leq i\leq
1904: n_{\ell-1}$, we apply the quantifier elimination method to $\exists
1905: x_{s-\ell+1}\vartheta_{\ell-1,i}$\@. After the $n_{\ell-1}$
1906: applications of the quantifier elimination method, we obtain for
1907: some $n_\ell\geq 1$, a formula
1908: $\vartheta_\ell:=\vartheta_{\ell,1}\OR\dots\OR\vartheta_{\ell,n_\ell}$
1909: that is logically equivalent to $\exists
1910: x_{s-\ell_1}\vartheta_{\ell-1}$\@. Let $\varphi_\ell:=\exists
1911: x_1\dots\exists x_{s-\ell}\vartheta_\ell$\@.
1912:
1913: \medskip
1914:
1915: We now prove the upper bounds on the parameters of $\psi$\@. Let
1916: $n_0:=1$ and $\vartheta_{0,1}:=\vartheta_0$\@. It is straightforward
1917: to prove by induction over $0\leq \ell\leq s$:
1918: \begin{enumerate}[(i)]
1919: \item There are indices $1\leq i_1,\dots,i_k\leq n_\ell$ such that
1920: \begin{equation*}
1921: \Terms(\varphi_\ell) =
1922: \Terms(\vartheta_{\ell,i_1})
1923: \cup\dots\cup
1924: \Terms(\vartheta_{\ell,i_k})
1925: \,,
1926: \end{equation*}
1927: where $k\leq |\Terms_+(\varphi)|^\ell$\@.
1928: \item There are indices $1\leq i_1,\dots,i_k\leq n_\ell$ such that
1929: \begin{equation*}
1930: \Divs(\varphi_\ell) =
1931: \Divs(\vartheta_{\ell,i_1})
1932: \cup\dots\cup
1933: \Divs(\vartheta_{\ell,i_k})
1934: \,,
1935: \end{equation*}
1936: where $k\leq (|\Terms_+(\varphi)|+1)^\ell$\@.
1937: \end{enumerate}
1938: The upper bounds on $|\Terms(\psi)\setminus\Terms_-(\varphi)|$ and
1939: $|\Divs(\psi)\setminus\Divs_-(\varphi)|$ follow immediately from~(i)
1940: and~(ii), respectively, since $|\Terms(\vartheta_{\ell,i})\setminus
1941: \Terms_-(\varphi)|\leq|\Terms_+(\varphi)|$ and
1942: $|\Divs(\vartheta_{\ell,i})\setminus\Divs_-(\varphi)|\leq
1943: |\Divs_+(\varphi)|+\ell$, for every $0\leq \ell\leq s$ and $1\leq i\leq
1944: n_\ell$\@.
1945:
1946: \medskip
1947:
1948: We establish upper bounds on $\maxCoef(\psi)$, $\maxDiv(\psi)$, and
1949: $\maxConst(\psi)$:
1950: %%
1951: We prove by induction over $\ell$ that
1952: \begin{equation*}
1953: \maxCoef(\varphi_\ell), \maxDiv(\varphi_\ell)
1954: <
1955: a^{2^{2\ell}}
1956: \quad\text{and}\quad
1957: \maxConst(\varphi_{\ell})
1958: <
1959: ba^{2^{2\ell}(|\Terms_+(\varphi)|+|\Divs_+(\varphi)|+\ell)}
1960: \,.
1961: \end{equation*}
1962: For $\ell=0$, these upper bounds are obviously true. Assume that
1963: $\ell>0$\@. For $1\leq i\leq n_{\ell-1}$, we examine at the formula
1964: produced by the quantifier elimination method applied to $\exists
1965: x_{s-\ell+1}\vartheta_{\ell-1,i}$\@. Note that Step~1 of the
1966: quantifier elimination method does not alter the absolute values of
1967: the coefficients and constants, and the $d$s in the divisibility
1968: predicate because of our preprocessing step by rewriting $\vartheta$
1969: to $\vartheta_0$\@. It suffices to look at the substitutions
1970: $\alpha[t+c+j/k\cdot x]$ carried out in Step~2, where $\alpha$ is an
1971: atomic formula in $\vartheta_{\ell-1,i}$, $t+c\LESS k\cdot x$ is an
1972: inequation of type~(\ref{eqn:atom_typeB}) in $\vartheta_{\ell-1,i}$,
1973: and $1\leq j\leq\lcm(x_{s-\ell+1},\vartheta_{\ell-1,i})$\@.
1974: \begin{itemize}
1975: \item Assume that $\alpha=d\divides t$, for some $d\geq 1$ and some
1976: term $t$\@. By the induction hypothesis, we have that
1977: \begin{equation*}
1978: kd<a^{2^{2(\ell-1)}}\cdot a^{2^{2(\ell-1)}}
1979: =
1980: a^{2\cdot 2^{\ell-1}}
1981: \leq
1982: a^{2^{2\ell}}
1983: \,.
1984: \end{equation*}
1985: It follows that $\maxDiv(\varphi_{\ell})< a^{2^{2\ell}}$\@.
1986: \item Assume that $\alpha=k'\cdot x\LESS t'$ or $\alpha=t'\LESS
1987: k'\cdot x$, for some $k'>0$ and some term $t'$\@. By the induction
1988: hypothesis, we have that $k$, $k'$, and the absolute values of the
1989: coefficients occurring in $t$ and $t'$ are smaller than
1990: $a^{2^{2(\ell-1)}}$\@. It follows that
1991: the absolute values of the coefficients in the normalized
1992: inequations of $k'\cdot (t+c+j)\LESS k\cdot t'$ and $k\cdot
1993: t'\LESS k'\cdot (t+c+j)$ are smaller than
1994: \begin{equation*}
1995: a^{2^{2(\ell-1)}}\cdot a^{2^{2(\ell-1)}} +
1996: a^{2^{2(\ell-1)}}\cdot a^{2^{2(\ell-1)}}
1997: =
1998: 2a^{2^{2\ell-1}}
1999: \leq
2000: a^{2^{2\ell}}
2001: \,.
2002: \end{equation*}
2003: Hence, $\maxCoef(\varphi_{\ell})<a^{2^{2\ell}}$\@.
2004:
2005: The absolute values of the constants in the normalized inequations
2006: $k'\cdot (t+c+j)\LESS k\cdot t'$ and $k\cdot t'\LESS k'\cdot
2007: (t+c+j)$ is bounded by
2008: \begin{multline*}
2009: \maxCoef(\varphi_{\ell-1})
2010: \cdot
2011: \big(\maxConst(\varphi_{\ell-1})+
2012: \lcm(x_{s-\ell+1},\vartheta_{\ell-1,i})\big)
2013: +
2014: \\
2015: \maxCoef(\varphi_{\ell-1})\cdot\maxConst(\varphi_{\ell-1})
2016: \,,
2017: \end{multline*}
2018: which rewrites to
2019: \begin{equation}
2020: \label{eqn:upper_constant}
2021: \maxCoef(\varphi_{\ell-1})
2022: \cdot
2023: \big(2\maxConst(\varphi_{\ell-1})+
2024: \lcm(x_{s-\ell+1},\vartheta_{\ell-1,i})\big)
2025: \,.
2026: \end{equation}
2027: An upper bound on $\lcm(x_{s-\ell+1},\vartheta_{\ell-1,i})$ is
2028: \begin{equation*}
2029: \big(a^{2^{2(\ell-1)}}\big)^{|\Terms_+(\varphi)|+|\Divs_+(\varphi)|+\ell-1}
2030: =
2031: a^{2^{2(\ell-1)}\cdot(|\Terms_+(\varphi)|+|\Divs_+(\varphi)|+\ell-1)}
2032: \end{equation*}
2033: since we determine the least common multiple of at most
2034: $|\Terms_+(\varphi)|+|\Divs_+(\varphi)|+\ell-1$ numbers and all
2035: these numbers are bounded by $a^{2^{2(\ell-1)}}$\@.
2036: %%
2037: By the induction hypothesis, we have that $|c|$ and the absolute value
2038: of the constant in $t'$ is smaller than
2039: $ba^{2^{2(\ell-1)}(|\Terms_+(\varphi)|+|\Divs_+(\varphi)|+\ell-1)}$\@.
2040: Therefore,~(\ref{eqn:upper_constant}) is smaller than
2041: \begin{align*}
2042: a^{2^{2\ell-1}}
2043: \big(2ba^{|\Terms_+(\varphi)|+|\Divs_+(\varphi)|+\ell-1}+
2044: a^{|\Terms_+(\varphi)|+|\Divs_+(\varphi)|+\ell-1}\big)
2045: &\leq
2046: 2ba^{2^{2\ell}(|\Terms_+(\varphi)|+|\Divs_+(\varphi)|+\ell-1)}
2047: \\
2048: &\leq
2049: ba^{2^{2\ell}(|\Terms_+(\varphi)|+|\Divs_+(\varphi)|+\ell)}
2050: \,.
2051: \end{align*}
2052: It follows that $\maxConst(\varphi_{\ell})<
2053: ba^{2^{2\ell}(|\Terms_+(\varphi)|+|\Divs_+(\varphi)|+\ell)}$\@.\qed
2054: \end{itemize}
2055: \end{proof}
2056:
2057: By iteratively applying Lemma~\ref{lem:qe_bounds} we obtain the
2058: following upper bounds for formulas in prenex normal form.
2059: \begin{lemma}
2060: \label{lem:qe*_bounds}
2061: For every $\varphi\in\pa$ of the form $Q_1 x_1\dots Q_r x_r \psi_0$
2062: with $\psi_0\in\qf$ there is logically equivalent $\psi\in\qf$ such
2063: that
2064: \begin{equation*}
2065: |\Terms(\psi)| \leq
2066: T^{(\ell+1)^{\qa(\varphi)}}
2067: \qquad\text{and}\qquad
2068: |\Divs(\psi)| \leq
2069: DT^{(\ell+1)^{\qa(\varphi)+2}}
2070: \,,
2071: \end{equation*}
2072: where $T=\max\{2,|\Terms(\varphi)|\}$,
2073: $D=\max\{1,|\Divs(\varphi)|\}$, and $\ell$ is the maximal length of
2074: a quantifier block in $\varphi$\@. Furthermore, it holds that
2075: \begin{align*}
2076: \maxCoef(\psi)
2077: &<
2078: a^{2^{2\qn(\varphi)}}
2079: \,,\\
2080: \maxDiv(\psi)
2081: &<
2082: a^{2^{2\qn(\varphi)}}
2083: \,,\\
2084: \intertext{and}
2085: \maxConst(\psi) &<
2086: ba^{2^{3\qn(\varphi)}DT^{(\ell+1)^{\qa(\varphi)+2}}}
2087: \,,
2088: \end{align*}
2089: where $a>\max\{2,\maxCoef(\varphi),\maxDiv(\varphi)\}$ and
2090: $b>\max\{2,\maxConst(\varphi)\}$\@.
2091: \end{lemma}
2092: \begin{proof}
2093: We construct the quantifier-free formula $\psi$ by successively
2094: eliminating the quantifier blocks in $\varphi$, starting from the
2095: innermost block. Assume that after the $k$th step, where $0\leq
2096: k<\qa(\varphi)$, we have produced the formula
2097: \begin{equation*}
2098: Q_1 x_1\dots Q_i x_i Q x_{i+1}\dots Q x_j \psi_k
2099: \,,
2100: \end{equation*}
2101: where $1\leq i<j\leq r$, $Q_1,\dots,Q_i,Q\in\{\exists,\forall\}$
2102: with $Q_i\not=Q$, and $\psi_k\in\qf$\@. Let $\psi_{k+1}\in\qf$ be
2103: the formula from Lemma~\ref{lem:qe_bounds} that is logically
2104: equivalent to $\varphi_k:=Q x_{i+1}\dots Q x_j \psi_k$\@. We define
2105: $\psi:=\psi_{\qa(\varphi)}$\@.
2106:
2107: For $1\leq i\leq\qa(\varphi)$, let $\ell_i$ be the length of the
2108: $i$th quantifier block. We prove by induction over $0\leq
2109: k\leq\qa(\varphi)$ that
2110: \begin{align*}
2111: |\Terms(\psi_k)|
2112: \leq
2113: T^{(\ell+1)^k}
2114: \qquad&\text{and}\qquad
2115: |\Divs(\psi_k)|\leq
2116: DT^{(\ell+1)^{k+2}}
2117: \,,
2118: \\
2119: \maxCoef(\psi_k)
2120: < a^{2^{2(\ell_1+\dots+\ell_k)}}
2121: \qquad&\text{and}\qquad
2122: \maxDiv(\psi_k)
2123: < a^{2^{2(\ell_1+\dots+\ell_k)}}
2124: \,,
2125: \\
2126: \intertext{and}
2127: \maxConst(\psi_k)
2128: &<
2129: ba^{2^{3(\ell_1+\dots+\ell_k)}
2130: DT^{(\ell+1)^{k+2}}}
2131: \,.
2132: \end{align*}
2133: The base cases for $k=0$ are trivial. For the step cases, let
2134: $k>0$\@.
2135: \begin{enumerate}[1.]
2136: \item By Lemma~\ref{lem:qe_bounds}, we have that
2137: \begin{align*}
2138: |\Terms(\psi_k)\setminus \Terms_-(\varphi_{k-1})|
2139: &\leq
2140: |\Terms_+(\varphi_{k-1})|^{\ell+1}
2141: \\
2142: &\leq
2143: |\Terms(\psi_{k-1})|^{\ell+1}
2144: \overset{\rm IH}{\leq}
2145: \big(T^{(\ell+1)^{k-1}}\big)^{\ell+1}
2146: =
2147: T^{(\ell+1)^k}
2148: \end{align*}
2149: and
2150: \begin{align*}
2151: |\Divs(\psi_k)\setminus\Divs_-(\varphi_{k-1})|
2152: &\leq
2153: (|\Terms_+(\varphi_{k-1})|+1)^{\ell}\cdot(|\Divs_+(\varphi_{k-1})|+\ell)
2154: \\
2155: &
2156: \leq
2157: (|\Terms(\psi_{k-1})|+1)^{\ell}\cdot(|\Divs(\psi_{k-1})|+\ell)
2158: \\
2159: &\overset{\rm IH}{\leq}
2160: \big(T^{(\ell+1)^{k-1}}+1\big)^{\ell}\cdot
2161: \big(DT^{{(\ell+1)}^{k+1}}+\ell\big)
2162: \\
2163: &\leq
2164: 2^{\ell+1}DT^{(\ell+1)^k+(\ell+1)^{k+1}}
2165: \leq
2166: DT^{(\ell+1)+(\ell+1)^k+(\ell+1)^{k+1}}
2167: \\
2168: &\leq
2169: DT^{{(\ell+1)}^{k+2}}
2170: \,.
2171: \end{align*}
2172: Note that $T\geq 2$ and $D\geq 1$\@.
2173:
2174: \item By Lemma~\ref{lem:qe_bounds}, we have that
2175: \begin{align*}
2176: \maxCoef(\psi_k)
2177: &\leq
2178: \big(\max\{2,\maxCoef(\psi_{k-1})\}\big)^{2^{2\ell_k}}
2179: \\
2180: &\overset{\rm IH}{<}
2181: \big(a^{2^{2(\ell_1+\dots+\ell_{k-1})}}\big)^{2^{2\ell_k}}
2182: =
2183: a^{2^{2(\ell_1+\dots+\ell_k)}}
2184: \,.
2185: \end{align*}
2186: Analogously, we obtain the upper bound for $\maxDiv(\psi_k)$\@.
2187:
2188: \item By Lemma~\ref{lem:qe_bounds}, we have that
2189: \begin{align*}
2190: \maxConst(\psi_k)
2191: &\leq
2192: \maxConst(\psi_{k-1})
2193: \cdot
2194: \big(a^{2^{2(\ell_1+\dots+\ell_{k-1})}}\big)^{2^{2\ell_k}
2195: (|\Terms_+(\varphi_{k-1})|+|\Divs_+(\varphi_{k-1})|+\ell_k)}
2196: \\
2197: &\leq
2198: \maxConst(\psi_{k-1})
2199: a^{2^{2(\ell_1+\dots+\ell_k)}
2200: (|\Terms(\psi_{k-1})|+|\Divs(\psi_{k-1})|+\ell_k)}
2201: \\
2202: &
2203: \leq
2204: \maxConst(\psi_{k-1})
2205: a^{2^{2(\ell_1+\dots+\ell_k)}
2206: (T^{(\ell+1)^{k-1}}+DT^{(\ell+1)^{k+1}}+\ell_k)}
2207: \\
2208: &\leq
2209: \maxConst(\psi_{k-1})
2210: a^{2^{2(\ell_1+\dots+\ell_k)}
2211: (DT^{(\ell+1)^k}+DT^{(\ell+1)^{k+1}})}
2212: \\
2213: &\leq
2214: \maxConst(\psi_{k-1})
2215: a^{2^{2(\ell_1+\dots+\ell_k)}
2216: DT^{(\ell+1)^{k+2}}}
2217: \\
2218: &\overset{\rm IH}{<}
2219: ba^{2^{3(\ell_1+\dots+\ell_{k-1})}
2220: DT^{(\ell+1)^{k+1}}}
2221: \cdot
2222: a^{2^{2(\ell_1+\dots+\ell_k)}
2223: DT^{(\ell+1)^{k+2}}}
2224: \\
2225: &\leq
2226: ba^{(2^{3(\ell_1+\dots+s_{k-1})}+2^{2(\ell_1+\dots+\ell_k)})
2227: DT^{(\ell+1)^{k+2}}}
2228: \\
2229: &\leq
2230: ba^{2^{3(\ell_1+\dots+\ell_k)}
2231: DT^{(\ell+1)^{k+2}}}
2232: \,.
2233: \qed
2234: \end{align*}
2235: \end{enumerate}
2236: \end{proof}
2237:
2238: Before we generalize Lemma~\ref{lem:qe*_bounds} to arbitrary formulas,
2239: we want to point out that transforming a formula first into prenex
2240: normal form and then eliminating the quantifiers is not a good thing
2241: to do. The formula size can increase because of the following reasons.
2242:
2243: First, a transformation into prenex normal form can increase the
2244: number of quantifier alternations. For instance, any transformation of
2245: $(\forall x\varphi)\wedge(\exists y\psi)$ into prenex normal form will
2246: introduce at least one additional alternation of quantifiers.
2247:
2248: Second, when transforming a formula into prenex normal form we have to
2249: introduce fresh variables when pushing quantifiers to the front. As
2250: an example, consider the formula in prenex normal form
2251: \begin{align*}
2252: \exists z_{n-1}\dots\exists z_2\exists z_1
2253: (&x=z_{n-1}+z_{n-1}\AND
2254: \\&
2255: z_{n-1}=z_{n-2}+z_{n-2}\AND\dots\AND z_2=z_1+z_1\AND z_1=y+y)
2256: \,,
2257: \end{align*}
2258: for some $n\geq 1$\@. It consists of $n$ distinct equations. A
2259: logically equivalent formula that consists of at most $4$ distinct
2260: equations is
2261: \begin{align*}
2262: \exists z\big(&
2263: x=z+z\AND
2264: \\&
2265: \exists z'(z=z'+z'
2266: \AND\dots\AND
2267: \exists z'(z=z'+z'\AND\exists z(z'=z+z\AND z=y+y))
2268: \dots)\big)
2269: \,.
2270: \end{align*}
2271: Furthermore, the formula length decreases by a factor of $\BigOh(\log
2272: n)$ since we use a fixed number of variables, \ie, we use $x,y,z,z'$
2273: instead of $x,y,z_1,\dots,z_{n-1}$\@.
2274:
2275: The third reason why a transformation into prenex normal form is not a
2276: good idea is illustrated by the formula $(\forall
2277: x\varphi)\IFF\psi$\@. Quantifiers do in general not distribute over
2278: $\rightarrow$ and $\leftrightarrow$\@. Therefore, we eliminate the
2279: connective $\leftrightarrow$ and obtain $((\forall
2280: x\varphi)\IMPL\psi)\AND(\psi\IMPL\forall x\varphi)$\@. Eliminating
2281: $\rightarrow$ yields $((\NEG\forall
2282: x\varphi)\OR\psi)\AND(\NEG\psi\OR\forall x\varphi)$\@. To move the
2283: quantifiers to the front, we have to push the first negation inward.
2284: Finally, we obtain $\exists x\forall x'
2285: ((\NEG\varphi\OR\psi)\AND(\NEG\psi\OR\varphi[x'/x]))$ assuming that
2286: $x$ does not occur free in $\psi$, and $x'$ does not occur free in
2287: $\varphi$ and $\psi$\@. We have not only doubled the length of the
2288: formula but we have also doubled the number of quantifiers. We want
2289: to \emph{eliminate} quantifiers and have ended up doubling our work.
2290:
2291:
2292: In analogy to the maximum of the lengths of the quantifier blocks of a
2293: formula in prenex normal form, we define the \emph{quantifier block
2294: length} of the formula $\varphi$ as
2295: \begin{equation*}
2296: \qbl(\varphi):=
2297: \max\set{\qbl_Q(\psi)}{Q\in\{\exists,\forall\}
2298: \text{ and }\psi\text{ is a subformula of }\varphi}
2299: \,,
2300: \end{equation*}
2301: where
2302: \begin{equation*}
2303: \qbl_Q(\varphi):=\begin{cases}
2304: \qbl_{\overline{Q}}(\psi)
2305: & \text{if $\varphi=\neg\psi$,}
2306: \\
2307: \qbl_Q(\psi_1)+\qbl_Q(\psi_2)
2308: & \text{if $\varphi=\psi_1\oplus\psi_2$ with $\oplus\in\{\wedge,\vee\}$,}
2309: \\
2310: \qbl_{Q}(\neg\psi_1\vee\psi_2)
2311: & \text{if $\varphi=\psi_1\rightarrow\psi_2$,}
2312: \\
2313: \qbl_Q((\psi_1\rightarrow\psi_2)\wedge(\psi_2\rightarrow\psi_1))
2314: & \text{if $\varphi=\psi_1\leftrightarrow\psi_2$,}
2315: \\
2316: 1+\qbl_Q(\psi) &\text{if $\varphi=Qx\psi$,}
2317: \\
2318: 0
2319: & \text{otherwise,}
2320: \end{cases}
2321: \end{equation*}
2322: for $Q\in\{\exists,\forall\}$\@.
2323:
2324: \begin{theorem}
2325: \label{thm:qe*_bounds}
2326: For every $\varphi\in\pa$ of length $n$, there is a logically
2327: equivalent $\psi\in\qf$ such that
2328: \begin{align*}
2329: &|\Terms(\psi)|
2330: \leq
2331: n^{(\qbl(\varphi)+1)^{\qa(\varphi)}}
2332: &\qquad\text{and}\qquad
2333: &|\Divs(\psi)|
2334: \leq
2335: n^{1+(\qbl(\varphi)+1)^{\qa(\varphi)+2}}
2336: \\
2337: &\maxCoef(\psi)
2338: <
2339: a^{2^{2\qn(\varphi)}}
2340: &\qquad\text{and}\qquad
2341: &\maxDiv(\psi)
2342: <
2343: a^{2^{2\qn(\varphi)}}
2344: \,,
2345: \end{align*}
2346: and
2347: \begin{equation*}
2348: \maxConst(\psi) <
2349: ba^{2^{3\qn(\varphi)}n^{1+(\qbl(\varphi)+1)^{\qa(\varphi)+2}}}
2350: \,,
2351: \end{equation*}
2352: where $a>\max\{2,\maxCoef(\varphi),\maxDiv(\varphi)\}$ and
2353: $b>\max\{2,\maxConst(\varphi)\}$\@.
2354: \end{theorem}
2355: \begin{proof}
2356: We require that variables are not reused in $\varphi$, \ie, the set
2357: of free variables of $\varphi$ is disjoint from the set of bound
2358: variables and the bound variables are pairwise distinct. Note that
2359: this can be achieved by replacing quantified variables by fresh
2360: variables. Such a variable renaming can increase the number of distinct
2361: atomic formulas. % by a factor of at most $\qn(\varphi)+1$\@.
2362: However, the number of atomic formulas after such a renaming still
2363: is less than or equal to the length of the original formula. Note
2364: that $n\geq\max\{2,|\Terms(\varphi)|, |\Divs(\varphi)|\}$\@.
2365:
2366: We construct the formula $\psi\in\qf$ in $\qa(\varphi)$ steps. Let
2367: $\varphi_0:=\varphi$\@. Let $0<k\leq\qa(\varphi)$ and assume that
2368: after the $(k-1)$st step we have produced the formula
2369: $\varphi_{k-1}$\@. Let $\Phi$ be the set of maximal subformulas
2370: $\vartheta$ of $\varphi_{k-1}$ with $\qa(\vartheta)\leq 1$ and where
2371: variables are either only existentially quantified or universally
2372: quantified.
2373: %%
2374: We can assume without loss of generality that every formula in
2375: $\Phi$ is in prenex normal form and that
2376: $\Phi=\{\vartheta_1,\dots,\vartheta_m\}$\@. For $1\leq i\leq m$,
2377: let $\xi_i\in\qf$ be the logically equivalent formula to
2378: $\vartheta_i$ from Lemma~\ref{lem:qe_bounds}\@.
2379: %%
2380: We replace in $\varphi_{k-1}$ every $\vartheta_i$ by $\xi_i$\@.
2381: We obtain the formula $\varphi_k$ that is logically equivalent
2382: to $\varphi$ and $\qa(\varphi_k)=\qa(\varphi)-k$\@.
2383: %%
2384: For $k=\qa(\varphi)$, we define $\psi:=\varphi_k$\@.
2385:
2386: For the formula $\varphi_k$, we have that
2387: \begin{align*}
2388: \Terms(\varphi_k)
2389: \subseteq
2390: \Terms(\varphi_{k-1})\setminus
2391: \Big(\bigcup_{1\leq i\leq m}\Terms_+(\vartheta_i)\Big)
2392: \cup
2393: \bigcup_{1\leq i\leq m}
2394: \big(\Terms(\xi_i)\setminus\Terms_-(\vartheta_i)\big)
2395: \,.
2396: \end{align*}
2397: Since variables are not reused in $\varphi$, it follows that
2398: \begin{equation*}
2399: |\Terms(\varphi_k)|\leq
2400: |\Terms(\varphi_{k-1})|-\sum_{1\leq i\leq m}|\Terms_+(\vartheta_i)|+
2401: \sum_{1\leq i\leq m} |\Terms_+(\vartheta_i)|^{\qn(\vartheta_i)+1}
2402: \,.
2403: \end{equation*}
2404: It is straightforward to show that the left hand side has its
2405: maximum when $m=1$ and
2406: $|\Terms_+(\vartheta_1)|=|\Terms(\varphi_{k-1})|$\@. Analogously to
2407: the step case in the proof of Lemma~\ref{lem:qe*_bounds} for
2408: formulas in prenex normal form, it follows that
2409: $|\Terms(\varphi_k)|\leq n^{(\qbl(\varphi)+1)^{k+1}}$ under the
2410: assumption that $|\Terms(\varphi_{k-1})|\leq
2411: n^{(\qbl(\varphi)+1)^k}$\@.
2412:
2413: We can argue similarly for $|\Divs(\varphi_k)|$\@. Similar as in the
2414: proof of Lemma~\ref{lem:qe*_bounds} for formulas in prenex normal
2415: form we obtain the upper bounds for $\maxCoef(\varphi_k)$,
2416: $\maxDiv(\varphi_k)$, and $\maxConst(\varphi_k)$\@.
2417: \end{proof}
2418:
2419:
2420: \subsection{Main Result}
2421: \label{subsec:main_result}
2422:
2423: We now prove our main result: The upper bound on the automata size of
2424: the minimal DWA for Presburger arithmetic formulas.
2425: \begin{theorem}
2426: \label{thm:main_result}
2427: The size of the minimal DWA for a formula $\varphi\in\pa$ of length
2428: $n$ is at most $2^{n^{(\qbl(\varphi)+1)^{\qa(\varphi)+4}}}$\@.
2429: \end{theorem}
2430: \begin{proof}
2431: Since we measure the length of integers linearly, we have that the
2432: absolute value of every integer occurring in $\varphi$ is bounded by
2433: $n$\@. It holds that $n> \maxConst(\varphi)$, $n>\maxCoef(\varphi)$,
2434: and $n>\maxDiv(\varphi)$\@.
2435:
2436: For $\qn(\varphi)=0$, we have that the size of the minimal DWA is at
2437: most $2^n$\@. For every atomic formula $\alpha_i$ of length $n_i$
2438: in $\varphi$, we can build a DWA of size at most $n_i$ by using the
2439: constructions in~\S\ref{subsec:(in)equations}
2440: and~\S\ref{subsec:divisibility}\@. Applying the product construct
2441: yields a DWA of size at most $\prod_{1\leq i\leq m} n_i\leq
2442: 2^{\sum_{1\leq i\leq m} n_i}\leq 2^n$, where $m$ is the number of
2443: atomic formulas in $\varphi$\@.
2444:
2445: In the following, assume that $\qn(\varphi)\geq 1$ and, therefore,
2446: we have that $\qa(\varphi)\geq 1$ and $\qbl(\varphi)\geq 1$\@.
2447: For the sake of readability, we define $a:=\qa(\varphi)$ and
2448: $\ell:=\qbl(\varphi)$\@.
2449: %%
2450: From Theorem~\ref{thm:qe*_bounds} it follows that there is a
2451: logically equivalent $\psi\in\qf$ with
2452: \begin{equation*}
2453: |\Terms(\psi)| \leq
2454: n^{(\ell+1)^a}
2455: \qquad\text{and}\qquad
2456: |\Divs(\psi)| \leq
2457: n^{1+(\ell+1)^{a+2}}
2458: \,.
2459: \end{equation*}
2460: Upper bounds on $\maxCoef(\psi)$, $\maxDiv(\psi)$, and
2461: $\maxConst(\psi)$ are
2462: \begin{equation*}
2463: \maxCoef(\psi), \maxDiv(\psi) <
2464: n^{2^{2\qn(\varphi)}}\leq
2465: 2^{2^{2a\ell}\log_2 n}\leq
2466: 2^{n^{1+2a\ell}}
2467: \end{equation*}
2468: and
2469: \begin{align*}
2470: \maxConst(\psi)
2471: <
2472: n^{1+2^{3\qn(\varphi)}n^{1+(\ell+1)^{a+2}}}
2473: \leq
2474: 2^{n^{3+3a\ell+(\ell+1)^{a+2}}}
2475: \leq
2476: 2^{n^{(\ell+1)^{a+1}+(\ell+1)^{a+2}}}
2477: \,.
2478: \end{align*}
2479: Note that $n\geq 2$, $a\ell\geq\qn(\varphi)$, and $x^{y}=2^{y\log_2
2480: x}$, for $x\geq 1$ and $y\geq 0$\@.
2481:
2482: Assume that there are $r\leq n$ free variables in $\varphi$\@.
2483: Since every term in $\psi$ contains at most the free variables of
2484: $\varphi$, the sum of the absolute values of the coefficients in a
2485: term is bounded by $n\cdot n^{2^{2\qn(\varphi)}}\leq
2486: 2^{n^{2+2a\ell}}<2^{n^{3+3a\ell}}$\@. With
2487: Theorem~\ref{thm:bound_qf_formula} at hand, we know that the size of
2488: the minimal DWA for $\psi$ is at most
2489: \begin{align*}
2490: \Big(2+2\cdot 2^{n^{(\ell+1)^{a+1}+(\ell+1)^{a+2}}}\Big)^{|\Terms(\psi)|}\cdot
2491: \maxDiv(\psi)^{|\Divs(\psi)|}
2492: \,.
2493: \end{align*}
2494: From
2495: \begin{align*}
2496: \Big(2+2\cdot 2^{n^{(\ell+1)^{a+1}+(\ell+1)^{a+2}}}\Big)^{|\Terms(\psi)|}
2497: \leq
2498: 2^{n^{(\ell+1)^{a+1}+(\ell+1)^{a+2}+(\ell+1)^a}}
2499: \leq
2500: 2^{n^{(\ell+1)^{a+3}}}
2501: \end{align*}
2502: and
2503: \begin{align*}
2504: \maxDiv(\psi)^{|\Divs(\psi)|}
2505: \leq 2^{n^{2+2a\ell+(\ell+1)^{a+2}}}
2506: \leq
2507: 2^{n^{2(\ell+1)^a+(\ell+1)^{a+2}}}
2508: \leq
2509: 2^{n^{(\ell+1)^{a+3}}}
2510: \end{align*}
2511: we conclude that the size of the minimal DWA for $\varphi$ is at
2512: most $2^{n^{(\ell+1)^{a+4}}}$\@.
2513: \end{proof}
2514:
2515: Theorem~\ref{thm:main_result} does not change if we measure the length
2516: of integers logarithmically and not linearly. The only change is that
2517: the maximal absolute integer in $\varphi$ is now smaller than $2^n$\@.
2518: We have to adjust the bounds on $\maxCoef(\psi)$, $\maxDiv(\psi)$, and
2519: $\maxConst(\psi)$\@. For instance, we still have that
2520: \begin{equation*}
2521: \maxCoef(\psi)<
2522: (2^n)^{2^{2\qn(\varphi)}}=2^{n2^{2\qn(\varphi)}}\leq
2523: 2^{n^{1+2\qa(\varphi)\qbl(\varphi)}}
2524: \,.
2525: \end{equation*}
2526: We argue analogously for
2527: $\maxDiv(\psi)$ and $\maxConst(\psi)$\@.
2528:
2529: \begin{corollary}
2530: \label{cor:aut_size}
2531: Let $\pa_c$ be the set of PA formulas with at most $c\geq 0$ quantifiers.
2532: %%
2533: The size of the minimal DWA for each $\varphi\in\pa_c$ is at most
2534: $2^{n^{\BigOh(1)}}$, where $n$ is the length of $\varphi$\@.
2535: \end{corollary}
2536: \begin{proof}
2537: If $\qn(\varphi)\leq c$ then $\qa(\varphi)\leq c$ and
2538: $\qbl(\varphi)\leq c$\@. Since $c$ is fixed the claim follows
2539: directly from Theorem~\ref{thm:main_result}\@.
2540: \end{proof}
2541:
2542:
2543: We want to remark that Theorem~\ref{thm:main_result} and
2544: Corollary~\ref{cor:aut_size} only give upper bounds on the sizes of
2545: the minimal DWAs for PA formulas. If the Boolean connectives and the
2546: quantifiers are handled by standard automata constructions, like
2547: complementation and subset construction, and the DWAs are minimized
2548: after every automata construction step, it may be the case that the
2549: whole construction uses one exponent more space. The reason is that
2550: an exponential blow-up can occur each time the subset construction is
2551: applied. It is an open question whether the standard automata
2552: constructions already suffice to construct a DWA in
2553: $2^{n^{(\qbl(\varphi)+1)^{\qa(\varphi)+4}}}$ space or time, for a
2554: given $\varphi\in\pa$ of length $n$\@. It is also open if there are
2555: more efficient automata constructions than the standard ones for
2556: constructing DWAs for PA formulas.
2557:
2558:
2559: %-------------------------------------------------------------------------
2560: \section{A Worst Case Example}
2561: \label{WORST}
2562:
2563: We give a worst case example that shows that our upper bound on the
2564: automata size is tight.
2565: %
2566: We use the formulas $\Prod_n(x,y,z)$ defined by Fischer and
2567: Rabin~\citeyear{Fischer_Rabin.1974}, for $n\geq 0$\@. It holds that
2568: \begin{equation*}
2569: \Zrepresents{\Prod_n}=
2570: \set{(a,b,c)\in\Nat}{ab=c\text{ and }
2571: a,b,c<\!
2572: \prod_{\substack{p\text{ is prime and}\\p<f(n+2)}}\!\!p}
2573: % \frakZ\models\Prod_n[a,b,c]
2574: % \quad\!\text{iff}\!\quad
2575: % ab=c\text{ and }
2576: % 0\leq a,b,c<
2577: % \!
2578: % \prod_{\substack{p\text{ prime and}\\p<f(n+2)}}\!\!p
2579: \,,
2580: \end{equation*}
2581: where $f(n):=2^{2^n}$\@. Note that it follows from the Prime Number
2582: Theorem that
2583: \begin{equation*}
2584: \prod_{\substack{p\text{ is prime and}\\p<f(n+2)}}\!\!p\geq
2585: 2^{f(n)^2}=
2586: %2^{2^{2^{n+1}}}=
2587: 2^{f(n+1)}
2588: \,.
2589: \end{equation*}
2590: Fischer and Rabin looked at the structure $(\Nat,+)$ and not at
2591: $\frakZ$, but it is straightforward to adapt the definition of
2592: $\Prod_n(x,y,z)$ to $\frakZ$\@.
2593: %%
2594: For $n\geq 0$, the length of $Prod_n$ and the number of quantifier
2595: alternations is linear in $n$\@. The quantifier block length is
2596: constant, \ie, there is a $c\geq 0$ such that for all $n\geq 0$,
2597: $\qbl(\Prod_n)=c$\@. By Theorem~\ref{thm:main_result} we know that the
2598: minimal DWA for $\Prod_n$ has at most $2^{2^{2^{\BigOh(n)}}}$ states.
2599:
2600: Before we prove the lower bound on the automata size for the formulas
2601: $\Prod_n$, we need the following lemma.
2602: \begin{lemma}
2603: \label{lem:mult_prefix}
2604: Let $\ell\geq 1$\@. For all $z\in\Nat$ with $\varrho^{\ell-1}\leq
2605: z\leq\varrho^{\ell}-2$, there are $x,y,z'\in[\varrho^{\ell}]$
2606: such that $xy = \varrho^{\ell} z+z'$\@.
2607: \end{lemma}
2608: \begin{proof}
2609: Assume that $\varrho^{\ell-1}\leq z\leq\varrho^{\ell}-2$\@.
2610: Let $x,y\in[\varrho^{\ell}]$ with $xy\geq \varrho^{\ell} z$ and
2611: $xy-\varrho^{\ell}z$ is minimal. Note that it is always possible to
2612: find $x,y\in[\varrho^{\ell}]$ with $xy\geq \varrho^{\ell}z$ since
2613: for $x=y=\varrho^{\ell}-1$, we have that
2614: \begin{equation*}
2615: xy
2616: =
2617: (\varrho^{\ell}-1)^2
2618: =
2619: \varrho^{2\ell}-2\varrho^{\ell}+1
2620: \geq
2621: \varrho^{\ell}(\varrho^{\ell}-2)
2622: \geq
2623: \varrho^{\ell}z
2624: \,.
2625: \end{equation*}
2626:
2627: Let $z':=xy-\varrho^{\ell}z$\@. We have to show that
2628: $z'\in[\varrho^{\ell}]$\@. Since $xy\geq \varrho^{\ell}z$ we have
2629: that $z'\geq 0$\@. For the sake of absurdity, assume that $z'\geq
2630: \varrho^{\ell}$\@. It follows that
2631: \begin{equation*}
2632: (x-1)y=xy-y = \varrho^{\ell}z+z'-y
2633: \geq
2634: \varrho^{\ell}z
2635: \end{equation*}
2636: since $y<\varrho^{\ell}$ and $z'\geq\varrho^{\ell}$\@. This
2637: contradicts the minimality of $xy-\varrho^{\ell}z$ since
2638: $xy>(x-1)y\geq \varrho^{\ell}z$\@.
2639: \end{proof}
2640:
2641: Our proof for the lower bound on the automata size for a formula
2642: $\Prod_n$ is based on the following lemma about the set
2643: \begin{equation*}
2644: \MULT_m:=\set{(a,b,c)\in\Int^3}{a,b\in[\varrho^m]\text{ and }ab=c}
2645: \,,
2646: \end{equation*}
2647: for $m\geq 0$\@.
2648: \begin{lemma}
2649: \label{lem:mbit_multiplication}
2650: Let $m\geq 0$\@. Every DWA representing $\MULT_m$ has at least
2651: $\varrho^m$ states.
2652: \end{lemma}
2653: \begin{proof}
2654: For $m=0$, the claim is trivial. In the following, assume that $m>0$
2655: and that $\autA=(Q,\Sigma^3,\delta,q_{\rmI},F)$ is a DWA
2656: representing $\MULT_m$. Let $K$ be the set of words of the form
2657: $(0,0,0)(0,0,b_{m-1})\dots(0,0,b_0)\in(\Sigma^3)^*$ with
2658: $b_{m-1}\not=0$ and $b_0\leq\varrho-2$\@. Let $w\in K$ and let $z$
2659: be the integer that is encoded by the third track of $w$\@. It
2660: holds that
2661: \begin{equation*}
2662: \varrho^{m-1}\leq z\leq\varrho^m-2
2663: \,.
2664: \end{equation*}
2665: From Lemma~\ref{lem:mult_prefix} it follows that there are
2666: $x,y,z'\in[\varrho^m]$ such that
2667: \begin{equation*}
2668: xy=\varrho^mz+z'
2669: \,.
2670: \end{equation*}
2671: We conclude that for every prefix $u$ of a word in $K$ there is a
2672: word $v\in(\Sigma^3)^*$ such that $\toints{uv}\in\MULT_m$\@.
2673:
2674: Now, let $L$ be the set of all prefixes of $K$\@.
2675: %%
2676: Let $u,u'\in L\setminus\{\lambda\}$ with $u\not=u'$\@. Moreover, let
2677: $v\in(\Sigma^3)^*$ with $\toints{uv}\in\MULT_m$\@.
2678: %%
2679: The first and second tracks of $uv$ and $u'v$ encode both the pair
2680: $(x,y)$\@. The third tracks of $uv$ and $w'v$ are different. It
2681: follows that $\toints{u'v}\notin\MULT_m$ and hence,
2682: $\widehat{\delta}(q_{\rmI},u)\not=\widehat{\delta}(q_{\rmI},u')$\@.
2683: We conclude that the DWA $\autA$ must have a distinct state for
2684: every word in $L$\@.
2685:
2686: In the following, we determine the cardinality of $L$\@. For
2687: $0\leq i\leq m+1$, let $L_i:=\set{w\in L}{\length{w}=i}$\@. We have
2688: that $L_0=\{\lambda\}$, $L_1=\{(0,0,0)\}$,
2689: $L_2=\set{(0,0,0)b}{b\in\Sigma\setminus\{0\}}$, $L_i=\set{wb}{w\in
2690: L_{i-1}\text{ and }b\in\Sigma}$, for $3\leq i\leq m$, and
2691: $L_{m+1}=K$\@. It holds that
2692: \begin{equation*}
2693: \begin{array}{@{}r@{\,}c@{\,}l@{}}
2694: |L|&=&
2695: |L_0|+|L_1|+|L_2|+|L_3|+\dots+|L_m|+|L_{m+1}|
2696: \\
2697: &=&
2698: 1 + 1 + (\varrho-1) + (
2699: \varrho-1)\varrho + \dots + (\varrho-1)\varrho^{m-2} +
2700: (\varrho-1)\varrho^{m-1}-2
2701: \\
2702: &=&
2703: \varrho^m
2704: \,.
2705: \qed
2706: \end{array}
2707: \end{equation*}
2708: % We conclude that $\autA$ has at least $\varrho^m$ states.
2709: \end{proof}
2710:
2711:
2712: \begin{theorem}
2713: \label{thm:worst_case}
2714: Let $n\geq 0$\@. The size of every DWA representing
2715: $\Zrepresents{\Prod_n}$ is at most least
2716: $2^{\bigl\lfloor\frac{f(n+1)}{2\log_2\varrho}\bigr\rfloor}$\@.
2717: \end{theorem}
2718: \begin{proof}
2719: Assume that for $n\geq 0$, there is a DWA $\autB$ with less than
2720: $2^{\bigl\lfloor\frac{f(n+1)}{2\log_2\varrho}\bigr\rfloor}$ states
2721: representing the set $\Zrepresents{\Prod_n}$\@. Let
2722: $m:=\big\lfloor\frac{f(n+1)}{2\log_2\varrho}\big\rfloor$\@. It holds
2723: that $\MULT_m\subseteq \Zrepresents{\Prod_n}$ since
2724: $(\varrho^m-1)^2<\varrho^{2m}=2^{2m\log_2\varrho}\leq2^{f(n+1)}$\@.
2725: %
2726: It is straightforward to construct from $\autB$ a DWA
2727: representing the set $\MULT_m$ that has as many states as $\autB$ by
2728: making some of the accepting states in $\autB$ non-accepting. This
2729: contradicts Lemma~\ref{lem:mbit_multiplication}\@.
2730: \end{proof}
2731:
2732: \begin{remark}
2733: We make the following remarks on nondeterministic word automata and
2734: alternating word
2735: automata~\cite{Brzozowski_Leiss.1980,Chandra_Kozen_Stockmeyer.1981}\@.
2736: \begin{enumerate}[(i)]
2737: \item The proof of Theorem~\ref{thm:worst_case} carries over to
2738: nondeterministic word automata. That means, that we obtain the
2739: same lower bound for nondeterministic word automata as for DWAs
2740: although nondeterministic word automata can sometimes be
2741: exponentially more succinct than DWAs.
2742: %%In particular, we have
2743: %%that for the formula $\Prod_n$ every nondeterministic word
2744: %%automaton has at least
2745: %%$2^{\big\lfloor\frac{f(n+1)}{\log_2\varrho}\bigr\rfloor}$ states.
2746: \item A lower bound for the number of states of alternating word
2747: automata for the formula $\Prod_n$ is at least
2748: $\bigl\lfloor\frac{f(n+1)}{2\log_2\varrho}\bigr\rfloor$\@. This
2749: lower bound follows by contradiction from the remark~(i) above and
2750: the fact that an alternating word automaton can be translated to
2751: an equivalent nondeterministic word automaton with exponentially
2752: more states. \ignore{ Note that alternating word automata can be
2753: double exponentially more succinct than DWAs~\cite{???}\@.
2754: However, for $\Prod_n$ they can be at most exponentially more
2755: succinct.
2756:
2757: In the following, we sketch the construction of an alternating
2758: word automaton for $\Prod_n$ that has exponentially less states
2759: than any DWA for $\Prod_n$\@. \dots}
2760: \end{enumerate}
2761: \end{remark}
2762:
2763:
2764: \section{Conclusion}
2765: \label{CONCL}
2766:
2767: We analyzed the automata-theoretic approach for deciding Presburger
2768: arithmetic and established a tight upper bound on the automata size.
2769: Moreover, we improved the automata constructions
2770: in~\cite{Boigelot.1999,Wolper_Boigelot.2000,Ganesh_Berezin_Dill.2002}
2771: for equations and inequations and proved that our automata
2772: constructions are optimal.
2773:
2774:
2775: The main technique to prove the upper bound on the automata size was
2776: to relate deterministic word automata with the formulas constructed by
2777: a quantifier elimination method.
2778: %%
2779: This technique can also be used to prove upper bounds on the sizes of
2780: minimal automata for other logics that admit quantifier elimination
2781: and where the structures are automata
2782: representable~\cite{Khoussainov_Nerode.1994,Blumensath_Graedel.2000,Rubin.2004},
2783: \ie, these structures are provided with automata for deciding equality
2784: on the domain and the atomic relations of the structure. Prominent
2785: examples are the mixed first-order theory over the structure
2786: $(\mathbb{R},\Int,\mathbin{<},+)$~\cite{Boigelot_Jodogne_Wolper.2001,Weispfenning.1999}
2787: and the first-order theory of
2788: queues~\cite{Rybina_Voronkov.2001,Rybina_Voronkov.2003}\@.
2789:
2790:
2791:
2792: \ignore{
2793: the $\varrho$'s complement representation to represent
2794: integers as words, where the first letter in a word is been
2795: interpreted as the most significant bit (big Endian). Similar
2796: representations have been used
2797: in~\cite{Boigelot.1999,Wolper_Boigelot.2000,Ganesh_Berezin_Dill.2002}\@.
2798:
2799: Another representation for integers as words is to interpret the first
2800: letter of a word as the least significant bit (little
2801: Endian)~\cite{Boudet_Comon.1996,Bartzis_Bultan.2003}\@. We can switch
2802: from one representation to the other by reversing the words and
2803: languages.
2804: %
2805: The size of a DWA representing a PA definable set can be exponentially
2806: smaller by interpreting the first letter as the least significant bit.
2807: There are examples showing that such exponential reductions occur.
2808: (see appendix~\ref{app:Endian})\@. However, we have not found an
2809: example that shows the converse, \ie, where the least significant bit
2810: encoding has an exponentially larger minimal DWA than using the most
2811: significant bit encoding.
2812: %
2813: It is an open problem how the two representations are precisely
2814: related and which representation is superior in practice. We point
2815: out that our results rely on interpreting the first letter as the most
2816: significant bit. For instance, Theorem~\ref{thm:bound_qf_formula} does
2817: not carry over if the first letter is interpreted as the least
2818: significant bit. Using the formulas defined
2819: in~\cite{Fischer_Rabin.1974}, which are used to describe Turing
2820: machines in PA, and using lower bounds on the BDD size for $m$-bit
2821: multiplication~\cite{Bryant.1991}, it is straightforward to show a
2822: similar lower bound for the least significant bit encoding as in
2823: Theorem~\ref{thm:worst_case}\@. Note that we cannot use lower bounds
2824: on the sizes of BDDs (or more generally, branching programs) when
2825: using the most significant bit encoding since the reading of the next
2826: digits by a DWA involves a left bit shift.
2827:
2828:
2829:
2830:
2831: There are also \emph{nonstandard} numeration systems for representing
2832: integers, \eg~\cite{Frougny.2002}\@. In a nonstandard numeration
2833: system, the base is an infinite sequence of integers that has certain
2834: properties. A standard example is the sequence of Fibonacci numbers
2835: $(\mathit{fib}_i)_{i\geq 0}$: a natural number $n$ is represented as a
2836: word $b_{n-1}\dots b_0\!\in\!\{0,1\}^*$ with $n\!=\!\sum_{0\leq
2837: i<n}b_i\cdot\mathit{fib}_i$\@.
2838: %
2839: The relationship between nonstandard numeration systems and formal
2840: language theory has been investigated, \eg,
2841: in~\cite{Frougny.1992,Shallit.1994,Hollander.1998}\@. It remains as
2842: future work to investigate the sizes of DWAs using different
2843: nonstandard numeration systems.
2844: }
2845:
2846:
2847:
2848:
2849: %\begin{thebibliography}{...}
2850: %...
2851: %\end{thebibliography}
2852: \bibliographystyle{acmtrans}
2853: \bibliography{prsb}
2854:
2855: \begin{received}
2856: Received Month Year; revised Month Year; accepted Month Year
2857: \end{received}
2858:
2859: \end{document}
2860:
2861:
2862: