report.tex

\documentclass[a4paper]{article}
\usepackage[a4paper,margin=3.5cm]{geometry}

\usepackage{fontspec}
\setmonofont[Scale=MatchLowercase]{DeJaVu Sans Mono}

\title{
  Four Valued Timed Propositional Temporal Logic for Runtime Verification\\
  \normalsize{} COMP4560 Report
}
\author{
  Alexander Cox
  \thanks{Studying a Bachelor of Science at The Australian National University (ANU)}\\
  \small\texttt{u6060697@anu.edu.au}\\
  \normalsize{}Supervised by Peter Baumgartner\thanks{Data61, CSIRO\@; ANU}
}

\usepackage{parskip}

\usepackage[backend=biber, style=alphabetic]{biblatex}
\addbibresource{report.bib}

\usepackage{mathtools}
\usepackage{amssymb}
\usepackage{amsthm}
% \numberwithin{equation}{subsection}
\usepackage{thmtools, thm-restate}
\usepackage{nameref, hyperref, cleveref}
% \usepackage[nothm]{thmbox}
\declaretheorem[numberwithin=subsection,name=Theorem]{thm}
\declaretheorem[sibling=thm,name=Lemma]{lem}
\declaretheorem[sibling=thm,name=Corollary]{corl}
\declaretheorem[sibling=thm,style=definition,name=Definition]{defn}
\declaretheorem[sibling=thm,style=definition,name={Decision Procedure}]{desc}
\declaretheorem[sibling=thm,style=remark,name=Notation]{notn}
\declaretheorem[sibling=thm,style=remark,name=Remark]{remk}
\declaretheorem[sibling=thm,style=remark,name=Example]{eg}
\usepackage{mdframed}
\mdfsetup{linewidth=1pt,rightline=false,bottomline=false,skipabove=\topskip,nobreak=true}
\surroundwithmdframed{thm}
\surroundwithmdframed{lem}
\surroundwithmdframed{corl}
\surroundwithmdframed{defn}
\surroundwithmdframed{desc}
% \surroundwithmdframed{eg}
\surroundwithmdframed{remk}
\surroundwithmdframed{notn}

\setcounter{secnumdepth}{2}
% \usepackage{alltt}
\usepackage{listings}
\usepackage{alltt}
\usepackage{hyperref}

\newcommand{\U}{\mathsf{U}}
\newcommand{\tand}{\text{ and }}
\newcommand{\tor}{\text{ or }}
\newcommand{\tiff}{\text{ iff }}
\newcommand{\fsome}{\text{ for some }}
\newcommand{\fall}{\text{ for all }}
\newcommand{\sn}{\bigcirc^+}
\newcommand{\wn}{\bigcirc^-}
\newcommand{\eval}{\mathcal{E}}
\newcommand{\ltlt}{LTL$_3$}
\newcommand{\rw}[1]{\Rightarrow_{#1}}
\begin{document}
\lstset{language=Scala,basicstyle=\ttfamily\small,showstringspaces=false,frame=tl,framerule=1pt,captionpos=b}
\maketitle

\begin{abstract}
  Runtime Verification aims to check whether a real-world execution trace of a system conforms to a correctness property. Since only a finite prefix of the trace is available to check at any time, the result could change if the system continues to run. This gives uncertainty to the result of the verification and a choice must be made to pick a logic which adequately models the results of the verification.

  In this report I survey logics in the literature intended for runtime verification and define a new logic combining desirable capabilities of existing logics.
  The new logic is a four-valued semantics (\emph{true, false, presumably true, presumably false}) for TPTL which models the uncertainty exhibited by runtime verification. I call this new logic RV-TPTL. This logic builds upon an existing four-valued logic for LTL called RV-LTL.

  I outline a verification procedure for RV-TPTL and implement an incomplete version of this procedure. This implementation gives promising results, indicating the potential usefulness of RV-TPTL for runtime verification.
  % What are you trying to do? Articulate your objectives using absolutely no jargon.
  % How is it done today, and what are the limits of current practice?
  % What's new in your approach and why do you think it will be successful?
  % Who cares? If you're successful, what difference will it make?
  % What are the risks and the payoffs?
  % How much will it cost?
  % How long will it take?
  % What are the midterm and final "exams" to check for success?
\end{abstract}
\newpage
\tableofcontents
\newpage

\section{Introduction}
\subsection{Runtime Verification}
Runtime verification~\autocite{colin2005rv} is a method of monitoring a system and checking whether it satisfies (or violates) a correctness property.
The properties of runtime verification are temporal properties specified in some formal language, often a temporal logic.

Runtime verification can be used in conjunction with other verification techniques, but it is also useful in and of itself. Some systems may be too complex to model, or may be otherwise difficult to test adequately. The inspiration for this runtime verification project was situational awareness systems, specifically the Fusemate system at Data61~\autocite{Baumgartner:Haslum:situational-awareness-industrial-operations:ASOR:2018}. The goal was to be able to verify properties of a supply chain system, for example, `Does the shipment of apples arrive at it's destination within 5 hours of being shipped?'

Runtime verification is closely related to model checking~\autocite{baier2008principles}. Model checking is concerned with verifying all possible runs of a system, utilizing a model of that system. In runtime verification, we are concerned only with real-world runs of a system, with the system not modeled, but monitored. In order to monitor the system some instrumentation may occur, so that the monitor can easily detect states of the system. In model checking each run of the system is infinite, whereas, in runtime verification, the runs to be verified are always a finite prefix of an infinite run.

In this project, the specification languages I have used are temporal logics, which I will now attempt to explain. I assume the reader is reasonably comfortable with logic, for an introduction to logic please see \textcite{bradley2007calculus}.

\section{Temporal Logic}

A temporal logic is a modal logic which can be used to reason about time. Some temporal logics are only capable of modelling order e.g., `this will happen in the future', and some are capable of order and explicit time e.g., `twenty minutes in the future this will happen'. All of the logics I will discuss are based on Linear Temporal Logic, which models temporal order. I had the need for explicit time, so I then discuss Timed Propositional Temporal logic, which extends Linear Temporal Logic with explicit time. Both of these logics are defined on infinite traces. Because of the need to reason about finite (prefixes of) traces in runtime verification, alternate variants of the model checking logics are necessary. I discuss some of these finite-trace variants that I think are the most interesting and then I construct a new logic based on those discussed.

\subsection{Linear Temporal Logic}
Linear Temporal Logic (LTL)\autocite{pnueli1977temporal} is a temporal logic created for model checking. LTL models the order of events but not the explicit time of events. For an in depth introduction to LTL see \textcite[Chapter 5]{baier2008principles}. The syntax and semantics of LTL follow. I use Bachus-Naur form to define the syntax grammar throughout this report. Assume that we have an infinite supply of propositional variables $a,b,c,\dots$
\begin{defn}[LTL Syntax]\label{ltlsyn}

  An LTL formula $\varphi$ is inductively defined as follows:
  \[\varphi ::= a ~|~ \bot ~|~ \neg \varphi ~|~\varphi \lor \varphi ~|~ \varphi \land \varphi ~|~ \bigcirc \varphi ~|~ \varphi \U\varphi\]
\end{defn}

Some formulae can be stated in terms of the above syntax, so I abbreviate them as is common in the literature.

\begin{notn}[LTL Abbreviations]\label{ltlabbrev}
  The following standard abbreviations are made:
  \begin{align*}
    \top &:= \neg \bot\\
    \varphi \to \psi &:= \neg \varphi \lor \psi\\
    \varphi \leftrightarrow \psi &:= (\varphi \to \psi) \land (\psi \to \varphi)\\
    \Diamond \varphi &:= \top \U{} \varphi\\
    \Box \varphi &:= \neg\Diamond\neg\varphi
  \end{align*}
  Note that I do not abbreviate $\land$ because it is needed in the explicit syntax so that formulae can be represented in negation normal form and disjunctive normal form, which is required for formula rewriting.
\end{notn}

We read $\top$ as `true', $\bot$ as `false', $\bigcirc$ as `next', $\Diamond$ as `eventually', $\Box$ as `always', and $\U$ as `until'.

The formulae of LTL are interpreted over sequences of states called traces.

\begin{defn}[Traces and states]
  Let $P$ be a set of propositional variables. A \emph{state} $\sigma_i \subseteq P$ is a set of propositional variables that are interpreted as true. A \emph{trace} $\sigma \in P^+$ is an infinite sequence of states.
\end{defn}

\begin{notn}[Satisfaction Relations]
  Let $\vDash_{\text{S}}$ signify semantic entailment in the logical system S (e.g., S = LTL),
  and call it the satisfaction relation for S. If the system is clear from the context I just write $\vDash$.
\end{notn}

\begin{notn}
Let $\sigma$ be a trace, then $\sigma_i$ is the $i$th state in $\sigma$, $\sigma^i$ is $\sigma$ with the first $i$ elements removed, and $\epsilon$ is the empty sequence.
\end{notn}

\begin{defn}[LTL Semantics]\label{ltlsem}

  Let $P$ be a set of propositional variables and $\sigma$ a trace. The satisfaction relation $\vDash_{\text{LTL}}$ is inductively defined as follows:
\begin{align*}
  \sigma &\vDash a \tiff a \in \sigma_0\\
  \sigma &\nvDash \bot\\
  \sigma &\vDash \neg \varphi \tiff \sigma \nvDash \varphi\\
  \sigma &\vDash \varphi \lor \psi \tiff \sigma \vDash \varphi \tor \sigma \vDash \psi\\
  \sigma &\vDash \varphi \land \psi \tiff \sigma \vDash \varphi \tand \sigma \vDash \psi\\
  \sigma &\vDash \bigcirc \varphi \tiff \sigma^1 \vDash \varphi\\
  \sigma &\vDash \varphi \U \psi \tiff \sigma^i \vDash \psi \fsome i \geq 0 \tand \sigma^j \vDash \varphi \fall 0 \leq j < i
\end{align*}

\end{defn}

\begin{defn}[Formula Equivalence]
  Two LTL formula are equivalent if and only if they agree on all traces. That is:
  \[\varphi\equiv\psi \tiff \fall \sigma\in P^+ \text{ we have } \sigma\vDash\varphi = \sigma\vDash\psi\]
\end{defn}

\begin{lem}[Expansion laws]\label{ltlexp}

  In LTL, the following equivalences hold:
  \begin{align}
    \Box \varphi &\equiv \varphi \land \bigcirc \Box \varphi\label{elbox}\\
    \Diamond \varphi &\equiv \varphi \lor \bigcirc \Diamond \varphi\label{eldiamond}\\
    \psi \U \varphi &\equiv \varphi \lor (\psi \land \bigcirc (\psi \U \varphi))\label{elU}
  \end{align}

\end{lem}

A proof of \Cref{ltlexp} is available in \textcite[249]{baier2008principles}.

\begin{eg}[LTL example]\label{ltleg}
  Let $r,y,g\in P$ and $\varphi = \Box g \to (\neg r \U y)$ be an LTL formula. Think of $r,y,g$ as red, yellow and green lights being activated i.e., traffic lights. Then the formula $\varphi$ specifies the property that after a green light, there should always be a yellow light before a red light.

  The trace $(\{g\},\{r\},\dots)$ violates $\varphi$.

  The trace $(\{g\},\{g\},\{g\},\dots)$ satisfies $\varphi$, as does $(\{g\},\{y\},\{r\},\{g\},\{y\},\{r\},\dots)$.
\end{eg}


\subsection{Finite LTL}
For runtime verification, we need to reason about finite traces. Since LTL is defined over infinite traces, a modification of the logic is necessary to apply it to runtime verification problems.
There are several variations of finite LTL semantics, I will consider Infinite Extension LTL (IE-LTL)~\autocite{rosu2005rewriting}, RV-LTL~\autocite{bauer2010comparing} and the two logics that RV-LTL is based upon, FLTL and LTL$_3$~\autocite{bauer2010comparing}.
Assume that each trace $\sigma$ in this section is finite.

\subsubsection{IE-LTL} The idea behind IE-LTL is to assume that the final state of a trace repeats forever. For IE-LTL, the only difference in the semantics is in the final state. The syntax remains the same as in LTL.
\begin{defn}[IE-LTL semantics]\label{ieltlsem}

  %Let $\sigma_f$ be the final state of the trace.
  Define the satisfaction relation for IE-LTL $\vDash_{\text{IE-LTL}}$ as follows. Copy the semantics from the LTL semantics (\Cref{ltlsem}) except for the `next' $\bigcirc$ and `until' $\U$ operators, and redefine them as follows:
  \begin{align*}
    \sigma &\vDash \bigcirc \varphi =
      \begin{cases}
        \top &\text{if } \sigma^1 \vDash \varphi \tand \sigma^1 \ne \epsilon\\
        \top &\text{if } \sigma \vDash \varphi \tand \sigma^1 = \epsilon\\
        \bot &\text{otherwise}
      \end{cases}\\
    \sigma &\vDash \varphi \U \psi =
    \begin{cases}
      \top &\text{if } \sigma^i \vDash \psi \fsome i > 0 \tand \sigma^j \vDash \varphi \fall 0 \leq j < i\\
      \top &\text{if } \sigma \vDash \psi \tand \sigma^1 = \epsilon\\
      \bot &\text{otherwise}
    \end{cases}
  \end{align*}
  A full definition is given in the Appendix as \Cref{ieltlsemfull}.
\end{defn}

\begin{eg}[IE-LTL examples]\label{ieltleg}
  Let $r,y,g\in P$ and $\varphi = \Box (g \to (\neg r \U y))$ be an IE-LTL formula, the same traffic light formula formula from \Cref{ltleg}.

  The trace $(\{g\},\{r\})$ violates $\varphi$. The trace $(\{g\})$ satisfies it, as does $(\{g\},\{y\},\{r\})$.

  Let $\psi = \Box \Diamond g $, be the property saying that there will always be another green.

  The trace $(\{g\},\{r\})$ violates $\psi$, as does $(\{g\},\{y\},\{r\})$. The trace $(\{g\})$ satisfies it.

\end{eg}


\subsubsection{FLTL} For FLTL, the next operator of LTL is split into a weak ($\wn$) and strong ($\sn$) version.
The strong next requires the existence of a next state to be true, while the weak next operator is vacuously true if there is no next state.
Thus, in the final state, the weak operator evaluates to true, and the strong next to false. The strong and weak next operators are dual of each other, with  $\neg\sn\varphi \equiv \wn\neg\varphi$.

\begin{defn}[FLTL Syntax]\label{fltlsyn}

  A FLTL formula $\varphi$ is inductively defined as follows:
  \[\varphi ::= a ~|~ \bot ~|~ \neg \varphi ~|~\varphi \lor \varphi ~|~ \varphi \land \varphi ~|~ \sn \varphi ~|~ \wn \varphi ~|~ \varphi \U\varphi\]

  $\sn$ is pronounced as `strong next' and $\wn$ as `weak next'.
\end{defn}

  FLTL uses the same abbreviations as LTL (\Cref{ltlabbrev}).

\begin{defn}[FLTL semantics]\label{fltlsem}

  Define the satisfaction relation for FLTL $\vDash_{\text{FLTL}}$ as follows.
  Copy the standard LTL semantics in \Cref{ltlsem}, and replace the rule for the next operator with:
  \begin{align*}
    \sigma&\vDash\sn\varphi \tiff \sigma^1\vDash\varphi \tand \sigma^1 \neq \epsilon\\
    \sigma&\vDash\wn\varphi \tiff \sigma^1\vDash\varphi \tor \sigma^1 = \epsilon
  \end{align*}
  A full definition is given in the Appendix as \Cref{fltlsemfull}.
\end{defn}


\begin{lem}[Expansion Laws for FLTL]\label{fltlexp}

  In FLTL, the following expansion laws are equivalences:
  \begin{align}
    \Box \varphi &\equiv \varphi \land \wn \Box \varphi \label{felBox}\\
    \Diamond \varphi &\equiv \varphi \lor \sn \Diamond \varphi\label{felDiamond}\\
    \psi \U \varphi &\equiv \varphi \lor (\psi \land \sn (\psi \U \varphi))\label{felU}
  \end{align}

\end{lem}

\begin{eg}[FLTL examples]\label{fltleg}
  Let $r,y,g\in P$ and $\varphi = \Box (g \to (\neg r \U y))$ be an FLTL formula, the same traffic light formula formula from \Cref{ltleg}.

  The trace $(\{g\},\{r\})$ violates $\varphi$. The trace $(\{g\})$ satisfies it, as does $(\{g\},\{y\},\{r\})$.

  Let $\psi = \Box \Diamond g $, the second property in \Cref{ieltleg}.

  The trace $(\{g\},\{r\})$ violates $\psi$, as does $(\{g\},\{y\},\{r\})$. The trace $(\{g\})$ satisfies $\psi$.

\end{eg}

A proof of \Cref{fltlexp} is available in \autocite[5.3]{bauer2010comparing}.
  %Bauer 5.3

\subsubsection{\ltlt} In \ltlt, a new truth value is introduced to represent uncertainty. The uncertainty is that there are some suffixes which satisfy the trace and some which do not. \ltlt\ uses the same syntax (\Cref{ltlsyn}) and abbreviations (\Cref{ltlabbrev}) as LTL.


\begin{defn}[\ltlt\ semantics]\label{ltltsem}

  The semantics for \ltlt\ is defined by cases relying on standard LTL semantics (\Cref{ltlsem}). The notation $\sigma\gamma$ refers to the concatenation of the infinite trace $\gamma$ to the finite trace $\sigma$.
  Define the satisfaction relation for \ltlt\ $\vDash_{\text{\ltlt}}$ as follows.
  \[\sigma\vDash_{\text{\ltlt}}\varphi =
    \begin{cases}
      \top & \text{if } \sigma\gamma \vDash{\text{LTL}} \varphi \fall \gamma \in P^+\\
      \bot & \text{if } \sigma\gamma \vDash{\text{LTL}} \varphi \fall \gamma \in P^+\\
      ? & \text{otherwise}
    \end{cases}
    \]
    Where $?$ is a truth value called `inconclusive'. The value $?$ is not part of the syntax of \ltlt, rather it is part of the semantic meta-language~\autocite[659]{bauer2010comparing}.
    % A full definition is given in Appendix \ref{fulldef} as \Cref{ltltsemfull}.
\end{defn}

It may not obvious on first reading that runtime verification using \ltlt\ is decidable. A runtime verification procedure for \ltlt\ is given in \textcite[6]{arafat2005runtime}. The procedure is doubly exponential with respect to the size of the input formula.

\begin{eg}[LTL$_3$ examples]
Let $r,y,g\in P$ and $\varphi = \Box (g \to (\neg r \U y))$ be an \ltlt\ formula, the same traffic light formula formula from \Cref{ltleg}.

  The trace $(\{g\},\{r\})$ violates $\varphi$. The trace $(\{g\})$ is inconclusive, as is $(\{g\},\{y\},\{r\})$.

  Let $\psi = \Box \Diamond g $, the second property in \Cref{ieltleg}.

  The trace $(\{g\},\{r\})$ is inconclusive, as is $(\{g\})$, and also $(\{g\},\{y\},\{r\})$.
\end{eg}

\subsubsection{RV-LTL} RV-LTL is based on FLTL and \ltlt. RV-LTL gains the capability to represent uncertainty from \ltlt, while giving more useful information than simply `the verification was inconclusive', by differentiating between inconclusive cases using the weak and strong next operators from FLTL.

RV-LTL uses the same syntax as FLTL (\Cref{fltlsyn}) and the abbreviations of LTL (\Cref{ltlabbrev}).

\begin{defn}[RV-LTL semantics]\label{rvltlsem}

  The semantics for RV-LTL are defined by cases.
  Define the satisfaction relation for RV-LTL $\vDash_{\text{RV-LTL}}$ as follows.
  \[\sigma\vDash_{\text{RV-LTL}}\varphi =
    \begin{cases}
      \top & \text{if } \sigma \vDash_{\text{\ltlt}} \varphi = \top\\
      \bot & \text{if } \sigma \vDash_{\text{\ltlt}} \varphi = \bot\\
      \top^P & \text{if } \sigma \vDash_{\text{\ltlt}} \varphi = ~?\tand \sigma\vDash_{\text{FLTL}} = \top \\
      \bot^P & \text{if } \sigma \vDash_{\text{\ltlt}} \varphi = ~?\tand \sigma\vDash_{\text{FLTL}} = \bot
    \end{cases}
  \]
  $\top^P$ is pronounced `presumably true' and $\bot^P$ is pronounced `presumably false'.
  Note that $\bot^P$ and $\top^P$ are part of the semantic meta-language, not the formula syntax.
\end{defn}

\begin{eg}[RV-LTL examples]
Let $r,y,g\in P$ and $\varphi = \Box (g \to (\neg r \U y))$ be an RV-LTL formula, the same traffic light formula formula from \Cref{ltleg}.

  The trace $(\{g\},\{r\})$ violates $\varphi$. The trace $(\{g\})$ presumably violates $\varphi$. Finally $(\{g\},\{y\},\{r\})$ presumably satisfies the trace.

  Let $\psi = \Box \Diamond g $, the second property in \Cref{ieltleg}.

  The trace $(\{g\},\{r\})$ presumably violates $\psi$ as does $(\{g\},\{y\},\{r\})$. The trace $(\{g\})$ presumably satisfies $\psi$.
\end{eg}

\subsection{Timed Propositional Temporal Logic}
Timed Propositional Temporal Logic (TPTL)\autocite{alur1994really} is an extension of LTL to encode explicit time into the logic.
In LTL, only the order of states is reasoned about, i.e., $\sigma_i$ is before $\sigma_{i+1}$, but for many verification problems it can be useful to reason about the explicit time at which a state occurs, i.e., $\sigma_i$ is 3 time units earlier than $\sigma_{i+1}$.
For this, we define a timed trace that contains the sequence of times corresponding to the sequence of states.
A quantifier called a \emph{freeze operator} is added to the logic, which binds occurrences of a variable to the time at which the operator is evaluated.
Integer comparison is added to the logic, to allow for specifications such as: ``If $p$ becomes true, $q$ will become true within 5 time units''.

TPTL is a generalisation of LTL, all properties expressed in LTL are expressible in TPTL as well.

\begin{defn}[Timed Trace]

  A Timed Trace $\rho = (\sigma,\tau)$ is a pair of a trace (state sequence) $\sigma \in P^+$ and a time sequence $\tau \in \mathbb{N}^+$ which is a sequence of non-negative integers that is monotonically non-decreasing ($\forall i. ~\tau_i \leq \tau_{i+1}$) and eventually always increasing ($\forall i. \exists j. ~\tau_i < \tau_j$).
\end{defn}

Assume there exist an infinite supply of time variables  and let $V=\{x,y,z\dots\}$ be the set of these variables.

\begin{defn}[TPTL Syntax]\label{tptlsyn}
  Let $a\in P$ be a propositional variable, $x\in V$ be a time variable and $c\in\mathbb{N}$ a constant.

  TPTL terms $\pi$ and formulas $\varphi$ are inductively defined as follows:
  \begin{align*}
    \pi &::= x + c ~|~ c\\
    \varphi &::= a ~|~ \pi \leq \pi ~|~ \bot ~|~ \neg \varphi ~|~\varphi \lor \varphi ~|~ \varphi \land \varphi ~|~ \bigcirc \varphi ~|~ \varphi \U \varphi ~|~ x. \varphi
  \end{align*}
\end{defn}

We read $x. \varphi$ as `freeze $x$ in $\varphi$'.

\begin{notn}[Abbreviations]\label{tptlabbrev}

  TPTL has the same abbreviations as LTL, plus abbreviations for comparison operations between terms such as $\pi_1 < \pi_2 := \pi_1 \leq \pi_2 \land \neg(\pi_2 \leq \pi_1)$, and so on as expected for $>,\geq,=,\neq$.
\end{notn}

\begin{defn}[TPTL Semantics]\label{tptlsem}

  Let $\rho = (\sigma,\tau)$ be a timed trace, $x\in V$, $c\in\mathbb{N}$, and let $\eval:V\to\mathbb{N}$ be an (initially empty) evaluation of time variables to times, with $\eval(x + c) = \eval(x) + c$, $\eval(c) = c$ and $\eval[x:=c]$ denoting the evaluation which agrees with $\eval$ for $V\setminus\{x\}$ and maps $x$ to $c$.
  TPTL uses the same semantics as LTL (\Cref{ltlsem}) for those operators which overlap with LTL, except the relation is defined over a timed trace rather than a standard trace. For those cases, substitute occurrences of $\sigma\vDash_{\text{LTL}}\cdots$ with $\rho,\eval\vDash_{\text{TPTL}}\cdots$. The remainder of the definition is as follows:
  \begin{align*}
    \rho,\eval &\vDash_{\text{TPTL}}\pi_1\leq\pi_2 \tiff \eval(\pi_1)\leq\eval(\pi_2)\\
    \rho,\eval &\vDash_{\text{TPTL}} x.\varphi \tiff \rho,\eval[x:=\tau_0]\vDash\varphi
  \end{align*}
  A full definition is given as \Cref{tptlsemfull}
\end{defn}

\begin{eg}[TPTL examples]\label{tptleg}
  Let $r,y,g\in P$ and \[\varphi = \Box ~x_1.~ (g \to (\neg r ~\U~ x_2.~ (y \land x_2 \leq x_1 + 10) ))\] be a TPTL formula, our traffic light example, but with the added requirement that yellow always occurs within 10 time steps from green.

  The timed trace $((1,\{g\}),(2,\{r\}),\dots)$ violates $\varphi$, as does $((1,\{g\}),(12,\{y\}),(15,\{r\}),\dots)$, and also $((1,\{g\}),(2,\{g\}),\dots)$.

  The timed trace $((0,\{g\}),(10,\{y\}),(15,\{r\}),(20,\{g\}),(30,\{y\}),(35,\{r\}),\dots)$ satisfies $\varphi$, as does $((100,\{\}),(200,\{\}),\dots)$ (vacuously).

\end{eg}

\subsection{Finite TPTL}

\subsubsection{IE-TPTL} As in IE-LTL, in IE-TPTL we assume that the final state of a trace repeats forever. I'm not sure if this has been studied before. In \textcite{chai2013rewriting} a runtime verification algorithm for TPTL is introduced, which looks like IE-TPTL, but it is not clear if that's what is used.\\
In IE-TPTL, the only difference from TPTL is the semantics in the final state. The syntax remains the same as in TPTL.

\begin{defn}[IE-TPTL semantics]\label{ietptlsem}

  Define the semantic relation $\vDash_{\text{IE-TPTL}}$ of IE-TPTL as follows. Copy the semantics from the TPTL semantics (\Cref{tptlsem}), and redefine the `next' $\bigcirc$ and `until' $\U$ operators as follows:
  \begin{align*}
    \rho,\eval&\vDash \bigcirc \varphi =
    \begin{cases}
      \top &\text{if } \rho^1,\eval \vDash \varphi \tand \rho^1 \ne \epsilon\\
      \top &\text{if } \rho,\eval\vDash \varphi \tand \rho^1 = \epsilon\\
      \bot &\text{otherwise}
    \end{cases}\\
    \rho,\eval&\vDash \varphi \U \psi =
    \begin{cases}
      \top &\text{if } \rho^i,\eval \vDash \psi \fsome i > 0 \tand \rho^j,\eval \vDash \varphi \fall 0 \leq j < i\\
      \top &\text{if } \rho,\eval\vDash \psi \tand \rho^1 = \epsilon\\
      \bot &\text{otherwise}
    \end{cases}
  \end{align*}
  A full definition is given as \Cref{ietptlsemfull}
\end{defn}

\begin{remk}
IE-TPTL has some interesting consequences when applied to timed formulae. For example, the formula $\Box x.~ \Diamond y.~ y > x$ is always false, since the time of the final state is repeated forever. I suspect another solution is desirable.

A solution to this problem could be to simplify the formula in the last state to only have time constraints remaining, which can be done since we know that the state will remain the same in an infinite extension. One would then pass the time constraints to a quantifier elimination procedure in order to make a decision.
\end{remk}

\begin{eg}[IE-TPTL examples]\label{ietptleg}
  Let $r,y,g\in P$ and \[\varphi = \Box ~x_1.~ (g \to (\neg r ~\U~ x_2.~ (y \land x_2 \leq x_1 + 10) ))\] be an IE-TPTL formula, our traffic light example from \Cref{tptleg}.

  The timed trace $((1,\{g\}),(2,\{r\}))$ violates $\varphi$, as does $((1,\{g\}),(12,\{y\}),(15,\{r\}))$, and also $((1,\{g\}),(2,\{g\}))$.

  The timed trace $((0,\{g\}),(10,\{y\}),(15,\{r\}))$ satisfies $\varphi$, as does $((100,\{\}))$ (vacuously).
\end{eg}

\subsubsection{RV-TPTL} The following finite semantics for TPTL, which I name RV-TPTL, is a combination of the RV-LTL four valued logic and TPTL. I have not seen this combination elsewhere in the literature, and thus assume it is new. The closest I have seen is the three valued TLTL$_3$~\autocite[6]{arafat2005runtime} which is based on \ltlt\ and TLTL, a different timed temporal logic. The broad idea is that if RV-LTL is finite LTL + uncertainty and TPTL is LTL + explicit time, then RV-TPTL is finite LTL + uncertainty + explicit time.

\begin{defn}[RV-TPTL Syntax]

  Define the formulas of RV-TPTL as:
  \begin{align*}
    \pi &::= x + c ~|~ c\\
    \varphi &::= a ~|~ \pi \leq \pi ~|~ \bot ~|~ \neg \varphi ~|~\varphi \lor \varphi ~|~ \varphi \land \varphi ~|~ \sn \varphi ~|~ \wn \varphi ~|~ \varphi \U \varphi ~|~ x. \varphi
  \end{align*}
\end{defn}

  RV-TPTL uses the same abbreviations as TPTL (\Cref{tptlabbrev}).

\begin{defn}[RV-TPTL Semantics]\label{rvtptlsem}

  I will give the semantics based on TPTL, in an analogous way to how RV-LTL was given.
  Let $\eval:V\to\mathbb{N}$ be an (initially empty) evaluation of time variables to times as in TPTL (\Cref{tptlsem}).
  The notation $\rho\omega$ refers to the concatenation of the infinite timed trace $\omega$ to the finite timed trace $\rho$.
  I will define two semantic relations in order to then define the RV-TPTL semantics. These are essentially TPTL$_3$ and FTPTL respectively.

  Let $\vDash_{T3}$ be given by:
  \[\rho,\eval\vDash_{T3}\varphi = \begin{cases}
    \top & \text{if } \rho\omega,\eval \vDash_{\text{TPTL}} \varphi \fall \omega \in (P^+,\mathbb{N}^+)\\
    \bot & \text{if }  \rho\omega,\eval \vDash_{\text{TPTL}} \varphi \fall \omega \in (P^+,\mathbb{N}^+)\\
      ? & \text{otherwise}
    \end{cases}
  \]

  Let $\vDash_{FT}$ be defined by taking TPTL semantics and adding:
  \begin{align*}\label{ftsem}
    \rho,\eval&\vDash_{FT}\sn\varphi \tiff \rho^1,\eval\vDash_{TPTL}\varphi \tand \rho^1 \neq \epsilon\\
    \rho,\eval&\vDash_{FT}\wn\varphi \tiff \rho^1,\eval\vDash_{TPTL}\varphi \tor \rho^1 = \epsilon
  \end{align*}

  Finally, define $\vDash_{\text{RV-TPTL}}$, the satisfaction relation for RV-TPTL, by the following:
  \[\rho\vDash_{\text{RV-TPTL}}\varphi =
    \begin{cases}
      \top & \text{if } \rho,\eval\vDash_{T3} \varphi = \top\\
      \bot & \text{if } \rho,\eval \vDash_{T3} \varphi = \bot\\
      \top^P & \text{if } \rho,\eval \vDash_{T3} \varphi = ~?\tand \rho,\eval\vDash_{FT} = \top \\
      \bot^P & \text{if } \rho,\eval \vDash_{T3} \varphi = ~?\tand \rho,\eval\vDash_{FT} = \bot
    \end{cases}
  \]
\end{defn}

\begin{eg}[RV-TPTL examples]
  Let $r,y,g\in P$ and \[\varphi = \Box ~x_1.~ (g \to (\neg r ~\U~ x_2.~ (y \land x_2 \leq x_1 + 10) ))\] be an IE-TPTL formula, our traffic light example from \Cref{tptleg}.

  The timed trace $((1,\{g\}),(2,\{r\}))$ violates $\varphi$,
  as does $((1,\{g\}),(12,\{y\}),(15,\{r\}))$.

  The timed trace $((0,\{g\}),(10,\{y\}),(15,\{r\}))$ presumably satisfies $\varphi$, as does $((100,\{\}))$.

  The timed trace $((1,\{g\}),(2,\{g\}))$ presumably violates the trace.
\end{eg}

\section{Runtime Verification using Formula Rewriting}
\subsection{Formula Rewriting}
Formula rewriting~\autocite{rosu2005rewriting}, or formula progression, is a technique used in runtime verification.
The idea is to simplify the formula using the truth values at the current state, then rewrite the formula using the expansion laws, and finally remove the top level `next' ($\bigcirc,\sn,\wn$) operators (except in the final state). This is also referred to as progression, the formula has been progressed. The resulting formula is true at the next state iff the original formula was true at the original state in the trace.
Each state is consumed in the process, and all relevant information from the past is brought forward in the rewritten formula.

In the final state, the formula may be rewritten with expansion laws and simplified based on the state, but one might not want to fully progress the formula, as is the case in RV-TPTL, FLTL and RV-LTL, where the semantics require that the `next' operators are not stripped as they were for the non-final states. For IE-LTL and IE-TPTL, the `next' operators are stripped in any case, so the final state distinction is not as important.

\begin{notn}[Rewrites]

  Let $\rw{\text{S},E}$ denote a formula rewriting step under the logical system S with the state $E$. E.g. $\varphi\rw{\text{RV-LTL},E}\psi$ says that the formula $\varphi$ rewrites to $\psi$ under RV-LTL using the state $E$.
\end{notn}

\begin{eg}[Traffic Lights]

  For a simple example, consider the LTL traffic light example from \textcite[175]{rosu2005rewriting}, with $P=\{r,y,g\}$, $\sigma = (\{g\},\{r\},\dots)$ and $\varphi = \Box (g \to (\neg r \U y))$. The trace $\sigma$ should violate the formula. Let $\rw{E}$ stand for $\rw{\text{IE-LTL},E}$ in this example. Here is the progression:
\begin{align}
  \Box (g \to (\neg r \U y)) &\rw{\{g\}} \Box (g \to (\neg r \U y)) \land (\neg r \U y)\label{rw1}\\
  &\rw{\{r\}} \bot\label{rw2}
\end{align}

The rewrite in~\eqref{rw1} uses the expansion law $\Box \varphi \equiv \varphi \land \bigcirc \Box \varphi$ and then rewrites that given that $g$ is true.
Then in~\eqref{rw2} the formula is rewritten to false, since the right conjunct is false given $r$ being true. This is the case whether or not $\{r\}$ is the final state in the trace. If the trace were longer no more of it would need to be validated, all possible suffixes of $\sigma$ violate the formula $\varphi$.
\end{eg}



\subsubsection{Decision procedure for RV-TPTL}
In order to decide if a trace satisfies or violates a formula in RV-TPTL, the following procedure can be used.

\begin{desc}[RV-TPTL]\label{decision}
  Let $\rho=(\rho_0,\rho_1,\dots,\rho_n)$ be a timed trace and $\varphi$ a RV-TPTL formula.

  Then let $\psi$ be the result of rewriting $\varphi$ $n$ times, corresponding to the first $n$ states of $\rho$, and let $\eval^{n-1}$ be the resulting time evaluation.

  Now rewrite $\psi$ using $\rho_n$, but do not remove the `next' operators i.e., do not progress the formula, only expand and simplify.
  Simplification will decide any non-`next' formulae, such that the resulting formula consists of conjunctions and/or disjunctions of `next' formulae e.g., $\sn p \land \wn q \lor \sn r$ is in the described form. Let $\phi$ be the resulting formula and $\eval^n$ be the resulting time evaluation.

  Then there are three cases to check in order to make a decision.

  First, we check if $\neg\phi$ is satisfiable, which can be checked using a tableau method such as in \textcite{alur1994really}. If $\neg\phi$ is unsatisfiable, then $\phi$ is valid and we have that $\rho_n\omega, \eval^n \vDash \phi$ for all $\omega\in (P^+,\mathbb{N}^+)$, and therefore $\rho,\eval^n \vDash \varphi$ and the decision procedure terminates.

  Secondly, if $\neg\phi$ was satisfiable, now check if $\phi$ is satisfiable using the same tableau method. If $\phi$ is unsatisfiable then we know that $\rho_n\omega, \eval^n \nvDash \phi$ for all $\omega\in (P^+,\mathbb{N}^+)$, and therefore $\rho,\eval^n \nvDash \varphi$ and the decision procedure terminates.

  Finally, if $\phi$ is satisfiable, then transform all $\sn$ formulae into $\bot^P$ and all $\wn$ formulae into $\top^P$. Then evaluate the formula based on $\lor$ being the least upper bound and $\land$ being the greatest lower bound, using the ordering $\top \geq \top^P \geq \bot^P \geq \bot$. The resulting formula is the result of the decision procedure.
\end{desc}

My implementation is only an incomplete version of the above decision procedure, I do not check satisfiability of $\phi$ or $\neg\phi$, so cannot tell if the formula is true or false for all suffixes. See \Cref{rvimp} for more information.

\begin{eg}[Apples]
  Let $\rw{E}$ stand for $\rw{\text{RV-TPTL},E}$ in this example.

  For a timed example in RV-TPTL, consider a container of apples which needs to be delivered to a store within a specified time.
  Let $V=\{sent, received\}$,
  \(\rho=((\{sent\},\{received\}),(1,4))\)
  and \(\varphi=\Box x. (sent \to \Diamond y. (received \land y \leq x + 3))\).
  The trace $\rho$ will presumably satisfy the formula.
  Here is the progression:
  \begin{align}
    &\Box x. (sent \to \Diamond y. (received \land y \leq x + 3))\nonumber\\
    \rw{\{sent\}}
    &\Box x. (sent \to \Diamond y. (received \land y \leq x + 3))\nonumber\\
    &\land \Diamond y. (received \land y \leq 4)
    \label{eg-apples1}\\
    \rw{\{received\}}
    &(\wn \Box x. (sent \to \Diamond y. (received \land y \leq x + 3))\nonumber\\
    &\land \sn \Diamond y. (received \land y \leq 4))\nonumber\\
    &\lor \wn \Box x. (sent \to \Diamond y. (received \land y \leq x + 3))\label{eg-apples2}\\
    \equiv
    &\top^P\label{eg-apples3}
  \end{align}
  The formula $\varphi$ is rewritten to~\eqref{eg-apples1} using simplification given $\{sent\}$ and the expansion law $\Box \varphi \equiv \varphi \land \wn \Box \varphi$~\eqref{felBox}.
  Then the formula is rewritten to~\eqref{eg-apples2} using the expansions laws~\eqref{felBox} and~\eqref{felDiamond} given $\{received\}$.
  Note that the next operators are not stripped in this last state of the trace.
  Since the end of the trace is reached, we have $(\top^P \land \bot^P) \lor \top^P$ by the semantics of RV-TPTL, which is equivalent to $\top^P$ in~\eqref{eg-apples3}.

  Thus the formula $\varphi$ presumably satisfies the trace $\rho$.
  Adding a finite suffix could change that result, namely if you have a trace where $sent$ is never followed by $received$.
  In this case you, would get the result $\bot^P$ instead.

  Note that this formula is only ever satisfied or violated by infinite traces, which is why the uncertainty given by RV-TPTL is plausibly desirable given a finite trace.
\end{eg}

\subsection{Related Work}
Formula rewriting was devised for LTL in \textcite{rosu2005rewriting}, as part of the Java PathExplorer project, and has been used in some NASA programs. The technique was revised for TPTL in \textcite{chai2013rewriting}, with a case study of its potential for use in a train control system. In both of these works, a separate rewrite engine called Maude~\autocite{clavel2002maude} was used. In the next section, I discuss the implementation of my rewrite based verification tool, which does not use Maude.

\section{Implementation in Scala}\label{implementaion}
I have implemented a runtime verifier in the Scala programming language.
It is embedded into Scala as an internal Domain Specific Language (DSL), this is also known as a shallow embedding.
I allow the user to choose a logic, either RV-TPTL or IE-TPTL.
My verifier is structured as a library that can be integrated into other Scala programs.
I will describe the interesting aspects of my implementation. I have tried to present the implementation without getting bogged down in details, so I have simplified the code listings to be more readable where possible.

\subsection{Shallow Embedding}
When implementing a Domain Specific Language, it is possible to write an internal or external DSL, also known as shallow or deep embedded DSLs respectively. In a deep embedding, the implementer is required to create a parser that translates the DSL into another another form for evaluation. In a shallow embedding, the DSL takes form within the parent language, delegating the parsing to the parser of the language, which has already been written and tested. The terms of the DSL become types within the parent language and then the implementer can use the libraries and infrastructure provided for that language~
\autocite{gibbons2014foldingdeepshallow}.

In the case of this project, I have written a shallow embedding of IE-TPTL and RV-TPTL in the programming language Scala~\autocite{Odersky04scala}.
I was partly inspired by some of the syntax examples in \textcite{barringer2011tracecontract}.
Using Scala classes, methods, and implicits I have constructed a convenient DSL for specifying temporal properties.

For example, to write the formula $\Box x. (a \to \Diamond y. (b \land (y \leq x + 2)))$ using my DSL, I can write \lstinline{G ('x ~ (a -> F ('y ~ (b /\ ('y <= 'x + 2)))))}.

The language is mostly defined using methods of the abstract class \lstinline{Formula}. Here are some of the basic definitions for LTL fragment:
\begin{lstlisting}[label=lstbasic]
abstract class Formula {
  ...
  def /\(f:Formula) = And(this,f)
  def \/(f:Formula) = Or(this,f)
  def ->(f:Formula) = Or(this.compl,f)
  def unary_!() = Neg(this)
  def U(f:Formula) = Until(this,f)
}

object Formula {
  def X(f:Formula) = Next(f)
  def N(f:Formula) = WeakNext(f)
  def F(f:Formula) = Future(f)
  def G(f:Formula) = Globally(f)
  ...
}
\end{lstlisting}
Formula are represented as case classes and objects in Scala, for example $\land$ is defined as:
\begin{lstlisting}
case class And(f1: Formula, f2: Formula) extends BinOp("∧") {...}
\end{lstlisting}
These case classes and objects all inherit from the abstract classes \lstinline{Formula}, either directly or via another abstract class such as \lstinline{BinOp} which represents binary operators.

Importantly, I implemented atoms as functions rather than propositional variables:
\begin{lstlisting}
case class Atom[A](name: String, interpretation: A => Boolean) extends Formula
...
  def apply[A](state: (Int,A)): Formula = this match {
      if (interpretation(state._2)) True
      else False
  }
\end{lstlisting}

The \texttt{apply} function takes a timed state and simplifies based on that interpretation. An \texttt{Atom} has an \texttt{interpretation} function (passed to the constructor) which takes any type as input (e.g., a String, a List, etc) and outputs a boolean, and the \texttt{apply} function maps that boolean to \texttt{True} or \texttt{False}, which are \texttt{Const} objects in my logic, not the Scala booleans \texttt{true} and \texttt{false}.
\begin{lstlisting}
abstract class Const(name: String, n: Int) extends Formula with Ordered[Const] {...}
case object False extends Const("⊥",0)
case object PFalse extends Const("⊥ᴾ",1)
case object PTrue extends Const("⊤ᴾ",2)
case object True extends Const("⊤",3)
\end{lstlisting}

Time terms and formulae are brought into the language using implicit classes and methods:
\begin{lstlisting}
  implicit def TimeVarSymbolNoOffset(x: Symbol) = TimeVar(x,0)
  implicit class TimeVarSymbol(x: Symbol) {
    def ~(f: Formula) = Freeze(x,f) // e.g. 'x ~ (a /\ b) is a Formula
    def +(t: Int) = TimeVar(x,t) // e.g. 'x + 15 is a TimeTerm
    def <=(t2: TimeTerm) = LTEQ(TimeVar(x,0),t2)
    def ~=(t2: TimeTerm) = LTEQ(TimeVar(x,0),t2) /\ LTEQ(t2,TimeVar(x,0))
    def <(t2: TimeTerm) = LTEQ(TimeVar(x,0),t2) /\ !LTEQ(t2,TimeVar(x,0))
    def >(t2: TimeTerm) = !LTEQ(TimeVar(x,0),t2)
    def >=(t2: TimeTerm) = LTEQ(t2,TimeVar(x,0))
  }
\end{lstlisting}
These are considered advanced features of Scala, and I did have some trouble understanding them at first. These methods allow me to convert other types into formulae and terms implicitly i.e., I can just write \lstinline{'x + 2} and the compiler will look for a \texttt{+} method for Symbol, which doesn't exist, and then look for a matching implicit, in this case evaluating to a \lstinline{TimeVar('x,2)}.

The time terms and formulae are represented again as classes such as \lstinline{LTEQ} for the less than or equal to ($\leq$) operator and \lstinline{Freeze} for the freeze ($x.$) quantifier:
\begin{lstlisting}
case class Freeze(x: Symbol, f: Formula) extends Formula {...}
case class LTEQ(t1: TimeTerm, t2: TimeTerm) extends Formula {...}
\end{lstlisting}

% Formulas are represented as a class structure, as shown in Listing \ref{lstclasses}.

% \begin{lstlisting}[caption={Class Structure},label=lstclasses]
% sealed abstract class Formula {...}
% case class Atom[A](name: String, interpretation: A => Boolean) extends Formula {...}
% sealed abstract class Const(name: String, n: Int) extends Formula with Ordered[Const] {...}
% sealed abstract class UnOp(opName: String) extends Formula {...}
% sealed abstract class BinOp(opName: String) extends Formula {...}
% case class Neg(f: Formula) extends UnOp("¬") {...}
% sealed trait temporalUnOp {...}
% case class Next(f: Formula) extends UnOp("○ˢ") with temporalUnOp {...}
% case class WeakNext(f: Formula) extends UnOp("○ᵂ") with temporalUnOp {...}
% case class Future(f: Formula) extends UnOp("◇") with temporalUnOp {...}
% case class Globally(f: Formula) extends UnOp("☐") with temporalUnOp {...}
% case class And(f1: Formula, f2: Formula) extends BinOp("∧") {...}
% case class Or(f1: Formula, f2: Formula) extends BinOp("∨") {...}
% case class Until(f1: Formula, f2: Formula) extends BinOp("U") {...}
% case class Freeze(x: Symbol, f: Formula) extends Formula {...}
% sealed abstract class TimeTerm {...}
% case class Time(c: Int) extends TimeTerm {...}
% case class TimeVar(x: Symbol, c: Int) extends TimeTerm {...}
% case class LTEQ(t1: TimeTerm, t2: TimeTerm) extends Formula {...}
% \end{lstlisting}

\subsection{Runtime Verification}
\subsubsection{Formula Rewriting}
I have implemented a runtime verifier on top of the shallow embedded domain specific language (DSL) for timed temporal logic. It uses a formula rewriting algorithm.
Other works on rewriting algorithms that I have read~\autocites{rosu2005rewriting,chai2013rewriting} used the rewriting engine Maude~\autocite{clavel2002maude} to perform their rewrites. This was not my approach.

Instead, I was given access to a `progression calculator' for LTL that my supervisor had written previously.
Using this as a base, I implemented my DSL to work with the provided progression functions which I then adapted to my project.
The progression function \texttt{expand} breaks down input formula into disjunctive normal form (DNF) clauses (a set of disjunctions between sets of conjunctions).
It then uses my simplification methods and expansion laws (\Cref{fltlexp}) to expand the formula (and subformula).
Once a formula is either simplified to True/False or has `next' ($\sn,\wn$) in front of it, it is done. Once all formulae are done, the resulting clause set is returned.

The other part of `progression' is the removal of `next' operators, which is done by the \texttt{unX} function. This function simply maps $\sn\varphi$ and $\wn\varphi$ to $\varphi$.

The simplification is processed by my \texttt{apply} and \texttt{simplify} methods.
The difference between these two methods is that \texttt{apply} does simplify based on the current state (the state is \emph{applied} to the formula), while \texttt{simplify} only uses the current time. Both methods check for some basic tautologies like $a\lor\neg a$.
The reason for the difference between the two simplification methods is that I only want to simplify propositional subformulae (subformulae not part of a temporal subformula) based on the current state interpretation.

When a temporal subformula is encountered, \texttt{apply} calls \texttt{simplify} on it.
The reason \texttt{simplify} has a time parameter, is to check if any time constraints in the subformula will always be true or false.
I found this simplification technique to be a significant performance improvement over plain rewriting, although I do not have measurements of this improvement.

My verifier takes a timed trace and a formula and recursively passes it to the \texttt{expand} and \texttt{unX} functions described above, until the final state is reached. In the final state the finalise method for the chosen logic is called. I will now describe these methods separately.

\subsubsection{IE-TPTL}
For the Infinite Extension semantics, we assume the final state is repeated forever. Because of this we can strip all temporal quantifiers i.e., $\Box \varphi, \Diamond \varphi, \psi \U \varphi, \bigcirc \varphi$ all become $\varphi$. While my implementation has `strong next' $\sn$ and `weak next' $\wn$ in it, in IE-TPTL they are both treated as if they were just the regular `next' $\bigcirc$.

For the freeze operator, the time of the final state is substituted into the occurrences of its bound variable. Any remaining time comparisons with free variables are treated as a tightly bound freeze quantifier e.g., $x + 2 < 5$ is treated like $x. (x + 2 < 5)$. Time comparisons without free variables are simply evaluated.

The remaining operators are simplified by \texttt{apply} as normal.

% \begin{lstlisting}[caption={Finalise method for IE-TPTL}]
% def finaliseIE[A](state: (Int, A)): Const = {
%     val t = state._1 // the time at the current state
%     val end = Int.MaxValue // a time far away
%     def inner(f: Formula): Formula = {
%       f match {
%         case op:temporalUnOp => inner(op.f) // strip temporal operators
%         case Until(_,sf) => inner(sf) // strip temporal operators
%         case Neg(sf) => Neg(inner(sf)) apply state
%         case Or(f1,f2) => Or(inner(f1),inner(f2)) apply state
%         case And(f1,f2) => And(inner(f1),inner(f2)) apply state
%         case fz @ Freeze(_, _) => {
%           val now = inner(fz.subst(t)) // substitute the time now
%           val fin = inner(fz.subst(end)) // and later
%           // then see if the result will eventually change
%           if (now != fin) {
%             vprintln(2,s"Subformula $f at time $t is $now, but eventually changes to $fin")
%             fin
%           }
%           else now
%         }
%         case lt @ LTEQ(_,_) => {...} // essentially same as Freeze
%         case _ => f apply state
%       }
%     }
%     inner(this)
%   }
% \end{lstlisting}

\begin{eg}[IE-TPTL verification example]\label{ieverifyeg}~\\
  The following shows an example of verifying the property $\Diamond y. ((y\leq x + 3) \land a)$ against the trace $((2,\epsilon),(5,(a)))$ and then $((2,\epsilon))$. It takes place in the Scala interpreter:
\begin{lstlisting}%[frame=none]
scala> val a = Atom("a",{x:List[String]=> x.contains("a")})
a: settlr.Atom[List[String]] = a

scala> val p = 'x ~ F('y~ (('y <= 'x + 3) /\ a))
p: settlr.Freeze = 'x. ◇ 'y. (('y <= 'x + 3) ∧ a)

scala> val trace = List( (2,List()), (5,List("a")))
trace: List[(Int, List[String])] = List((0,List()), (1,List(a)))

scala> verifyIETrace(p,trace)
Verifying: 'x. ◇ 'y. (('y <= 'x + 3) ∧ a)
Trace: [(2, List()),(5, List(a))]
Forumula Progressed: ◇ 'y. (('y <= 5) ∧ a)
Remaining Trace: [(5, List(a))]
finalise: ◇ 'y. (('y <= 5) ∧ a) @ time: 5, state: List(a)
Finalise result: ⊤
Satisfies trace.

res0: settlr.Formula = ⊤

scala> val trace2 = List( (2,List()))
trace2: List[(Int, List[Nothing])] = List((2,List()))

scala> verifyIETrace(p,trace2)
Verifying: 'x. ◇ 'y. (('y <= 'x + 3) ∧ a)
Trace: [(2, List())]
finalise: 'x. ◇ 'y. (('y <= 'x + 3) ∧ a) @ time: 2, state: List()
Finalise result: ⊥
Violates trace.

res1: settlr.Formula = ⊥
\end{lstlisting}
\end{eg}

\subsubsection{RV-TPTL}\label{rvimp}
My implementation is an approximation of RV-TPTL, since I do not check the values of all suffixes of the trace, instead I use simplification methods. If time permitted I would use a tableau procedure in the final state as I described in \Cref{decision}. My approximation should not give any incorrect results of `satisfied/violated', but may incorrectly give `presumably satisfied' when it should give `satisfied' and `presumably violated' when it should give `violated'. My implementation cannot detect these incorrect cases. This is regrettable and would be a priority if there were more time.

In the RV-TPTL \texttt{finalise} method, the formula is rewritten (but not progressed with \texttt{unX}) before finalising. This means the resulting formula is made up of conjunctions and/or disjunctions of `next' subformulae. This rewrite is necessary because the semantics are not defined for $\Box,\Diamond,\U$ in the final state (deliberately).

Then all occurrences of `weak next' ($\wn$) are replaced with `presumably true' ($\top^P$) and occurrences of `strong next' ($\sn$) are replaced with `presumably false' ($\bot^P$). Now the conjunctions and disjunctions can be evaluated, where `and' is the minimum of the conjuncts and `or' is the maximum of the disjuncts, with the ordering $\top>\top^P>\bot^P>\bot$.

\begin{eg}[RV-TPTL verification examples]~\\
  The following example is a continuation of the \Cref{ieverifyeg} example showing how verification results in RV-TPTL differ.
\begin{lstlisting}%[frame=none]
scala> verifyRVTrace(p,trace)
Verifying: 'x. ◇ 'y. (('y <= 'x + 3) ∧ a)
Trace: [(2, List()),(5, List(a))]
Forumula Progressed: ◇ 'y. (('y <= 5) ∧ a)
Remaining Trace: [(5, List(a))]
finalise: ◇ 'y. (('y <= 5) ∧ a) @ time: 5, state: List(a)
Result is {{}} by simplification
Finalise result: ⊤
Satisfies trace.

res2: settlr.Formula = ⊤

scala> verifyRVTrace(p,trace2)
Verifying: 'x. ◇ 'y. (('y <= 'x + 3) ∧ a)
Trace: [(2, List())]
finalise: 'x. ◇ 'y. (('y <= 'x + 3) ∧ a) @ time: 2, state: List()
Finalise result: ⊥ᴾ
Presumably violates trace.

res3: settlr.Formula = ⊥ᴾ
\end{lstlisting}
\end{eg}

\subsection{Discussion of Implementation}
My implemented runtime verification library demonstrates that formula rewriting is a viable technique for runtime verification in Scala, just as it is using other rewriting systems such as Maude. While no measurements have been taken, the implementation appears to run quickly for moderate sized traces, so long as the formula being checked is not long and complex. Rewriting has the downside of a worst-case exponential complexity in the formula length. \textcite[178]{rosu2005rewriting} claim that this exponential complexity is only of theoretical importance rather than practical, as most tested formula grow linearly.

A formal complexity analysis of TPTL based rewriting is desirable however, as I have not seen one. Before I implemented a simplification method that detected impossible time constraints, some timed formula (specifically of the form $\Box x. \varphi$) grow very quickly and were impractical to verify. After this simplification technique they became practical and only grew linearly.

% \section{Discussion}
\section{Future Work}
Since my implementation of the RV-TPTL runtime verification procedure is incomplete, my first step in any future work would be to correctly and completely implement \Cref{decision}. I will now describe some other interesting improvements.

\subsubsection{Finding Changes in Results}
It would be useful to be able to find the point at which a timed formula (or subformula) changes from one result to another. For example, suppose there is a timed formula and a trace $\rho$, with a time constraint that is not violated at $\rho_i$, but is violated at $\rho_{i+1}$. Also, let there be a time gap of at least 1, i.e., $\tau_i < \tau_{i+1} - 1$. Then it would be useful to diagnose where in that gap the time constraint is violated. One way to do this would be for the user to select some intermediate times to test, by giving a time $\tau_j$ with $\tau_i < \tau_j < \tau_{i+1}$. The verifier could test different states $\sigma_j$ and see where the violation occurs. Possible sensible imputations could be $\sigma_j := \sigma_i$ or $\sigma_j := \sigma_{i+1}$.

Another option would be to loop over all times between $\tau_i$ and $\tau_{i+1}$, to find the first possible violation. Similarly, these methods could be used if the formula is satisfied, presumably satisfied, presumably violated at $\rho_{i+1}$. This would be useful for both IE-TPTL and RV-TPTL verification to diagnose the exact point at which a decision can be made or changed.

Peter Baumgartner mentioned a preliminary version of these ideas to me, after reading \textcite{chai2014fivevalued}, which deals with the uncertainty produced by verifying concurrent systems.

A looping technique could be used at the end of an IE-TPTL trace so that one could diagnose at what time after the final state might the formula change from one result to another. But this performs very badly, as I found out with some simple tests. A better solution would be to simplify the formula at the final state to only contain time constraints, and then pass this to a quantifier elimination procedure to make a decision.

\subsubsection{Memoization}
\textcite[180]{rosu2005rewriting} developed a performance enhancement for their LTL rewriting algorithm called memoization. Using this method, the input formula-state combinations are hashed and mapped to their rewritten result. Each time the formula-state combination is seen again, the algorithm uses the cached result instead of rewriting using the algorithm. \citeauthor{rosu2005rewriting} found that this significantly improved performance in their system. This would not work as it is for TPTL, since the time is an important factor in the rewriting procedure, and most real-world traces would have a time which changes. Because of this, the algorithm would rarely see the same formula-time-state combination twice, rendering memoization useless.

However, there may be some variation of this method which could improve performance, perhaps by checking untimed subformula against a cache. There may also be some smart algorithm for dealing with the timed portion of formulae, but I have not thought of one. It would be useful to investigate this method for performance improvements in TPTL rewriting algorithms.

\subsubsection{Alternative verification algorithms}
Other verification algorithms have been devised for verification of various LTL based logics. \textcite{rosu2005rewriting} developed a generalisation of Binary Decision Diagrams, called Binary Transition Trees (BTTs), which is an optimised automata-based algorithm for LTL runtime verification. \textcite{bauer2010comparing} propose a runtime verification algorithm for RV-LTL based on the product automata of monitors for \ltlt\ and FLTL. \textcite{alur1994really} present a tableau based procedure for model checking of TPTL properties.
Some derivative or combination of these procedures would be useful in producing more performant verification procedures for IE-TPTL and RV-TPTL.


\section{Conclusion}
In this report, I have given a limited survey of temporal logics for runtime verification and presented my own four-valued logic RV-TPTL. I have discussed formula rewriting algorithms and given a formula rewriting based decision procedure for RV-TPTL runtime verification. I have described some of the interesting aspects of my (incomplete) implementation. I conclude that RV-TPTL is a viable and potentially useful logic for use in runtime verification.

\subsubsection{Acknowledgements}
I would like to thank Peter Baumgartner for supervising me and Myvanwy Williamson for reminding me to take breaks.

\nocite{*}
\printbibliography{}
\newpage
\section{Appendix}\label{appendix}
\subsection{Full Definitions}\label{fulldef}
\mdfsetup{nobreak=true}
These are expanded definitions which were only partially given in the main text.

\begin{defn}[IE-LTL semantics]\label{ieltlsemfull}

  %Let $\sigma_f$ be the final state of the trace.
  Define the satisfaction relation for IE-LTL $\vDash_{\text{IE-LTL}}$ as follows.
  Let $P$ be a set of propositional variables and $\sigma$ a trace.
  \begin{align*}
    \sigma &\vDash a \tiff a \in \sigma_0\\
    \sigma &\nvDash \bot\\
    \sigma &\vDash \neg \varphi \tiff \sigma \nvDash \varphi\\
    \sigma &\vDash \varphi \lor \psi \tiff \sigma \vDash \varphi \tor \sigma \vDash \psi\\
    \sigma &\vDash \varphi \land \psi \tiff \sigma \vDash \varphi \tand \sigma \vDash \psi\\
    \sigma &\vDash \bigcirc \varphi =
    \begin{cases}
      \top &\text{if } \sigma^1 \vDash \varphi \tand \sigma^1 \ne \epsilon\\
      \top &\text{if } \sigma \vDash \varphi \tand \sigma^1 = \epsilon\\
      \bot &\text{otherwise}
    \end{cases}\\
    \sigma &\vDash \varphi \U \psi =
    \begin{cases}
      \top &\text{if } \sigma^i \vDash \psi \fsome i > 0 \tand \sigma^j \vDash \varphi \fall 0 \leq j < i\\
      \top &\text{if } \sigma \vDash \psi \tand \sigma^1 = \epsilon\\
      \bot &\text{otherwise}
    \end{cases}
  \end{align*}
  Original was \Cref{ieltlsem}
\end{defn}

\begin{defn}[FLTL semantics]\label{fltlsemfull}

  Define the satisfaction relation for FLTL $\vDash_{\text{FLTL}}$ as follows.
  \begin{align*}
    \sigma &\vDash a \tiff a \in \sigma_0\\
    \sigma &\nvDash \bot\\
    \sigma &\vDash \neg \varphi \tiff \sigma \nvDash \varphi\\
    \sigma &\vDash \varphi \lor \psi \tiff \sigma \vDash \varphi \tor \sigma \vDash \psi\\
    \sigma &\vDash \varphi \land \psi \tiff \sigma \vDash \varphi \tand \sigma \vDash \psi\\
    \sigma&\vDash\sn\varphi \tiff \sigma^1\vDash\varphi \tand \sigma^1 \neq \epsilon\\
    \sigma&\vDash\wn\varphi \tiff \sigma^1\vDash\varphi \tor \sigma^1 = \epsilon\\
    \sigma &\vDash \varphi \U \psi \tiff \sigma^i \vDash \psi \fsome i \geq 0 \tand \sigma^j \vDash \varphi \fall 0 \leq j < i
  \end{align*}
  Original was \Cref{fltlsem}
\end{defn}
% \begin{defn}{\ltlt\ semantics}\label{ltltsemfull}

%   The notation $\sigma\gamma$ refers to the concatenation of the infinite trace $\gamma$ to the finite trace $\sigma$.
%   Define the satisfaction relation for \ltlt $\vDash_{\text{\ltlt}}$ as follows.
%   \[\sigma\vDash_{\text{\ltlt}}\varphi =
%     \begin{cases}
%       \top & \text{if } \sigma\gamma \vDash{\text{LTL}} \varphi \fall \gamma \in P^+\\
%       \bot & \text{if } \sigma\gamma \vDash{\text{LTL}} \varphi \fall \gamma \in P^+\\
%       ? & \text{otherwise}
%     \end{cases}
%     \]
%   Original was \Cref{ltltsem}.
% \end{defn}

\begin{defn}[TPTL Semantics]\label{tptlsemfull}

  Let $\rho = (\sigma,\tau)$ be a timed trace, $x\in V$, $c\in\mathbb{N}$, and let $\eval:V\to\mathbb{N}$ be an (initially empty) evaluation of time variables to times, with $\eval(x + c) = \eval(x) + c$, $\eval(c) = c$ and $\eval[x:=c]$ denoting the evaluation which agrees with $\eval$ for $V\setminus\{x\}$ and maps $x$ to $c$.

  \begin{align*}
    \rho,\eval&\vDash a \tiff a \in \rho_0\\
    \rho,\eval&\nvDash \bot\\
    \rho,\eval&\vDash \neg \varphi \tiff \rho,\eval \nvDash \varphi\\
    \rho,\eval&\vDash \varphi \lor \psi \tiff \rho,\eval \vDash \varphi \tor \rho,\eval \vDash \psi\\
    \rho,\eval&\vDash \varphi \land \psi \tiff \rho,\eval \vDash \varphi \tand \rho,\eval \vDash \psi\\
    \rho,\eval&\vDash \bigcirc \varphi \tiff \rho^1 \vDash \varphi\\
    \rho,\eval&\vDash \varphi \U \psi \tiff \rho^i,\eval \vDash \psi \fsome i \geq 0 \tand \rho^j,\eval \vDash \varphi \fall 0 \leq j < i\\
    \rho,\eval &\vDash_{\text{TPTL}}\pi_1\leq\pi_2 \tiff \eval(\pi_1)\leq\eval(\pi_2)\\
    \rho,\eval &\vDash_{\text{TPTL}} x.\varphi \tiff \rho,\eval[x:=\tau_0]\vDash\varphi
  \end{align*}
  Original was \Cref{tptlsem}
\end{defn}

\begin{defn}[IE-TPTL semantics]\label{ietptlsemfull}

  Define the semantic relation $\vDash_{\text{IE-TPTL}}$ of IE-TPTL as follows. Copy the semantics from the TPTL semantics (\Cref{tptlsem}), and redefine the `next' $\bigcirc$ and `until' $\U$ operators as follows:
  \begin{align*}
    \rho,\eval&\vDash a \tiff a \in \rho_0\\
    \rho,\eval &\vDash \pi_1\leq\pi_2 \tiff \eval(\pi_1)\leq\eval(\pi_2)\\
    \rho,\eval&\nvDash \bot\\
    \rho,\eval&\vDash \neg \varphi \tiff \rho,\eval \nvDash \varphi\\
    \rho,\eval&\vDash \varphi \lor \psi \tiff \rho,\eval \vDash \varphi \tor \rho,\eval \vDash \psi\\
    \rho,\eval&\vDash \varphi \land \psi \tiff \rho,\eval \vDash \varphi \tand \rho,\eval \vDash \psi\\
    \rho,\eval&\vDash \bigcirc \varphi =
    \begin{cases}
      \top &\text{if } \rho^1,\eval \vDash \varphi \tand \rho^1 \ne \epsilon\\
      \top &\text{if } \rho,\eval\vDash \varphi \tand \rho^1 = \epsilon\\
      \bot &\text{otherwise}
    \end{cases}\\
    \rho,\eval&\vDash \varphi \U \psi =
    \begin{cases}
      \top &\text{if } \rho^i,\eval \vDash \psi \fsome i > 0 \tand \rho^j,\eval \vDash \varphi \fall 0 \leq j < i\\
      \top &\text{if } \rho,\eval\vDash \psi \tand \rho^1 = \epsilon\\
      \bot &\text{otherwise}
    \end{cases}\\
    \rho,\eval &\vDash x.\varphi \tiff \rho,\eval[x:=\tau_0]\vDash\varphi
      \end{align*}
  Original was \Cref{ietptlsem}
\end{defn}



% \newpage
% \subsection{List of Definitions}
% \listoftheorems[ignoreall,show={defn}]
\newpage
\subsection{Authorship Declarations}
The formula rewriting functions in the \texttt{progress} object were originally written by my supervisor Peter Baumgartner as a formula progression calculator for another project. I have modified them to suit my project, but they are substantially similar. There were other functions in \texttt{progress} which I removed.

The original structure of the \texttt{Formula} classes was taken from Peter's work but substantially modified. The main remnants are some of the names of classes, some variable declarations and the \texttt{compl} method of \texttt{Formula}.

The \texttt{package} object is mostly Peter's work.

The \texttt{verifier} object is entirely my work.

\end{document}