From: Christoph Egger Date: Mon, 25 Apr 2016 07:27:50 +0000 (+0200) Subject: Add more text X-Git-Url: https://git.siccegge.de//index.cgi?a=commitdiff_plain;h=edc63ce858f06a6b08536f876c7328820edd92a8;p=talk%2Fcoalgebraic-mu-calculus-cool-2.git Add more text --- diff --git a/chapters/benchmark.tex b/chapters/benchmark.tex new file mode 100644 index 0000000..5342771 --- /dev/null +++ b/chapters/benchmark.tex @@ -0,0 +1,13 @@ +\section{Benchmarks} +\subsection*{Dummy} + +\begin{frame} + TODO: some representative benchmarks with GMUL/TreeTab/Cool(/MLSolver?) +\end{frame} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../vortrag" +%%% TeX-engine: luatex +%%% TeX-PDF-mode: t +%%% End: diff --git a/chapters/early.tex b/chapters/early.tex new file mode 100644 index 0000000..d557390 --- /dev/null +++ b/chapters/early.tex @@ -0,0 +1,22 @@ +\section{``Early'' formulas} +\subsection*{Dummy} + +\begin{frame} + \begin{itemize} + \item Existing benchmark formulas either require exponential model + or have small unfolding + \item \emph{early} class of formulas have exponential unfolding but + exponetial subgraphs can be dealt with fast + \end{itemize} +\end{frame} + +\begin{frame} + TODO construction +\end{frame} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../vortrag" +%%% TeX-engine: luatex +%%% TeX-PDF-mode: t +%%% End: diff --git a/chapters/finishingcool.tex b/chapters/finishingcool.tex new file mode 100644 index 0000000..a90f7b8 --- /dev/null +++ b/chapters/finishingcool.tex @@ -0,0 +1,50 @@ +\section{Finishing Cool} +\subsection*{Dummy} + +\begin{frame}{Where we left (TODO)} + \begin{itemize} + \item actually implementing deferral tracking + \item deciding when some deferral can be considered ``finished'' + \item \dots + \item finding ``right'' heuristic for when to try and close the tableaux + \item fixing all the bugs + \end{itemize} +\end{frame} + +\begin{frame}{Extra nodes} + \begin{itemize} + \item Different set of deferrals create different Nodes + \item Exponential increase in Nodes + \end{itemize} +\end{frame} + +\begin{frame} + TODO: graphviz der $p\#q\#$ formel +\end{frame} + +\begin{frame}{Propagation} + \begin{itemize} + \item Cool works in rounds + \begin{itemize} + \item One further solution from each Core (propositional) + \item All possible modal steps + \end{itemize} + \item Check for satisfiability after \#{}OpenStates rounds\pause + \item Ideas + \begin{itemize} + \item Creating cycles forces earlier propagation + \item Use \#{}OpenStates steps, not rounds + \end{itemize} + \end{itemize} +\end{frame} + +\begin{frame} + TODO: auswertungen mit ``jedes'' mal propagieren, current magic, nie propagieren +\end{frame} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../vortrag" +%%% TeX-engine: luatex +%%% TeX-PDF-mode: t +%%% End: diff --git a/chapters/optimizations.tex b/chapters/optimizations.tex new file mode 100644 index 0000000..9877634 --- /dev/null +++ b/chapters/optimizations.tex @@ -0,0 +1,67 @@ +\section{Optimizing} +\subsection*{Dummy} + +\begin{frame}{Semnatic Branching} + \begin{itemize} + \item Idea: Add aditional information when considering second + alternative of an or: ${\phi \vee \psi}$ becomes ${\phi \vee + (¬\phi \wedge \psi)}$ + \item Do not reexplore branches already known to be unsat already + \end{itemize} +\end{frame} + +\begin{frame}{Non-atomic Negations} + TODO: ? + \begin{itemize} + \item Consider $\heartsuit\heartsuit\heartsuit{}p \wedge \overline{\heartsuit}\overline{\heartsuit}\overline{\heartsuit}¬p$ + \item Same as $\heartsuit\heartsuit\heartsuit{}p \wedge + ¬\heartsuit\heartsuit\heartsuit{}p$ and thus obviously unsatisfiable + \item Cool normalizes formulas to make best use of Global Caching + \end{itemize} +\end{frame} + +\begin{frame}{Subset Nodes} + \begin{itemize} + \item Lemma: If some Node is already satisfiable, all Nodes with + subsets of formulas, deferrals are also satisfiable + \item Too expensive to check in general\pause + \item Might be interesting for Nodes with full focus and its + siblings with the same set of formulas + \item Cheap but does this happen often? + \end{itemize} +\end{frame} + +\begin{frame}{Normalization} + TODO: ? + \begin{itemize} + \item Global Caching better with more same formulas + \item Preprocessing in Cool currently does not consider + (propositional) Comutativity, Associativity or Distributivity laws + \end{itemize} +\end{frame} + + +\begin{frame}{Removing Edges} + \begin{block}{Propagation} + \begin{itemize} + \item Runs in $O(edge\cdot nodes)$ + \item Needs to consider all satisfiable nodes + \item Iterates over all edges + \end{itemize} + \end{block}\pause + \begin{itemize} + \item Idea: Remove unneeded edges + \item Cores are $\exists$-quantified -- all unsatisfiable children + may be removed + \item States are essentially $\forall$-quantified -- all satisfiable + children may be removed + \end{itemize} +\end{frame} + + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "../vortrag" +%%% TeX-engine: luatex +%%% TeX-PDF-mode: t +%%% End: diff --git a/vortrag.tex b/vortrag.tex index 3b07c62..24bf9b2 100644 --- a/vortrag.tex +++ b/vortrag.tex @@ -89,7 +89,7 @@ \end{tabular} \\ \vspace{0.6cm} - 2016~\textendash~01~\textendash~19 + 2016~\textendash~04~\textendash~26 } \titlepage \end{frame} @@ -106,16 +106,6 @@ \tableofcontents{} \end{frame} -\begin{frame}{Where we left} - \begin{itemize} - \item actually implementing deferral tracking - \item deciding when some deferral can be considered ``finished'' - \item \dots - \item finding ``right'' heuristic for when to try and close the tableaux - \item fixing all the bugs - \end{itemize} -\end{frame} - \input{chapters/finishingcool} \input{chapters/early} \input{chapters/optimizations} @@ -130,8 +120,8 @@ \end{center} \vspace*{\fill} - Download: https://static.siccegge.de/talks/cool-FAU-2016-01-19.pdf\\ - https://git.siccegge.de/?p=talk/coalgebraic-mu-calculus-cool.git + Download: https://static.siccegge.de/talks/cool-FAU-2016-04-26.pdf\\ + https://git.siccegge.de/?p=talk/coalgebraic-mu-calculus-cool-2.git \end{frame} \end{document}