mirror of
https://github.com/janishutz/eth-summaries.git
synced 2026-09-10 19:15:25 +02:00
53 lines
3.6 KiB
TeX
53 lines
3.6 KiB
TeX
\newpage
|
|
\subsubsection{Linear Time Properties (LTL)}
|
|
\begin{examdetails}
|
|
Has appeared in most exams over the last 10 years.
|
|
Typically a task where you provide an LTL formula, one where you show correctness / counterexamples for one and one on Liveness/Safety Properties
|
|
\end{examdetails}
|
|
We refer to Section~\ref{sec:ltl} for intuition, as these tend to mostly be intuition exercises.
|
|
|
|
For doing verification of liveness / safety properties using \texttt{spin} and Promela,
|
|
the operators are translated to Promela as follows:
|
|
\verb+[] <> ! && || -> U+ for $\square \Diamond \neg \land \lor \Rightarrow U$, respectively.
|
|
In addition, we have the equality operator as a primitive propositional formula. We have \texttt{p == true} for $p$ in the operators.
|
|
|
|
Execute \texttt{spin -a file.pml}, followed by \texttt{gcc pan.c} and \texttt{./a.out}.
|
|
|
|
As a reminder, these are the operators (details in Section~\ref{sec:ltl-details}):
|
|
\begin{itemize}
|
|
\item Now: $p$ states that the proposition is true ``\textit{now}''
|
|
\item Holds until: $\Phi U \Psi$ states that $\Phi$ holds (with no other valid proposition holding between) until $\Psi$ holds.
|
|
\item Next: $\bigcirc \Phi$ states that $\Phi$ holds for the ``next'' (if nothing else specified from start state)
|
|
\item Eventually: $\Diamond \Phi$ states that $\Phi$ holds \textit{eventually}, $\Diamond \Phi \equiv (\texttt{true} U \Phi)$
|
|
\item Always (from now on): $\square \Phi$ states that from now on, $\Phi$ will always hold, $\square \Phi \equiv \neg \Diamond \neg \Phi$
|
|
\end{itemize}
|
|
For the implication (where the left hand side is called the \textit{antecedent}, right hand side is called the \textit{consequent}),
|
|
remember to show the case where the antecedent is true and state that for antecedent false, it is trivially true
|
|
|
|
|
|
\paragraph{Tips and tricks}
|
|
\begin{itemize}
|
|
\item You can't just write $\Diamond \neg s_1$, where $s_1$ is a state,
|
|
you need to specify the propositions (as a set, such as $\{ A, B \}$ instead of the $s_1$.
|
|
\item We can also create statements, such as never as $\square \neg \Phi$ (always not $\Phi$), etc.
|
|
\item Often, an \texttt{if} in the description means we should use a $\Rightarrow$.
|
|
\item A typical task is ``something will do something (denoted $A$ here) $N$ times'' ($N$ in that case known an low),
|
|
an LTL formula in the $N = 2$ case is then $\Diamond (A \land \bigcirc \Diamond A)$.
|
|
Note that $\Diamond (A \land \Diamond A)$ is \bi{NOT} correct (because that is true also for $A$ happening only once).
|
|
\item If property $A$ has to be true infinitely many times, the LTL formula is $\square \Diamond A$
|
|
\item Be careful with parenthesis (e.g. with $\neg$)!
|
|
\end{itemize}
|
|
|
|
|
|
\paragraph{Liveness and Safety Properties}
|
|
Proofs here run using the definitions directly, either by showing a counter example (for disproving) or showing that, in fact, the definition holds.
|
|
Indirect proofs may also come in handy, because it is typically easier to show that something is not a safety property (or liveness property) than to show that it is.
|
|
|
|
These two properties are \textit{mutually exclusive} (with one exception, \texttt{true}), to the extent that an LTL formula can't be both at the same time, but be a conjunct of both.
|
|
In fact, every LTL formula is a either one of the two, or a conjunct of both.
|
|
|
|
Finally, as a reminder, an LTL formula is for example $\square \Diamond A$, with $A$ an atomic proposition.
|
|
|
|
Having an eventually in the formula fairly early on \textit{can} be an indicator that it is a liveness property,
|
|
an always in the same positions \textit{can} indicate a safety property.
|