To apply bounded model checking, seek an initial path in a transition system satisfyingA satisfying assignment for its bounded encoding is enough to disprove the specification. Use a lasso path: positions $q_0,\dots ,q_k$ follow the transition relation, and a final arrow returns from $q_k$ to some $q_{\ell }$, $0\le \ell \le k$. The repeated part is $q_{\ell }\cdots q_k$. On such a lasso path, $GFr$ is equivalent to having $r$ true at some position of the repeated part.

For this example an explicit Boolean formula for the bounded search isHere $I(q)$ means $q\in \{s_0,s_3\}$ and $T(q,r)$ means that the source diagram has the arrow $q\to r$; each can be encoded by finite Boolean variables for the states. The loop requirements are the fairness assumption and the negated specification respectively. Unrolling the transition relation and adding a loop closure is the usual bounded model checking construction.^[ref]

At bound $k=0$, an initial self-loop would be needed. The only such choice is $q_0=s_3$, whose repeated label satisfies $a\wedge b$ and $a$. It violates both loop requirements. The other initial state, $s_0$, has no self-loop. Thus $E_0$ has no satisfying assignment.

At bound $k=1$, chooseBoth required arrows $s_0\to s_1$ and $s_1\to s_0$ exist. At $q_1$, $a$ is false and hence $a\wedge b$ is false, so both repeated-part requirements are true. Equivalently, the label values are $a(q_0)=b(q_0)=b(q_1)=1$ and $a(q_1)=c(q_0)=c(q_1)=0$. These values give a satisfying assignment of $E_1$, representing the fair counterexample $(s_0{s}_1{)}^{\omega }$. ConsequentlyHere the bound counts forward arrows before the returning arrow, so $k=1$ stores two positions and describes a two-state repeated part. There is no need for a completeness bound: the exhibited fair counterexample settles the negative answer. These satisfying assignments are checked directly; no claim of executing an external SAT solver is needed.

Denote the three families found in part (a) by $A=(s_0{s}_1{)}^{\omega }$, $B_n=(s_0{s}_1{)}^n{s}_2^{\omega }$ and $C_m=s_3^m{s}_4{s}_5^{\omega }$, where $n,m\ge 1$. All are fair paths in a transition system. The verdicts areEach verdict follows from the infinite path in a transition system semantics, rather than from a finite prefix alone.

For ${\phi }_1=FGa$, take $C_1=s_3{s}_4{s}_5^{\omega }$. From $s_4$ onwards, $a$ is always false, so there is no time after which $a$ is always true. Therefore the first specification fails, with fair counterexample $C_1$. The path in a transition system $A$ is another fair counterexample, because it encounters $s_1$, where $a$ is false, infinitely often. Each $B_n$ does satisfy $FGa$, since $s_2$ satisfies $a$ forever.

For ${\phi }_2=(X\neg a)\to FGa$, take $A$. Its next state is $s_1$, so $X\neg a$ is true, but $FGa$ is false as just shown. Thus the second specification fails, with fair counterexample $A$. Alternatively, $C_1$ has next state $s_4$, making its antecedent true and its consequent false. For $C_m$ with $m\ge 2$, the next state is still $s_3$, so this implication is true there because its antecedent is false; this does not rescue a universally quantified specification.

For ${\phi }_3=Ga$, the fair path in a transition system $C_1$ reaches $s_4$, where $a$ is false. Thus the third specification fails, with fair counterexample $C_1$. In fact every fair initial path in a transition system reaches $s_1$ or $s_4$, so none satisfies $Ga$.

For ${\phi }_4=b\mathrm{U}G\neg b$, strong until requires an eventual position satisfying $G\neg b$, together with $b$ at every earlier position. On $A$, $b$ is true forever, so $G\neg b$ never holds. Thus the fourth specification fails, with fair counterexample $A$. On each $B_n$, $b$ holds until entry into $s_2$, after which $\neg b$ holds forever. On each $C_m$, $b$ holds until entry into $s_5$, after which $\neg b$ holds forever. These latter paths in a transition system satisfy the strong until requirement.

For ${\phi }_5=b\mathrm{W}G\neg b$, weak until permits either the preceding strong until behavior or $Gb$. Every $B_n$ and $C_m$ satisfies the strong until behavior, and $A$ satisfies $Gb$. These exhaust the fair initial paths in a transition system. Therefore the fifth specification holds on every fair initial path. Allowing the left operand to continue forever is exactly what distinguishes this answer from the previous one.

For ${\phi }_6=(XXb)\mathrm{U}G\neg b$, the two next-time operators belong to the left operand of strong until. The fair path in a transition system $C_1$ has $b$ true at positions zero and one, then false at every position from two onwards. Therefore $G\neg b$ first holds at position two. But $XXb$ is false already at position zero, since $b$ is false at position two. A witness for strong until cannot occur at zero or one, where its right operand is false, or at two or later, where its left operand has already failed. Thus the sixth specification fails, with fair counterexample $C_1$.

Indeed, every fair initial path in a transition system fails the sixth specification. On $A$, the right operand never holds. On $B_n$ and $C_m$, let $j\ge 2$ be the first position of the permanent $\neg b$ tail. The left operand $XXb$ is false at $j-2$, strictly before any possible right-operand witness. This also checks that the two next-time operators cannot be ignored or shifted onto the whole strong until formula.

Use the two incoming initial arrows in the source figure: $I=\{s_0,s_3\}$. An atomic proposition is true precisely at the states whose displayed labels contain it. In particular, $c$ is false at every state. Hence $GF\neg c$ is true on every infinite path in a transition system, and the first implication in the fairness assumption imposes no restriction.

Write $p=a\wedge b$. The remaining implication is $FGp\to GF\neg b$. By the linear temporal logic duality $\neg FGp=GF\neg p$, it is equivalent tosince $\neg b$ implies $\neg p$. Thus a path is fair exactly when it visits states not labelled with both $a$ and $b$ infinitely often. This condition also follows directly: if $p$ eventually holds forever, then $b$ eventually holds forever and the required $GF\neg b$ is impossible; if $p$ does not eventually hold forever, the implication has a false antecedent.

Every initial path in a transition system in the upper component either alternates forever between $s_0$ and $s_1$, or makes finitely many alternations and then stays at $s_2$. These are all fair: the first visits $s_1$ infinitely often, and the second visits $s_2$ infinitely often; neither state satisfies $a\wedge b$.

In the lower component, a path in a transition system can stay at $s_3$ forever, or leave it after finitely many visits and pass through $s_4$ to $s_5$. The constant path in a transition system $s_3^{\omega }$ is unfair because $a\wedge b$ holds forever while $\neg b$ never holds. Every departing path in a transition system is fair because $s_5$ satisfies neither $a$ nor $b$. Here $v^{\omega }$ means infinite repetition of the finite word $v$. ThereforeThis notation lists initial paths in a transition system. If one instead allows arbitrary starting states, their suffixes starting at $s_1,s_2,s_4,s_5$ are fair as well; the fair paths in a transition system from each initial state, and hence all verdicts below, are unchanged.

A transition relation requires an explicit interpretation of the Boolean variables as current and next state bits. Take the four states $q_{00},q_{01},q_{10},q_{11}$. Encode the current state by $(u,x)$ and the next state by $(y,z)$, and defineThe extra current bit $u$ is deliberately unused by the Boolean formula. A four-state transition system normally needs four bits to describe a pair of states; a Boolean formula using only three of them simply describes a transition relation independent of the fourth bit.

When $x=0$, the condition is $y=1$, so the permitted next states are $q_{10}$ and $q_{11}$. When $x=1$, the condition is $y\vee z$, so the permitted next states are $q_{01},q_{10},q_{11}$. The resulting adjacency matrix, with rows and columns both ordered $q_{00},q_{01},q_{10},q_{11}$, isThe directed graph below plots all ten directed edges, including the three self-loops. No arrow enters $q_{00}$, but it is a valid state with two outgoing arrows. Every state has a successor. As permitted, no initial states are distinguished.

Choose the variable ordering of a binary decision diagram $y<x<z$. The Boolean cofactor with $y=1$ is the constant one, while the Boolean cofactor with $y=0$ is $x\wedge z$. Consequently the right panel in part (d) has the following arrows:Here an entry such as $0\to x$ denotes the zero arrow to the $x$ decision node. There are $\boxed{3+2=5}$ vertices: three decision nodes and two terminal nodes, saving one decision node relative to either of the previous orderings. Testing $y$ first is effective because its one branch settles the entire Boolean function immediately. The ordering $y<z<x$ works equally well.

This is also minimal among ordinary binary decision diagrams for this Boolean function. Each Boolean variable is essential: setting $y=0,z=1$ leaves $f=x$; setting $y=0,x=1$ leaves $f=z$; and setting $x=z=0$ leaves $f=y$. If a Boolean variable were never tested, the represented Boolean function could not depend on it. Thus at least three decision nodes are necessary, and the construction attains that bound.

A reduced ordered binary decision diagram is obtained by sharing equal terminal nodes, removing a decision node whose two children are equal, and sharing decision nodes with the same tested Boolean variable and the same ordered pair of children. Apply these rules to the binary decision tree in part (c) as follows.

The left panel below is therefore the resulting reduced ordered binary decision diagram. Its full description is

There are $\boxed{4+2=6}$ vertices: four decision nodes and two terminal nodes.

The original binary decision diagram also has four decision nodes and two terminal nodes, and is already reduced for $x<y<z$: the two $y$ decision nodes have different children and no decision node has two equal children. Thus reversing the order has not made this example smaller. Indeed $y\vee (x\wedge z)$ is unchanged by interchanging $x$ and $z$, and the new binary decision diagram is the original one with those two labels exchanged. The uniqueness of a reduced ordered binary decision diagram applies to a fixed variable ordering of a binary decision diagram; it does not assert that every ordering has the same size.

For a complete binary decision tree with variable ordering of a binary decision diagram $z<y<x$, first test $z$, then $y$, then $x$ on every branch. The four Boolean cofactors after the first two tests are

The eight terminal nodes, read from left to right in the figure, are $\boxed{0,0,1,1,0,1,1,1}$. The repeated tests are intentional: this is the full binary decision tree before any reduction.

For example, the branch $z=1,y=0,x=1$ ends at one, whereas $z=0,y=0,x=1$ ends at zero. This checks the dependence on $z$ that must survive the later reduction.

Splitting the Boolean function according to the first tested Boolean variable givesThe identity $y\vee (\neg y\wedge z)=y\vee z$ follows by considering $y=0$ and $y=1$. Using it and distributing Boolean conjunction over Boolean disjunction,The first two terms combine to $y$ because $x\vee \neg x=1$. This also explains the truth table: $y=1$ always makes the output one, while with $y=0$ the output is one exactly when both $x$ and $z$ are one.

Follow the binary decision diagram from its top decision node to a terminal node, choosing the outgoing arrow specified by each tested Boolean variable. If $x=0$, the left $y$ decision node returns $y$, independently of $z$. If $x=1$, the right $y$ decision node returns one when $y=1$ and otherwise returns $z$. Thus the truth table, with rows in the order $(x,y,z)$, is:

Thus the output column of the truth table, in the displayed order, is $\boxed{(0,0,1,1,0,1,1,1)}$. In particular, the skipped $z$ test on the left does not constrain $z$: both values give the same result.

Write $\epsilon ={\epsilon }_t$, $\alpha ={\alpha }_t$, and $s_i=y_i{h}_t(x_i)\in \{-1,1\}$. Correctly classified observations have $s_i=1$ and total $D_t$-weight $1-\epsilon$; incorrectly classified observations have $s_i=-1$ and total weight $\epsilon$. The normalizing constant in the AdaBoost update is thereforeFor $0<\epsilon <1$, the definition of $\alpha$ givesIf observation $i$ is correct, its multiplier in the normalized update isif it is incorrect, the multiplier isThe corresponding denominators are exactly $1+s_i(1-2\epsilon )$: they are $2(1-\epsilon )$ when $s_i=1$ and $2\epsilon$ when $s_i=-1$. ConsequentlyAs a check, the new total mass on correctly classified observations is $(1-\epsilon )/(2(1-\epsilon ))=1/2$, and the mass on incorrectly classified observations is $\epsilon /(2\epsilon )=1/2$. The update thus produces a probability distribution and assigns the two groups equal aggregate mass. When $\epsilon =1/2$, $\alpha =0$ and every individual weight is unchanged.

The displayed finite update assumes $0<{\epsilon }_t<1$. The usual weak learner guarantees ${\epsilon }_t<1/2$, but it can return a perfect classifier with ${\epsilon }_t=0$; then the logarithm is infinite and the normalized exponential formula is not defined. AdaBoost stops on that perfect hypothesis rather than executing this update. Similarly, the printed formula is not an ordinary finite update at ${\epsilon }_t=1$.

Use weighted decision stump optimization with the convention $\mathrm{sign}(0)=+1$, and write $w_j=D((x_j,y_j))$. For each coordinate $i$, sort the examples by their $i$th coordinate and group all equal coordinate values. For a threshold between the $k$th and $(k+1)$st distinct values, the decision stump predicts $-1$ on the left and $+1$ on the right. Its weighted misclassification risk isStart with a threshold below the minimum observed value. Every prediction is then $+1$, and the initial error is ${\sum }_{y_j=-1}{w}_j$. Sweep the threshold from left to right. When it passes an entire group $G$ of equal coordinate values, that group's prediction changes from $+1$ to $-1$, so updateRecord the smallest value and a threshold achieving it, including the final threshold above all observations, which predicts $-1$ everywhere on the sample. Representatives can be chosen strictly between successive distinct values; the two outer representatives are finite real numbers below the minimum and above the maximum.

Every threshold has exactly the same sample predictions as one of these representatives. In particular, if a threshold equals an observed value, the equality group is on the $+1$ side under the chosen sign function convention, which duplicates the representative immediately before that group. Thus the sweep includes every possible sample labelling by the stated decision stump. Repeating for all $n$ coordinates and returning the globally smallest error proves optimality.

Sorting costs $O(m\log m)$ per coordinate and the grouped sweep costs $O(m)$. The overall time complexity iswith $O(m)$ working storage when coordinates are processed one at a time. Pre-sorted coordinate orders can be reused across repeated AdaBoost rounds, leaving $O(nm)$ work per round for changing weights. The paper allows only the orientation $\mathrm{sign}(x_i-b)$; reversing its polarity would enlarge the hypothesis class and is unnecessary here.

The two-interval approximation by one interval supplies an approximation guarantee for every input probability distribution $D$. Merge overlapping target intervals, and write the target positive set as at most two disjoint ordered intervals $I_1,I_2$. Put $p_j=D(I_j)$ and $p=p_1+p_2$. If there is only one nonempty component, the target already belongs to the interval hypothesis class and has zero misclassification risk. If the interval notation permits empty intervals and the target is empty, choose that same empty interval in $H$.

In the two-component case, choosing the heavier component as the hypothesis loses only the lighter component, so its misclassification risk isAlternatively, choose the single interval $J$ spanning both components. This produces no false negatives, and its false positives lie in the gap. Its misclassification risk is at most $1-p$. Both candidates are in $H$, so there exists an interval $h^{\ast }$ withFor the last step, use $p/2\le 1/3$ if $p\le 2/3$, and $1-p\le 1/3$ if $p\ge 2/3$. This avoids any assumption that an empty interval or the whole real line belongs to $H$.

Use empirical risk minimization over intervals on independent labelled examples. The generalization result needed here is the VC uniform convergence theorem: for a binary hypothesis class of finite VC dimension $v$, there is a universal constant $A$ such that, for any labelled-data probability distribution and $0<\eta ,\delta <1$, a sample sizeensures, with probability at least $1-\delta$, that every hypothesis's empirical misclassification risk differs from its misclassification risk by at most $\eta$. This theorem does not require the labels to be realizable by the hypothesis class.^[ref]

The interval hypothesis class has VC dimension two: any two ordered points can receive all four labellings, whereas an interval cannot label three ordered points $1,0,1$. Take $\eta =1/24$ and choose an interval $\hat{h}$ minimizing the empirical misclassification risk. On the simultaneous convergence event,ThereforeSince $v$ and $\eta$ are fixed constants, $O(1+\log (1/\delta ))$ examples suffice, which is polynomial in $1/\delta$ as required by the paper's definition of weak PAC learning.

For completeness, empirical risk minimization over intervals is computationally effective. Sort the sample and group equal coordinates, since one interval cannot split identical inputs. Give each group weight equal to the number of positive labels minus the number of negative labels in that group. The number of empirical mistakes made by an interval is the total number of positives minus the total weight of the consecutive groups it contains. Select the consecutive block of maximum weight, or select a finite interval outside the sample if every nonempty block has negative weight. This enumerates all possible sample labellings by intervals and attains the minimum empirical misclassification risk; sorting and a maximum-block scan are sufficient. The time complexity is $O(m\log m)$.

An embedding is determined by its chosen increasing sequence of positions. Accordingly, the all-subsequence embedding kernel $K(x,y)$ counts pairs of embeddings, one in $x$ and one in $y$, that spell the same subsequence. The two embeddings are distinguished even when they spell the same word as another pair. The empty word contributes exactly one pair.

Let $n=|x|$, $p=|y|$, and define $F(i,j)=K(x_1\cdots x_i,y_1\cdots y_j)$ for prefixes. When either prefix is empty, only the empty word has an embedding in both, soTo derive a dynamic programming recurrence, count pairs that do not use position $i$ of $x$ or do not use position $j$ of $y$. Inclusion-exclusion givesThe remaining pairs use both final positions. These positions must be the final letters of the common word, so they contribute nothing if $x_i\ne y_j$. If $x_i=y_j$, deleting those two final positions is a bijection to arbitrary embedding pairs on the two shorter prefixes, including their empty pair. Their contribution is therefore $F(i-1,j-1)$. HenceEquivalently, when the final symbols agree the recurrence simplifies to $F(i,j)=F(i-1,j)+F(i,j-1)$; when they differ, subtract the diagonal term. Fill the table in increasing prefix order and return $F(n,p)$. The boundary values and the disjoint counting argument prove correctness by induction on $i+j$.

A one-row implementation of this dynamic programming uses the saved old diagonal entry:The assignment to diagonal retains the value from the previous row before F[j] was overwritten. Swapping $x$ and $y$ if necessary minimizes the row length. Thus the time complexity is $O(|x||y|)$ arithmetic operations and the extra space complexity is $O(\min (|x|,|y|))$ integer cells. Empty inputs return one immediately.

These counts include multiplicity: for $x=y=aa$, the empty word contributes $1$, the word $a$ contributes $2\cdot 2=4$, and $aa$ contributes $1$, giving $K(aa,aa)=6$, not three. More generally, each result is at most $2^{n+p}$, since it counts some pairs of position subsets. Exact integers therefore require $O(n+p)$ bits; the stated quadratic bound is an arithmetic-operation bound, with a conservative $O(np(n+p))$ bound for elementary bit arithmetic.

The proposed positive-semidefinite kernel is valid: for each finite string only finitely many coordinates ${\varphi }_u(x)$ are nonzero, so $x\mapsto ({\varphi }_u(x){)}_{u\in {\Delta }^{\ast }}$ is a well-defined feature map into the inner product space of finitely supported coordinate families, and its inner product is exactly $K$.

A real positive-semidefinite kernel on an input set $X$ is a function $K:X\times X\to \mathbb{R}$ for which there is an inner product space $\mathcal{F}$ and a feature map $\varphi :X\to \mathcal{F}$ satisfyingEquivalently, $K$ is symmetric and every finite Gram matrix $(K(x_i,x_j){)}_{i,j}$ is positive semidefinite: ${\sum }_{i,j}{a}_i{a}_{j}K(x_i,x_j)\ge 0$ for all real coefficients $a_i$. An infinite-dimensional Hilbert space is allowed.

Replace every inner product $x_i\cdot x_j$ in part (b) by $K(x_i,x_j)$ and solveThis is precisely the Lagrangian dual problem obtained by replacing each original input by $\varphi (x_i)$ in the primal problem. The weight vector it determines isand the intercept follows from the same Karush-Kuhn-Tucker conditions. For example, if ${\alpha }_i>0$,Thus training needs only the finite Gram matrix, even if the feature map has infinitely many coordinates. This is the kernel trick. The result is an affine linear classifier in the feature space; its boundary in the original input space can be nonlinear. The squared-slack diagonal term and the equality constraint remain unchanged.

Use Lagrange multipliers ${\alpha }_i\ge 0$ for $1-{\xi }_i-y_i(w\cdot x_i+b)\le 0$ and ${\mu }_i\ge 0$ for $-{\xi }_i\le 0$. The optimization Lagrangian isThe Lagrange dual function is the infimum over the now unconstrained primal variables. The first-order optimality conditions in $w$ and $b$ giveIf the latter equality fails, the infimum over $b$ is $-\infty$. The first-order optimality condition in ${\xi }_i$ givesSubstitution, or completing the square separately in $w$ and each ${\xi }_i$, producesprovided ${\sum }_i{\alpha }_i{y}_i=0$. For fixed nonnegative ${\alpha }_i$, this expression is maximized over ${\mu }_i\ge 0$ at ${\mu }_i=0$. Thus the simplest Lagrangian dual problem isIn particular, there is no upper box constraint ${\alpha }_i\le C$. That constraint belongs to the linear-slack penalty; squared slack instead contributes the displayed diagonal quadratic penalty. With $Y=\mathrm{diag}(y_1,\dots ,y_m)$ and Gram matrix $G_{ij}=x_i\cdot x_j$, the objective can also be writtenSince $G$ is positive semidefinite and $C>0$, the matrix in parentheses is positive-definite. The objective of the Lagrangian dual problem is therefore strictly concave, and the feasible maximizer is unique.

The primal problem is a convex optimization problem, and $w=0,b=0,{\xi }_i=2$ is strictly feasible for both families of inequalities. Slater's condition gives strong duality, so an optimum of the Lagrangian dual problem yields a primal optimum. The Karush-Kuhn-Tucker conditions supplyFor any $i$ with ${\alpha }_i>0$, the intercept is consequentlyAll such choices agree at an exact optimum. If all labels have one sign, the optimal coefficients can all be zero: choose $w=0$, $\xi =0$, and any constant intercept of that sign with magnitude at least one.

Take labels $y_i\in \{-1,1\}$ and fix the standard normalization in which the squared weight penalty has coefficient $1/2$. The squared-slack support vector machine, a form of soft-margin support vector machine, has primal problemThe slack variables of a support vector machine permit margin violations. Penalizing $\Vert w{\Vert }^2$ favors a wide support-vector-machine margin, while $C>0$ sets the cost of the violations. The intercept $b$ is unpenalized, and the resulting classifier is $h(x)=\mathrm{sign}(w\cdot x+b)$, with a fixed choice at zero. The square on ${\xi }_i$ is essential to the Lagrangian dual problem below.

Choose distinct points $x_1,\dots ,x_{d+2}$ of $S$. The $d+2$ vectors $(x_i,1)$ lie in the $(d+1)$-dimensional vector space ${\mathbb{R}}^{d+1}$, so they are linearly dependent. Hence there are real numbers ${\lambda }_i$, not all zero, such thatThe second equality forces both a positive and a negative coefficient. Put $I_{+}=\{i:{\lambda }_i>0\}$, $I_{-}=\{i:{\lambda }_i<0\}$, andRearranging the first equality givesEach side is a convex combination: the coefficients are positive and sum to one. Thus $z$ belongs to both convex hulls. Place the points with indices in $I_{+}$ in $A$, those with indices in $I_{-}$ in $B$, and assign every zero-coefficient point and every remaining point of $S$ to $A$. Then $A,B$ are nonempty, disjoint, and have union $S$. Adding points cannot shrink a convex hull, soThis proves the intersecting convex hull partition theorem, including when $S$ has more than $d+2$ points or is infinite: only the initial finite collection was needed.