\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}