Theory Robot
theory Robot
imports
ClockView
SPRViewSingle
"HOL-Library.Saturated"
begin
subsection‹The Robot›
text‹
\label{sec:kbps-theory-robot}
\begin{figure}[tb]
\includegraphics[width=\textwidth]{robot_clock}
\caption{The implementation of the robot using the clock semantics.}
\label{fig:kbps-theory-robot-clock}
\end{figure}
\begin{figure}[tb]
\includegraphics[width=\textwidth]{robot_spr}
\caption{The implementation of the robot using the SPR semantics.}
\label{fig:kbps-theory-robot-spr}
\end{figure}
Recall the autonomous robot of \S\ref{sec:kbps-robot-intro}: we are
looking for an implementation of the KBP:
\begin{center}
\begin{tabular}{lll}
$\mathbf{do}$\\
& $\gcalt$ $\mathbf{K}_{\mbox{robot}}$ \textsf{goal} & $\rightarrow$ \textsf{Halt}\\
& $\gcalt$ $\lnot\mathbf{K}_{\mbox{robot}}$ \textsf{goal} & $\rightarrow$ \textsf{Nothing}\\
$\mathbf{od}$\\
\end{tabular}
\end{center}
in an environment where positions are identified with the natural
numbers, the robot's sensor is within one of the position, and the
proposition \textsf{goal} is true when the position is in
$\{2,3,4\}$. The robot is initially at position zero, and the effect
of its \textsf{Halt} action is to cause the robot to instantaneously
stop at its current position. A later \textsf{Nothing}
action may allow the environment to move the robot further to the
right.
To obtain a finite environment, we truncate the number line at 5,
which is intuitively sound for determinining the robot's behaviour due
to the synchronous view, and the fact that if it reaches this
rightmost position then it can never satisfy its objective. Running
the Haskell code generated by Isabelle yields the automata shown in
Figure~\ref{fig:kbps-theory-robot-clock} and
Figure~\ref{fig:kbps-theory-robot-spr} for the clock and synchronous
perfect recall semantics respectively. These have been minimised using
Hopcroft's algorithm \<^citep>‹"DBLP:journals/acta/Gries73"›.
The (inessential) labels on the states are an upper bound on the set
of positions that the robot considers possible when it is in that
state. Transitions are annotated with the observations yielded by the
sensor. Double-circled states are those in which the robot performs
the \textsf{Halt} action, the others \textsf{Nothing}. We observe that
the synchronous perfect-recall view yields a ``ratchet'' protocol,
i.e. if the robot learns that it is in the goal region then it halts
for all time, and that it never overshoots the goal region. Conversely
the clock semantics allows the robot to infinitely alternate its
actions depending on the sensor reading. This is effectively the
behaviour of the intuitive implementation that halts iff the sensor
reads three or more.
We can also see that minimisation does not yield the smallest automata
we could hope for; in particular there are a lot of redundant states
where the prescribed behaviour is the same but the robot's state of
knowledge different. This is because our implementations do not
specify what happens on invalid observations, which we have modelled
as errors instead of don't-cares, and these extraneous distinctions
are preserved by bisimulation reduction. We discuss this further in
\S\ref{sec:kbps-alg-auto-min}.
›
type_synonym digit = "5 sat"
datatype Agent = Robot
datatype EnvAct = Stay | MoveRight