Commit 209dfbb6 authored by Mihaela SIGHIREANU's avatar Mihaela SIGHIREANU
Browse files

sketch of coNP for entail

parent d604fec2
%!TEX root = cade-28.tex
\section{Complexity of the entailment problem}
Theorem~\ref{thm-entail} states that the upper bound of the entailment problem is \textsc{EXPTIME}.
The lower bound is given by the complexity of the entailment problem for quantifier free formulas in \textsc{ASL}, which is shown to be \textsc{coNP} in~\cite{BrotherstonGK17}.
\textbf{Claim:} The entailment problem in \slah\ is in \textbf{coNP}.
\begin{proof}
Let fix $\varphi \models \psi$ an entailment problem in \slah.
We build in polynomial time a \PbA\ formula $\chi$ from $\varphi$ and $\psi$
such that
for any stack $s$, $s\models \chi$
iff $\exists h.~s,h\models \varphi$ and $s,h \not\models \psi$.
We suppose that both formula $\varphi$ and $\psi$ have been transformed in normal form as follows:
\begin{itemize}
\item atoms $\hls{}(x,y;v')$ with $\abs(\varphi)\models (v'<2 \lor x=y)$ have been removed and replaced by $x=y$\mihaela{use $\xi$ ?}
\item atoms $\hls{}(x,y;v')$ with $\abs(\varphi)\models v'=2$ have been replaced by $y-x=2 : x\pto 2 \star \blk(x+1,y)$
\item ...\mihaela{TODO}
\end{itemize}
The normalization can be done in a linear number of calls to the \EPbA\ procedure.
The formula $\chi$ shall ensure that $\varphi$ is satisfiable, so
it contains as conjunct $\abs(\varphi)$.
The entailment may be invalid iff one of the following holds:
\begin{itemize}
\item $\psi$ is not satisfiable, i.e., $\abs(\psi)$ is not satisfiable.
\item there exists an address inside a spatial atom of $\varphi$
which is not inside a spatial atom of $\psi$;
we denote this formula by $cov(\varphi,\psi)$;
\item similarly, $cov(\psi,\varphi)$ (the semantics is non intuitionistic),
\item a points-to or a heap-list atom of $\psi$ ``covers'' a domain of addresses
which is inside the one of a block atom of $\varphi$;
we denote this formula by $nblk(\varphi,\psi)$;
\item a points-to atom of $\psi$ defines an address inside (strictly)
a heap-list atom of $\varphi$;
we denote this formula by $npto(\varphi,\psi)$;
\item a points-to atom $x\pto v$ of $\psi$ defines the same address as the start address
of a heap-list atom $\hls{}(x,y;v')$ in $\varphi$;
we denote this formula by $npto'(\varphi,\psi)$;
(this is true because we are in the normal form);
\item a points-to atoms $x\pto v$ of $\psi$ defines the same address as a
points-to atom $x\pto v'$ of $\varphi$ but $v\neq v'$;
\item a heap-list atom $\hls{}(x,y;v')$ of $\psi$ starts at an address at which is defined a points-to atom $x\pto v$ of $\varphi$ such that $v> v'$;
\item a heap-list atom $\hls{}(x,y;v')$ of $\psi$ ``covers'' the domain of
addresses if an atom $\hls{}(z,w;v)$ of $\varphi$ but $v' < v$;
\item a heap-list atom $\hls{}(x,y;v')$ of $\psi$ ``covers'' a domain of addresses
that can not be filded into a $\hls{}$ atom with chunks of maximal size less or equal to $v'$\mihaela{difficult in P!}
\end{itemize}
\end{proof}
......@@ -88,6 +88,7 @@ Zhilin Wu\inst{2} \orcidID{0000-0003-0899-628X}
\appendix
%\section{Appendixes}
\input{app-sat-hls.tex}
\input{app-ent-hls.tex}
%% temporary
%\newpage
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment