%!TeX root = main.tex
%
In this paper, we study the finite satisfiability problem for the "logic $\BE*$" 
under the homogeneity assumption. $\BE$ is the cornerstone of Halpern and Shoham's 
interval temporal logic, and features modal operators corresponding to the prefix
(a.k.a.~``Begins'') and suffix (a.k.a.~``Ends'') relations on intervals. 
In terms of complexity, $\BE$ lies in between the "``Chop'' logic $\C*$", 
whose satisfiability problem is known to be non-elementary, and the 
$\pspace$-complete interval "logic $\D*$" of the sub-interval (a.k.a.~``During'') 
relation. $\BE$ was shown to be $\expspace$-hard, and the only known
satisfiability procedure is primitive recursive, but not elementary.
Our contribution consists of tightening the complexity bounds of the satisfiability 
problem for $\BE$, by proving it to be $\expspace$-complete. 
We do so by devising an equi-satisfiable normal form with boundedly many nested modalities. 
The normalization technique resembles Scott's quantifier elimination, but it turns 
out to be much more involved due to the limitations enforced by the homogeneity assumption. 


\begin{comment}
%PLAIN TEXT
%
In this paper we study the finite satisfiability problem for the logic BE under the homogeneity assumption. BE is the cornerstone of Halpern and Shoham's interval temporal logic, and features modal operators corresponding to the prefix (a.k.a. "Begins") and suffix (a.k.a. "Ends") relations on intervals. In terms of complexity, BE lies in between the "Chop" logic C, whose satisfiability problem is known to be non-elementary, and the PSPACE-complete interval logic D, based on the sub-interval (a.k.a. "During") relation. BE was shown to be EXPSPACE-hard, and the only known satisfiability procedure is primitive recursive, but not elementary. Our contribution consists of tightening the complexity bounds of the satisfiability problem for BE, by proving it to be EXPSPACE-complete. We do so by devising an equi-satisfiable normal form with boundedly many nested modalities. The normalization technique resembles Scott's quantifier elimination, but it turns out to be much more involved due to the limitations enforced by the homogeneity assumption. 
\end{comment}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End:
