\newcommand{\prog}{\mathcal{P}}
\section{Approach for Verifying Stabilization with SMT Solvers}
\label{sec:verify}
In this section, we present the approach of verifying self-stabilization properties with SMT solvers by utilizing techniques from bounded model checking.
Verification of stabilization consists of two parts: (1) verifying {\em closure} and (2) verifying {\em convergence}.
In Section \ref{sec:vercl}, we identify the formula whose satisfiability can be used to determine whether closure property is satisfied. In Section \ref{sec:verconv}, we identify the formula whose satisfiability can be used to determine whether convergence property is satisifed.
\subsection{Verifying Closure}
\label{sec:vercl}
Let $\prog$ be the given program and let $\inv{}$ be the legitimate state predicate to conclude that $\prog$ is stabilizing. Let $\transp{}$ be the predicate that characterizes transitions of $\prog$.
Observe that the closure property requires that if $(s_0, s_1)$ is a transition of program $\prog$ and state $s_0$ is a legitimate state then state $s_1$ is also a legitimate state.
Thus, this can be captured by formula $\neg \closureformula$, where
$\closureformula \ \ = \ \ (\invar{(s_0)} \wedge \transp{(s_0, s_1)} \wedge \neg\invar{(s_1)})$
{\bf Remark. } \ For compactness, the formula $\closureformula$ does not explicitly specify the program or the set of legitimate states that are inputs in deciding closure.
Based on whether $\closureformula$ is satisfiable or not, we have two scenarios, $SC_1$ and $SC_2$:
\begin{enumerate}
\item $SC_1:$ if $\closureformula$ is satisfiable then it proves that it is possible to begin in a legitimate state, execute a program transition and be in a state that is not a legitimate state. This implies that the closure property is not satisfied. Moreover, in this case, assignment to $s_0$ and $s_1$ (which in turn includes values of variables of the program in state $s_0$ and $s_1$) provides a counterexample.
\item $SC_2:$ if $\closureformula$ is unsatisfiable then this implies that the closure property is satisfied.
\end{enumerate}
\subsection{Verifying Convergence}
\label{sec:verconv}
We verify convergence by checking that starting from an arbitrary state, the program, say $\prog$, reaches a legitimate state (in $\inv{}$) in $k$ steps, where $k$ is a given parameter used in the verification. Observe that the convergence property requires us to consider a sequence of states, $s_0, s_1, \cdots, s_k$ such that each successive transitions are program transitions. Moreover, to verify (negation of) convergence requirement, we require that $\invar{(s_k)}$ should be false. Additionally, in this verification, we can utilize the closure requirement to add additional constraints requiring that $\invar{(s_j)}$, $0 \leq j \leq k$, should be false. Additionally, in bounded model checking, one typically adds constraint about what the initial state should be. Thus, the formula $\convformula$ used for verifying convergence is as follows:
\begin{tabbing}
$\convformula = \ $ \=
%$\initial{(s_0)} \wedge$\\
%\>
$\transp{(s_0, s_1)} \wedge \transp{(s_1, s_2)} \wedge \cdots \wedge \transp{(s_{k-1}, s_{k})}$\\
\> $\neg\invar{(s_0)} \wedge \neg\invar{(s_1)}\wedge \cdots \wedge \neg\invar{(s_k)}$\\\
\end{tabbing}
Based on whether $\convformula$ is satisfiable or not, we have the following two scenarios:
\begin{enumerate}
\item $SC_3:$ if $\convformula$ is satisfiable, convergence cannot be achieved in $k$ steps. In this case, the number of steps needs to be increased. If the state space of the program is finite and $k$ equals the number of states in the program then this implies that the convergence property is not satisfied.
\item $SC_4:$ if $\convformula$ is unsatisfiable, then it proves that even if we begin in an arbitrary state, it is impossible for the program to be in an illegitimate state if it executes for $k$ steps. In other words, the convergence property is satisfied.
\end{enumerate}