6/21
\begin{frame}
\frametitle{Where is Modal Logic Applied?}

\begin{goal}{}
Variants of modal logic used in industry:
\begin{itemize}
\item linear time logic,
\item computational tree logic,
\item $\mu$-calculus.
\end{itemize}
\end{goal}
\pause
\medskip

\begin{exampleblock}{}
They typically have more modalities. For example
\begin{talign}
G \phi \quad&\riff\quad \text{in all reachable worlds $\phi$ is true} \\
F \phi \quad&\riff\quad \text{in some reachable world $\phi$ is true}
\end{talign}
\end{exampleblock}
\pause
\medskip

\begin{goal}{}
You can then formulate properties like:
\begin{itemize}
\item There always is a path to successful termination.
\item Never two processes are in the same critical section.\\
(Needed in case of shared resources.)
\end{itemize}
\end{goal}
\end{frame}