~spidernet/RealTimeSystemsModels

b73c5e81b914d835407e60995e0132abcbcd8ad5 — Alessio Chiapperini 4 months ago
Add latex sources for report and slides
A  => .gitignore +9 -0
@@ 1,9 @@
*.aux
*.bbl
*.blg
*.log
*.out
*.toc
*.nav
*.snm
*.vrb

A  => report/Makefile +13 -0
@@ 1,13 @@
all: bib

.PHONY: clean

pdf:
	pdflatex report.tex

bib: pdf
	bibtex report.aux
	pdflatex report.tex

clean:
	rm -f *.bbl *.blg *.idx *.lof *.log *.out *.pdf *.aux

A  => report/biblio.bib +93 -0
@@ 1,93 @@
  title={{CCS} + time = an interleaving model for real time systems},
  author={Yi, Wang},
  booktitle={International Colloquium on Automata, Languages, and Programming},
  pages={217--228},
  year={1991},
  organization={Springer}
}

  title={Communication and concurrency},
  author={Milner, Robin},
  volume={84},
  year={1989},
  publisher={Prentice hall New York etc.}
}

@phdthesis{alur1991techniques,
  title={Techniques for automatic verification of real-time systems},
  author={Alur, Rajeev},
  year={1991},
  school={stanford university}
}

@article{alur1994theory,
  title={A theory of timed automata},
  author={Alur, Rajeev and Dill, David L},
  journal={Theoretical computer science},
  volume={126},
  number={2},
  pages={183--235},
  year={1994},
  publisher={Elsevier}
}

@article{larsen1997uppaal,
  title={UPPAAL in a nutshell},
  author={Larsen, Kim G and Pettersson, Paul and Yi, Wang},
  journal={International Journal on Software Tools for Technology Transfer (STTT)},
  volume={1},
  number={1},
  pages={134--152},
  year={1997},
  publisher={Springer}
}

@inproceedings{bozga1998kronos,
  title={Kronos: A model-checking tool for real-time systems},
  author={Bozga, Marius and Daws, Conrado and Maler, Oded and Olivero, Alfredo and Tripakis, Stavros and Yovine,
      Sergio},
  booktitle={International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems},
  pages={298--302},
  year={1998},
  organization={Springer}
}

@inproceedings{daws1995tool,
  title={The tool KRONOS},
  author={Daws, Conrado and Olivero, Alfredo and Tripakis, Stavros and Yovine, Sergio},
  booktitle={International Hybrid Systems Workshop},
  pages={208--219},
  year={1995},
  organization={Springer}
}

@inproceedings{laroussinie1995timed,
  title={From timed automata to logic—and back},
  author={Laroussinie, Fran{\c{c}}ois and Larsen, Kim G and Weise, Carsten},
  booktitle={International Symposium on Mathematical Foundations of Computer Science},
  pages={529--539},
  year={1995},
  organization={Springer}
}

@article{aceto2002your,
  title={Is your model checker on time? On the complexity of model checking for timed modal logics},
  author={Aceto, Luca and Laroussinie, Fran{\c{c}}ois},
  journal={The Journal of Logic and Algebraic Programming},
  volume={52},
  pages={7--51},
  year={2002},
  publisher={Elsevier}
}

@article{hennessy1985algebraic,
  title={Algebraic laws for nondeterminism and concurrency},
  author={Hennessy, Matthew and Milner, Robin},
  journal={Journal of the ACM (JACM)},
  volume={32},
  number={1},
  pages={137--161},
  year={1985},
  publisher={ACM}
}


A  => report/report.pdf +0 -0

A  => report/report.tex +1055 -0
@@ 1,1055 @@
% vim: ts=2:sw=2
\documentclass[11pt]{article}

\usepackage[italian,english]{babel}
\usepackage{hyperref}
\usepackage{url}
\usepackage{amssymb,amsmath,amsfonts,amsthm,mathtools}
\usepackage{stmaryrd}
\usepackage{listings}
\usepackage{tikz}
\usetikzlibrary{shapes,shapes.geometric,arrows,fit,calc,positioning,automata,}
\usepackage{pgfplots}
\usepackage{pgfplotstable}
\usepackage{lmodern}
\usepackage[utf8]{inputenc}
\usepackage[nottoc]{tocbibind}
\usepackage{numprint}
\usepackage[labelfont=bf]{caption}
\usepackage{float}
\usepackage{adjustbox}
\usepackage{nicefrac}
\usepackage[bottom]{footmisc}
\usepackage{bussproofs}
\usepackage{graphicx}
\usepackage{verbatim}
\usepackage{tabu}
\npthousandsep{\,}

\usepackage[sc]{mathpazo}
\linespread{1.05}
\usepackage[T1]{fontenc}

\newcommand{\R}{\mathbb{R}}
\newcommand{\N}{\mathbb{N}}
\newcommand\eqdef{\stackrel{\text{def}}{=}}
\newcommand\eqmin{\stackrel{\text{min}}{=}}
\newcommand\eqmax{\stackrel{\text{max}}{=}}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{corollary}{Corollary}[theorem]
\newtheorem{lemma}[theorem]{Lemma}
\theoremstyle{definition}
\newtheorem{definition}{Definition}[section]
\newtheorem{example}{Example}[section]

\makeatletter

\makeatletter %% <- make @ usable in command names
\newcommand*\Neg[2][0mu]{\Neginternal{#1}{\negslash}{#2}}
\newcommand*\sNeg[2][0mu]{\Neginternal{#1}{\snegslash}{#2}}
\newcommand*\ssNeg[2][0mu]{\Neginternal{#1}{\ssnegslash}{#2}}
\newcommand*\sssNeg[2][0mu]{\Neginternal{#1}{\sssnegslash}{#2}}
\newcommand*\Neginternal[3]{\mathpalette\Neg@{{#1}{#2}{#3}}}
\newcommand*\Neg@[2]{\Neg@@{#1}#2}
\newcommand*\Neg@@[4]{%
  \mathrel{\ooalign{%
    $\m@th#1#4$\cr
    \hidewidth$\m@th#3{#1}\mkern\muexpr#2*2$\hidewidth\cr
  }}%
}

\newcommand*\negslash[1]{\m@th#1\not\mathrel{\phantom{=}}}
\newcommand*\snegslash[1]{\rotatebox[origin=c]{60}{$\m@th#1-$}}
\newcommand*\ssnegslash[1]{\rotatebox[origin=c]{60}{$\m@th#1{\dabar@}\mkern-7mu{\dabar@}$}}
\newcommand*\sssnegslash[1]{\rotatebox[origin=c]{60}{$\m@th#1\dabar@$}}

\newcommand{\fixed@sra}{$\vrule height 2\fontdimen22\textfont2 width 0pt\leftrightarrow$}
\newcommand{\shortarrow}[1]{%
    \mathrel{\text{\rotatebox[origin=c]{\numexpr#1*45}{\fixed@sra}}}
}

\newenvironment{myfont}{\fontfamily{qhv}\selectfont}{\par}
\DeclareTextFontCommand{\chfont}{\myfont}

\begin{document}
\title{Models for real-time systems: timed automata and THML}
\author{Alessio Chiapperini (119697)}
\maketitle
% \tableofcontents
% \newpage

\section{Introduction}
A \emph{real-time system} is a system whose correct behaviour depends not only on the logical order in which events are
performed but also on their timing. In order to model the behaviour of real-time systems we will introduce two
formalism, namely the notion of timed automata introduced by Aldur and Dill~\cite{alur1991techniques, alur1994theory}
and the timed extension of the Hennessy-Milner logic~\cite{laroussinie1995timed}. Before doing that, in the next
section we will introduce some preliminary concepts.

\section{Preliminaries}
In this section we will introduce some useful concepts that will be used in later sections.
% \subsection{CCS}\label{sec:ccs}

\subsection{LTS and TLTS}
\subsubsection{Labelled Transitions Systems}
As is customary in the theory of concurrency, the semantics of a language or a logic is given in terms of automata,
also called \emph{labelled transition systems} (LTS). In this model processes are represented by vertices of certain
edge-labelled graphs and a change in process state caused by performing an action is understood as moving along an
edge, labelled by the action name, that goes out of that state. A LTS is formally defined as:

\begin{definition}
  A \emph{labelled transition system} (LTS), is a triple $(\chfont{Proc},\chfont{Act}, \{ \xrightarrow{\alpha} : \alpha
  \in \chfont{Act} \})$ where:
  \begin{itemize}
    \item \chfont{Proc} is a set of \emph{states} (or \emph{processes});
    \item \chfont{Act} is a set of \emph{actions} (or \emph{labels});
    \item $\xrightarrow{\alpha} \subseteq \chfont{Proc} \times \chfont{Proc}$ is a \emph{transition relation}, for
      every $\alpha \in \chfont{Act}$.
  \end{itemize}
  A labelled transition system is \emph{finite} if its sets of states and actions are both finite.
\end{definition}
\subsubsection{Timed Labelled Transitions Systems}
To give semantics to real-time systems we use a variation of a labelled transition system, in which we describe the
passage of time by adding special 'delay' transitions to the model. The resulting structure is a timed version of the 
model of LTSs.
\definition{} A \emph{timed labelled transition system}, also known as timed transition system is a triple
\begin{equation*}
  (\text{\chfont{Proc}}, \text{\chfont{Lab}}, \{\xrightarrow{~\alpha~}~: \alpha \in \text{\chfont{Lab}} \})
\end{equation*}
Where
\begin{itemize}
  \item \chfont{Proc} is a set of \emph{states} or processes;
  \item $\text{\chfont{Lab}} = \text{\chfont{Act}} \cup \R_{\geq 0}$ is a set of \emph{labels} consisting of \emph{actions} and
    \emph{time delays};
  \item $\xrightarrow{~\alpha~} \subseteq \text{\chfont{Proc}} \times \text{\chfont{Proc}}$, for each $\alpha \in \text{\chfont{Lab}}$, is a
    binary relation on states, called the \emph{transition relation}.
\end{itemize}
We write
\begin{align*}
  &s \xrightarrow{~a~} s' \text{ if } a \in \text{\chfont{Act} and } (s,s') \in \xrightarrow{~a~} \text{, and}\\
  &s \xrightarrow{~d~} s' \text{ if } d \in \R_{\geq 0} \text{ and } (s,s') \in \xrightarrow{~d~}.
\end{align*}
Transitions of the first type are ordinary transitions that are due to the performance of actions, while the second
type are time-elapsing transitions that describe how a system evolves as time passes. However these transitions don't
reflect our intuition of passage of time, in fact a TLTS must satisfy a so called \emph{time-additivity} requirement:
\begin{equation*}
  \text{if } s \xrightarrow{~d~}s' \text{ and } 0 \leq d' \leq d \text{ then } s \xrightarrow{~d'~} s''
  \xrightarrow{d-d'} s' \text{ for some state } s''
\end{equation*}
We can also say that $s \xrightarrow{~0~} s$ for every state $s$.\\
A final requirement that is imposed on TLTS is that delay transitions are \emph{deterministic}, i.e. for all $s,s',s''$
and for each $d \in \R_{\geq 0}$
\begin{equation*}
  \text{if } s \xrightarrow{~d~} s' \text{ and } s \xrightarrow{~d~} s'' \text{ then } s' = s''
\end{equation*}
This captures the way in which a system can evolve by just idling as time passes. From now on, we restrict to TLTSs
that satisfy these requirements.

\subsection{HML}
In what follows we will present a property language introduced by Hennessy and Milner in~\cite{hennessy1985algebraic}.
This logic is known as \emph{Hennessy-Milner logic} (HML).
\begin{definition}
The set $\mathcal{M}$ of \emph{Hennessy-Milner formulae} over a set of actions \chfont{Act} is given by the following
abstract syntax:
  \begin{equation*}
    F,G ::= \mathit{tt}~|~\mathit{ff}~|~F \land G~|~F \lor G~|~\langle a \rangle F~|~[a]F
  \end{equation*}
  Where $a \in \chfont{Act}$ and $\mathit{tt}$ and $\mathit{ff}$ are used to denote `true' and `false' respectively.
\end{definition}
Hennessy-Milner logic is a so-called multi-modal logic, since it involves modal operators that are parameterized by
actions.\\
The semantics of formulae is defined with respect to a given LTS 
\begin{equation*}
  (\chfont{Proc},\chfont{Act}, \{\xrightarrow{a} : a \in \chfont{Act} \}).
\end{equation*}
We use $\llbracket F \rrbracket$ to denote the set of processes in \chfont{Proc} that satisfies $F$. Now we define it formally.

\begin{definition}
  (Denotational semantics) We define $\llbracket F \rrbracket \subseteq \chfont{Proc}$ for $F \in \mathcal{M}$ by\\\\
  {\tabulinesep=1.5mm
  \setlength{\tabcolsep}{40pt}
  \begin{tabu}{l l}
    $\llbracket \mathit{tt} \rrbracket = \chfont{Proc}$
    &
    $\llbracket \mathit{ff} \rrbracket = \emptyset$\\
    $\llbracket F \land G \rrbracket = \llbracket F \rrbracket \cap \llbracket G \rrbracket$
    &
    $\llbracket F \lor G \rrbracket = \llbracket F \rrbracket \cup \llbracket G \rrbracket$\\
    $\llbracket \langle a \rangle F \rrbracket = \langle \cdot a \cdot \rangle \llbracket F \rrbracket$
    &
    $\llbracket [ a ] F \rrbracket = [ \cdot a \cdot ] \llbracket F \rrbracket$\\
  \end{tabu}
  }
  \\\\\\Where the operators $\langle \cdot a \cdot \rangle$, $[\cdot a \cdot] : 2^{\chfont{Proc}} \to
  2^{\chfont{Proc}}$ are defined as
  \begin{align*}
    \langle \cdot a \cdot \rangle S &= \{ p \in \chfont{Proc} : p \xrightarrow{a} p' \text{ and } p' \in S \text{ for
    some } p' \}\\
    [ \cdot a \cdot ] S &= \{ p \in \chfont{Proc} : p \xrightarrow{a} p' \text{ implies } p' \in S \text{ for
    each } p' \}
  \end{align*}
  We write $p \models F$ iff $p \in \llbracket F \rrbracket$. Two formulae are \emph{equivalent} iff they are satisfied
  by the same processes in every transition system.
\end{definition}

\subsubsection{HML with recursion}
A HML formula can only describe a \emph{finite} part of the overall behaviour of a process, and how much we can
explore depends on the \emph{modal-depth} of the formula. If we want to describe properties that describe a situation
that may or must occur in arbitrarily long computations of a process, we have to extend our logic by adding recursion.\\

The syntax of HML with one variable $X$, denoted by $\mathcal{M}_{\{ X \}}$ is given by the following grammar:
\begin{equation*}
    F,G ::= X~|~\mathit{tt}~|~\mathit{ff}~|~F \land G~|~F \lor G~|~\langle a \rangle F~|~[a]F
\end{equation*}
Semantically a formula F (which may contain a variable X) is interpreted as a function $\mathcal{O}_F :
2^{\chfont{Proc}} \to 2^{\chfont{Proc}}$ that given a set of processes that are assumed to satisfy $X$, gives us the set
of processes that satisfy $F$.

\begin{definition}
  Let $(\chfont{Proc},\chfont{Act}, \{\xrightarrow{a} : a \in \chfont{Act} \})$ be a LTS. For each $S \subseteq
  \chfont{Proc}$ and formula $F$, we define $\mathcal{O}_F(S)$ as follows:

  \begin{align*}
    \mathcal{O}_X(S) &= S\\
    \mathcal{O}_{\mathit{tt}}(S) &= \chfont{Proc}\\
    \mathcal{O}_{\mathit{ff}}(S) &= \emptyset\\
    \mathcal{O}_{F_1 \land F_2}(S) &= \mathcal{O}_{F_1}(S) \cap \mathcal{O}_{F_2}(S)\\
    \mathcal{O}_{F_1 \lor F_2}(S) &= \mathcal{O}_{F_1}(S) \cup \mathcal{O}_{F_2}(S)\\
    \mathcal{O}_{\langle a \rangle F}(S) &= \langle \cdot a \cdot \rangle \mathcal{O}_F(S)\\
    \mathcal{O}_{[ a ] F}(S) &= [ \cdot a \cdot ] \mathcal{O}_F(S)\\
  \end{align*}
\end{definition}

The idea underlying the definition of the function $\mathcal{O}_F$ is that if $\llbracket X \rrbracket \subseteq
\chfont{Proc}$ gives the set of processes that satisfy $X$ then $\mathcal{O}_F(\llbracket X \rrbracket)$ will be the 
set of processes that satisfy F. We assume that $\llbracket X \rrbracket$ is given by a recursive equation for $X$ of
the form

\begin{equation*}
  X \eqmin F_X \quad \text{or} \quad X \eqmax F_X
\end{equation*}

\begin{comment}
\section{TCCS}\label{sec:tccs}
For the timed extension of CCS we consider the work done in~\cite{yi1991ccs+}. The author proposes an interleaving
model for ``real-time'' systems by extending Milner's CCS~\cite{milner1989communication} with a notion of time, this 
model is independent of the time domain as long as it is a numerical domain. For convenience, from
now on we consider $\R_{\geq 0}$ as the time domain. Syntactically TCCS extends CCS with just a single construct, a new
prefix $\varepsilon(d).P$ that means 'delay $d$ units of time and then behave as $P$', note that $d$ can be any
positive number. TCCS takes the view that a real-time system has a two-phase behaviour, phases when the system idles 
while time passes and phases when the system performs atomic actions, considered instantaneous in time.

\subsection{Timed labelled transition systems}
To give semantics to real-time systems we use a variation of a labelled transition system, in which we describe the
passage of time by adding special 'delay' transitions to the model. These transitions would be used to give the
formal semantics of the delay-prefixing operators $\varepsilon(d)$ with $d \in \R_{\geq 0}$. The resulting structure is
a timed version of the model of LTSs.
\definition{} A \emph{timed labelled transition system}, also known as timed transition system is a triple
\begin{equation*}
  (\text{\chfont{Proc}}, \text{\chfont{Lab}}, \{\xrightarrow{~\alpha~}~: \alpha \in \text{\chfont{Lab}} \})
\end{equation*}
Where
\begin{itemize}
  \item \chfont{Proc} is a set of \emph{states} or processes;
  \item $\text{\chfont{Lab}} = \text{\chfont{Act}} \cup \R_{\geq 0}$ is a set of \emph{labels} consisting of \emph{actions} and
    \emph{time delays};
  \item $\xrightarrow{~\alpha~} \subseteq \text{\chfont{Proc}} \times \text{\chfont{Proc}}$, for each $\alpha \in \text{\chfont{Lab}}$, is a
    binary relation on states, called the \emph{transition relation}.
\end{itemize}
We write
\begin{align*}
  &s \xrightarrow{~a~} s' \text{ if } a \in \text{\chfont{Act} and } (s,s') \in \xrightarrow{~a~} \text{, and}\\
  &s \xrightarrow{~d~} s' \text{ if } d \in \R_{\geq 0} \text{ and } (s,s') \in \xrightarrow{~d~}.
\end{align*}
Transitions of the first type are ordinary transitions that are due to the performance of actions, while the second
type are time-elapsing transitions that describe how a system evolves as time passes. However these transitions don't
reflect our intuition of passage of time, in fact a TLTS must satisfy a so called \emph{time-additivity} requirement:
\begin{equation*}
  \text{if } s \xrightarrow{~d~}s' \text{ and } 0 \leq d' \leq d \text{ then } s \xrightarrow{~d'~} s''
  \xrightarrow{d-d'} s' \text{ for some state } s''
\end{equation*}
We can also say that $s \xrightarrow{~0~} s$ for every state $s$.\\
A final requirement that is imposed on TLTS is that delay transitions are \emph{deterministic}, i.e. for all $s,s',s''$
and for each $d \in \R_{\geq 0}$
\begin{equation*}
  \text{if } s \xrightarrow{~d~} s' \text{ and } s \xrightarrow{~d~} s'' \text{ then } s' = s''
\end{equation*}
% and that action transitions are \emph{persistent}: for all $s,s'$, action $a$ and delay $d \in \R_{\geq 0}$
% \begin{equation*}
%   \text{if } s \xrightarrow{~a~}\text{ and } s \xrightarrow{~d~} s' \text{ then } s' \xrightarrow{~a~}
% \end{equation*}
This captures the way in which a system can evolve by just idling as time passes. From now on, we restrict to TLTSs
that satisfy these requirements.

\subsection{Syntax and semantics}
As indicated in section~\ref{sec:tccs}, the only construct to add to the syntax of CCS are the delay-prefixing
operators $\varepsilon(d)$, with $d \in \R_{\geq 0}$. Formally, the collection $\mathcal{P}$ of timed CCS expressions
is given by the grammar of CCS expressions of section~\ref{sec:ccs}, extended my the following formation rule:\\\\
if $P$ is in $\mathcal{P}$ and $d \in \R_{\geq 0}$ then $\varepsilon(d).P$ is in $\mathcal{P}$.\\\\
In what follows we don't distinguish the terms $P$ and $\varepsilon(0).P$, and we assume that the behaviour of each
process constant is given by a defining equation $K \eqdef P$. Since we are identifying $P$ with $\varepsilon(0).P$, we
have the following rule:
\begin{prooftree}
  \AxiomC{$P \xrightarrow{\alpha}P'$}
  \UnaryInfC{$\varepsilon(0).P \xrightarrow{\alpha}P'$}
\end{prooftree}

\subsubsection{Parallel composition and maximal progress}
So far we have seen three types of transitions: $P \xrightarrow{~\alpha~} Q$, $P \xrightarrow{~\tau~} Q$ and $P
\xrightarrow{~d~} Q$ in which the latter takes $d$ units of time and is internal, while the other ones take no time.
Now we ask ourselves whether $\tau.P$ is allowed to wait, or a more general question is whether an agent is allowed to
wait, when it can perform a $\tau$ transition. The solution adopted by Wang Yi in~\cite{yi1991ccs+} is to postulate
that the ovolution of processes obeys the so-called \emph{maximal-progress assumption}. Intuitively, this means that
if a process is ready to perform a $\tau$-action then it will do so without further delay. Therefore the
maximal-progress assumption can be formalized as follows:
\begin{center}
  for each TCCS process $P$, if $P \xrightarrow{\tau}$ then $P \ssNeg[1mu]{\xrightarrow{d}}$ for any $d > 0$.
\end{center}
The maximal-progress assumption is expressed in the operational semantics of timed CCS by the following rules:
\begin{center}
    \centerAlignProof
    \AxiomC{}
    \UnaryInfC{$\tau.P \xrightarrow{0} \tau.P$}
    \DisplayProof
    \qquad
    \AxiomC{$P \xrightarrow{d} P'$}
    \AxiomC{$Q \xrightarrow{d} Q'$}
    \AxiomC{NoSync($P,Q,d$)}
    \TrinaryInfC{$P~|~Q \xrightarrow{d} P'~|~Q'$}
    \DisplayProof
\end{center}
Where the predicate NoSync($P,Q,d$) intuitively expresses that no synchronization between $P$ and $Q$ becomes available
by delaying less than $d$ time units. Formally:\\
\begin{align*}
  \text{NoSync}(P,Q,d) \iff &\text{ for each } 0 \leq d' < d \text{ and expressions } P',Q', \\
  & \text{ if } P \xrightarrow{d'} P' \text{ and } Q \xrightarrow{d'} Q' \text{ then } P'~|~Q' \ssNeg[1mu]{\xrightarrow{\tau}}.
\end{align*}
The SOS of TCCS is descibed in table~\ref{fig:sos}, the rules for standard actions are the same as for CCS.

\begin{figure}
\centering
  \begin{tabular}{c c}
  \hline\hline\\
  %\bottomAlignProof
  \AxiomC{$P \xrightarrow{d'} P'$}
  \UnaryInfC{$\varepsilon(d).P \xrightarrow{d+d'} P'$}
  \DisplayProof
  &
  \AxiomC{}
  \RightLabel{for $d' \leq d$}
  \UnaryInfC{$\varepsilon(d).P \xrightarrow{d'} \varepsilon(d-d').P$}
  \DisplayProof
  \\\\
  \AxiomC{$P \xrightarrow{d} P'$}
  \RightLabel{$K \eqdef P$}
  \UnaryInfC{$K \xrightarrow{d} P'$}
  \DisplayProof
  &
  \AxiomC{}
  \RightLabel{for $\alpha \neq \tau$}
  \UnaryInfC{$\alpha.P \xrightarrow{d} \alpha.P$}
  \DisplayProof
  \\\\
  \AxiomC{$P_i \xrightarrow{d} P'_i$ for each $i \in I$}
  \UnaryInfC{$\sum_{i \in I} P_i \xrightarrow{d} \sum_{i \in I} P'_i$}
  \DisplayProof
  &
  \AxiomC{$P \xrightarrow{d} P'$}
  \UnaryInfC{$P[f] \xrightarrow{d} P'[f]$}
  \DisplayProof
  \\\\
  \AxiomC{$P \xrightarrow{d} P'$}
  \UnaryInfC{$P \setminus L \xrightarrow{d} P' \setminus L$}
  \DisplayProof
  &
  \AxiomC{}
  \UnaryInfC{$\tau.P \xrightarrow{0} \tau.P$}
  \DisplayProof
  \\\\
  \AxiomC{$P \xrightarrow{d} P'$}
  \AxiomC{$Q \xrightarrow{d} Q'$}
  \AxiomC{NoSync($P,Q,d$)}
  \TrinaryInfC{$P~|~Q \xrightarrow{d} P'~|~Q'$}
  \DisplayProof
  &
  \\\\
  \hline\hline
\end{tabular}
  \caption{SOS rules for TCCS ($d, d' \in \R_{\geq 0}$)}
  \label{fig:sos}
\end{figure}

\subsection{Considerations}
Timed CCS is a simple extension of Milner's CCS and can be used to describe aspects of timed-dependent behaviour in the
evolution of reactive systems. From an expressiveness point of view, however, the resulting calculus is not completely
satisfactory. Let's see an example:
\begin{example}
Consider the following TLTS:
  \begin{equation*}
    (\text{\chfont{Proc}},\text{\chfont{Lab}}, \{\xrightarrow{~\alpha~}~:~\alpha \in \text{\chfont{Lab}}\})
  \end{equation*}
\end{example}
Where \chfont{Proc} $=\R_{\geq 0}$, \chfont{Lab} $=\{a\} \cup \R_{\geq 0}$ such that $\xrightarrow{~a~} = \{(5,0)\}$ and for all $d \in
\R_{\geq 0}$, we define $\xrightarrow{~d~} = \{(d',d'') \in \R_{\geq 0} \times \R_{\geq 0}~:~ d'+d=d''\}$. The diagram
below shows a small part of the timed labelled transition system defined above.
\begin{figure}[h!]
  \centering
  \tikzset{every loop/.style={min distance=10mm,in=0,out=60,looseness=10}}
  \begin{tikzpicture}[>=stealth',shorten >=1pt,auto,node distance=2.8cm,semithick]
    \draw[thick,-] (0,0) -- (12,0) node[anchor=north west] {};
    \draw[] (12.5,0) node[] {$\ldots$};
    \foreach \x in {0,1,2,3,4,5}
      \draw (\x*2 cm,7pt) -- (\x*2 cm,-7pt) node[anchor=north] {$\x$};

    \tikzstyle{every state}=[draw=none]

      \node[state,inner sep=0pt, minimum size=0pt]         (A) at (0,0) {};
      \node[state,inner sep=0pt, minimum size=0pt]         (B) at (2,0) {};
      \node[state,inner sep=0pt, minimum size=0pt]         (C) at (4,0) {};
      \node[state,inner sep=0pt, minimum size=0pt]         (D) at (5,0) {};
      \node[state,inner sep=0pt, minimum size=0pt]         (E) at (6,0) {};
      \node[state,inner sep=0pt, minimum size=0pt]         (F) at (7,0) {};
      \node[state,inner sep=0pt, minimum size=0pt]         (G) at (8,0) {};
      \node[state,inner sep=0pt, minimum size=0pt]         (H) at (9,0) {};
      \node[state,inner sep=0pt, minimum size=0pt]         (I) at (10,0) {};
      \node[state,inner sep=0pt, minimum size=0pt]         (J) at (11,0) {};

      \path (A) edge [->,bend right=40,anchor=north]    node {\scriptsize 3} (E)
            (B) edge [->,bend right=70,anchor=north]    node {\scriptsize 1} (C)
            (B) edge [->,loop above,anchor=south]       node {\scriptsize 0} (B)
            (D) edge [->,bend right=60,anchor=north]    node {\scriptsize 2} (H)
            (E) edge [->,bend right=60,anchor=north]    node {\scriptsize 0.5} (F)
            (H) edge [->,bend left=60,anchor=south]     node {\scriptsize 1} (J)
            (J) edge [->,loop above,anchor=south]       node {\scriptsize 0} (J)
            (I) edge [->,bend right,anchor=south]     node {\scriptsize $a$} (A);
  \end{tikzpicture}
\end{figure}

This TLTS cannot be described, up to isomorphism, using TCCS. To see this we exploit the fact that a subclass of TCCS
process terms afford the following \emph{persistency property} of action transitions.
\begin{center}
  For all processes $P$, $Q$, action $a$ and delay $d$, if $P \xrightarrow{a}$ and $P \xrightarrow{d} Q$ then $Q
  \xrightarrow{a}$.
\end{center}
In fact, a slightly more elaborate argument shows that each TCCS process term affords the above property. However, the
TLTS above does \emph{not} have the persistency property. In fact, state 5 has an outgoing $a$-labelled transition, but
none of the states that it can reach by delaying a positive amount of time has that transition.\\
The above example would seem to suggest that an automaton-based formalism with some explicit notion of clocks that can
be used to determine when transitions are available and when they are disabled might be a natural and powerful
formalism for real-time behaviours.
\end{comment}

\section{Timed automata}
The model of timed automata introduced by Alur and Dill in~\cite{alur1991techniques,alur1994theory} is a classical
formalism for modelling real-time systems with a dense representation of time (i.e. the time domain is $\R_{\geq 0}$).
The development of timed-automata was largely driven by the goal of obtaining decidability results for several
important properties. Several real-time model checking tools exsist such \textsc{Uppaal}~\cite{larsen1997uppaal} and
\textsc{Kronos}~\cite{daws1995tool,bozga1998kronos} based on the formalism of timed automata.

\subsection{Syntax of timed automata}
Timed automata are essentialy nondeterministic finite automata with a finite set of real-valued clocks, which measure
delays between events that occur in the automaton, so that transitions can be conditioned on clock values and the
performing of a particular transition can reset selected clocks. Therefore the main ingredients that timed automata
add to the standard model of nondeterministic finite automata are clocks, clock constraints and clock resets.

Let $C = \{x,y,\ldots\}$ be a finite set of clock names that can be used in the automaton.
\begin{definition}
  The set $\mathcal{B}(C)$ of \emph{clock constraints} over the set of clocks $C$ is defined by the following abstract
  syntax:
  \begin{equation*}
    g,g_1,g_2 ::= x \bowtie n~|~ g_1 \land g_2
  \end{equation*}
  Where $x \in C$ is a clock, $n \in \N$ and $\bowtie \in \{\leq, <, =, >, \geq \}$.
\end{definition}
Each clock from the set $C$ stores the amount of time elapsed from the last moment when the clock was reset. This is
formally expressed by a function $v : C \to \R_{\geq 0}$ called (\emph{clock}) \emph{valuation}. The value of a
particular clock is denoted by $v(x)$. For $d \in \R_{\geq 0}$, the valuation $v+d$ is the clock valuation such that
$(v+d)(x) = v(x) + d$ for each $x \in C$. For a subset $R \subseteq C$ we let $v[R]$ be the valuation such that
$v[R](x) = 0$ when $x \in R$ and $v[R](x) = v(x)$ when $x \in C \setminus R$.\\

Now we can define when a clock constraint satisfies a given valuation, or in other words how the constraint evaluates
under the valuation.
\begin{definition}
  Let $g \in \mathcal{B}(C)$ be a clock constraint for a given set of clocks $C$ and let $v : C \to \R_{\geq 0}$ be a
  clock valuation. The \emph{evaluation} of clock constraints ($v \models g$) is defined inductively on the structure
  of $g$:
  \begin{align*}
    &v \models x \bowtie n \text{ iff } v(x) \bowtie n\\
    &v \models g_1 \land g_2 \text { iff } v \models g_1 \text{ and } v \models g_2
  \end{align*}
  Where $x \in C$ is a clock, $n \in \N$, $g_1, g_2 \in \mathcal{B}(C)$ and $\bowtie \in \{ \leq, <, =, > \geq \}$.
\end{definition}

\begin{definition}
  Two clock constraints $g_1$ and $g_2$ are said to be \emph{equivalent} iff they are satisfied by the same valuations,
  i.e. for all valuations $v$, $v \models g_1 \Leftrightarrow v \models g_2$.
\end{definition}

\begin{definition}
  A \emph{timed automaton} over a finite set of clocks $C$ and a finite set of actions \chfont{\chfont{Act}} is a quadruple
  \begin{equation*}
    (L,l_0,E,I)
  \end{equation*}
  where
  \begin{itemize}
    \item $L$ is a finite set of \emph{locations}, ranged over by $l$;
    \item $l_0 \in L$ is the \emph{initial location};
    \item $E \subseteq L \times \mathcal{B}(C) \times \chfont{Act} \times 2^C \times L$ is a finite set of
      \emph{edges};
    \item $I : L \to \mathcal{B}(C)$ assigns \emph{invariants} to locations.
  \end{itemize}
  We can write $l \xrightarrow{g,a,R} l'$ instead of $(l,g,a,R,l') \in E$, where $l$ is the \emph{source location}, $g$
  is the \emph{guard}, $a$ is the \emph{action}, $R$ is the set of clocks to be reset and $l'$ is the \emph{target
  location}.
\end{definition}

\subsection{Semantics of timed automata}
A suitable notion of the \emph{state} of computation or a \emph{configuration} of a timed automaton consists of a pair
$(l,v)$, where $l$ is the control location the automaton is in and $v$ is the clock valuation determined by the current
clock values. The pair $(l,v)$ is a legal state of the timed automaton only if the valuation $v$ satisfies the
invariant of location $l$. Initially, the control location is $l_0$ and the value of each clock is 0.\\

The operational semantics of a timed automata is defined through an infinite-state transition system defined as
follows:
\begin{definition}
  Let $\mathcal{A} = (L,l_0,E,I)$ be a timed automaton over a set of clocks $C$ and a set of actions \chfont{Act}. We define the
  timed transition system $T(\mathcal{A})$ generated by $\mathcal{A}$ as $T(\mathcal{A}) = (\chfont{Proc}, \chfont{Lab}, \{\xrightarrow{~\alpha~}~:~
  \alpha \in \chfont{Lab}\})$ where:
  \begin{itemize}
    \item \chfont{Proc} $= \{ (l,v) : (l,v) \in L \times (C \to \R_{\geq 0}) \text{ and } v \models I(l)\}$, meaning
      that states are of the form $(l,v)$, where $l$ is a location of the timed automaton and $v$ is a valuation that
      satisfies the invariant of $l$;
    \item \chfont{Lab} $= \chfont{Act} \cup \R_{\geq 0}$ is the set of labels;
    \item the transition relation is defined by
    \begin{itemize}
      \item $(l,v) \xrightarrow{~a~} (l',v')$ if there is an edge $(l \xrightarrow{g,a,R} l') \in E$ such that $v
        \models g$, $v' = v[R]$ and $v' \models I(l')$,
      \item $(l,v) \xrightarrow{~d~} (l,v+d)$ for all $d \in \R_{\geq 0}$ such that $v \models I(l)$ and $v+d \models
        I(l)$.
    \end{itemize}
  \end{itemize}
  Let $v_0$ denote the valuation such that $v_0(x) = 0$ for all $x \in C$. If $v_0$ satisfies the invariant of the
  initial location $l_0$, then $(l_0,v_0)$ is called the \emph{initial state} or \emph{initial configuration} of
  $T(\mathcal{A})$.
\end{definition}
There's a fundamental difference between a clock constraint used in the guard and when it's used in an invariant. Let's
see an example:
\begin{example}
  In the timed automaton (a) of figure~\ref{fig:ex_clock} $x \leq 1$ is a guard. There's no restriction on
  time-elapsing, therefore, arbitrary long delays are possible. This means that, as long as the value of clock $x$ is
  less or equal to 1, we can perform the $a$-transition and reset $x$. However, if the total time delay after the last
  reset of $x$ is strictly greater than 1, then it's not possibile to take the action $a$ and the only available
  transitions are the delay steps. In the automaton (b), $x \leq 1$ is used in the invariant, meaning that it is never
  possibile to delay for more than 1 unit time, hence it's always possibile to take the $a$-transition.
\end{example}
\begin{figure}
  \centering
  \begin{tikzpicture}[>=stealth',shorten >=1pt,auto,node distance=2cm]
    \node[state,initial text=,accepting]      (q0) {};
    \node[] at (-1.8,0) {\large (a)};
    \node[] at (0.7,0.9) {\scriptsize $x \leq 1$};
    \node[] at (-0.7,0.9) {\scriptsize $x := 0$};

      \path[->] 
          (q0) edge[loop above] node {a} (q0);
  \end{tikzpicture}
  \qquad\qquad
  \begin{tikzpicture}[>=stealth',shorten >=1pt,auto,node distance=2cm]
    \node[state,initial text=,accepting]      (q0) {};
    \node[] at (-1.8,0) {\large (b)};
    \node[] at (1.2,0) {$x \leq 1$};
    \node[] at (-0.7,0.9) {\scriptsize $x := 0$};

      \path[->] 
          (q0) edge[loop above] node {a} (q0);
  \end{tikzpicture}
  \caption{Clock constraint $x \leq 1$ (a) in the guard and (b) in the invariant.}
  \label{fig:ex_clock}
\end{figure}

% \subsection{Networks and parallel composition of timed automata}
% Many real-life systems consist of a number of independent components running in parallel and communicating whenever
% necessary. Process algebras like CCS and TCCS provide this possibility by means of the operation of parallel
% composition. In case of timed automata, our formalism so far enables us to model only a single component. In this
% section

% \section{Timed behavioural equivalences}
\subsection{Region graphs}\label{sec:reg_graph}
As we've seen in the previous section, timed automata generate timed transition systems with infinitely many reachable
states. This is due to the fact that states of timed automata contain not only the control location but also a clock
valuation, and we have uncountably many valuations. So we could ask ourselves if algorithmic verification is possibile.
The answer is yes, using the \emph{region graph} technique due to~\cite{alur1991techniques, alur1994theory}.

The idea behind the region technique is simple: even though the collection of valuations for a given timed
automaton is (uncountably) infinite, it can be partitioned into finitely many equivalence classes in such a way that
any two valuations from the same equivalence class will not create any 'significant difference' in the behaviour of the
system.\\
Before defining the equivalence relation $\equiv$ we introduce some notation.

\begin{definition}
  Let $d \in \R_{\geq 0}$ be a real number. By $\lfloor d \rfloor$ we denote the integer part of $d$ and by $frac(d)$
  the fractional part of $d$. Any $d \in \R_{\geq 0}$ can now be written as $d = \lfloor d \rfloor + frac(d)$.
\end{definition}
Let $\mathcal{A}$ be a timed automaton and let $x \in C$ be one of its clocks. We define $c_x \in \N$ as the maximal
constant appearing in a clock constraint or invariant of $x$.

\begin{definition}
  Let $\mathcal{A}$ be a timed automaton, we say that two clock valuations $v$ and $v'$ are equivalent, written $v
  \equiv v'$, iff:
  \begin{enumerate}
    \item for each $x \in C$ we either have that 
      \begin{equation*}
        v(x) > c_x \land v'(x) > c_x \text{ or } \lfloor v(x) \rfloor = \lfloor v'(x) \rfloor
      \end{equation*}
    \item for each $x \in C$ s.t. $v(x) \leq c_x$ we have 
      \begin{equation*}
        frac(v(x)) = 0 \text{ iff } frac(v'(x)) = 0;
      \end{equation*}
    \item for all $x, y \in C$ such that $v(x) \leq c_x$ and $v(y) \leq c_y$ we have
      \begin{equation*}
        frac(v(x)) \leq frac(v(y)) \text{ iff } frac(v'(x)) \leq frac(v'(y))
      \end{equation*}
  \end{enumerate}
\end{definition}
Now we can define the notion of a region.

\begin{definition}
  An $\equiv$-equivalence class $[v]_{\equiv}$ represented by some clock valuation $v$ is called a \emph{region}.
\end{definition}
Each region can be uniquely characterized by a finite collection of clock constraints that it satisfies.
\begin{example}
  Consider a timed automaton with one clock $x$ such that $c_x = 3$, we have 8 regions:
  \begin{itemize}
    \item $[x=0]_{\equiv}$, $[x=1]_{\equiv}$, $[x=2]_{\equiv}$, $[x=3]_{\equiv}$,
    \item $[0 < x < 1]_{\equiv}$,$[1 < x < 2]_{\equiv}$,$[2 < x < 3]_{\equiv}$ and
    \item $[3 < x]_{\equiv}$
  \end{itemize}
  Depicted in the following way:\\\\
  \begin{tikzpicture}
    \centering
    \draw[thick,-] (0,0) -- (8,0) node[anchor=north west] {};
    \draw[] (7.5,-0.5) node[] {$x$};
    \foreach \x in {0,1,2,3} {
      \draw (\x*2 cm,7pt) -- (\x*2 cm,-7pt) node[anchor=north] {$\x$};
      \filldraw (\x*2,0) circle (3pt);
    }
  \end{tikzpicture}
\end{example}

\begin{example}
  Consider a timed automaton with two clocks $x$ and $y$ such that $c_x=2$ and $c_y=1$, we have 28 regions:\\\\
  \begin{center}
  \begin{tikzpicture}
    \draw[thick,-] (0,0) -- (9,0) node[anchor=north west] {$x$};
    \draw[thick,-] (0,0) -- (0,7) node[anchor=south east] {$y$};
    \draw[thick,-] (0,2) -- (9,2);
    \draw[thick,-] (2,0) -- (2,7);
    \draw[thick,-] (4,0) -- (4,7);
    \draw[thick,-] (0,0) -- (2,2);
    \draw[thick,-] (2,0) -- (4,2);

    \foreach \x in {0,1,2,3,4}
        \draw (\x*2 cm,5pt) -- (\x*2 cm,-5pt) node[anchor=north] {$\x$};
    \foreach \y in {0,1,2,3}
        \draw (5pt,\y*2 cm) -- (-5pt,\y*2 cm) node[anchor=east] {$\y$};

    \foreach \x in {0,1,2} {
      \foreach \y in {0,1} {
        \filldraw (\x*2,\y*2) circle (3pt);
      }
    }

  \end{tikzpicture}
  \end{center}
\end{example}
As we can see in the examples above, each region of a timed automata can be uniquely represented by specifying the
following items of information:
\begin{itemize}
  \item for each clock $x$ a constraint from the set
    \begin{gather*}
      \big\{ \{ x = n: n \in \{0,1,\ldots, c_x\} \big\}\\
      \cup \big\{ \{ n < x < n +1 : n \in \{0,1,\ldots, c_x - 1\} \big\} \cup \{c_x < x \}
    \end{gather*}
  \item for each pair of distinct clocks $x$ and $y$ that, for some $n < c_x$ and $m < c_y$, satisfy constraints of the form
    $n < x < n+1$ and $m < y < m+1$, an indication whether $frac(v(x))$ is less than, equal to, or greater than
    $frac(v(y))$, for each valuation $v$ in that region.
\end{itemize}
Now we can define the concept of \emph{region graph}. Intuitively, every configuration of the form $(l,v)$ is replaced
by a \emph{symbolic state} $(l,[v]_{\equiv})$ in the region graph, where $[v]_{\equiv}$ is the region represented by
$v$. Whenever we have a transition between two configurations, we will have a transition between the corresponding
symbolic states.

\begin{definition}
  The \emph{region graph} of a timed automaton $\mathcal{A}$ over a set of clocks $C$ and actions \chfont{Act} is a
  LTS:
  \begin{equation*}
    T_r(\mathcal{A}) = (\chfont{Proc}, \chfont{Act} \cup \{\varepsilon\}, \{\xRightarrow{a}:a \in \chfont{Act} \cup
    \{\varepsilon\}\})
  \end{equation*}
  where
  \begin{itemize}
    \item \chfont{Proc} $= \{(l,[v]_{\equiv}) : l \in L, v : C \to \R_{\geq 0} \}$, states are symbolic states;
    \item the transition relation $\Rightarrow$ is defined as follows:
      \begin{enumerate}
        \item for each label $a \in \chfont{Act}$, we have $(l,[v]_{\equiv}) \xRightarrow{a} (l',[v']_{\equiv})$ iff
          $(l,v) \xrightarrow{~a~} (l',v')$;
        \item $(l,[v]_{\equiv}) \xRightarrow{\varepsilon} (l,[v']_{\equiv})$ iff $(l,v) \xrightarrow{~d~} (l,v')$ for
          some $d \in \R_{\geq 0}$.
      \end{enumerate}
  \end{itemize}
\end{definition}

\begin{example}
Consider the following timed automata
  \begin{center}
    \begin{tikzpicture}[>=stealth',shorten >=1pt,auto,node distance=6cm]
      \node[state,initial,initial text=,accepting]  (l0)                {$l_0$};
      \node[state]                                  (l1) [right of=l0]  {$l_1$};
      \node[] at (1,1) {\scriptsize $x=1$};
      \node[] at (5,1) {\scriptsize $y:=0$};
      \node[] at (6.7,0.8) {\scriptsize $y=0$};
      \node[] at (5,-1) {\scriptsize $y=1$};
      \node[] at (1,-1) {\scriptsize $x:=0,y:=0$};

        \path[->] 
            (l0) edge[bend left] node {a} (l1)
            (l1) edge[bend left] node {c} (l0)
            (l1) edge[loop above] node {b} (l1);
    \end{tikzpicture}
  \end{center}
  The regions with assigned numbers are:\\
  \begin{center}
    \begin{tikzpicture}[>=stealth',shorten >=1pt,auto,node distance=2.8cm,semithick]
        \node[state,inner sep=3pt, minimum size=1pt]              (1) at (0,0) {1};
        \node[state,inner sep=0pt, minimum size=0pt, draw=none]   (5) at (2,0) {5};
        \node[state,inner sep=3pt, minimum size=1pt]              (2) at (4,0) {2};
        \node[state,inner sep=0pt, minimum size=0pt, draw=none]   (10) at (6,0) {10};
        \node[state,inner sep=0pt, minimum size=0pt, draw=none]   (7) at (0,2) {7};
        \node[state,inner sep=3pt, minimum size=1pt]              (3) at (0,4) {3};
        \node[state,inner sep=0pt, minimum size=0pt, draw=none]   (12) at (0,6) {12};
        \node[state,inner sep=0pt, minimum size=0pt, draw=none]   (6) at (2,4) {6};
        \node[state,inner sep=3pt, minimum size=1pt]              (4) at (4,4) {4};
        \node[state,inner sep=0pt, minimum size=0pt, draw=none]   (11) at (6,4) {11};
        \node[state,inner sep=0pt, minimum size=0pt, draw=none]   (8) at (4,2) {8};
        \node[state,inner sep=0pt, minimum size=0pt, draw=none]   (13) at (4,6) {13};
        \node[state,inner sep=0pt, minimum size=0pt, draw=none]   (9) at (2,2) {9};

        \node[] at (0,-0.8) {0};
        \node[] at (-0.8,0) {0};
        \node[] at (4,-0.8) {1};
        \node[] at (5.5,-0.5) {$x$};
        \node[] at (-0.8,4) {1};
        \node[] at (-0.5,5.5) {$y$};
        \node[] at (2,5) {17};
        \node[] at (5,5) {18};
        \node[] at (5,2) {16};
        \node[] at (1,3) {15};
        \node[] at (3,1) {14};

        \path[-]
          (1) edge[] node   {} (5)
          (5) edge[] node   {} (2)
          (2) edge[] node   {} (10)
          (1) edge[] node   {} (7)
          (7) edge[] node   {} (3)
          (3) edge[] node   {} (12)
          (3) edge[] node   {} (6)
          (6) edge[] node   {} (4)
          (4) edge[] node   {} (11)
          (2) edge[] node   {} (8)
          (8) edge[] node   {} (4)
          (4) edge[] node   {} (13)
          (1) edge[] node   {} (9)
          (4) edge[] node   {} (9)
          ;
    \end{tikzpicture}
  \end{center}
Part of the region graph reachable from the initial configuration $(l_0,1) = (l_0,[x=y=0]_{\equiv})$ is:\\
\begin{center}
  \begin{tikzpicture}[>=stealth,>=implies,shorten >=1pt,auto,node distance=3cm,semithick]
    \tikzset{elliptic state/.style={ellipse}}
    \tikzset{every loop/.style={min distance=5mm,in=60,out=90,looseness=10}}
    \tikzstyle{every state}=[draw=none]
      \node[state,initial text=,accepting]                      (l01)                         {$(l_0,1)$};
      \node[state]                                              (l09)   [right of=l01]        {$(l_0,9)$};
      \node[state]                                              (l04)   [right of=l09]        {$(l_0,4)$};
      \node[elliptic state,inner sep=0pt, minimum size=0pt]     (l018)  [right of=l04]        {$(l_0,18)$};
      \node[elliptic state,inner sep=0pt, minimum size=0pt]     (l12)   [below of=l01]        {$(l_1,2)$};
      \node[state]                                              (l116)  [right of=l12]        {$(l_1,16)$};
      \node[state]                                              (l111)  [right of=l116]       {$(l_1,11)$};
      \node[elliptic state,inner sep=0pt, minimum size=0pt]     (l118)  [right of=l111]       {$(l_1,18)$};
      
      \path[->]
        (l01) edge[double] node {$\varepsilon$} (l09)
        (l09) edge[double] node {$\varepsilon$} (l04)
        (l04) edge[double] node {$\varepsilon$} (l018)
        (l018) edge[double,loop above] node {$\varepsilon$} (l018)
        (l04) edge[double] node[pos=0.2] {$a$} (l12)
        (l12) edge[double,loop above] node {$\varepsilon$} (l12)
        (l12) edge[double] node {$\varepsilon$} (l116)
        (l116) edge[double] node {$\varepsilon$} (l111)
        (l111) edge[double] node {$\varepsilon$} (l118)
        (l111) edge[double] node[pos=0.3] {$c$} (l01)
        (l118) edge[double,loop above] node {$\varepsilon$} (l118)
        ;   
  \end{tikzpicture}
\end{center}
The reflexive closure of the $\xRightarrow{\varepsilon}$ transitions has been omitted.
\end{example}
An important application of region graphs is to the reachability problem.\\
Given a timed automata $\mathcal{A}$ we write $(l,v) \longrightarrow (l',v')$ whenever
\begin{itemize}
  \item $(l,v) \xrightarrow{~a~} (l',v')$ for some action $a$, or
  \item $(l,v) \xrightarrow{~d~} (l',v')$ for some $d \in \R_{\geq 0}$.
\end{itemize}
The reachability problem for timed automata is defined as follows. Given a timed automaton $\mathcal{A} = (L,l_0,E,I)$
over a set of clocks $C$ and a configuration $(l,v)$, the question is whether $(l,v)$ is reachable from the initial
configuration, i.e. whether $(l_0,v_0) \longrightarrow^* (l,v)$ where $v_0(x) = 0~\forall x \in C$.

Using the region graph technique, we have the following lemma.
\begin{lemma}
  Let $\mathcal{A} = (L,l_0,E,I)$ be a timed automaton and $(l,v)$ a configuration. It holds that $(l_0,v_0)
  \longrightarrow^* (l,v)$ in $\mathcal{A}$ iff $(l_0,[v_0]_{\equiv}) \Rightarrow^* (l,[v]_{\equiv})$ in its region
  graph $T_r(\mathcal{A})$.
\end{lemma}
A corollary of this lemma, shown by Alur and Dill~\cite{alur1994theory} is:
\begin{corollary}
  The reachability problem for timed automata is decidable.
\end{corollary}
\begin{theorem}
  The reachability problem for timed automata is \textsc{PSPACE}-complete.
\end{theorem}

\section{THML}\label{sec:thml}
Since HML is a convenient formalism for the description of behavioural properties of reactive systems modelled
semantically as LTSs, and since the semantics of timed automata is given in terms of TLTSs. It is natural to define a
notion of HML for real-time systems. In what follows we introduce this variation of HML described by Laroussinie et
al.~\cite{laroussinie1995timed}.

\subsection{Syntax and semantics}
If we want to define a modal logic for describing the properties of TLTSs, it seems reasonable to augment the
syntax of HML with two new modalities used to express the possibile and necessary behaviour of systems as time
progresses, these two new modalities will be denoted by $\mathrlap{\exists}\,\exists$ and
$\mathrlap{\forall}\,\forall$ with the following meaning:
\begin{itemize}
  \item a process satisfies a formula of the form $\mathrlap{\exists}\,\exists F$ iff it \emph{can delay for some amount
    of time} thereby reaching a state satisfying $F$;
  \item a process satisfies a formula of the form $\mathrlap{\forall}\,\forall F$ iff \emph{no matter how long it
    delays} it will always reach a state satisfying $F$.
\end{itemize}
We also need to extend HML with a way of expressing 'quantitative real-time constraints'. The choice made by
Laroussinie et al. is to augment HML with clock constraints and clock resets. Intuitively a formula of the form
\begin{equation*}
  x~\texttt{\underline{in}}~F
\end{equation*}
says that a state in a TLTS will satisfy $F$ after the value of $x$ has been set to zero. For simplicity we assume that
the clocks used in the formulae are disjoint with the clocks that appear in time automata.

We can now present the syntax of THML.
\begin{definition}
  The set of Hennessy-Milner formulae with time $\mathcal{M}_t$, over a set of actions \chfont{Act} and a set of
  formula clocks $D$ is given by the following syntax:
  \begin{equation*}
    F ::= \mathit{tt}~|~\mathit{ff}~|~F \land G~|~F \lor G~|~\langle a \rangle F~|~[a]F~|~\mathrlap{\exists}\,\exists
    F~|~\mathrlap{\forall}\,\forall F~|~ x~\texttt{\underline{in}}~F~|~ g
  \end{equation*}
  where $a \in \chfont{Act}$, $x \in D$ and $g \in \mathcal{B}(D)$.
\end{definition}
This logic can be used to describe properties of states in a TLTS over the set of actions \chfont{Act}. The semantics
of a formula in the language $\mathcal{M}_t$ is given by characterizing the collection of states that satisfy it.

The semantics of formulae is given with respect to a given TLTS
\begin{equation*}
  (\chfont{Proc}, \chfont{Lab}, \{\xrightarrow{~\alpha~}~:~\alpha \in \chfont{Lab}\}).
\end{equation*}
An \emph{extended state} over \chfont{Proc} is a pair $(p,u)$ where $p$ is a state in \chfont{Proc} and $u$ is a
mapping $u : D \to \R_{\geq 0}$. The set of extended states over \chfont{Proc} is denoted by
$\mathcal{ES}(\chfont{Proc})$.

\begin{definition}
  We define $\llbracket F \rrbracket \subseteq \mathcal{ES}(\chfont{Proc})$ for $F \in \mathcal{M}_t$ by\\\\
  {\tabulinesep=1.5mm
  \begin{tabu}{l l}
    $\llbracket \mathit{tt} \rrbracket = \mathcal{ES}(\chfont{Proc})$
    &
    $\llbracket F \lor G \rrbracket = \llbracket F \rrbracket \cup \llbracket G \rrbracket$\\
    $\llbracket \mathit{ff} \rrbracket = \emptyset$
    &
    $\llbracket \langle a \rangle F \rrbracket = \langle \cdot a \cdot \rangle \llbracket F \rrbracket$\\
    $\llbracket F \land G \rrbracket = \llbracket F \rrbracket \cap \llbracket G \rrbracket$
    &
    $\llbracket [ a ] F \rrbracket = [ \cdot a \cdot ] \llbracket F \rrbracket$\\
    $\llbracket \mathrlap{\exists}\,\exists F \rrbracket = \langle \cdot \varepsilon \cdot \rangle \llbracket F
    \rrbracket$
    &
    $\llbracket \mathrlap{\forall}\,\forall F \rrbracket = [ \cdot \varepsilon \cdot ] \llbracket F \rrbracket$\\
    $\llbracket x~\texttt{\underline{in}}~F \rrbracket = \{(p,u) : (p,u[x \mapsto 0]) \in \llbracket F \rrbracket \}$
    &
    $\llbracket g \rrbracket = \{(p,u) : p \in \chfont{Proc}, u \models g \}$\\
  \end{tabu}
  }
  \\Where the operators $\langle \cdot a \cdot \rangle, [\cdot a \cdot], \langle \cdot \varepsilon \cdot \rangle, [\cdot
  \varepsilon \cdot] : \wp(\mathcal{ES}(\chfont{Proc})) \to \wp(\mathcal{ES}(\chfont{Proc}))$ are defined by 
  \begin{align*}
    & \langle \cdot a \cdot \rangle S = \{(p,u) \in \mathcal{ES}(\chfont{Proc}) : \exists p'. p \xrightarrow{a} p'
    \text{ and } (p',u) \in S \}\\
    & [ \cdot a \cdot ] S = \{(p,u) \in \mathcal{ES}(\chfont{Proc}) : \forall p'. p \xrightarrow{a} p'
    \text{ implies } (p',u) \in S \}\\
    & \langle \cdot \varepsilon \cdot \rangle S = \{(p,u) \in \mathcal{ES}(\chfont{Proc}) : \exists d \in \R_{\geq
    0} . \exists p' \in \chfont{Proc}. p \xrightarrow{d} p' \text{ and }\\
    & \qquad\qquad\quad(p',u+d) \in S \}\\
    & [ \cdot \varepsilon \cdot ] S = \{(p,u) \in \mathcal{ES}(\chfont{Proc}) : \forall d \in \R_{\geq
    0} . \forall p' \in \chfont{Proc}. p \xrightarrow{d} p' \text{ implies }\\
    & \qquad\qquad\quad(p',u+d) \in S \}
  \end{align*}
  We write $(p,u) \models F$ iff $(p,u) \in \llbracket F \rrbracket$. Two formulae are \emph{equivalent} iff they are
  satisfied by the same extended states in every TLTS.
\end{definition}

\begin{definition}
A state $p$ in a TLTS satisfies a formula $F$, $p \models F$, iff $(p,u_0) \models F$, where $u_0$ is a clock valuation
mapping each formula clock to zero.
\end{definition}
The above definition can be applied to a TLTS $T(\mathcal{A})$ generated from a timed automaton $\mathcal{A}$. For this
TLTS, extended states take the form $((l,v),u)$ where $v$ is a valuation for the set of clocks $C$ in $\mathcal{A}$ and
$u$ is a valuation for the set of clocks $D$ used in writing the formulae of $\mathcal{M}_t$. We assume that $C$ and
$D$ are disjoint: $C \cap D = \emptyset$.

\begin{definition}\label{def:sat}
A timed automaton $\mathcal{A}$ satisfies a formula $F \in \mathcal{M}_t$ iff $((l_0,v_0),u_0) \models F$.\\
Where $l_0$ is the initial location in $\mathcal{A}$ and $v_0,u_0$ are clock valuations that map each clock variable
in the automaton and in the formula to 0. From now on, we'll use $\mathcal{A} \models F$ instead of 
$((l_0,v_0),u_0) \models F$.
\end{definition}
An alternative characterization of the satisfactory relation $\models$ can be obtained by definining it as relating
extended states to formulae by structural induction:
\begin{align*}
  & (p,u) \models \mathit{tt} \text{ for each } (p,u)\\
  & (p,u) \models \mathit{ff} \text{ for no } (p,u)\\
  & (p,u) \models F \land F \text{ iff } (p,u) \models F \text{ and } (p,u) \models G\\
  & (p,u) \models F \lor F \text{ iff } (p,u) \models F \text{ or } (p,u) \models G\\
  & (p,u) \models \langle a \rangle F \text{ iff } p \xrightarrow{a} p' \text{ for some } p' \text{ such that } (p',u)
  \models F\\
  & (p,u) \models [a] F \text{ iff whenever } p \xrightarrow{a} p' \text{ then } (p',u) \models F\\
  & (p,u) \models \mathrlap{\exists}\,\exists F \text{ iff } p \xrightarrow{d} p' \text { for some } p' \text{ and } d \in
  \R_{\geq 0} \text{ such that } (p',u+d) \models F\\
  & (p,u) \models \mathrlap{\forall}\,\forall F \text{ iff } (p',u+d) \models F \text{ for each } d \in \R_{\geq 0}
  \text{ and } p' \text{ such that } p \xrightarrow{d} p'\\
  & (p,u) \models y~\texttt{\underline{in}}~F \text{ iff } (p,u[y \mapsto 0]) \models F\\
  & (p,u) \models g \text{ iff } u \models g
\end{align*}

\subsection{Model checking}
In section~\ref{sec:reg_graph} we've seen that the concept of regions and region graphs enables us to prove that
reachability for timed automata is decidable. The notion of regions is also the key tool for proving the decidability
of model-checking problems for timed automata w.r.t. THML.

The model checking problem for THML consists in deciding if $((l,v),u) \models F$ where $(l,v)$ is a state of a timed
automaton $\mathcal{A}$, $l$ being a location of $\mathcal{A}$, $v$ and $u$ being respectively a valuation for the set
of clocks $C$ of $\mathcal{A}$ and for the set of formula clocks $D$, finally $F$ is a formula of $\mathcal{M}_t$. To
do this we'll consider \emph{symbolic model checking} problems of the form
\begin{equation*}
  [l,\gamma] \vdash F,
\end{equation*}
where $\gamma$ is a region over $C \cup D$, a region over the disjoint union of the set of automata and formula
clocks.\\
Let's introduce some notation on regions:
\begin{itemize}
  \item given a region $\gamma$ and a constraint $g$ we say that $\gamma$ satisfies $g$ ($\gamma \models g$), if $v
    \models g$ for some (or all) $v \in \gamma$;
  \item for two regions $\gamma$ and $\gamma'$ and a set of clocks $R$, we say that $y'$ is the reset of $\gamma$ with
    respect to $R$ ($\gamma' = \gamma[R]$), if $v[R] \in \gamma'$ for some (or all) $v \in \gamma$;
  \item given two regions $\gamma$ and $\gamma'$, we say that $\gamma'$ is a delay successor of $\gamma$, written
    $\gamma \leadsto \gamma'$, if for each $v \in \gamma$ there exists $d \in \R_{\geq 0}$ such that $v+d \in \gamma'$.
\end{itemize}

\begin{definition}
Let $\mathcal{A}$ be a timed automaton with clocks $C$, let's consider formulae over $\mathcal{M}_t$ with a set of
formula clocks $D$, where $C$ and $D$ are disjoint. If $l$ is a location of $\mathcal{A}$, $F$ is a formula and
  $\gamma$ a region over $C \cup D$ such that $\gamma \models I(l)$, we define \emph{symbolic satisfaction} $[l,\gamma] \vdash
F$ as follows:
  \begin{align*}
    & [l,\gamma] \vdash \mathit{tt} \text{ for each } [l,\gamma]\\
    & [l,\gamma] \vdash \mathit{ff} \text{ for no } [l,\gamma]\\
    & [l,\gamma] \vdash F \land G \text{ iff } [l,\gamma] \vdash F \text{ and } [l,\gamma] \vdash G\\
    & [l,\gamma] \vdash F \lor G \text{ iff } [l,\gamma] \vdash F \text{ or } [l,\gamma] \vdash G\\
    & [l,\gamma] \vdash \langle a \rangle F \text{ iff there is an edge } l \xrightarrow{g,a,R} l' \text{ in } \mathcal{A}
    \text{ with } \gamma \models g \text{ and } [l',\gamma[R]] \vdash F\\
    & [l,\gamma] \vdash [ a ] F \text{ iff whenever } l \xrightarrow{g,a,R} l' \text{ is an edge in } \mathcal{A}
    \text{ such that } \gamma \models g \text{ then } [l',\gamma[R]] \vdash F\\
    & [l,\gamma] \vdash \mathrlap{\exists}\,\exists F \text{ iff } \gamma \leadsto \gamma' \text{ for some } \gamma'
    \text{ such that } \gamma' \models I(l) \text{ and } [l,\gamma'] \vdash F\\
    & [l,\gamma] \vdash \mathrlap{\forall}\,\forall F \text{ iff whenever } \gamma \leadsto \gamma' \text{ with } 
    \gamma' \models I(l) \text{ and } [l,\gamma'] \vdash F
  \end{align*}
\end{definition}
The above symbolic satisfaction is closely related to the satisfaction relation given in definition~\ref{def:sat} as
stated in the following theorem:
\begin{theorem}
  Let $\mathcal{A}$ be a timed automaton with clock set $C$ and consider formulae over $\mathcal{M}_t$ with a set of
  formula clocks $D$, with $C$ and $D$ disjoint. Then
  \begin{equation*}
    ((l,v), u) \models F \text{\upshape\text{ iff }} [l,[vu]] \vdash F,
  \end{equation*}
  where $v$ is a valuation over $C$, $u$ is a valuation over $D$, and $vu$ is the valuation over $C \cup D$ such that
  $vu(z)$ equals $v(z)$ for $z \in C$ and $u(z)$ otherwise.
\end{theorem}
From this theorem and from the finiteness of the number of regions it follows that model checking for THML is
decidable.
\begin{theorem}
  THML model checking over timed automata is decidable.
\end{theorem}

\subsection{Recursion in THML}
Like Hennessy-Milner logic, its timed extension can be extended to handle recursively defined formulae. This allows us
to overcome the fact that the behaviour of a real-time system we can explore is determined by the modal depth of the
formula. Using recursively defined properties we can express \emph{safety} and \emph{invariant} properties. The syntax
of THML with one variable $X$ is given by the following grammar:
\begin{equation*}
  F ::= X~|~\mathit{tt}~|~\mathit{ff}~|~F \land G~|~F \lor G~|~\langle a \rangle F~|~[a]F~|~\mathrlap{\exists}\,\exists
  F~|~\mathrlap{\forall}\,\forall F~|~ x~\texttt{\underline{in}}~F~|~ g
\end{equation*}
As we've seen above we'll interpret formulae over the collection of extended states (\chfont{Proc}) associated with a 
given timed automaton $\mathcal{A}$. Semantically a formula $F$, which may contain a variable $X$ is interpreted as a
function $\mathcal{O}_F : \mathcal{ES}(\chfont{Proc}) \to \mathcal{ES}(\chfont{Proc})$, that given a set of extended
states that are assumed to satisfy $X$, gives us the set of extended states that satisfy F. The function
$\mathcal{O}_F$ is defined as follows.
\begin{definition}
  \begin{align*}
    \mathcal{O}_X(S) &= S\\
    \mathcal{O}_{\mathit{tt}}(S) &= \mathcal{ES}(\chfont{Proc})\\
    \mathcal{O}_{\mathit{ff}}(S) &= \emptyset\\
    \mathcal{O}_{F_1 \land F_2}(S) &= \mathcal{O}_{F_1}(S) \cap \mathcal{O}_{F_2}(S)\\
    \mathcal{O}_{F_1 \lor F_2}(S) &= \mathcal{O}_{F_1}(S) \cup \mathcal{O}_{F_2}(S)\\
    \mathcal{O}_{\langle a \rangle F}(S) &= \langle \cdot a \cdot \rangle \mathcal{O}_F(S)\\
    \mathcal{O}_{[ a ] F}(S) &= [ \cdot a \cdot ] \mathcal{O}_F(S)\\
    \mathcal{O}_{\mathrlap{\exists}\,\exists F}(S) &= \langle \cdot \varepsilon \cdot \rangle \mathcal{O}_F(S)\\
    \mathcal{O}_{\mathrlap{\forall}\,\forall F}(S) &= [ \cdot \varepsilon \cdot ] \mathcal{O}_F(S)\\
    \mathcal{O}_{x~\texttt{\underline{in}}~F}(S) &= \{(p,u) : (p,u[x \mapsto 0]) \in \mathcal{O}_F(S) \}\\
    \mathcal{O}_g(S) &= \{ (p,u) : u \models g \}
  \end{align*}
\end{definition}
\begin{theorem}
  The model checking problem for $\mathcal{M}_t$ over timed automata is \textsc{PSPACE}-complete~\cite{aceto2002your}.
\end{theorem}

\section{Conclusions}
In conclusion, we have introduced the well established formalism for modelling real-time systems (i.e. timed automata), 
we've described its properties and using the region graph technique introduced in~\cite{alur1991techniques,
alur1994theory} we've seen that the reachability problem for timed automata is decidable and \textsc{PSPACE}-complete.
In the same articles Alur and Dill also prove that the inclusion problem for timed automata is \textsc{co-NP}-complete
and that the class of timed regular languages are not closed under complementation. In section~\ref{sec:thml}, we've 
seen one of many formalims built on top of timed-automata for describing properties of reactive real-time systems, namely the timed 
extension of Hennessy-Milner logic, originally introduced in~\cite{laroussinie1995timed}. Using the concept of region 
graphs we've seen that the model-checking problem for THML over timed-automata is decidable and
\textsc{PSPACE}-complete~\cite{aceto2002your}.\\
There has been an extensive research on extending temporal logic to the setting of real time. Like timed automata,
temporal logic has been extended by adding quantitative timing information. The main extensions of LTL are timed
propositional temporal logic (TPTL) and metric temporal logic (MTL). A timed version of CTL, knows as TCTL has been
developed together with model-checking algorithms.

\newpage
\bibliographystyle{alpha}
\bibliography{biblio}
\nocite{*}
\end{document}

A  => slides/Makefile +13 -0
@@ 1,13 @@
all: bib

.PHONY: clean

pdf:
	-pdflatex slides.tex

bib: pdf
	-bibtex slides.aux
	-pdflatex slides.tex

clean:
	rm -f *.bbl *.blg *.idx *.lof *.log *.out report.pdf *.aux

A  => slides/UdineLogo.pdf +0 -0

A  => slides/UdineLogoFull.pdf +0 -0

A  => slides/beamer.thud.tex +54 -0
@@ 1,54 @@
\def\thud@unisep{0pt}
\def\thud@se@and{0pt}
\def\thud@se@qual{.5ex}
\def\thud@se@sep{1em}

%% Copied and adapted from beamerbasetitle.sty
\long\def\beamer@author[#1]#2{%
    \def\@author{#2}%
    \def\beamer@shortauthor{#1}%
    \ifbeamer@autopdfinfo%
        \def\beamer@andstripped{}%
        \beamer@stripands#2 \and\relax
        {\let\inst=\@gobble\let\thanks=\@gobble\def\and{, }\hypersetup{pdfauthor={\beamer@andstripped}}}
    \fi%
}
%% Copied and adapted from beamerbasetitle.sty
\long\def\beamer@institute[#1]#2{%
    \def\beamer@temp{#2}%
    \ifx\beamer@temp\@empty
        \def\insertinstitute{}
    \else
        \def\insertinstitute{#2}%
    \fi
    \def\beamer@shortinstitute{#1}%
}
%% Copied and adapted from beamerbasetitle.sty
\long\def\beamer@date[#1]#2{%
    \def\@date{#2}%
    \def\beamer@shortdate{#1}%
}

\institute[UniUD]{\thud@universityA}

\def\insertdate{\ifx\thud@cycle\@empty\datename\else\cyclename~\thud@cycle\ --- \shortdatename\fi~\@date}
\def\insertshortdate{\shortdatename~\@date}
\def\insertauthor{%
    \parbox[c]{.26\linewidth}{\centering%
        \let\thud@candidate\@author
        \thud@showentry*{candidate}%
    }
}

\renewcommand\maketitle[1][]{%
    \begingroup%
    \setbeamertemplate{background canvas}{%
        \parbox[c][\paperheight]{\paperwidth}{\centering%
            \includegraphics[height=.9\paperheight,width=.9\paperwidth,keepaspectratio]{UdineLogoFull}%
        }%
    }%
    \def\thud@tmpcmd{#1}%
    \ifx\@empty\thud@tmpcmd\def\thud@tmpcmd{environment=}\fi%
    \expandafter\frame\expandafter[\thud@tmpcmd]{\titlepage}%
    \endgroup%
}

A  => slides/biblio.bib +93 -0
@@ 1,93 @@
  title={{CCS} + time = an interleaving model for real time systems},
  author={Yi, Wang},
  booktitle={International Colloquium on Automata, Languages, and Programming},
  pages={217--228},
  year={1991},
  organization={Springer}
}

  title={Communication and concurrency},
  author={Milner, Robin},
  volume={84},
  year={1989},
  publisher={Prentice hall New York etc.}
}

@phdthesis{alur1991techniques,
  title={Techniques for automatic verification of real-time systems},
  author={Alur, Rajeev},
  year={1991},
  school={stanford university}
}

@article{alur1994theory,
  title={A theory of timed automata},
  author={Alur, Rajeev and Dill, David L},
  journal={Theoretical computer science},
  volume={126},
  number={2},
  pages={183--235},
  year={1994},
  publisher={Elsevier}
}

@article{larsen1997uppaal,
  title={UPPAAL in a nutshell},
  author={Larsen, Kim G and Pettersson, Paul and Yi, Wang},
  journal={International Journal on Software Tools for Technology Transfer (STTT)},
  volume={1},
  number={1},
  pages={134--152},
  year={1997},
  publisher={Springer}
}

@inproceedings{bozga1998kronos,
  title={Kronos: A model-checking tool for real-time systems},
  author={Bozga, Marius and Daws, Conrado and Maler, Oded and Olivero, Alfredo and Tripakis, Stavros and Yovine,
      Sergio},
  booktitle={International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems},
  pages={298--302},
  year={1998},
  organization={Springer}
}

@inproceedings{daws1995tool,
  title={The tool KRONOS},
  author={Daws, Conrado and Olivero, Alfredo and Tripakis, Stavros and Yovine, Sergio},
  booktitle={International Hybrid Systems Workshop},
  pages={208--219},
  year={1995},
  organization={Springer}
}

@inproceedings{laroussinie1995timed,
  title={From timed automata to logic—and back},
  author={Laroussinie, Fran{\c{c}}ois and Larsen, Kim G and Weise, Carsten},
  booktitle={International Symposium on Mathematical Foundations of Computer Science},
  pages={529--539},
  year={1995},
  organization={Springer}
}

@article{aceto2002your,
  title={Is your model checker on time? On the complexity of model checking for timed modal logics},
  author={Aceto, Luca and Laroussinie, Fran{\c{c}}ois},
  journal={The Journal of Logic and Algebraic Programming},
  volume={52},
  pages={7--51},
  year={2002},
  publisher={Elsevier}
}

@article{hennessy1985algebraic,
  title={Algebraic laws for nondeterminism and concurrency},
  author={Hennessy, Matthew and Milner, Robin},
  journal={Journal of the ACM (JACM)},
  volume={32},
  number={1},
  pages={137--161},
  year={1985},
  publisher={ACM}
}


A  => slides/book.thud.tex +248 -0
@@ 1,248 @@
\def\thud@unisep{.5em}
\def\thud@se@and{.2ex}
\def\thud@se@qual{1ex}
\def\thud@se@sep{2em}

\geometry{%
    hcentering,%
    bindingoffset=.025\paperwidth,%
    outer=.075\paperwidth,%
    nofoot,nomarginpar,%
    vdivide={.08\paperheight,*,.06\paperheight}%
}

\ifthud@phd\let\thud@spacing\singlespacing\else\def\thud@spacing{\setstretch{1.3}}\fi

\def\thud@newpagestyle#1#2{
    \@namedef{ps@#1}{
        \let\@oddfoot\@empty
        \let\@evenfoot\@empty
        \let\@mkboth\markboth
        \let\ps@plain\ps@empty%
        \@nameuse{thud@chs@#1}%
        \@nameuse{thud@pts@#1}%
        #2%
    }
}

\def\chaptermark#1{\ifnum\c@secnumdepth>\m@ne\relax\def\thud@tmpcmd{\thechapter. \ #1}\else\let\thud@tmpcmd\@empty\fi\markboth{\thud@tmpcmd}{\thud@tmpcmd}}
\def\sectionmark#1{\markright{\ifnum\c@secnumdepth>\z@\relax\thesection. \ \fi#1}}

\def\thud@headruledbox#1#2#3{\underline{\makebox[\textwidth]{%
    {\small#1\bfseries#2\hfill#3}\rule[-0.5ex]{0pt}{1ex}%
}}}
\def\thud@defheads#1{%
    \def\@evenhead{\thud@headruledbox{#1}\thepage\leftmark}%
    \def\@oddhead{\thud@headruledbox{#1}\rightmark\thepage}%
}

\let\ps@bookplain\ps@plain

\thud@newpagestyle{plain}{\thud@defheads\relax}
\thud@newpagestyle{big}{\thud@defheads\relax}
\thud@newpagestyle{sfbig}{\thud@defheads\sffamily}

\def\thud@declgigantic{\DeclareFontShape{T1}{cmr}{ch}{n}{<-> cmr17}{}}
\def\thud@gigantic{\fontsize{99.45}{100\p@}\usefont{T1}{cmr}{ch}{n}}

\thud@save{@makechapterhead}
\thud@save{@makeschapterhead}
\long\def\thud@mkchaphdstub#1#2#3{%
    {\parindent\z@\relax
    \raggedleft\normalfont
    \vspace*{30\p@}%
    #1%% Either \iftrue or \iffalse
        \ifnum\c@secnumdepth>\m@ne\relax
            \if@mainmatter
                {\thud@gigantic\thechapter}\Huge\par\nobreak\vskip15\p@\relax\hrule\vskip15\p@\relax%
            \fi%
        \fi%
    \fi%
    \interlinepenalty\@M\relax%
    \Huge\bfseries#2#3\par\nobreak%
    \vskip40\p@\relax}%
}
\long\def\thud@defmakechapterhead#1{
    \thud@declgigantic%
    \def\@makechapterhead##1{\expandafter\thud@mkchaphdstub\noexpand\iftrue{#1}{##1}}
    \def\@makeschapterhead##1{\expandafter\thud@mkchaphdstub\noexpand\iffalse{#1}{##1}}
}

\def\thud@chs@plain{%
    \thud@restore{@makechapterhead}
    \thud@restore{@makeschapterhead}
}
\def\thud@chs@big{\thud@defmakechapterhead\relax}
\def\thud@chs@sfbig{\thud@defmakechapterhead\sffamily}

\thud@save{@part}
\thud@save{@spart}
\long\def\thud@spartstub#1#2{
    {\raggedleft
    \interlinepenalty\@M\relax
    \normalfont%
    #1%% Either \iftrue or \iffalse
        \ifnum\c@secnumdepth>-2\relax
            \if@mainmatter
                {\thud@gigantic\thepart\par\vskip20\p@\relax\hrule\vskip20\p@\relax}%
            \fi%
        \fi%
    \else%
        \hrule\vskip20\p@\relax%
    \fi%
    \Huge\bfseries#2\par}%
    \@endpart%
}
\def\thud@defpartstub#1{
    \def\@part[##1]##2{
        \ifnum\c@secnumdepth>-2\relax
            \refstepcounter{part}%
            \addcontentsline{toc}{part}{\thepart\hspace{1em}##1}%
        \else
            \addcontentsline{toc}{part}{##1}%
        \fi%
        \markboth{}{}%
        \expandafter\thud@spartstub\noexpand\iftrue{#1##2}%
    }
    \def\@spart##1{
        \expandafter\thud@spartstub\noexpand\iffalse{#1##1}%
    }
}

\def\thud@pts@plain{%
    \thud@restore{@part}
    \thud@restore{@spart}
}
\def\thud@pts@big{%
    \thud@declgigantic%
    \thud@defpartstub\relax
}
\def\thud@pts@sfbig{%
    \thud@declgigantic%
    \thud@defpartstub\sffamily
}

\def\printindex{\InputIfFileExists{\jobname.ind}{}{\ClassWarningNoLine{\@currname}{No file \jobname.ind.}}}

\newif\ifthud@endpart
\def\maybeblank{\ifthud@endpart\else\ifodd\c@page\@endpart\fi\fi\global\thud@endpartfalse}
\g@addto@macro\@endpart{\global\thud@endparttrue}
\def\thud@patchMatter#1{%
    \thud@save{#1matter}
    \@namedef{#1matter}{%
        \thud@save{cleardoublepage}
        \def\cleardoublepage{\maybeblank\thud@endparttrue}
        \@nameuse{thud@save@#1matter}
        \thud@restore{cleardoublepage}
    }
}
\thud@patchMatter{main}
\thud@patchMatter{back}
\thud@save{part}
\def\part{\maybeblank\thud@save@part}

\newcounter{thud@secnumdepth}
\newif\ifthud@unnmkchp
\thud@save{chapter}
\def\chapter{\maybeblank\@ifplus{\thud@unnmkchptrue\thud@save@chapter}{\thud@unnmkchpfalse\thud@save@chapter}}
\thud@save{@chapter}
\def\@chapter[#1]#2{%
    \ifthud@unnmkchp\c@thud@secnumdepth=\c@secnumdepth\relax\c@secnumdepth=-100\relax\fi%
    \thud@save@@chapter[#1]{#2}%
    \ifthud@unnmkchp\c@secnumdepth=\c@thud@secnumdepth\relax\fi%
}
\thud@save{@schapter}
\def\@schapter#1{\thud@save@@schapter{#1\ifthud@unnmkchp\@mkboth{#1}{#1}\fi}}

\def\abstract{\chapter+*{\abstractname}}
\def\acknowledgements{\chapter+*{\acknowledgementsname}}
\def\summary{\chapter+*{\summaryname}}

\newenvironment{titlelike}[1]{
    \cleardoublepage\thispagestyle{empty}%
    \def\thud@titlelike{#1}%
    \vspace*{\z@\@plus.3fil}%
    \begin{\thud@titlelike}%
}{
    \end{\thud@titlelike}%
    \vspace*{\z@\@plus.6fil}%
    \newpage\thispagestyle{empty}%
}
\newenvironment{approval}{\begin{titlelike}{center}}{\end{titlelike}}
\newenvironment{dedication}{\begin{titlelike}{flushright}}{\end{titlelike}}

\def\thud@patchNoUc#1{
    \thud@save{#1}
    \@namedef{#1}{
        \thud@save{MakeUppercase}
        \let\MakeUppercase\@iden
        \@nameuse{thud@save@#1}%
        \thud@restore{MakeUppercase}
    }
}
\def\thud@patchNoUcI#1{%
    \thud@save{#1}
    \@namedef{#1}##1{
        \thud@save{MakeUppercase}
        \let\MakeUppercase\@iden
        \@nameuse{thud@save@#1}{##1}%
        \thud@restore{MakeUppercase}
    }
}
\thud@patchNoUc{tableofcontents}
\thud@patchNoUc{listoffigures}
\thud@patchNoUc{listoftables}
\thud@patchNoUc{theindex}
\thud@patchNoUcI{thebibliography}

\thud@save{@starttoc}
\def\@starttoc#1{\singlespacing\thud@save@@starttoc{#1}\thud@spacing}

\def\maketitle{
    \begin{titlepage}%
        \noindent%
        \ifpdf\makebox[\z@][l]{\raisebox{-.98\textheight}[\z@][\z@]{\includegraphics[height=\textheight]{UdineLogo}}}\fi%
        \begin{minipage}[t][\textheight][s]{.99\linewidth}%
            \let\footnotesize\small
            \let\footnoterule\relax
            {\Large\textsc{\thud@universityA}}%
            \ifx\thud@chair\@empty\else\par\medskip\chairname: \thud@chair\fi%
            \vfill%
            \begin{center}%
                {\large\textsc{\thesisname\ifx\thud@phdnumber\@empty\else\space\thud@phdnumber\fi}\par}
                \vskip 4em\relax%
                {\huge\bfseries\@title\par}
                \vskip 5em\@plus1fill\relax%
                {\large%
                    \parbox[t]{.4\linewidth}{%
                        \let\thud@candidate\@author
                        \thud@showentry*{candidate}%
                    }%
                    \quad%
                    \parbox[t]{.4\linewidth}{%
                        \thud@showentry{supervisor}%
                        \thud@showentry{cosupervisor}%
                        \thud@showentry{tutor}%
                        \thud@showentry{reviewer}%
                    }%
                }
                \par\vskip 1em\@plus1fill\relax%
                {\large\ifx\thud@cycle\@empty\datename\else\cyclename~\thud@cycle\ --- \shortdatename\fi~\@date}\par
            \end{center}%
        \end{minipage}%
    \end{titlepage}
    \thispagestyle{empty}%
    \setcounter{footnote}{0}
    {\parindent\z@\relax%
        \textsc{\institutecontactsname}\\\thud@universityB\par%
        \ifx\thud@contacts\@empty\else\vskip2em\relax\textsc{\authorcontactsname}\\\thud@contacts\par\fi%
        \ifx\thud@rights\@empty\else\vfill\thud@rights\par\fi%
    }%
    \thud@spacing%
    \let\thanks\relax\let\maketitle\relax
}

\AtBeginDocument{%
    \pagestyle{sfbig}%
    \frontmatter%
}

A  => slides/plain_english.bst +1097 -0
@@ 1,1097 @@
% BibTeX standard bibliography style `plain'
	% version 0.99a for BibTeX versions 0.99a or later, LaTeX version 2.09.
	% Copyright (C) 1985, all rights reserved.
	% Copying of this file is authorized only if either
	% (1) you make absolutely no changes to your copy, including name, or
	% (2) if you do make changes, you name it something other than
	% btxbst.doc, plain.bst, unsrt.bst, alpha.bst, and abbrv.bst.
	% This restriction helps ensure that all standard styles are identical.
	% The file btxbst.doc has the documentation for this style.

ENTRY
  { address
    author
    booktitle
    chapter
    edition
    editor
    howpublished
    institution
    journal
    key
    month
    note
    number
    organization
    pages
    publisher
    school
    series
    title
    type
    volume
    year
  }
  {}
  { label }

INTEGERS { output.state before.all mid.sentence after.sentence after.block }

FUNCTION {init.state.consts}
{ #0 'before.all :=
  #1 'mid.sentence :=
  #2 'after.sentence :=
  #3 'after.block :=
}

STRINGS { s t }

FUNCTION {output.nonnull}
{ 's :=
  output.state mid.sentence =
    { ", " * write$ }
    { output.state after.block =
	{ add.period$ write$
	  newline$
	  "\newblock " write$
	}
	{ output.state before.all =
	    'write$
	    { add.period$ " " * write$ }
	  if$
	}
      if$
      mid.sentence 'output.state :=
    }
  if$
  s
}

FUNCTION {output}
{ duplicate$ empty$
    'pop$
    'output.nonnull
  if$
}

FUNCTION {output.check}
{ 't :=
  duplicate$ empty$
    { pop$ "empty " t * " in " * cite$ * warning$ }
    'output.nonnull
  if$
}

FUNCTION {output.bibitem}
{ newline$
  "\bibitem{" write$
  cite$ write$
  "}" write$
  newline$
  ""
  before.all 'output.state :=
}

FUNCTION {fin.entry}
{ add.period$
  write$
  newline$
}

FUNCTION {new.block}
{ output.state before.all =
    'skip$
    { after.block 'output.state := }
  if$
}

FUNCTION {new.sentence}
{ output.state after.block =
    'skip$
    { output.state before.all =
	'skip$
	{ after.sentence 'output.state := }
      if$
    }
  if$
}

FUNCTION {not}
{   { #0 }
    { #1 }
  if$
}

FUNCTION {and}
{   'skip$
    { pop$ #0 }
  if$
}

FUNCTION {or}
{   { pop$ #1 }
    'skip$
  if$
}

FUNCTION {new.block.checka}
{ empty$
    'skip$
    'new.block
  if$
}

FUNCTION {new.block.checkb}
{ empty$
  swap$ empty$
  and
    'skip$
    'new.block
  if$
}

FUNCTION {new.sentence.checka}
{ empty$
    'skip$
    'new.sentence
  if$
}

FUNCTION {new.sentence.checkb}
{ empty$
  swap$ empty$
  and
    'skip$
    'new.sentence
  if$
}

FUNCTION {field.or.null}
{ duplicate$ empty$
    { pop$ "" }
    'skip$
  if$
}

FUNCTION {emphasize}
{ duplicate$ empty$
    { pop$ "" }
    { "{\em " swap$ * "}" * }
  if$
}

INTEGERS { nameptr namesleft numnames }

FUNCTION {format.names}
{ 's :=
  #1 'nameptr :=
  s num.names$ 'numnames :=
  numnames 'namesleft :=
    { namesleft #0 > }
    { s nameptr "{ff~}{vv~}{ll}{, jj}" format.name$ 't :=
      nameptr #1 >
	{ namesleft #1 >
	    { ", " * t * }
	    { numnames #2 >
		{ "," * }
		'skip$
	      if$
	      t "others" =
		{ " et~al." * }
		{ " and " * t * }
	      if$
	    }
	  if$
	}
	't
      if$
      nameptr #1 + 'nameptr :=
      namesleft #1 - 'namesleft :=
    }
  while$
}

FUNCTION {format.authors}
{ author empty$
    { "" }
    { author format.names }
  if$
}

FUNCTION {format.editors}
{ editor empty$
    { "" }
    { editor format.names
      editor num.names$ #1 >
	{ ", editors" * }
	{ ", editor" * }
      if$
    }
  if$
}

FUNCTION {format.title}
{ title empty$
    { "" }
    { title "t" change.case$ }
  if$
}

FUNCTION {n.dashify}
{ 't :=
  ""
    { t empty$ not }
    { t #1 #1 substring$ "-" =
	{ t #1 #2 substring$ "--" = not
	    { "--" *
	      t #2 global.max$ substring$ 't :=
	    }
	    {   { t #1 #1 substring$ "-" = }
		{ "-" *
		  t #2 global.max$ substring$ 't :=
		}
	      while$
	    }
	  if$
	}
	{ t #1 #1 substring$ *
	  t #2 global.max$ substring$ 't :=
	}
      if$
    }
  while$
}

FUNCTION {format.date}
{ year empty$
    { month empty$
	{ "" }
	{ "there's a month but no year in " cite$ * warning$
	  month
	}
      if$
    }
    { month empty$
	'year
	{ month " " * year * }
      if$
    }
  if$
}

FUNCTION {format.btitle}
{ title emphasize
}

FUNCTION {tie.or.space.connect}
{ duplicate$ text.length$ #3 <
    { "~" }
    { " " }
  if$
  swap$ * *
}

FUNCTION {either.or.check}
{ empty$
    'pop$
    { "can't use both " swap$ * " fields in " * cite$ * warning$ }
  if$
}

FUNCTION {format.bvolume}
{ volume empty$
    { "" }
    { "volume" volume tie.or.space.connect
      series empty$
	'skip$
	{ " of " * series emphasize * }
      if$
      "volume and number" number either.or.check
    }
  if$
}

FUNCTION {format.number.series}
{ volume empty$
    { number empty$
	{ series field.or.null }
	{ output.state mid.sentence =
	    { "number" }
	    { "Number" }
	  if$
	  number tie.or.space.connect
	  series empty$
	    { "there's a number but no series in " cite$ * warning$ }
	    { " in " * series * }
	  if$
	}
      if$
    }
    { "" }
  if$
}

FUNCTION {format.edition}
{ edition empty$
    { "" }
    { output.state mid.sentence =
	{ edition "l" change.case$ " edition" * }
	{ edition "t" change.case$ " edition" * }
      if$
    }
  if$
}

INTEGERS { multiresult }

FUNCTION {multi.page.check}
{ 't :=
  #0 'multiresult :=
    { multiresult not
      t empty$ not
      and
    }
    { t #1 #1 substring$
      duplicate$ "-" =
      swap$ duplicate$ "," =
      swap$ "+" =
      or or
	{ #1 'multiresult := }
	{ t #2 global.max$ substring$ 't := }
      if$
    }
  while$
  multiresult
}

FUNCTION {format.pages}
{ pages empty$
    { "" }
    { pages multi.page.check
	{ "pages" pages n.dashify tie.or.space.connect }
	{ "page" pages tie.or.space.connect }
      if$
    }
  if$
}

FUNCTION {format.vol.num.pages}
{ volume field.or.null
  number empty$
    'skip$
    { "(" number * ")" * *
      volume empty$
	{ "there's a number but no volume in " cite$ * warning$ }
	'skip$
      if$
    }
  if$
  pages empty$
    'skip$
    { duplicate$ empty$
	{ pop$ format.pages }
	{ ":" * pages n.dashify * }
      if$
    }
  if$
}

FUNCTION {format.chapter.pages}
{ chapter empty$
    'format.pages
    { type empty$
	{ "chapter" }
	{ type "l" change.case$ }
      if$
      chapter tie.or.space.connect
      pages empty$
	'skip$
	{ ", " * format.pages * }
      if$
    }
  if$
}

FUNCTION {format.in.ed.booktitle}
{ booktitle empty$
    { "" }
    { editor empty$
	{ "In " booktitle emphasize * }
	{ "In " format.editors * ", " * booktitle emphasize * }
      if$
    }
  if$
}

FUNCTION {empty.misc.check}
{ author empty$ title empty$ howpublished empty$
  month empty$ year empty$ note empty$
  and and and and and
  key empty$ not and
    { "all relevant fields are empty in " cite$ * warning$ }
    'skip$
  if$
}

FUNCTION {format.thesis.type}
{ type empty$
    'skip$
    { pop$
      type "t" change.case$
    }
  if$
}

FUNCTION {format.tr.number}
{ type empty$
    { "Technical Report" }
    'type
  if$
  number empty$
    { "t" change.case$ }
    { number tie.or.space.connect }
  if$
}

FUNCTION {format.article.crossref}
{ key empty$
    { journal empty$
	{ "need key or journal for " cite$ * " to crossref " * crossref *
	  warning$
	  ""
	}
	{ "In {\em " journal * "\/}" * }
      if$
    }
    { "In " key * }
  if$
  " \cite{" * crossref * "}" *
}

FUNCTION {format.crossref.editor}
{ editor #1 "{vv~}{ll}" format.name$
  editor num.names$ duplicate$
  #2 >
    { pop$ " et~al." * }
    { #2 <
	'skip$
	{ editor #2 "{ff }{vv }{ll}{ jj}" format.name$ "others" =
	    { " et~al." * }
	    { " and " * editor #2 "{vv~}{ll}" format.name$ * }
	  if$
	}
      if$
    }
  if$
}

FUNCTION {format.book.crossref}
{ volume empty$
    { "empty volume in " cite$ * "'s crossref of " * crossref * warning$
      "In "
    }
    { "Volume" volume tie.or.space.connect
      " of " *
    }
  if$
  editor empty$
  editor field.or.null author field.or.null =
  or
    { key empty$
	{ series empty$
	    { "need editor, key, or series for " cite$ * " to crossref " *
	      crossref * warning$
	      "" *
	    }
	    { "{\em " * series * "\/}" * }
	  if$
	}
	{ key * }
      if$
    }
    { format.crossref.editor * }
  if$
  " \cite{" * crossref * "}" *
}

FUNCTION {format.incoll.inproc.crossref}
{ editor empty$
  editor field.or.null author field.or.null =
  or
    { key empty$
	{ booktitle empty$
	    { "need editor, key, or booktitle for " cite$ * " to crossref " *
	      crossref * warning$
	      ""
	    }
	    { "In {\em " booktitle * "\/}" * }
	  if$
	}
	{ "In " key * }
      if$
    }
    { "In " format.crossref.editor * }
  if$
  " \cite{" * crossref * "}" *
}

FUNCTION {article}
{ output.bibitem
  format.authors "author" output.check
  new.block
  format.title "title" output.check
  new.block
  crossref missing$
    { journal emphasize "journal" output.check
      format.vol.num.pages output
      format.date "year" output.check
    }
    { format.article.crossref output.nonnull
      format.pages output
    }
  if$
  new.block
  note output
  fin.entry
}

FUNCTION {book}
{ output.bibitem
  author empty$
    { format.editors "author and editor" output.check }
    { format.authors output.nonnull
      crossref missing$
	{ "author and editor" editor either.or.check }
	'skip$
      if$
    }
  if$
  new.block
  format.btitle "title" output.check
  crossref missing$
    { format.bvolume output
      new.block
      format.number.series output
      new.sentence
      publisher "publisher" output.check
      address output
    }
    { new.block
      format.book.crossref output.nonnull
    }
  if$
  format.edition output
  format.date "year" output.check
  new.block
  note output
  fin.entry
}

FUNCTION {booklet}
{ output.bibitem
  format.authors output
  new.block
  format.title "title" output.check
  howpublished address new.block.checkb
  howpublished output
  address output
  format.date output
  new.block
  note output
  fin.entry
}

FUNCTION {inbook}
{ output.bibitem
  author empty$
    { format.editors "author and editor" output.check }
    { format.authors output.nonnull
      crossref missing$
	{ "author and editor" editor either.or.check }
	'skip$
      if$
    }
  if$
  new.block
  format.btitle "title" output.check
  crossref missing$
    { format.bvolume output
      format.chapter.pages "chapter and pages" output.check
      new.block
      format.number.series output
      new.sentence
      publisher "publisher" output.check
      address output
    }
    { format.chapter.pages "chapter and pages" output.check
      new.block
      format.book.crossref output.nonnull
    }
  if$
  format.edition output
  format.date "year" output.check
  new.block
  note output
  fin.entry
}

FUNCTION {incollection}
{ output.bibitem
  format.authors "author" output.check
  new.block
  format.title "title" output.check
  new.block
  crossref missing$
    { format.in.ed.booktitle "booktitle" output.check
      format.bvolume output
      format.number.series output
      format.chapter.pages output
      new.sentence
      publisher "publisher" output.check
      address output
      format.edition output
      format.date "year" output.check
    }
    { format.incoll.inproc.crossref output.nonnull
      format.chapter.pages output
    }
  if$
  new.block
  note output
  fin.entry
}

FUNCTION {inproceedings}
{ output.bibitem
  format.authors "author" output.check
  new.block
  format.title "title" output.check
  new.block
  crossref missing$
    { format.in.ed.booktitle "booktitle" output.check
      format.bvolume output
      format.number.series output
      format.pages output
      address empty$
	{ organization publisher new.sentence.checkb
	  organization output
	  publisher output
	  format.date "year" output.check
	}
	{ address output.nonnull
	  format.date "year" output.check
	  new.sentence
	  organization output
	  publisher output
	}
      if$
    }
    { format.incoll.inproc.crossref output.nonnull
      format.pages output
    }
  if$
  new.block
  note output
  fin.entry
}

FUNCTION {conference} { inproceedings }

FUNCTION {manual}
{ output.bibitem
  author empty$
    { organization empty$
	'skip$
	{ organization output.nonnull
	  address output
	}
      if$
    }
    { format.authors output.nonnull }
  if$
  new.block
  format.btitle "title" output.check
  author empty$
    { organization empty$
	{ address new.block.checka
	  address output
	}
	'skip$
      if$
    }
    { organization address new.block.checkb
      organization output
      address output
    }
  if$
  format.edition output
  format.date output
  new.block
  note output
  fin.entry
}

FUNCTION {mastersthesis}
{ output.bibitem
  format.authors "author" output.check
  new.block
  format.title "title" output.check
  new.block
  "Master's thesis" format.thesis.type output.nonnull
  school "school" output.check
  address output
  format.date "year" output.check
  new.block
  note output
  fin.entry
}

FUNCTION {misc}
{ output.bibitem
  format.authors output
  title howpublished new.block.checkb
  format.title output
  howpublished new.block.checka
  howpublished output
  format.date output
  new.block
  note output
  fin.entry
  empty.misc.check
}

FUNCTION {phdthesis}
{ output.bibitem
  format.authors "author" output.check
  new.block
  format.btitle "title" output.check
  new.block
  "PhD thesis" format.thesis.type output.nonnull
  school "school" output.check
  address output
  format.date "year" output.check
  new.block
  note output
  fin.entry
}

FUNCTION {proceedings}
{ output.bibitem
  editor empty$
    { organization output }
    { format.editors output.nonnull }
  if$
  new.block
  format.btitle "title" output.check
  format.bvolume output
  format.number.series output
  address empty$
    { editor empty$
	{ publisher new.sentence.checka }
	{ organization publisher new.sentence.checkb
	  organization output
	}
      if$
      publisher output
      format.date "year" output.check
    }
    { address output.nonnull
      format.date "year" output.check
      new.sentence
      editor empty$
	'skip$
	{ organization output }
      if$
      publisher output
    }
  if$
  new.block
  note output
  fin.entry
}

FUNCTION {techreport}
{ output.bibitem
  format.authors "author" output.check
  new.block
  format.title "title" output.check
  new.block
  format.tr.number output.nonnull
  institution "institution" output.check
  address output
  format.date "year" output.check
  new.block
  note output
  fin.entry
}

FUNCTION {unpublished}
{ output.bibitem
  format.authors "author" output.check
  new.block
  format.title "title" output.check
  new.block
  note "note" output.check
  format.date output
  fin.entry
}

FUNCTION {default.type} { misc }

MACRO {jan} {"January"}

MACRO {feb} {"February"}

MACRO {mar} {"March"}

MACRO {apr} {"April"}

MACRO {may} {"May"}

MACRO {jun} {"June"}

MACRO {jul} {"July"}

MACRO {aug} {"August"}

MACRO {sep} {"September"}

MACRO {oct} {"October"}

MACRO {nov} {"November"}

MACRO {dec} {"December"}

MACRO {acmcs} {"ACM Computing Surveys"}

MACRO {acta} {"Acta Informatica"}

MACRO {cacm} {"Communications of the ACM"}

MACRO {ibmjrd} {"IBM Journal of Research and Development"}

MACRO {ibmsj} {"IBM Systems Journal"}

MACRO {ieeese} {"IEEE Transactions on Software Engineering"}

MACRO {ieeetc} {"IEEE Transactions on Computers"}

MACRO {ieeetcad}
 {"IEEE Transactions on Computer-Aided Design of Integrated Circuits"}

MACRO {ipl} {"Information Processing Letters"}

MACRO {jacm} {"Journal of the ACM"}

MACRO {jcss} {"Journal of Computer and System Sciences"}

MACRO {scp} {"Science of Computer Programming"}

MACRO {sicomp} {"SIAM Journal on Computing"}

MACRO {tocs} {"ACM Transactions on Computer Systems"}

MACRO {tods} {"ACM Transactions on Database Systems"}

MACRO {tog} {"ACM Transactions on Graphics"}

MACRO {toms} {"ACM Transactions on Mathematical Software"}

MACRO {toois} {"ACM Transactions on Office Information Systems"}

MACRO {toplas} {"ACM Transactions on Programming Languages and Systems"}

MACRO {tcs} {"Theoretical Computer Science"}

READ

FUNCTION {sortify}
{ purify$
  "l" change.case$
}

INTEGERS { len }

FUNCTION {chop.word}
{ 's :=
  'len :=
  s #1 len substring$ =
    { s len #1 + global.max$ substring$ }
    's
  if$
}

FUNCTION {sort.format.names}
{ 's :=
  #1 'nameptr :=
  ""
  s num.names$ 'numnames :=
  numnames 'namesleft :=
    { namesleft #0 > }
    { nameptr #1 >
	{ "   " * }
	'skip$
      if$
      s nameptr "{vv{ } }{ll{ }}{  ff{ }}{  jj{ }}" format.name$ 't :=
      nameptr numnames = t "others" = and
	{ "et al" * }
	{ t sortify * }
      if$
      nameptr #1 + 'nameptr :=
      namesleft #1 - 'namesleft :=
    }
  while$
}

FUNCTION {sort.format.title}
{ 't :=
  "A " #2
    "An " #3
      "The " #4 t chop.word
    chop.word
  chop.word
  sortify
  #1 global.max$ substring$
}

FUNCTION {author.sort}
{ author empty$
    { key empty$
	{ "to sort, need author or key in " cite$ * warning$
	  ""
	}
	{ key sortify }
      if$
    }
    { author sort.format.names }
  if$
}

FUNCTION {author.editor.sort}
{ author empty$
    { editor empty$
	{ key empty$
	    { "to sort, need author, editor, or key in " cite$ * warning$
	      ""
	    }
	    { key sortify }
	  if$
	}
	{ editor sort.format.names }
      if$
    }
    { author sort.format.names }
  if$
}

FUNCTION {author.organization.sort}
{ author empty$
    { organization empty$
	{ key empty$
	    { "to sort, need author, organization, or key in " cite$ * warning$
	      ""
	    }
	    { key sortify }
	  if$
	}
	{ "The " #4 organization chop.word sortify }
      if$
    }
    { author sort.format.names }
  if$
}

FUNCTION {editor.organization.sort}
{ editor empty$
    { organization empty$
	{ key empty$
	    { "to sort, need editor, organization, or key in " cite$ * warning$
	      ""
	    }
	    { key sortify }
	  if$
	}
	{ "The " #4 organization chop.word sortify }
      if$
    }
    { editor sort.format.names }
  if$
}

FUNCTION {presort}
{ type$ "book" =
  type$ "inbook" =
  or
    'author.editor.sort
    { type$ "proceedings" =
	'editor.organization.sort
	{ type$ "manual" =
	    'author.organization.sort
	    'author.sort
	  if$
	}
      if$
    }
  if$
  "    "
  *
  year field.or.null sortify
  *
  "    "
  *
  title field.or.null
  sort.format.title
  *
  #1 entry.max$ substring$
  'sort.key$ :=
}

ITERATE {presort}

SORT

STRINGS { longest.label }

INTEGERS { number.label longest.label.width }

FUNCTION {initialize.longest.label}
{ "" 'longest.label :=
  #1 'number.label :=
  #0 'longest.label.width :=
}

FUNCTION {longest.label.pass}
{ number.label int.to.str$ 'label :=
  number.label #1 + 'number.label :=
  label width$ longest.label.width >
    { label 'longest.label :=
      label width$ 'longest.label.width :=
    }
    'skip$
  if$
}

EXECUTE {initialize.longest.label}

ITERATE {longest.label.pass}

FUNCTION {begin.bib}
{ preamble$ empty$
    'skip$
    { preamble$ write$ newline$ }
  if$
  "\begin{thebibliography}{"  longest.label  * "}" * write$ newline$
}

EXECUTE {begin.bib}

EXECUTE {init.state.consts}

ITERATE {call.type$}

FUNCTION {end.bib}
{ newline$
  "\end{thebibliography}" write$ newline$
}

EXECUTE {end.bib}

A  => slides/plain_italian.bst +1116 -0
@@ 1,1116 @@
% BibTeX standard bibliography style `plain'
    % version 0.99a for BibTeX versions 0.99a or later, LaTeX version 2.09.
    % Copyright (C) 1985, all rights reserved.
    % Copying of this file is authorized only if either
    % (1) you make absolutely no changes to your copy, including name, or
    % (2) if you do make changes, you name it something other than
    % btxbst.doc, plain.bst, unsrt.bst, alpha.bst, and abbrv.bst.
    % This restriction helps ensure that all standard styles are identical.
    % The file btxbst.doc has the documentation for this style.

%%---------------------------------------------------------------------
 %This file is an italian version of plain.bst   
 %Use it by putting \bibliographystyle{plain_italian}
 %author: Vittorio De Martino, settembre 2002 (v.demart@dada.it)
 
 %Changes:        ["original"-->"italian"]  
 %             "Daly, P., and Cox, D.R."-->"Daly P. e Cox D.R."  
 %             "Technical Report"-->"Relazione Tecnica"
 %             "Ph.D. thesis"-->"Tesi di Dottorato di Ricerca"
 %             "Master thesis"-->"Tesi di Master"
 %             "editor/editors"-->"Curatore/curatori o meglio (A cura di)"
%%---------------------------------------------------------------------

ENTRY
  { address
    author
    booktitle
    chapter
    edition
    editor
    howpublished
    institution
    journal
    key
    month
    note
    number
    organization
    pages
    publisher
    school
    series
    title
    type
    volume
    year
  }
  {}
  { label }

INTEGERS { output.state before.all mid.sentence after.sentence after.block }

FUNCTION {init.state.consts}
{ #0 'before.all :=
  #1 'mid.sentence :=
  #2 'after.sentence :=
  #3 'after.block :=
}

STRINGS { s t }

FUNCTION {output.nonnull}
{ 's :=
  output.state mid.sentence =
    { ", " * write$ }
    { output.state after.block =
    { add.period$ write$
      newline$
      "\newblock " write$
    }
    { output.state before.all =
        'write$
        { add.period$ " " * write$ }
      if$
    }
      if$
      mid.sentence 'output.state :=
    }
  if$
  s
}

FUNCTION {output}
{ duplicate$ empty$
    'pop$
    'output.nonnull
  if$
}

FUNCTION {output.check}
{ 't :=
  duplicate$ empty$
    { pop$ "empty " t * " in " * cite$ * warning$ }
    'output.nonnull
  if$
}

FUNCTION {output.bibitem}
{ newline$
  "\bibitem{" write$
  cite$ write$
  "}" write$
  newline$
  ""
  before.all 'output.state :=
}

FUNCTION {fin.entry}
{ add.period$
  write$
  newline$
}

FUNCTION {new.block}
{ output.state before.all =
    'skip$
    { after.block 'output.state := }
  if$
}

FUNCTION {new.sentence}
{ output.state after.block =
    'skip$
    { output.state before.all =
    'skip$
    { after.sentence 'output.state := }
      if$
    }
  if$
}

FUNCTION {not}
{   { #0 }
    { #1 }
  if$
}

FUNCTION {and}
{   'skip$
    { pop$ #0 }
  if$
}

FUNCTION {or}
{   { pop$ #1 }
    'skip$
  if$
}

FUNCTION {new.block.checka}
{ empty$
    'skip$
    'new.block
  if$
}

FUNCTION {new.block.checkb}
{ empty$
  swap$ empty$
  and
    'skip$
    'new.block
  if$
}

FUNCTION {new.sentence.checka}
{ empty$
    'skip$
    'new.sentence
  if$
}

FUNCTION {new.sentence.checkb}
{ empty$
  swap$ empty$
  and
    'skip$
    'new.sentence
  if$
}

FUNCTION {field.or.null}
{ duplicate$ empty$
    { pop$ "" }
    'skip$
  if$
}

FUNCTION {emphasize}
{ duplicate$ empty$
    { pop$ "" }
    { "{\em " swap$ * "}" * }
  if$
}

INTEGERS { nameptr namesleft numnames }

FUNCTION {format.names}
{ 's :=
  #1 'nameptr :=
  s num.names$ 'numnames :=
  numnames 'namesleft :=
    { namesleft #0 > }
    { s nameptr "{ff~}{vv~}{ll}{, jj}" format.name$ 't :=
      nameptr #1 >
    { namesleft #1 >
        { ", " * t * }
        { numnames #2 >
        { "," * }
        'skip$
          if$
          t "others" =
        { " e~altri" * }
        { " e " * t * }
          if$
        }
      if$
    }
    't
      if$
      nameptr #1 + 'nameptr :=
      namesleft #1 - 'namesleft :=
    }
  while$
}

FUNCTION {format.authors}
{ author empty$
    { "" }
    { author format.names }
  if$
}

FUNCTION {format.editors}
{ editor empty$
    { "" }
    { editor format.names
      editor num.names$ #1 >
    { ", (A cura di)" * }
    { ", (A cura di)" * }
      if$
    }
  if$
}
FUNCTION {format.editorit}
{ editor empty$
    { "" }
    {"A cura di " editor format.names *} 
      if$
}

FUNCTION {format.title}
{ title empty$
    { "" }
    { title "t" change.case$ }
  if$
}

FUNCTION {n.dashify}
{ 't :=
  ""
    { t empty$ not }
    { t #1 #1 substring$ "-" =
    { t #1 #2 substring$ "--" = not
        { "--" *
          t #2 global.max$ substring$ 't :=
        }
        {   { t #1 #1 substring$ "-" = }
        { "-" *
          t #2 global.max$ substring$ 't :=
        }
          while$
        }
      if$
    }
    { t #1 #1 substring$ *
      t #2 global.max$ substring$ 't :=
    }
      if$
    }
  while$
}

FUNCTION {format.date}
{ year empty$
    { month empty$
    { "" }
    { "there's a month but no year in " cite$ * warning$
      month
    }
      if$
    }
    { month empty$
    'year
    { month " " * year * }
      if$
    }
  if$
}

FUNCTION {format.btitle}
{ title emphasize
}

FUNCTION {tie.or.space.connect}
{ duplicate$ text.length$ #3 <
    { "~" }
    { " " }
  if$
  swap$ * *
}

FUNCTION {either.or.check}
{ empty$
    'pop$
    { "can't use both " swap$ * " fields in " * cite$ * warning$ }
  if$
}

FUNCTION {format.bvolume}
{ volume empty$
    { "" }
    { "volume" volume tie.or.space.connect
      series empty$
    'skip$
    { " di " * series emphasize * }
      if$
      "volume e numero" number either.or.check
    }
  if$
}

FUNCTION {format.number.series}
{ volume empty$
    { number empty$
        { series field.or.null }
        { series empty$
            { "there's a number but no series in " cite$ * warning$ }
            { " in " * series * }
          if$
        output.state mid.sentence =
        { "numero" }
        { "Numero" }
          if$
          number tie.or.space.connect
}
      if$
    }
    { "" }
  if$
}

FUNCTION {format.edition}
{ edition empty$
    { "" }
    { output.state mid.sentence =
    { edition "l" change.case$ " edizione" * }
    { edition "t" change.case$ " edizione" * }
      if$
    }
  if$
}

INTEGERS { multiresult }

FUNCTION {multi.page.check}
{ 't :=
  #0 'multiresult :=
    { multiresult not
      t empty$ not
      and
    }
    { t #1 #1 substring$
      duplicate$ "-" =
      swap$ duplicate$ "," =
      swap$ "+" =
      or or
    { #1 'multiresult := }
    { t #2 global.max$ substring$ 't := }
      if$
    }
  while$
  multiresult
}

FUNCTION {format.pages}
{ pages empty$
    { "" }
    { pages multi.page.check
    { "pp." pages n.dashify tie.or.space.connect }
    { "p." pages tie.or.space.connect }
      if$
    }
  if$
}

FUNCTION {format.vol.num.pages}
{ volume field.or.null
  number empty$
    'skip$
    { "(" number * ")" * *
      volume empty$
    { "there's a number but no volume in " cite$ * warning$ }
    'skip$
      if$
    }
  if$
  pages empty$
    'skip$
    { duplicate$ empty$
    { pop$ format.pages }
    { ":" * pages n.dashify * }
      if$
    }
  if$
}

FUNCTION {format.chapter.pages}
{ chapter empty$
    'format.pages
    { type empty$
    { "capitolo" }
    { type "l" change.case$ }
      if$
      chapter tie.or.space.connect
      pages empty$
    'skip$
    { ", " * format.pages * }
      if$
    }
  if$
}

FUNCTION {format.in.ed.booktitle}
{ booktitle empty$
    { "" }
    { editor empty$
    { " In " booktitle emphasize * }
    { " In "  * booktitle emphasize * " " format.editorit *}
      if$
    }
  if$
}

FUNCTION {empty.misc.check}
{ author empty$ title empty$ howpublished empty$
  month empty$ year empty$ note empty$
  and and and and and
  key empty$ not and
    { "all relevant fields are empty in " cite$ * warning$ }
    'skip$
  if$
}

FUNCTION {format.thesis.type}
{ type empty$
    'skip$
    { pop$
      type "t" change.case$
    }
  if$
}

FUNCTION {format.tr.number}
{ type empty$
    { "Relazione Tecnica" }
    'type
  if$
  number empty$
    { "t" change.case$ }
    { number tie.or.space.connect }
  if$
}

FUNCTION {format.article.crossref}
{ key empty$
    { journal empty$
    { "need key or journal for " cite$ * " to crossref " * crossref *
      warning$
      ""
    }
    { "In {\em " journal * "\/}" * }
      if$
    }
    { "In " key * }
  if$
  " \cite{" * crossref * "}" *
}

FUNCTION {format.crossref.editor}
{ editor #1 "{vv~}{ll}" format.name$
  editor num.names$ duplicate$
  #2 >
    { pop$ " e~altri" * }
    { #2 <
    'skip$
    { editor #2 "{ff }{vv }{ll}{ jj}" format.name$ "others" =
        { " e~altri" * }
        { " e " * editor #2 "{vv~}{ll}" format.name$ * }
      if$
    }
      if$
    }
  if$
}

FUNCTION {format.book.crossref}
{ volume empty$
    { "empty volume in " cite$ * "'s crossref of " * crossref * warning$
      "In "
    }
    { "Volume" volume tie.or.space.connect
      " di " *
    }
  if$
  editor empty$
  editor field.or.null author field.or.null =
  or
    { key empty$
    { series empty$
        { "need editor, key, or series for " cite$ * " to crossref " *
          crossref * warning$
          "" *
        }
        { "{\em " * series * "\/}" * }
      if$
    }
    { key * }
      if$
    }
    { format.crossref.editor * }
  if$
  " \cite{" * crossref * "}" *
}

FUNCTION {format.incoll.inproc.crossref}
{ editor empty$
  editor field.or.null author field.or.null =
  or
    { key empty$
    { booktitle empty$
        { "need editor, key, or booktitle for " cite$ * " to crossref " *
          crossref * warning$
          ""
        }
        { "In {\em " booktitle * "\/}" * }
      if$
    }
    { "In " key * }
      if$
    }
    { "In " format.crossref.editor * }
  if$
  " \cite{" * crossref * "}" *
}

FUNCTION {article}
{ output.bibitem
  format.authors "author" output.check
  new.block
  format.title "title" output.check
  new.block
  crossref missing$
    { journal emphasize "journal" output.check
      format.vol.num.pages output
      format.date "year" output.check
    }
    { format.article.crossref output.nonnull
      format.pages output
    }
  if$
  new.block
  note output
  fin.entry
}

FUNCTION {book}
{ output.bibitem
  author empty$
    { format.editors "author and editor" output.check }
    { format.authors output.nonnull
      crossref missing$
    { "author and editor" editor either.or.check }
    'skip$
      if$
    }
  if$
  new.block
  format.btitle "title" output.check
  crossref missing$
    { format.bvolume output
      new.block
      format.number.series output
      new.sentence
      publisher "publisher" output.check
      address output
    }
    { new.block
      format.book.crossref output.nonnull
    }
  if$
  format.edition output
  format.date "year" output.check
  new.block
  note output
  fin.entry
}

FUNCTION {booklet}
{ output.bibitem
  format.authors output
  new.block
  format.title "title" output.check
  howpublished address new.block.checkb
  howpublished output
  address output
  format.date output
  new.block
  note output
  fin.entry
}

FUNCTION {inbook}
{ output.bibitem
  author empty$
    { format.editors "author and editor" output.check }
    { format.authors output.nonnull
      crossref missing$
    { "author and editor" editor either.or.check }
    'skip$
      if$
    }
  if$
  new.block
  format.btitle "title" output.check
  crossref missing$
    { format.bvolume output
      format.chapter.pages "chapter and pages" output.check
      new.block
      format.number.series output
      new.sentence
      publisher "publisher" output.check
      address output
    }
    { format.chapter.pages "chapter and pages" output.check
      new.block
      format.book.crossref output.nonnull
    }
  if$
  format.edition output
  format.date "year" output.check
  new.block
  note output
  fin.entry
}

FUNCTION {incollection}
{ output.bibitem
  format.authors "author" output.check
  new.block
  format.title "title" output.check
  new.block
  crossref missing$
    { format.in.ed.booktitle "booktitle" output.check
      format.bvolume output
      format.number.series output
      format.chapter.pages output
      new.sentence
      publisher "publisher" output.check
      address output
      format.edition output
      format.date "year" output.check
    }
    { format.incoll.inproc.crossref output.nonnull
      format.chapter.pages output
    }
  if$
  new.block
  note output
  fin.entry
}

FUNCTION {inproceedings}
{ output.bibitem
  format.authors "author" output.check
  new.block
  format.title "title" output.check
  new.block
  crossref missing$
    { format.in.ed.booktitle "booktitle" output.check
      format.bvolume output
      format.number.series output
      format.pages output
      address empty$
    { organization publisher new.sentence.checkb
      organization output
      publisher output
      format.date "year" output.check
    }
    { address output.nonnull
      format.date "year" output.check
      new.sentence
      organization output
      publisher output
    }
      if$
    }
    { format.incoll.inproc.crossref output.nonnull
      format.pages output
    }
  if$
  new.block
  note output
  fin.entry
}

FUNCTION {conference} { inproceedings }

FUNCTION {manual}
{ output.bibitem
  author empty$
    { organization empty$
    'skip$
    { organization output.nonnull
      address output
    }
      if$
    }
    { format.authors output.nonnull }
  if$
  new.block
  format.btitle "title" output.check
  author empty$
    { organization empty$
    { address new.block.checka
      address output
    }
    'skip$
      if$
    }
    { organization address new.block.checkb
      organization output
      address output
    }
  if$
  format.edition output
  format.date output
  new.block
  note output
  fin.entry
}

FUNCTION {mastersthesis}
{ output.bibitem
  format.authors "author" output.check
  new.block
  format.title "title" output.check
  new.block
  "Tesi per Master" format.thesis.type output.nonnull
  school "school" output.check
  address output
  format.date "year" output.check
  new.block
  note output
  fin.entry
}

FUNCTION {misc}
{ output.bibitem
  format.authors output
  title howpublished new.block.checkb
  format.title output
  howpublished new.block.checka
  howpublished output
  format.date output
  new.block
  note output
  fin.entry
  empty.misc.check
}

FUNCTION {phdthesis}
{ output.bibitem
  format.authors "author" output.check
  new.block
  format.btitle "title" output.check
  new.block
  "Tesi di Dottorato di Ricerca" format.thesis.type output.nonnull
  school "school" output.check
  address output
  format.date "year" output.check
  new.block
  note output
  fin.entry
}

FUNCTION {proceedings}
{ output.bibitem
  editor empty$
    { organization output }
    { format.editors output.nonnull }
  if$
  new.block
  format.btitle "title" output.check
  format.bvolume output
  format.number.series output
  address empty$
    { editor empty$
    { publisher new.sentence.checka }
    { organization publisher new.sentence.checkb
      organization output
    }
      if$
      publisher output
      format.date "year" output.check
    }
    { address output.nonnull
      format.date "year" output.check
      new.sentence
      editor empty$
    'skip$
    { organization output }
      if$
      publisher output
    }
  if$
  new.block
  note output
  fin.entry
}

FUNCTION {techreport}
{ output.bibitem
  format.authors "author" output.check
  new.block
  format.title "title" output.check
  new.block
  format.tr.number output.nonnull
  institution "institution" output.check
  address output
  format.date "year" output.check
  new.block
  note output
  fin.entry
}

FUNCTION {unpublished}
{ output.bibitem
  format.authors "author" output.check
  new.block
  format.title "title" output.check
  new.block
  note "note" output.check
  format.date output
  fin.entry
}

FUNCTION {default.type} { misc }

MACRO {jan} {"gennaio"}

MACRO {feb} {"febbraio"}

MACRO {mar} {"marzo"}

MACRO {apr} {"aprile"}

MACRO {may} {"maggio"}

MACRO {jun} {"giugno"}

MACRO {jul} {"luglio"}

MACRO {aug} {"agosto"}

MACRO {sep} {"settembre"}

MACRO {oct} {"ottobre"}

MACRO {nov} {"novembre"}

MACRO {dec} {"dicembre"}

MACRO {acmcs} {"ACM Computing Surveys"}

MACRO {acta} {"Acta Informatica"}

MACRO {cacm} {"Communications of the ACM"}

MACRO {ibmjrd} {"IBM Journal of Research and Development"}

MACRO {ibmsj} {"IBM Systems Journal"}

MACRO {ieeese} {"IEEE Transactions on Software Engineering"}

MACRO {ieeetc} {"IEEE Transactions on Computers"}

MACRO {ieeetcad}
 {"IEEE Transactions on Computer-Aided Design of Integrated Circuits"}

MACRO {ipl} {"Information Processing Letters"}

MACRO {jacm} {"Journal of the ACM"}

MACRO {jcss} {"Journal of Computer and System Sciences"}

MACRO {scp} {"Science of Computer Programming"}

MACRO {sicomp} {"SIAM Journal on Computing"}

MACRO {tocs} {"ACM Transactions on Computer Systems"}

MACRO {tods} {"ACM Transactions on Database Systems"}

MACRO {tog} {"ACM Transactions on Graphics"}

MACRO {toms} {"ACM Transactions on Mathematical Software"}

MACRO {toois} {"ACM Transactions on Office Information Systems"}

MACRO {toplas} {"ACM Transactions on Programming Languages and Systems"}

MACRO {tcs} {"Theoretical Computer Science"}

READ

FUNCTION {sortify}
{ purify$
  "l" change.case$
}

INTEGERS { len }

FUNCTION {chop.word}
{ 's :=
  'len :=
  s #1 len substring$ =
    { s len #1 + global.max$ substring$ }
    's
  if$
}

FUNCTION {sort.format.names}
{ 's :=
  #1 'nameptr :=
  ""
  s num.names$ 'numnames :=
  numnames 'namesleft :=
    { namesleft #0 > }
    { nameptr #1 >
    { "   " * }
    'skip$
      if$
      s nameptr "{vv{ } }{ll{ }}{  ff{ }}{  jj{ }}" format.name$ 't :=
      nameptr numnames = t "others" = and
    { "et al" * }
    { t sortify * }
      if$
      nameptr #1 + 'nameptr :=
      namesleft #1 - 'namesleft :=
    }
  while$
}

FUNCTION {sort.format.title}
{ 't :=
  "A " #2
    "An " #3
      "The " #4 t chop.word
    chop.word
  chop.word
  sortify
  #1 global.max$ substring$
}

FUNCTION {author.sort}
{ author empty$
    { key empty$
    { "to sort, need author or key in " cite$ * warning$
      ""
    }
    { key sortify }
      if$
    }
    { author sort.format.names }
  if$
}

FUNCTION {author.editor.sort}
{ author empty$
    { editor empty$
    { key empty$
        { "to sort, need author, editor, or key in " cite$ * warning$
          ""
        }
        { key sortify }
      if$
    }
    { editor sort.format.names }
      if$
    }
    { author sort.format.names }
  if$
}

FUNCTION {author.organization.sort}
{ author empty$
    { organization empty$
    { key empty$
        { "to sort, need author, organization, or key in " cite$ * warning$
          ""
        }
        { key sortify }
      if$
    }
    { "The " #4 organization chop.word sortify }
      if$
    }
    { author sort.format.names }
  if$
}

FUNCTION {editor.organization.sort}
{ editor empty$
    { organization empty$
    { key empty$
        { "to sort, need editor, organization, or key in " cite$ * warning$
          ""
        }
        { key sortify }
      if$
    }
    { "The " #4 organization chop.word sortify }
      if$
    }
    { editor sort.format.names }
  if$
}

FUNCTION {presort}
{ type$ "book" =
  type$ "inbook" =
  or
    'author.editor.sort
    { type$ "proceedings" =
    'editor.organization.sort
    { type$ "manual" =
        'author.organization.sort
        'author.sort
      if$
    }
      if$
    }
  if$
  "    "
  *
  year field.or.null sortify
  *
  "    "
  *
  title field.or.null
  sort.format.title
  *
  #1 entry.max$ substring$
  'sort.key$ :=
}

ITERATE {presort}

SORT

STRINGS { longest.label }

INTEGERS { number.label longest.label.width }

FUNCTION {initialize.longest.label}
{ "" 'longest.label :=
  #1 'number.label :=
  #0 'longest.label.width :=
}

FUNCTION {longest.label.pass}
{ number.label int.to.str$ 'label :=
  number.label #1 + 'number.label :=
  label width$ longest.label.width >
    { label 'longest.label :=
      label width$ 'longest.label.width :=
    }
    'skip$
  if$
}

EXECUTE {initialize.longest.label}

ITERATE {longest.label.pass}

FUNCTION {begin.bib}
{ preamble$ empty$
    'skip$
    { preamble$ write$ newline$ }
  if$
  "\begin{thebibliography}{"  longest.label  * "}" * write$ newline$
}

EXECUTE {begin.bib}

EXECUTE {init.state.consts}

ITERATE {call.type$}

FUNCTION {end.bib}
{ newline$
  "\end{thebibliography}" write$ newline$
}

EXECUTE {end.bib}

A  => slides/slides.pdf +0 -0

A  => slides/slides.tex +648 -0
@@ 1,648 @@
\def\thudbabelopt{italian,english}
\documentclass[beamer={noamsthm,10pt},target=mst]{thud}[2014/03/11]

\usepackage[utf8x]{inputenc}
\usepackage{parcolumns}
\usepackage{amsmath,amsfonts,amssymb,amsthm,mathtools}
\usepackage{latexsym}
\usepackage{hyperref}
\usepackage{url}
\usepackage{stmaryrd}
\usepackage{listings}
\usepackage{tikz}
\usetikzlibrary{shapes,shapes.geometric,arrows,fit,calc,positioning,automata,}
\usepackage{pgfplots}
\usepackage{pgfplotstable}
\usepackage{lmodern}
\usepackage{numprint}
\usepackage[labelfont=bf]{caption}
\usepackage{float}
\usepackage{adjustbox}
\usepackage{nicefrac}
\usepackage[bottom]{footmisc}
\usepackage{bussproofs}
\usepackage{graphicx}
\usepackage{verbatim}
\usepackage{tabu}
\npthousandsep{\,}

\usepackage[T1]{fontenc}

\newcommand{\R}{\mathbb{R}}
\newcommand{\N}{\mathbb{N}}
\newcommand\eqdef{\stackrel{\text{def}}{=}}
\newcommand\eqmin{\stackrel{\text{min}}{=}}
\newcommand\eqmax{\stackrel{\text{max}}{=}}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{corollary}{Corollary}[theorem]
\newtheorem{lemma}[theorem]{Lemma}
\theoremstyle{definition}
\newtheorem{definition}{Definition}[section]
\newtheorem{example}{Example}[section]

\title{Models for real-time systems: timed automata and THML}
\author{Alessio Chiapperini}
\course{Informatica}
\date{2018-2019}
\cycle{XXVIII}

\usetheme{boxes}
\usecolortheme{orchid}
\setbeamertemplate{blocks}[rounded][shadow=true]

\addtobeamertemplate{navigation symbols}{}{%
        \usebeamerfont{footline}%
        \usebeamercolor[fg]{footline}%
        \hspace{1em}%
        %\parbox{0\linewidth}{\vspace*{-8pt}\insertframenumber/\inserttotalframenumber}
        %\vspace*{-8pt}
        \raisebox{2pt}{\insertframenumber/\inserttotalframenumber}
}

\makeatletter %% <- make @ usable in command names
\newcommand*\Neg[2][0mu]{\Neginternal{#1}{\negslash}{#2}}
\newcommand*\sNeg[2][0mu]{\Neginternal{#1}{\snegslash}{#2}}
\newcommand*\ssNeg[2][0mu]{\Neginternal{#1}{\ssnegslash}{#2}}
\newcommand*\sssNeg[2][0mu]{\Neginternal{#1}{\sssnegslash}{#2}}
\newcommand*\Neginternal[3]{\mathpalette\Neg@{{#1}{#2}{#3}}}
\newcommand*\Neg@[2]{\Neg@@{#1}#2}
\newcommand*\Neg@@[4]{%
  \mathrel{\ooalign{%
    $\m@th#1#4$\cr
    \hidewidth$\m@th#3{#1}\mkern\muexpr#2*2$\hidewidth\cr
  }}%
}

\newcommand*\negslash[1]{\m@th#1\not\mathrel{\phantom{=}}}
\newcommand*\snegslash[1]{\rotatebox[origin=c]{60}{$\m@th#1-$}}
\newcommand*\ssnegslash[1]{\rotatebox[origin=c]{60}{$\m@th#1{\dabar@}\mkern-7mu{\dabar@}$}}
\newcommand*\sssnegslash[1]{\rotatebox[origin=c]{60}{$\m@th#1\dabar@$}}

\newcommand{\fixed@sra}{$\vrule height 2\fontdimen22\textfont2 width 0pt\leftrightarrow$}
\newcommand{\shortarrow}[1]{%
    \mathrel{\text{\rotatebox[origin=c]{\numexpr#1*45}{\fixed@sra}}}
}

\newenvironment{myfont}{\fontfamily{qhv}\selectfont}{\par}
\DeclareTextFontCommand{\chfont}{\myfont}

\begin{document}

\maketitle

\section{Introduction}
\begin{frame}{Introduction}
    \begin{block}{Real-time system}
        A \emph{real-time system} is a system whose correct behaviour depends not only on the logical order in which events are
        performed but also on their timing.
    \end{block}
To model their behaviour we'll introduce two formalisms: 
\begin{enumerate}
    \item timed automata
    \item a timed extension of Hennessy-Milner logic.
\end{enumerate}
\end{frame}

\section{Preliminaries}
\subsection{LTS}
\begin{frame}{Preliminaries: LTS}
    In the theory of concurrency, the semantics of a language is usually given in terms of automata, also called
    \emph{labelled transition systems} (LTS) where
    \begin{itemize}
        \item processes are represented as vertices of an edge-labelled graph
        \item a change in process state caused by performing an action means moving along an edge, labelled by the
            action name, that goes out of that state
    \end{itemize}

    \begin{block}{Definition: LTS}
        A LTS is a triple $(\chfont{Proc},\chfont{Act}, \{ \xrightarrow{\alpha} : \alpha \in \chfont{Act} \})$ where:
        \begin{itemize}
            \item \chfont{Proc} is a set of \emph{states} (or \emph{processes});
            \item \chfont{Act} is a set of \emph{actions} (or \emph{labels});
            \item $\xrightarrow{\alpha} \subseteq \chfont{Proc} \times \chfont{Proc}$ is a \emph{transition relation}, for
            every $\alpha \in \chfont{Act}$.
        \end{itemize}
    \end{block}
\end{frame}

\subsection{TLTS}
\begin{frame}{Preliminaries: TLTS}
    To give semantics to real-time systems we use a variation of a labelled transition system, in which we describe the
    passage of time by adding special 'delay' transitions to the model. The resulting structure is a timed version of the 
    model of LTSs.

    \begin{block}{Definition: TLTS}
        A \emph{timed labelled transition system}, also known as timed transition system is a triple
        \begin{equation*}
            (\text{\chfont{Proc}}, \text{\chfont{Lab}}, \{\xrightarrow{~\alpha~}~: \alpha \in \text{\chfont{Lab}} \})
        \end{equation*}
        Where
        \begin{itemize}
        \item \chfont{Proc} is a set of \emph{states} or processes;
        \item $\text{\chfont{Lab}} = \text{\chfont{Act}} \cup \R_{\geq 0}$ is a set of \emph{labels} consisting of \emph{actions} and
            \emph{time delays};
        \item $\xrightarrow{~\alpha~} \subseteq \text{\chfont{Proc}} \times \text{\chfont{Proc}}$, for each $\alpha \in \text{\chfont{Lab}}$, is a
            binary relation on states, called the \emph{transition relation}.
        \end{itemize}
    \end{block}
\end{frame}

\begin{frame}{Preliminaries: TLTS}
    There are two types of transitions:
    \begin{enumerate}
        \item $s \xrightarrow{~a~} s' \text{ if } a \in \text{\chfont{Act} and } (s,s') \in \xrightarrow{~a~}$ and
        \item $s \xrightarrow{~d~} s' \text{ if } d \in \R_{\geq 0} \text{ and } (s,s') \in \xrightarrow{~d~}$.
    \end{enumerate}
    The first type of transitions are ordinary transitions that are due to the performance of an action, while the
    second type are time-elapsing transitions that describe how a system evolves as time passes. \\~\\

    In order to capture the evolution of a system as time passes, our TLTS must satisfy two requirements:
    \begin{enumerate}
        \item \emph{time-additivity}:
            \begin{equation*}
                \text{if } s \xrightarrow{~d~}s' \text{ and } 0 \leq d' \leq d \text{ then } s \xrightarrow{~d'~} s''
                \xrightarrow{d-d'} s' \text{ for some state } s''
            \end{equation*}
        \item \emph{determinism} of delay transitions, i.e. for all $s,s',s''$ and for each $d \in \R_{\geq 0}$
            \begin{equation*}
                \text{if } s \xrightarrow{~d~} s' \text{ and } s \xrightarrow{~d~} s'' \text{ then } s' = s''
            \end{equation*}

    \end{enumerate}
\end{frame}

\subsection{HML}
\begin{frame}{Preliminaries: HML (syntax)}
    \begin{block}{Hennessy-Milner formulae}
        The set $\mathcal{M}$ of \emph{Hennessy-Milner formulae} over a set of actions \chfont{Act} is given by the following
        abstract syntax:
        \begin{equation*}
            F,G ::= \mathit{tt}~|~\mathit{ff}~|~F \land G~|~F \lor G~|~\langle a \rangle F~|~[a]F
        \end{equation*}
        Where $a \in \chfont{Act}$ and $\mathit{tt}$ and $\mathit{ff}$ are used to denote `true' and `false' respectively.
    \end{block}
    Hennessy-Milner logic is a so-called multi-modal logic, since it involves modal operators that are parameterized by
    actions.
\end{frame}

\begin{frame}{Preliminaries: HML (semantics)}
    The semantics of formulae is defined with respect to a given LTS 
    \begin{equation*}
        (\chfont{Proc},\chfont{Act}, \{\xrightarrow{a} : a \in \chfont{Act} \}).
    \end{equation*}
    We use $\llbracket F \rrbracket$ to denote the set of processes in \chfont{Proc} that satisfies $F$.
    
    \begin{block}{Denotational semantics}
        We define $\llbracket F \rrbracket \subseteq \chfont{Proc}$ for $F \in \mathcal{M}$ by \\~\\
        {\tabulinesep=1.5mm
        \setlength{\tabcolsep}{40pt}
        \begin{tabu}{l l}
            $\llbracket \mathit{tt} \rrbracket = \chfont{Proc}$
            &
            $\llbracket \mathit{ff} \rrbracket = \emptyset$\\
            $\llbracket F \land G \rrbracket = \llbracket F \rrbracket \cap \llbracket G \rrbracket$
            &
            $\llbracket F \lor G \rrbracket = \llbracket F \rrbracket \cup \llbracket G \rrbracket$\\
            $\llbracket \langle a \rangle F \rrbracket = \langle \cdot a \cdot \rangle \llbracket F \rrbracket$
            &
            $\llbracket [ a ] F \rrbracket = [ \cdot a \cdot ] \llbracket F \rrbracket$\\
        \end{tabu}
        }
        \\~\\Where the operators $\langle \cdot a \cdot \rangle$, $[\cdot a \cdot] : 2^{\chfont{Proc}} \to
        2^{\chfont{Proc}}$ are defined as
        \begin{align*}
            \langle \cdot a \cdot \rangle S &= \{ p \in \chfont{Proc} : p \xrightarrow{a} p' \text{ and } p' \in S \text{ for
            some } p' \}\\
            [ \cdot a \cdot ] S &= \{ p \in \chfont{Proc} : p \xrightarrow{a} p' \text{ implies } p' \in S \text{ for
            each } p' \}
        \end{align*}
    \end{block}
\end{frame}

\begin{frame}{Preliminaries: HML with recursion (syntax)}
A HML formula only describes a \emph{finite} part of the overall behaviour of a process, and this depends on the 
\emph{modal-depth} of the formula. If we want to describe properties that describe a situation that may or must occur 
in arbitrarily long computations of a process, we have to extend our logic by adding recursion.

    \begin{block}{Syntax of HML with one variable}
        The syntax of HML with one variable $X$, denoted by $\mathcal{M}_{\{ X \}}$ is given by the following grammar:
        \begin{equation*}
            F,G ::= X~|~\mathit{tt}~|~\mathit{ff}~|~F \land G~|~F \lor G~|~\langle a \rangle F~|~[a]F
        \end{equation*}
    \end{block}
\end{frame}

\begin{frame}{Preliminaries: HML with recursion (semantics)}
    Semantically a formula F (which may contain a variable X) is interpreted as a function $\mathcal{O}_F :
    2^{\chfont{Proc}} \to 2^{\chfont{Proc}}$ that given a set of processes that are assumed to satisfy $X$, gives us the set
    of processes that satisfy $F$.

    \begin{block}{Semantics}
        Let $(\chfont{Proc},\chfont{Act}, \{\xrightarrow{a} : a \in \chfont{Act} \})$ be a LTS. For each $S \subseteq
        \chfont{Proc}$ and formula $F$, we define $\mathcal{O}_F(S)$ as follows:
        \begin{align*}
            \mathcal{O}_X(S) &= S\\
            \mathcal{O}_{\mathit{tt}}(S) &= \chfont{Proc}\\
            \mathcal{O}_{\mathit{ff}}(S) &= \emptyset\\
            \mathcal{O}_{F_1 \land F_2}(S) &= \mathcal{O}_{F_1}(S) \cap \mathcal{O}_{F_2}(S)\\
            \mathcal{O}_{F_1 \lor F_2}(S) &= \mathcal{O}_{F_1}(S) \cup \mathcal{O}_{F_2}(S)\\
            \mathcal{O}_{\langle a \rangle F}(S) &= \langle \cdot a \cdot \rangle \mathcal{O}_F(S)\\
            \mathcal{O}_{[ a ] F}(S) &= [ \cdot a \cdot ] \mathcal{O}_F(S)\\
        \end{align*}
    \end{block}
\end{frame}

\section{Timed automata}
\begin{frame}{Timed automata}
    Timed automata are essentialy nondeterministic finite automata with the addition of three main ingredients:
    \begin{enumerate}
        \item a finite set of real-valued clocks, which measure delays between events that occur in the automaton;
        \item clock constraints: transitions can be conditioned on clock values;
        \item clock resets: the performing of a particular transition can reset selected clocks.
    \end{enumerate}
\end{frame}

\subsection{Syntax}
\begin{frame}{Timed automata: clock constraints}
    Let $C = \{x,y,\ldots\}$ be a finite set of clock names that can be used in the automaton.
    \begin{block}{Clock constraints}
        The set $\mathcal{B}(C)$ of \emph{clock constraints} over the set of clocks $C$ is defined by the following abstract
        syntax:
        \begin{equation*}
            g,g_1,g_2 ::= x \bowtie n~|~ g_1 \land g_2
        \end{equation*}
        Where $x \in C$ is a clock, $n \in \N$ and $\bowtie \in \{\leq, <, =, >, \geq \}$.
    \end{block}
    \begin{itemize}
        \item Each clock stores the amount of time elapsed from the last moment when the clock was reset.
        \item This is expressed by a function $v : C \to \R_{\geq 0}$ called (\emph{clock}) \emph{valuation}.
        \item For $d \in \R_{\geq 0}$, the valuation $v+d$ is the clock valuation such that $(v+d)(x) = v(x) + d$ for
            each $x \in C$
        \item  For a subset $R \subseteq C$ we let $v[R]$ be the valuation such that $v[R](x) = 0$ when $x \in R$ and
            $v[R](x) = v(x)$ when $x \in C \setminus R$.
    \end{itemize}
\end{frame}

\begin{frame}{Timed automata: clock constraints}
    \begin{block}{Clock constraint evaluation}
        Let $g \in \mathcal{B}(C)$ be a clock constraint for a given set of clocks $C$ and let $v : C \to \R_{\geq 0}$ be a
        clock valuation. The \emph{evaluation} of clock constraints ($v \models g$) is defined inductively on the structure
        of $g$:
        \begin{align*}
            &v \models x \bowtie n \text{ iff } v(x) \bowtie n\\
            &v \models g_1 \land g_2 \text { iff } v \models g_1 \text{ and } v \models g_2
        \end{align*}
        Where $x \in C$ is a clock, $n \in \N$, $g_1, g_2 \in \mathcal{B}(C)$ and $\bowtie \in \{ \leq, <, =, > \geq \}$.
    \end{block}
\end{frame}

\begin{frame}{Timed automata: syntax}
    \begin{block}{Timed automaton}
        A \emph{timed automaton} over a finite set of clocks $C$ and a finite set of actions \chfont{\chfont{Act}} is a quadruple
        \begin{equation*}
            (L,l_0,E,I)
        \end{equation*}
        where
        \begin{itemize}
            \item $L$ is a finite set of \emph{locations}, ranged over by $l$;
            \item $l_0 \in L$ is the \emph{initial location};
            \item $E \subseteq L \times \mathcal{B}(C) \times \chfont{Act} \times 2^C \times L$ is a finite set of
            \emph{edges};
            \item $I : L \to \mathcal{B}(C)$ assigns \emph{invariants} to locations.
        \end{itemize}
        We can write $l \xrightarrow{g,a,R} l'$ instead of $(l,g,a,R,l') \in E$, where $l$ is the \emph{source location}, $g$
        is the \emph{guard}, $a$ is the \emph{action}, $R$ is the set of clocks to be reset and $l'$ is the \emph{target
        location}.
    \end{block}
\end{frame}

\subsection{Semantics}
\begin{frame}{Timed automata: configurations}
    \begin{block}{State of computation}
        The \emph{state} of computation or a \emph{configuration} of a timed automaton consists of a pair $(l,v)$,
        where:
        \begin{itemize}
            \item $l$ is the control location the automaton is in;
            \item $v$ is the clock valuation determined by the current clock values.
        \end{itemize}
    \end{block}
    The pair $(l,v)$ is a legal state of the timed automaton only if the valuation $v$ satisfies the
    invariant of location $l$. Initially, the control location is $l_0$ and the value of each clock is 0.
\end{frame}

\begin{frame}{Timed automata: semantics}
    The operational semantics of a timed automata is defined through an infinite-state transition system defined as
    follows:
    \begin{block}{Semantics}
        Let $\mathcal{A} = (L,l_0,E,I)$ be a timed automaton over a set of clocks $C$ and a set of actions \chfont{Act}. We define the
        timed transition system $T(\mathcal{A})$ generated by $\mathcal{A}$ as $T(\mathcal{A}) = (\chfont{Proc}, \chfont{Lab}, \{\xrightarrow{~\alpha~}~:~
        \alpha \in \chfont{Lab}\})$ where:
        \begin{itemize}
            \item \chfont{Proc} $= \{ (l,v) : (l,v) \in L \times (C \to \R_{\geq 0}) \text{ and } v \models I(l)\}$;
            \item \chfont{Lab} $= \chfont{Act} \cup \R_{\geq 0}$ is the set of labels;
            \item the transition relation is defined by
            \begin{itemize}
            \item $(l,v) \xrightarrow{~a~} (l',v')$ if there is an edge $(l \xrightarrow{g,a,R} l') \in E$ such that $v
                \models g$, $v' = v[R]$ and $v' \models I(l')$,
            \item $(l,v) \xrightarrow{~d~} (l,v+d)$ for all $d \in \R_{\geq 0}$ such that $v \models I(l)$ and $v+d \models
                I(l)$.
            \end{itemize}
        \end{itemize}
    \end{block}
    Let $v_0$ denote the valuation such that $v_0(x) = 0$ for all $x \in C$. If $v_0$ satisfies the invariant of the
    initial location $l_0$, then $(l_0,v_0)$ is called the \emph{initial state} or \emph{initial configuration} of
    $T(\mathcal{A})$.
\end{frame}

\subsection{Region graphs}
\begin{frame}{Region graphs}
    \textbf{Idea}: the collection of valuations for a given timed automaton can be partitioned into finitely many 
    equivalence classes in such a way that any two valuations from the same equivalence class will not create any
    'significant difference' in the behaviour of the system.
\end{frame}

\begin{frame}{Region graphs}
    \begin{block}{Clock valuations equivalence}
        Let $\mathcal{A}$ be a timed automaton, we say that two clock valuations $v$ and $v'$ are equivalent, written $v
        \equiv v'$, iff:
        \begin{enumerate}
            \item for each $x \in C$ we either have that 
            \begin{equation*}
                v(x) > c_x \land v'(x) > c_x \text{ or } \lfloor v(x) \rfloor = \lfloor v'(x) \rfloor
            \end{equation*}
            \item for each $x \in C$ s.t. $v(x) \leq c_x$ we have 
            \begin{equation*}
                frac(v(x)) = 0 \text{ iff } frac(v'(x)) = 0;
            \end{equation*}
            \item for all $x, y \in C$ such that $v(x) \leq c_x$ and $v(y) \leq c_y$ we have
            \begin{equation*}
                frac(v(x)) \leq frac(v(y)) \text{ iff } frac(v'(x)) \leq frac(v'(y))
            \end{equation*}
        \end{enumerate}
    \end{block}
\end{frame}

\begin{frame}{Region graphs}
    \begin{block}{Region}
        An $\equiv$-equivalence class $[v]_{\equiv}$ represented by some clock valuation $v$ is called a \emph{region}.
    \end{block}
    Each region can be uniquely characterized by a finite collection of clock constraints that it satisfies.
\end{frame}

\begin{frame}{Region graphs}
    Each region of a timed automata can be uniquely represented by specifying the
    following items of information:
    \begin{itemize}
    \item for each clock $x$ a constraint from the set
        \begin{gather*}
        \big\{ \{ x = n: n \in \{0,1,\ldots, c_x\} \big\}\\
        \cup \big\{ \{ n < x < n +1 : n \in \{0,1,\ldots, c_x - 1\} \big\} \cup \{c_x < x \}
        \end{gather*}
    \item for each pair of distinct clocks $x$ and $y$ that, for some $n < c_x$ and $m < c_y$, satisfy constraints of the form
        $n < x < n+1$ and $m < y < m+1$, an indication whether $frac(v(x))$ is less than, equal to, or greater than
        $frac(v(y))$, for each valuation $v$ in that region.
    \end{itemize}
\end{frame}

\begin{frame}{Region graphs}
    \begin{block}{Region graph}
        The \emph{region graph} of a timed automaton $\mathcal{A}$ over a set of clocks $C$ and actions \chfont{Act} is a
        LTS:
        \begin{equation*}
            T_r(\mathcal{A}) = (\chfont{Proc}, \chfont{Act} \cup \{\varepsilon\}, \{\xRightarrow{a}:a \in \chfont{Act} \cup
            \{\varepsilon\}\})
        \end{equation*}
        where
        \begin{itemize}
            \item \chfont{Proc} $= \{(l,[v]_{\equiv}) : l \in L, v : C \to \R_{\geq 0} \}$, states are symbolic states;
            \item the transition relation $\Rightarrow$ is defined as follows:
            \begin{enumerate}
                \item for each label $a \in \chfont{Act}$, we have $(l,[v]_{\equiv}) \xRightarrow{a} (l',[v']_{\equiv})$ iff
                $(l,v) \xrightarrow{~a~} (l',v')$;
                \item $(l,[v]_{\equiv}) \xRightarrow{\varepsilon} (l,[v']_{\equiv})$ iff $(l,v) \xrightarrow{~d~} (l,v')$ for
                some $d \in \R_{\geq 0}$.
            \end{enumerate}
        \end{itemize}
    \end{block}
\end{frame}

\subsection{Reachability problem}
\begin{frame}{Reachability problem}
    \begin{block}{Reachability problem}
        Given a timed automaton $\mathcal{A} = (L,l_0,E,I)$
        over a set of clocks $C$ and a configuration $(l,v)$, the question is whether $(l,v)$ is reachable from the initial
        configuration, i.e. whether $(l_0,v_0) \longrightarrow^* (l,v)$ where $v_0(x) = 0~\forall x \in C$.
    \end{block}
    \begin{lemma}
        Let $\mathcal{A} = (L,l_0,E,I)$ be a timed automaton and $(l,v)$ a configuration. It holds that $(l_0,v_0)
        \longrightarrow^* (l,v)$ in $\mathcal{A}$ iff $(l_0,[v_0]_{\equiv}) \Rightarrow^* (l,[v]_{\equiv})$ in its region
        graph $T_r(\mathcal{A})$.
    \end{lemma}

    \begin{corollary}
        The reachability problem for timed automata is decidable.
    \end{corollary}

    \begin{theorem}
        The reachability problem for timed automata is \textsc{PSPACE}-complete.
    \end{theorem}
\end{frame}

\section{THML}
\begin{frame}{THML}
    \begin{itemize}
        \item Since HML is used to describe the properties of reactive systems modeled as LTSs and since the semantics
            of timed automata is given in terms of TLTSs, it's natural to define a notion of HML for real-time systems.
        \item To define a modal logic for describing properties of TLTSs we introduce two new modalities, 
            $\mathrlap{\exists}\,\exists$ and $\mathrlap{\forall}\,\forall$:
            \begin{enumerate}
                \item a process satisfies $\mathrlap{\exists}\,\exists F$ iff it \emph{can delay for some amount of
                    time} reaching a state state satisfying $F$;
                \item a process satisfies $\mathrlap{\forall}\,\forall F$ iff \emph{no matter how long it delays} it
                    will always reach a state sastisfying $F$;
            \end{enumerate}
        \item We also extend HML with a way of expressing ``quantitative real-time constraints''. A formula of the form
            $x~\texttt{\underline{in}}~F$ says that a state in a TLTS will satisfy $F$ after the value of $x$ has been 
            set to zero.
    \end{itemize}
\end{frame}

\subsection{Syntax}
\begin{frame}{THML: syntax}
    \begin{block}{Syntax}
        The set of Hennessy-Milner formulae with time $\mathcal{M}_t$, over a set of actions \chfont{Act} and a set of
        formula clocks $D$ is given by the following syntax:
        \begin{equation*}
            F ::= \mathit{tt}~|~\mathit{ff}~|~F \land G~|~F \lor G~|~\langle a \rangle F~|~[a]F~|~\mathrlap{\exists}\,\exists
            F~|~\mathrlap{\forall}\,\forall F~|~ x~\texttt{\underline{in}}~F~|~ g
        \end{equation*}
  where $a \in \chfont{Act}$, $x \in D$ and $g \in \mathcal{B}(D)$.
    \end{block}
\end{frame}

\subsection{Semantics}
\begin{frame}{THML: semantics}
    The semantics of formulae is given with respect to a given TLTS
    \begin{equation*}
        (\chfont{Proc}, \chfont{Lab}, \{\xrightarrow{~\alpha~}~:~\alpha \in \chfont{Lab}\}).
    \end{equation*}
    \begin{block}{Extended state}
        An \emph{extended state} over \chfont{Proc} is a pair $(p,u)$ where $p$ is a state in \chfont{Proc} and $u$ is a
        mapping $u : D \to \R_{\geq 0}$. The set of extended states over \chfont{Proc} is denoted by
        $\mathcal{ES}(\chfont{Proc})$.
    \end{block}
\end{frame}

\begin{frame}{THML: semantics}
    \begin{block}{Semantics}
        We define $\llbracket F \rrbracket \subseteq \mathcal{ES}(\chfont{Proc})$ for $F \in \mathcal{M}_t$ by\\~\\
        {\tabulinesep=1.5mm
        \begin{tabu}{l l}
            $\llbracket \mathit{tt} \rrbracket = \mathcal{ES}(\chfont{Proc})$
            &
            $\llbracket F \lor G \rrbracket = \llbracket F \rrbracket \cup \llbracket G \rrbracket$\\
            $\llbracket \mathit{ff} \rrbracket = \emptyset$
            &
            $\llbracket \langle a \rangle F \rrbracket = \langle \cdot a \cdot \rangle \llbracket F \rrbracket$\\
            $\llbracket F \land G \rrbracket = \llbracket F \rrbracket \cap \llbracket G \rrbracket$
            &
            $\llbracket [ a ] F \rrbracket = [ \cdot a \cdot ] \llbracket F \rrbracket$\\
            $\llbracket \mathrlap{\exists}\,\exists F \rrbracket = \langle \cdot \varepsilon \cdot \rangle \llbracket F
            \rrbracket$
            &
            $\llbracket \mathrlap{\forall}\,\forall F \rrbracket = [ \cdot \varepsilon \cdot ] \llbracket F \rrbracket$\\
            $\llbracket x~\texttt{\underline{in}}~F \rrbracket = \{(p,u) : (p,u[x \mapsto 0]) \in \llbracket F \rrbracket \}$
            &\\
            $\llbracket g \rrbracket = \{(p,u) : p \in \chfont{Proc}, u \models g \}$
        \end{tabu}
        }
    \end{block}
\end{frame}

\begin{frame}{THML: semantics}
    Where the operators $\langle \cdot a \cdot \rangle, [\cdot a \cdot], \langle \cdot \varepsilon \cdot \rangle, [\cdot
    \varepsilon \cdot] : \wp(\mathcal{ES}(\chfont{Proc})) \to \wp(\mathcal{ES}(\chfont{Proc}))$ are defined by 
    \begin{align*}
        & \langle \cdot a \cdot \rangle S = \{(p,u) \in \mathcal{ES}(\chfont{Proc}) : \exists p'. p \xrightarrow{a} p'
        \text{ and } (p',u) \in S \}\\
        & [ \cdot a \cdot ] S = \{(p,u) \in \mathcal{ES}(\chfont{Proc}) : \forall p'. p \xrightarrow{a} p'
        \text{ implies } (p',u) \in S \}\\
        & \langle \cdot \varepsilon \cdot \rangle S = \{(p,u) \in \mathcal{ES}(\chfont{Proc}) : \exists d \in \R_{\geq
        0} . \exists p' \in \chfont{Proc}. p \xrightarrow{d} p' \text{ and }\\
        & \qquad\qquad\quad(p',u+d) \in S \}\\
        & [ \cdot \varepsilon \cdot ] S = \{(p,u) \in \mathcal{ES}(\chfont{Proc}) : \forall d \in \R_{\geq
        0} . \forall p' \in \chfont{Proc}. p \xrightarrow{d} p' \text{ implies }\\
        & \qquad\qquad\quad(p',u+d) \in S \}
    \end{align*}
    We write $(p,u) \models F$ iff $(p,u) \in \llbracket F \rrbracket$. Two formulae are \emph{equivalent} iff they are
    satisfied by the same extended states in every TLTS.
\end{frame}

\begin{frame}{THML: semantics}
    \begin{definition}
    A state $p$ in a TLTS satisfies a formula $F$, $p \models F$, iff $(p,u_0) \models F$, where $u_0$ is a clock valuation
    mapping each formula clock to zero.
    \end{definition}
    The above definition can be applied to a TLTS $T(\mathcal{A})$ generated from a timed automaton $\mathcal{A}$. For this
    TLTS, extended states take the form $((l,v),u)$ where $v$ is a valuation for the set of clocks $C$ in $\mathcal{A}$ and
    $u$ is a valuation for the set of clocks $D$ used in writing the formulae of $\mathcal{M}_t$. We assume that $C$ and
    $D$ are disjoint: $C \cap D = \emptyset$.

    \begin{definition}\label{def:sat}
    A timed automaton $\mathcal{A}$ satisfies a formula $F \in \mathcal{M}_t$ iff $((l_0,v_0),u_0) \models F$.\\
    Where $l_0$ is the initial location in $\mathcal{A}$ and $v_0,u_0$ are clock valuations that map each clock variable
    in the automaton and in the formula to 0. From now on, we'll use $\mathcal{A} \models F$ instead of 
    $((l_0,v_0),u_0) \models F$.
    \end{definition}
\end{frame}

\subsection{Model checking}
\begin{frame}{THML: model checking}
    The notion of regions is the key tool for proving the decidability of model-checking problems for timed automata
    w.r.t. THML.
    \begin{block}{Model checking}
        The model checking problem for THML consists in deciding if $((l,v),u) \models F$ where :
        \begin{itemize}
            \item $(l,v)$ is a state of a timed automaton $\mathcal{A}$;
            \item $l$ is a location of $\mathcal{A}$;
            \item $v$ and $u$ are respectively a valuation for the set of clocks $C$ of $\mathcal{A}$ and for the set of 
                formula clocks $D$;
            \item $F$ is a formula of $\mathcal{M}_t$. 
        \end{itemize}
    \end{block}
\end{frame}
       
\begin{frame}{THML: model checking}
    To do this we'll consider \emph{symbolic model checking} problems of the form
    \begin{equation*}
    [l,\gamma] \vdash F,
    \end{equation*}
    where $\gamma$ is a region over $C \cup D$, a region over the disjoint union of the set of automata and formula
    clocks.\\~\\

    Let's introduce some notation on regions:
    \begin{itemize}
        \item given a region $\gamma$ and a constraint $g$ we say that $\gamma$ satisfies $g$ ($\gamma \models g$), if $v
            \models g$ for some (or all) $v \in \gamma$;
        \item for two regions $\gamma$ and $\gamma'$ and a set of clocks $R$, we say that $\gamma'$ is the reset of $\gamma$ with
            respect to $R$ ($\gamma' = \gamma[R]$), if $v[R] \in \gamma'$ for some (or all) $v \in \gamma$;
        \item given two regions $\gamma$ and $\gamma'$, we say that $\gamma'$ is a delay successor of $\gamma$, written
            $\gamma \leadsto \gamma'$, if for each $v \in \gamma$ there exists $d \in \R_{\geq 0}$ such that $v+d \in \gamma'$.
    \end{itemize}
\end{frame}

\begin{frame}{THML: model checking}
    Let $\mathcal{A}$ be a timed automaton with clocks $C$, let's consider formulae over $\mathcal{M}_t$ with a set of
    formula clocks $D$, where $C$ and $D$ are disjoint. If $l$ is a location of $\mathcal{A}$, $F$ is a formula and
    $\gamma$ a region over $C \cup D$ such that $\gamma \models I(l)$, we define \emph{symbolic satisfaction} $[l,\gamma] \vdash
    F$ as follows:
    \begin{align*}
        & [l,\gamma] \vdash \mathit{tt} \text{ for each } [l,\gamma]\\
        & [l,\gamma] \vdash \mathit{ff} \text{ for no } [l,\gamma]\\
        & [l,\gamma] \vdash F \land G \text{ iff } [l,\gamma] \vdash F \text{ and } [l,\gamma] \vdash G\\
        & [l,\gamma] \vdash F \lor G \text{ iff } [l,\gamma] \vdash F \text{ or } [l,\gamma] \vdash G\\
        & [l,\gamma] \vdash \langle a \rangle F \text{ iff there is an edge } l \xrightarrow{g,a,R} l' \text{ in } \mathcal{A}
        \text{ with } \gamma \models g \text{ and } [l',\gamma[R]] \vdash F\\
        & [l,\gamma] \vdash [ a ] F \text{ iff whenever } l \xrightarrow{g,a,R} l' \text{ is an edge in } \mathcal{A}
        \text{ such that } \gamma \models g\\
        & \qquad\quad\text{ then } [l',\gamma[R]] \vdash F\\
        & [l,\gamma] \vdash \mathrlap{\exists}\,\exists F \text{ iff } \gamma \leadsto \gamma' \text{ for some } \gamma'
        \text{ such that } \gamma' \models I(l) \text{ and } [l,\gamma'] \vdash F\\
        & [l,\gamma] \vdash \mathrlap{\forall}\,\forall F \text{ iff whenever } \gamma \leadsto \gamma' \text{ with } 
        \gamma' \models I(l) \text{ then } [l,\gamma'] \vdash F
    \end{align*}
\end{frame}

\begin{frame}{THML: model checking}
    \begin{theorem}
    Let $\mathcal{A}$ be a timed automaton with clock set $C$ and consider formulae over $\mathcal{M}_t$ with a set of
    formula clocks $D$, with $C$ and $D$ disjoint. Then
    \begin{equation*}
        ((l,v), u) \models F \text{\upshape\text{ iff }} [l,[vu]] \vdash F,
    \end{equation*}
    where $v$ is a valuation over $C$, $u$ is a valuation over $D$, and $vu$ is the valuation over $C \cup D$ such that
    $vu(z)$ equals $v(z)$ for $z \in C$ and $u(z)$ otherwise.
    \end{theorem}

    From this theorem and from the finiteness of the number of regions it follows that model checking for THML is
    decidable.

    \begin{theorem}
    THML model checking over timed automata is decidable.
    \end{theorem}

    \begin{theorem}
    The model checking problem for $\mathcal{M}_t$ over timed automata is \textsc{PSPACE}-complete.
    \end{theorem}
\end{frame}


\section{Bibliography}
\begin{frame}[allowframebreaks]{Bibliography}
    \bibliographystyle{unsrt}
    \bibliography{biblio}
    \nocite{*}
\end{frame}

\end{document}

A  => slides/thud.cls +185 -0
@@ 1,185 @@
\NeedsTeXFormat{LaTeX2e}[1995/12/01]
\ProvidesClass{thud}[2014/03/11]

\RequirePackage{kvoptions}
\SetupKeyvalOptions{prefix={\@currname @opt@}}

\def\thud@tmpcmd{\relax}
\DeclareStringOption[\relax]{beamer}[]
\DeclareStringOption{target}

\ProcessKeyvalOptions{\@currname}

\newif\ifthud@beamer
\ifx\thud@opt@beamer\thud@tmpcmd\else\thud@beamertrue\fi

\def\thud@save#1{\expandafter\let\csname thud@save@#1\expandafter\endcsname\csname#1\endcsname}
\def\thud@restore#1{\expandafter\let\csname#1\expandafter\endcsname\csname thud@save@#1\endcsname}
\def\@ifplus#1{\@ifnextchar+{\@firstoftwo{#1}}}

\def\thud@tmpcmd{bach}
\ifx\thud@opt@target\thud@tmpcmd
    \chardef\thud@target\z@\relax
\else
    \def\thud@tmpcmd{mst}
    \ifx\thud@opt@target\thud@tmpcmd
        \chardef\thud@target\@ne\relax
    \else
        \def\thud@tmpcmd{phd}
        \ifx\thud@opt@target\thud@tmpcmd
            \chardef\thud@target\tw@\relax
        \else
            \ClassError{\@currname}{Invalid value for the \protect"target\protect" option}
                {Specify one of \protect"bach\protect", \protect"mst\protect" or \protect"phd\protect"}
        \fi
    \fi
\fi
\newif\ifthud@phd
\ifnum\thud@target=\tw@\relax\thud@phdtrue\fi

\ifthud@beamer
\LoadClass[\thud@opt@beamer]{beamer}
\else
\LoadClass[onecolumn,twoside,\ifthud@phd 10\else 11\fi pt]{book}
\fi

\def\thud@nonegiven#1{\ClassError{thud}{No \expandafter\string\csname#1\endcsname\space given}{Provide an \expandafter\string\csname#1\endcsname.}}
\def\@author{\thud@nonegiven{author}}
\def\@date{\begingroup\expandafter\advance\expandafter\year\ifnum\month>3 -1 \else -2 \fi\the\year-\advance\year1 \the\year\endgroup}

\RequirePackage{graphicx}
\RequirePackage[\thudbabelopt]{babel}
\ifthud@beamer\else
\RequirePackage{setspace}
\RequirePackage[\ifthud@phd c5paper\else a4paper\fi]{geometry}
\fi

\addto\captionsenglish{%
    \def\abstractname{Abstract}%
    \def\acknowledgementsname{Acknowledgements}%
    \def\authorcontactsname{Author's Contacts}%
    \def\candidatename{Candidate}%
    \def\chairname{Chair}%
    \def\conclusionsname{Conclusions}%
    \def\cosupervisorname{Co-Supervisor}%
    \def\cosupervisorsname{Co-Supervisors}%
    \def\cyclename{Cycle}%
    \def\datename{Academic Year}%
    \def\indexname{Index}%
    \def\institutecontactsname{Institute Contacts}%
    \def\introductionname{Introduction}%
    \def\prefacename{Preface}%
    \def\reviewername{Reviewer}%
    \def\reviewersname{Reviewers}%
    \def\shortdatename{A.Y.}%
    \def\summaryname{Summary}%
    \def\supervisorname{Supervisor}%
    \def\supervisorsname{Supervisors}%
    \def\thesisname{\ifcase\thud@target Bachelor\space\or Master\space\or Ph.D.~\fi Thesis}%
    \def\tutorname{Tutor}%
    \def\tutorsname{Tutors}%
}
\addto\captionsitalian{%
    \def\abstractname{Sommario}%
    \def\acknowledgementsname{Ringraziamenti}%
    \def\authorcontactsname{Contatti dell'autore}%
    \def\candidatename{}%
    \def\chairname{Direttore}%
    \def\conclusionsname{Conclusioni}%
    \def\cosupervisorname{Co-relatore}%
    \def\cosupervisorsname{Co-relatori}%
    \def\cyclename{Ciclo}%
    \def\datename{Anno accademico}%
    \def\indexname{Indice analitico}%
    \def\institutecontactsname{Contatti dell'Istituto}%
    \def\introductionname{Introduzione}%
    \def\prefacename{Prefazione}%
    \def\reviewername{Controrelatore}%
    \def\reviewersname{Controrelatori}%
    \def\shortdatename{A.A.}%
    \def\summaryname{Riassunto}%
    \def\supervisorname{Relatore}%
    \def\supervisorsname{Relatori}%
    \def\thesisname{Tesi di \ifcase\thud@target Laurea\or Laurea Magistrale\or Dottorato\fi}%
    \def\tutorname{Tutor aziendale}%
    \def\tutorsname{Tutor aziendali}%
}

\gdef\thud@universityA{%
    Universit\`a degli Studi di Udine\\[\thud@unisep]%
    Dipartimento di Scienze Matematiche, Informatiche e Fisiche\\[\thud@unisep]%
    \ifcase\thud@target Corso di Laurea\or Corso di Laurea Magistrale\or Dottorato di Ricerca\fi\space in \thud@course%
}
\gdef\thud@universityB{%
    Dipartimento di Scienze Matematiche, Informatiche e Fisiche\\%
    Universit\`a degli Studi di Udine\\
    Via delle Scienze, 206\\
    33100 Udine --- Italia\\
    +39 0432 558400\\
    \@ifundefined{url}\texttt\url{http://www.dimi.uniud.it/}
}

\def\@true{true}
\define@key{defentry}{long}[true]{%
    \def\thud@de@a{#1}%
    \ifx\@true\thud@de@a\let\thud@de@b\long\fi%
}
\define@key{defentry}{phd}[true]{%
    \def\thud@de@a{#1}%
    \ifx\@true\thud@de@a%
        \expandafter\let\csname ifthud@de@c\expandafter\endcsname\csname ifthud@phd\endcsname%
    \fi%
}
\define@key{defentry}{nonempty}[true]{%
    \def\thud@de@a{#1}%
    \ifx\@true\thud@de@a%
        \expandafter\let\csname ifthud@de@d\expandafter\endcsname\csname iftrue\endcsname%
    \fi%
}
\newcommand\thud@defentry[2][]{
	\let\thud@de@b\relax
	\let\ifthud@de@c\iftrue
	\let\ifthud@de@d\iffalse
    \setkeys{defentry}{#1}%
    \ifthud@de@d%% Either \iftrue or \iffalse
        \@namedef{thud@#2}{\thud@nonegiven{#2}}
    \else
        \expandafter\let\csname thud@#2\endcsname\@empty
    \fi
    \expandafter\thud@de@b\ifthud@de@c%% Either \iftrue or \ifthud@phd
        \@namedef{#2}##1{\expandafter\gdef\csname thud@#2\endcsname{##1}}
    \else
        \@namedef{#2}##1{\ClassWarning{\@currname}{\expandafter\string\csname#2\endcsname\space in non-PhD thesis}}
    \fi%
}
\thud@defentry{chair}
\thud@defentry[phd,long]{contacts}
\thud@defentry{cosupervisor}
\thud@defentry[nonempty]{course}
\thud@defentry[phd]{email}
\thud@defentry[phd]{homepage}
\thud@defentry[phd]{phdnumber}
\thud@defentry[phd]{reviewer}
\thud@defentry[phd,long]{rights}
\thud@defentry{supervisor}
\thud@defentry[phd]{telephone}
\thud@defentry[phd]{cycle}
\thud@defentry{tutor}

\newsavebox\thud@tmpbox
\def\thud@showentry@#1#2{%
    \expandafter\ifx\csname thud@#2\endcsname\@empty\else%
        \def\thud@varname{\@nameuse{#2name}}%
        #1%% Either \iftrue or \iffalse
            \def\and{\\[\thud@se@and]\gdef\thud@varname{\@nameuse{#2sname}}}%
        \else%
            \let\and\@undefined
        \fi%
        \begin{lrbox}{\thud@tmpbox}\parbox[t]{\linewidth}{\@nameuse{thud@#2}}\end{lrbox}%
        \textsc{\thud@varname}\\[\thud@se@qual]%
        \usebox{\thud@tmpbox}\\[\thud@se@sep]\null%
    \fi%
}
\def\thud@showentry{\@ifstar{\expandafter\thud@showentry@\noexpand\iffalse}{\expandafter\thud@showentry@\noexpand\iftrue}}

\input{\ifthud@beamer beamer\else book\fi.thud.tex}