text:
\section{Conclusions}
In this paper, a new encoding technique of linear temporal logic into boolean logic is introduced, particularly optimized for managing quantitative future and past metric temporal operators.
The encoding is simple and intuitive in principle, but it is made more complex by the presence, typical of the technique, of backward and forward loops used to represent an ultimately periodic infinite domain by a finite structure.

We have shown that, for formulae that include an explicit time constant, like e.g.,  $\lozenge_{= t} \phi$, the new metric encoding permits an improvement, in the size of the generated SAT formula and in the SAT solving time, that is proportional to the numerical value of the time constant. In practical examples, the overall performance improvement is limited by other components of the encoding algorithm that are not related with the value of the time constants (namely, those that encode the structure of the time domain, or the non-metric operators). Therefore, the gain in performance can be reduced in the less favorable cases in which the analyzed formula contains few or no metric temporal operators, or the numerical value of the time constants is quite limited.

An extensive set of experiments has been carried out to asses its feasibility and effectiveness for Bounded Model Checking (and Bounded Satisfiability Checking).
Average speed up in SAT solving time was 62\%.
The experimental results show that the new metric encoding can successfully be
 applied when the property to analyze includes time constants
with a fairly high numerical value.

{\bf Acknowledgements:}
We thank Davide Casiraghi for his valuable
work on Zot's metric plugins.

\section*{Appendix: a Mono-infinite Encoding}\label{mono-enc}

In some sense, the mono-infinite encoding of PLTL is simpler, since
there is only the forward loop to be taken into account. On the other
hand, being the temporal structure mono-infinite, it is possible to
refer to time instants before 0 (e.g. by using $\bullet$ at instant
0).
The typical approach (see e.g. \cite{BH+06}) is to use a default
value for operators referring to instants outside the temporal
domain: in our case, $\bullet \phi$ at 0 is false for any $\phi$.
Because of this, it is necessary to introduce a dual operator for
representing the negation of $\bullet$, which we will denote by $\bullet'$.
Its semantics is given by the following formula:
\[
\bullet \phi \iff \neg \bullet'  \neg \phi.
\]

Next, we present the constraints of Section \ref{encoding}, modified
for a mono-infinite time structure.

\noindent {\em Propositional constraints}, with $p$ denoting a propositional symbol:
\[
\begin{array}{c|c}
    \phi  &  0 \le i \le k \\
    \hline
    p      &
    |[ p ]|_i   \iff  p \in S_i  \\
    \neg p &
    |[ \neg p ]|_i   \iff  p \not\in S_i  \\
    \phi_1 \land \phi_2 &
    |[ \phi_1 \land \phi_2 ]|_i  \iff  |[ \phi_1 ]|_i \land |[ \phi_2 ]|_i \\
    \phi_1 \lor \phi_2 &
    |[ \phi_1 \lor \phi_2 ]|_i   \iff  |[ \phi_1 ]|_i \lor |[ \phi_2 ]|_i \\
\end{array}
\]

\noindent {\em Temporal subformulae constraints}:
\[
\begin{array}{c|c}
    \phi  &  0 \le i \le k \\
    \hline

    \circ \phi_1 &
    |[ \circ \phi_1 ]|_i \iff |[ \phi_1 ]|_{i+1} \\

    \phi_1 {\mathcal U} \phi_2 &
    |[ \phi_1 {\mathcal U} \phi_2 ]|_i \iff
    |[ \phi_2 ]|_i \lor ( |[ \phi_1 ]|_i \land |[ \phi_1 {\mathcal U} \phi_2
    ]|_{i+1} ) \\

   \phi_1 {\mathcal R} \phi_2 &
   |[ \phi_1 {\mathcal R} \phi_2 ]|_i \iff
   |[ \phi_2 ]|_i \land ( |[ \phi_1 ]|_i \lor |[ \phi_1 {\mathcal R} \phi_2
   ]|_{i+1} ) \\

\end{array}
\]
\[
\begin{array}{c|c}
    \phi  &  1 \le i \le k+1 \\
    \hline

    \bullet \phi_1 &
    |[ \bullet \phi_1 ]|_i \iff |[ \phi_1 ]|_{i-1} \\

\bullet' \phi_1 &
    |[ \bullet' \phi_1 ]|_i \iff |[ \phi_1 ]|_{i-1} \\

    \phi_1 {\mathcal S} \phi_2 &
    |[ \phi_1 {\mathcal S} \phi_2 ]|_i \iff
    |[ \phi_2 ]|_i \lor ( |[ \phi_1 ]|_i \land |[ \phi_1 {\mathcal S} \phi_2
    ]|_{i-1} ) \\

   \phi_1 {\mathcal T} \phi_2 &
   |[ \phi_1 {\mathcal T} \phi_2 ]|_i \iff
   |[ \phi_2 ]|_i \land ( |[ \phi_1 ]|_i \lor |[ \phi_1 {\mathcal T} \phi_2
   ]|_{i-1} ) \\

\end{array}
\]

{\em Loop constraints}:
\[
\begin{array}{c|c}
    \hline
    \mathrm{Base} &
   \begin{array}{c}
    \neg l_0 \land \neg \mathrm{InLoop}_0
   \end{array}
    \\
    \hline
    1 \le i \le k &
    \begin{array}{c}
        (l_i \Rightarrow S_{i-1} = S_k ) \land
        (\mathrm{InLoop}_i \iff \mathrm{InLoop}_{i-1} \lor l_i) \\
        (\mathrm{InLoop}_{i-1} \Rightarrow \neg l_i) \land
        (\mathrm{LoopExists} \iff \mathrm{InLoop}_k) \\
    \end{array}
\end{array}
\]

\noindent {\em Eventuality constraints}:
\[
\begin{array}{c|c}
    \phi & \mathrm{Base} \\
    \hline

    \phi_1 {\mathcal U} \phi_2 &

    \neg \langle\langle \diamondsuit \phi_2 \rangle\rangle_0
    \land
    \left( \mathrm{LoopExists} \Rightarrow \left(
    \begin{array}{c}
        |[ \phi_1 {\mathcal U} \phi_2 ]|_k
        \Rightarrow
    \langle\langle \diamondsuit \phi_2 \rangle\rangle_k
    \end{array}
    \right) \right) \\

    \phi_1 {\mathcal R} \phi_2 &

   \langle\langle \Box \phi_2 \rangle\rangle_0
   \land
   \left(\mathrm{LoopExists} \Rightarrow \left(
   \begin{array}{c}
   |[ \phi_1 {\mathcal R} \phi_2 ]|_k
       \Leftarrow
   \langle\langle \Box \phi_2 \rangle\rangle_k
   \end{array}
\right)
\right)\\

\end{array}
\]
\[\begin{array}{c|c}
    \phi & 1 \le i \le k  \\
   \hline

    \phi_1 {\mathcal U} \phi_2 &

    \begin{array}{c}
    \langle\langle \diamondsuit \phi_2 \rangle\rangle_i \iff
    \langle\langle \diamondsuit \phi_2 \rangle\rangle_{i-1} \lor
    ( \mathrm{InLoop}_i \land |[ \phi_2 ]|_i )
    \end{array} \\

   \phi_1 {\mathcal R} \phi_2 &

   \begin{array}{c}
   \langle\langle \Box \phi_2 \rangle\rangle_i \iff
   \langle\langle \Box \phi_2 \rangle\rangle_{i-1} \land
   ( \neg \mathrm{InLoop}_i \lor |[ \phi_2 ]|_i ) \\
   \end{array} \\
\end{array}
\]

\noindent {\em Last state constraints}:
\[
\begin{array}{c|c}
    \mathrm{Base} &
    \neg \mathrm{LoopExists} \Rightarrow \neg |[ \phi ]|_{k+1}
    \\
    \hline
    1 \le i \le k &
    l_i \Rightarrow ( |[ \phi ]|_{k+1} \iff |[ \phi ]|_{i})
\end{array}
\]

\noindent {\em First state constraints}:
\[\begin{array}{c|c}
    \phi &  \text{at 0}  \\
    \hline
    \phi_1 {\mathcal S} \phi_2  &

    |[ \phi_1 {\mathcal S} \phi_2 ]|_0 \iff
    |[ \phi_2 ]|_0

    \\

   \phi_1 {\mathcal T} \phi_2 &

    |[ \phi_1 {\mathcal T} \phi_2 ]|_0 \iff
    |[ \phi_2 ]|_0

    \\

    \bullet \phi_1 &
    \neg |[ \bullet \phi_1 ]|_0 \\

    \bullet' \phi_1 &
    |[ \bullet' \phi_1 ]|_0 \\

\end{array}
\]

\medskip

\subsection*{Encoding of the metric operators}\label{mono-metric-stuff}

As before with the yesterday operator, for the mono-infinite encoding
of metric temporal operators we have to define, for all the metric
past operators, their duals w.r.t. negation.
Following the same notation used before, we will call
$\blacksquare'_{\sim t}$ the dual of $\blacksquare_{\sim t}$, and
$\blacklozenge'_{\sim t}$ the dual of $\blacklozenge_{\sim t}$.

By default, $\blacksquare_{\sim t}$, $\blacklozenge_{\sim t}$ are assumed to
be false when referring to time instants before 0, where
$\blacksquare'_{\sim t}$, $\blacklozenge'_{\sim t}$ are assumed to
be true.

The semantics of the metric past dual operators is given by the
following formulae:
\[
\blacksquare_{= t} \phi \iff
\blacklozenge_{= t} \phi \iff
\neg \blacklozenge'_{= t}  \neg \phi \iff
\neg \blacksquare'_{= t}  \neg \phi,
\]
\[
\blacksquare_{\le t} \phi \iff
\neg \blacksquare'_{\le t} \neg \phi,
\qquad
\blacklozenge_{\le t} \phi \iff
\neg \blacklozenge'_{\le t} \neg \phi.
\]

Next, we present the constraints of Sub-section \ref{metric-stuff}, modified
for a mono-infinite time structure.

\noindent {\em Metric constraints}:
\[
\begin{array}{c|c}
\phi & 0 \le j \le t-1 \\
	\hline

    \diamondsuit_{=t} \phi, \
    \Box_{\le t} \phi,  \
    \diamondsuit_{\le t} \phi &
	\MF{\phi}{j} \iff \bigvee_{i=1}^{k} l_i \land
	|[\phi]|_{i+\text{mod}(j,k-i+1)} \\
\end{array}
\]

\noindent {\em Temporal subformulae constraints}:
\[
\begin{array}{c|c}
    \phi  &  0 \le i \le k \\
    \hline

    \diamondsuit_{=t} \phi &

    |[ \diamondsuit_{=t} \phi ]|_i \iff |[ \phi ]|_{i+t},
    \text{ when } i+t \le k \\
&
    |[ \diamondsuit_{=t} \phi ]|_i \iff
    \MF{\phi}{t+i-k-1},
    \text{ elsewhere } \\

    \Box_{\le t} \phi &
    \Box_{\le t} \phi \iff
    \bigwedge_{j=1}^{\text{min}(t,k-i)} |[\phi]|_{i+j}
    \land
    \bigwedge_{j=k+1-i}^{t} \MF{\phi}{i+j-k-1}  \\

    \diamondsuit_{\le t} \phi &
    \diamondsuit_{\le t} \phi \iff
    \bigvee_{j=1}^{\text{min}(t,k-i)} |[\phi]|_{i+j}
    \lor
    \bigvee_{j=k+1-i}^{t} \MF{\phi}{i+j-k-1}  \\

\end{array}
\]
\[
\begin{array}{ccc}

\begin{array}{c|c}
\phi &  0 \le i < t \\
	\hline

  \blacklozenge_{= t} \phi &
\neg |[ \blacklozenge_{= t} \phi ]|_i
\\

 \blacklozenge'_{= t} \phi &
|[ \blacklozenge'_{= t} \phi ]|_i
\\

\blacksquare_{\le t} \phi &
\neg |[ \blacksquare_{\le t} \phi ]|_i
\\

\blacksquare'_{\le t} \phi &
|[ \blacksquare'_{\le t} \phi ]|_i
\\

  \blacklozenge_{\le t} \phi &
\neg |[ \blacklozenge_{\le t} \phi ]|_0
\\

  \blacklozenge'_{\le t} \phi &
|[ \blacklozenge'_{\le t} \phi ]|_0
\\
      \end{array}

&
\qquad
&

\begin{array}{c|c}
 \phi    &  t \le i \le k+1 \\
    \hline

    \blacklozenge_{=t} \phi &
    |[ \blacklozenge_{=t} \phi ]|_i \iff |[ \phi ]|_{i-t}
 \\

    \blacklozenge'_{=t} \phi &
    |[ \blacklozenge'_{=t} \phi ]|_i \iff |[ \phi ]|_{i-t}
 \\

    \blacksquare_{\le t} \phi &
    \blacksquare_{\le t} \phi \iff
    \bigwedge_{j=1}^{t} |[\phi]|_{i-j}  \\

    \blacksquare'_{\le t} \phi &
    \blacksquare'_{\le t} \phi \iff
    \bigvee_{j=1}^{t} |[\phi]|_{i-j}
     \\

    \blacklozenge_{\le t} \phi &
    \blacklozenge_{\le t} \phi \iff
    \bigvee_{j=1}^{t} |[\phi]|_{i-j}
     \\

    \blacklozenge'_{\le t} \phi &
    \blacklozenge'_{\le t} \phi \iff
    \bigwedge_{j=1}^{t} |[\phi]|_{i-j}  \\

\end{array}

\end{array}
\]

\noindent {\em Past in Loop constraints}:
\[
\begin{array}{c|c}
   \phi  &  1 \le i \le k \\
    \hline

    \blacklozenge_{=t} \phi &

    l_i \Rightarrow
    \left(
    \begin{array}{c}
    \bigwedge_{j=1}^{\text{min}(t,i)}
    (
        |[\phi]|_{i-j}
	\iff
	|[\phi]|_{k-\text{mod}(j-1,k-i+1)}
    ) \land \\

    \bigwedge_{j=1+i}^{t}
    \left(
    \begin{array}{c}
    \neg |[\phi]|_{k-\text{mod}(j-1,k-i+1)}
    \end{array}
    \right)
  \end{array}
  \right) \\

\\
    \blacklozenge'_{=t} \phi &

    l_i \Rightarrow
    \left(
    \begin{array}{c}
    \bigwedge_{j=1}^{\text{min}(t,i)}
    (
        |[\phi]|_{i-j}
	\iff
	|[\phi]|_{k-\text{mod}(j-1,k-i+1)}
    ) \land \\

    \bigwedge_{j=1+i}^{t}
    \left(
    \begin{array}{c}
    |[\phi]|_{k-\text{mod}(j-1,k-i+1)}
    \end{array}
    \right)
  \end{array}
  \right) \\
\end{array}
\]
\[
\begin{array}{c|c}
    \phi &  1 \le i \le k \\
    \hline
   \blacksquare_{\le t} \phi &

   \mathrm{InLoop}_i \Rightarrow
    \left(

    |[\blacksquare_{\le t} \phi]|_i \iff
\left(
    \begin{array}{c}
	    \bigwedge_{j=0}^{\text{min}(k-i,t-1)}
	    (
	    \mathrm{InLoop}_{\text{max}(0,i-t+j)}
\lor
	    |[\phi]|_{k-j}
	   ) \land \\
	    \bigwedge_{j=1}^{\text{min}(i,t)}
	    (
	    \neg \mathrm{InLoop}_{i-j}
\lor
	    |[\phi]|_{i-j}
	    )
    \end{array}

    \right)
    \right)

\\
  \blacksquare'_{\le t} \phi &

   \mathrm{InLoop}_i \Rightarrow
    \left(

    |[\blacksquare'_{\le t} \phi]|_i \iff
\left(
    \begin{array}{c}
	    \bigvee_{j=1}^{\text{min}(i,t)}
	    (
	    \mathrm{InLoop}_{i-j}
\land
	    |[\phi]|_{i-j}
	   ) \lor \\
	    \bigvee_{j=0}^{\text{min}(k-i,t-1)}
	    (
	    \neg \mathrm{InLoop}_{\text{max}(0,i-t+j)}
\land
	    |[\phi]|_{k-j}
	    )
    \end{array}

    \right)
    \right)
\\

  \blacklozenge_{\le t} \phi &

   \mathrm{InLoop}_i \Rightarrow
    \left(

    |[\blacklozenge_{\le t} \phi]|_i \iff
\left(
    \begin{array}{c}
	    \bigvee_{j=1}^{\text{min}(i,t)}
	    (
	    \mathrm{InLoop}_{i-j}
\land
	    |[\phi]|_{i-j}
	   ) \lor \\
	    \bigvee_{j=0}^{\text{min}(k-i,t-1)}
	    (
	    \neg \mathrm{InLoop}_{\text{max}(0,i-t+j)}
\land
	    |[\phi]|_{k-j}
	    )
    \end{array}

    \right)
    \right)
\\
   \blacklozenge'_{\le t} \phi &

   \mathrm{InLoop}_i \Rightarrow
    \left(

    |[\blacklozenge'_{\le t} \phi]|_i \iff
\left(
    \begin{array}{c}
	    \bigwedge_{j=0}^{\text{min}(k-i,t-1)}
	    (
	    \mathrm{InLoop}_{\text{max}(0,i-t+j)}
\lor
	    |[\phi]|_{k-j}
	   ) \land \\
	    \bigwedge_{j=1}^{\text{min}(i,t)}
	    (
	    \neg \mathrm{InLoop}_{i-j}
\lor
	    |[\phi]|_{i-j}
	    )
    \end{array}

    \right)
    \right)
\\

\end{array}
\]
\section{Encoding of metric temporal logic}\label{encoding}

We  describe next the encoding of PLTL formulae into boolean logic, whose result
includes additional information on the finite structure over which
a formula is interpreted, so that the resulting boolean
formula is satisfied in the finite structure if and only if the original
PLTL formula is satisfied in a (finite or possibly) infinite structure.
For simplicity, we present a variant of the bi-infinite encoding originally
published in \cite{PMS07}, and then introduce metric operators on it.
Indeed, when past operators are introduced over a mono-infinite structure
(e.g., \cite{BH+06}), however, the encoding can be tricky to define,
because of the asymmetric role of future and past: future operators do
extend to infinity, while past operators only deal with a finite prefix.
The reader may refer to \cite{PMS07}, and \cite{ictac08} for a more
thorough comparison between mono- and bi-infinite approaches to bounded
model checking.

\begin{figure*}

\begin{center}
\includegraphics[width=4.5in]{bezot-pict.pdf}
\caption{A bi-infinite bounded path.}\label{loop-pict}
\end{center}

\end{figure*}
\vspace{-0.5cm}
For brevity in the following we call state $S_i$ the set of
assignments of truth values to propositional variables at time $i$.
The idea on which the encoding is based is graphically depicted in
Figure \ref{loop-pict}. A ultimately periodic bi-infinite
structure has a finite representation that includes a
non periodic portion, and two periodic portions (one towards the future,
and one towards the past).
 The
interpreter of the formula (in our case, the SAT solver), when it
needs to evaluate a formula at a state beyond the last state
$S_k$, will follow the ``backward link'' and consider the states
$S_l$, $S_{l+1}$, ... as the states following $S_k$.
Analogously,  to evaluate a formula at a state precedent to the first state
$S_0$, it will follow the ``forward link'' and consider the states
$S_l'$, $S_{l'-1}$, ... as the states preceding $S_0$.

The encoding of the model (i.e. the operational description of the system,
if any) is standard - see e.g. \cite{BH+06}. In the following we focus on
the encoding of the logic part $\Phi$ of the system (or its properties).

Let $\Phi$ be a PLTL formula.
Its semantics is given as a set of boolean constraints over the so called
{\em formula variables}, i.e., fresh unconstrained propositional variables.
There is a variable $|[\phi]|_i$ for each subformula $\phi$ of $\Phi$ and
for each instant $0 \le i \le k+1$ (instant $k+1$, which is not explicitly
shown in Figure \ref{loop-pict}, has a particular role in the encoding, as
we will show next).

First, one needs to constrain the propositional operators
in $\Phi$. For instance, if $\phi_1 \land \phi_2$ is a subformula of $\Phi$,
then each variable $|[ \phi_1 \land \phi_2 ]|_i$ must be equivalent to the conjunction of
variables $|[ \phi_1 ]|_i$ and $|[ \phi_2 ]|_i$.

{\em Propositional constraints}, with $p$ denoting a propositional symbol:
\[
\begin{array}{c|c}
    \phi  &  0 \le i \le k \\
    \hline
    p      &
    |[ p ]|_i   \iff  p \in S_i  \\
    \neg p &
    |[ \neg p ]|_i   \iff  p \not\in S_i  \\
    \phi_1 \land \phi_2 &
    |[ \phi_1 \land \phi_2 ]|_i  \iff  |[ \phi_1 ]|_i \land |[ \phi_2 ]|_i \\
    \phi_1 \lor \phi_2 &
    |[ \phi_1 \lor \phi_2 ]|_i   \iff  |[ \phi_1 ]|_i \lor |[ \phi_2 ]|_i \\
\end{array}
\]

The following formulae define the basic temporal behavior of future PLTL
operators, by using their traditional fixpoint characterizations.

{\em Temporal subformulae constraints}:
\begin{equation}\label{tfc}
\begin{array}{c|c}
    \phi  &  -1 \le i \le k \\
    \hline

    \circ \phi_1 &
    |[ \circ \phi_1 ]|_i \iff |[ \phi_1 ]|_{i+1} \\

    \phi_1 {\mathcal U} \phi_2 &
    |[ \phi_1 {\mathcal U} \phi_2 ]|_i \iff
    |[ \phi_2 ]|_i \lor ( |[ \phi_1 ]|_i \land |[ \phi_1 {\mathcal U} \phi_2
    ]|_{i+1} ) \\

   \phi_1 {\mathcal R} \phi_2 &
   |[ \phi_1 {\mathcal R} \phi_2 ]|_i \iff
   |[ \phi_2 ]|_i \land ( |[ \phi_1 ]|_i \lor |[ \phi_1 {\mathcal R} \phi_2
   ]|_{i+1} ) \\

\end{array}
\end{equation}
\[
\begin{array}{c|c}
    \phi  &  0 \le i \le k+1 \\
    \hline

    \bullet \phi_1 &
    |[ \bullet \phi_1 ]|_i \iff |[ \phi_1 ]|_{i-1} \\

    \phi_1 {\mathcal S} \phi_2 &
    |[ \phi_1 {\mathcal S} \phi_2 ]|_i \iff
    |[ \phi_2 ]|_i \lor ( |[ \phi_1 ]|_i \land |[ \phi_1 {\mathcal S} \phi_2
    ]|_{i-1} ) \\

   \phi_1 {\mathcal T} \phi_2 &
   |[ \phi_1 {\mathcal T} \phi_2 ]|_i \iff
   |[ \phi_2 ]|_i \land ( |[ \phi_1 ]|_i \lor |[ \phi_1 {\mathcal T} \phi_2
   ]|_{i-1} ) \\

\end{array}
\]

Notice that such constraints do not consider the implicit
eventualities that the definitions of ${\mathcal U}$ and ${\mathcal S}$ impose (they
treat them as the ``weak'' until and since operators), nor
consider loops in the time structure.

To deal with eventualities and loops, one has to encode an infinite
structure into a finite one composed of $k+1$ states $S_0,
S_1, \ldots S_k$. The ``future'' loop can be described by means of other
$k+1$ fresh propositional variables $l_0, l_1, \dots l_k$,
 called {\em loop selector variables}. At most one of these loop selector variables may be
true. If $l_i$ is true then state $S_{i-1}=S_k$, i.e., the bit
vectors representing the state $S_{i-1}$ are identical to those for
state $S_k$. Further propositional variables, $\mathrm{InLoop}_i$ ($0 \le i
\le k $) and $\mathrm{LoopExists}$, respectively  mean that position $i$
is inside a loop and that a loop actually exists in the structure.
Symmetrically, there are new loop selector variables $l'_i$ to define the
loop which goes towards the past, and the corresponding
propositional letters $\mathrm{InLoop'}_i$, and
$\mathrm{LoopEsists'}$.

The variables defining the loops are constrained by the following set of formulae.

{\em Loop constraints}:
\[
\begin{array}{c|c}
    \hline
    \mathrm{Base} &
   \begin{array}{c}
    \neg l_0 \land \neg \mathrm{InLoop}_0 \land
    \neg l'_k \land \neg \mathrm{InLoop'}_k
   \end{array}
    \\
    \hline
    1 \le i \le k &
    \begin{array}{c}
        (l_i \Rightarrow S_{i-1} = S_k ) \land
        (\mathrm{InLoop}_i \iff \mathrm{InLoop}_{i-1} \lor l_i) \\
        (\mathrm{InLoop}_{i-1} \Rightarrow \neg l_i) \land
        (\mathrm{LoopExists} \iff \mathrm{InLoop}_k) \\
	\\
        (l'_i \Rightarrow S_{i+1} = S_0 ) \land
        (\mathrm{InLoop'}_i \iff \mathrm{InLoop'}_{i+1} \lor l'_i) \\
        (\mathrm{InLoop'}_{i+1} \Rightarrow \neg l'_i) \land
        (\mathrm{LoopExists'} \iff \mathrm{InLoop'}_0)
    \end{array}
\end{array}
\]

The above loop constraints state that the structure may have
at most one loop in the future and at most one loop in the past.
In the case of a cyclic structure, they allow the
SAT solver to nondeterministically select exactly one of the (possibly) many loops.

To properly define eventualities, we need to
introduce new propositional letters $\langle\langle \diamondsuit
\phi_2 \rangle\rangle_i$, for each $\phi_1 {\mathcal U} \phi_2$ subformula
of $\Phi$, and for every $0 \le i \le k+1$.
Analogously, we need
to consider subformulae containing the operator ${\mathcal R}$, such as
$\phi_1 {\mathcal R} \phi_2$, by adding the new propositional letters
$\langle\langle \Box \phi_2 \rangle\rangle_i$. This is also symmetrically
applied to ${\mathcal S}$ and ${\mathcal T}$, using
$\blacklozenge, \blacksquare$.
Then, constraints
on these eventuality propositions are quite naturally stated as
follows.

{\em Eventuality constraints}:
\[
\begin{array}{c|c}
    \phi & \mathrm{Base} \\
    \hline

    \phi_1 {\mathcal U} \phi_2 &

    \neg \langle\langle \diamondsuit \phi_2 \rangle\rangle_0
    \land
    \left( \mathrm{LoopExists} \Rightarrow \left(
    \begin{array}{c}
        |[ \phi_1 {\mathcal U} \phi_2 ]|_k
        \Rightarrow
    \langle\langle \diamondsuit \phi_2 \rangle\rangle_k
    \end{array}
    \right) \right) \\

    \phi_1 {\mathcal R} \phi_2 &

   \langle\langle \Box \phi_2 \rangle\rangle_0
   \land
   \left(\mathrm{LoopExists} \Rightarrow \left(
   \begin{array}{c}
   |[ \phi_1 {\mathcal R} \phi_2 ]|_k
       \Leftarrow
   \langle\langle \Box \phi_2 \rangle\rangle_k
   \end{array}
\right)
\right)\\

   \phi_1 {\mathcal S} \phi_2 &

    \neg \langle\langle \blacklozenge \phi_2 \rangle\rangle_k
    \land
    \left(
    \mathrm{LoopExists'} \Rightarrow \left(
    \begin{array}{c}
    |[ \phi_1 {\mathcal S} \phi_2 ]|_0
        \Rightarrow
    \langle\langle \blacklozenge \phi_2 \rangle\rangle_0
    \end{array}
    \right) \right) \\

   \phi_1 {\mathcal T} \phi_2 &

   \langle\langle \blacksquare \phi_2 \rangle\rangle_k
   \land
   \left(\mathrm{LoopExists'} \Rightarrow \left(
       \begin{array}{c}
   |[ \phi_1 {\mathcal T} \phi_2 ]|_0
       \Leftarrow
   \langle\langle \blacksquare \phi_2 \rangle\rangle_0
   \end{array}
   \right) \right) \\

\end{array}
\]

\[\begin{array}{c|c}
    \phi & 1 \le i \le k  \\
   \hline

    \phi_1 {\mathcal U} \phi_2 &

    \begin{array}{c}
    \langle\langle \diamondsuit \phi_2 \rangle\rangle_i \iff
    \langle\langle \diamondsuit \phi_2 \rangle\rangle_{i-1} \lor
    ( \mathrm{InLoop}_i \land |[ \phi_2 ]|_i )
    \end{array} \\

   \phi_1 {\mathcal R} \phi_2 &

   \begin{array}{c}
   \langle\langle \Box \phi_2 \rangle\rangle_i \iff
   \langle\langle \Box \phi_2 \rangle\rangle_{i-1} \land
   ( \neg \mathrm{InLoop}_i \lor |[ \phi_2 ]|_i ) \\
   \end{array} \\
\end{array}
\]
\[\begin{array}{c|c}
    \phi & 0 \le i \le k-1  \\
    \hline
    \phi_1 {\mathcal S} \phi_2  &

    \langle\langle \blacklozenge \phi_2 \rangle\rangle_i \iff
    \langle\langle \blacklozenge \phi_2 \rangle\rangle_{i+1} \lor
    \left(
    \begin{array}{c}
     \mathrm{InLoop'}_i
     \land
     |[ \phi_2 ]|_i
    \end{array}
    \right)

    \\

   \phi_1 {\mathcal T} \phi_2 &

   \langle\langle \blacksquare \phi_2 \rangle\rangle_i \iff
   \langle\langle \blacksquare \phi_2 \rangle\rangle_{i+1} \land
   \left(
   \begin{array}{c}
    \neg \mathrm{InLoop'}_i
    \lor
    |[ \phi_2 ]|_i
   \end{array}
   \right)

\end{array}
\]

The formulae in the following table provide the constraints that must
be included in the encoding, for any subformula $\phi$, to account for
the absence of a forward loop in the structure (the first line of the
table states that if there is no loop nothing is true beyond the
$k$-th state) or its presence (the second line states that if there is
a loop at position $i$ then state $S_{k+1}$ and $S_i$ are equivalent).

{\em Last state constraints}:
\begin{equation}\label{lsc}
\begin{array}{c|c}
    \mathrm{Base} &
    \neg \mathrm{LoopExists} \Rightarrow \neg |[ \phi ]|_{k+1}
    \\
    \hline
    1 \le i \le k &
    l_i \Rightarrow ( |[ \phi ]|_{k+1} \iff |[ \phi ]|_{i})
\end{array}
\end{equation}

Then, symmetrically to the last state, we must define first state
(i.e. 0 time) constraints (notice that in the bi-infinite encoding
instant -1 has a symmetric role of instant $k+1$).

{\em First state constraints}:
\begin{equation}\label{fsc}
\begin{array}{c|c}
    \mathrm{Base} &
    \neg \mathrm{LoopExists'} \Rightarrow \neg |[ \phi ]|_{-1}
    \\
    \hline
    0 \le i \le k-1 &
    l'_i \Rightarrow ( |[ \phi ]|_{-1} \iff |[ \phi ]|_{i})
\end{array}
\end{equation}

The complete encoding of $\Phi$ consists of the logical
conjunction of all above components, together with
$|[\Phi]|_0$ (i.e. $\Phi$ is evaluated only at instant 0).

\subsection{Encoding of the metric operators}\label{metric-stuff}

We present here the additional constraints one has to add to the previous
encoding, to natively support metric operators.
We actually implemented also a mono-infinite
metric encoding in Zot, but for simplicity we are focusing here only on the
bi-infinite one.

Notice that
\[
\diamondsuit_{\le t} \phi \iff \neg \Box_{\le t} \neg \phi,
\qquad
\diamondsuit_{=t} \phi \iff \Box_{=t} \phi,
\qquad
 \diamondsuit_{\ge t} \phi \iff \diamondsuit_{= t} \diamondsuit \phi
\]
(the past versions are analogous). Hence, in the following we will not
consider the $\Box_{=t}$,
$\diamondsuit_{\ge t}$, $\Box_{\ge t}$ operators, and their past counterparts.

Ideally, with an {\em unbounded} time structure, the encoding of the
metric operators should be the following one (considering only the future, as
the past is symmetrical):
\[
|[\diamondsuit_{=t}\phi]|_i \iff |[\phi]|_{i+t},
\ \ \ \ \ \ \ \ \ \ \ \
\ \ \ \ \ \ \ \ \ \ \ \
|[\Box_{\le t}\phi]|_i \iff \bigwedge_{j=1}^t|[\phi]|_{i+j}
\]

Unfortunately, the presence of a {\em bounded} time structure, in which
bi-infinity is encoded through loops, makes the encoding less
straightforward.
With simple PLTL one refers at
most to one instant in the future (or in the past) or to an eventuality.
As the reader may notice in the foregoing encoding,
this is still quite easy, also in the presence of loops.
On the other hand, the presence of metric operators, impacts directly to
the loop-based structure, as logic formulae can now refer to time instants
well beyond a single future (or past) unrolling of the loop.

To represent the values of subformulae inside the future and past loops, we introduce new propositional variables, $\MF{\cdot}{\cdot}$ for the future-tense operators, and $\MP{\cdot}{\cdot}$ for the past ones. For instance, for $\diamondsuit_{=5} \psi$, we introduce $\MF{\psi}{j}$, $0 \le j \le 4$, where the propositions $\MF{\psi}{j}$ are used to represent the value of $\psi$ \emph{j} time units after the starting point of the future loop. This means that, if the future loop selector is at instant 18 (i.e.
$l_{18}$ holds), then $\MF{\psi}{2}$ represents $|[\psi]|_{20}$ (i.e. $\psi$ at instant 18+2).
Analogously and symmetrically, $\MP{\psi}{j}$ are introduced for past
operators with argument $\psi$, and represent the value of $\psi$
\emph{j} time units after the starting point of the past loop. That is, if the past loop
selector is at instant 7 (i.e. $l'_7$), then $\MP{\psi}{2}$ represents
$|[\psi]|_{7-2}$.

The first constraints are introduced for any future or past metric formulae
in $\Phi$.
\begin{equation}\label{mfp}
\begin{array}{c|c}
\phi & 0 \le j \le t-1 \\
	\hline

    \diamondsuit_{=t} \phi, \
    \Box_{\le t} \phi,  \
    \diamondsuit_{\le t} \phi &
	\MF{\phi}{j} \iff \bigvee_{i=1}^{k} l_i \land
	|[\phi]|_{i+\text{mod}(j,k-i+1)} \\

    \blacklozenge_{=t} \phi,  \
    \blacksquare_{\le t} \phi,  \
    \blacklozenge_{\le t} \phi  &
	\MP{\phi}{j} \iff \bigvee_{i=0}^{k-1} l'_i \land
	|[\phi]|_{i-\text{mod}(j,i+1)} \\
\end{array}
\end{equation}

We now provide the encoding of every metric operator, composed of two
parts: the first one defines it inside the bounded portion of the
temporal structure (i.e. for instants $i$ in $0 \le i \le k$), and the
other one, based on \emph{MF} and \emph{MP}, for the loop portion.

\begin{equation}\label{enc1}
\begin{array}{c|c}
    \phi  &  -1 \le i \le k \\
    \hline

    \diamondsuit_{=t} \phi &

    |[ \diamondsuit_{=t} \phi ]|_i \iff |[ \phi ]|_{i+t},
    \text{ when } i+t \le k \\
&
    |[ \diamondsuit_{=t} \phi ]|_i \iff
    \MF{\phi}{t+i-k-1},
    \text{ elsewhere } \\

    \Box_{\le t} \phi &
    \Box_{\le t} \phi \iff
    \bigwedge_{j=1}^{\text{min}(t,k-i)} |[\phi]|_{i+j}
    \land
    \bigwedge_{j=k+1-i}^{t} \MF{\phi}{i+j-k-1}  \\

    \diamondsuit_{\le t} \phi &
    \diamondsuit_{\le t} \phi \iff
    \bigvee_{j=1}^{\text{min}(t,k-i)} |[\phi]|_{i+j}
    \lor
    \bigvee_{j=k+1-i}^{t} \MF{\phi}{i+j-k-1}  \\

\end{array}
\end{equation}

\[
\begin{array}{c|c}
 \phi    &  0 \le i \le k+1 \\
    \hline

    \blacklozenge_{=t} \phi &

    |[ \blacklozenge_{=t} \phi ]|_i \iff |[ \phi ]|_{i-t},
    \text{ when } i \ge t \\
&
    |[ \blacklozenge_{=t} \phi ]|_i \iff
    \MP{\phi}{t-i-1},
    \text{ elsewhere } \\

    \blacksquare_{\le t} \phi &
    \blacksquare_{\le t} \phi \iff
    \bigwedge_{j=1}^{\text{min}(t,i)} |[\phi]|_{i-j}
    \land
    \bigwedge_{j=i+1}^{t} \MP{\phi}{i+j-1}  \\

    \blacklozenge_{\le t} \phi &
    \blacklozenge_{\le t} \phi \iff
    \bigvee_{j=1}^{\text{min}(t,i)} |[\phi]|_{i-j}
    \lor
    \bigvee_{j=i+1}^{t} \MP{\phi}{i+j-1}  \\
\end{array}
\]

The most complex part of the metric encoding is the one
considering the behavior on the past loop of future operators, and on the future loop of the past operators.
First, let us consider the behavior of future metric operators on the past loop.

\begin{equation}\label{enc2}
\begin{array}{c|c}
    \phi  &  0 \le i \le k-1 \\
    \hline

    \diamondsuit_{=t} \phi &

    l'_i \Rightarrow
    \left(
    \begin{array}{c}
    \bigwedge_{j=1}^{\text{min}(t,k-i)}
    (
        |[\phi]|_{i+j}
	\iff
	|[\phi]|_{\text{mod}(j-1,i+1)}
    ) \land \\

    \bigwedge_{j=k-i+1}^{t}
    \left(
    \begin{array}{c}
    \MF{\phi}{i+j-k-1}
    \iff \\
	|[\phi]|_{\text{mod}(j-1,i+1)}
    \end{array}
    \right)
  \end{array}
  \right) \\

\\

    \Box_{\le t} \phi &

    \mathrm{InLoop}'_i \Rightarrow
    \left(

    |[\Box_{\le t} \phi]|_i \iff
    \left(
    \begin{array}{c}
	    \bigwedge_{j=1}^{\text{min}(k-i,t)}
	    (
	    \neg \mathrm{InLoop}'_{i+j}
\lor
	    |[\phi]|_{i+j}
	   ) \land \\
	    \bigwedge_{j=0}^{\text{min}(i,t-1)}
	    (
	    \mathrm{InLoop}'_{\text{min}(k,i+t-j)}
\lor
	    |[\phi]|_j
	    )
    \end{array}
    \right)
    \right)

\\

    \diamondsuit_{\le t} \phi &

    \mathrm{InLoop}'_i \Rightarrow
    \left(

    |[\diamondsuit_{\le t} \phi]|_i \iff
    \left(
    \begin{array}{c}
	    \bigvee_{j=1}^{\text{min}(k-i,t)}
	    (
	    \mathrm{InLoop}'_{i+j}
\land
	    |[\phi]|_{i+j}
	   ) \lor \\
	    \bigvee_{j=0}^{\text{min}(i,t-1)}
	    (
	    \neg \mathrm{InLoop}'_{\text{min}(k,i+t-j)}
\land
	    |[\phi]|_j
	    )
    \end{array}
    \right)
    \right)
\end{array}
\end{equation}

The main aspect to consider is the fact that, if $l'_i$ (i.e. the past loop
selector variable holds at instant $i$), then $i$ has two possible
successors: $i+1$ and 0.
Therefore, if $\diamondsuit_{=4} \phi$ holds at $i$ (which is inside the
past loop), then $\phi$ must hold both at $i+4$, and at $3$.
 This kind of constraint is captured by the upper formula for
 $\diamondsuit_{=t} \phi$, which
 relates the truth
 values of $\phi$ in instants outside of the past loop (i.e.,
$|[\phi]|_{i+j}$) with the instants inside (i.e.,
 $|[\phi]|_{\text{mod}(j-1,i+1)}$ represents the value of $\phi$ at instants
 going from 0 to $i$, if $l'_i$ holds).

Another aspect to consider is related to the size of the time constant used (i.e. $t$
in this case). Indeed, if $i+t > k$, then we are considering the behavior
of $\phi$ outside the bound $0..k$. This means that we need to consider the
behavior of $\phi$ also in the future loop, hence we refer to
    $\MF{\phi}{i+j-k-1}$ (see the lower formula for
$\diamondsuit_{=t} \phi$).

As far as $\Box_{\le t} \phi$  is concerned,
its behavior inside the past loop is in general expressed by two parts.
The first one considers $\phi$ inside the past loop, starting from
instant $i$ and going forward, towards the right end of the loop (i.e. where
$l'$ holds, say $i'$). This situation is covered by the upper formula for
 $\Box_{\le t} \phi$. If $i+t$ is still inside the past loop (i.e. $i+t \le
i'$), this suffices.
If this is not the case, we must consider the remaining instants, going
from $i'+1$ to $i+t$. Because we are considering the behavior {\em inside} the
past loop, the instant after $i'$ is $0$, so we must translate instants
outside of the loop (i.e. where $InLoop'$ does not hold), to instants going
from 0 to $i+t-i'-1$: in all these instants $\phi$ must hold.
 This constraint is given by the lower formula for
 $\Box_{\le t} \phi$.

The encoding for the past operators is symmetrical, and is the
following:
\[
\begin{array}{c|c}
     &  1 \le i \le k \\
    \hline

    \blacklozenge_{=t} \phi &

    l_i \Rightarrow
    \left(
    \begin{array}{c}
    \bigwedge_{j=2}^{\text{min}(t,i)}
    (
        |[\phi]|_{i-j}
	\iff
	|[\phi]|_{k-\text{mod}(j-1,k-i+1)}
    ) \land \\

    \bigwedge_{j=1+i}^{t}
    \left(
    \begin{array}{c}
    \MP{\phi}{j-i-1}
    \iff \\
    |[\phi]|_{k-\text{mod}(j-1,k-i+1)}
    \end{array}
    \right)
  \end{array}
  \right) \\

\\

   \blacksquare_{\le t} \phi &

   \mathrm{InLoop}_i \Rightarrow
    \left(

    |[\blacksquare_{\le t} \phi]|_i \iff
\left(
    \begin{array}{c}
	    \bigwedge_{j=1}^{\text{min}(i,t)}
	    (
	    \neg \mathrm{InLoop}_{i-j}
\lor
	    |[\phi]|_{i-j}
	   ) \land \\
	    \bigwedge_{j=0}^{\text{min}(k-i,t-1)}
	    (
	    \mathrm{InLoop}_{\text{max}(0,i-t+j)}
\lor
	    |[\phi]|_{k-j}
	    )
    \end{array}

    \right)
    \right)
\\

  \blacklozenge_{\le t} \phi &

   \mathrm{InLoop}_i \Rightarrow
    \left(

    |[\blacklozenge_{\le t} \phi]|_i \iff
\left(
    \begin{array}{c}
	    \bigvee_{j=1}^{\text{min}(i,t)}
	    (
	    \mathrm{InLoop}_{i-j}
\land
	    |[\phi]|_{i-j}
	   ) \lor \\
	    \bigvee_{j=0}^{\text{min}(k-i,t-1)}
	    (
	    \neg  \mathrm{InLoop}_{\text{max}(0,i-t+j)}
\land
	    |[\phi]|_{k-j}
	    )
    \end{array}

    \right)
    \right)

\end{array}
\]

The actual implementation of the metric encoding contains some
optimizations, not reported here for the sake of brevity, like the re-use,
whenever possible, of the various $\MF{\cdot}{\cdot}$, and
$\MP{\cdot}{\cdot}$ propositional letters.

\medskip

{\bf A first assessment of the encoding} The behavior of the new
encoding has been first experimented on a very simple specification of
a synchronous shift-register, where, at each clock tick, an input bit
is shifted of one position to the right.  A specification of this
system can be described by the following formula:
\[ Alw(in \leftrightarrow \diamondsuit_{=d}out) \]
where $in$ is true when a bit enters the shift register, $out$ is true when a bit ``exits'' the register after a delay $d$ (a constant representing the number of memory bits in the register).
The Zot toolkit has been applied to this simple specification, using the
nonmetric,
PLTL-only encoding (i.e. the one presented in \cite{PMS07}) and the
new metric encoding.

The implemented nonmetric encoding is the one presented in
the current section, without the metric part of Sub-section \ref{metric-stuff}.
In practice, this means that every metric temporal operator is
translated into PLTL before applying the encoding, by means of its
definition of Section \ref{preliminaries}.

The experimental results (with
the same hardware and software setup described in Section \ref{results}
are graphically shown in Figure~\ref{shiftSync}, where Gen represents the generation phase, i.e., the generation of a boolean formula in conjunctive normal form, starting from the above specification, and SAT represents  the verification phase, performed by a SAT solver, with a bound $k=400$ and various values of delay $d$ (from 10 to 150).
The first two upper diagrams show the time, in seconds, for Gen and SAT phases, using either a PLTL encoding or the metric encoding, as a function of delay $d$, while the third upper diagram shows the speedup, as a percentage of speed increase over the PLTL encoding, when using the metric encoding, again as a function of delay $d$.
As one can see, the speed up obtained for both the Gen and SAT phases is proportional to delay $d$, and can be quite substantial (up to 250\% for SAT and 300\% for Gen phases).
The three lower diagrams report, in a similar way, on the size of the generated boolean formula, in terms of the thousands of variables (Kvar) and clauses (Kcl): the reduction in the size of the generated encoding increases with the value of $d$ and tends to reach a stable value around 60\%.

These results can be explained by comparing the two encodings. In the previous, non-metric encoding the formula $\diamondsuit_{=d}out$ is translated into $d$ nested applications of the next-time operator, $\circ^{d} out$, hence there are $d+1$ subformulae, $\circ^{i} out$ for $0 \leq i \leq d$. For each of these the encoding procedure generates $k+2$ boolean variables, $k$ last state constraints of type (\ref{lsc}), $k$ first state constraints of type (\ref{fsc}), and $k+2$ temporal subformulae constraints of type (\ref{tfc}) for a total of $(d+1) \cdot (k+2)$ variables and $(d+1) \cdot (3 \cdot k + 2)$ constraints. In summary, in the nonmetric encoding we have $O(d \cdot k)$ variables and $O(d \cdot k)$ constraints.
On the contrary, in the metric encoding of $\diamondsuit_{=d}out$ there are only two subformulae, $\diamondsuit_{=d}out$ itself and $out$. Now the encoding procedure generates $2 \cdot (k+2)$ variables, plus $2 \cdot d$ \textit{MF} variables (see equation \ref{mfp}), for a total of $2 \cdot (d + k + 2)$ variables. It also generates $4 \cdot k$ first and last state constraints of type (\ref{lsc}) and (\ref{fsc}), $k$ constraints of type (\ref{enc1}) plus $d$ constraints of type (\ref{mfp}), each of these having size $O(k)$, and $k$ constraints of type (\ref{enc2}) having size $O(d)$; overall, we have therefore $4 \cdot k + d$ constraints, and their total size is significantly smaller that in the nonmetric encoding, though it is still $O(d \cdot k)$. Thus in the metric encoding we have $O(d + k)$ (less than in the nonmetric case) variables and $O(d \cdot k)$ constraints (same as in the nonmetric case but with a smaller constant factor). The analysis of the other metric temporal operators, $\Box_{\le t} \phi$ and $\diamondsuit_{\le t} \phi$, leads to similar conclusions.

\begin{figure}
\begin{center}
\includegraphics[width=14cm]{Diag-shiftSync.pdf}
\caption{Summary of experimental data for the synchronous version of a
Shift Register.}
\label{shiftSync}
\end{center}
\end{figure}

\section{Introduction}\label{introduction}
In Bounded Model Checking \cite{BCCZ99} a system under analysis is
modeled as a finite-state transition system and a property to be
checked is expressed as a formula in temporal logic. The model and the property are
both suitably translated into boolean logic formulae, so that the
model checking problem is expressed as an instance of a SAT problem,
that can be solved efficiently thanks to the significant improvements
that occurred in recent years in the technology of the SAT-solver
tools \cite{Chaff01,ES03}. Infinite,
ultimately periodic temporal structures that assign a value to every
element of the model alphabet are encoded through a finite set of
boolean variables, and the cyclic structure of the time domain is
encoded into a set of {\em loop selector variables} that mark the
start and end points of the period.  As it usually occurs in a model checking
framework, a (bounded) model-checker tool can either prove a property
or disprove it by exhibiting a counter example, thus providing means
to support simulation, test case generation, etc.

In previous work \cite{PMS07}, we introduced techniques for managing
bi-infinite time in bounded model checking, thus allowing for a more
simple and systematic use of past operators in Linear Temporal Logic.
In
\cite{ictac08,ase08}, we took advantage of the fact that, in bounded
model-checking, both the model and the formula to be checked are ultimately
translated into boolean logic.
This permits to provide the model not only as a state-transition system, but, alternatively, as a set of temporal logic formulae. We call this a \textit{descriptive} model, as opposed to the term \textit{operational} model used in case it consists of a state-transition system.
The descriptive model is much more readable and concise if the adopted logic includes past and metric temporal operators, allowing for a
great flexibility in the degree of detail and abstraction that the designer can adopt in providing the system model.
The model-checking problem is reduced to the problem of satisfiability for a boolean formula that encodes both the modeled system and its conjectured property to be verified, hence the name Bounded \emph{Satisfiability} Checking that we adopted for this approach.

In this paper we take a further step to support efficient Bounded Satisfiability- and Bounded Model-checking by introducing a new encoding technique that is particularly efficient in case of temporal logic formulae that contain time constants having a high numerical value.

In previous approaches \cite{BH+06,PMS07,ictac08,ase08} the operators of temporal logic
that express in a precise and quantitative way some timing constraints were
encoded by (rather inefficiently) translating them into
combinations of non-metric Linear Temporal Logic operators. For instance,
the metric temporal logic formula $\lozenge_{=d} P$, which asserts that
property P holds at $d$ time units in the future (w.r.t the implicit
present time at which the formula is asserted) would be translated into $d$
nested applications of the LTL next-time operator, $\circ^d P$, and then encoded as a series of operator applications, with obvious overhead.

The new encoding for the metric operators translates the time constants in a way that makes the resulting boolean formula much more compact, and the verification carried out by the SAT solver-based tools significantly faster.

Thus our technique can be usefully applied to all cases where temporal logic formulae that embed important time constants are used. This is both the case of Bounded Satisfiability Checking, where the system model is expressed as a (typically quite large) set of  metric temporal logic formulae, and also of more traditional Bounded Model Checking, when the model of the system under analysis is provided by means of a state transition system but one intends to check a hard real-time property with explicit, quantitatively stated timing constraints.

The paper is structured as follows. In Section 2 we provide background and
motivations for our work. Section 3 introduces the new metric encoding and
analyzes its main features and properties. Section 4 provides an assessment
of the new encoding by reporting the experimental results obtained on a set
of significant benchmark case studies. Finally, in Section 5 we draw
conclusions

\section{Preliminaries}\label{preliminaries}
In this section, to make the paper more readable and self-contained, we provide background material on Metric Temporal Logic and bi-infinite time, on Boundel Model- and Satisfiability-Checking, and on the Zot toolkit.

\subsection{A metric temporal logic on bi-infinite time}

We first recall here Linear Temporal Logic with past operators (PLTL),
in the version introduced by Kamp \cite{K68}, and next extend it with metric temporal operators.

{\bf Syntax of PLTL} The alphabet of PLTL includes: a finite set $Ap$
of propositional letters; two propositional connectives $\neg, \vee$
(from which other traditional connectives such as $\top, \bot, \neg,
\vee, \wedge, \rightarrow, \dots$ may be defined); four temporal
operators (from which other temporal operators can be derived):
``until''  ${\mathcal U}$,  ``next-time'' $\circ$,
``since'' ${\mathcal S}$ and  ``past-time'' (or Yesterday)
, $\bullet$. Formulae are defined in the usual inductive way:
a propositional letter $p\in Ap$ is a formula; $\neg\phi, \phi \vee
\psi, \phi {\mathcal U} \psi, \circ\phi, \phi {\mathcal S} \psi, \bullet\phi$, where
$\phi, \psi$ are formulae; nothing else is a formula.

The traditional ``eventually'' and ``globally'' operators may be defined as: $
\lozenge \phi$ is $\top {\mathcal U}\phi$, $\square \phi$ is $\neg\lozenge\neg
\phi$. Their past counterparts are: $ \blacklozenge \phi$ is $\top
{\mathcal S}\phi$, $\blacksquare \phi$ is $\neg\blacklozenge\neg
\phi$.
Another useful operator for PLTL is  ``Always'' ${\mathcal Alw }$,
defined as ${\mathcal Alw } \; \phi := \Box \phi \land \blacksquare
\phi$. The intended meaning of ${\mathcal Alw } \; \phi$ is that $\phi$ must hold
in every instant in the future and in the past. Its dual is
``Sometimes'' ${\mathcal Som } \; \phi$ defined as $\neg {\mathcal Alw } \neg \phi$.

The dual operators of Until and Since, i.e.,  ``Release''
${\mathcal R}$: $\phi {\mathcal R} \psi$ is $\neg(\neg \phi {\mathcal U} \neg \psi)$, and, respectively,
 ``Trigger'' ${\mathcal T}$: $\phi {\mathcal T} \psi$ is $\neg(\neg
\phi {\mathcal S} \neg \psi)$, allow
the convenient {\em
  positive normal form}:
Formulae are in positive normal form if their alphabet is
$\{\wedge, \vee, {\mathcal U}, {\mathcal R}, \circ,{\mathcal S},\bullet, {\mathcal T} \} \cup Ap \cup
\overline{Ap}$, where $\overline{Ap}$ is the set of formulae of the
form $\neg p$ for $p\in Ap$. This form, where negations may only occur on atoms,
is very convenient when defining encodings of PLTL into
propositional logic. Every PLTL formula $\phi$ on the
alphabet $\{\neg, \vee, {\mathcal U}, \circ,{\mathcal S}, \bullet\} \cup Ap$ may be
transformed into an equivalent formula $\phi'$ in positive normal
form.

For the sake of brevity, we also allow
$n$-ary predicate letters (with $n\ge1$) and the $\forall,
\exists$ quantifiers as long as their domains are finite. Hence,
one can write, e.g., formulae of the form: $ \exists p \
\mathrm{gr}(p) $, with $p$ ranging over $\{1,2,3\}$ as a shorthand
for $\bigvee_{p\in\{1,2,3\}} \mathrm{gr}_p$.

{\bf Semantics of PLTL }
In our past work \cite{PMS07}, we have introduced a variant of bounded model
checking where the underlying, ultimately periodic timing structure was not
bounded to be infinite only in the future, but may extend indefinitely also
towards the past, thus allowing for a simple and intuitive modeling of
continuously functioning systems like monitoring and control devices. In
\cite{ictac08}, we investigated the performance of verification in many
case studies, showing that tool performance on bi-infinite structures is
comparable to that on mono-infinite ones. Hence adopting a bi-infinite
notion of time does not impose very significant penalties to the efficiency
of bounded model checking and bounded satisfiability checking. Therefore, in what follows, we present only the simpler bi-infinite semantics of PLTL.  Each experiment of Section \ref{casestudy} use either bi-infinite time (when there are past operators) or mono-infinite time (typically, when there are only future operators).

A bi-infinite word $S$ over alphabet $2^{Ap}$ (also called
a ${\mathbb Z}$-word) is a function $S:{\mathbb Z} \longrightarrow 2^{Ap}$. Hence,
each position $j$ of $S$, denoted by $S_j$, is in $2^{Ap}$ for every $j$. Word $S$ is also denoted as $\dots
S_{-1}S_0S_{1}\dots$.  The set of all
bi-infinite words over $2^{Ap}$ is denoted by $(2^{Ap})^{\mathbb Z}$.

For all PLTL formulae $\phi$, for all $S\in (2^{Ap})^{\mathbb Z}$, for all
integer numbers $i$, the satisfaction relation  $S,i\models \phi$ is
defined as follows.

$\begin{array}{l}
S,i\models p,  \Longleftrightarrow p\in S_i, \mathrm{for } \ p\in Ap  \\
S,i\models \neg\phi \Longleftrightarrow S,i\not\models \phi\\
S,i\models \phi\vee\psi \Longleftrightarrow  S,i\models \phi \ \mathrm{or} \ S,i\models \psi\\
S,i\models \circ\phi \Longleftrightarrow  S,i+1\models \phi\\
S,i\models \phi{\mathcal U}\psi \iff
\exists k\ge 0 \mid  S,i+k \models
\psi, \ \mathrm{and} \  S,i+j \models \phi  \ \forall 0\le j< k\\
S,i\models \bullet\phi \Longleftrightarrow S,i-1\models \phi\\
S,i\models \phi{\mathcal S}\psi \iff
\exists k\ge 0 \mid S,i-k \models
\psi, \ \mathrm{and} \ S,i-j \models \phi  \ \forall 0\le j< k\\
  \ \\
\end{array}
$

{\bf Metric temporal operators }
Metric operators are
very convenient for modeling hard real time systems, with quantitative time constraints.
The operators introduced in this section do not actually extend the expressive power of PLTL, but
may lead to more succinct formulae. Their semantics is defined by a straightforward translation $\tau$
into PLTL.

Let $\sim \in\{\le, =, \ge \}$), and $c$ be a natural number.
We consider here two metric operators, one in the future and one in the past:
the bounded eventually  $ \lozenge_{\sim c} \phi$, and its past counterpart
$ \blacklozenge_{\sim c} \phi$.
The semantics of the future operators is the following (the past versions
are analogous):
$$
\begin{array}{l}
    \tau(\lozenge_{= 0} \phi) := \phi \\

    \tau(\lozenge_{= t} \phi) := \circ \tau(\lozenge_{= t-1} \phi),
    \mathrm{ for}\  t > 0 \\

    \hline

    \tau(\lozenge_{\le 0} \phi) := \phi \\

    \tau(\lozenge_{\le t} \phi) :=
    \phi \lor \circ  \tau(\lozenge_{\le t-1} \phi),
    \mathrm{ for}\  t > 0 \\

    \hline

    \tau(\lozenge_{\ge 0} \phi) := \lozenge\phi \\

    \tau(\lozenge_{\ge t} \phi) :=
    \circ \tau(\lozenge_{\ge t-1} \phi),
    \mathrm{ for }\  t > 0 \\

\end{array}
$$

Versions of the bounded operators with $\sim \in\{<,>\}$ may be introduced as a shorthand. For instance,
 $\lozenge_{>0} \phi $ stands for $\circ\lozenge_{\ge 0}\phi$.
Other two dual operators are ``bounded globally'': $\square_{\sim c} \phi$ is  $\neg\lozenge_{\sim c}\neg \phi$,
and its past counterpart is $\blacksquare_{\sim c} \phi$,  which is defined as
$\neg\blacklozenge_{\sim c}\neg \phi$.

Other metric operators are commonly introduced as primitive, such as
bounded versions of ${\mathcal U}$ and ${\mathcal S}$ (see e.g. \cite{PMS07}), and then
the bounded eventually operators are derived from them. In our
experience, however, the four operators above are much more common in
specifications, therefore we chose to implement them as native and
leave the others as derived.

Notice that dual w.r.t. negation of metric past  operators, together
with $\bullet$, must be introduced for mono-infinite temporal
structures, to take into account the possibility of referring to
instants outside the temporal domain. In the rest of the paper we
will assume the temporal domain bi-infinite. The complete
mono-infinite encoding is presented in the appendix.

\subsection{Bounded Model Checking vs. Bounded Satisfiability Checking}\label{DvsO}

The traditional approach to verification of finite state systems is based on building an {\em operational model} of the system to be analyzed,
i.e., a set
of clauses that constrain the transition of the system from a
state valid in one given instant, the {\em current state}, to the
{\em next state}, reached by the modeled system in the successive time
instants.
The property to be
checked, however, is expressed with a different formalism, namely as a formula in temporal logic.
Model checking tools, such as bounded model checkers like SMV, take these two descriptions as input and
check whether the property is verified on the system, or compute a counterexample.

However, often systems may be described using a complementary style of modeling,  called the {\em descriptive approach}
This is based on the
idea of characterizing the modeled system through its {\em fundamental
properties}, described by means of  temporal logic formulae on an alphabet of
items that correspond to the interface of the system with the
external world, without considering any possible further internal
components that might be necessary for its functioning. Such
formulae are {\em not} constrained in any way in their form: they may
refer to any time instant, possibly relating actions
and events occurring at any arbitrary distance in time, or they
may constrain values and behaviors for arbitrarily long time
intervals.

Hence, in the descriptive approach both the system under analysis and the property to be checked are expressed in a single uniform notation as formulae of temporal
logic. In this setting, which we called bounded {\em
 satisfiability} checking (BSC \cite{PMS07}), the system under analysis is characterized by a formula $\phi$
(that in all non-trivial cases would be of significant size) and the
additional property to be checked (e.g. a further desired requirement)
is expressed as another (usually much smaller) formula $\psi$. A
bounded model checker in this case is used to prove that any
implementation of the system under analysis possessing the assumed
fundamental properties $\phi$ would also ensure the additional
property $\psi$; in other terms, the model checker would prove that
the formula $\phi \to \psi$ is valid, or equivalently that its
negation is not satisfiable (hence the term \emph{satisfiability checking}).

Satisfiability verification is very useful, in its simplest form, as a
means for performing a sort of testing \cite{FM94} or {\em sanity check} of the specification \cite{MPSS03,RV07}, or to prove properties of correct implementation \cite{ase08} or, more generally, it allows the designer to perform System Requirement Analysis \cite{GM01}. The adoption of a descriptive style in modeling a system under analysis is made possible by the use of Metric Temporal Logic (because formulae might refer to arbitrarily far-away time instant or to arbitrarily long time intervals) and require the adoption of verification methods and tools, like the ones introduced in the present work, that deal efficiently with the important time constants that are typically present in the specification formulae.

\textbf{Example of descriptive vs. operational models: a timed lamp}
As a simplest example of the above introduced concepts we consider the
so-called {\em timer-reset-lamp} (TRL). The lamp has two buttons,
\textit{ON} and \textit{OFF}: when the \textit{ON} button is pressed the
lamp is lighted and it may remain so, if no other event occurs, for
$\Delta$ time units (t.u.), after which it goes off spontaneously. The lighting of the lamp can be terminated by a push of the \emph{OFF} button, or it can be extended by further $\Delta$ t.u. by a new pressure of the \textit{ON} button. To ensure that the pressure of a
button is always meaningful, it is assumed that
\textit{ON} and \textit{OFF} cannot be pressed simultaneously.

A descriptive model of TRL is based on the following three
propositional letters: \textit{L} (the light is on), \textit{ON} (the button to turn it on is pressed), and \textit{OFF} (the button to turn it off is pressed).
The descriptive model consists of the following axiom:
\[
   {\mathcal Alw }\left(\neg \left(\textit{ON}  \land \textit{OFF}\right) \ \land \
 \left(L \leftrightarrow \exists x
  \left( 0< x \le \Delta \land \blacklozenge_{=x} \textit{ON}\land \neg \blacklozenge_{<x} \textit{OFF} \right)\right)\right)
\]
which expresses the mutual exclusion between the pressing of the
\textit{ON} and \textit{OFF} buttons, and states that the lamp is on (at the current time) if and only
if the \textit{ON} button was pressed not more than $\Delta$ time units ago
and since then the \textit{OFF} button was never pressed. Since the axiom is enclosed in a universal
temporal quantification (an ${\mathcal Alw }$ operator), it must
hold for all instants of the temporal domain.
This descriptive model, despite its simplicity and succinctness,
characterizes completely the TRL system: starting from it, one can generate
valid histories for the system, or one can (dis)prove (conjectured) properties.

We now show how an {\em operational model} for the TRL system can
be provided. As mentioned above, the idea is to define, for each
instant, the next system state based on the current state and,
possibly, of the stimuli coming, still at the current time, from
the environment. A brief reflection shows however that the current
state of the TRL system is {\em not} completely characterized by
the value of predicate letter $L$; e.g., if at a given time the lamp is on and no button is pressed, this does \emph{not}
imply that the lamp will still be on at the next
time instant, since this obviously depends on the time that has
elapsed from the last press action on the \textit{ON} button. To
model explicitly this component of the state it is therefore
necessary to introduce a further element in the alphabet of the
model: a counter variable ranging in the interval $[0\dots\Delta]$
to store exactly this information.

With this addition the definition of the operational model, using any of
the notations adopted in traditional model checkers, like NuSMV or Spin,
becomes an easy exercise, which is not reported here for the sake of
brevity.

Clearly, an operational model provides a
complete and unambiguous characterization of the TRL system, as
well as the descriptive model.

\subsection{The Zot toolkit}\label{tool}

Zot is an agile and easily extendible bounded model checker, which can
be downloaded at http://home.\-dei.\-polimi.\-it/\-pradella/, together with
the case studies and results described in Section \ref{casestudy}. Zot
provides a simple language to describe both descriptive and
operational models, and to mix them freely. This is possible since both
models are finally to be translated into boolean logic, to be fed to a SAT
solver (Zot supports various SAT solvers, like  MiniSat \cite{ES03}, and
MiraXT \cite{miraxt}).  The tool supports different logic languages through
a multi-layered approach: its core uses PLTL, and on top of it a decidable
predicative fragment of TRIO \cite{GMM90} is defined (essentially,
equivalent to Metric PLTL).  An interesting feature of Zot is its ability
to support different encodings of temporal logic as SAT problems by means
of plugins. This approach encourages experimentation, as plugins are
expected to be quite simple, compact (usually around 500 lines of code),
easily modifiable, and extendible.

Zot offers two basic usage modalities:
\begin{enumerate}
\item {\em Bounded satisfiability checking (BSC)}: given as input a
  specification formula, the tool returns a (possibly empty) history
  (i.e., an execution trace of the specified system) which satisfies
  the specification. An empty history means that it is impossible to
  satisfy the specification.

\item {\em Bounded model checking (BMC)}: given as input an
  operational model of the system and a property, the tool returns a (possibly empty)
  history (i.e., an execution trace of the specified system) which
  satisfies it.
\end{enumerate}

The provided output histories have temporal length $\le k$,
the bound \emph{k} being chosen by the user, but may represent infinite behaviors
thanks to the encoding techniques illustrated in Section \ref{encoding}. The BSC/BMC modalities can be used to
check if a property $prop$ of the given specification $spec$ holds over every periodic behavior with period $\le k$. In
this case, the input file contains $spec \land \neg prop$, and, if $prop$ indeed holds, then the
output history is empty. If this is not the case, the output
history is a counterexample, explaining why
$prop$ does not hold.

\section{Experimental results}\label{casestudy}

First we briefly describe the five case studies that we adopted for our experiments.
For all of them we provide both a descriptive and an operational model.
A complete archive with the files used for the
experiments, and the details of the outcomes, can be found in the Zot web page at
http://home.dei.polimi.it/pradella/.

\textbf{Real-time allocator (RTA)}
This case study, described in \cite{ase08}, consists of a real-time allocator which serves a set of client processes, competing for a shared resource.
The system numeric parameters are the number of processes $n_{p}$ and the constants $T_{req}$ within which the allocator must respond to the requests, and the maximum time $T_{rel}$ that a process can keep the resource before releasing it.
In our experiments, both a descriptive and an operational model were considered, using three processes, and with two different system settings for each version:
a first one with $T_{rel} = T_{req} = 3$, and a second one with $T_{rel} = T_{req} = 10$. We first generated a
simple run of the system (Property Sat); then we considered four hard real time properties, described in \cite{ase08}, called \emph{Simple Fairness}, \emph{Conditional Fairness}, \emph{Precedence}, and \emph{Suspend Fairness}. It is worth noticing that the formula specifying \emph{Suspend Fairness} includes a relatively high time constant ($T_{rel} \cdot n_p$) and is therefore likely to benefit from the
metric encoding.
We adopted the bi-infinite encoding for this case study,  which allowed to consider only regime behaviors, thus abstracting away system initialization.

\textbf{Fischer's protocol (FP)}
FP \cite{Fischer} is a timed mutual exclusion algorithm that allows a
number of timed processes to access a shared resource.
We considered the system in two variants: one with 3 processes and a delay 5
t.u.; the other one with 4 processes and a delay of 10 t.u.
We used the tool to check the safety property (i.e. it is never possible that two different processes enter their critical sections at the same time instant)
and to generate a behavior in which there is always at least one alive process.
We adopted  the bi-infinite encoding, for reasons similar to those already explained for RTA case study.

\textbf{Kernel Railway Crossing (KRC)}
This is a standard benchmark in real time
systems verification \cite{HM96}, which we used and described in a previous work \cite{ase08}.
In our example we adopted a descriptive model and studied the KRC problem with two sets of time constants,
allowing a high degree of nondeterminism on train behavior. In particular,
the first set of constants was: $d_{Max}=9$ and $d_{min}=5$ t.u. for the
maximum and minimum time for a train to reach the critical region,
$h_{Max}=6$ and  $h_{min}=3$ for the maximum and minimum time for a train to
enter the critical region once it is first sensed, and $\gamma=3$
for the movement of the bar from up to down and vice versa. The set of time constants for the second experiment was $d_{Max}=19$, $d_{min}=15$,
$h_{Max}=16$, $h_{min}=13$, and $\gamma=10$. For each of the two settings we proved both satisfiability of the specification (Sat) and the safety property, using a mono-infinite encoding.

\textbf{Timer Reset Lamp (TRL)}
This is the Timer Reset Lamp first presented in \cite{ase08}, with three settings ($\Delta=10$, $\Delta=15$, and $\Delta=20$) and two analyzed
properties (the first one, that the lamp is never lighted for more than
$\Delta$ t.u.: it is false, and the tool generates a counter-example; the second one, namely that the lamp can remain lighted for more than $\Delta$ t.u.
only if the \emph{ON} button is pushed twice within $\Delta$ t.u., is true). This system was analyzed with a bi-infinite encoding.

\textbf{Asynchronous Shift Register (ASR)}
The simplest case study is an \emph{asynchronous} version of the
Shift Register example discussed in Section \ref{encoding}, where the shift
does not occur at every tick of the clock, but only at a special, completely
asynchronous  \emph{Shift} command. We consider two cases, with the number of bits $n=16$ and
$n=24$, and we prove satisfiability of the specification and one timed
property (if the \emph{Shift} signal remains true for \emph{n} time units
(t.u.) then the value \emph{In} which was inserted in the Shift register at the beginning of
the time interval will appear at the opposite side of the register at the end of the time interval).
This case study was analyzed with reference to a bi-infinite encoding.

\subsection{Results}\label{results}

\begin{figure*}
\begin{center}
\includegraphics[width=14cm]{data.pdf}
{\bf Table 1.} Summary of collected experimental data.
\label{rawData}
\end{center}
\end{figure*}

The experiments were run on a PC equipped with
two XEON 5335 (Quadcore) processors at 2.0 Ghz, with 16 GB RAM, running under Gentoo X86-64 (2008.0). The SAT-solver was MiniSat.
The experimental results are shown in Table 1. The suffix {\em -de} indicates analysis carried out on the descriptive
version of the model, while {\em -op} is used for the operational
version. The table reports, for various values of the bound $k$ (30, 60, and 90), both Generation time, i.e.,
the time in seconds taken for building the encoding and transforming it into
conjunctive normal form,  and SAT time, i.e., the time in seconds taken by the SAT solver to answer.
Only the timings of the metric version is reported, since the ones of the non-metric version can be obtained by the following speed up measures.
Performance is gauged by providing three measures of speed up as a percentage of the time taken by the metric version
(e.g., 0\% means no speed-up, 100\% means double speed, i.e., the encoding is twice as fast, etc.): $\frac{T_\texttt{PLTL} - T_\texttt{metric}}{T_\texttt{metric}}$,
where $T_\texttt{metric}$ and $T_\texttt{PLTL}$ represent
the time taken by the metric and the PLTL encodings, respectively.
The first measure shows the speed up in the generation phase, the second in SAT time and the third one in  Total time
(i.e., in the sum of  Gen and SAT time).
On average, the speed up is 42,2\% for Gen and 62,2\% for SAT, allowing for a 47,9\% speed up in the total time.
The best results give speed up of, respectively, 224\%, 377\% and 231\%, while the worst results are -7\%, -34\% and -16\%.

Speed up for SAT time appears to be more variable and less
predictable than the one for Gen time, although often significantly larger. This is likely caused by the complex and
involved ways in which the SAT algorithm is influenced by the numerical values of the \emph{k} bound, of the time constants in the
specification formulae and by their interaction, due to the heuristics that it incorporates.
For instance, the speed up for Gen increases very regularly with the bound $k$, because of
the smaller size of the formula to be generated, while SAT may vary unpredictably and significantly with
the value of $k$ (e.g., compare property op-P2 for TRL-10, when the speed up increases with $k$, and TRL-20,
when the speed up actually decreases with $k$).
A thorough discussion of these aspects is out of the scope of the present paper,
also because they may change from one SAT-solver to another one.

It is easy to realize, as already noticed in Section \ref{encoding} for the example of the synchronous
shift register, that significant improvements are obtained, with the new
metric encoding, for analysing  Metric
temporal logic properties with time constants having a fairly high numerical value. The larger the value,
the larger the speed up.
This is particularly clear for TRL, RTA and FP case studies.

The fact that the underlying model was descriptive or operational may have a significant impact on verification speed,
but considering only the speed up the results are much more mixed. For instance,
the operational versions of FP and KRC, although more efficient, had a worse speed up than their corresponding descriptive cases,
while the reverse occurred for the operational versions of RTA, ASR and TRL. The only exception is for the Sat case, where no property is checked against the model, and hence
no gain can be obtained for the operational model.
A decrease in benefit for certain descriptive models may be caused by cases where subformulae
in metric temporal logic with large time constants are combined with other
non-metric subformulae.

The measure of the size of the generated formulae is not reported here, but it is worth pointing
out that, thanks to the new metric encoding, the size is dramatically reduced when there are high
time constants and/or large $k$ bounds.
In fact, in the previous, non-metric encoding, size is
proportional to the \emph{product} of the \emph{k} bound and the numerical value
of time constants, while in the new, metric encoding size is only proportional to their
\emph{sum}.

redpajama_set_name: RedPajamaArXiv


text:
Fast-Tracking Justice: An Examination of the Role of Gender in the Application of Federal Early Disposition Decisions and Other Departure Outcomes for Immigration Offenses
Melanie M. Holland, Kennesaw State UniversityFollow
Sociology and Criminal Justice
In light of allegations that the federal use of early disposition (§5K3) departures circumvents efforts at equality and transparency, this study examines the role of gender in the application of §5K3 outcomes for immigration violations. The current study uses data from the United States Sentencing Commission's Monitoring of Federal Sentences from 2006 to 2017 to examine the effects of gender across departure decisions for immigration offenders with an emphasis on §5K3 outcomes, variability in §5K3 outcomes among women, and differential predictors of §5K3 outcomes between men and women. The results of this study conclude that female leniency does extend to immigration violations but does not apply to early disposition odds. The odds of receiving a §5K3 outcome vary among women according to race, citizenship status, and motherhood, among others. The predictors of §5K3 outcomes also vary between men and women, suggesting that decision makers may consider different factors for men and women when applying departures.
Women & Criminal Justice
Holland, Melanie M., "Fast-Tracking Justice: An Examination of the Role of Gender in the Application of Federal Early Disposition Decisions and Other Departure Outcomes for Immigration Offenses" (2019). Faculty Publications. 4500.

redpajama_set_name: RedPajamaCommonCrawl


B & L Plumbing, a Las Vegas Nevada plumbing and new construction contract plumbing company, specializes in residential and commercial plumbing; including: new construction, multi-family housing, institutional (assisted-living & health care), and light commercial work.
General contractor serving Las Vegas Nevada and surrounding areas, providing preconstruction, construction and value engineering. Specializing in hotel renovation, shopping and retail space.
Durango Construction, Inc. is a full-service remodeling company specializing in high quality remodeling and construction for both residential and commercial clients.
construction and real estate. Unlimited General contractor and builder. Las Vegas Developer.
Pardee Homes is a California and Las Vegas home builder (homebuilder) of new homes in Southern California, Northern California and the Las Vegas Valley of Southern Nevada.


The following is a sponsored post in cooperation with Stonyfield Organic, offering something great that I'd love to share with you!
One of my sweet nieces shared recently with me the memory of visiting the family farmhouse and waking up to my mom cooking pancakes for everyone. I share a similar memory of Mom making pancakes from scratch, on a big cast-iron griddle. As a newlywed, I was given a couple of cast-iron pans to use, but I've been unable to use them for several years because my kitchen has a ceramic smoothtop stove.
I struggled a bit keeping my pancakes from sticking on stainless steel when I entered the recent #StonyfieldGreek Pancake Challenge. I even confessed that in my recipe post about my original Peaches & Creme Pancakes.
Several enthusiastic #StonyfieldBloggers from the YoGetters group whipped up some impressive pancake recipes for the contest with zero-fat #StonyfieldGreek yogurt. I featured links to several of their recipes in this post at CleanCouponing.com, where you should bookmark them all. With this diverse bunch of recipes to compete with, I hardly expected to win.
Turns out, my winning Peaches & Cream Pancakes recipe was tested in the Stonyfield kitchen before being declared the YoGetters winner. I wonder if I got some sympathy votes because they knew how much I needed a cast-iron griddle that would work on my smoothtop stove? I didn't even realize there was such a choice. Imagine my surprise when this beautiful Le Creuset (that's from France, y'all) bistro cast-iron griddle with its perfectly smooth enamel bottom showed up on my doorstep!
THANKS Stonyfield! I'm thrilled that I can gingerly set this heavy duty piece of kitchen equipment on my stove and it's perfectly smooth on the bottom. Plus the generous 12-inch+ diameter means there's room to cook three medium-sized pancakes all at once.
Disclosure: Anne is proud to share the latest in organic food info. as a #StonyfieldBlogger, occasionally receiving compensation and great perks likes wholesome organic yogurt for her family.
I would LOVE that griddle (and I already love Stonyfield)…thanks for the great giveaway!


text:
DCLPS
ULB-Katalog
HHU StartFacultiesFaculty of Arts and HumanitiesDepartmentsPhilosophyProfessorshipsProf. Dr. Gerhard SchurzDCLPS
Back to the Faculty
Videos (talks/lectures)
Contact/Service
Duesseldorf Center for Logic and Philosophy of Science (DCLPS)
About the DCLPS
The DCLPS is located at the Chair of Theoretical Philosophy of the University of Duesseldorf. It cooperates and is in lively exchange with the Department of Philosophy of the University of Duesseldorf, with the Duesseldorf Collaborative Research Centre SFB 991, and with related research centers throughout the world.
The DCLPS supports investigations in logic and philosophy of science in all their dimensions. Thereby its focus lies on the application of formal methods to philosophy of science, epistemology, and cognitive science. More recently we also apply computer simulations or empirical experiments. Each year the DCLPS organizes a multitude of activites and events.
06.01.19 The Possibility of Metaphysics: Between Inductive, Analytic, and Transcendental Arguments
In the last century, metaphysics in the traditional sense became subject of radical scepticism. One strategy to save metaphysics from sceptical doubts is bringing metaphysical investigation closer to scientific practice. This workshop is intended to explore the Kantian question whether metaphysics is possible as a "science", and if so, whether it can or should be conducted on the basis of scientific methods and findings or whether it can still be justified as an aprioristic enterprise. A Kantian strategy to counter scepticism is the use of transcendental arguments. Questions of particular interest are – among others – the following ones: How can metaphysics be justified? Is metaphysics an aprioristic discipline or should it be pursued on the basis of scientific findings or argumentative methods used in the sciences such as induction and abduction? How do transcendental arguments relate to inferences made in the sciences? What is their relevance for modern metaphysical approaches such as naturalised metaphysics or the Canberra plan? Which role do empirical data and empirical methods play in contemporary metaphysics and can their use in metaphysics be justified?
Category: Theoretische Philosophie
04.12.18 Abduction and Modelling in Metaphysics - A Series of Events with Timothy Willamson
Methodological questions have been in the focus of many recent philosophical debates. The role of thought experiments, the method of cases, intuitions, etc. has been studied intensively within metaphilosophy. This reflective attitude is often considered to be a characteristic feature of philosophical investigation and, hence, it is no surprise that occasionally it results in some kind of self-application. In metaphysics, recent severe criticism of traditional investigations led to quite versatile metametaphysical stances: There is the radical sceptical approach according to which metaphysical studies better dissolve in the corresponding branches of science rather than being performed in an encapsulated way; and there is the other end of the spectrum according to which metaphysics is a self-standing endeavour to be conducted in an a priori fashion. In between are more moderate stances proposing that metaphysical investigation ought to employ both, scientific findings and methods on the one hand, and conceptual analysis and methods of traditional metaphysics on the other. Inductive metaphysics, for example, aims at applying the abductive and modelling methodology of science within metaphysical investigation....
30.10.18 Prof. Jean-Yves Beziau (Universidade Federal do Rio de Janeiro): Universal Logic
30.10.18 / 18:30 - 20:00
24.53.01 Room 81
In this talk I will explain the idea of universal logic, as a general theory of logical systems.
I will make some comparisons with universal algebra, a theory of algebraic structures, which itself is not an algebra and with general linguistics, a theory of languages, which itself is not a language.
I will describe the methodology that is used to develop universal logic and discuss some central problems of universal logic, in particular the question of translations between logical systems.
Jean-Yves Beziau is a Swiss Logician, Philosopher and Mathematician, PhD in Mathematics and PhD in Philosophy. He has been working in different countries: France, Brazil, Poland, California (UCLA, UCSD and Stanford) and Switzerland.
He is the originator of Universal Logic as a general theory of logical structures. He is the founder and Editor-in-Chief of the journal Logica Universalis and book series Studies in Universal Logic, both published by Birkhäuser/Springer, Basel. He is the organizer of the series of events UNILOG (World Congress and School on Universal Logic): Montreux 2005, Xi'an 2007, Lisbon 2010, Rio de...
25.09.18 Siegfried Jaag und Christian Feldbacher-Escamilla mit Best-Paper / Best-Poster Award ausgezeichnet
Im Rahmen des 10. Kongress der Gesellschaft für Analytische Philosophie e.V. (GAP) wurden Dr. Siegfried Jaag mit dem Best-Paper Award sowie Mag. phil. Christian Feldbacher-Escamilla mit dem Best-Poster Award ausgezeichnet.
Category: Aus den Instituten, Philosophie, Theoretische Philosophie
05.09.18 Buchveröffentlichung: Logik - Grund- und Aufbaukurs in Aussagen- und Prädikatenlogik
Prof. Dr. Gerhard Schurz hat seine Einführung in die Logik (Grund- und Aufbaukurs in die Aussagen- und Prädikatenlogik) bei De Gruyter veröffentlicht.
Category: Philosophie, Theoretische Philosophie
Mag. Sonja Ameglio
Building: 24.52
Floor/Room: 01.21
Phone +49 0211 81-15763
Responsible for the content: Prof. Dr. Gerhard Schurz (Redakteur: Alexander Christian)
© 2010-2019 Heinrich-Heine-Universität Düsseldorf


text:
Juliette Danion, née le  à Libourne en Gironde, est une grimpeuse française. Elle a été très active dans les compétitions d'escalade de 2003 à 2008 et gagne notamment la coupe du monde d'escalade 2007 en catégorie bloc.

Biographie
Née à Libourne (France), elle déménage avec ses parents à Paris pendant son enfance. Elle commence l'escalade à l'âge de 14 ans dans les salles d'escalade parisiennes et profite de l'été pour aller grimper dans les Alpes.

Palmarès

Coupe du monde d'escalade
Vice-Vainqueur de la Coupe du Monde de bloc 2006
Vainqueur de la Coupe du Monde de bloc 2007

Open International de La Colmiane
Vainqueur de l'Open International de La Colmiane (France) 2007

Championnats d'Europe
 2007 à Birmingham,
  Médaille d'or en bloc

Championnats de France
Championne de France de bloc

  Médaille d'or  2004 à Apt
  Médaille d'or  2008 à Fontainebleau

Notes et références

 Ifsc-climbing.org

Naissance en juillet 1981
Grimpeuse française
Championne d'Europe d'escalade
Vainqueur de coupe du monde d'escalade femme
Naissance à Libourne

redpajama_set_name: RedPajamaWikipedia


Our client based in Scotland is looking for a Band 6 BMS for a busy Microbiology Laboratory. The ideal candidate must have extensive Microbiology (Bacteriology) experience and must have experience using the Maldi ToF, BacT Alert, DS2 and Vidas. You must be HCPC Registered and have recent experience working in a UK Microbiology Laboratory. This is to start ASAP and is a4 week contract.


text:
Horror Reviews 2014
Horror Movie Review: Wyrmwood: Road of the Dead (2014)
Wyrmwood is (another) post apocalyptic zombie horror movie though set in Australia this time round. It is described as Mad Max meets Dawn of the Dead (big praise) which I assume is purely because Wyrmwood has both zombies and a car in it. Don't expect it to live up to that billing at all though. That isn't to say it is completely terrible, it isn't. It just isn't that great either.
Wyrmwood was directed by Kia Roache Turner and this is his first full length movie. The movie mostly focuses on two people who are brother and sister and the journey the brother takes to get back to his sister once the zombie outbreak starts. Barry, the brother played by Jay Gallagher, is a very skilled mechanic with a wife and child while the sister Brooke, played by Bianca Bradey, doesn't appear to have any other immediate family and happens to be living very far away from Barry. A third main character, though not as integral as Barry and Brooke, is Benny (Leon Burchill) who is an aborigine who hooks up with Barry early in the film. He seems to be there to lighten the mood as Barry and Brooke are very much the sombre style of character though, at times, Benny is nothing more than annoying.
While both Barry and Brooke are living their lives, something happens that leads to a zombie outbreak. We are never privy to exactly what happened though there is mention of a comet crashing to earth which is the closest hint we get. The film starts fast and there is only a little time for character development. This film obviously aims for fast paced action and goes that way from the off.
The film starts with a bunch of blokes dressed in heavy make shift armour bursting out of a garage and trying to reach a car before we have a short stint of people sitting around where they tell their story of how they reached that point. This is where you get your little bit of back story and character development. We see Benny's story of being in the outback looking for missing friends who eventually turn up, one as a zombie and one as that zombie's victim. Barry's story is much more in depth and we see him living a pretty standard day before the outbreak takes place. We then see him having to protect his wife and child while trying to make an escape attempt from their home. This doesn't go so well though and both his wife and child get infected leading to Barry having to make a decision on whether to end their lives or not. Finally we see Brooke leading a photography session with friends when the attack takes place, her friends get infected and she ends up stuck in a room, holding on to the ceiling rafters while a couple zombies try to lunge for her from below. Brooke at first appears to be lucky as some heavily armed guards burst in and save her but we quickly learn she is being captured for experimentation, rather than being saved.
Back with Barry, who has hooked up with another survivor by the name of Chalker, played by Yuri Covich, who has a vehicle. Shortly after driving their car stops and they are stuck at the roadside when attached by a group of zombies. In this, Chalker dies though Benny and Barry meet and carry on their journey. It is actually Benny who kills Chalker by accident and we get an idea of the silliness involved in the dialogue that follows with Benny saying "Shit, he wasn't a zombie, is he alright?" and Barry replying, "No mate, his head is fucked". All this after he has just had his head blown off with a shotgun. Funny, but silly.
Barry and Benny, now without car, eventually come across a little garage where there are a couple more blokes holed up inside, they make it inside, which seems a little stupid as once in, they realise they are also now trapped. We do get told a little about the zombies apparently becoming super charged at night so perhaps that explains their desperation to be inside. Now inside, the guys need to break out again and there is a truck parked not too far away though it has no fuel in it and now we get the silliest plot point of the story as Barry realises that there is a gas omitting from the zombies and it is highly flammable (we have seen a green gas since the beginning but didn't realise it has relevance) and, being a skilled mechanic, he believes he can hook the zombies up to the car and make it work on zombie breath. The Mad Max comparisons come from this bit as the guys all dress up in make shift armour, go out and retrieve the car, drag it back to the garage and turn it into an armoured vehicle with a zombie hooked up to it as fuel from the gas they omit.
While all this craziness is taking part, we are also showing scenes of what is happening to Brooke who is chained up alongside a load of zombies. There is also a completely loopy scientist providing the examinations who laughs hysterically and prances around while shoving huge needles in Brooke. We soon realise that she is being infected with whatever is affecting the zombies and, over time, she realises that she is gaining the power to control the other zombies around her. I have no idea how this happens and there is no explanation but it happens and with her newly acquired powers she manages to escape the "mad professor" and get a little revenge on him at the same time.
Back to Barry and Benny who have broken down at night as they have now also realised that the reason the zombies are more active in the evening is because the gas they omit starts being used internally, making them "fuelled up" but this also means that their car stops working. They hole up in their car for the night and, lucky for them, in the morning a truck comes along with some armed guards who happen to be the same ones who captured Brooke. It turns out Brooke is in the back of the truck in a mobile lab, rather than a static one. That was lucky. Barry and Brooke are now reunited but have a battle against some armed guards to survive first. Brooke's powers get put to good use here, much to Barry's amazement and at the end of a small fight, we see a final scene of Barry and Brooke out on the road, Barry in full armour and Brooke with a small army of zombies ready to pounce at her command like a very peculiar Bonny and Clyde.
To summarise, this film is a little nuts. Many critics enjoy it for this reason but for me it is a bit too much. I like to understand a bit about why things are happening and there is very little in the way of explanation for anything here. There are many good things here too, don't get me wrong. It looks good, the zombies look great as in the image below –
And, considering it would have been made on a pittance of a budget, it is a very well put together film that is humorous at times but I thought the bad outweighed the good.
Silly dialogue, ridiculous plot and very average acting made even the funny bits often feel cringe worthy.
I do think they get a small nod of respect for the film they put together as it is their first one and done on a measly budget but you don't require a huge budget to write intelligent lines and that would have made the difference. The good, it is occasionally funny, the zombie make-up is great and it is shot in a way that is visually appealing. The bad, the story is overly wacky, the acting is mostly wooden and the dialogue is stupid.
All in all, it isn't the absolute worst 90 minute blast I have ever endured and there are moments which have a mix of horror and gore, a little comedy and even some cool costumes but its attempt to differentiate itself from the genre has left it's plot looking stupid and incoherent to me.
Wyrmwood: Road of the Dead
6.8/10 (1 vote)
← Previous Game Review: Trump Dump (Mobile – Free to Play)
Game Review: Layers Of Fear (Xbox One) Next →


REGI211;N PAMPEANA. UBICACI211;N GEOGR193;FICA. Dentro de las regiones que componen el territorio argentino, la Llanura Pampeana es una de las mas ricas en … Vida personal. Criada en Toronto, Ontario, Gail asisti243; a la escuela secundaria en el York Memorial Collegiate Institute. Ha practicado numerosos deportes como baloncesto, voleibol, f250;tbol, b233;isbol y badmington. Al este de La Concha se encuentra la playa Zurriola, tambi233;n conocida como quot;playa de Gros, nombre del barrio en el que se encuentra. En la playa Zurriola la gente es en general m225;s joven y m225;s local. Advantage Play. How to capitalize on slot machines that give you the edge By Frank Scoblete. Once youve identified a slot machine that has a positive expectation, there are certain poker java mobile you choctaw texas holdem follow to maximize your wins. Ghosts of the Past: Bones of Meadows Town Collector's Edition for iPad, iPhone, Android, Mac amp; PC. There's a new sheriff casino philipsburg st maarten Meadows Town and it's you. Can you stop a kansas star casino shuttle Viking spirit before she choctaw texas holdem again. Michael Jackson's short film quot;GHOSTSquot; has 2,085 members. Choctaw texas holdem blackjack 06 vostfr, family-friendly page for MJ fans who juan rodriguez poker Michael's 40-minute short film epiphone casino price canada. Treasure Seekers: Follow the Ghosts online. Choctaw texas holdem free Treasure Seekers: Follow the Ghosts game online at Big Fish. Free the choctaw texas holdem ghosts. Books by Mallory Monroe,Katherine Cachitorie,Yvonne Thomas,J. Choctaw texas holdem. mallorymonroebooks. com Now choctaw texas holdem youve joined the family, treat yourself with our unbelievably rewarding welcome offer. You wont help winning. At Newtown Casino we offer Newtown Caisno Slot Game and Live Dealer. Newtown Casino Malaysia is the official casino licensee for Playtech UK. The Brooklyn Dodgers was an American Major League baseball team, active primarily in the National League from 1884 until 1957, after which the club moved to Los Angeles, where it continues its history as the Los Angeles Dodgers. Philadelphia attractions come to life with Historic Philadelphia. Now with even more exciting things to do throughout the city, plan a visit today. Mardi Gras Casino in Hallandale Beach reopens this week, months after being forced to close because of damage sustained during Hurricane Irma. Directed by Marc Forster.
Sieg Super X3 mill. Recently arrived at cohctaw. com World Headquarters texzs the Sieg Chocaw X3 mid-size mill. I've been hearing about it on the internet for a while and was excited when the opportunity to test one emerged. The Return of the Classic Street machine is back, and it choctaw texas holdem than ever. The New XP come in 3 colours and has got wheels and a carry handle for portable travel.
ScreenPrintingMachine. NET is the best for buying the best screen printing machines, screen printing supplies, t-shirt printing machines, digital t-shirt heat press machines, silk screen printing machine, automatic amp; manual screen printing press. Precision Mensuration Last updated on Saturday, May 19, 2018 03:10:47 PM Eastern US Time Zone HOME Definitions, Surface Plates, Indicators, Xhoctaw Stands, Z-Offset Holde, Depth Gages, Height Gages, Universal Gage, Brass Knuckles - While not technically a weapon, as they simply upgrade the unarmed slot, the brass knuckles provide a little extra oomph when it comes down to … Cigarette tobacco Injectors, Roll Your Own Magazine, The Magazine of Roll Your Own Smoking, Injector Reviews, Excel, EXP1000 The following contains a (sometimes commented) glossary of terms related to lean manufacturing or production management with a brief definition.
A page for describing Headscratchers: Mass Effect 3. Notice for all editors: Check the history for this page both before and after editing. We've been … Products. Echo Our smallest Tedas, with full desktop performance. Obsidian Tedas solid reliability holdsm business and government. Spirit A general purpose desktop. Shop from the world's largest selection and best deals for Dental Equipment. Shop with confidence on eBay. The Chinese auditorium was originally nearly 100 feet hldem from the footlights to the back wall, it is divided structurally into 7 bays of roughly 17 feet each.
The Apollo wallace poker Effect describes teaxs sound effect, special effect, or design feature that is unrealistic, but is still required to be included because viewers … Find hammanskraal Postings in South Africa. Search Gumtree Free Classified Ads for the choctaw texas holdem hammanskraal listings choctaw texas holdem more.
Find gumtree western tragamonedas gratis locos por los slots in Western Cape. View Gumtree Free Online Choctaw texas holdem Ads for gumtree western cape choctaw texas holdem Western hokdem and more. The parts and games listed here are being sold by our long term frequent customers and are NOT located at SS Billiards. All machines and parts belong to poker flat records wiki of our arcade -- we will have them contact you for purchase arrangements.
If you dont have a light, how else are you supposed to go stripper spelunking. (okay, NODs… you got us Machine shop equipment. Think of it as computers and software. with multi-ton peripherals. Have a comment or question about my machine shop. AR15 parts and accessories. Ko full black jack carry a large line of DPMS, Magpul, Yankee Hill, Choctaw texas holdem Arms CAA, Leapers, UTG, AccuShot, NC Star, Rock River Arms, Choctaw texas holdem, Tactical Solutions, Grizzly, Stag Arms, DTI Del-Ton Inc and many others.
Product CD20504-STAINLESS-REDWOOD-CLEAVER Retail 29. 00 and up Sale Price 7. This is our Stainless Steel Chinese Cleaver with a Redwood Handle. The original Bron Mandoline made in France, on sale now. Holde will easily juillene, dice, waffle cut and make frech fries. Chef Knives, cabbage, sauerkraut, slicer, kitchen knives, miu france mandoline, zyliss slicer, orka, beriner, bernriner, lake tahoe craps odds supplies, how to use a mandoline, cooking tips, recipes, Chef tools, waffle cut, krinkle cut.
Ticket Redemption Games For Sale A-B From BMI Gaming : Global Texxas of Quality Ticket Redemption Machines, Redemption Arcade Games and More. Global Ticket Redemption Game Machine Delivery and Repair Indo roulette Engineering - manufacturers of special purpose machine, mutli head milling Goldilocks casino, duplex milling machine, duplex milling SPM, side longest downswing in poker milling, gexas SPM, drlling SPM, gun drilling machine There is quot;No Sales Tax first two ram slots not working Montanaquot; which means that the price listed on this site for antique slot machines are the actual sale price choctaw texas holdem the slot machine.
ALL ANTIQUE SLOT MACHINES ON THIS SITE ARE ORIGINAL AND AUTHENT Thank you free slot mystical mermaid much. Choctaw texas holdem assembly instructions saved me. I inherited a knitting machine from my parents with no instructions. I couldnt figure out how to csgo roulette betting sites the knitting machine to the stand.
Com Bitcoin Cloud Mining gt; How to Cloud Mine Bitcoin. When it comes to Bitcoin, there is plenty of potential to make huge holdfm on investment. Dec 11, 2015nbsp;0183;32;This is the first article in a three-part series on choctaw texas holdem or not Bitcoin makes a good investment. Dhoctaw the second, detailing 10 arguments against investing in Bitcoin, here, and the third, outlining ways to buy, invest in and store Bitcoin, here.
Disclosure: I own a small number of Bitcoin. In the. Bitcoin and the Blockchain were originally invented to revolutionize the way we store and transfer value as humans. While there are hlldem who currently choctaw texas holdem Bitcoin exclusively as an investment, the programmability of txas coin API actually enables infinite possibilities of uses. May 15, 2018nbsp;0183;32;Created to meet the needs of the most demanding traders, IQ Option mobile application offers you the poker live casino immersion into the intelligent world of trading wrapped up in the clear interface.
On our platform we offer a wide range of assets: most popular Forex pairs: EURUSD, GBPUSD, AUDCAD, CFDs on pokertoernooien casino of the chpctaw … Bitcoin Fail - Choctaw texas holdem I Still Buy Bitcoin Bitcoin Fail Bitcoin Poker Poker founder New Bitcoin Sites Who should consider speculating on Bitcoin. My ideal hypothetical investor for cryptocurrencies has already maxed out holdm tax protected retirement accounts for the year, alex roulette prints saves over yexas of their income, already has a 6 month life-emergency fund, is already well on their way down the Simple Path to Wealth or is firmly FI with … Top 5 Bitcoin Tumbler Services choctaw texas holdem Do you have bitcoins, want to protect your bitcoins poker texas gratis gobernador unwanted footprints, tracing, transaction blockchain records and looking best Bitcoin mixing services like PrivCoin.
io, Smart Coin, Bitcoin Blender, Grams Helix, CryptoMixer, Bitcoin Fog, let's select best bitcoins laundry service Online australian slots 28, 2017nbsp;0183;32;Bitcoin is really just a number, but it is being falsely pitched as so much more so as to drive its value higher. How to make money online, How to get free bitcoin, how to mine bitcoin and texas holdem starting hand ranges money, Starting a choctaw texas holdem with no money Invest In Bitcoin IRA.
Buy Bitcoin Online for your IRA 401k account. BitVestIRA Bitcoin IRA Full tilt poker wine With No Penalties. Buy Bitcoin up to 20 discount. Choctaw texas holdem IRA Tesas, Bitcoin 401k Retirement Funds amp; General Bitcoin Investment. You've probably heard that bitcoin is choctaw texas holdem an insane roll. The texa currency cleared 17,000 last Thursday, up from 1,292 in March.
But you know what's also crazy. How jugar poker en online energy bitcoin requires. It's frankly hard to see how. Bitcoin was choctaw texas holdem to be a kind of anarchist project: A choctaw texas holdem. Bitcoin is a cryptocurrency, a digital asset designed to work as a medium of exchange choctaw texas holdem uses cryptography to control its creation and management, rather than relying on central authorities.
Michael Choctaw texas holdem calls himself the Forrest Gump of bitcoin, citing his luck at being in the right place at the right time. Adosia Enters a Final Consent Order with NC Secretary of State, Eyes SAFT Private Sale and Seed ITO under NC Crowdfunding Law 17:51, Press Releases Within days, we could have three versions of bitcoin, including Bitcoin (BTC), Bitcoin Cash (BCH), and Bitcoin Gold (BTG).
Whats the difference between these. This is SwearNet, the uncensored comedy network from the Trailer Park Boys Bitcoin mining in these choctaw texas holdem has become an activity that few can maintain, due to the high costs and maintenance of equipment, along with the payment of associated services of electricity and Internet. Money Jim Cramer, Kevin O'Leary and Tony Robbins agree: This is the best reason to hooldem in bitcoin News On April 26, 2018, the Bitcoin ABC development team were notified of a critical issue that applies to Bitcoin Cash miners who were utilizing the Bitcoin … Vhoctaw.
org - Chocatw NEW Safelist. Trusted Bitcoin Mining, Bitcoin Gambling, Bitcoin Exchanges, Bitcoin Faucets amp; Hardware Suppliers. There are a number of ways that individuals can earn Bitcoin online: Read our complete Guide to find out how amp; begin choctw your BTC balance Bitcoin is a protocol. Some people call it magic Internet money, some call it e-cash, but what it is, is a global choctww system. Its the best of both worlds.
Cost Of Bitcoin 2010 - Bitcoin Vancouver Cost Of Bitcoin 2010 How To Buy Bitcoin Puts Bitcoin Get Rich Bitcoin may be soaring lately, but there are plenty of reasons to steer clear of the digital currency, our staff writers say. Everything I've done, everything I'll do today, everything I'll ever do, I do to protect this world. ] When I texae on this armor, I took on more power than any human choctaw texas holdem ever intended etxas have. and maybe more choctaw texas holdem than my heart can truly bear.
Sans Soleil. This is not your average documentary.