master-thesis.tex

% !TeX root = thesis.tex
% !TeX spellcheck = en_US
% !TeX encoding = UTF-8
\documentclass[english, LaM, oneside]{sapthesis}%remove "english" for a thesis written in Italian

%\usepackage[utf8]{inputenx}
%\usepackage{xcolor}
%\usepackage{indentfirst}
%\usepackage{microtype}

%\usepackage{lettrine}
%\linespread{0.9}

% This can be used to make space between section names more compact. The titlesec package allows changing how chapters are displayed, numerated, etc.
%\usepackage[compact]{titlesec}
% to get the bibliography in the toc
\usepackage[nottoc,notlot,notlof,chapter]{tocbibind}

\newcommand{\thesistitle}{{\sc ltl} and Past {\sc ltl} on Finite Traces for Planning and Declarative Process Mining}

\usepackage{index}
\usepackage{hyperref}
\usepackage{wrapfig}
\usepackage[round]{natbib}
\bibliographystyle{plainnat}

\usepackage[intoc,refpage]{nomencl} %refeq
\makenomenclature

%\usepackage{qtree}
% The algorithm packages have to be after hyperref.
\usepackage{algorithm}
\usepackage{algpseudocode}

\algnewcommand\algorithmicforeach{\textbf{foreach}}
\algdef{S}[FOR]{ForEach}[1]{\algorithmicforeach\ #1\ \algorithmicdo}

\usepackage{mathtools}
\usepackage{amssymb, amsmath, amsthm}
\usepackage{xspace, float, graphicx, pstricks}
%\usepackage{mathabx}

\usepackage{caption}% http://ctan.org/pkg/caption
\captionsetup[ruled]{labelsep=period}
\makeatletter
\@addtoreset{algorithm}{chapter}% algorithm counter resets every chapter
\makeatother
\renewcommand{\thealgorithm}{\thechapter.\arabic{algorithm}}% Algorithm # is <chapter>.<algorithm>

\usepackage{subcaption}
%\usepackage[autostyle]{csquotes}  
\usepackage{graphicx}
%\graphicspath{{./images/}}
\usepackage{rotating}     

\usepackage{listings}
% Custom colors
\usepackage{color}
\definecolor{deepblue}{rgb}{0,0,0.5}
\definecolor{deepred}{rgb}{0.6,0,0}
\definecolor{deepgreen}{rgb}{0,0.5,0}
\definecolor{backcolour}{rgb}{0.95,0.95,0.92}
\definecolor{codegray}{rgb}{0.5,0.5,0.5}

\usepackage{accsupp}    
\newcommand{\noncopynumber}[1]{
	\BeginAccSupp{method=escape,ActualText={}}
	#1
	\EndAccSupp{}
}
\lstdefinestyle{Python}{
	language        = Python,
	backgroundcolor=\color{backcolour},
	basicstyle      = \ttfamily,
	keywordstyle    = \color{deepblue},
	stringstyle     = \color{deepgreen},
	commentstyle    = \color{codegray}\ttfamily,
	numberstyle=\tiny\color{codegray}\noncopynumber,
	columns=flexible,
	numbers=left,
	stepnumber=1
}

\lstdefinestyle{Mona}{
	basicstyle      = \ttfamily,
	numberstyle=\tiny\color{codegray}\noncopynumber,	
	columns=flexible,
	numbers=left,
	stepnumber=1	
}

\lstdefinelanguage{PDDL}{
  basicstyle      = \ttfamily,
  sensitive=false,    % not case-sensitive
  morecomment=[l]{;}, % line comment
  alsoletter={:,-},   % consider extra characters
  numberstyle=\tiny\color{codegray}\noncopynumber,	
  numbers=left,
  stepnumber=1,
  morekeywords={
    define,domain,problem,not,and,or,when,forall,exists,either,
    :domain,:requirements,:types,:objects,:constants,
    :predicates,:action,:parameters,:precondition,:effect,
    :fluents,:primary-effect,:side-effect,:init,:goal,
    :strips,:adl,:equality,:typing,:conditional-effects,
    :negative-preconditions,:disjunctive-preconditions,
    :existential-preconditions,:universal-preconditions,:quantified-preconditions,
    :functions,assign,increase,decrease,scale-up,scale-down,
    :metric,minimize,maximize,
    :durative-actions,:duration-inequalities,:continuous-effects,
    :durative-action,:duration,:condition
  }
}
%references color
\hypersetup{
	hyperfootnotes=true,            
	bookmarks=true,         
	colorlinks=true,
	linkcolor=black, %red
	linktoc=page,
	anchorcolor=black,
	citecolor=black, %red
	urlcolor=black, %blue
	pdftitle={\thesistitle},
	pdfsubject = {Master Thesis, University of Rome ``Sapienza''},
	pdfauthor={Francesco Fuggitti},
	pdfkeywords={master thesis, sapienza, roma, university, francesco fuggitti}
	pdfauthor = {\textcopyright\ \today\ Francesco Fuggitti},
}

\theoremstyle{plain}
\newtheorem{theorem}{Theorem}[chapter] % reset theorem numbering for each chapter
\newtheorem{lemma}[theorem]{Lemma}
\theoremstyle{definition}
\newtheorem{definition}{Definition}[chapter]
\newtheorem{example}{Example}[chapter]

\newgeometry{twoside}

%opening
\title{\thesistitle}
\author{Francesco Fuggitti}
\IDnumber{1735212}
\course[override]{Master of Science in Engineering in Computer Science}
\courseorganizer{Faculty of Information Engineering, Informatics, and Statistics}
\submitdate{2017/2018}
\copyyear{2018}
\advisor{Prof. Giuseppe De Giacomo}
\authoremail{fuggitti.1735212@studenti.uniroma1.it}
\examdate{$31^{\text{st}}$ October 2018}
\examiner{Prof. Alberto Marchetti Spaccamela}
\examiner{Prof. Silvia Bonomi}
\examiner{Prof. Francesco Delli Priscoli}
\examiner{Prof. Maurizio Lenzerini}
\examiner{Prof. Daniele Nardi}
\examiner{Prof. Leonardo Querzoni}
\examiner{Prof. Marco Schaerf}    

\allowdisplaybreaks

\begin{document}
	\input{macros}
	
	\frontmatter	
	\maketitle
	
\begin{abstract}
The application of \LTL and Past \LTL on Finite Traces is of particular interest for different fields in Artificial Intelligence (AI) and Computer Science (CS). In this thesis, we focus on the application of these two formal languages to Planning and Declarative Process Mining. For this purpose, the design and implementation of the \LTLfToDFA framework has been crucial to the application of \LTLf and \PLTL in both research fields. In Planning, we direct our attention to \FOND planning for \LTLf and \PLTL goals showing a new encoding of those temporal goals in standard \PDDL. We formally provide experimental evidence that it is possible to restrict the manner used by the plan to reach the goal specified in future and past modalities. With respect to Declarative Process Mining, we generalize the Janus approach for computing the interestingness of traces out of event logs, giving a new representation of the constraint formula allowing propositional formulas as activation condition.
\end{abstract}
	

	
	\tableofcontents
%	\listoffigures
%	\listoftables
	
	\mainmatter
	\input{chapters/introduction}
	\input{chapters/ltl}
	\input{chapters/ltlf2dfa}
	\input{chapters/planning}
	\input{chapters/janus}
	\input{chapters/conclusions}
	
%	\appendix 
%	\input{chapters/appendix-flloat}
%	\input{chapters/appendix-rltg}

	
	\backmatter
	\phantomsection
	
	\bibliography{bib.bib}
	

\end{document}