extensions.tex

\section{Second-order quantification}

Following the corpus of results on counterpart relations as models for monodic second-order modal logics, we can
straightforwardly define a syntax for Monadic \ac{SOLTL}, with membership as the sole operator beside the temporal and
propositional ones.

\begin{definition}[Second-Order Linear Temporal Logic]
Let $\Sigma$ be a (multi-sorted) signature and $X$ a denumerable set of first-order variables typed over $S_\Sigma$, and
$\mathcal{X}$ a denumerable set of second-order variables typed over $S_\Sigma$. The set $\mathcal{F}_\Sigma$ of
formulae for Monodic \ac{SOLTL} is the set generated by the following grammar:
\[
  \phi \Coloneqq tt \;|\; \epsilon_\tau \in \chi_\tau
                    \;|\; \neg\phi
                    \;|\; \phi \lor \phi
                    \;|\; \existss{x_\tau}{\phi}
                    \;|\; \existss{\chi_\tau}{\phi}
                    \;|\; \nextop{\phi}
                    \;|\; \until{\phi}{\phi}
\]
where $\epsilon \in \terms{\Sigma}{X}$, $\exists x_\tau$ ranges over first-order variables of sort $\tau \in S_\Sigma$,
$\exists \chi_\tau$ ranges over second-order variables of sort $\tau \in S_\Sigma$,
$O$ is a unary operator which states that $\phi$ must hold at the next step and $U$ is a binary operator which states
that the first formula must hold until the second formula holds at some point in the current or next steps.
\end{definition}

Other operators are derived the same as for \ac{FOLTL}, with the addition of equality, which in
this case becomes itself a derived operator, $\epsilon_\tau = \eta_\tau \equiv \foralls{\chi_\tau}(\epsilon_\tau \in
\chi_\tau \leftrightarrow \eta_\tau \in \chi_\tau)$.

To define a semantic with counterpart relations for the Monodic \ac{SOLTL} we need to extend some concept to the
second-order. First we need a new context, a second-order context, which is a subset of second-order variables, i.e.
$\Delta \subseteq \mathcal{X}$. Second, given a counterpart model $M = (W, \rightsquigarrow, d)$ and a world $w \in W$,
we require a second-order assignment $\xi$, i.e $\xi$ is a partial function such that $\xi : \mathcal{X} \rightharpoonup
2^{d(w)}$, which intuitively assigns a set of values in the domain $d(w)$ to each second-order variable.

\begin{definition}[Semantic of \ac{SOLTL}]
Let $M$ be a counterpart model, $\Gamma$ and $\Delta$ respectively a first-order and second-order context, $\pi = w_0
\overset{cr_0}{\rightsquigarrow} w_1 \overset{cr_1}{\rightsquigarrow} \ldots$ a sequence of accessible arrows,
$\sigma$ and $\xi$ respectively a first-order assignment and a second-order assignment for the world $w_0$:
The validity of a formula-in-context $\phi$, denoted $\semtwo{\sigma}{\xi}{w}{\Gamma}{\Delta}{\phi}$, is defined
inductively as follows:
\begin{align*}
  \pi, \sigma, \xi &\vDash_\Gamma^\Delta tt \\
  \pi, \sigma, \xi &\vDash_\Gamma^\Delta \epsilon_\tau \in \chi_\tau
      &&\text{iff } \sigma(\epsilon) \text{ defined and } \sigma(\epsilon) \in \xi(\chi) \\
  \pi, \sigma, \xi &\vDash_\Gamma^\Delta \neg\phi
      &&\text{iff } \semntwo{\pi}{\sigma}{\xi}{\Gamma}{\Delta}{\phi} \\
  \pi, \sigma, \xi &\vDash_\Gamma^\Delta \phi_1 \lor \phi_2
      &&\text{iff } \semtwo{\pi}{\sigma}{\xi}{\Gamma}{\Delta}{\phi_1} \text{ or }
      \semtwo{\pi}{\sigma}{\xi}{\Gamma}{\Delta}{\phi_2} \\
  \pi, \sigma, \xi &\vDash_\Gamma^\Delta \existss{x_\tau}{\phi}
      &&\text{iff } \existss{v \in d(w_0)}{\semtwo{\pi}{\ext{x}{\sigma}{v}}{\xi}{\Gamma, x}{\Delta}{\phi}} \text{ with }
      x \not\in \Gamma \\
  \pi, \sigma, \xi &\vDash_\Gamma^\Delta \existss{\chi_\tau}{\phi}
      &&\text{iff } \existss{v \in 2^{d(w_0)}}{\semtwo{\pi}{\sigma}{\ext{\chi}{\xi}{v}}{\Gamma}{\Delta,\chi}{\phi}}
        \text{ with } \xi \not\in \Delta \\
  \pi, \sigma, \xi &\vDash_\Gamma^\Delta \nextop{\phi}
      &&\text{iff } \semtwo{\suffix(\pi,1)}{cr_0 \circ \sigma}{2^{cr_0} \circ \xi}{\Gamma}{\Delta}{\phi} \\
  \pi, \sigma, \xi &\vDash_\Gamma^\Delta \until{\phi_1}{\phi_2}
     &&\text{iff } \semtwo{\pi}{\sigma}{\xi}{\Gamma}{\Delta}{\phi_2} \text{ or } (\semtwo{\pi}{\sigma}{\xi}{\Gamma}{\Delta}{\phi_1} \\
         &&&\qquad\text { and } \semtwo{\suffix(\pi,1)}{cr_0 \circ \sigma}{2^{cr_0} \circ \xi}{\Gamma}{\Delta}{\until{\phi_1}{\phi_2}}) \\
\end{align*}
  where $2^{cr}$ is the lifting of the partial function $cr$ to the power-set of the image, and $\extend$ defined as
  in~\Cref{def:fosemantic}.
\end{definition}

\section{Branching time}
A further axis of extension is to expand the logic to a branching time logic, thus by introducing operators that
quantify over the set of possible traces instead of a single one. The logic that requires every temporal operator to be
prefixed by a path quantifier is called \ac{CTL}. The path quantifiers are: all, $\forallpath{\phi}$,
which holds if $\phi$ holds on all traces starting from the current world, and exists, $\existpath{\phi}$ which holds if
there exists at least one trace starting from the current world where $\phi$ holds.

Here we introduce the syntax and semantic for a quantified version of \ac{CTL}~\cite{hodkinson_decidable_2002}.

\begin{align*}
  \phi &\Coloneqq tt \;|\; \epsilon_\tau = \epsilon_\tau
                    \;|\; \neg\phi
                    \;|\; \phi \lor \phi
                    \;|\; \existss{x_\tau}{\phi}
                    \;|\; \existpath{\psi}
                    \;|\; \forallpath{\psi} \\
  \psi &\Coloneqq \nextop{\phi} \;|\; \until{\phi}{\phi}
\end{align*}

Semantically, a single trace, i.e. a chain $\pi$, is a sequence of worlds related by the accessibility relation, however
the given a world $w$ there could be more than one world $w'$ such that $\worldcr{w}{cr}{w'}$. By chosing a specific
accesible world whenever we have one or more choices we are effectively building a tree, thus the name of \ac{CTL},
where each infinite descending path from the starting world is a trace as we defined for the semantics of \ac{LTL}. The
path quantifiers are thus the equivalent of quantifiers forall and exists of \ac{FOL} but for the subset of paths
starting from the current world.

\begin{align*}
  \pi, \sigma &\vDash_\Gamma tt \\
  \pi, \sigma &\vDash_\Gamma \epsilon_\tau = \eta_\tau &&\text{iff } \sigma(\epsilon) = \sigma(\eta) \\
  \pi, \sigma &\vDash_\Gamma \neg\phi &&\text{iff } \semn{\pi}{\sigma}{\Gamma}{\phi} \\
  \pi, \sigma &\vDash_\Gamma \phi_1 \lor \phi_2
      &&\text{iff } \sem{\pi}{\sigma}{\Gamma}{\phi_1} \text{ or } \sem{\pi}{\sigma}{\Gamma}{\phi_2} \\
  \pi, \sigma &\vDash_\Gamma \existss{x_\tau}{\phi}
      &&\text{iff } \existss{v \in d(w_0)}{\sem{\pi}{\extend_x(\sigma, v)}{\Gamma, x}{\phi}}
        \text{ with } x \not\in \Gamma \\
  \pi, \sigma &\vDash_\Gamma \nextop{\phi}
      &&\text{iff } \sem{\suffix(\pi, 1)}{cr_0 \circ \sigma}{\Gamma}{\phi} \\
  \pi, \sigma &\vDash_\Gamma \until{\phi_1}{\phi_2}
      &&\text{iff } \sem{\pi}{\sigma}{\Gamma}{\phi_2} \\ &&&\quad\text{ or } (\sem{\pi}{\sigma}{\Gamma}{\phi_1}
        \text { and } \sem{\suffix(\pi, 1)}{cr_0 \circ \sigma}{\Gamma}{\until{\phi_1}{\phi_2}}) \\
  \pi, \sigma &\vDash_\Gamma \existpath{\phi}
      &&\text{iff } \existss{\pi' \in \paths(\pi_0)}{\sem{\pi'}{\sigma}{\Gamma}{\phi}} \\
  \pi, \sigma &\vDash_\Gamma \forallpath{\phi}
      &&\text{iff } \foralls{\pi' \in \paths(\pi_0)}{\sem{\pi'}{\sigma}{\Gamma}{\phi}} \\
\end{align*}
Where $\extend$ is defined as in~\Cref{def:fosemantic}, and paths is the set of traces starting from the argument world,
$\paths(w) = \set{\pi | \pi = w \overset{cr_0}{\rightsquigarrow} w_1 \overset{cr_1}{\rightsquigarrow} \ldots}$.

Temporal operators that operate on single world are semantically identical to their \ac{LTL} variants. The path
operators instead quantify over the set of paths that start from the current world. Recall the formula evaluated in
\Cref{sec:execexample}, we identified the traces for which the formula holds, for example starting from the world $w_2$
in~\Cref{fig:exmemsignature}, the traces that have the world $w_3$ as next in the sequence are valid for the formula,
while the traces that have the world $w_4$ as next in the sequence do not. With \ac{LTL} is impossible to build a
formula that encodes this disparity or that requires that every possible future of the world $w_2$ has a change in
location. Instead we can simply encode the latter property in \ac{CTL} by prepending the temporal operator with a
universal path quantifier: $\existss{x_{\tau_o}}{\existss{l_{\tau_l}}{\rho(x) = l \land \forallpath{\nextop{(\rho(x)
\neq l)}}}}$.

Logically the next step would be investigating an axiomatic system for \ac{CTL} or extending the semantic to \ac{CTL}* a
superset of both \ac{LTL} and \ac{CTL}, where path quantifiers and temporal operators may appear freely in formulae.
Another approach is to add a probability measure to the transitions in the
counterpart model, thus adding a probability operator, as in \ac{PCTL}~\cite{brazdil_satisfiability_2008}.