\section{Introduction}
The recent Large Hadron Collider (LHC) discovery of a scalar particle with 125 GeV  which is compatible with Standard Model (SM) Higgs boson predicted by Brout-Englert-Higgs symmetry breaking mechanism opens up a gateway to search for physics beyond the SM \cite{Aad:2012tfa, Chatrchyan:2012xdj}. But, an evidence for new physics beyond the SM using analysis of combined  ATLAS and CMS data for probing the couplings of Higgs boson has not been observed yet.
 Possible deviation from the SM predictions of Higgs boson couplings would imply the presence of new physics involving massive particles that are decoupled at energy scales much larger than the Higgs sector energies being probed \cite{Appelquist:1974tg}.  The SM Effective Field Theory (EFT) is a well-known model independent method for investigation of any deviation from SM \cite{Buchmuller:1985jz,Grzadkowski:2010es}. The origin of this method is based on all new physics contributions to the SM described by a systematic expansion in a series of high dimensional operators beyond the SM fields. All high dimensional operators conform to $SU(3)_C\times SU(2)_L\times U(1)_Y$ SM gauge symmetry. The dimension-6 operators play an important role in the framework since they match to ultraviolet (UV) models which are simplified by the universal one-loop effective action. There have been many analyses for constraints on SM EFT operators with available data from LHC-Run 1 \cite{Corbett:2012ja,Ellis:2014jta,Ellis:2014dva, Falkowski:2015fla,Corbett:2015ksa,Ferreira:2016jea,Aad:2015tna,Green:2016trm} and with electroweak precision measurements provided from previous accelerator, namely Large Electron Positron (LEP) \cite{Jones:1979bq,Grinstein:1991cd,Hagiwara:1993qt, Han:2004az}. Especially, the prediction on dimension-6 operators have been examined in many rewarding studies at High Luminosity LHC (HL-LHC) \cite{Englert:2015hrx,Buckley:2015lku, Khanpour:2017inb} and future $e^+e^-$ colliders \cite{Amar:2014fpa,Kumar:2015eea,Ellis:2015sca,Ge:2016zro,Cohen:2016bsd,Ellis:2017kfi,Alam:2017hkf,Khanpour:2017cfq,Englert:2017gdy}.

The precision measurements of Higgs boson couplings with the other SM particles at the LHC and planned future colliders will give us detailed information about its true nature. The future multi-TeV $e^+e^-$ colliders with extremely high luminosity and clean environment due to the absence of hadronic initial state, would give access to precise measurement, especially for the Higgs couplings. The  Compact Linear Collider (CLIC) is one the mature proposed linear colliders with centre of mass energies from a few hundred GeV up to 3 TeV \cite{CLIC:2016zwp}. The first energy stage of CLIC operation was chosen to be $\sqrt s$=380 GeV, with the predicted integrated luminosity of 500 $fb^{-1}. $ The primary motivation of  this stage is the precision measurements of SM Higgs properties and also the model independent Higgs couplings to both fermions and bosons \cite{CLIC:2016zwp, Abramowicz:2016zbo}.

In this study, we focus on the analysis of $e^+e^-\to \nu \bar{\nu} H$ production process in order to assess the projection of the first energy stage of the CLIC on the CP-conserving dimension-6 operators involving the Higgs and gauge bosons ($W^{\pm}$, $\gamma$, $Z$) defined by an SM EFT Lagrangian in the next section.

\section{Effective Operators}
The well known SM Lagrangian ( $\mathcal{L}_{\rm SM}$ ) involving renormalizable interactions is suppressed by higher dimensional operators in SM EFT approach. All these operators parametrised by an energy scale of non-observed states assumed larger than vacuum expectation value of Higgs field ($v$). A few different operator bases are presented in the literature, we consider SM EFT operators as the strongly interacting light Higgs Lagrangian ($\mathcal{L}_{\rm SILH}$) in bar convention \cite{Englert:2015hrx,Contino:2013kra,Alloul:2013naa}.  Assuming the baryon and lepton number conservation, the most general form of dimension-6 effective Lagrangian including Higgs boson couplings that keep SM gauge symmetry is given as follows;
\begin{eqnarray}
\mathcal{L} = \mathcal{L}_{\rm SM} + \sum_{i}\bar c_{i}O_{i}
\end{eqnarray}
where  $\bar c_{i}$ are normalized Wilson coefficients that are free parameters. In this work, we consider the dimension-6 CP-conserving interactions of the Higgs boson and electroweak gauge boson in SILH basis as \cite{Alloul:2013naa}:
\begin{eqnarray}\label{massb}
	\begin{split}
		\mathcal{L}_{\rm SILH} = & \
		 \frac{\bar c_{H}}{2 v^2} \partial^\mu\big[\Phi^\dag \Phi\big] \partial_\mu \big[ \Phi^\dagger \Phi \big]
		+ \frac{\bar c_{T}}{2 v^2} \big[ \Phi^\dag {\overleftrightarrow{D}}^\mu \Phi \big] \big[ \Phi^\dag {\overleftrightarrow{D}}_\mu \Phi \big] - \frac{\bar c_{6} \lambda}{v^2} \big[\Phi^\dag \Phi \big]^3
		\\
		& \
		  - \bigg[\frac{\bar c_{u}}{v^2} y_u \Phi^\dag \Phi\ \Phi^\dag\cdot{\bar Q}_L u_R
		  + \frac{\bar c_{d}}{v^2} y_d \Phi^\dag \Phi\ \Phi {\bar Q}_L d_R
		+\frac{\bar c_{l}}{v^2} y_l \Phi^\dag \Phi\ \Phi {\bar L}_L e_R
		 + {\rm h.c.} \bigg]
		\\
		&\
		 + \frac{i g\ \bar  c_{W}}{m_{W}^2} \big[ \Phi^\dag T_{2k} \overleftrightarrow{D}^\mu \Phi \big]  D^\nu  W_{\mu \nu}^k + \frac{i g'\ \bar c_{B}}{2 m_{W}^2} \big[\Phi^\dag \overleftrightarrow{D}^\mu \Phi \big] \partial^\nu  B_{\mu \nu} \\
		&\
		+ \frac{2 i g\ \bar c_{HW}}{m_{W}^2} \big[D^\mu \Phi^\dag T_{2k} D^\nu \Phi\big] W_{\mu \nu}^k
		+ \frac{i g'\ \bar c_{HB}}{m_{W}^2}  \big[D^\mu \Phi^\dag D^\nu \Phi\big] B_{\mu \nu}   \\
		&\
		 +\frac{g'^2\ \bar c_{\gamma}}{m_{W}^2} \Phi^\dag \Phi B_{\mu\nu} B^{\mu\nu}
		+\frac{g_s^2\ \bar c_{g}}{m_{W}^2} \Phi^\dag \Phi G_{\mu\nu}^a G_a^{\mu\nu}
	\end{split}
\end{eqnarray}
where $\lambda$ represents the Higgs quartic coupling; $y_u$, $y_d$ and $y_l$ are the $3\times3$ Yukawa coupling matrices in flavor space; $g'$, $g$ and $g_s$ denotes coupling constant of  $U(1)_Y$, $SU(2)_L$ and $SU(3)_C$ gauge fields, respectively; the generators of $SU(2)_L$ in the fundamental representation are given by $T_{2k}=\sigma_k/2$, $\sigma_k$ being the Pauli matrices; $\Phi$ is Higgs field contains a single $SU(2)_L$ doublet of fields; $B^{\mu\nu}=\partial_\mu B_\nu-\partial_\nu B_\mu$  and $W^{\mu \nu}=\partial_\mu W_\nu^k-\partial_\nu W_\mu^k+g\epsilon_{ijk}W_\mu^iW_\nu^j$ are the electroweak field strength tensors and $G^{\mu\nu}$ is the strong field strength tensors; and the Hermitian derivative operators  defined as,
$\Phi^\dag \overleftrightarrow{D}_\mu \Phi = \Phi^\dag D^{\mu}\Phi - D_{\mu}\Phi^{\dag}\Phi$.
The SM EFT Lagrangian (Eq.(\ref{massb})) containing the Wilson coefficients in the SILH bases of dimension-6 CP-conserving operators can be defined in terms of the mass eigenstates after electroweak symmetry breaking (Higgs boson, W, Z, photon, etc.) as follows
\begin{eqnarray}\label{gbase}
	\mathcal{L} &=& - \frac{m_{ H}^2}{2 v} g^{(1)}_{ hhh}h^3 + \frac{1}{2} g^{(2)}_{ hhh} h\partial_\mu h \partial^\mu h
    - \frac{1}{4} g_{ hgg} G^a_{\mu\nu} G_a^{\mu\nu} h
    - \frac{1}{4} g_{ h\gamma\gamma} F_{\mu\nu} F^{\mu\nu} h\nonumber\\
   & -& \frac{1}{4} g_{ hzz}^{(1)} Z_{\mu\nu} Z^{\mu\nu} h
    - g_{ hzz}^{(2)} Z_\nu \partial_\mu Z^{\mu\nu} h
    + \frac{1}{2} g_{ hzz}^{(3)} Z_\mu Z^\mu h
    - \frac{1}{2} g_{ haz}^{(1)} Z_{\mu\nu} F^{\mu\nu} h
    - g_{ haz}^{(2)} Z_\nu \partial_\mu F^{\mu\nu} h\nonumber\\
    &-& \frac{1}{2} g_{ hww}^{(1)} {W^+}^{\mu\nu} {W^-}_{\mu\nu} h
    - \Big[g_{ hww}^{(2)} {W^+}^\nu \partial^\mu {W^-}_{\mu\nu} h + {\rm h.c.} \Big]
    +g (1-\frac12 \bar c_{ H}) m_{\sss W} {W^-}_\mu  {W+}^\mu h\nonumber\\
& -&\bigg[
      \tilde y_u \frac{1}{\sqrt{2}} \big[{\bar u} P_R u\big] h +
      \tilde y_d \frac{1}{\sqrt{2}} \big[{\bar d} P_R d\big] h +
      \tilde y_\ell \frac{1}{\sqrt{2}} \big[{\bar \ell} P_R \ell\big] h
     + {\rm h.c.} \bigg] \ ,
\end{eqnarray}

where $W_{\mu\nu}$, $Z_{\mu\nu}$ and $F_{\mu\nu}$ are the field strength tensors of $W$-boson, $Z$-boson and photon, respectively; $m_H$ represent the mass of the Higgs boson;  the effective couplings in gauge basis defined as dimension-6 operators are given in Table~\ref{mtable} in which $a_{H}$ ($g_H$) coupling is the SM contribution to the Higgs boson to two photons (gluons) vertex at loop level.
\begin{table}[h]
\caption{The relations between Lagrangian  parameters in the mass basis (Eq.\ref{massb}) and the Lagrangian in gauge  basis (Eq.\ref{gbase}). ($c_W\equiv\cos \theta_W$, $s_W\equiv\sin \theta_W$)}

\begin{ruledtabular}\label{mtable}
\begin{tabular}{ll}
    $g_{hhh}^{(1)}$= $1 + \frac78 \bar c_{ 6} - \frac12 \bar c_{H}$&$g_{hhh}^{(2)}$= $\frac{g}{m_{\sss W}} \bar c_{H}$\\
    $g_{hgg}$= $g_{ H}- \frac{4 \bar c_{g} g_s^2 v}{m_{\sss W}^2}$ &$g_{h\gamma\gamma}$= $a_{ H} - \frac{8 g \bar c_{ \gamma} s_{\sss W}^2}{m_{\sss W}}$ \\
    $g^{(1)}_{ hzz}$= $\frac{2 g}{c_{\sss W}^2 m_{\sss W}} \Big[ \bar c_{HB} s_{\sss W}^2 - 4 \bar c_{ \gamma} s_{\sss W}^4 + c_{\sss W}^2 \bar c_{ HW}\Big]$& $g^{(2)}_{ hzz}$= $\frac{g}{c_{\sss W}^2 m_{\sss W}} \Big[(\bar c_{ HW} +\bar c_{ W}) c_{\sss W}^2  + (\bar c_{ B} + \bar c_{ HB}) s_{\sss W}^2 \Big]$ \\
    $g^{(3)}_{hzz}$=  $\frac{g m_{\sss W}}{c_{\sss W}^2} \Big[ 1 -\frac12 \bar c_{H} - 2 \bar c_{T} +8 \bar c_{\gamma} \frac{s_{\sss W}^4}{c_{\sss W}^2}  \Big]$&  $g^{(1)}_{ haz}$= $\frac{g s_{\sss W}}{c_{\sss W} m_{\sss W}} \Big[  \bar c_{ HW} - \bar c_{HB} + 8 \bar c_{ \gamma} s_{\sss W}^2\Big]$ \\
    $g^{(2)}_{haz}$= $\frac{g s_{\sss W}}{c_{\sss W} m_{\sss W}} \Big[  \bar c_{ HW} - \bar c_{ HB} - \bar c_{ B} + \bar c_{ W}\Big]$& $\tilde y_d$= $y_d \Big[1  -\frac12 \bar c_{ H} + \frac32 \bar c_{ d}\Big]$   \\
       $g^{(1)}_{ hww}$= $\frac{2 g}{m_{\sss W}} \bar c_{ HW}$ &   $\tilde y_u$= $y_u \Big[1 -\frac12 \bar c_{ H} + \frac32 \bar c_{ u}\Big]$ \\
$g^{(2)}_{ hww}$= $\frac{g}{m_{\sss W}} \Big[ \bar c_{ W} + \bar c_{ HW} \Big]$ & $\tilde y_\ell$= $y_\ell \Big[1  -\frac12 \bar c_{ H} + \frac32 \bar c_{ \ell}\Big]$ \\
  \end{tabular}
\end{ruledtabular}
\end{table}
 \begin{figure}
\includegraphics{fd2.pdf}
\caption{The Feynman diagrams for the process $e^+e^-\to \nu \bar{\nu} H$. \label{fd}}
\end{figure}
\begin{figure}
\includegraphics{cs_380.pdf}
\caption{ The total cross section as a function of CP-conserving $\bar{c}_W$=-$\bar{c}_B$, $\bar{c}_{HW}$, $\bar{c}_{HB}$ and $\bar{c}_{\gamma}$ couplings for $e^+e^-\to \nu \bar{\nu} H$ process at the CLIC with $\sqrt s$=380 GeV. \label{fig1}}
\end{figure}

We use the parametrization in Ref. \cite{Alloul:2013naa}  based on the formulation given in Ref. \cite{Contino:2013kra} in our analysis. The parametrization is not complete as described in detail in section 3 of Ref. \cite{Alonso:2013hga} and also Ref.\cite{Brivio:2017bnu}. It chooses to remove two fermionic invariants while retaining all the bosonic operators. This choice assumes completely unbroken $U(3)$ flavor symmetry of the UV theory where the coefficient of these operators are unit matrices in flavor space. Therefore, we assume flavor diagonal dimension-six  effects. It is sufficient for the purpose of this paper in which we do not consider higher order electroweak effects but only claim a sensitivity study for $\bar c_{ W}$,  $\bar c_{ B}$, $\bar c_{ HW}$, $\bar c_{ HB}$ and $\bar c_{\gamma}$ couplings.

We have used the Monte Carlo simulations with leading order in \verb|MadGraph5_aMC@NLO| \cite{Alwall:2014hca} involving effect of the dimension-6 operators on $H \nu \bar{\nu} $ production mechanism in $e^+e^-$ collisions. The effective Lagrangian of the SM EFT in Eq.(\ref{massb})  is implemented into the \verb|MadGraph5_aMC@NLO| based on FeynRules \cite{Alloul:2013bka} and UFO \cite{Degrande:2011ua} framework.
 In this study, we focus on searching for the dimension-6 Higgs-gauge boson couplings via $e^+e^-\to\nu \bar{\nu} H$ process as shown in Fig.\ref{fd}.
This process is sensitive to Higgs-gauge boson couplings; $g_{hzz}$, $g_{hww}$, $g_{hz\gamma}$,  and the couplings of a quark or lepton pair and one single Higgs field; $\tilde y_u$, $\tilde y_d$, $\tilde y_l$ in the mass basis.  In the gauge basis, $e^+e^-\to\nu \bar{\nu} H$ process is sensitive to the seven Wilson coefficients:  $\bar c_{ W}$,  $\bar c_{ B}$, $\bar c_{ HW}$, $\bar c_{ HB}$,  $\bar c_{H}$, $\bar c_{ \gamma}$ and  $\bar c_{T}$ related to Higgs-gauge boson couplings and also effective fermionic couplings. Due to the small Yukawa couplings of the first and second generation fermions, we neglect the effective fermionic couplings. We set $\bar c_{ W} + \bar c_{ B}$  and  $\bar c_{T}$ to zero in all our calculations since the linear combination of  $\bar c_{ W} + \bar c_{ B}$  and  $\bar c_{T}$ strongly constrained from the electroweak precision test of the oblique parameters $S$ and $T$.  The cross sections of $e^+e^-\to\nu \bar{\nu} H$ process as a function of $\bar c_{ W}$,  $\bar c_{ B}$, $\bar c_{ HW}$, $\bar c_{ HB}$ and $\bar c_{\gamma}$ couplings are shown in Fig.\ref{fig1}. There have been many studies in the literature considering individual, subsets or simultaneous change of dimension-6 operators \cite{Ellis:2015sca, Ellis:2017kfi}. Here we vary individually dimension- 6 operators and calculate the contributions to the corrections from new physics in the analysis. We presume that only one of the effective couplings is non-zero at any given time, while the other couplings are fixed to zero. One can easily see the deviation from SM for this couplings even in a small value region for $e^+e^-\to\nu \bar{\nu} H$ process. Therefore, we will only consider these five among the Higgs-gauge boson effective couplings in the detailed analysis including detector simulations through the process $e^+e^-\to\nu \bar{\nu} H$ at CLIC with 380 GeV center of mass energy in the next section.

 \section{Signal and Background Analysis}
 We perform the detailed analysis of $\bar c_{ W}$,  $\bar c_{ B}$, $\bar c_{ HW}$, $\bar c_{ HB}$ and $\bar c_{\gamma}$ effective couplings via $e^+e^-\to\nu \bar{\nu} H$ process as well as other relevant background at the first energy stage of CLIC. The  $e^+e^-\to\nu \bar{\nu} H$ signal process includes both s-channel $e^+e^-\to Z^*/\gamma^* \to ZH \to \nu \bar{\nu} H$ process (Higgsstrahlung) and t-channel $e^+e^-\to \nu\bar{\nu} W^*/W^*\to \nu \bar{\nu} H$ process (WW-fusion) as shown in Fig.\ref{fd}. In the initial energy stage of CLIC at $\sqrt s$=380 GeV, these two process have approximately the same amount contribution to the production cross section of the $e^+e^-\to\nu \bar{\nu} H$ process. In our analysis, we include effective dimension-6 couplings and SM contribution as well as interference between effective couplings and SM contributions ($S+B_H$) that lead to $e^+e^-\to\nu \bar{\nu} H$ process where Higgs decay to pair of $b$-quark. We consider the following relevant backgrounds; $B_H$: $e^+e^-\to\nu \bar{\nu} H$ process which has the same final state of the considered signal process including only SM contribution where the Higgs decays to pair of $b$-quark; $B_{ZZ}$: $e^+e^-\to Z Z$ process where one $Z$ decays to $b\bar b$ and the other decays to $\nu\bar \nu$; $B_{tt}$: $e^+e^-\to t \bar t$ process where two b quarks are from $t (\bar t)$ decaying to $W^+b (W^{-} \bar b)$ in which $W^{\pm}$ decay leptonically;  $B_{Z\nu\nu}$: $e^+e^-\to\nu \bar{\nu} Z$ process in which  $Z$ decays to $b\bar b$. The generated signal and all backgrounds at parton level in \verb|MadGraph5_aMC@NLO| are passed through the Pythia 6 \cite{Sjostrand:2006za} for parton shower and hadronization. The detector responses are taken into account with ILD detector card \cite{Behnke:2013lya} in \verb|Delphes 3.3.3| \cite{deFavereau:2013fsa} package. Then, all events are analysed by using the ExRootAnalysis utility \cite{exroot} with ROOT \cite{Brun:1997pa}.

Requiring missing energy transverse (${\not}E_T$), no charged leptons and at least 2 jets with their transverse momenta ($p_T^j$) greater than 20 GeV and pseudo-rapidity ($\eta^j$) between -2.5 and 2.5 are the pre-selection of the event to be further analysed. The energy resolution of jets for $|\eta^j|\leqslant 3$ is assumed to be
\begin{eqnarray}
\frac{\Delta E_{jets}}{E_{jets}}=1.5\%+\frac{50\%}{\sqrt{E_{jets}(GeV)}}
\end{eqnarray}
The momentum resolution for jets as a function of $p_T^j$ and $\eta^j$  is
\begin{eqnarray}
\frac{\Delta p_T^{j}}{p_T^{j}}=(1.0+0.01\times p_T^{j})\times 10^{-3}~~ \textrm{for}~~|\eta^j|\leqslant 1\\
\frac{\Delta p_T^{j}}{p_T^{j}}=(1.0+0.01\times p_T^{j})\times 10^{-2} ~~\textrm{for} ~~~1<|\eta^j|\leqslant 2.4
\end{eqnarray}
Jets are clustered with the anti-$k_t$ algorithm \cite{Cacciari:2008gp} using FastJet \cite{Cacciari:2011ma} where a cone radius is used as $R = 0.5$. In order to select the signal and background events, the following kinematic cuts and requirements are applied;
\textbf{i)} requiring at least two jets tagged as the b-jet which significantly suppress the light-quark jet backgrounds. These two b-jets are used to reconstruct Higgs boson-mass. \textbf{ii)} One of the b-tagged jets with the highest $p_T$ is defined as $b1$ while the other is $b2$ with lower $p_T$. Fig.~\ref{fig2} shows $p_T$  distributions of $b1$ and $b2$ of signal (for $\bar{c}_{HW}$=0.05) and all relevant background processes versus reconstructed Higgs boson-mass from $b1$ and $b2$ ($M_{b,\bar b}$). As it can be seen in Fig.~\ref{fig2}, the $b_1$ with $p_T^{b1}>50$ GeV, $b_2$ with $p_T^{b2}>$30 GeV and pseudo-rapidity of the b-tagged jets to be $|\eta^{b1,b2}|\leqslant 2.0$ are considered to reduce $B_{ZZ}$ and $B_{Z\nu\nu}$. In ILD detector card, both b-tagging efficiency and misidentification rates are given as function of jet transverse momentum. For the transverse momentum of leading jet ($b1$) ranging from 50 GeV to 180 GeV, b-tagging efficiency is between 64\% and 72 \%, c-jet misidentification rate is 17\%-20\%, and misidentification rate of light jet 1.2\%-1.76\%.
The missing transverse energy (${\not}E_T$) and scalar transverse energy sum ($H_T$)  for signal (for $\bar{c}_{HW}$=0.05) and all relevant background processes versus $M_{b,\bar b}$ are shown in Fig.~\ref{fig3}. \textbf{iii)} The missing transverse energy is required to be ${\not}E_T>30$ GeV to suppress the backgrounds  at low missing energy region. \textbf{iv)} Especially, to reduce $tt$ background process, the scalar transverse energy sum ($H_T$) is required to be 100 GeV $<H_T<$ 200 GeV.
Normalized distributions of reconstructed invariant mass of Higgs-boson from $b\bar b$ for signal with $\bar{c}_{HW} $=0.05, $\bar{c}_{HB} $=0.05, $\bar{c}_{\gamma} $=0.05, $\bar{c}_{W}=- \bar{c}_{B}$=0.05  and relevant backgrounds processes are given in Fig.\ref{fig4}.\textbf{ v)} Finally, the reconstructed invariant mass of Higgs-boson from two b-jet is selected to be in the range 92 GeV $< M_{inv}^{rec}(b1,b2)< 136$ GeV. The kinematic distributions for each processes are normalized to the number of expected events which is defined to be the cross section of each processes times integrated luminosity with $L_{int}$=500 fb$^{-1}$.

Effects of the cuts used in the analysis can be seen from the Table~\ref{tab2} which shows number of events after each cut. Requiring two b-tagged jets reduces the  $B_{ZZ}$, $B_{tt}$ and $B_{Z\nu\nu}$ backgrounds more than signal $S+B_H$ and background with same final state, $B_H$. Cut-2 effects on both signal and all relevant backgrounds, especially $B_{ZZ}$ and $B_{Z\nu\nu}$. ${\not}E_T$ cut decreases both $B_{tt}$ and $B_{ZZ}$ backgrounds while $H_T$ cut significantly suppresses $B_{tt}$ background. Final effect of the all cuts is approximately 15\%  for signal $S+B_H$ and $B_H$ background while 0.3\%-0.8\% for other relevant backgrounds.
 \begin{table}
\caption{Number of signal and background events after applied kinematic cuts used for the analysis for $\bar{c}_{HW}$=0.05 with $L_{int}=500$ fb$^{-1}$  \label{tab2}}
\begin{ruledtabular}
\begin{tabular}{clcccccc}
Cuts & Definitions&$S+B_H$&$B_H$&$B_{ZZ}$&$B_{tt}$&$B_{Z\nu\nu}$ \\ \hline
Cut-0 &  $N_j \geqslant 2$, lepton vetos, MET>0 with pre-selection cuts & 30432.5&19383.2&207847&211384&94405.6 \\
Cut-1 & two jets with $b$-tagging&8003.41&5035.96&10047.4&25636.2&6995.5  \\
Cut-2 & $p_{T}^{b1} > 50$ GeV, $p_{T}^{b2} > 30$ GeV and  $| \eta^{b1,\,b2}|\leqslant 2.0$&5862.8&3421.5&6662.6&24766.9&3205.9\\
Cut-3 & ${\not}E_T>30$ GeV&5548.4&3109.1&2705.4&8686.6 &3122.5 \\
Cut-4 & 100 GeV $<H_T<$ 200 GeV  &5407.9&3017.9&2158.1&1927.1&2823.3  \\
Cut-5 &100 GeV $< M_{inv}^{rec}(b1,b2)< 136$ GeV& 4211.6&2433.7&17.9&824.8&20.9 \\
\end{tabular}
\end{ruledtabular}
\end{table}

\begin{figure}
\includegraphics[scale=0.16]{2D_ptb1_SB_chw005.pdf}
\includegraphics[scale=0.16]{2D_ptb1_BH.pdf}
\includegraphics[scale=0.16]{2D_ptb1_BZZ.pdf}
\includegraphics[scale=0.16]{2D_ptb1_Btt.pdf}
\includegraphics[scale=0.16]{2D_ptb1_BZvv.pdf}\\
\includegraphics[scale=0.16]{2D_ptb2_SB_chw005.pdf}
\includegraphics[scale=0.16]{2D_ptb2_BH.pdf}
\includegraphics[scale=0.16]{2D_ptb2_BZZ.pdf}
\includegraphics[scale=0.16]{2D_ptb2_Btt.pdf}
\includegraphics[scale=0.16]{2D_ptb2_BZvv.pdf}
\caption{ Normalized distributions of transverse momentum of tagged b-jets; $b1$  (first row) and $b2$ (second row) versus reconstructed Higgs boson-mass from $b1$ and $b2$ ($M_{b,\bar b}$) for signal with $\bar{c}_{HW} $=0.05 and relevant background processes.  \label{fig2}}
\end{figure}

\begin{figure}
\includegraphics[scale=0.16]{2D_met_SB_chw005.pdf}
\includegraphics[scale=0.16]{2D_met_BH.pdf}
\includegraphics[scale=0.16]{2D_met_BZZ.pdf}
\includegraphics[scale=0.16]{2D_met_Btt.pdf}
\includegraphics[scale=0.16]{2D_met_BZvv.pdf}\\
\includegraphics[scale=0.16]{2D_HT_SB_chw005.pdf}
\includegraphics[scale=0.16]{2D_HT_BH}
\includegraphics[scale=0.16]{2D_HT_BZZ.pdf}
\includegraphics[scale=0.16]{2D_HT_Btt.pdf}
\includegraphics[scale=0.16]{2D_HT_BZvv.pdf}
\caption{  Normalized distributions of missing transverse energy (first row) and scalar transverse energy sum (second row) for signal versus reconstructed Higgs boson-mass from $b1$ and $b2$ ($M_{b,\bar b}$) with $\bar{c}_{HW} $=0.05 and relevant backgrounds processes. \label{fig3}}
\end{figure}

\begin{figure}
\includegraphics[scale=0.4]{ratio_clic_005_htcut_chw.pdf}
\includegraphics[scale=0.4]{ratio_clic_chb005_htcut.pdf}\\
\includegraphics[scale=0.4]{ratio_clic_ca005_htcut.pdf}
\includegraphics[scale=0.4]{ratio_clic_005_htcut_cw.pdf}
\caption{ Normalized distributions of reconstructed invariant mass of Higgs-boson from $b\bar b$ for signal with $\bar{c}_{HW} $=0.05, $\bar{c}_{HB} $=0.05, $\bar{c}_{\gamma} $=0.05, $\bar{c}_{W}=- \bar{c}_{B}$=0.05   and relevant backgrounds processes. \label{fig4}}
\end{figure}
\section{sensitivity of  Higgs-gauge boson couplings}
We calculate the sensitivity of the dimension-6 Higgs-gauge boson couplings in $e^+e^-\to \nu \nu H$ process  by
applying $\chi^{2}$ criterion with and without a
systematic error. The $\chi^{2}$ function is defined as follows
\begin{eqnarray}
\chi^{2} (\bar{c_i})=\sum_i^{n_{bins}}\left(\frac{N_{i}^{NP}(\bar{c_i})-N_{i}^{B}}{N_{i}^{B}\Delta_i}\right)^{2}
\end{eqnarray}
where $N_i^{NP}$ is the total number of events in the existence of effective couplings ($S$) and total backgrounds ($B_H$, $B_{ZZ}$, $B_{tt}$ and $B_{Z\nu\nu}$), $N_i^B$ is number of events of total backgrounds in $i$th bin of the invariant mass distributions of reconstructed Higgs boson, $\Delta_i=\sqrt{\delta_{sys}^2+\frac{1}{N_i^B}}$ is the combined systematic ($\delta_{sys}$) and statistical errors in each bin. So, the numerator in Eq.(7) equals to the number of extra events due to the presence of new operators.
In this analysis, we focused on $\bar{c}_{HB} $, $\bar{c}_{W}=- \bar{c}_{B}$ and $\bar{c}_{HW}$ couplings which are the
main coefficients contributing to $e^+e^-\to\nu \bar{\nu} H$ signal process. The 95\% Confidence Level (C.L.) limits including only statistical error on dimension-6 Higgs-gauge boson couplings at $\sqrt s$=380 GeV and $L_{int}$=500 fb$^{-1}$ (CLIC-380) are compared with the LHC at 14 TeV center of mass energies for the integrated luminosity of 300 fb$^{-1}$ (LHC-300) and 3000 fb$^{-1}$ (LHC-3000) \cite{Englert:2015hrx} in Fig.~\ref{fig5}. We see that CLIC-380 results would be significantly more sensitive to $\bar{c}_{HW}$ and somewhat sensitive to $\bar{c}_{W}=- \bar{c}_{B}$ whereas sensitivity to $\bar{c}_{HB} $ is comparable with expected LHC results. The prediction on the limits for the future lepton colliders; ILC \cite{Khanpour:2017cfq,Ellis:2015sca} of an integrated luminosity $L_{int}=$300 fb$^{-1}$ at the center of mass energy $\sqrt s=$ 500 GeV, FCC-ee \cite{Ellis:2015sca} for $L_{int}$=10 $ab^{-1}$ at $\sqrt s=$ 240 GeV, CEPC \cite{Ge:2016tmm} for $L_{int}$=5 $ab^{-1}$ at $\sqrt s=$ 240 GeV  are also shown in Fig.~\ref{fig5} .  In order to include the systematical uncertainties  we recompute the bounds. For example including a 10\% conservative systematic uncertainty, the constraint on $\bar{c}_{HW}$ is $[-0.07959; 0.02423]$. This bound is four times lower than the obtained limits without systematic uncertainties.

\begin{figure}
\includegraphics[scale=0.8]{limit_lv_rv.pdf}
\caption{ Obtained allowed range (CLIC-380), LHC at 14 TeV center of mass energies for the integrated luminosity of 300 fb$^{-1}$ (LHC-300) and 3000 fb$^{-1}$ (LHC-3000) \cite{Englert:2015hrx}, ILC-300 at $\sqrt s=$ 500 GeV with $L_{int}=$300 fb$^{-1}$  \cite{Khanpour:2017cfq,Ellis:2015sca}, FCC-ee  for $L_{int}$=10 $ab^{-1}$ at $\sqrt s=$ 240 GeV \cite{Ellis:2015sca}, CEPC for $L_{int}$=5 $ab^{-1}$ at $\sqrt s=$ 240 GeV \cite{Ge:2016tmm} at 95\% C.L. for $\bar{c}_{HW} $, $\bar{c}_{HB} $, $\bar{c}_{W}=- \bar{c}_{B}$ coefficients. The limits are each derived with all other coefficients set to zero.   \label{fig5}}
\end{figure}

\section{Conclusions}
We have investigated the CP-conserving dimension-6 operators of Higgs boson with other SM gauge boson via $e^+e^-\to\nu \bar{\nu} H$ process using an effective Lagrangian approach at first energy stage of CLIC ($\sqrt s=380$ GeV, $L_{int}$=500 fb$^{-1}$). We have used leading-order strongly interacting light Higgs basis assuming vanishing tree-level electroweak oblique parameterize and flavor universality of the new physics sector. We analyzed only hadronic ($b\bar b$ ) decay channel of the Higgs boson including dominant background processes by considering realistic detector effect in the analysis. We have shown the kinematic distributions of b-jets in final state, missing transverse energy, scalar transverse energy sum and invariant mass distributions. Due to the fact that the signal final state consists of two neutrinos and two b-jets, the distributions of missing transverse energy and scalar transverse energy sum are performed for determining a cut-based analysis. We have obtained 95 \% C.L. limits on dimension-six operators analysing invariant mass distributions of two b-jets from Higgs decay in $e^+e^-\to\nu \bar{\nu} H$ signal process and the other dominant backgrounds. The $e^+e^-\to\nu \nu H$ process is more sensitive to $\bar{c}_{HW}$ couplings than the other dimension-six couplings at first energy stage of CLIC. Our results show that a CLIC with $\sqrt s=380$ GeV, $L_{int}$=500 fb$^{-1}$ will be able to probe the dimension-six couplings of Higgs-gauge boson interactions in $e^+e^-\to\nu \bar{\nu} H$  process especially for $\bar{c}_{HW}$ couplings at scales beyond the HL-LHC bounds while they become competitive with the $\bar{c}_{HB} $, $\bar{c}_{W}=- \bar{c}_{B}$ couplings.

\begin{acknowledgments}
This work was partially supported by the Abant Izzet Baysal University Scientific Research Projects under the Project no: 2017.03.02.1137. H. Denizli's work was partially supported by Turkish Atomic Energy Authority (TAEK) under the grant No. 2013TAEKCERN-A5.H2.P1.01-24. The authors would like to thank to CLICdp group for the discussions, especially to Philipp G. Roloff for valuable suggestions in the CLICdp Working Group analysis meeting. Authors would also like to thank to L. Linssen for encouraging us to involve in CLICdp collaboration.
\end{acknowledgments}


\section{Introduction}
\label{sec:introduction}
Autonomous vehicle planning and control
frameworks~\cite{KTINTH15,apex} often follow the  hierarchical planning architecture
outlined by Firby~\cite{Firby89} and Gat~\cite{Gat98}.
The key idea here is to separate the complications involved in low-level
hardware control from high-level planning decisions to accomplish the navigation
objective.
A typical example of such separation-of-concerns is proving the controllability
property (vehicle can be steered from any start point to arbitrary neighborhood
of the target point) of the motion-primitives of the vehicle followed by the search
(path-planning) for an obstacle-free path (called the \emph{roadmap}) and then
utilizing the controllability property to compose the low-level primitives to
follow the path (path-following).
However, in the absence of the controllability property, it is not always
possible to follow arbitrary roadmaps with given motion-primitives.
In these situations we need to study a motion planning problem that is
not opaque to the motion-primitives available to the controller.

We study this motion planning problem in a simpler setting of systems modeled as
constant-rate multi-mode systems~\cite{ATW12}---a switched system with
constant-rate dynamics (vector) in every mode---and study the reachability
problem for the non-convex safety sets.
Alur et al.~\cite{ATW12} studied this problem for convex safety sets and
showed that it can be solved in polynomial time.
Our key result is that even for the case when the safety set is defined using
polyhedral obstacles, the problem of deciding reachability is undecidable.
On a positive side we show that if the safety set is an open set
defined by linear inequalities, the problem is decidable and can be
solved using a variation of cell-decomposition algorithm~\cite{SS83}.
We present a novel bounded model-checking~\cite{clarke2001bounded} inspired
algorithm equipped with acceleration to decide the reachability.
We use the Z3-theorem prover as the constraint satisfaction engine for the
quadratic formulas in our implementation.
We show the efficiency of our algorithm by comparing its performance with
the popular sampling based algorithm \emph{rapidly-exploring
  random tree} (RRT)  as implemented in the \textit{Open Motion Planning
Library (OMPL)}.

For a detailed survey of motion planning algorithms we refer to the
 excellent expositions by Latombe~\cite{latombe2012robot} and
 LaValle~\cite{Lav06}.
The motion-planning problem while respecting system dynamics can be
modeled~\cite{frazzoli2000robust} in the framework of hybrid
automata~\cite{ACHH92,Hen96}; however the reachability problem is
undecidable even for simple stopwatch automata~\cite{HKPV98}.
There is a vast literature on decidable subclasses of hybrid
automata~\cite{ACHH92,BBM98}.
Most notable among these classes are initialized rectangular hybrid
automata~\cite{HKPV98}, two-dimensional piecewise-constant derivative
systems~\cite{AMP95}, timed automata~\cite{alurDill94}, and
discrete-time control for hybrid automata~\cite{HK99}.
For a review of related work on multi-mode systems we refer to~\cite{AFMT13,ATW12}.

\section{Motivating Example}
\label{sec:motivation}
Let us consider a two-dimensional
multi-mode system with three modes $m_1, m_2$ and $m_3$ shown geometrically with
their rate-vectors in Figure~\ref{fig:l-shaped}(a).
We consider the reach-while-avoid problem in the arena given in
Figure~\ref{fig:l-shaped}(b) with two rectangular obstacles $\mathcal{O}_1$ and $\mathcal{O}_2$
and source and target points $\point{x}_s$ and $\point{x}_t$, respectively.
In particular, we are interested in the question whether it is possible to move
a point-robot from point $\point{x}_s$ to point $\point{x}_t$ using directions dictated by
the multi-mode system given in Figure~\ref{fig:l-shaped}(a) while avoiding
passing through or even grazing any obstacle.

It follows from our results in Section~\ref{sec:undec} that in general the
problem of deciding reachability is undecidable even with polyhedral obstacles.
However, the example considered in Figure~\ref{fig:l-shaped} has an interesting
property that the safety set can be represented as a union of finitely many
polyhedral open sets (cells).
This property, as we show later, makes the problem decidable.
In fact, if we decompose the workspace  into cells using any off-the-shelf
cell-decomposition algorithm, we only need to consider the sequences of obstacle-free
cells to decide reachability.
In particular, for a given sequence of obstacle-free convex sets such
that the starting
point is in the first set, and the target point is in last set, one can write
a linear program checking whether there is a sequence of intermediate states,
one each in the intersection of successive sets, such that these points are
reachable in the sequence using the constant-rate multi-mode system.
Our key observation is that one need not to consider cell-sequences larger than
the total number of cells since for reachability, it does not help for the system to
leave a cell and enter it again.

This approach, however, is not very efficient since one
needs to consider all sequences of the cells.
However, this result provides an upper bound on sequence of ``meta-steps'' or
``bound'' through the cells that system needs to take in order to reach the
target and hint towards a bounded model-checking~\cite{clarke2001bounded}
approach.
We progressively increase bound $k$  and ask whether there is a sequence of points
$\point{x}_0, \ldots, \point{x}_{k+1}$ such that $\point{x}_0 = \point{x}_s$, $\point{x}_{k+1} = \point{x}_t$, and
for all $0 \leq i \leq k$ we have that $\point{x}_i$ can reach $\point{x}_{i+1}$ using the
rates provided by the multi-mode system (convex cone of rates translated to
$\point{x}_i$ contains $\point{x}_{i+1}$) and the line segment $\lambda \point{x}_i + (1-\lambda)
\point{x}_{i+1}$ does not intersect any obstacle.
Notice that if this condition is satisfied, then the system can safely move from
point $\point{x}_i$ to $\point{x}_{i+1}$ by carefully choosing a scaling down of the
rates so as to stay in the safety set, as illustrated in Figure~\ref{fig:l-shaped}.

Let us first consider $k= 0$ and notice that one can reach point $\point{x}_t$ from
$\point{x}_s$ using just the mode $m_1$, however unfortunately the line segment
connecting these points passes through both obstacles.
In this case we increase the bound by $1$ and consider the problem of finding a
point $\point{x}$ such that the system can reach from $\point{x}_s$ to $\point{x}$ and also from
$\point{x}$ to $\point{x}_t$, and the line segment connecting $\point{x}_s$ with $\point{x}$, and $\point{x}$
with $\point{x}_t$ do not intersect any obstacles.
It is easy to see from the Figure~\ref{fig:l-shaped} that it is indeed the
case. We can alternate modes $m_1, m_2$ from $x_s$ to $x$, and
modes $m_1, m_3$ from $x$ to $x_t$.
Hence, there is a schedule that steers the system from $\point{x}_s$ to $\point{x}_t$ as
shown in the Figure~\ref{fig:l-shaped}(c).
\begin{figure}[t]
  \centering

    \begin{tikzpicture}[scale=0.4]
    \tikzstyle{lines}=[draw=black!30,rounded corners]
    \tikzstyle{vectors}=[-latex, rounded corners]
    \tikzstyle{rvectors}=[-latex,very thick, rounded corners]
    \draw[lines] (4.2,0)--(10.2,0);
    \draw[lines] (7, 3.2)--(7,-3);
    \draw[->, ultra thick, red] (7, 0) --node[black, right]{$~~~m_1$} (9, 1.8) node[left]{$$};
    \draw[->, ultra thick, green!50!black] (7, 0) --node[black, right]{$m_2$} (7, -1.8) node[left]{$$};
    \draw[->, ultra thick, blue] (7, 0) --node[black, left]{$m_3~$} (5, 1.8) node[left]{$$};
    \node at (10, -1) {$(a)$};
    \end{tikzpicture}
    \hfill
    \begin{tikzpicture}[scale=0.7]
      \draw (0,0) rectangle (4, 4);

      \filldraw[fill=black!40!white, draw=black] (0.15, 1) rectangle(3.75, 0.25);
      \filldraw[fill=black!40!white, draw=black] (3, 3.95) rectangle(3.75, 1.05);

      \draw[-,orange](0,1) -- (4, 1);
      \draw[-,orange](0,0.25) -- (4, 0.25);
      \draw[-,orange](3.75,0) -- (3.75, 4);
      \draw[-,orange](0.15,0) -- (0.15, 4);

      \draw[-,orange](0, 1.05) -- (4, 1.05);
      \draw[-,orange](0,3.95) -- (4, 3.95);

      \node [fill, draw, circle, minimum width=3pt, inner sep=0pt, pin={[fill=white, outer sep=2pt]225:$\point{x}_s$}] at (0.1,0.1) {};
      \node [fill, draw, circle, minimum width=3pt, inner sep=0pt, pin={[fill=white, outer sep=2pt]135:$\point{x}_t$}] at (3.9,3.9) {};

      \node at (2, .6) {$\mathcal{O}_1$};
      \node at (3.38, 2) {$\mathcal{O}_2$};
      \node at (4.8, 0) {$(b)$};
    \end{tikzpicture}
    \hfill
    \begin{tikzpicture}[scale=0.7]
	\draw (0,0) rectangle (4, 4);

        \filldraw[fill=black!40!white, draw=black] (0.15, 1) rectangle(3.75,
        0.25);
	\filldraw[fill=black!40!white, draw=black] (3, 3.95) rectangle(3.75, 1.05);
	 \draw [black!30, thick] (0.1, 0.1) -- (3.9, 0.1);
	 \draw [black!30, thick] (3.9, 0.1) -- (3.9, 3.9);
	 \node [fill, draw, circle, minimum width=3pt, inner sep=0pt, pin={[fill=white, outer sep=2pt]225:$\point{x}_s$}] at (0.1,0.1) {};
	 \node [fill, draw, circle, minimum width=3pt, inner sep=0pt, pin={[fill=white, outer sep=2pt]135:$\point{x}_t$}] at (3.9,3.9) {};
	 \node [fill, draw, circle, minimum width=3pt, inner sep=0pt,
           pin={[fill=white, outer sep=2pt]225: $\point{x}$}] at (3.9,0.1) {};
         \def0.15{0.15}
         \def0.15{0.15}
         \def0.3{0.15}
         \foreach \i in {0,...,24}{
           \draw[->,red](0.1+0.3*\i,0.1)--(0.1+0.15+0.3*\i, 0.1+0.15);
           \draw[->,green!50!black](0.1+0.15+0.3*\i,0.1+0.15)--(0.1+0.15+0.3*\i, 0.1);
	 }

         \def0.15{0.15}
         \def0.15{0.15}
         \def0.3{0.3}
         \foreach \i in {0,...,12}{
           \draw[->,blue](3.9,0.1+0.3*\i)--(3.9-0.15, 0.1+0.3*\i+0.15);
           \draw[->,red](3.9-0.15, 0.1+0.3*\i+0.15)--(3.9, 0.1+0.3*\i+2*0.15);
	 }

         \node at (2, .6) {$\mathcal{O}_1$};
        \node at (3.38, 2) {$\mathcal{O}_2$};
         \node at (4.8, 0) {$(c)$};
\end{tikzpicture}
\caption{ a) A multi-mode system, b) an
  ``L''-shaped arena consisting of obstacles $\mathcal{O}_1$ and $\mathcal{O}_2$ with
  start and target points $\point{x}_s$ and $\point{x}_t$ along with the
  cell-decomposition shown by orange lines, and
  c) a safe schedule from $\point{x}_s$ to $\point{x}_t$. }
\label{fig:l-shaped}
\end{figure}

The property  we need to check to ensure a safe schedule is the following:
there exists a sequence of points $x_s=x_0,x_1,x_2,\dots, x_n=x_t$ such that
for all $0\leq \lambda \leq 1$, and for all $i$, the line $\lambda x_i+(1-\lambda)x_{i+1}$
joining $x_i$ and $x_{i+1}$ does not intersect any obstacle $\mathcal{O}$.
This can be thought of as a first-order formula of the
form $\exists X \forall Y F(X, Y)$ where $F(X, Y)$ is a linear formula.
By invoking the Tarski-Seidenberg theorem we know that checking the satisfiability
of this  property is decidable.
However, one can also give a direct quantifier elimination based on
Fourier-Motzkin elimination procedure to get existentially quantified quadratic
constraints that can be efficiently checked using theorem provers such as Z3
(\url{https://github.com/Z3Prover/z3}).
This gives us a complete procedure to decide reachability for multi-mode systems
when the safety set can be represented as a union of finitely many polyhedral open sets.

\section{Problem Formulation}
\label{sec:problem}
\noindent{\bf Points and Vectors.}
Let $\mathbb R$ be the set of real numbers.
We represent the states in our system as points in $\mathbb R^n$, which is equipped
with the standard \emph{Euclidean norm} $\norm{\cdot}$.
We denote points in this state space by $\point{x}, \point{y}$,  vectors by $\vec{r}, \vec{v}$, and
the $i$-th coordinate of point $\point{x}$ and vector $\vec{r}$ by $\point{x}(i)$ and $\vec{r}(i)$,
respectively.
The distance $\norm{\point{x}, \point{y}}$ between points $\point{x}$ and $\point{y}$ is defined as
$\norm{\point{x} - \point{y}}$.

\noindent{\bf Boundedness and Interior.}
We denote an {\em open ball} of radius $d \in {\mathbb R}_{\geq 0}$ centered at $\point{x}$ as
$\ball{d}{\point{x}} {=} \set{\point{y} {\in} \mathbb R^n \::\: \norm{\point{x},\point{y}} < d}$.
We denote a closed ball of radius $d \in {\mathbb R}_{\geq 0}$ centered at $\point{x}$ as
$\overline{\ball{d}{\point{x}}}$.
We say that a set $S \subseteq \mathbb R^n$ is {\em bounded} if there exists
$d \in {\mathbb R}_{\geq 0}$ such that, for all $\point{x}, \point{y} \in S$, we have
$\norm{\point{x},\point{y}} \leq d$.
The {\em interior} of a set $S$, $\interior(S)$, is the set of all points
$\point{x} \in S$, for which there exists $d > 0$ s.t. $\ball{d}{\point{x}} \subseteq S$.

\noindent{\bf Convexity.} A point $\point{x}$ is a \emph{convex
  combination} of a finite set of points $X = \set{\point{x}_1, \point{x}_2, \ldots, \point{x}_k}$ if
there are $\lambda_1, \lambda_2, \ldots, \lambda_k \in [0, 1]$ such that
$\sum_{i=1}^{k} \lambda_i = 1$ and $\point{x} = \sum_{i=1}^k \lambda_i \cdot \point{x}_i$.
We say that $S \subseteq \mathbb R^n$ is {\em convex} iff, for all
$\point{x}, \point{y} \in S$ and all $\lambda \in [0,1]$, we have
$\lambda \point{x} + (1-\lambda) \point{y} \in S$ and moreover,
$S$ is a {\em convex polytope} if there exists $k \in \mathbb N$, a
matrix $A$ of size $k \times n$ and a vector $\vec{b} \in \mathbb R^k$ such that $\point{x}
\in S$ iff $A\point{x} \leq \vec{b}$.
A closed \emph{hyper-rectangle} is a convex polytope that can
be characterized as $\point{x}(i) \in [a_i, b_i]$ for each $i \leq n$ where $a_i, b_i
\in \mathbb R$.

\begin{definition}
  \label{def:BMMS}
  A (constant-rate) multi-mode system (MMS) is a tuple $\mathcal{H} = (M, n, R)$ where:
    $M$ is a finite nonempty set of \emph{modes},
    $n$ is the number of continuous variables, and
    $R : M \to \mathbb R^n$ maps to each mode a rate vector
    whose $i$-th entry specifies the change in the value of the $i$-th
    variable per time unit.
    For computation purposes, we assume that the real numbers
    are rational.
\end{definition}

\begin{example}
  An example of a 2-dimensional multi-mode system  $\mathcal{H} = (M, n, R)$ is shown in
Figure~\ref{fig:l-shaped}(a) where $M = \set{ m_1, m_2, m_3}$, $n = 2$, and the
rate vector is such that $R(m_1) = (1, 1)$, $R(m_2) = (0, -1)$, and $R(m_3) =
(-1, 1)$.
\end{example}
A \emph{schedule} of an MMS specifies a timed sequence of mode switches.
Formally, a \emph{schedule} is defined as a finite or infinite sequences of
\emph{timed actions}, where a timed action $(m, t) \in M \times {\mathbb R}_{\geq 0}$ is a
pair consisting of a mode and a time delay.
A finite \emph{run} of an MMS $\mathcal{H}$ is a finite sequence of states and timed
actions $r = \seq{\point{x}_0, (m_1, t_1), \point{x}_1,  \ldots, (m_k, t_k), \point{x}_k}$
such that for all $1 \leq i \leq k$ we have that
$\point{x}_i = \point{x}_{i-1} + t_i \cdot R(m_i)$.
For such a run $r$ we say that $\point{x}_0$ is the \emph{starting state}, while
$\point{x}_k$ is its \emph{terminal state}.
An \emph{infinite run} of an MMS $\mathcal{H}$ is similarly defined to be an infinite
sequence $\seq{\point{x}_0, (m_1, t_1), \point{x}_1, (m_2, t_2), \ldots}$ such that for all
$i \geq 1$ we have that $\point{x}_i = \point{x}_{i-1} + t_i \cdot  R(m_i)$.

Given a finite schedule $\sigma = \seq{(m_1, t_1), (m_2, t_2), \ldots, (m_k,
  t_k)}$ and a state $\point{x}$, we write $\text{\it Run}(\point{x}, \sigma)$ for the (unique)
finite run  $\seq{\point{x}_0, (m_1, t_1), \point{x}_1, (m_2, t_2), \ldots,
  \point{x}_k}$ such that $\point{x}_0 = \point{x}$.
In this case, we also say that the schedule $\sigma$ steers the MMS $\mathcal{H}$ from the state
$\point{x}_0$ to the state $\point{x}_k$.

We consider the problem of MMS reachability within a given \emph{safety set}
$S$.
We specify the safety set by a pair $(\mathcal{W}, \mathcal{O})$, where
$\mathcal{W} \subseteq \mathbb R^n$ is called the \emph{workspace} and
$\mathcal{O} = \set{\mathcal{O}_1, \mathcal{O}_2, \ldots, \mathcal{O}_k}$ is a finite set of
\emph{obstacles}.
In this case the safety set $S$ is characterized as $S_{\mathcal{W} \backslash \mathcal{O}}  = \mathcal{W} \setminus \mathcal{O}$.
 We assume in the rest of the
paper that $\mathcal{W} = \mathbb R^n$ and for all $1 \leq i \leq k$, $\mathcal{O}_i$ is a
\emph{convex} (not necessarily closed) polytope specified by a set of linear
inequalities.

We say that a finite run
$\seq{\point{x}_0, (m_1, t_1), \point{x}_1, (m_2, t_2),  \ldots}$ is $S$-safe if for
all $i \geq 0$ we have that $\point{x}_i \in S$ and
$\point{x}_i + \tau_{i+1} \cdot R(m_{i+1}) \in S$ for all $\tau_{i+1} \in [0, t_{i+1}]$.
Notice that if $S$ is a convex set then for all $i \geq 0$,
$\point{x}_i \in S$ implies that for all $i \geq 0$ and for all $\tau_{i+1} \in
[0, t_{i+1}]$ we have that $\point{x}_i + \tau_{i+1} \cdot  R(m_{i+1}) \in S$.
We say that a schedule $\sigma$ is $S$-safe from a state $\point{x}$, or is $(S,
\point{x})$-safe, if the
corresponding unique run $\text{\it Run}(\point{x}, \sigma)$ is $S$-safe.
Sometimes we simply call a schedule or a run safe when the safety set and
the starting state are clear from the context.
We say that a state $\point{x}'$ is $S$-safe reachable from a state $\point{x}$ if there
exists a finite schedule $\sigma$  that is $S$-safe at $\point{x}$ and steers the
system from state $\point{x}$ to $\point{x}'$.

We are interested in solving the following problem.

\begin{definition}[Reachability]
  Given a constant-rate multi-mode system $\mathcal{H} = (M, n, R)$, safety
  set $S$, start state $\point{x}_s$, and target state $\point{x}_t$, the
  reachability problem $\textsc{Reach}(\mathcal{H}, S_{\mathcal{W} \backslash \mathcal{O}}, \point{x}_s, \point{x}_t)$ is to decide
  whether there exists an $S$-safe finite schedule that steers the
  system from state $\point{x}_s$ to $\point{x}_t$.
\end{definition}

Alur \emph{et al.}~\cite{ATW12} gave a polynomial-time algorithm to
decide if a state $\point{x}_t$ is $S$-safe reachable from a state $\point{x}_0$
for an MMS $\mathcal{H}$ for a convex safety set $S$.  In particular, they
characterized the following necessary and sufficient condition.
\begin{theorem} [\cite{ATW12}]
  \label{thmcms}
  Let $\mathcal{H} = (M, n, R)$ be a multi-mode system and let $S \subset \mathbb R^n$ be an
  open, convex safety set.
  Then, there is an $S$-safe schedule from $\point{x}_s \in S$ to $\point{x}_t \in S$, if and only if there is $\vec{t} \in {\mathbb R}_{\geq 0}^{|M|}$
  satisfying:
  $  \point{x}_s + \sum_{i=1}^{|M|} R(m_i) \cdot \vec{t}(i) = \point{x}_t$.
\end{theorem}
A key property of this result is that if $\point{x}_t$ is reachable from $\point{x}_s$ without
considering the safety set, then it is also reachable inside arbitrary convex
set as long as both $\point{x}_s$ and $\point{x}_t$ are strictly in the interior of the
safety set.

We study the extension of this theorem for the reachability problem with
non-convex safety sets.  A key contribution of this paper is a precise
characterization of the decidability of the reachability problem for
multi-mode systems.
\begin{theorem}
  \label{thm:main}
  Given a constant-rate multi-mode system $\mathcal{H}$, workspace
  $\mathcal{W} = \mathbb R^n$, obstacles set $\mathcal{O}$, start state $\point{x}_s$ and target
  state $\point{x}_t$, the reachability problem
  $\textsc{Reach}(\mathcal{H}, S_{\mathcal{W} \setminus \mathcal{O}}, \point{x}_s, \point{x}_t)$ is in general
  undecidable.
  However, if the obstacle set $\mathcal{O}$ is given as finitely many closed
  polytopes, each defined by a finite set of linear inequalities, then
  reachability is decidable.
\end{theorem}

\section{Decidability}
\label{sec:decidability}
We prove the decidability condition of Theorem \ref{thm:main} in this section.
\begin{theorem}
\label{thm:dec}
For a MMS $\mathcal{H} = (M, n, R)$, a safety set $S$, a start state $\point{x}_s$,
and a target state $\point{x}_t$, the problem $\textsc{Reach}(\mathcal{H}, S_{\mathcal{W} \backslash \mathcal{O}}, \point{x}_s, \point{x}_t)$
is decidable if $\mathcal{O}$ is given as finitely many closed polytopes.
\end{theorem}
For the rest of this section let us fix  a MMS $\mathcal{H} =
(M, n, R)$,
a start state $\point{x}_s$ and a target state $\point{x}_t$.  Before we prove
this theorem, we define cell cover (a notion related to, but distinct
from the one of cell decomposition introduced
in~\cite{latombe2012robot}).

\begin{definition}[Cell Cover]
  Given a safety set $S \in \mathbb R^n$, a cell of $S$ is an open, convex
  set that is a subset of $S$.  A \emph{cell cover} of $S$ is a
  collection $\mathcal{C} = \set{c_1, \ldots, c_N}$ of cells whose union
  equals $S$.  Cells $c, c' \in \mathcal{C}$ are \emph{adjacent} if and only
  if $c \cap c'$ is non-empty.
\end{definition}

A \emph{channel} in $S$ is a finite sequence
$\seq{c_1, c_2, \ldots, c_N}$ of cells of $S$ such that $c_i$ and
$c_{i+1}$ are adjacent for all $1 \leq i < N$.  It follows that
$\cup_{1 \leq i \leq N} c_i$ is a path-connected open set.
A $\mathcal{C}$-channel is a channel whose cells are in cell cover
$\mathcal{C}$.

Given a channel $\pi = \seq{c_1, \ldots, c_N}$, a multi-mode
system $\mathcal{H} = (M, n, R)$, start and target states
$\point{x}_s, \point{x}_t \in S$, we say that $\pi$ is a \emph{witness} to
reachability if the following linear program is feasible:
\begin{gather}
  \bigexists_{0 \leq i \leq N} \point{x}_i  \,.
  \Big( \point{x}_s = \point{x}_0  \wedge  \point{x}_t = \point{x}_N \Big) \wedge
  \Big(1 \leq i < N \rightarrow \point{x}_i \in (c_i \cap c_{i+1})\Big)
  \,\wedge  \label{eq4} \\
  \bigexists_{1 \leq i \leq N, m \in M} t_i^{(m)} \,. \Big(t_i^{(m)}
  \geq 0\Big) \wedge \bigwedge_{1
    \leq i \leq N} \Big(\point{x}_i = \point{x}_{i-1} + \sum_{m\in M} R(m) \cdot
    t_i^{(m)}\Big) \enspace.\nonumber
\end{gather}

\begin{lemma}
  \label{witness}
  If $S$ is an open safety set, there exists a finite $S$-safe
  schedule that solves $\textsc{Reach}(\mathcal{H}, S, \point{x}_s, \point{x}_t)$ if and only if
  $S$ contains a witness channel $\seq{c_1, c_2, \ldots, c_N}$ for some
  $N \in \mathbb{N}$.
\end{lemma}
\begin{proof}
  ($\Leftarrow$) If $\seq{c_1, c_2, \ldots, c_N}$ is a witness channel,
  then for $0 < i \leq N$, $\point{x}_{i-1}$ and $\point{x}_i$ are in $c_i$.
  Theorem~\ref{thmcms} guarantees the existence of a $c_i$-safe
  schedule for each $i$.  The concatenation of these schedules is a
  solution to $\textsc{Reach}(\mathcal{H}, S, \point{x}_s, \point{x}_t)$.

  ($\Rightarrow$)
  The run of a finite schedule that solves
  $\textsc{Reach}(\mathcal{H}, S, \point{x}_s, \point{x}_t)$ defines a closed, bounded subset $P$ of $S$.
  Since $S$ is open, every point $x \in P$ is contained in a cell
  of $S$.
  Collectively, these cells form an open cover of $P$.
  By compactness, then, there is a finite subcover of $P$.
  If any element of the subcover is entered by the run more than once, there
  exists another run that is contained in that cell between the first entry and
  the last exit.
  For such a run, if two elements of the subcover are entered at the same time,
  the one with the earlier exit time is redundant.
  Therefore, there is a subcover in which no two elements are entered by
  the run of the schedule at the same time.
  This subcover can be ordered according to the time at which the run enters
  each cell to produce a sequence that satisfies the definition of witness
  channel.

  \qed
\end{proof}

\begin{lemma}
  \label{generic-witness-to-c-witness}
  If $S$ is an open safety set and $\mathcal{C}$ a cell cover of
  $S$, there exists a witness channel for $\textsc{Reach}(\mathcal{H}, S, \point{x}_s, \point{x}_t)$
  iff there exists a witness $\mathcal{C}$-channel.
\end{lemma}
\begin{proof}
  One direction is obvious.  Suppose therefore that there exists a
  witness channel; let $\sigma$ be the finite schedule whose existence is
  guaranteed by Lemma~\ref{witness}.  The path that is traced in the MMS $\mathcal{H}$
  when steered by $\sigma$ is a bounded closed subset $P$ of $S$
  because it is the continuous image of a compact interval of the real
  line.  (The time interval in which $\mathcal{H}$ moves from $\point{x}_s$ to
  $\point{x}_t$.)  Since $\mathcal{C}$ is an open cover of $P$, there exists a
  finite subset of $\mathcal{C}$ that covers $P$; specifically, there is an
  irredundant finite subcover such that no two cells are entered at
  the same time during the run of $\sigma$.  This subcover can be
  ordered according to entry time to produce a sequence of cells that
  satisfies the definition of witness channel. \qed
\end{proof}

\begin{lemma}
\label{cell-decomposition-to-cover}
  If $\mathcal{O}$ is a finite set of closed polytopes, then a finite cell
  cover of the safety set $S$ is computable.
\end{lemma}
\begin{proof}
  If $\mathcal{O}$ is a finite set of closed polytopes, one can apply the the
  vertical decomposition algorithm of \cite{latombe2012robot} to
  produce a cell \emph{decomposition}.  Each cell $C$ in this
  decomposition of dimension less than $n$ that is not contained in
  the obstacles (and hence is entirely contained in $S$) is replaced
  by a convex open set obtained as follows.  Let $B$ be an
  $n$-dimensional box around a point of $C$ that is in $S$.  The
  desired set is the convex hull of the set of vertices of either $C$
  or $B$. \qed
\end{proof}

\begin{proof}[of Theorem~\ref{thm:dec}]
  Lemmas~\ref{witness}--\ref{generic-witness-to-c-witness}
  imply that $\textsc{Reach}(\mathcal{H}, S, \point{x}_s, \point{x}_t)$ is decidable if a finite
  cell cover of $S$ is available.  If $\mathcal{O}$ is given as a finite set
  of closed polytopes, each presented as a set of linear inequalities,
  then Lemma~\ref{cell-decomposition-to-cover} applies.  \qed
\end{proof}

\begin{algorithm}[t]
  \KwIn{MMS $\mathcal{H} = (M, n, R)$, two points $\point{x}_s, \point{x}_t$, workspace $\mathcal{W}$,
    obstacle set $\mathcal{O}$, and an upper bound $B$ on number of cells in a cell-cover. }
  \KwOut{NO, if no safe schedule exists and otherwise
    such a schedule.}
  \BlankLine
  $k \leftarrow 0$;
\While{$k \leq B $}{
    Check if the following formula is satisfiable:
    \begin{eqnarray*}
     \bigexists\limits_{1 \leq i \leq N} \point{x}_i && \bigexists\limits_{1 \leq i \leq N, m \in M}
     t_i^{(m)} \text{ s.t. }
      \left( \point{x}_s = \point{x}_1  \wedge  \point{x}_t = \point{x}_N \right) \wedge
      \bigwedge\limits_{\stackrel{1\leq i \leq N}{m \in M}}  t_i^{(m)} \geq 0  \wedge  \\
      &
      \bigwedge\limits_{i=2}^{N} & \left(\point{x}_i = \point{x}_{i-1} + \sum_{m\in M} R(m) \cdot
      t_i^{(m)}\right)  \wedge
       \bigwedge\limits_{i=2}^{N} \textsc{ObstacleFree}(\point{x}_{i-1}, \point{x}_{i})
    \end{eqnarray*}
    \lIf{not satisfiable}{
      $k \leftarrow k+1$
    }
    \uElse
        {
          Let $\sigma$ be an empty sequence\;
          \For{$i = 1$ to $k-1$ }{
            $\sigma = \sigma :: \textsc{Reach\_Convex}(\mathcal{H}, \point{x}_i, \point{x}_{i+1}, S)$}
        }
        \Return $\sigma$\;
  }
  \caption{\textsc{BoundedMotionPlan}($\mathcal{H}, \mathcal{W}, \mathcal{O}, \point{x}_s, \point{x}_t, B$)}
  \label{alg:mainLoop}
\end{algorithm}

\begin{algorithm}[h!]
\caption{\label{algo:mms} $\textsc{Reach\_Convex}(\mathcal{H}, \point{x}_s, \point{x}_t, S)$}
\KwIn{MMS $\mathcal{H} = (M, n, R)$, two points $\point{x}_s, \point{x}_t$, convex, open, safety set $S$}
\KwOut{NO if no $S$-safe schedule from $\point{x}_s$ to $\point{x}_t$ exists and otherwise
  such a schedule.}
$t_1 =
\min\limits_{m \in M} \max \set{\tau \::\: \point{x}_s + \tau \cdot R(m) \in S}$\;
$t_2 =
\min\limits_{m \in M} \max \set{\tau \::\: \point{x}_t + \tau \cdot R(m) \in S}$\;
$t_\text{safe} = \min \set{t_1, t_2}$\;
Check whether the following linear program is feasible:
\begin{align}
  \point{x}_s + \sum_{m\in M} R(m) \cdot t^{(m)} = \point{x}_t
  & \text{ and } &
  t^{(m)} \geq 0 \text{ for all $m \in M$}~\label{eqn3}
\end{align}

\lIf{no satisfying assignment exists}{\Return NO}
\Else{
  Find an assignment $\{t^{(m)}\}_{m\in M}$.

  Set $l = \lceil (\sum_{m \in M} t^{(m)})/t_\text{safe}\rceil $.

  {\bf return} the following schedule  $\seq{(m_i, t_i)}$ where
  \[
  m_k = (k \bmod |M|) + 1 \text{  and } t_k = t^{(m_k)} / l
  \text{  for $k = 1, 2, \ldots, l|M|$.}
  \]
}
\end{algorithm}

The algorithm implicit in the proof of Theorem~\ref{thm:dec} requires
one to compute the cell cover in advance, and enumerate
sequences of cells in order to decide reachability.  We next present
an algorithm inspired by bounded model
checking~\cite{clarke2001bounded} that implicitly enumerates sequences
of cells of increasing length till the upper bound on number of cells
is reached, or a safe schedule from the source point to the target
point is discovered.  The key idea is to guess a sequence of points
${\point{x}_1, \ldots, \point{x}_N}$ starting from the source point and ending in
the target point such that for every $1 \leq i < N$ the point
$\point{x}_{i+1}$ is reachable from $\point{x}_i$ using rates provided by the
multi-mode system.  Moreover, we need to check that the line segment
connecting $\point{x}_i$ and $\point{x}_{i+1}$ does not intersect with obstacles,
i.e:
$\bigforall_{0 \leq \lambda \leq 1} (\lambda \point{x}_i + (1-\lambda) \point{x}_{i+1}) \not \in \cup_{j = 1}^{k} \mathcal{O}_j$.
We write $\textsc{ObstacleFree}(\point{x}_i, \point{x}_{i+1})$ for this condition.
Algorithm~\ref{alg:mainLoop} sketches a bounded-step algorithm to
decide reachability for multi-mode systems that always terminates for
multi-mode systems with sets of closed obstacles defined by linear
inequalities thanks to Theorem~\ref{thm:dec}.

Notice that at line~$2$ of algorithm \ref{alg:mainLoop}, we need to check the feasibility of
the constraints system, which is of the form $\exists X \forall Y F(X, Y)$ where
universal quantifications are implicit in the test for $\textsc{ObstacleFree}$.
If the solver we use to solve the constraints has full support to solve the
$\forall$ quantification, we can use that to solve the above constraint. In our
experiments, we used the Z3 solver (\url{https://github.com/Z3Prover/z3})
to implement the Algorithm~\ref{alg:mainLoop} and found that the
solver was unable to solve in some cases.
Fortunately, the universal quantification in our constraints is of very special
form and can be easily removed using the Fourier-Motzkin elimination procedure,
which results in quadratic constraints that are efficiently solvable by Z3
solver.
In Section~\ref{sec:experiments} we present the experimental results on some
benchmarks to demonstrate scalability.

\section{Undecidability}
\label{sec:undec}
In this section we give a sketch of the proof of the following undecidability
result.
\begin{theorem}
  \label{thm:undec}
  Given a constant-rate multi-mode system $\mathcal{H}$, convex workspace
  $\mathcal{W}$, obstacles set $\mathcal{O}$, start state $\point{x}_s$ and target state $\point{x}_t$,
  the reachability problem $\textsc{Reach}(\mathcal{H}, S_{\mathcal{W} \backslash \mathcal{O}}, \point{x}_s, \point{x}_t)$ is
  in general undecidable.
\end{theorem}
\begin{proof}{(Sketch.)}
We prove the undecidability of this problem by giving a reduction from
the halting problem for two-counter machines that is known to be
undecidable~\cite{Min67}.
Given a two counter machine $\mathcal{A}$ having instructions $L = \ell_1$, $\dots$,
$\ell_{n-1}, \ell_{halt}$,  we construct a multi-mode system $\mathcal{H}_\mathcal{A}$ along
with  non-convex safety $S_{\mathcal{W} \backslash \mathcal{O}}$ characterized using linear constraints.
The idea is to simulate the unique run of two-counter machine $\mathcal{A}$ via the unique
safe schedule of the MMS $\mathcal{H}_\mathcal{A}$ by going through a sequence of modes such
that a pre-specified target point is reachable iff the counter machine halts.

\noindent \textbf{Modes}. For every increment/decrement instruction $\ell_i$ of the counter machine we
have two modes $\mathcal{M}_i$ and $\mathcal{M}_{ik}$, where  $k$ is the index of the unique
instruction $\ell_k$ to which the control shifts in $\mathcal{A}$ from $\ell_i$.
For every zero check instruction $\ell_i$,  we have four modes $\mathcal{M}^1_i,
\mathcal{M}^2_i, \mathcal{M}_{ik}$ and $\mathcal{M}_{im}$, where  $k,m$ are respectively the indices of
the unique instructions $\ell_k, \ell_m$ to which the control shifts from
$\ell_i$ depending on whether the counter value is $>0$ or $=0$.
There are three modes $\mathcal{M}_{halt}, \mathcal{M}^{c_1}_{halt}$ and $\mathcal{M}^{c_2}_{halt}$
corresponding to the halt instruction.
We have a special ``initial'' mode $\mathcal{I}$ which is the first mode to be
applied in any safe schedule.

\noindent \textbf{Variables}. The MMS $\mathcal{H}_\mathcal{A}$ has two variables $C=\{c_1, c_2\}$ that store the value
of two counters.
There is a unique variable $S=\{s_0\}$ used to enforce that mode  $\mathcal{I}$
as the first mode.
For every increment or decrement instruction $\ell_i$,
there are variables $w_{ij}, x_{ij}$, where $j$ is the index of the unique
instruction
$\ell_j$ to which control shifts from $\ell_i$.
We define variable $z_{i\#}$ for each zero-check instruction $\ell_i$.

\noindent \textbf{Simulation}.   A simulation of the two counter machine going through instructions
$\ell_0$, $\ell_1$, $\ell_2$, $\dots, \ell_y, \ell_{halt}$ is achieved by going through modes
$\mathcal{I}, \mathcal{M}_{0}, \mathcal{M}_{01}, \mathcal{M}_1$ or $\mathcal{M}^1_1$ or $\mathcal{M}^2_1 \dots, \mathcal{M}_y, \mathcal{M}_{y~halt}$ in order, spending exactly one unit of time in each mode.
Starting from a point $\point{x}_s$ with $s_0=1$ and $v=0$ for all variables $v$ other than $s_0$, we
want to reach a point $\point{x}_t$  where $w_{halt}=1$ and
 $v=0$ for all variables $v$ other than $w_{halt}$.
The idea is to start in  mode $\mathcal{I}$, and
spending one unit of time in  $\mathcal{I}$ obtaining $s_0=0, w_{01}=1$
(spending a time other than one violates safety, see Lemma~\ref{one}).
Growing $w_{01}$ represents that the current instruction is $\ell_0$, and the next one is $\ell_1$.
Next, we shift to mode $\mathcal{M}_0$,
spend one unit of time there to obtain $x_{01}=1, w_{01}=0$.
This is followed by
mode $\mathcal{M}_{01}$, where $x_{01}$ becomes 0, and one of the variables $z_{1\#}, w_{12}$ attain 1, depending on whether
$\ell_1$ is a zero check instruction or not (again, spending a time other than
one in $\mathcal{M}_0, \mathcal{M}_{01}$ violates safety, see Lemma~\ref{two}).

In general, while at a  mode $\mathcal{M}_{ij}$, the next instruction
$\ell_k$ after $\ell_j$ is chosen  by ``growing'' the variable $w_{jk}$ if $\ell_j$ is not a zero-check instruction, or
by ``growing'' the  variable $z_{j\#}$  if $\ell_j$ is a zero-check instruction.
 In parallel, $x_{ij}$ grows down to 0, so that $x_{ij}+w_{jk}=1$ or $x_{ij}+z_{j\#}=1$.
 The sequence of choosing modes, and enforcing that one unit of time be spent in each mode
 is necessary to adhere to the safety set as can be seen by Lemmas~\ref{two} and~\ref{three}.
 \begin{itemize}
\item  In the former case, the control shifts from $\mathcal{M}_{ij}$ to mode
$\mathcal{M}_j$ where variable $x_{jk}$ grows at rate 1 while $w_{jk}$ grows at rate -1, so that
 $x_{jk}+w_{jk}=1$. Control shifts from $\mathcal{M}_j$ to $\mathcal{M}_{jk}$, where the next instruction $\ell_g$ after $\ell_k$ is chosen
 by growing  variable $w_{kg}$ if $\ell_k$ is not zero-check instruction, or
 the variable $z_{k\#}$ is grown if $\ell_k$ is a zero-check instruction.
  \item  In the latter case, one of the modes $\mathcal{M}^1_j,\mathcal{M}^2_j$ is chosen from $\mathcal{M}_j$ where
   $z_{j\#}$ grows at rate -1.
  Assume $\ell_j$ is the instruction ``If the counter value is $>0$, then goto $\ell_m$, else goto $\ell_h$".
      If  $\mathcal{M}^1_j$ is chosen, then the variable $x_{jm}$ grows at rate 1
   while if $\mathcal{M}^2_j$ is chosen, then the variable $x_{jh}$ grows at rate 1.
   In this case, we have $z_{j\#}+x_{jm}=1$ or $z_{j\#}+x_{jh}=1$.
   From $\mathcal{M}^1_j$, control shifts to $\mathcal{M}_{jm}$, while from
   $\mathcal{M}^2_j$, control shifts to $\mathcal{M}_{jh}$.
\end{itemize}
Continuing in the above fashion, we eventually reach mode $\mathcal{M}_{y~halt}$
where $x_{y~halt}$ grows down to 0, while the variable $w_{halt}$ grows to 1, so that
$x_{y~halt}+w_{halt}=1$(see Lemma~\ref{last} which enforces this).

Starting from $\point{x}_s$---which lies in the hyperplane $H_0$
given as  $s_0+w_{0j}=1$  where $\ell_j$ is the unique instruction  following
$\ell_0$---a safe execution stays in $H_0$ as long as control stays in the initial mode
$\mathcal{I}$.
Control then switches to mode $\mathcal{M}_0$,  to the hyperplane $H_1$ given by
 $w_{0j}+x_{0j}=1$.  Note that $H_0 \cap H_1$ is non-empty and intersect at the
point   where $w_{0j}=1$, and all other variables are $0$.
Spending a unit of time at $\mathcal{M}_0$, control switches to mode $\mathcal{M}_{0j}$, and
to the hyperplane $H_2$ given by $x_{0j}+w_{jk}=1$ depending on whether
$\ell_j$ is not a zero-check instruction.
Again, note that $H_1 \cap H_2$ is non-empty and intersect
at the point where $c_1=1, x_{0j}=1$ and all other variables are zero.
This continues, and we obtain a safe transition from hyperplane $H_i$ to
$H_{i+1}$ as dictated by the simulation of the two counter machine.
The sequence of safe hyperplanes lead to the hyperplane $H_{last}$ given by
$w_{halt}=1$ and all other variables 0 iff the two counter machine halts.
Appendix \ref{app:undec-eg}
gives an example of a reduction
from 2-counter machines.
\qed
\end{proof}

\section{Experimental Results}
\label{sec:experiments}
In this section, we discuss some preliminary results obtained with an
implementation of Algorithm~\ref{alg:mainLoop}.
In order to show competitiveness of the proposed algorithm, we compare its
performance with a popular implementation of the RRT algorithm~\cite{Lav06} on a
collection of micro-benchmarks (some of these benchmarks are inspired by \cite{saha}).

\subsection{Experimental Setup}
Rapidly-exploring Random
Tree (RRT)~\cite{Lav06} is a space-filling data structure that is used to search a
region by incrementally building a tree.
It is constructed by selecting random points in the state space and can provide
better coverage of reachable states of a system than mere simulations.
There are many versions of RRTs available;  we use the \emph{Open Motion Planning
Library (OMPL)} implementation of RRT for our experiments. The
OMPL  library (http://ompl.kavrakilab.org)
consists of many
state-of-the-art, sampling-based motion planning algorithms. We used the RRT API provided by the OMPL library.
The results for RRT were obtained with a goal bias parameter set to $0.05$, and obstacles implemented
as \texttt{StateValidityCheckerFunction()} as mentioned in the documentation~\cite{sucan2012the-open-motion-planning-library}.

We implemented our algorithm on the top of the Z3
solver~\cite{DeMoura:2008:ZES:1792734.1792766}. The
implementation involves coding formulae in FO-logic over reals and checking
for a satisfying assignment. Our algorithm was implemented in Python 2.7. The OMPL implementation was done in C++.
The experiments with Algorithm~\ref{alg:mainLoop}
and RRT were performed on a computer running Ubuntu 14.10,
with an Intel Core i7-4510 2.00 GHz quadcore CPU, with 8 GB RAM.
We compared the two algorithms by executing them on a
set of microbenchmarks whose
 obstacles are hyper-rectangular, though our
algorithm can handle general polyhedral obstacles.
\begin{figure}[t]
    \begin{center}
    \begin{tikzpicture}
      \draw (0,0) rectangle (7, 4);
      \filldraw[fill=black!40!white, draw=black] (1, 0) rectangle(2, 3.5);
      \filldraw[fill=black!40!white, draw=black] (2.5, 4) rectangle(3.5, 0.5);
      \filldraw[fill=black!40!white, draw=black] (4, 0) rectangle(5, 3.5);
      \filldraw[fill=black!40!white, draw=black] (5.5, 4) rectangle(6.5, 0.5);
      \node [fill, draw, circle, minimum width=3pt, inner sep=0pt, pin={[fill=white, outer sep=2pt]225:$\point{x}_s$}] at (0.2,0.1) {};
      \node [fill, draw, circle, minimum width=3pt, inner sep=0pt, pin={[fill=white, outer sep=2pt]135:$\point{x}_t$}] at (6.9,3.9) {};
      \draw [black!30, thick] (0.2, 0.1) -- (0.2, 3.9);
      \node [fill, draw, circle, minimum width=3pt, inner sep=0pt, pin={[fill=white, outer sep=2pt]135:$\point{x}_1$}] at (0.2,3.9) {};
      \draw [black!30, thick] (0.2, 3.9) -- (2.2, 3.9);
      \node [fill, draw, circle, minimum width=3pt, inner sep=0pt, pin={[fill=white, outer sep=2pt]135:$\point{x}_2$}] at (2.2,3.9) {};
      \draw [black!30, thick] (2.2, 0.2) -- (2.2, 3.9);
      \node [fill, draw, circle, minimum width=3pt, inner sep=0pt, pin={[fill=white, outer sep=2pt]225:$\point{x}_3$}] at (2.2,0.2) {};
      \draw [black!30, thick] (2.2, 0.2) -- (3.7, 0.2);
      \node [fill, draw, circle, minimum width=3pt, inner sep=0pt, pin={[fill=white, outer sep=2pt]225:$\point{x}_4$}] at (3.7,0.2) {};
      \draw [black!30, thick] (3.7, 3.9) -- (3.7, 0.2);
      \node [fill, draw, circle, minimum width=3pt, inner sep=0pt, pin={[fill=white, outer sep=2pt]135:$\point{x}_5$}] at (3.7,3.9) {};
      \draw [black!30, thick] (3.7, 3.9) -- (5.2, 3.9);
      \node [fill, draw, circle, minimum width=3pt, inner sep=0pt, pin={[fill=white, outer sep=2pt]135:$\point{x}_6$}] at (5.2,3.9) {};
      \draw [black!30, thick] (5.2, 0.2) -- (5.2, 3.9);
      \node [fill, draw, circle, minimum width=3pt, inner sep=0pt, pin={[fill=white, outer sep=2pt]225:$\point{x}_7$}] at (5.2,0.2) {};
      \draw [black!30, thick] (6.9, 0.2) -- (5.2, 0.2);
      \node [fill, draw, circle, minimum width=3pt, inner sep=0pt, pin={[fill=white, outer sep=2pt]225:$\point{x}_8$}] at (6.9,0.2) {};
      \draw [black!30, thick] (6.9, 0.2) -- (6.9, 3.9);

      \node at (1.5, 1.75) {$\mathcal{O}_1$};
      \node at (3, 1.75) {$\mathcal{O}_2$};
      \node at (4.5, 1.75) {$\mathcal{O}_3$};
      \node at (6, 1.75) {$\mathcal{O}_4$};
    \end{tikzpicture}
\begin{tikzpicture}
\draw (0,0) rectangle (4, 4);

\filldraw[fill=black!40!white, draw=black](0.5, 3) rectangle (3.5, 3.5);
\filldraw[fill=black!40!white, draw=black](0.5, 1) rectangle (1, 3);
\filldraw[fill=black!40!white, draw=black](0.5, 0.5) rectangle (3.5, 1);
\filldraw[fill=black!40!white, draw=black](1.25, 1.25) rectangle (3.5, 1.5);
\filldraw[fill=black!40!white, draw=black](1.25, 2.5) rectangle (3.5, 2.75);
\filldraw[fill=black!40!white, draw=black](3.25, 1.5) rectangle (3.5, 2.5);
\filldraw[fill=black!40!white, draw=black](2, 1.65) rectangle (3, 1.85);
\filldraw[fill=black!40!white, draw=black](2, 2.15) rectangle (3, 2.3);
\filldraw[fill=black!40!white, draw=black](2, 1.85) rectangle (2.15, 2.15);

\node [fill, draw, circle, minimum width=3pt, inner sep=0pt, pin={[fill=white, outer sep=2pt]225:$\point{x}_s$}] at (0.1,0.1) {};
\draw [black!30, thick] (0.1, 0.1) -- (3.9, 0.1);
\node [fill, draw, circle, minimum width=3pt, inner sep=0pt, pin={[fill=white, outer sep=2pt]225:$\point{x}_1$}] at (3.9,0.1) {};

\draw [black!30, thick] (3.9, 0.1) -- (3.9, 2.85);
\node [fill, draw, circle, minimum width=3pt, inner sep=0pt, pin={[fill=white, outer sep=2pt]355:$\point{x}_2$}] at (3.9,2.85) {};
\draw [black!30, thick] (3.9, 2.85) -- (1.15, 2.85);
\node [fill, draw, circle, minimum width=3pt, inner sep=0pt, pin={[outer sep=-2pt]120:$\point{x}_3$}] at (1.15,2.85) {};

\draw [black!30, thick] (1.15, 1.6) -- (3.075, 1.6);
\node [fill, draw, circle, minimum width=3pt, inner sep=0pt, pin={[outer sep=-3pt]225:$\point{x}_4$}] at (1.15,1.6) {};

\draw [black!30, thick] (1.15, 1.6) -- (1.15, 2.85);
\node [fill, draw, circle, minimum width=3pt, inner sep=0pt, pin={[outer sep=-3pt]355:$\point{x}_5$}] at (3.075,1.6) {};

\draw [black!30, thick] (3.075, 1.6) -- (3.075, 2);
\node [fill, draw, circle, minimum width=3pt, inner sep=0pt, pin={[outer sep=-3pt]355:$\point{x}_6$}] at (3.075,2) {};

\draw [black!30, thick] (3.075, 2) -- (2.3, 2);
\node [fill, draw, circle, minimum width=3pt, inner sep=0pt, pin={[outer sep=-3pt]180:$\point{x}_t$}] at (2.3,2) {};
\end{tikzpicture}
 \begin{tikzpicture}
  \draw (0,0) rectangle (4, 4);

  \filldraw[fill=black!40!white, draw=black] (0.15, 1) rectangle(3.75, 0.25);
  \filldraw[fill=black!40!white, draw=black] (3, 3.95) rectangle(3.75, 1.05);

  \node [fill, draw, circle, minimum width=3pt, inner sep=0pt, pin={[fill=white, outer sep=2pt]180:$\point{x}_s$}] at (2.85,3.7) {};
  \node [fill, draw, circle, minimum width=3pt, inner sep=0pt, pin={[fill=white, outer sep=2pt]0:$\point{x}_t$}] at (3.85,3.7) {};

  \node at (2, .6) {$\mathcal{O}_1$};
  \node at (3.38, 2) {$\mathcal{O}_2$};
  \node at (0, -0.6) {};
  \node at (-1, 0) {};
 \end{tikzpicture}
\end{center}

\caption{a) Snake-shaped arena with four obstacles (left), b) Maze-shaped
  arena with three $C$-shaped patterns (middle) and c) modified L-shaped
  arena (right).}

\label{fig:modified_Lshaped}
\label{fig:maze-shaped}
\end{figure}
\begin{table}[t]
\begin{center}
\begin{tabular}{ | c | c | c | c | c | c |}
\hline
\multirow{2}{*}{\textbf{Dimension}} & \multirow{2}{*}{\textbf{Arena Size}} &
\multicolumn{2}{| c |}{~~~~~\textbf{OMPLRRT}~~~~~} & \multicolumn{2}{| c |}{~~~~~\textbf{BoundedMotionPlan}~~~~~} \\
\cline{3-6}
 & & Time(s) & Nodes & Time(s) & Witness Length \\

\hline
2 & 100 $\times$ 100 & 0.011 & 8 & 0.012 & 2 \\
\hline
2 & 1000 $\times$ 1000 & 0.076 & 245 & 0.012 & 2 \\
\hline
3 & 100 $\times$ 100 &  0.107 & 4836 & 0.183 & 2 \\
\hline
3 & 1000 $\times$ 1000 & 1.9 & 1800 & 0.19 & 2 \\
\hline
4 & 100 $\times$ 100 & 1.2 & 612 & 0.201 & 2 \\
\hline
4 & 1000 $\times$ 1000 & 94.39 & 2857 & 0.206 & 2 \\
\hline
5 & 100 $\times$ 100 & 3.12 & 778 & 2.69 & 2 \\
\hline
5 & 1000 $\times$ 1000 &  149.4 & 2079 & 2.68 & 2 \\
\hline
6 & 1000 $\times$ 1000 & 105 & 3822 & 15.3 & 2 \\
\hline
7 & 1000 $\times$ 1000 & 319.63 & 2639 & 190.3 & 2 \\
\hline
\end{tabular}
\end{center}
\caption{Summary of results for the $L$ shaped arena}
\label{ellShaped}
\end{table}
We considered the following microbenchmarks.
\begin{itemize}
\item \textbf{L-shaped arena.}
      This class of microbenchmarks contains  examples with hyper-rectangular
  workspace and certain ``L'' shaped obstacles as shown in
  Figure~\ref{fig:l-shaped}.
  The initial vertex is the lower left vertex of the square ($\point{x}_s$) and the
  target is the right upper vertex of the square ($\point{x}_t$).
  Our algorithm can give the solution to this problem with bound $B = 2$
  returning the sequence $\seq{\point{x}_1, \point{x}, \point{x}_t}$ as shown in the figure,
  while the \textsc{Rrt} algorithm in this case samples most of the points which lie
  on the other side of the obstacles and if the control modes are not in the
  direction of the line segments $\point{x}_1 \point{x}$ and $\point{x}\px_t$,
  then it grows in arbitrary directions and hits the obstacles a large number of
  times, leading to a large number of iterations slowing the growth.
  We experimented with L-shaped examples for dimensions ranging from $2$ to
  $7$. In most of the cases, we found that the performance of
  the \textsc{BoundedMotionPlan} algorithm was better than that of
  OMPLRRT. Another important point to note is that RRT or other simulation-based
  algorithms do not perform well as the input size increases, which can be
  clearly seen from the running times obtained on increasing arena
  sizes in Table~\ref{ellShaped}. Our algorithm worked better than RRT
  for higher dimensions ($\geq$ 3).

\item \textbf{Snake-shaped arena.}
  The name comes from the serpentine appearance of the safe sets in these arenas.
  The motivation to study these microbenchmarks comes from motion planning
  problems in regular environments.
  The arena has rectangular obstacles coming from the top and the
  bottom (as shown in Figure~\ref{fig:maze-shaped} for two dimensions)
  alternately.
  The starting point is the lower left vertex $\point{x}_s$ and the target point is
  $\point{x}_t$.
  A sample free-path through the arena is also shown in the figure.
  \textsc{Rrt} algorithm performs well for lower dimensions but fails to
  terminate for higher dimensions.
  The results for this class of obstacles are summarised in Table~\ref{snakeShaped}. Experiments
  were performed for up to 3 dimensions and 4 obstacles.

\item \textbf{Maze-shaped arena.}
  These benchmarks mimic the motion planning situations where the task of the
  robot is to navigate through a maze.
  We model a maze using finitely many concentric ``C''-shaped obstacles with
  different orientations as shown
  in Figure~\ref{fig:maze-shaped}.
  The task is to navigate from the lower left outer corner to the
  center point of the square.
  This kind of arena seems to be particularly challenging for the RRT algorithm
  and the growth of the tree seems to be quite slow.
  Also, the performance of our tool degrades as the bound increases due to a
  increase in the number of constraints, and hence, these examples
  require more time as compared to the other two microbenchmarks.
  However, as shown in Table~\ref{mazeShaped}, \textsc{OmplRrt} and
  \texttt{BoundedMotionPlan}
  perform almost equally well, with the latter being slightly better.
\item \textbf{Modified L-shaped obstacles.}
  These set of microbenchmarks contains a hyperrectangular workspace and 2
  hyperrectangular obstacles arranged in a ``L-shaped'' fashion as shown in
  Figure~\ref{fig:modified_Lshaped}. The initial vertex lies very close to one
  of the obstacles. The target vertex is the vertex very close to the start
  vertex but on the other side of the obstacle. Our algorithm can give the
  solution to this problem with bound $B = 3$ while \textsc{Rrt} algorithm
  spends time in sampling from the bigger obstacle-free part of the arena. The
  results are  summarised in Table~\ref{modifiedEll}.
\end{itemize}

\begin{table}[t]
\begin{center}
\begin{tabular}{ | c | c | c | c | c | c | c | c |}
\hline
\multirow{2}{*}{\textbf{Dim.}} & \multirow{2}{*}{\textbf{Arena Size}} & \multirow{2}{*}{\textbf{Obstacles}} & \multicolumn{3}{| c |}{\textbf{OMPLRRT}} & \multicolumn{2}{| c |}{\textbf{BoundedMotionPlan}} \\ \cline{4-8}
 & & & Time(s) & Nodes &  Nodes in Path & Time(s) & Witness Length \\
 \hline
 2 & 350 $\times$ 350 & 3 & 3.56 & 13142 & 72 & 2.54 & 4 \\
 \hline
 2 & 350 $\times$ 350 & 4 & 4.12 & 15432 & 96 & 4.23 & 5 \\
 \hline
 2 & 3500 $\times$ 3500 & 3 & 4.79 & 15423 & 83 & 2.57 & 4 \\
 \hline
 3 & 350 $\times$ 350 & 3 & 102.3 & 86314 & 67 & 96.43 & 4 \\
 \hline
 3 & 3500 $\times$ 3500 & 3 & 100.22 & 1013 & 27 & 96.42 & 4 \\
 \hline
\end{tabular}
\end{center}
\caption{Summary of results for the snake-shaped arena}
\label{snakeShaped}
\end{table}

\begin{table}[t]
\begin{center}
\begin{tabular}{ | c | c | c | c | c | c | c | c | }
\hline
\multirow{2}{*}{\textbf{Dim.}} & \multirow{2}{*}{\textbf{Arena Size}} & \multirow{2}{*}{\textbf{Obstacles}} & \multicolumn{3}{| c |}{\textbf{OMPLRRT}} & \multicolumn{2}{| c |}{\textbf{BoundedMotionPlan}} \\ \cline{4-8}
& & & Time(s) & Nodes &  Nodes in Path & Time(s) & Bound \\
\hline
2 & $600 \times 600$ & 2 & 1.8 & 9500 & 60 & 1.3 & 4 \\
\hline
2 & $6000 \times 6000$ & 3 & 23.5 & 11256 & 78 & 45.23 & 5 \\
\hline
3 & $600 \times 600$ & 2 & 132.6 & 90408 & 71 & 120.3 & 5 \\
\hline
3 & $6000 \times 6000$ & 3 & 1002.6 & 183412 & 93 & 953.4 & 5 \\
\hline
\end{tabular}
\end{center}
\caption{Summary of results for the maze-shaped arena}
\label{mazeShaped}
\end{table}

\begin{table}[h]
  \begin{center}
    \centering
\begin{tabular}{ | c | c | c | c | c | c | c | }
\hline
\textbf{Dimension } & \textbf{Arena Size} & \multicolumn{3}{| c |}{\textbf{OMPLRRT}} & \multicolumn{2}{| c |}{\textbf{BoundedMotionPlan}} \\
\hline
& & Time & Nodes &  Nodes in Path & Time & Bound \\
\hline
2 & $100 \times 100$ & 0.445 & 27387 & 40 & 0.126 & 3 \\
\hline
2 & $1000 \times 1000$ & 2.57 & 38612 & 47 & 0.132 & 3 \\
\hline
3 & $100 \times 100$ & 115.23 & 57645 & 71 & 92.1 & 3 \\
\hline
3 & $1000 \times 1000$ & 675.62 & 183412 & 93 & 95.23 & 3 \\
\hline
4 & $100 \times 100$ & 287.32 & 64230 & 65 & 283.23 & 3 \\
\hline
4 & $1000 \times 1000$ & 923.45 & 192453 & 78 & 292.53 & 3 \\
\hline
5 & $100 \times 100$ & 523.62 & 73422 & 69 & 534.45 & 3 \\
\hline
5 & $1000 \times 1000$ & 1043 & 223900 & 72 & 533.96 & 3\\
\hline
\end{tabular}
\end{center}
\caption{Summary of results for the modified L-shaped obstacles}
\label{modifiedEll}
\end{table}

The micro-benchmarks presented above involved the situations where
the target point is reachable from the source point.
It is interesting to see the performance of two algorithms in cases when there
is no path from the source to target point.
For the cases when an upper bound on cell-decomposition can be imposed,
our algorithm is capable of producing negative answer.
Table~\ref{negtab} summarizes the performance of \textsc{OmplRrt}
and \texttt{BoundedMotionPlan} for $L$-shaped arenas when the target
point is not reachable.  The timeout for
RRT was set to be 500 seconds, and it did not terminate until the timeout,
which is as expected. On the other hand, \textsc{BoundedMotionPlan} performed well, with running times close to those when the target point is reachable.
\begin{table}[t]
\begin{center}
\centering
\begin{tabular} { | c | c | c | c |}
\hline
\multirow{2}{*}{~~~~\textbf{Dimension}~~~~} & \multicolumn{2}{| c |}{~~~~~~~~~~\textbf{OMPLRRT}~~~~~~~~~} & {~~~~\textbf{BoundedMotionPlan}~~~~} \\ \cline{2-4}
& Time(s) & Nodes & Time(s) \\ \hline
2 & 500 (TO) & 5301778 & 0.0088 \\ \hline
3 & 500 (TO) & 7892122 & 0.032 \\ \hline
4 & 500 (TO) & 4325621 & 0.056 \\ \hline
5 & 500 (TO) & 5624609 & 2.73 \\ \hline
6 & 500 (TO) & 4992951 & 18.34 \\ \hline
7 & 500 (TO) & 3765123 & 213.23 \\ \hline

\end{tabular}
\end{center}
\caption{Summary of results for the unreachable L-shaped obstacles.}
\label{negtab}
\end{table}

\noindent\textbf{Discussion}.
Our implementation of \textsc{BoundedMotionPlan} even though
preliminary, compares favorably with a state-of-the-art implementation
of \textsc{Rrt}. \textsc{BoundedMotionPlan}, in addition, can naturally deal
with restrictions on the dynamics of the MMS, that is, with systems
such that the positive linear span of the mode vectors is not
$\mathbb R^n$.

A trend observed in our experiments is that if a large fraction of the
arena is covered by obstacles, then the probability of a randomly sampled
point lying in the obstacle region is high and this makes RRT ineffective in
this situation by wasting a lot of iterations.
Another trend is that as the arena size increases, it becomes more
difficult for RRT to navigate to the destination points even with higher values
of goal bias.

Our algorithm performs better in situations when it terminates early
(target reachable from source with shorter witnesses) while
the performance of our algorithm degrades as the bound or the
dimensions increases since the number of constraints introduced by the
Fourier-Motzkin like-procedure implemented in our algorithm grows
exponentially with the dimension exhibiting the curse of
dimensionality.

\section{Conclusion}
\label{sec:conclusion}
In this paper we studied the motion planning problem for constant-rate
multi-mode system with non-convex safety sets given as a convex set of
obstacles.
We showed that while the general problem is already undecidable in this simple
setting of linearly defined obstacles, decidability can be recovered by making
appropriate assumption on the obstacles.
Moreover, our algorithm performs satisfactorily when compared to well-known
algorithms for motion planning, and can easily be adapted to provide
semi-algorithms for motion-planning problems for objects with polyhedral
shapes.
While the algorithm is complete for classes of safety sets for which a
bound on the size of a cell cover can be effectively computed,
bounds based on cell decompositions of the safety set may be too large to
be of practical use.  This situation is akin to that encountered in
bounded model checking of finite-state systems, in which bounds based
on the radii of the the state graph are usually too large.  We are
therefore motivated to look at extensions of the algorithm that
incorporate practical termination checks.