scamr.tex

In this section, we describe a {\em relational modeling} approach to
abstract a system. The technique described in this section can be
viewed as an enrichment of the procedure to construct an
$\epsilon$-precision transition system from the previous section.  The
central idea of this paper is that a discrete abstraction based on a
transition system can be augmented with additional information which
can greatly improve the accuracy of the abstraction. The refined
discrete abstraction takes the form of a $\epsilon$-precision {\em
relational} transition system $\RTSAbstraction{\epsilon}{\System}$. We
use the abbreviation $\epsilon$-RTS for $\epsilon$-precision
relational transition system.

\subsection{$\epsilon$-RTS}
Let $\exprs{\vx}$ denote a set of Boolean-valued expressions over the
variable $\vx$ and their Boolean combinations.  For example, if $\vx =
\setof{x_1,x_2}$, then $\exprs{\vx}$ could be $\setof{ x_1 > 0, x^2_1
+ x_2 > 0, x_2 < 1 \wedge x_1 + x_2 > -1}$.  An $\epsilon$-RTS
$\RTSAbstraction{\epsilon}{\System}$ is a labeled transition system
described by the tuple:
$(\Cells,\vx,\CellEdges,\InitCells,\CellLabelingFunction,
\EdgeLabelingFunction,\UnsafeStates)$, where:

\begin{itemize}[label=--,leftmargin=1em,labelsep=*]
\item
$\Cells$ is a set of cells,
\item
$\vx$ represents a variable that takes values in $\ContStates$,
\item
$\CellEdges$ is a finite subset of $\Cells \times \Cells$,
\item
$\InitCells$ is a set of initial cells,
\item
$\CellLabelingFunction$ is a function mapping a cell $C$ to a
an expression $e(\vx) \in \exprs{\vx}$,
\item
$\EdgeLabelingFunction$ maps an edge $(C,C')$ to a pair $(g(\vx),
r(\vx,\vxp))$, where the {\em guard relation} $g(\vx) \in \exprs{\vx}$
and the {\em reset relation} $r(\vx,\vxp) \in \exprs{\vx,\vxp}$, and
$\vxp$ is a special variable.
\item
$\UnsafeStates \subset \ContStates$ is a set of unsafe states.
\end{itemize}


The operation of $\RTSAbstraction{\epsilon}{\System}$ is described in
terms of its configuration and its moves. A configuration is a pair
$(C, \nu)$, where $C \in \Cells$, and $\nu$ is a valuation function
assigning values in $\ContStates$ to the variable $\vx$.  The
transition system starts in some cell $C \in \InitCells$.  The move
function $\mu$ maps a configuration $(C,\nu)$ to the next
configuration $(C',\nu')$, iff there is a transition $(C,C') \in
\CellEdges$ such that:
\begin{enumerate}
\item
There exists $\contState \in \ContStates$ such that
$\quant_\epsilon(\contState) = C$ and exists $\contState' \in
\ContStates$ such that $\quant_\epsilon(\contState') = C'$,
and $\contState' = \simmap_\Delta(\contState, t, u)$,
\item
If $\CellLabelingFunction(C) =  e(\vx)$, and if
$\CellLabelingFunction(C') = e'(\vx)$, then for $\nu(\vx) =
\contState$ and $\nu(\vx') = \contState'$, the expressions
$e(\nu(\vx))$ and $e'(\nu'(\vx))$ evaluate to true,
\item
If $\EdgeLabelingFunction((C,C'))$ = $(g(\vx), r(\vx,\vxp))$,
for $\nu(\vx) = \contState$ and $\nu'(\vxp) = \contState'$,
$g(\nu(\vx))$ and $r(\nu(\vx), \nu'(\vx))$ evaluate to true.
\end{enumerate}

\begin{example}
Consider a system with the following two reachability relations
discovered using simulations. The values of the inputs are irrelevant
to this example, so we just assume it is some fixed constant $u$.
Also, let $\Delta = 0.1$.
\begin{eqnarray}
\label{eq:transitions}
(0.05, 0.1) & = & \simmap_\Delta((0.1, 0.1), 0, u), \\
(1.35,1.15) & = & \simmap_\Delta((0.9, 0.8), 0.1, u).
\end{eqnarray}

Consider the following $\RTSAbstraction{\epsilon}{\System}$ where,
$\Cells = \setof{C_1,C_2}$, $\vx = (x_1,x_2)$, $\InitCells = \setof{C_1}$,
$\CellEdges = \setof{(C_1,C_1), (C_1, C_2)}$, and,
\[
\begin{array}{l}
\CellLabelingFunction(C_1) = (0 \le x_1 < 1) \wedge (0 \le x_2 < 1), \\
\CellLabelingFunction(C_2) = (1 \le x_1 < 2) \wedge (1 \le x_2 < 2), \\
\EdgeLabelingFunction((C_1,C_1)) = (g_1,r_1), \text{ where, } \\
\qquad g_1 = (0 \le x_1 < 0.5) \wedge (0 \le x_2 < 1), \\
\qquad r_1 = (0 < x^+_1 - 0.5x_1 < 0.1) \wedge (0 < x^+_2 - x_2 < 0.001), \\
\EdgeLabelingFunction((C_1,C_2)) = (g_2,r_2), \text{ where, } \\
\qquad g_2 = (0.5 \le x_1 < 1) \wedge (0 \le x_2 < 1), \\
\qquad r_2 = (0.4 < x^+_1 - x_1 < 0.5) \wedge (0.3 < x^+_2 - x_2 < 0.4). \\
\end{array}
\]

Observe that the $\epsilon$-RTS is a valid abstraction of the given
trajectory fragments in Eq.~\ref{eq:transitions}.
\end{example}