96 lines
4.1 KiB
TeX
96 lines
4.1 KiB
TeX
|
\relax
|
||
|
|
\providecommand\hyper@newdestlabel[2]{}
|
||
|
|
\providecommand\HyperFirstAtBeginDocument{\AtBeginDocument}
|
||
|
|
\HyperFirstAtBeginDocument{\ifx\hyper@anchor\@undefined
|
||
|
|
\global\let\oldcontentsline\contentsline
|
||
|
|
\gdef\contentsline#1#2#3#4{\oldcontentsline{#1}{#2}{#3}}
|
||
|
|
\global\let\oldnewlabel\newlabel
|
||
|
|
\gdef\newlabel#1#2{\newlabelxx{#1}#2}
|
||
|
|
\gdef\newlabelxx#1#2#3#4#5#6{\oldnewlabel{#1}{{#2}{#3}}}
|
||
|
|
\AtEndDocument{\ifx\hyper@anchor\@undefined
|
||
|
|
\let\contentsline\oldcontentsline
|
||
|
|
\let\newlabel\oldnewlabel
|
||
|
|
\fi}
|
||
|
|
\fi}
|
||
|
|
\global\let\hyper@last\relax
|
||
|
|
\gdef\HyperFirstAtBeginDocument#1{#1}
|
||
|
|
\providecommand\HyField@AuxAddToFields[1]{}
|
||
|
|
\providecommand\HyField@AuxAddToCoFields[2]{}
|
||
|
|
\@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{1}{section.1}\protected@file@percent }
|
||
|
|
\newlabel{sec:org6f2d2bd}{{1}{1}{Introduction}{section.1}{}}
|
||
|
|
\@writefile{toc}{\contentsline {subsection}{\numberline {1.1}Model Checking}{1}{subsection.1.1}\protected@file@percent }
|
||
|
|
\newlabel{sec:org4914978}{{1.1}{1}{Model Checking}{subsection.1.1}{}}
|
||
|
|
\citation{Pnueli77}
|
||
|
|
\citation{ClarkeE81}
|
||
|
|
\citation{Lamport80}
|
||
|
|
\citation{EmersonH86}
|
||
|
|
\citation{Vardi95}
|
||
|
|
\citation{Keller76}
|
||
|
|
\citation{Sistlac85}
|
||
|
|
\citation{Holzmann97}
|
||
|
|
\citation{HolzmannPy96}
|
||
|
|
\citation{FernandezMJJ92}
|
||
|
|
\citation{Peled96}
|
||
|
|
\@writefile{toc}{\contentsline {subsection}{\numberline {1.2}A brief history of LTL model checking}{3}{subsection.1.2}\protected@file@percent }
|
||
|
|
\newlabel{sec:org25c390b}{{1.2}{3}{A brief history of LTL model checking}{subsection.1.2}{}}
|
||
|
|
\citation{SymbMC}
|
||
|
|
\citation{Clarke08}
|
||
|
|
\citation{ClarkeES86}
|
||
|
|
\citation{KantLMPBD15}
|
||
|
|
\citation{DijkP17}
|
||
|
|
\citation{CimattiCGGPRST02}
|
||
|
|
\citation{BiereCCZ99}
|
||
|
|
\citation{BolligW96}
|
||
|
|
\@writefile{toc}{\contentsline {subsection}{\numberline {1.3}The origin of symbolic model checking}{4}{subsection.1.3}\protected@file@percent }
|
||
|
|
\newlabel{sec:orgce6f633}{{1.3}{4}{The origin of symbolic model checking}{subsection.1.3}{}}
|
||
|
|
\citation{BabarM10}
|
||
|
|
\citation{BabarBDM10}
|
||
|
|
\citation{AmparoreDBGM17}
|
||
|
|
\citation{ClarkeGH97}
|
||
|
|
\@writefile{toc}{\contentsline {section}{\numberline {2}Background}{5}{section.2}\protected@file@percent }
|
||
|
|
\newlabel{sec:orga42ce82}{{2}{5}{Background}{section.2}{}}
|
||
|
|
\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Linear Temporal Logic}{5}{subsection.2.1}\protected@file@percent }
|
||
|
|
\newlabel{sec:orgdbca314}{{2.1}{5}{Linear Temporal Logic}{subsection.2.1}{}}
|
||
|
|
\@writefile{toc}{\contentsline {paragraph}{LTL Semantics}{6}{section*.1}\protected@file@percent }
|
||
|
|
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}CTL*}{6}{subsection.2.2}\protected@file@percent }
|
||
|
|
\newlabel{sec:orgfa1652d}{{2.2}{6}{CTL*}{subsection.2.2}{}}
|
||
|
|
\citation{Bryant86}
|
||
|
|
\citation{MDD}
|
||
|
|
\@writefile{toc}{\contentsline {paragraph}{CTL* Semantics}{7}{section*.2}\protected@file@percent }
|
||
|
|
\@writefile{toc}{\contentsline {paragraph}{State formulae: semantics}{7}{section*.3}\protected@file@percent }
|
||
|
|
\@writefile{toc}{\contentsline {paragraph}{Path formulae: semantics}{7}{section*.4}\protected@file@percent }
|
||
|
|
\@writefile{toc}{\contentsline {subsection}{\numberline {2.3}Decision Diagrams}{8}{subsection.2.3}\protected@file@percent }
|
||
|
|
\newlabel{sec:org4ea21ea}{{2.3}{8}{Decision Diagrams}{subsection.2.3}{}}
|
||
|
|
\@writefile{toc}{\contentsline {paragraph}{Reduced ordered MDDs}{8}{section*.5}\protected@file@percent }
|
||
|
|
\citation{VardiW94}
|
||
|
|
\bibstyle{/usr/share/texmf-dist/bibtex/bst/base/acm}
|
||
|
|
\bibdata{tesi}
|
||
|
|
\bibcite{AmparoreDBGM17}{1}
|
||
|
|
\@writefile{toc}{\contentsline {subsection}{\numberline {2.4}Automata over infinite words}{9}{subsection.2.4}\protected@file@percent }
|
||
|
|
\newlabel{sec:org350d6d0}{{2.4}{9}{Automata over infinite words}{subsection.2.4}{}}
|
||
|
|
\bibcite{BabarBDM10}{2}
|
||
|
|
\bibcite{BabarM10}{3}
|
||
|
|
\bibcite{BiereCCZ99}{4}
|
||
|
|
\bibcite{BolligW96}{5}
|
||
|
|
\bibcite{Bryant86}{6}
|
||
|
|
\bibcite{CimattiCGGPRST02}{7}
|
||
|
|
\bibcite{Clarke08}{8}
|
||
|
|
\bibcite{ClarkeE81}{9}
|
||
|
|
\bibcite{ClarkeES86}{10}
|
||
|
|
\bibcite{ClarkeGH97}{11}
|
||
|
|
\bibcite{EmersonH86}{12}
|
||
|
|
\bibcite{FernandezMJJ92}{13}
|
||
|
|
\bibcite{Holzmann97}{14}
|
||
|
|
\bibcite{HolzmannPy96}{15}
|
||
|
|
\bibcite{MDD}{16}
|
||
|
|
\bibcite{KantLMPBD15}{17}
|
||
|
|
\bibcite{Keller76}{18}
|
||
|
|
\bibcite{Lamport80}{19}
|
||
|
|
\bibcite{SymbMC}{20}
|
||
|
|
\bibcite{Peled96}{21}
|
||
|
|
\bibcite{Pnueli77}{22}
|
||
|
|
\bibcite{Sistlac85}{23}
|
||
|
|
\bibcite{DijkP17}{24}
|
||
|
|
\bibcite{Vardi95}{25}
|
||
|
|
\bibcite{VardiW94}{26}
|