101 lines
No EOL
4.2 KiB
TeX
101 lines
No EOL
4.2 KiB
TeX
\documentclass[99-notes-packed.tex]{subfiles}
|
|
|
|
\begin{document}
|
|
\paragraph*{LTL}
|
|
Let $\phi, \psi$ be LTL expressions, $p \in AP$ an atomic predicate, $\rightarrow^\ast$ indicating 0 or more steps (like regex):
|
|
\begin{align*}
|
|
\phi, \psi \Coloneqq&\ p\ |\ \top\ |\ \bot\ |\ \phi \wedge \psi\ |\ \phi \vee \psi\ |\ \neg \phi\ |\ \phi \implies \psi \\
|
|
|&\ X \phi:
|
|
\pi \models X \phi \iff
|
|
\exists {\pi}^{'}: \pi \rightarrow {\pi}^{'} \models \phi \\
|
|
|&\ F \phi:
|
|
\pi \models F \phi \iff
|
|
\exists {\pi}^{'}: \pi \rightarrow^\ast {\pi}^{'} \models \phi \\
|
|
|&\ G \phi:
|
|
\pi \models G \phi \iff
|
|
\forall {\pi}^{'}: (\pi \rightarrow^\ast {\pi}^{'}) \implies ({\pi}^{'} \models \phi) \\
|
|
|&\ \phi U \psi: \pi_0 \models \phi U \psi \\
|
|
& \iff \exists \pi_0 \rightarrow^\ast P \models \psi: \forall \pi_i \in \pi_0 \rightarrow^\ast \pi_N \rightarrow \Pi: \pi_i \models \phi \\
|
|
|&\ \phi W \psi:
|
|
\pi \models \phi W \psi \iff \pi \models (\phi U \psi) \vee (G \phi)
|
|
\end{align*}
|
|
|
|
\paragraph*{CTL}
|
|
Orthogonally (in terms of expressibility), CTL prefixes all $X | F | G | U$ operators with temporal signifiers:
|
|
\begin{align*}
|
|
A \sim \forall&:\ \textrm{for all paths} \\
|
|
E \sim \exists&:\ \textrm{exists some path}
|
|
\end{align*}
|
|
|
|
\begin{example}[incomparability of CTL, LTL]
|
|
No LTL equivalent exists for CTL formula $AG(EF a)$. Likewise, no CTL equivalent exists for LTL formula $F(G a)$.
|
|
\end{example}
|
|
|
|
\paragraph*{Kripke Structure} is an alternative means of representing a transition system. Let $AP$ be a set of atomic predicates. A Kripke structure over $AP$ is a tuple $(S, \rightarrowtriangle, \models)$ where:
|
|
\begin{itemize}
|
|
\item $S$: set of state.
|
|
\item $\rightarrowtriangle \subseteq S \times S$: transition relation.
|
|
\item $\models \subseteq S \times AP$: state-predicate mapping.
|
|
\end{itemize}
|
|
|
|
LTL and CTL operate upon Kripke structures.
|
|
|
|
A state $s \models \phi$ if for all paths incident from $s$, each path satisfies $\phi$.
|
|
|
|
\paragraph*{LTS-Kripke Translation}
|
|
A translation system $\eta$ maps states in LTSs to states in Kripke structures. This allows us to perform LTL/CTL validation on LTS:
|
|
\begin{equation*}
|
|
P \models_{\eta} \phi \iff \eta(P) \models \phi
|
|
\end{equation*}
|
|
|
|
\begin{definition}[De Nicola-Vaandrager Translation]
|
|
The \textbf{DV-translation} translates process graphs into Kripke structures. Let the process graph be defineed as $(S, I, \rightarrowtriangle)$, as was the case for LTS.
|
|
|
|
The associated Kripke structure is $((S^{'}, I), \rightarrowtriangle^{'}, \models)$, where:
|
|
\begin{align*}
|
|
S^{'} \coloneqq& S \cup \{[s, a, t] \in \rightarrowtriangle | a \ne \tau\} \\
|
|
\rightarrowtriangle^{'} \coloneqq&
|
|
\{(s, [s, a, t]), ([s, a, t], t) | [s, a, t] \in S^{'}\} \\
|
|
\cup& \{(s, t) | (s, \tau, t) \in \rightarrowtriangle \}
|
|
\end{align*}
|
|
|
|
In short, we create new states out of transitions due to visible actions, and create linkages accordingly.
|
|
\end{definition}
|
|
|
|
\begin{theorem}
|
|
Processes $P, Q$ satisfy the same LTL formulas if:
|
|
\begin{equation*}
|
|
P =_{CT}^{\infty} Q
|
|
\end{equation*}
|
|
Moreover, finitely-branching processes $P, Q$ satisfies \textbf{iff}.
|
|
\end{theorem}
|
|
|
|
\begin{theorem}
|
|
Processes $P, Q$ satisfy the same $LTL_{-X}$ formulas (i.e., LTL without $X$) if:
|
|
\begin{equation*}
|
|
P =_{WCT}^{\infty} Q
|
|
\end{equation*}
|
|
\end{theorem}
|
|
|
|
\begin{theorem}
|
|
Processes $P, Q$ satisfy the same CTL formulas if:
|
|
\begin{equation*}
|
|
P =_{B} Q
|
|
\end{equation*}
|
|
Moreover, finitely-branching processes satisfies \textbf{iff}.
|
|
|
|
On the otherhand, when CTL is expanded to $CTL^{\infty}$ (i.e., CTL with infinite $\wedge$), all processes also satisfy \textbf{iff}.
|
|
\end{theorem}
|
|
|
|
\begin{theorem}
|
|
A \textbf{divergence-free} process is one where no reachable state $p$ has $p \xrightarrow{\tau^\infty} !$ -- infinite $\tau$s.
|
|
|
|
Two \textbf{divergence-free} processes $P, Q$ satisfy the same ${CTL}_{-X}$ formulas if:
|
|
\begin{equation*}
|
|
P =_{BB} Q
|
|
\end{equation*}
|
|
|
|
Moreover, when CTL is adjusted to ${CTL}^{\infty}_{-X}$, we have \textbf{iff}. Same goes if $P, Q$ are additionall finitely branching.
|
|
\end{theorem}
|
|
|
|
\end{document} |