\section{Quantified BMC for Hybrid Automata}
\seclabel{algorithm}

	%

	%

	%

	%

The idea of the quantified SMT-based BMC for hybrid automata presented in this paper was inspired from the compact QBF encodings for addressing the BMC problem of purely discrete systems~\cite{jussila2007compressing,janota2012solving, mangassarian2010tc}.
To construct a quantified formula $\Omega(k)$ for the BMC of $\H$ of length $k$, we introduce a {\em bit-vector} $\vec{t} = \tuple{t_1, t_2,...,t_{\ceil{\log_2 k}}}$ to index each iteration of the BMC. The next-state of each iteration is connected to the current-state of the next iteration using two multiplexers, where the vector $\vec{t}$ functions as common select lines. We do not describe those multiplexers here but refer to its similar presentation in~\cite{mangassarian2010tc}. Hence, depending on the truth assignment given to the vector $\vec{t}$, the single copy of a transition relation $T$ simulates different iteration of the BMC.
The QBMC formula is then given as:
\begin{align}
\Omega(k) \mathrel{\stackrel{\scriptscriptstyle\Delta}{=}} & \ \exists V_0, V_1,...,V_k,\delta \:\forall \vec{t} \:\exists V, V' \mid I(V_0) \wedge T(V,V') \ \wedge \nonumber\\
 & \bigwedge_{i = 0}^{k-1}{{t^{k}(i) \rightarrow [(V = V_i) \wedge (V' = V_{i+1})]}} \wedge (\bigvee_{i = 0}^{k}{P(V_i)}),
\eqlabel{bmc_quantifier}
\vspace{1em}
\end{align}
where we note that the existential $\delta$ encodes the real time elapse and would appear in the trajectories $\T$ of the disjunct $T = D \vee \T$.

In the prefix of $\Omega(k)$, the existential variables $V_i$ is understood to {\em dominate} the universal $\vec{t}$ to ensure state contiguity. Intuitively, if there exists a truth assignment to each existential variable $V_i$, then the quantified first order formulas in SMT will be satisfied for all universal variable assignments.
Here, the current state $q$ and the next state $q'$ under the transition relation $T(V, V')$ are connected to the current state and the next state for each particular iteration $t^{k}(i)$, which is associated with a truth assignment given to $\vec{t}$.
This allows the QBMC of hybrid automaton $\H$ to be compactly encoded using only a single copy of a transition relation with adding some state variable equalities at each time. Whereas, the quantifier-free encoding in \eqref{bmc_smt} requires $k$ copies of the transition relation $T$.
This advantage of non-coping transition relation encoding has been proved to significantly reduce the problem size of the QBF encoding in \cite{mangassarian2010tc}. Similarly, the proposed QBMC method also requires less memory usage compared to other quantifier-free SMT-based BMC approaches, that will be demonstrated in details later in \secref{experiment}.

To illustrate \eqref{bmc_quantifier}, we consider the QBMC of the hybrid automaton of~\egref{example} with $k = 3$ as follows:
\begin{align}
 \Omega(3) = &\ \exists V_0, V_1, V_2, V_3, \delta \forall t_1, t_2 \exists V, V' \mid I(V_0) \wedge T(V,V')\nonumber\\
	& \wedge \ \{\bar{t_1} \rightarrow [(V = V_0) \wedge (V' = V_1)]\}\nonumber\\
	& \wedge \ \{t_1\wedge \bar{t_2} \rightarrow [(V = V_1) \wedge (V' = V_2)]\}\nonumber\\
	& \wedge \ \{t_1 \wedge t_2 \rightarrow [(V = V_2) \ \wedge (V' = V_3)]\}\nonumber\\
	& \wedge \ (P(V_0) \ \vee P(V_1) \ \vee P(V_2) \ \vee P(V_3)),
\eqlabel{example_bmc_quantified}
\end{align}
where $V = V'$ is a shorthand indicating every variable $v \in V$ equals its corresponding counterpart $v' \in V$.
In~\eqref{example_bmc_quantified}, if the value of $t_1$ is $0$, then there is a continuous trajectory that evolves from the initial state $q_0$, where $q_0.\ell_0 = \ell\mathit{oc_{1}}$ and $\mathit{x}_0 = 0$, to the next state $q_1$, where $q_1.\ell_1 = \ell\mathit{oc_{1}}$ and $\mathit{x}_1 \leq 5$.
When $t_1 = 1$ and $t_2 = 0$, the system takes the discrete transition from the current state $q_1$ to the next state $q_2$, where $q_2.\ell_2 = \ell\mathit{oc_{2}}$ and the value of $\mathit{x}_2$ is not higher than 10.
At $k = 3$, both $t_1$, and $t_2$ are true, then $q_2$ becomes the current state, and $q_3$ is the next state, where $q_3.\ell_3 = \ell\mathit{oc_{1}}$, and $\mathit{x}_3 \leq 5$. The discrete transition taken from $q_2$ to $q_3$ when $\mathit{x} \geq 10$ will reset the value of $\mathit{x}$ to 0.

		%

		%

		%

If it terminates, an SMT solver supporting the combined theory of bitvectors and reals with quantifiers will return SAT for the QBMC formula if there exists an execution from an initial state to a bad state, i.e.,\xspace if a bad state is reachable.
Otherwise, if it terminates, it will return UNSAT if a bad state is not reachable in $k$ steps.
We note that the combination theory of linear real arithmetic with bitvectors is decidable, and Z3 is in essence a decision procedure for this theory.
For instance, the example from~\eqref{example_bmc_quantified} has the state $q$, where $q.\ell = \ell\mathit{oc_{2}}$, and $\mathit{x} < 2.5$ is unreachable.
Up to $k = 3$, if the system has any safety specification containing the state $q$, that means $q \models \bigvee_{i = 0}^{3}{P(\localvar{q}{i})}$, and an SMT solver will return SAT on checking the formula $\Omega(3)$.
Thus, we can assert that the system is unsafe for $k = 3$, which in this case, was just illustrating a reachability query.

\section{Conclusion and Future Works}
\seclabel{conclusion}
In this paper, we present a new SMT-based technique that encodes, in a quantified form, the BMC problem for rectangular hybrid systems which also subsumes this encoding for timed systems.
The preliminary results for the Fischer mutual exclusion protocol and Lynch-Shavit protocol indicate the capability of our method to solve the BMC problem for hybrid systems including more than thousand locations.
We compare the QBMC approach to the quantifier-free BMC approaches in the dReach tool that uses the dReal SMT solver, and the HyComp tool built on top of nuXmv that uses the MathSAT SMT solver. The experimental results demonstrate that our approach is competitive to these tools in terms of execution time and memory consumption.

\emph {Future works.} As solvers for fragments of many-sorted first-order logic such as LRA, NRA, etc., continue to improve, QBMC encodings such as the one described in this paper will become more effective, similar to how QBMC for discrete systems has been shown to be effective with QBF encodings~\cite{mangassarian2010tc}. In future, we plan to conduct additional experiments for other benchmarks to cover a wider range of applications, and compare the results to more tools and techniques, such as Uppaal and tools built on top of CVC4~\cite{DBLP:conf/cav/BarrettCDHJKRT11}. We intend to compare the proposed QBMC with IC3-based algorithms that might provide trade-offs between memory consumption and execution time. We will also investigate more general classes of hybrid automata whose dynamics are expressed by linear or polynomial differential equations.

\section{Experimental Results}
\seclabel{experiment}
\newcommand{\timeout}[0]{T/O\xspace}
\newcommand{\memout}[0]{M/O\xspace}
\newcommand{\nomem}[0]{N/A\xspace}
\newcolumntype{C}[1]{>{\centering\let\newline\\\arraybackslash\hspace{0pt}}m{#1}}
We implement the QBMC method described in \secref{algorithm} as a module within HyST~\cite{bak2015hscc}.
HyST takes as input a hybrid automaton model in an extended form of the SpaceEx XML format~\cite{frehse2011cav} (supporting e.g.,\xspace nonlinear functions instead of only affine ones). Then it will generate a Python script that includes the transition relations of a hybrid system expressed as quantified SMT formulas using the Z3 Python API.
We evaluate the proposed QBMC method on several instances of Fischer and Lynch-Shavit mutual exclusion protocols. We compare the results to that of dReach, which is a state-of-the-art BMC tool for nonlinear hybrid automata~\cite{gao2013cade}, and with that of HyComp using the MathSAT SMT solver~\cite{cimatti2015tacas} in terms of execution time and memory consumption.
We note that the comparison focuses only the BMC feature of dReach and HyComp, and all of the models of them were generated using HyST.
The experiments are performed on Intel I5 2.4GHz processor with 4GB RAM, executing the method described in this paper and dReach in a VirtualBox virtual machine running Ubuntu 64-bit.
Z3 version 4.3.2 was used in the evaluation.
We collect the execution times in second and the peak memory usages in MB for different examples. The preliminary implementation described in this paper, along with all the examples, is available online at: \url{https://github.com/LuanVietNguyen/QBMC}

\begin{table}[t!]
\setlength{\tabcolsep}{1.2em}
\renewcommand{\arraystretch}{2
\centering
\caption{The performance comparison between QBMC, HyComp and dReach in solving the BMC of \egref{example}. $k$ is a number of steps in the BMC computation. ``Time" and ``Mem" are the time and memory usages measured in second and MB, respectively.\vspace{2em}
}
\begin{tabular}{|c|c|c|c|c|c|c|}
	\hline
	\multirow{2}{*}{Tools} &
	\multicolumn{2}{c|}{k $\leq$ 32} &
	\multicolumn{2}{c|}{k $\leq$ 64} &
	\multicolumn{2}{c|}{k $\leq$ 128} \\
	\cline{2-7}
	& Time & Mem & Time &  Mem & Time &  Mem \\
	\hline

	QBMC\xspace & 0.81 & 17.3 & 3.22 & 27.7 & 5.36 & 41.2\\
	\hline

	dReach  & 82.6 & 106.7 & 1128.2 & 275.5 & 19896 & 812.6 \\
	\hline

	HyComp  & 0.4 & 98.1 & 0.6 & 105.8 & 1.62 & 128.7\\
	\hline
\end{tabular}
\tablabel{examples_table}
\end{table}

We first evaluate our QBMC encoding on the illustrative hybrid automata presented in~\egref{example}, and compare the results to those of dReach and HyComp.
The performances of those three different methods are shown in \tabref{examples_table}.
The constant values of the rectangular differential inclusion dynamics are given as: $a_1 = 0, b_1 = 1, a_2 = 0$, and $b_2 = 2$.
The set of bad state used in this experiment is given in \eqref{badset_ex}, where all states in this set are unreachable and the system is always safe.
For all of the values of $k$ up to 128, the BMC results of QBMC, HyComp and dReach are all UNSAT, illustrating the correctness of the BMC procedure.
The time and memory consumptions shown in~\tabref{examples_table} preliminarily indicate that our QBMC approach is capable of solving BMC faster than dReach, but slower than HyComp.
However, our approach is more scalable as it requires significantly less memory usage compared to dReach and HyComp.

\begin{figure}[t!]
	\vspace{2em}
	\centering
	\scriptsize

	\begin{tikzpicture}[-,>=stealth',shorten >=1pt,auto,node distance=6cm,main node/.style={circle,fill=black!20,draw}]
		\tikzset{every state/.style={minimum size=2cm}, font=\normalsize}

		\node[initial,state] (rem)      			{\makecell[c]{$\act{rem}$\\$\localvardot{x}{i} = 1$}};
		\node[state]		 (try) [right of=rem]	{\makecell[c]{$\act{try}$\\$\localvardot{x}{i} = 1$\\$\localvar{x}{i} \leq \Delta_1$}};
		\node[state]		 (wait) [below=25mm of try]	{\makecell[c]{$\act{wait}$\\$\localvardot{x}{i} = 1$}};
		\node[state]		 (cs) at (rem |- wait)
{\makecell[c]{$\act{cs}$\\$\localvardot{x}{i} = 1$}};
		%
		\path[->]			(rem)	edge   node {\makecell[c]{$g = \bot$\\$\localvar{x}{i} := 0$}} (try);
		\path[->]			(try)	edge   node {$g := i$; $\localvar{x}{i} := 0$} (wait);

		\path[->]			(wait)	edge[out=150,in=320]   node [above,xshift=10mm,yshift= -2mm] {\makecell[c]{$g \neq i \wedge \localvar{x}{i} \geq \Delta_2$\\$\localvar{x}{i} := 0$}} (rem);
		\path[->]			(wait)	edge   node {\makecell[c]{$g = i \wedge \localvar{x}{i} \geq \Delta_2$\\$\localvar{x}{i} := 0$}} (cs);
		\path[->]			(cs)	edge   node {$g := \bot$} (rem);
	\end{tikzpicture}

	\caption{Fischer's mutual exclusion algorithm for a process with identifier $i \in \{1, \ldots, N\}$. Here, $g$ is a global variable of type $\{\bot, 1, \ldots, N\}$, $\localvar{x}{i}$ is a local variable of type $\mathbb{R}$, and both $\Delta_1$ and $\Delta_2$ are constants of type $\mathbb{R}$.}%
	\figlabel{code:fischer}%
\end{figure}

\subsection{Fischer mutual exclusion protocol}
Next, we evaluate QBMC\xspace with several scenarios using the Fischer mutual exclusion protocol~\cite{johnson2012forte}.
Fischer mutual exclusion is a timed distributed algorithm that ensures a mutual exclusion safety property, namely that at most one process in a network of $N$ processes may enter a critical section simultaneously. \figref{code:fischer} shows the model of Fischer protocol in including four discrete locations $\act{Loc} \mathrel{\stackrel{\scriptscriptstyle\Delta}{=}} \{\act{rem}, \act{try}, \act{wait}, \act{cs}\}$, where $\Delta_1$ and $\Delta_2$ are two real timing parameters. Here, if $\Delta_1 < \Delta_2$ a mutual exclusion is guaranteed.
The set of bad states is defined by:
\begin{align*}
\phi \ \mathrel{\stackrel{\scriptscriptstyle\Delta}{=}} \ \neg \forall i, j \in \{1, \ldots, N\} \ | \ (i \neq j \wedge \ q_i = cs) \ \implies \ q_j \neq cs,
\end{align*}
where $q_i$ and $q_j$ are variables modeling the discrete location of the automata, $cs$ is the critical section location.
To evaluate QBMC\xspace, we perform the BMC for both of the safe and unsafe version of Fischer protocol. In the safe version, a state where the set of bad states $\phi$ is satisfied is not reachable, while in the unsafe one, a state where $\phi$ is satisfied is reachable.
We then also compare the performance of QBMC\xspace in solving the BMC of Fischer protocol with HyComp and dReach.

\begin{sidewaystable
\centering
\caption{The performance of the BMC of Fischer mutual exclusion protocol using QBMC\xspace, HyComp, and dReach.}  \vspace{2em}
\setlength{\tabcolsep}{0.8em}
{\renewcommand{\arraystretch}{1.5}
\begin{tabular}{|c|c|c|c|c|c|c|c|c|c|c|c|}
\hline
\multirow{2}{*}{Example} & \multirow{2}{*}{NoL} & \multirow{2}{*}{k ($\leq$) } & \multicolumn{3}{c|}{QBMC\xspace} & \multicolumn{3}{c|}{HyComp} & \multicolumn{3}{c|}{dReach} \\
\cline{4-12}
                         &                      &                    											& Time   & Mem   & Result   & Time   & Mem   & Result   & Time   & Mem   & Result   \\
\hline
\multirow{2}{*}{FU-2\xspace}        & \multirow{4}{*}{$4^2$}    & 8                 &  1.1      &   24.7    &    SAT      &  0.4      &   100.9    &    SAT      &   48.4     &   28.9    &  SAT        \\
\cline{3-12}
                         &                      											& 16                &  1.52      &  28.2     &   SAT       &   0.5     &  101.4     &     SAT      &  50.3      &  30.7     & SAT         \\
\cline{1-1}\cline{3-12}
\multirow{2}{*}{FS-2\xspace} % Taylor2Luan: probably this would be simpler with a \newcommand that takes an argument, e.g. \fischerunsafe{2}        &     & 8                  												&  1.6      &  25.2     &   UNSAT       & 0.5       & 101.4      &   UNSAT       &  64.1      &  120.8    &    UNSAT       \\
\cline{3-12}
                         &                      &16                 											&  6.4      &   30    &      UNSAT      & 2.8       & 107.3      &   UNSAT       &  \timeout      &  \nomem     &  $\times$        \\
\hline
\multirow{2}{*}{FU-3\xspace}        & \multirow{4}{*}{$4^3$}    & 8               &  6.9     &   48.7    &   UNSAT         &  2.1      & 131.8     &  UNSAT        &  270      &  214     &   UNSAT       \\
\cline{3-12}
                         &                      & 16                 											&  22.7     &  49.7     &   SAT        &  6.7      &  149.6     &    SAT       &    959.3     &  235.3      &     SAT      \\
\cline{1-1}\cline{3-12}
\multirow{2}{*}{FS-3\xspace}        &     & 8                  											&  8.3     &   48.7    &    UNSAT        &  2.2      & 131.8       &  UNSAT        &   \timeout       &  \nomem     &   $\times$     \\
\cline{3-12}
                         &                      & 16                 											&  52.4      &  52.4     &    UNSAT        &  55.8      &  214.4      & UNSAT         &       \timeout      &  \nomem     &  $\times$     \\
\hline
\multirow{2}{*}{FU-4\xspace}        & \multirow{4}{*}{$4^4$}    & 8                &  40.1      &  73.2     &   UNSAT         &  13.3      & 318.2      & UNSAT         &        \timeout      &  \nomem     &  $\times$        \\
\cline{3-12}
                         &                      & 16                 											&  119.1      &  156.2     &   UNSAT         &  569.4      &   895.4    &  UNSAT        &       \timeout      &  \nomem     &  $\times$         \\
\cline{1-1}\cline{3-12}
\multirow{2}{*}{FS-4\xspace}        &     & 8                  											&  76.1      &  74.1     &     UNSAT       &  9.9      &  319.1     &  UNSAT        &   \timeout      &  \nomem     &  $\times$         \\
\cline{3-12}
                         &                      & 16                 											&  \timeout      &  \nomem     &  $\times$        &   788     &  1010.4     &   UNSAT       &   \timeout      &  \nomem     &  $\times$         \\
\hline
\multirow{2}{*}{FU-5\xspace}        & \multirow{4}{*}{$4^5$}    & 8                &  288.8      &   249.9    &    UNSAT       &  109.1      &   1345.4    &    UNSAT      &   \timeout      &  \nomem     &  $\times$       \\
\cline{3-12}
                         &                      & 16                 											&  21456     &   473.8    &     UNSAT     &   \nomem      &    \memout    &    $\times$       &  \timeout      &  \nomem     &  $\times$       \\
\cline{1-1}\cline{3-12}
\multirow{2}{*}{FS-5\xspace}        &     & 8                  											&  344.4      &  254.4     &   UNSAT      &  172.4      &    1405.9   &   UNSAT       &    \timeout      &  \nomem     &  $\times$        \\
\cline{3-12}
                         &                      & 16                 											&  \timeout      &   \nomem     &   $\times$   & \nomem      &  \memout      &   $\times$             &    \timeout      &  \nomem     &  $\times$          \\
\hline
\end{tabular}
\tablabel{trials_table_2}
\end{sidewaystable}

\tabref{trials_table_2} shows the execution time and memory usage comparison among HyComp, dReach and QBMC\xspace for Fischer protocol with different numbers of processes, where NoL is the number of locations; FS\xspace, FU\xspace denote the safe and unsafe versions of Fischer protocol, respectively, and the number following the hyphen (-) describes a number of processes for each version.
For instance, FS-2\xspace} % Taylor2Luan: probably this would be simpler with a \newcommand that takes an argument, e.g. \fischerunsafe{2, FU-2\xspace are the safe and unsafe versions of the Fischer protocol with $2$ processes, respectively. We choose $\Delta_1 = 5$, $ \Delta_2 = 70$ for a safe version, and $\Delta_1 = 75$, $\Delta_2 = 70$ for an unsafe one.
In \tabref{trials_table_2}, \timeout means the computation time out ($\geq$ 12 hours), \memout represents that the peak memory usage is higher than 4GB, and \nomem denotes that the information of times or memory usages cannot be captured due to either \timeout or \memout. Also, $\times$ means that the BMC procedure cannot terminate.

\paragraph*{Compared to HyComp.} According to \tabref{trials_table_2}, we can see that HyComp is generally faster than QBMC\xspace, but it requires a higher memory consumption than QBMC\xspace.
For instance, up to $k = 8$, HyComp can address the BMC of the safe version of Fischer protocol with 5 processes in 172.4 seconds, which is approximately twice faster than QBMC\xspace (terminates after 344 seconds). However, HyComp consumes 1405.9 MB of memory, which is more than five times higher than QBMC (using only 254.4 MB).
Additionally, with $k \leq 16$, the BMC of the unsafe version of Fischer protocol with 5 processes cannot terminate in HyComp due to out of memory (requiring more than 4GB).
However, QBMC\xspace can solve it using less than 500 MB.
Hence, we can deduce that QBMC\xspace is superior than HyComp with respect to memory consumption.

\paragraph*{Compared to dReach.} Generally, \tabref{trials_table_2} also indicates that QBMC\xspace outperforms dReach in solving the BMC of Fischer protocol. As an example, with $k \leq 16$,  dReach solves the BMC of the unsafe version of Fischer protocol with 3 processes in 959.3 seconds using 235.3 MB of memory, while QBMC\xspace only terminates in 22.7 seconds ($\approx$ 40 time faster) using only 49.7 MB. Moreover, the BMC of both unsafe and safe versions of Fischer protocol with more than 3 processes is not able to terminate in dReach. Although dReach is capable to address the BMC of a wide range of nonlinear hybrid systems, handling scalability is not its strength.

Overall, QBMC\xspace has a competitive execution time and is more scalable to other state-of-the-art SMT solvers.
Due the state-space (and formula) explosion of BMC, the reduction of memory consumption is one of the major challenges to address.
Since QBMC\xspace requires a smaller amount of memory usage than other quantifier-free BMC approaches, it is effective in solving the BMC of large scale problems.
According to \tabref{trials_table_2}, the BMC of the unsafe version of 4-processes Fischer protocol can be checked completely using QBMC up to $k = 32$ with only 254.1 MB of memory consumption. This result indicates that QBMC\xspace is effective for bug detection.
However, as $k$ increases, the higher execution time and the larger memory usage are required for the quantified encoding of BMC due to the increasing number of all possible paths from an initial state in the set of initial states to a bad state that does not satisfy the set of safety specifications.

\subsection{Lynch-Shavit mutual exclusion protocol}
The Lynch-Shavit protocol is a modified version of Fischer protocol where the mutual exclusion property is time-independent\cite{lynch1992timing}. Intuitively, the protocol ensures that mutual exclusion is always satisfied even if the timing constraints are violated.
We first modeled the hybrid automata of Lynch-Shavit protocol~\cite{abdulla2004using} in an extended form of the SpaceEx XML format. Then, we used the HyST tool to translate it to other model formats (e.g., for HyComp and dReach), and create the QBMC encoding.
Each process of Lynch-Shavit protocol has 9 discrete locations, so the Lynch-Shavit protocol with 4 processes includes 6561 locations.
The set of bad states of Lynch-Shavit protocol is defined similar to Fischer protocol, where two processes may be in the critical section.

The performance analyzing the BMC of Lynch-Shavit protocol using QBMC\xspace and HyComp are shown in~\tabref{lynch_table}, in which the BMC results of QBMC and HyComp are both UNSAT. Due to scalability problem, the BMC of Lynch-Shavit protocol using dReach could not terminate correctly. Thus, we do not demonstrate the time and memory consumptions for the BMC of Lynch-Shavit protocol using dReach in~\tabref{lynch_table}. However, we still provide the model files in our preliminary implementation package for interested readers to investigate.
Again, we can see the trade-off between the two approaches.
HyComp is generally faster than QBMC\xspace, but requires a much higher memory usage.
As a result, the BMC of Lynch-Shavit protocol with 4 processes can be solved by QBMC\xspace up to $k = 16$ with consuming approximately 1GB memory, but cannot be solved in HyComp up to $k = 8$ due to out of memory.
Hence, that demonstrates the proposed QBMC approach is efficient and scalable in addressing the BMC of large hybrid systems.

\begin{table}[t!]
\setlength{\tabcolsep}{1.2em}
\renewcommand{\arraystretch}{2

	\centering

	\caption{The performance comparison between QBMC\xspace and HyComp in solving the BMC of Lynch-Shavit mutual exclusion protocol.
	}
	\vspace{2em}
	\begin{tabular}{|c|c|c|c|c|c|c|c|c|}
		\hline
		\multirow{2}{*}{Tools} &
		\multirow{2}{*}{NoL} &
		\multicolumn{2}{c|}{k $\leq$ 4} &
		\multicolumn{2}{c|}{k $\leq$ 8} &
		\multicolumn{2}{c|}{k $\leq$ 16} \\
		\cline{3-8}
		& &Time & Mem & Time &  Mem & Time &  Mem\\
		\hline
		\multirow{3}{*}{QBMC\xspace}
		& $9^2$ & 3.7 & 52.2 & 5.1 & 52.3 & 25.9 & 52.7\\
		\cline{2-8}
		& $9^3$ & 15.5 & 65.6 & 31.3 & 87.5 & 1091.5 & 144.5\\
		\cline{2-8}
		& $9^4$ & 256.1 & 702.8 & 1062.1 & 708.9 & 43178 & 1196.2\\
		\hline
		\multirow{3}{*}{HyComp}
		& $9^2$ & 0.8 & 121.9 & 1.33 & 132.8 & 9.5 & 170.5\\
		\cline{2-8}
		& $9^3$ & 2.7 & 307.9 & 12.81 & 380.8 & 192.8 & 771.4\\
		\cline{2-8}
		& $9^4$ & 63.9 & 2655.4 & \nomem & \memout & \nomem & \memout\\
		\hline
	\end{tabular}

	\tablabel{lynch_table}

\end{table}

\section{Introduction}
\seclabel{intro}
Boolean Satisfiability (SAT) is the canonical NP-complete problem and is to determine if a given Boolean formula is satisfiable, i.e.,\xspace check if there exists an assignment of values to variables where the formula is true.
A Boolean formula is given in Conjunctive Normal Form (CNF), that is, a conjunction of clauses, each of which is a disjunction of literals.
Satisfiability Modulo Theories (SMT) is a generalization of SAT, where literals are interpreted with respect to a background theory (e.g.,\xspace linear real arithmetic, nonlinear integer arithmetic, bit-vectors, etc.).

SMT-based techniques have been developed to formally verify hybrid systems~\cite{eggers2008atva,gao2013fmcad,johnson2014formats,cimatti2015tacas,shmarov2017smt,bae2017modular}.
Typically, these SMT-based methods are used in bounded model checking (BMC), which is to check for a transition system $A$ and a specification $P$ whether $I(V_0) \wedge \bigwedge_{i=0}^{k-1} T(V_i,V_{i+1}) \wedge (\bigvee_{i=0}^{k} P(V_i))$ is satisfiable.
Here, $I(V_0)$ encodes an initial set of states over a set of variables $V_0$, $T(V_i,V_{i+1})$ represents the transition relation from iteration $i$ to $i+1$ over sets of variables $V_i$ and $V_{i+1}$, and $P(V_i)$ encodes the specification at step $i$.
An SMT solver either returns SAT if there is a sequence of states leading the transition system $A$ from a state in $I$ to a state in $P$, or UNSAT if a state in $P$ can not be reached in $k$ steps.
In principle, BMC is complete as it can prove that no bad state can be reached if a large enough bound k is used. However, as k increases, SMT-based BMC may require excessive memory due to the underlying complex combination theories in a SMT solver. To increase scalability, it is essential to reduce the memory usage while performing SMT-based BMC for large hybrid systems.

Hybrid automaton is a modeling formalism used to verify dynamical systems including both continuous states and dynamics as well as discrete states and transitions.
Examples of systems naturally modeled by hybrid automata arise in the interaction of physical plants and software controllers in real-time systems and cyber-physical systems (CPS).
In essence, hybrid automata augment finite state machines with a set of real-valued variables that evolve continuously over intervals of real time.
In hybrid automata, a transition relation $T = D \cup \T$ encodes both discrete transitions $D$ and continuous trajectories $\T$ over intervals of real-time.
Rectangular hybrid automata (RHA) are a special class of hybrid automata with continuous dynamics described by rectangular differential inclusions and where all other quantities (guard conditions, invariants, resets, etc.) of the automata are linear inequalities over constants~\cite{henzinger1996lics,johnson2012forte}.
Sets of states, as well as discrete transitions and continuous trajectories of RHA, can be symbolically represented by SMT formulas over real and Boolean variables.

Depending on the underlying logics supported, SMT solvers may or may not support quantifiers.
While quantifiers may make the language more expressive, they often increase the complexity of computations like checking satisfiability and may also lead to undecidability.
Techniques allowing quantifiers, such as in quantified Boolean formula (QBF) solvers, have been developed for the BMC of purely discrete systems, such as finite state machines~\cite{jussila2007compressing,mangassarian2010tc}.
However, to the best of our knowledge, there has been no effort to develop quantified BMC (QBMC) methods for timed or hybrid automata, which we develop in this paper.
Of course, this is partially because the underlying SMT solver requires support for complex combination theories and efficient algorithms to check quantified formulas, which until recently, were either not available or not scalable.

In this paper, we propose a SMT-based verification technique that encodes the BMC problem for timed automata and RHA in a quantified form, which we call QBMC (quantified bounded model checking).
As the logic encoding requires some finite sort for the discrete states (such as a enumerated type or bit-vectors) and reals for the continuous states and trajectories, we uses LRABV (linear real arithmetic with bit-vectors) for encoding QBMC for timed automata and RHA. We note that general hybrid automata would need NRABV (nonlinear real arithmetic with bit-vectors) or beyond, such as those whose solutions involve special (transcendental) functions like sin, cos, exp, etc.
While none of these logics are officially supported in the SMT-LIB2 standard as of the time of this writing~\cite{BarFTRR17}, several solvers do have unofficial support for this combination theory, such as the latest versions of Z3, which is the SMT solver used in this paper~\cite{demoura2008tacas}.

For implementation, we take hybrid automata in the SpaceEx format~\cite{frehse2011cav}, which are then translated to the QBMC encoding sequence proposed in this paper using the HyST model transformation tool~\cite{bak2015hscc}. HyST allows the same model to be analyzed simultaneously in several hybrid systems analysis tools, so it is convenient to compare the performance of our proposed approach with existing works.
The QBMC is performed by querying the Z3 SMT solver via its Python API and using its quantifier-handling procedures~\cite{demoura2008tacas}.
We present preliminary experimental results where the QBMC approach and Z3 perform competitively to (a) the dReach tool that performs BMC using an SMT check by querying the dReal $\delta$-decidable SMT solver~\cite{gao2012lics,gao2013fmcad,kong2015dreach}, and (b) the HyComp tool built on top of nuXmv that uses the MathSAT SMT solver~\cite{cimatti2015hycomp}.
The examples include standard ones such as Fischer and Lynch-Shavit mutual exclusion, as well as an illustrative example to describe the encoding.
Overall, the main contribution of this paper is the first encoding of BMC as a quantified problem for RHA that has less memory requirement and competitive execution time when compared to state-of-the-art SMT solvers.
Our results subsume the case for timed automata, as RHA are more expressive than timed automata, and we note this is also the first QBMC approach for timed automata.

\section*{Acknowledgements}
\vspace{-1em}
The material presented in this paper is based upon work supported by the National Science Foundation (NSF) through grant numbers 1918450 and 2028001. Any opinions, findings, and conclusions or recommendations expressed in this paper are those of the authors and do not necessarily reflect the views of NSF. This paper is based on an earlier workshop paper that did not appear in an archival proceedings: Luan Viet Nguyen, Djordje Maksimovic, Taylor T. Johnson, Andreas Veneris, "Quantified Bounded Model Checking for Rectangular Hybrid Automata," which was presented at the 9th International Workshop on Constraints in Formal Verification (CFV 2015), Austin, Texas, November 2015, colocated with the 34th IEEE/ACM International Conference on Computer-Aided Design (ICCAD 2015).

\bibliographystyle{eptcs}

\section{Preliminaries}

\defV{V}

In this section, we introduce the preliminaries that are needed for this work. We first define a hybrid automaton model, discuss its semantics and safety specification. Then we present the traditional encoding (quantifier-free) of the BMC for hybrid automata.

\subsection{Hybrid Automata}
\noindent
{\bf Syntax.} A hybrid automaton is essentially a finite state machine extended with a set of real-valued variables that evolve continuously over intervals of real-time.
The syntactic structure of a hybrid automaton is formally defined as follows.
A hybrid automaton $\H$ is a tuple, $\H$ $\mathrel{\stackrel{\scriptscriptstyle\Delta}{=}}$ $\langle$${\mathit{Loc}}$, ${\mathit{Var}}$, ${\mathit{Inv}}$, ${\mathit{Flow}}$, ${\mathit{Trans}}$, ${\mathit{Init}}$$\rangle$, with the components as follows.
\begin{itemize}
\item ${\mathit{Loc}}$ is a finite set of discrete locations.
\item ${\mathit{Var}}$ is a finite set of $n$ continuous, real-valued variables, and $\Q \mathrel{\stackrel{\scriptscriptstyle\Delta}{=}} {\mathit{Loc}} \times \mathbb{R}^n$ is the state-space.
\item ${\mathit{Inv}}$ is a finite set of invariants, one for each discrete location, and for each location $\ell \in {\mathit{Loc}}$, ${\mathit{Inv}}(\ell) \subseteq \mathbb{R}^n$.
\item ${\mathit{Flow}}$ is a finite set of ordinary differential inclusions, one for each continuous variable $x \in {\mathit{Var}}$, and ${\mathit{Flow}}(\ell, x) \subseteq \mathbb{R}^n$ describes the continuous dynamics in each location $\ell \in {\mathit{Loc}}$.
\item ${\mathit{Trans}}$ is a finite set of transitions between locations.
Each transition is a tuple $\tau \mathrel{\stackrel{\scriptscriptstyle\Delta}{=}} \tuple{\ell, \ell', g, u}$, where $\ell$ is a source location and $\ell'$ is a target location that may be taken when a guard condition $g$ is satisfied, and the post-state is updated by an update map $u$.
\item ${\mathit{Init}}$ is an initial condition, which consists of a set of locations in ${\mathit{Loc}}$ and a formula over ${\mathit{Var}}$, so that ${\mathit{Init}} \subseteq \Q$.
\end{itemize}

For RHA, all the expressions appearing in invariants, guards, and updates must be boolean combinations of constant inequalities, and the flows are rectangular differential inclusions e.g., $\dot{x} \in [a, b]$ for $a \leq b$.
Timed automata is the important subclass of RHA in which every continuous variable is a precise clock e.g., $\dot{x} = 1$.
We use the dot (.) notation to refer to different components of tuples e.g.,\xspace $\H.{\mathit{Inv}}$ refers to the invariants of automaton $\H$ and $\tau.g$ refers to the guard of a transition $\tau$.
If clear from context, we drop $\H$ and $\tau$ and refer to the individual components of the tuple.

\vspace{1em}
\noindent
{\bf Semantics.}
The semantics of a hybrid automaton $\H$ are defined in terms of executions, which are sequences of states.
A \emph{state} $q$ of $\H$ is a tuple $q \mathrel{\stackrel{\scriptscriptstyle\Delta}{=}} \tuple{\ell, \mathit{v}}$, where $\ell \in {\mathit{Loc}}$ is a location, and $\mathit{v} \in \mathbb{R}^n$ is a valuation of all variables in ${\mathit{Var}}$.
Formally, for a set of variables ${\mathit{Var}}$, a \emph{valuation} is a function mapping each $x \in {\mathit{Var}}$ to a point in its type---here, $\mathbb{R}$.
The state-space $\Q$ is the set of all states of $\H$.
Updates of states are described by a transition relation $T \subseteq \Q \times \Q$.
For a transition $\tuple{q, q'} \in T$ where $q \mathrel{\stackrel{\scriptscriptstyle\Delta}{=}} \tuple{\ell, \mathit{v}}$ and $q' \mathrel{\stackrel{\scriptscriptstyle\Delta}{=}} \tuple{\ell', \mathit{v}'}$, we denote  $q \rightarrow q' \in T$ as the transition between the current state $q$ and the next state $q'$.
The transition relation $T$ is partitioned into disjoint sets of discrete transitions and continuous trajectories that respectively describe the discrete and continuous behaviors of the automaton.
Thus, $T \mathrel{\stackrel{\scriptscriptstyle\Delta}{=}} D \cup \T$, where:
\begin{inparaenum}[(a)]
	\item $D \subseteq \Q \times \Q$ is the set of discrete transitions that describe instantaneous updates of state,
	\item $\T \subseteq \Q \times \Q$ is the set of continuous trajectories that describe updates of state over real time intervals.
\end{inparaenum}

\vspace{1em}
\emph{Discrete transitions}.
A discrete transition $q \rightarrow q' \in D$ models an instantaneous update from the current state $q$ to the next state $q'$.
There is a discrete transition $q \rightarrow q' \in D$ if and only if (iff):
$\exists \tau \in {\mathit{Trans}} : q.\mathit{v} \models \operatorname{\mathsf {act}}{\tau}.g \wedge q'.\mathit{v}' \models \operatorname{\mathsf {act}}{\tau}.u$, where $\operatorname{\mathsf {act}}{\tau}.g$, and $\operatorname{\mathsf {act}}{\tau}.u$ are the guard condition and the update map of the discrete transition $\tau$, respectively.

\vspace{1em}
\emph{Continuous trajectories}.
A continuous trajectory $q \rightarrow q' \in \T$  models the update of state $q$ to $q'$ over an interval of real time.
The set-valued function $\Delta$ returns a set of states and is defined as: $\Delta(q.\ell, q.v, x, t) \in q.v.x + \int_{\delta = t_0}^{t} {\mathit{f}}(q.\ell, x) d\delta$, where ${\mathit{f}} \in {\mathit{Flow}}$ is a flow rate---a formula over ${\mathit{Var}} \cup \dot{{\mathit{Var}}}$ that describes the evolution of a real variables $x \in {\mathit{Var}}$ over a real time interval $J = [t_0, t]$--- and $q.v.x$ is the value of continuous variable $x$ of the state $q$ at $t = t_0$.
Then, there is a trajectory $q \rightarrow q' \in \T$ iff:
$\exists t_{\alpha} \in \nnReal \ \forall t_{\beta} \in \nnReal \ \exists \ell \in {\mathit{Loc}} \ : $ $t_{\beta} \leq t_{\alpha} \ \wedge \ \Delta(q.\ell, q.v, {\mathit{Var}}, t_{\beta}) \models {\mathit{Inv}}(\ell) \ \wedge \ q'.\mathit{v}'.{\mathit{Var}} \in \Delta(q.\ell, q.v, {\mathit{Var}}, t_{\alpha})$.
For each real variable $x$, $q.\mathit{v}.x$ must evolve to the valuation $q'.\mathit{v}'.x$ at precisely time $t_{\alpha}$ and corresponding to the flow rate of $x$ in location $\ell$.
Additionally, all states along the trajectory must satisfy the invariant ${\mathit{Inv}}(\ell)$ i.e.,\xspace at every point in the interval of real time $t_{\beta} \leq t_{\alpha}$.

\vspace{1em}
\emph{Executions}.
An \emph{execution} of $\H$ is a sequence $\pi \mathrel{\stackrel{\scriptscriptstyle\Delta}{=}} q_0 \rightarrow q_1 \rightarrow q_2 \rightarrow ...$, such that:
\begin{inparaenum}[(a)]
	\item $q_0 \in {\mathit{Init}}$ is an initial state, and
	\item either $\localvar{q}{i} \rightarrow \localvar{q}{i + 1} \in D$ is a discrete transition or $\localvar{q}{i} \rightarrow \localvar{q}{i + 1} \in \T$ is a continuous trajectory for each consecutive pair of states in the sequence $\pi$.
\end{inparaenum}
A state $\localvar{q}{k} \mathrel{\stackrel{\scriptscriptstyle\Delta}{=}} \tuple{\localvar{\ell}{k},\localvar{\mathit{v}}{k}}$ is \emph{reachable} from initial state $q_0 \mathrel{\stackrel{\scriptscriptstyle\Delta}{=}} \tuple{\localvar{\ell}{0},\localvar{\mathit{v}}{0}} \in {\mathit{Init}}$ iff there exists a finite execution $\pi \mathrel{\stackrel{\scriptscriptstyle\Delta}{=}} q_0 \rightarrow q_1 \rightarrow ... \rightarrow \localvar{q}{k}$.

\vspace{1em}
\noindent
{\bf Safety specifications.}
In this paper, we develop the QBMC procedure to check whether safety properties of hybrid automata are satisfied up to iteration $k$.
A \emph{safety specification} $\phi$ is a formula over ${\mathit{Loc}}$ and ${\mathit{Var}}$ that describes a set of states $\ds{\phi} \subseteq \Q$, where $\ds{\cdot}$ is the set of states satisfying $\phi$.
For an automaton $\H$ and a safety specification $\phi$, the automaton satisfies the specification, denoted $\H \models \phi$, iff for every execution $\pi$, for every state $q_0, q_1, \ldots, q_k$ in the execution $\pi$, we have $\pi.q_k \in \ds{\phi}$.
If $\H \models \phi$ for every $i \in \{0, \ldots, k\}$, then the system is safe up to iteration $k$.
If $\H \models \phi$ for any $k$, then the system is safe.
For a safety specification $\phi$, a \emph{counterexample} is an execution $\pi$ where some state $q \in \pi$ violates $\phi$, i.e.,\xspace $q \not\models \phi$, or equivalently, $q \notin \ds{\phi}$.

\subsection{Quantifier-Free BMC for Hybrid Automata}

BMC has been used widely in verification and falsification of safety and liveness properties of various classes of systems, from finite state machines to hybrid automata.
The key idea is to search for a counterexample execution whose length is bounded by a number of steps $k$.
In other words, BMC will explore all executions from any initial state of a system to detect whether there is a way to reach a bad state that violates a given property (or to find a loop in the case of liveness).
Then this path is considered as a counterexample to the property that may help the user to debug the system.
For finite state systems, BMC can be encoded as a propositional formula to be checked as satisfiable or unsatisfiable using a Boolean SAT solver.
For hybrid automata, BMC can be encoded as a formula over reals and finite sorts (such as Booleans, bit-vectors, or enumerated types).
In this paper, we focus only on hybrid automata with rectangular differential inclusion dynamics ($\dot{x} \in [a, b]$ for real constants $a \leq b$), and for this class of automata, the formulas are within linear real arithmetic (LRA).
Before presenting the QBMC approach in \secref{algorithm}, which is the main contribution of this paper, we first illustrate BMC for hybrid automata using the traditional quantifier-free encoding.

Let $P$ be a set of given specifications of the hybrid automata, the BMC problem will determine whether a specification $P(\localvar{q}{k}) \in P$ is safe after $k$ steps, and it is:
\begin{equation}

\Phi(k) \mathrel{\stackrel{\scriptscriptstyle\Delta}{=}} I(V_0) \wedge \bigwedge_{i = 0}^{k-1}{\localvar{T}{i}(V_i, V_{i+1})} \wedge (\bigvee_{i = 0}^{k}{P(V_i)}),
\eqlabel{bmc_smt}
\end{equation}
where $V_i$ corresponds to the set of variables ${\mathit{Var}}$ of the automaton $\H$ appropriately renamed.
In~\eqref{bmc_smt}, $I(V_0)$ encodes the initial set of states, $\localvar{T}{i}(V_i, V_{i+1})$ encodes the transition between consecutive pairs of sets of states, and $P(V_i)$ is a safety specification at iteration $i$.
We note that the sets of variables $V_i$ for each iteration $i$ are implicitly existentially quantified, e.g.,\xspace we could equivalently prefix $\exists V_0, V_1, \ldots, V_k$.
We drop the sets of variables for a shorter notation, e.g.,\xspace~\eqref{bmc_smt} is equivalent to $I_0 \wedge \bigwedge_{i = 0}^{k-1}{\localvar{T}{i}} \wedge (\bigvee_{i = 0}^{k}{P_i})$.

\begin{figure}[t!]%

	\centering%
	\begin{adjustbox}{max size={0.75\columnwidth}{0.75\textheight}}%
	\begin{tikzpicture}[-,>=stealth',shorten >=1pt,auto,node distance=8cm,main node/.style={circle,fill=black!20,draw}]
		\tikzset{every state/.style={minimum size=0.85cm}}
		\node[initial,state] (one) {\makecell[c]{$\ell\mathit{oc_{1}}$\\$\mathit{x} \leq 5$\\$\dot{\mathit{x}} \in [a_1,b_1]$}} ;
		\node[state]		 (two) [right of=one]	{\makecell[c]{$\ell\mathit{oc_{2}}$\\$\mathit{x} \leq 10$\\$\dot{\mathit{x}} \in [a_2,b_2]$}};
		\path[->]			(one)	edge[bend left] node{\makecell[c]{$\mathit{x} \geq 2.5$}} (two);
		\path[->]			(two)	edge[bend left] node{\makecell[c]{$\mathit{x} \geq 10$\\$\mathit{x} := 0$}} (one);
	\end{tikzpicture}%
	\end{adjustbox}%

	\caption{The hybrid automaton $\H$ for~\egref{example}.}
	\figlabel{example_hybrid_automaton}%

\end{figure}%
\eglabel{example}%

\vspace{1em}
\noindent
{\bf Illustrative Example.}
Consider the hybrid automaton $\H$ shown in~\figref{example_hybrid_automaton}.
Assume that the automaton starts at location $\ell\mathit{oc_{1}}$, and the initial value of $\mathit{x}$ is $0$.
Two intervals $[a_1, b_1]$ and $[a_2, b_2]$ describe the rectangular differential inclusions for locations $\ell\mathit{oc_{1}}$, and $\ell\mathit{oc_{2}}$, respectively.
This automaton would be a \emph{timed automaton} if all of the constants values are equal, i.e.,\xspace $a_1 = b_1 = a_2 = b_2$.
This automaton would be a \emph{multi-rate timed automaton} if $a_1 = b_1$ and $a_2 = b_2$ but possibly $a_1 \neq a_2$.
Otherwise, this automaton is a \emph{rectangular hybrid automaton}.
Suppose that $a_1 = 1$, $b_1 = 2$, $a_2 = 3$, and $b_2 = 4$.
We introduce $k + 1$ copies $x_0, x_1,...,x_k$ and $\ell_0, \ell_1,...,\ell_k$, where the variable $x_i$ gives the value of the variable $x$, and $\ell_i$ indicates the location at the state $\localvar{q}{i}$, representing the $i^{th}$ step of the BMC computation for the automaton shown in~\figref{example_hybrid_automaton}. The set of bad states are defined by:

\begin{equation}
P \mathrel{\stackrel{\scriptscriptstyle\Delta}{=}} \ \bigvee_{i = 0}^{k} \localvar{q}{i}.\ell_i = \ell\mathit{oc_{2}} \ \wedge \ \mathit{x} < 2.5.
\eqlabel{badset_ex}
\end{equation}

The BMC computation of $\H$ for each $k$ up to $2$ can be encoded as:
\begin{itemize}
	\item $k = 0$: $I_0$ := $(\ell_0 = \ell\mathit{oc_{1}} \wedge \mathit{x}_0 = 0)$;
	%

	\item $k = 1$ ($D_0$): $(\ell_0 = \ell\mathit{oc_{1}} \wedge \ell_1 = \ell\mathit{oc_{2}} \wedge x_0 \leq 5 \wedge x_0 \geq 2.5  \wedge x_1 = x_0)$,

  \item $k = 1$ ($\T_0$): $(\ell_0 = \ell\mathit{oc_{1}} \implies (\ell_1 = \ell_0 \wedge x_0 + a_1 \delta \leq x_1 \wedge x_1 \leq x_0 + b_1 \delta \wedge x_1 \leq 5))$,
  %

	\item $k = 2$ ($D_1$): $(\ell_1 = \ell\mathit{oc_{1}} \wedge \ell_2 = \ell\mathit{oc_{2}} \wedge x_1 \leq 5 \wedge x_1 \geq 2.5  \wedge x_2 = x_1)$,

  \item $k = 2$ ($\T_1$): $(\ell_1 = \ell\mathit{oc_{1}} \implies (\ell_2 = \ell_1 \wedge x_1 + a_1 \delta \leq x_2 \wedge x_2 \leq x_1 + b_1 \delta \wedge x_2 \leq 5))$,
	%
	%
	%

		%

		%

		%

\end{itemize}
where $\delta$ is a fresh, real constant. In general, a universally quantified assertion that the invariant is satisfied for every real time along the trajectory from time $t_0$ to time $t_0 + \delta$, although this is unnecessary for rectangular differential inclusions with linear guards and invariants for convexity reasons~\cite{johnson2012forte,cimatti2015tacas}, which makes this assertion fall into the combination theory of linear real arithmetic with bit-vectors (or some finite sort to encode the locations).
We split the discrete transitions and trajectories for clarity, but the entire formula to be checked for iteration $k = 1$ would just be the disjunction of these conjuncted with the formula representing $k = 0$ and the bad set of states, i.e., $I_0 \wedge (D_0 \vee \T_0) \wedge P$.
For $k = 2$, this full formula would be $I_0 \wedge (D_0 \vee \T_0) \wedge (D_1 \vee \T_1) \wedge P$.

For $k=1$, we dropped the obviously infeasible transition from $\ell\mathit{oc_{2}}$ to $\ell\mathit{oc_{1}}$ from $D_0$, which would be found as being unsatisfiable since $\ell_0 \neq \ell\mathit{oc_{2}}$.
However, the transition from $\ell\mathit{oc_{1}}$ to $\ell\mathit{oc_{2}}$ also cannot occur since $x_0 = 0$, but $x_0 \not\geq 2.5$, so that this part is unsatisfiable and no discrete transitions may be taken from the set of initial states.
We also dropped the continuous dynamics for $\ell\mathit{oc_{2}}$ from $\T_0$ since this would also be infeasible since $\ell_0 \neq \ell\mathit{oc_{2}}$.
However, real time may elapse, and as encoded, would correspond to any choice of time $\delta$ such that $x_1 \in [a_1 \delta, b_1 \delta]$ and $x_1 \leq 5$.
Since $a_1 = 1$ and $b_1 = 2$, at most between $2.5$ and $5$ seconds of real time could elapse, and either case would yield $x_1 \in [0, 5]$.

For $k = 2$, we also dropped the infeasible transition and trajectory for clarity.
In this case, the transition from $\ell\mathit{oc_{1}}$ to $\ell\mathit{oc_{2}}$ is enabled since $x_1 \in [0, 5]$, so the update to $\ell\mathit{oc_{2}}$ may occur.
However, now the continuous trajectory would be infeasible since $x_1$ could already be $5$ and the invariant requires $x_2 \leq 5$, so no real-time $\delta > 0$ may elapse, as otherwise $x_1 + a_1 \delta \leq 5$ is unsatisfiable for $x_1 = 5$.
So, the only state update would be to $\ell\mathit{oc_{2}}$ owing to the discrete transition.

\section{#1}%

\newcommand{\pow}[1]{{\bf P}(#1)}
\newcommand{\inverse}[1]{#1^{-1}}
\newcommand{\range}[1]{\ms{range{(#1)}}}
\newcommand{\domain}[1]{{\it dom}(#1)}
\newcommand{\type}[1]{\ms{type{(#1)}}}
\newcommand{\dtype}[1]{\ms{dtype{(#1)}}}
\newcommand{\mathrel{\lceil}}{\mathrel{\lceil}}
\newcommand{\matrel{\lceil}}{\matrel{\lceil}}
\newcommand{\mathrel{\downarrow}}{\mathrel{\downarrow}}
\newcommand{\point}[1]{\wp(#1)}

\def{\cal A}{{\cal A}}
\def{\cal B}{{\cal B}}
\def\C{{\cal C}}
\def\D{{\cal D}}
\def\E{{\cal E}}
\def\mathit{false}{{\cal F}}
\def\G{{\cal G}}
\def\H{{\cal H}}
\def{\ensuremath{\cap}}{{\cal I}}
\def\K{{\cal K}}
\def\L{{\cal L}}
\def\M{{\cal M}}
\def\O{{\cal O}}
\def\P{{\cal P}}
\def\Q{{\cal Q}}
\def\R{{\cal R}}
\def\S{{\cal S}}
\def\mathit{true}{{\cal T}}
\def\V{{\cal V}}
\def\U{{\cal U}}
\def\X{{\cal X}}
\def\Y{{\cal Y}}

\newcommand{\col}[1]{\relax\ifmmode \mathscr #1\else $\mathscr #1$\fi}

\def\col{S}{\col{S}}

\definecolor{HIOAcolor}{rgb}{0.776,0.22,0.07}
\newcommand{\textcolor{HIOAcolor}{\tt HIOA\hspace{3pt}}}{\textcolor{HIOAcolor}{\tt HIOA\hspace{3pt}}}
\newcommand{\textcolor{HIOAcolor}{\tt PVS\hspace{3pt}}}{\textcolor{HIOAcolor}{\tt PVS\hspace{3pt}}}
\newcommand{\textcolor{HIOAcolor}{\tt PVS\hspace{1pt}}}{\textcolor{HIOAcolor}{\tt PVS\hspace{1pt}}}
\newcommand{\textcolor{HIOAcolor}{\tt HIOA\hspace{6pt}}}{\textcolor{HIOAcolor}{\tt HIOA\hspace{6pt}}}
\newcommand{\textcolor{HIOAcolor}{\tt HIOA}}{\textcolor{HIOAcolor}{\tt HIOA}}
\newcommand{\lessgtr}{\lessgtr}

\newcommand{\SC}[2]{\relax\ifmmode {\tt Scount}(#1,#2) \else ${\tt Scount}(#1,#2)$\fi}
\newcommand{\SCM}[2]{\relax\ifmmode {\tt Smin}(#1,#2) \else ${\tt Smin}(#1,#2)$\fi}
\newcommand{\Aut}[1]{\relax\ifmmode {\tt Aut}(#1) \else ${\tt Aut}(#1)$\fi}

\newcommand{\auto}[1]{{\operatorname{\mathsf{#1}}}}
\newcommand{\operatorname{\mathsf {act}}}[1]{{\operatorname{\mathsf{#1}}}}
\newcommand{\smodel}[1]{{\operatorname{\mathsf{#1}}}}
\newcommand{\pvstheory}[1]{{\operatorname{\mathit{#1}}}}

\newcommand{{\bf automaton}}{{\bf automaton}}
\newcommand{{\bf asserts}}{{\bf asserts}}
\newcommand{{\bf assumes}}{{\bf assumes}}
\newcommand{{\bf backward}}{{\bf backward}}
\newcommand{{\bf by}}{{\bf by}}
\newcommand{{\bf case}}{{\bf case}}
\newcommand{{\bf  choose}}{{\bf  choose}}
\newcommand{{\bf components}}{{\bf components}}
\newcommand{{\bf const}}{{\bf const}}
\newcommand{{\bf converts}}{{\bf converts}}
\newcommand{{\bf do}}{{\bf do}}
\newcommand{\mathit{Eff}}{{\bf eff}}
\newcommand{{\bf else}}{{\bf else}}
\newcommand{{\bf elseif}}{{\bf elseif}}
\newcommand{{\bf enumeration}}{{\bf enumeration}}
\newcommand{{\bf ensuring}}{{\bf ensuring}}
\newcommand{{\bf exempting}}{{\bf exempting}}
\newcommand{{\bf fi}}{{\bf fi}}
\newcommand{{\bf for}}{{\bf for}}
\newcommand{{\bf forward}}{{\bf forward}}
\newcommand{{\bf freely}}{{\bf freely}}
\newcommand{{\bf from}}{{\bf from}}
\newcommand{{\bf generated}}{{\bf generated}}
\newcommand{{\bf local}}{{\bf local}}
\newcommand{{\bf hidden}}{{\bf hidden}}
\newcommand{{\bf if}}{{\bf if}}
\newcommand{{\bf in}}{{\bf in}}
\newcommand{{\bf implies}}{{\bf implies}}
\newcommand{{\bf includes}}{{\bf includes}}
\newcommand{{\bf introduces}}{{\bf introduces}}
\newcommand{{\bf input}}{{\bf input}}
\newcommand{{\bf kind}}{{\bf kind}}
\newcommand{{\bf initially}}{{\bf initially}}
\newcommand{{\bf internal}}{{\bf internal}}
\newcommand{{\bf invariant}}{{\bf invariant}}
\newcommand{{\bf od}}{{\bf od}}
\newcommand{{\bf of}}{{\bf of}}
\newcommand{{\bf output}}{{\bf output}}
\newcommand{{\bf partitioned}}{{\bf partitioned}}
\newcommand{\mathit{Pre}}{{\bf pre}}
\newcommand{{\bf id}}{{\bf id}}
\newcommand{{\bf stop}}{{\bf stop}}
\newcommand{{\bf flowrate}}{{\bf flowrate}}
\newcommand{\LFlowrate}{{\bf lflowrate}}
\newcommand{\UFlowrate}{{\bf uflowrate}}
\newcommand{\operatorname{\mathsf {act}}{Init}}{{\bf Init}}
\newcommand{\operatorname{\mathsf {act}}{V}}{{\bf var}}
\newcommand{{\bf signature}}{{\bf signature}}
\newcommand{{\bf simulation}}{{\bf simulation}}
\newcommand{{\bf sort}}{{\bf sort}}
\newcommand{{\bf states}}{{\bf states}}
\newcommand{{\bf tasks}}{{\bf tasks}}
\newcommand{{\bf then}}{{\bf then}}
\newcommand{{\bf to}}{{\bf to}}
\newcommand{{\bf trait}}{{\bf trait}}
\newcommand{{\bf traits}}{{\bf traits}}
\newcommand{{\bf transitions}}{{\bf transitions}}
\newcommand{{\bf tuple}}{{\bf tuple}}
\newcommand{{\bf type}}{{\bf type}}
\newcommand{{\bf union}}{{\bf union}}
\newcommand{{\bf uses}}{{\bf uses}}
\newcommand{{\bf where}}{{\bf where}}
\newcommand{{\bf while}}{{\bf while}}
\newcommand{{\bf with}}{{\bf with}}

\newcommand{\vspace{0.1in}}{\vspace{0.1in}}
\newcommand{\hspace{-0.1in}}{\hspace{-0.1in}}

\newcommand{\mathrel{\stackrel{\scriptscriptstyle\Delta}{=}}}{\mathrel{\stackrel{\scriptscriptstyle\Delta}{=}}}

\newcommand{\seclabel}[1]{\label{sec:#1}}
\newcommand{\secref}[1]{Section~\ref{sec:#1}}
\newcommand{\secreftwo}[2]{Sections~\ref{sec:#1}~and~\ref{sec:#2}}
\newcommand{\secrefthree}[3]{Sections~\ref{sec:#1},~\ref{sec:#2},~and~\ref{sec:#3}}
\newcommand{\chlabel}[1]{\label{ch:#1}}
\newcommand{\chref}[1]{Chapter~\ref{ch:#1}}
\newcommand{\chreftwo}[2]{Chapters~\ref{ch:#1}~and~\ref{ch:#2}}
\newcommand{\chrefthree}[3]{Chapters~\ref{ch:#1},~\ref{ch:#2},~and~\ref{ch:#3}}
\newcommand{\chreffour}[4]{Chapters~\ref{ch:#1},~\ref{ch:#2},~\ref{ch:#3},~and~\ref{ch:#4}}
\newcommand{\figlabel}[1]{\label{fig:#1}}
\newcommand{\figref}[1]{Figure~\ref{fig:#1}}
\newcommand{\figreftwo}[2]{Figures~\ref{fig:#1}~and~\ref{fig:#2}}
\newcommand{\figrefs}[2]{Figures~\ref{fig:#1}~and~\ref{fig:#2}}
\newcommand{\figrefthree}[3]{Figures~\ref{fig:#1},~\ref{fig:#2},~and~\ref{fig:#3}}
\newcommand{\figreffour}[4]{Figures~\ref{fig:#1},~\ref{fig:#2},~\ref{fig:#3},~and~\ref{fig:#4}}
\newcommand{\tablabel}[1]{\label{tab:#1}}
\newcommand{\tabref}[1]{Table~\ref{tab:#1}}
\newcommand{\tabreftwo}[2]{Tables~\ref{tab:#1},~and~\ref{tab:#2}}
\newcommand{\tabrefthree}[3]{Tables~\ref{tab:#1},~\ref{tab:#2},~and~\ref{tab:#3}}
\newcommand{\applabel}[1]{\label{app:#1}}
\newcommand{\appref}[1]{Appendix~\ref{app:#1}}
\newcommand{\lnlabel}[1]{\label{line:#1}}
\newcommand{\lnrngref}[2]{lines~\ref{line:#1}--\ref{line:#2}\xspace}
\newcommand{\lnref}[1]{line~\ref{line:#1}\xspace}
\newcommand{\lnrefthru}[2]{lines~\ref{line:#1}~through~\ref{line:#2}\xspace}
\newcommand{\lnreftwo}[2]{lines~\ref{line:#1}~and~\ref{line:#2}\xspace}
\newcommand{\lnrefthree}[3]{lines~\ref{line:#1},~\ref{line:#2},~and~\ref{line:#3}\xspace}
\newcommand{\lnreffour}[4]{lines~\ref{line:#1},~\ref{line:#2},~\ref{line:#3},~and~\ref{line:#4}\xspace}
\newcommand{\lnreffive}[5]{lines~\ref{line:#1},~\ref{line:#2},~\ref{line:#3},~\ref{line:#4},~and~\ref{line:#5}\xspace}

\newcommand{\thmref}[1]{Theorem~\ref{thm:#1}\xspace}
\newcommand{\thmlabel}[1]{\label{thm:#1}}
\newcommand{\assref}[1]{Assumption~\ref{ass:#1}\xspace}
\newcommand{\asslabel}[1]{\label{ass:#1}}
\newcommand{\invlabel}[1]{\label{inv:#1}}
\newcommand{\invref}[1]{Invariant~\ref{inv:#1}}
\newcommand{\lemlabel}[1]{\label{lem:#1}}
\newcommand{\lemref}[1]{Lemma~\ref{lem:#1}}
\newcommand{\celabel}[1]{\label{ce:#1}}
\newcommand{\ceref}[1]{Counterexample~\ref{ce:#1}}

\newcommand{\proplabel}[1]{\label{prop:#1}}
\newcommand{\propref}[1]{Proposition~\ref{prop:#1}}
\newcommand{\deflabel}[1]{\label{def:#1}}
\newcommand{\defref}[1]{Definition~\ref{def:#1}}

\newcommand{\eqlabel}[1]{\label{eq:#1}}
\renewcommand{\eqref}[1]{Equation~\ref{eq:#1}}
\newcommand{\eqrefthru}[2]{Equations~\ref{eq:#1}~through~\ref{eq:#2}}
\newcommand{\eqreftwo}[2]{Equations~\ref{eq:#1}~and~\ref{eq:#2}}
\newcommand{\eqrefthree}[3]{Equations~\ref{eq:#1},~\ref{eq:#2},~and~\ref{eq:#3}}

\newcommand{\enumref}[1]{\ref{#1}}

\newcommand{\remove}[1]{}
\newcommand{\salg}[1]{\relax\ifmmode {\mathcal F}_{#1}\else ${\mathcal F}_{#1}$\fi}
\newcommand{\msp}[1]{\relax\ifmmode (#1, \salg{#1}) \else $(#1, \salg{#1})$\fi}
\newcommand{\msprod}[2]{\relax\ifmmode ( #1 \times #2, \salg{#1} \otimes \salg{#2}) \else $(#1 \times #2, \salg{#1} \otimes \salg{#2})$\fi}
\newcommand{\dist}[1]{\relax\ifmmode {\mathcal P}\msp{#1}
  \else ${\mathcal P}\msp{#1}$\fi}
\newcommand{\subdist}[1]{\relax\ifmmode {\mathcal S}{\mathcal P}\msp{#1}
  \else ${\mathcal S}{\mathcal P}\msp{#1}$\fi}
\newcommand{\disc}[1]{\relax\ifmmode {\sf Disc}(#1)
  \else ${\sf Disc}(#1)$\fi}

\newcommand{\Trajeq}{\relax\ifmmode {\mathcal R}_\mathit{true} \else ${\mathcal R}_\mathit{true}$\fi}
\newcommand{\Acteq}{\relax\ifmmode {\mathcal R}_A \else ${\mathcal R}_A$\fi}
\newcommand{\noop}{\relax\ifmmode \lambda \else $\lambda$\fi}
\newcommand{\close}[1]{\relax\ifmmode \overline{#1} \else $\overline{#1}$\fi}

\newcommand{\mathop{\mathsf {c}}}{\mathop{\mathsf {c}}}
\newcommand{\mathop{\mathsf {full}}}{\mathop{\mathsf {full}}}
\newcommand{\mathop{\mathsf {fstate}}}{\mathop{\mathsf {fstate}}}
\newcommand{\mathop{\mathsf {lstate}}}{\mathop{\mathsf {lstate}}}
\newcommand{\mathop{\mathsf {ltime}}}{\mathop{\mathsf {ltime}}}
\newcommand{\mathop{\mathsf {tdist}}}{\mathop{\mathsf {tdist}}}
\newcommand{\mathop{\mathsf {extbeh}}}{\mathop{\mathsf {extbeh}}}
\newcommand{\mathop{\mathsf {apply}}}[2]{\mathop{\mathsf {apply}({#1},{#2})}}
\newcommand{\mathop{\mathsf {supp}}}{\mathop{\mathsf {supp}}}
\newcommand{\mathrel{R}}{\mathrel{R}}
\newcommand{C}{C}
\newcommand{\mathord{\mathsf {flatten}}}{\mathord{\mathsf {flatten}}}
\newcommand{\mathord{\mathsf {Disc}}}{\mathord{\mathsf {Disc}}}
\newcommand{\lift}[1]{\mathrel{{\mathcal L}(#1)}}
\newcommand{\expansion}[1]{\mathrel{{\mathcal E}(#1)}}

\newcommand{\operatorname{\mathsf {SubDisc}}}{\operatorname{\mathsf {SubDisc}}}
\newcommand{\operatorname{\mathsf {tran}}}{\operatorname{\mathsf {tran}}}

\renewcommand{{\exec{}}}{{\operatorname{\mathsf {Execs}}}}
\newcommand{{\operatorname{\mathsf {Frags}}}}{{\operatorname{\mathsf {Frags}}}}

\newcommand{{\operatorname{\mathsf {trace}}}}{{\operatorname{\mathsf {trace}}}}

\newcommand{{\operatorname{\mathsf {finite}}}}{{\operatorname{\mathsf {finite}}}}
\newcommand{{\operatorname{\mathsf {hide}}}}{{\operatorname{\mathsf {hide}}}}

\newcommand{{\operatorname{\mathsf {Early}}}}{{\operatorname{\mathsf {Early}}}}
\newcommand{{\operatorname{\mathsf {Late}}}}{{\operatorname{\mathsf {Late}}}}
\newcommand{{\operatorname{\mathsf {Toss}}}}{{\operatorname{\mathsf {Toss}}}}

\newcommand{:=}{:=}

\newcommand{{\operatorname{\mathsf {counter}}}}{{\operatorname{\mathsf {counter}}}}
\newcommand{{\operatorname{\mathsf {chosen}}}}{{\operatorname{\mathsf {chosen}}}}

\newcommand{{\operatorname{\mathsf {random}}}}{{\operatorname{\mathsf {random}}}}
\newcommand{{\operatorname{\mathsf {unif}}}}{{\operatorname{\mathsf {unif}}}}

\newcommand{i.e.,\xspace}{i.e.,\xspace}
\newcommand{I.e.,\xspace}{I.e.,\xspace}

\newcommand{e.g.,\xspace}{e.g.,\xspace}
\newcommand{E.g.,\xspace}{E.g.,\xspace}

\newcommand{\mybox}[3]{
  \framebox[#1][l]
  {
    \parbox{#2}
    {
      #3
    }
  }
}

\newcommand{\two}[4]{
  \parbox{.95\columnwidth}{\vspace{1pt} \vfill
    \parbox[t]{#1\columnwidth}{#3}%
    \parbox[t]{#2\columnwidth}{#4}%
  }}

\newcommand{\twosep}[4]{
  \parbox{\columnwidth}{\vspace{1pt} \vfill
    \parbox[t]{#1\columnwidth}{#3}%
   	\vrule width 0.2pt
    \parbox[t]{#2\columnwidth}{#4}%
  }}

\newcommand{\eqntwo}[4]{
  \parbox{\columnwidth}{\vspace{1pt} \vfill
    \parbox[t]{#1\columnwidth}{$ #3 $}
    \parbox[t]{#2\columnwidth}{$ #4 $}
  }}

\newcommand{\three}[6]{\vspace{1pt} \vfill
        \parbox{\columnwidth}{%
        \parbox[t]{#1\columnwidth}{#4}%
        \parbox[t]{#2\columnwidth}{#5}%
        \parbox[t]{#3\columnwidth}{#6}%
      }}

\newcommand{\tup}[1]
           {
             \relax\ifmmode
             \langle #1 \rangle
             \else $\langle$ #1 $\rangle$ \fi
           }

\newcommand{\lit}[1]{ \relax\ifmmode
                \mathord{\mathcode`\-="702D\sf #1\mathcode`\-="2200}
                \else {\it #1} \fi }

\newcommand{\scriptsize}{\scriptsize}

\newcommand{\footnotesize}{\footnotesize}

\lstdefinelanguage{ioa}{
  basicstyle=\scriptsize,
  keywordstyle=\bf \scriptsize,
  identifierstyle=\it \scriptsize,
  emphstyle=\tt \scriptsize,
  mathescape=true,
  tabsize=20,
  sensitive=false,
  columns=fullflexible,
  keepspaces=false,
  flexiblecolumns=true,
  basewidth=0.05em,
  escapeinside={(*@}{@*)},
  moredelim=[il][\rm]{//},
  moredelim=[is][\sf \scriptsize]{!}{!},
  moredelim=[is][\bf \scriptsize]{*}{*},
  keywords={automaton,and,
  	 choose,const,continue, components,
  	 discrete, do,
  	 eff, Eff, external,else, elseif, evolve, end,
  	 fi,for, forward, from,
  	 hidden,
  	 in,input,internal,if,invariant, initially, imports,
     let,
     or, output, operators, od, of,
     pre, Pre,
     return,
     such,satisfies, stop, signature, simulation,
     trajectories,trajdef, transitions, that,then, type, types, to, tasks,
     variables, vocabulary,
     when,where, with,while},
  emph={set, seq, tuple, map, array, enumeration},
   literate=
        {(}{{$($}}1
        {)}{{$)$}}1

        {\\in}{{$\in\ $}}1
        {\\preceq}{{$\preceq\ $}}1
        {\\subset}{{$\subset\ $}}1
        {\\subseteq}{{$\subseteq\ $}}1
        {\\supset}{{$\supset\ $}}1
        {\\supseteq}{{$\supseteq\ $}}1
        {\\forall}{{$\forall$}}1
        {\\le}{{$\le\ $}}1
        {\\ge}{{$\ge\ $}}1
        {\\gets}{{$\gets\ $}}1
        {\\cup}{{$\cup\ $}}1
        {\\cap}{{$\cap\ $}}1
        {\\langle}{{$\langle$}}1
        {\\rangle}{{$\rangle$}}1
        {\\exists}{{$\exists\ $}}1
        {\\bot}{{$\bot$}}1
        {\\rip}{{$\rip$}}1
        {\\emptyset}{{$\emptyset$}}1
        {\\notin}{{$\notin\ $}}1
        {\\not\\exists}{{$\not\exists\ $}}1
        {\\ne}{{$\ne\ $}}1
        {\\to}{{$\to\ $}}1
        {\\implies}{{$\implies\ $}}1

        {<}{{$<\ $}}1
        {>}{{$>\ $}}1
        {=}{{$=\ $}}1
        {~}{{$\neg\ $}}1
        {|}{{$\mid$}}1
        {'}{{$^\prime$}}1

        {\{\cal A}}{{$\forall\ $}}1
        {\\E}{{$\exists\ $}}1
        {\\nE}{{$\nexists\ $}}1
        {\\/}{{$\vee\,$}}1
        {\\vee}{{$\vee\,$}}1
        {/\\}{{$\wedge\,$}}1
        {\\wedge}{{$\wedge\,$}}1
        {=>}{{$\Rightarrow\ $}}1
        {->}{{$\rightarrow\ $}}1
        {<=}{{$\Leftarrow\ $}}1
        {<-}{{$\leftarrow\ $}}1
        {~=}{{$\neq\ $}}1
        {\\U}{{$\cup\ $}}1
        {\{\ensuremath{\cap}}}{{$\cap\ $}}1
        {|-}{{$\vdash\ $}}1
        {-|}{{$\dashv\ $}}1
        {<<}{{$\ll\ $}}2
        {>>}{{$\gg\ $}}2
        {||}{{$\|$}}1
        {[}{{$[$}}1
        {]}{{$\,]$}}1
        {[[}{{$\langle$}}1
        {]]]}{{$]\rangle$}}1
        {]]}{{$\rangle$}}1
        {<=>}{{$\Leftrightarrow\ $}}2
        {<->}{{$\leftrightarrow\ $}}2
        {(+)}{{$\oplus\ $}}1
        {(-)}{{$\ominus\ $}}1
        {_i}{{$_{i}$}}1
        {_j}{{$_{j}$}}1
        {_{i,j}}{{$_{i,j}$}}3
        {_{j,i}}{{$_{j,i}$}}3
        {_0}{{$_0$}}1
        {_1}{{$_1$}}1
        {_2}{{$_2$}}1
        {_n}{{$_n$}}1
        {_p}{{$_p$}}1
        {_k}{{$_n$}}1
        {-}{{$\ms{-}$}}1
        {@}{{}}0
        {\\delta}{{$\delta$}}1
        {\\R}{{$\R$}}1
        {\\Rplus}{{$\Rplus$}}1
        {\\act{N}}{{$\act{N}$}}1
        {\\times}{{$\times\ $}}1
        {\\tau}{{$\tau$}}1
        {\\alpha}{{$\alpha$}}1
        {\\beta}{{$\beta$}}1
        {\\gamma}{{$\gamma$}}1
        {\\ell}{{$\ell\ $}}1
        {--}{{$-\ $}}1
        {\\TT}{{\hspace{1.5em}}}3
      }

\lstdefinelanguage{ioaNums}[]{ioa}
{
  numbers=left,
  numberstyle=\tiny,
  stepnumber=2,
  numbersep=4pt
}

\lstdefinelanguage{ioaNumsRight}[]{ioa}
{
  numbers=right,
  numberstyle=\tiny,
  stepnumber=2,
  numbersep=4pt
}

\newcommand{\lstinline[language=IOA]}{\lstinline[language=IOA]}

\lstnewenvironment{IOA}%
  {\lstset{language=IOA}}
  {}

\lstnewenvironment{IOANums}%
  {
  \if@firstcolumn
    \lstset{language=IOA, numbers=left, firstnumber=auto}
  \else
    \lstset{language=IOA, numbers=right, firstnumber=auto}
  \fi
  }
  {}

\lstnewenvironment{IOANumsRight}%
  {
    \lstset{language=IOA, numbers=right, firstnumber=auto}
  }
  {}

\newcommand{\figioa}[5]{
  \begin{figure}[#1]
      \hrule \mathit{false}
      {\scriptsize \bf #2}
      \lstinputlisting[language=ioaLang]{#5}
      \mathit{false} \hrule \mathit{false}
      \caption{#3}
      \label{fig: #4}
  \end{figure}
}

\newcommand{\linefigioa}[9]{

}

\newcommand{\twofigioa}[8]{
  \begin{figure}[#1]
    \hrule \mathit{false}
    {\scriptsize \bf #2} \\
    \two{#5}{#6}
    {
      \lstinputlisting[language=ioaLang]{#7}
    }
    {
      \lstinputlisting[language=ioaLang]{#8}
    }
    \mathit{false} \hrule \mathit{false}
    \caption{#3}
    \label{fig: #4}
  \end{figure}
}

\lstdefinelanguage{ioaLang}{%
  basicstyle=\ttfamily\small,
  keywordstyle=\rmfamily\bfseries\small,
  identifierstyle=\small,
  keywords={assumes,automaton,axioms,backward,bounds,by,case,choose,components,const,d,det,discrete,do,eff,else,elseif,ensuring,enumeration,evolve,fi,fire,follow,for,forward,from,hidden,if,in,%
    input,initially,internal,invariant,let, local,od,of,output,pre,schedule,signature,so,%
    simulation,states,variables, tasks, stop,tasks,that,then,to,trajdef,trajectory,trajectories,transitions,tuple,type,union,urgent,uses,when,where,while,yield},
  literate=

        {\\in}{{$\in$}}1
        {\\preceq}{{$\preceq$}}1
        {\\subset}{{$\subset$}}1
        {\\subseteq}{{$\subseteq$}}1
        {\\supset}{{$\supset$}}1
        {\\supseteq}{{$\supseteq$}}1
        {\\rho}{{$\rho$}}1
        {\\infty}{{$\infty$}}1

        {<}{{$<$}}1
        {>}{{$>$}}1
        {=}{{$=$}}1
        {~}{{$\neg$}}1
        {|}{{$\mid$}}1
        {'}{{$^\prime$}}1

        {\{\cal A}}{{$\forall$}}1 {\\E}{{$\exists$}}1
        {\\/}{{$\vee$}}1 {/\\}{{$\wedge$}}1
        {=>}{{$\Rightarrow$}}1
        {->}{{$\rightarrow$}}1
        {<=}{{$\leq$}}1 {>=}{{$\geq$}}1 {~=}{{$\neq$}}1
        {\\U}{{$\cup$}}1 {\{\ensuremath{\cap}}}{{$\cap$}}1
        {|-}{{$\vdash$}}1 {-|}{{$\dashv$}}1
        {<<}{{$\ll$}}2 {>>}{{$\gg$}}2
        {||}{{$\|$}}1

        {<=>}{{$\Leftrightarrow$}}2
        {<->}{{$\leftrightarrow$}}2
        {(+)}{{$\oplus$}}1
        {(-)}{{$\ominus$}}1
}

\lstdefinelanguage{bigIOALang}{%
  basicstyle=\ttfamily,
  keywordstyle=\rmfamily\bfseries,
  identifierstyle=,
  keywords={assumes,automaton,axioms,backward,by,case,choose,components,const,%
    d,det,discrete,do,eff,else,elseif,ensuring,enumeration,evolve,fi,for,forward,from,hidden,if,in%
    input,initially,internal,invariant,local,od,of,output,pre,schedule,signature,so,%
    tasks, simulation,states,stop,tasks,that,then,to,trajdef,trajectories,transitions,tuple,type,union,urgent,uses,when,where,yield},
  literate=

        {\\in}{{$\in$}}1
        {\\preceq}{{$\preceq$}}1
        {\\subset}{{$\subset$}}1
        {\\subseteq}{{$\subseteq$}}1
        {\\supset}{{$\supset$}}1
        {\\supseteq}{{$\supseteq$}}1

        {<}{{$<$}}1
        {>}{{$>$}}1
        {=}{{$=$}}1
        {~}{{$\neg$}}1
        {|}{{$\mid$}}1
        {'}{{$^\prime$}}1

        {\{\cal A}}{{$\forall$}}1 {\\E}{{$\exists$}}1
        {\\/}{{$\vee$}}1 {/\\}{{$\wedge$}}1
        {=>}{{$\Rightarrow$}}1
        {->}{{$\rightarrow$}}1
        {<=}{{$\leq$}}1 {>=}{{$\geq$}}1 {~=}{{$\neq$}}1
        {\\U}{{$\cup$}}1 {\{\ensuremath{\cap}}}{{$\cap$}}1
        {|-}{{$\vdash$}}1 {-|}{{$\dashv$}}1
        {<<}{{$\ll$}}2 {>>}{{$\gg$}}2
        {||}{{$\|$}}1

        {<=>}{{$\Leftrightarrow$}}2
        {<->}{{$\leftrightarrow$}}2
        {(+)}{{$\oplus$}}1
        {(-)}{{$\ominus$}}1
}

\lstnewenvironment{BigIOA}%
  {\lstset{language=bigIOALang,basicstyle=\ttfamily}
   \csname lst@SetFirstLabel\endcsname}
  {\csname lst@SaveFirstLabel\endcsname\vspace{-4pt}\noindent}

\lstnewenvironment{SmallIOA}%
  {\lstset{language=ioaLang,basicstyle=\ttfamily\scriptsize}
   \csname lst@SetFirstLabel\endcsname}

  {\csname lst@SaveFirstLabel\endcsname\noindent}

\newcommand{\mathit{true}}{\mathit{true}}
\newcommand{\mathit{false}}{\mathit{false}}

\newcommand{{\operatorname{\texttt{Bool}}}}{{\operatorname{\texttt{Bool}}}}
\newcommand{{\operatorname{\texttt{Char}}}}{{\operatorname{\texttt{Char}}}}
\newcommand{{\operatorname{\texttt{Int}}}}{{\operatorname{\texttt{Int}}}}
\newcommand{{\operatorname{\texttt{Nat}}}}{{\operatorname{\texttt{Nat}}}}
\newcommand{{\operatorname{\texttt{AugmentedReal}}}}{{\operatorname{\texttt{AugmentedReal}}}}
\newcommand{{\operatorname{\texttt{String}}}}{{\operatorname{\texttt{String}}}}
\newcommand{{\operatorname{\texttt{Discrete}}}}{{\operatorname{\texttt{Discrete}}}}

\newcommand{\Rightarrow}{\Rightarrow}
\newcommand{\Leftrightarrow}{\Leftrightarrow}

\newlength{\bracklen}
\newcommand{\sem}[1]{\settowidth{\bracklen}{[}
     [\hspace{-0.5\bracklen}[#1]\hspace{-0.5\bracklen}]}

\newcommand{1}{1}
\renewcommand{\arraystretch}{1}

\newcommand{\mathcal{S}}{\mathcal{S}}
\newcommand{\mathcal{V}}{\mathcal{V}}

\newcommand{\mathcal{V}_\mathit{spec}}{\mathcal{V}_\mathit{spec}}
\newcommand{\mathcal{V}_\mathit{A}}{\mathcal{V}_\mathit{A}}
\newcommand{\mathcal{V}_\mathit{sigs}}{\mathcal{V}_\mathit{sigs}}
\newcommand{\mathcal{V}_\mathit{sorts}}{\mathcal{V}_\mathit{sorts}}
\newcommand{\mathcal{V}_\mathit{ops}}{\mathcal{V}_\mathit{ops}}
\newcommand{\mathit{sort}}{\mathit{sort}}
\newcommand{\mathit{sig}}{\mathit{sig}}
\newcommand{\mathit{id}}{\mathit{id}}
\newcommand{\lsl`->`}{\lsl`->`}

\newcommand{\super}[2]{\ensuremath{\mathit{#1}^\mathit{#2}}}
\newcommand{\tri}[3]{\ensuremath{\mathit{#1}^\mathit{#2}_\mathit{#3}}}
\newcommand{\ensuremath{\mathit{Assumptions}}}{\ensuremath{\mathit{Assumptions}}}
\newcommand{\actPred}[3][\pi]{\tri{P}{#2,#1}{#3}}
\newcommand{\actualTypes}[1]{\super{actualTypes}{#1}}
\newcommand{\actuals}[1]{\super{actuals}{#1}}
\newcommand{\autActVars}[2][\pi]{\vars{#2}{},\vars{#2,#1}{}}
\newcommand{\bracket}[2]{\mathit{#1}[\mathit{#2}]}
\newcommand{\compVars}[1]{\super{compVars}{#1}}
\newcommand{\mathit{context}}{\mathit{context}}
\newcommand{\ensuring}[2]{\tri{ensuring}{#1}{#2}}
\newcommand{\initPred}[1]{\tri{P}{#1}{init}}
\newcommand{\initVals}[1]{\super{initVals}{#1}}
\newcommand{\initially}[2]{\tri{initially}{#1}{#2}}
\newcommand{\invPred}[2]{\tri{Inv}{#1}{#2}}
\newcommand{\knownVars}[1]{\super{knownVars}{#1}}
\newcommand{\localPostVars}[2]{\tri{localPostVars}{#1}{#2}}
\newcommand{\localVars}[2]{\tri{localVars}{#1}{#2}}
\newcommand{\locals}[1]{\bracket{Locals}{#1}}
\newcommand{\nam}[1]{\rho^{\mathit{#1}}}
\newcommand{\otherActPred}[3][\pi]{\otherTri{P}{#2,#1}{#3}}
\newcommand{\otherParams}[2]{\otherTri{params}{#1}{#2}}
\newcommand{\otherSub}[2]{\otherTri{\sigma}{#1}{#2}}
\newcommand{\otherTri}[3]{\tri{\smash{#1'}}{#2}{#3}}
\newcommand{\otherVars}[2]{\otherTri{vars}{#1}{#2}}
\newcommand{\params}[2]{\tri{params}{#1}{#2}}
\newcommand{\postVars}[1]{\super{postVars}{#1}}
\newcommand{\pre}[2]{\tri{Pre}{#1}{#2}}
\newcommand{\prog}[2]{\tri{Prog}{#1}{#2}}
\newcommand{\prov}[2]{\tri{Prov}{#1}{#2}}
\newcommand{\stateSorts}[1]{\super{stateSorts}{#1}}
\newcommand{\stateVars}[1]{\super{stateVars}{#1}}
\newcommand{\states}[1]{\bracket{States}{#1}}
\newcommand{\sub}[2]{\tri{\sigma}{#1}{#2}}
\newcommand{\sugActPred}[3][\pi]{\tri{P}{#2,#1}{#3,desug}}
\newcommand{\sugLocalVars}[2]{\ifthenelse{\equal{}{#2}}%
                             {\tri{localVars}{#1}{desug}}%
                             {\tri{localVars}{#1}{#2,desug}}}
\newcommand{\sugVars}[2]{\ifthenelse{\equal{}{#2}}%
                        {\tri{vars}{#1}{desug}}%
                        {\tri{vars}{#1}{#2,desug}}}
\newcommand{\cVars}[1]{\super{cVars}{#1}}

\newcommand{\dot{\varrho}}{\dot{\varrho}}
\newcommand{\map}[2]{\tri{\dot{\varrho}}{#1}{#2}}

\newcommand{\types}[1]{\super{types}{#1}}

\newcommand{\subActPred}[3][\pi]{\sub{#2,#1}{#3}(\tri{P}{#2,#1}{#3,desug})}
\newcommand{\subLocalVars}[2]{\sub{#1}{#2}(\tri{localVars}{#1}{#2,desug})}

\newcommand{\hat{A}}{\hat{A}}
\newcommand{\renameAction}[1]{\ensuremath{\rho_{#1}(\vars{\hat{A}{#1},\pi}{})}}
\newcommand{\renameComponent}[1]{\ensuremath{\rho_{#1}\hat{A}_{#1}}}

\newenvironment{Syntax}{\[\begin{subSyntax}}{\end{subSyntax}\]\vspace{-.3in}}
\newenvironment{subSyntax}{\begin{array}{l}}{\end{array}}
\newcommand{\w}[1]{\mbox{\hspace*{#1em}}}

\newcommand{\ms}[1]{\ifmmode%
\mathord{\mathcode`-="702D\it #1\mathcode`\-="2200}\else%
$\mathord{\mathcode`-="702D\it #1\mathcode`\-="2200}$\fi}

\newcommand{\kw}[1]{{\bf #1}}
\newcommand{\tcon}[1]{{\tt #1}}
\newcommand{\syn}[1]{{\tt #1}}
\newcommand{\pvskw}[1]{{\sc #1}}
\newcommand{\pvsid}[1]{{\operatorname{\mathit{#1}}}}

\def{\cal A}{{\cal A}}
\def{\cal B}{{\cal B}}
\def\D{{\cal D}}
\def\mathit{true}{{\cal T}}

\newcommand{{\bf v}}{{\bf v}}
\newcommand{{\bf w}}{{\bf w}}
\newcommand{{\bf x}}{{\bf x}}
\newcommand{{\bf X}}{{\bf X}}
\newcommand{{\bf V}}{{\bf V}}
\newcommand{{\bf y}}{{\bf y}}
\newcommand{{\bf a}}{{\bf a}}
\newcommand{{\bf b}}{{\bf b}}
\newcommand{{\bf q}}{{\bf q}}
\newcommand{{\bf s}}{{\bf s}}
\newcommand{{\bf m}}{{\bf m}}

\newcommand{\arrow}[1]{\mathrel{\stackrel{#1}{\rightarrow}}}
\newcommand{\sarrow}[2]{\mathrel{\stackrel{#1}{\rightarrow_{#2}}}}
\newcommand{\concat}{\mathbin{^{\frown}}}
\newcommand{\mathrel{\diamond}}{\mathrel{\diamond}}

\def\CC{{\mathscr C}}

\lstdefinelanguage{pvs}{
  basicstyle=\tt \scriptsize,
  keywordstyle=\sc \scriptsize,
  identifierstyle=\it \scriptsize,
  emphstyle=\tt \scriptsize,
  mathescape=true,
  tabsize=20,
  sensitive=false,
  columns=fullflexible,
  keepspaces=false,
  flexiblecolumns=true,
  basewidth=0.05em,
  moredelim=[il][\rm]{//},
  moredelim=[is][\sf \scriptsize]{!}{!},
  moredelim=[is][\bf \scriptsize]{*}{*},
  keywords={and,
  	 begin,
  	 cases, const,
  	 do,
  	 external, else, exists, end, endcases, endif,
  	 fi,for, forall, from,
  	 hidden,
  	 in, if, importing,
     let, lambda, lemma,
     measure,
     not,
     or, of,
     return, recursive,
     stop,
     theory, that,then, type, types, type+, to, theorem,
     var,
     with,while},
  emph={nat, setof, sequence, eq, tuple, map, array, enumeration, bool, real, exp, nnreal, posreal},
   literate=
        {(}{{$($}}1
        {)}{{$)$}}1

        {\\in}{{$\in\ $}}1
        {\\mapsto}{{$\rightarrow\ $}}1
        {\\preceq}{{$\preceq\ $}}1
        {\\subset}{{$\subset\ $}}1
        {\\subseteq}{{$\subseteq\ $}}1
        {\\supset}{{$\supset\ $}}1
        {\\supseteq}{{$\supseteq\ $}}1
        {\\forall}{{$\forall$}}1
        {\\le}{{$\le\ $}}1
        {\\ge}{{$\ge\ $}}1
        {\\gets}{{$\gets\ $}}1
        {\\cup}{{$\cup\ $}}1
        {\\cap}{{$\cap\ $}}1
        {\\langle}{{$\langle$}}1
        {\\rangle}{{$\rangle$}}1
        {\\exists}{{$\exists\ $}}1
        {\\bot}{{$\bot$}}1
        {\\rip}{{$\rip$}}1
        {\\emptyset}{{$\emptyset$}}1
        {\\notin}{{$\notin\ $}}1
        {\\not\\exists}{{$\not\exists\ $}}1
        {\\ne}{{$\ne\ $}}1
        {\\to}{{$\to\ $}}1
        {\\implies}{{$\implies\ $}}1

        {<}{{$<\ $}}1
        {>}{{$>\ $}}1
        {=}{{$=\ $}}1
        {~}{{$\neg\ $}}1
        {|}{{$\mid$}}1
        {'}{{$^\prime$}}1

        {\{\cal A}}{{$\forall\ $}}1
        {\\E}{{$\exists\ $}}1
        {\\/}{{$\vee\,$}}1
        {\\vee}{{$\vee\,$}}1
        {/\\}{{$\wedge\,$}}1
        {\\wedge}{{$\wedge\,$}}1
        {->}{{$\rightarrow\ $}}1
        {=>}{{$\Rightarrow\ $}}1
        {->}{{$\rightarrow\ $}}1
        {<=}{{$\Leftarrow\ $}}1
        {<-}{{$\leftarrow\ $}}1
        {~=}{{$\neq\ $}}1
        {\\U}{{$\cup\ $}}1
        {\{\ensuremath{\cap}}}{{$\cap\ $}}1
        {|-}{{$\vdash\ $}}1
        {-|}{{$\dashv\ $}}1
        {<<}{{$\ll\ $}}2
        {>>}{{$\gg\ $}}2
        {||}{{$\|$}}1
        {[}{{$[$}}1
        {]}{{$\,]$}}1
        {[[}{{$\langle$}}1
        {]]]}{{$]\rangle$}}1
        {]]}{{$\rangle$}}1
        {<=>}{{$\Leftrightarrow\ $}}2
        {<->}{{$\leftrightarrow\ $}}2
        {(+)}{{$\oplus\ $}}1
        {(-)}{{$\ominus\ $}}1
        {_i}{{$_{i}$}}1
        {_j}{{$_{j}$}}1
        {_{i,j}}{{$_{i,j}$}}3
        {_{j,i}}{{$_{j,i}$}}3
        {_0}{{$_0$}}1
        {_1}{{$_1$}}1
        {_2}{{$_2$}}1
        {_n}{{$_n$}}1
        {_p}{{$_p$}}1
        {_k}{{$_n$}}1
        {-}{{$\ms{-}$}}1
        {@}{{}}0
        {\\delta}{{$\delta$}}1
        {\\R}{{$\R$}}1
        {\\Rplus}{{$\Rplus$}}1
        {\\act{N}}{{$\act{N}$}}1
        {\\times}{{$\times\ $}}1
        {\\tau}{{$\tau$}}1
        {\\alpha}{{$\alpha$}}1
        {\\beta}{{$\beta$}}1
        {\\gamma}{{$\gamma$}}1
        {\\ell}{{$\ell\ $}}1
        {--}{{$-\ $}}1
        {\\TT}{{\hspace{1.5em}}}3
      }

\lstdefinelanguage{BigPVS}{
  basicstyle=\tt,
  keywordstyle=\sc,
  identifierstyle=\it,
  emphstyle=\tt ,
  mathescape=true,
  tabsize=20,
  sensitive=false,
  columns=fullflexible,
  keepspaces=false,
  flexiblecolumns=true,
  basewidth=0.05em,
  moredelim=[il][\rm]{//},
  moredelim=[is][\sf \scriptsize]{!}{!},
  moredelim=[is][\bf \scriptsize]{*}{*},
  keywords={and,
  	 begin,
  	 cases, const,
  	 do, datatype,
  	 external, else, exists, end, endif, endcases,
  	 fi,for, forall, from,
  	 hidden,
  	 in, if, importing,
     let, lambda, lemma,
     measure,
     not,
     or, of,
     return, recursive,
     stop,
     theory, that,then, type, types, type+, to, theorem,
     var,
     with,while},
  emph={nat, setof, sequence, eq, tuple, map, array, first, rest, add, enumeration, bool, real, posreal, nnreal},
   literate=
        {(}{{$($}}1
        {)}{{$)$}}1

        {\\in}{{$\in\ $}}1
        {\\mapsto}{{$\rightarrow\ $}}1
        {\\preceq}{{$\preceq\ $}}1
        {\\subset}{{$\subset\ $}}1
        {\\subseteq}{{$\subseteq\ $}}1
        {\\supset}{{$\supset\ $}}1
        {\\supseteq}{{$\supseteq\ $}}1
        {\\forall}{{$\forall$}}1
        {\\le}{{$\le\ $}}1
        {\\ge}{{$\ge\ $}}1
        {\\gets}{{$\gets\ $}}1
        {\\cup}{{$\cup\ $}}1
        {\\cap}{{$\cap\ $}}1
        {\\langle}{{$\langle$}}1
        {\\rangle}{{$\rangle$}}1
        {\\exists}{{$\exists\ $}}1
        {\\bot}{{$\bot$}}1
        {\\rip}{{$\rip$}}1
        {\\emptyset}{{$\emptyset$}}1
        {\\notin}{{$\notin\ $}}1
        {\\not\\exists}{{$\not\exists\ $}}1
        {\\ne}{{$\ne\ $}}1
        {\\to}{{$\to\ $}}1
        {\\implies}{{$\implies\ $}}1

        {<}{{$<\ $}}1
        {>}{{$>\ $}}1
        {=}{{$=\ $}}1
        {~}{{$\neg\ $}}1
        {|}{{$\mid$}}1
        {'}{{$^\prime$}}1

        {\{\cal A}}{{$\forall\ $}}1
        {\\E}{{$\exists\ $}}1
        {\\/}{{$\vee\,$}}1
        {\\vee}{{$\vee\,$}}1
        {/\\}{{$\wedge\,$}}1
        {\\wedge}{{$\wedge\,$}}1
        {->}{{$\rightarrow\ $}}1
        {=>}{{$\Rightarrow\ $}}1
        {->}{{$\rightarrow\ $}}1
        {<=}{{$\Leftarrow\ $}}1
        {<-}{{$\leftarrow\ $}}1
        {~=}{{$\neq\ $}}1
        {\\U}{{$\cup\ $}}1
        {\{\ensuremath{\cap}}}{{$\cap\ $}}1
        {|-}{{$\vdash\ $}}1
        {-|}{{$\dashv\ $}}1
        {<<}{{$\ll\ $}}2
        {>>}{{$\gg\ $}}2
        {||}{{$\|$}}1
        {[}{{$[$}}1
        {]}{{$\,]$}}1
        {[[}{{$\langle$}}1
        {]]]}{{$]\rangle$}}1
        {]]}{{$\rangle$}}1
        {<=>}{{$\Leftrightarrow\ $}}2
        {<->}{{$\leftrightarrow\ $}}2
        {(+)}{{$\oplus\ $}}1
        {(-)}{{$\ominus\ $}}1
        {_i}{{$_{i}$}}1
        {_j}{{$_{j}$}}1
        {_{i,j}}{{$_{i,j}$}}3
        {_{j,i}}{{$_{j,i}$}}3
        {_0}{{$_0$}}1
        {_1}{{$_1$}}1
        {_2}{{$_2$}}1
        {_n}{{$_n$}}1
        {_p}{{$_p$}}1
        {_k}{{$_n$}}1
        {-}{{$\ms{-}$}}1
        {@}{{}}0
        {\\delta}{{$\delta$}}1
        {\\R}{{$\R$}}1
        {\\Rplus}{{$\Rplus$}}1
        {\\act{N}}{{$\act{N}$}}1
        {\\times}{{$\times\ $}}1
        {\\tau}{{$\tau$}}1
        {\\alpha}{{$\alpha$}}1
        {\\beta}{{$\beta$}}1
        {\\gamma}{{$\gamma$}}1
        {\\ell}{{$\ell\ $}}1
        {--}{{$-\ $}}1
        {\\TT}{{\hspace{1.5em}}}3
      }

\lstdefinelanguage{pvsNums}[]{pvs}
{
  numbers=left,
  numberstyle=\tiny,
  stepnumber=2,
  numbersep=4pt
}

\lstdefinelanguage{pvsNumsRight}[]{pvs}
{
  numbers=right,
  numberstyle=\tiny,
  stepnumber=2,
  numbersep=4pt
}

\newcommand{\lstinline[language=PVS]}{\lstinline[language=PVS]}

\lstnewenvironment{BigPVS}%
  {\lstset{language=BigPVS}}
  {}

\lstnewenvironment{PVSNums}%
  {
  \if@firstcolumn
    \lstset{language=pvs, numbers=left, firstnumber=auto}
  \else
    \lstset{language=pvs, numbers=right, firstnumber=auto}
  \fi
  }
  {}

\lstnewenvironment{PVSNumsRight}%
  {
    \lstset{language=pvs, numbers=right, firstnumber=auto}
  }
  {}

\newcommand{\figpvs}[5]{
  \begin{figure}[#1]
      \hrule \mathit{false}
      {\scriptsize \bf #2}
      \lstinputlisting[language=pvs]{#5}
      \mathit{false} \hrule \mathit{false}
      \caption{#3}
      \label{fig: #4}
  \end{figure}
}

\newcommand{\linefigpvs}[9]{

}

\newcommand{\twofigpvs}[8]{
  \begin{figure}[#1]
    \hrule \mathit{false}
    {\scriptsize \bf #2} \\
    \two{#5}{#6}
    {
      \lstinputlisting[language=pvsLang]{#7}
    }
    {
      \lstinputlisting[language=pvsLang]{#8}
    }
    \mathit{false} \hrule \mathit{false}
    \caption{#3}
    \label{fig: #4}
  \end{figure}
}

\lstdefinelanguage{pvsproof}{
  basicstyle=\tt \scriptsize,
  mathescape=true,
  tabsize=4,
  sensitive=false,
  columns=fullflexible,
  keepspaces=false,
  flexiblecolumns=true,
  basewidth=0.05em,
}

\newcommand{\abs}[1]{\left\vert#1\right\vert}
\newcommand{\pair}[1]{\left\langle#1\right\rangle}
\newcommand{\tuple}[1]{\left\langle#1\right\rangle}

\newcommand{\floor}[1]{\left\lfloor#1\right\rfloor}
\newcommand{\ceil}[1]{\left\lceil#1\right\rceil}
\newcommand{\norm}[1]{\left\Vert#1\right\Vert}
\newcommand{\twonorm}[1]{\left\Vert#1\right\Vert_{2}}
\newcommand{\infnorm}[1]{\left\Vert#1\right\Vert_{\infty}}
\newcommand{\argmin}[2]{\underset{#2}{\operatorname{argmin}} #1}
\newcommand{\argmax}[2]{\underset{#2}{\operatorname{argmax}} #1}
\newcommand{\maxel}[2]{\underset{#2}{\operatorname{max}} #1}
\newcommand{\minel}[2]{\underset{#2}{\operatorname{min}} #1}
\newcommand{\sgn}[1]{\operatorname{sgn} \left( #1 \right)}
\newcommand{\lima}[2]{\underset{#2}{\operatorname{lim}} #1}
\newcommand{\supel}[2]{\underset{#2}{\operatorname{sup}} \ #1}
\newcommand{\infel}[2]{\underset{#2}{\operatorname{inf}} \ #1}

\def\act{Init}_i{\operatorname{\mathsf {act}}{Init}_i}
\def\act{Init_G}[i]{\operatorname{\mathsf {act}}{Init_G}[i]}
\def\act{Init_L}[i]{\operatorname{\mathsf {act}}{Init_L}[i]}
\def\act{Prop}_i{\operatorname{\mathsf {act}}{Prop}_i}

\def\operatorname{\mathsf {act}}{V}{\operatorname{\mathsf {act}}{Var}}
\def\Var_i{\operatorname{\mathsf {act}}{V}_i}
\def\Var_j{\operatorname{\mathsf {act}}{V}_j}
\def\Var_h{\operatorname{\mathsf {act}}{V}_h}

\def\act{Act}{\operatorname{\mathsf {act}}{Act}}
\def{\Act}_i{{\act{Act}}_i}

\def\act{Loc}{\operatorname{\mathsf {act}}{Loc}}
\def\act{Mode}_i{\act{Loc}_i}

\def\act{Mode}{\operatorname{\mathsf {act}}{Mode}}
\def\act{Mode}_i{\act{Mode}_i}

\defv_{min}{v_{min}}
\defv_{max}{v_{max}}

\def\mathit{next}{\mathit{next}}
\def\next[i]{\mathit{next}[i]}
\def\mathit{last}{\mathit{last}}

\def\mathsf{ITerm}{\mathsf{ITerm}}
\def\mathsf{DTerm}{\mathsf{DTerm}}
\def\mathsf{RTerm}{\mathsf{RTerm}}
\def\mathsf{RPoly}{\mathsf{RPoly}}
\def\mathsf{RAtom}{\mathsf{RAtom}}
\def\mathsf{ZTerm}{\mathsf{ZTerm}}
\def\mathsf{ZPoly}{\mathsf{ZPoly}}
\def\mathsf{ZAtom}{\mathsf{ZAtom}}
\def\mathsf{Formula}{\mathsf{Formula}}
\def\mathsf{Atom}{\mathsf{Atom}}
\def\mathsf{Sent}{\mathsf{Sent}}

\newcommand{\checkmark\xspace}{\checkmark\xspace}
\newcommand{\hspace{1pt}\ding{55}\xspace}{\hspace{1pt}\ding{55}\xspace}

\newcommand{LH-assertion\xspace}{LH-assertion\xspace}
\newcommand{LH-assertions\xspace}{LH-assertions\xspace}
\newcommand{\toolname}{{\it Passel}\xspace}
\newcommand{{\it Passel}\xspace}{{\it Passel}\xspace}
\newcommand{\toolmurphi}{Mur$\varphi$\xspace}
\newcommand{Spin\xspace}{Spin\xspace}
\newcommand{MCMT\xspace}{MCMT\xspace}
\newcommand{Charon\xspace}{Charon\xspace}
\newcommand{PHAVer\xspace}{PHAVer\xspace}
\newcommand{HyTech\xspace}{HyTech\xspace}
\newcommand{HyLink\xspace}{HyLink\xspace}
\newcommand{HARE\xspace}{HARE\xspace}
\newcommand{PVS\xspace}{PVS\xspace}
\newcommand{SAL\xspace}{SAL\xspace}
\newcommand{KeYmaera\xspace}{KeYmaera\xspace}
\newcommand{SpaceEx\xspace}{SpaceEx\xspace}
\newcommand{UPAAAL\xspace}{UPAAAL\xspace}
\newcommand{Isabelle/HOL\xspace}{Isabelle/HOL\xspace}
\newcommand{Yices\xspace}{Yices\xspace}
\newcommand{Z3\xspace}{Z3\xspace}
\newcommand{IIV\xspace}{IIV\xspace}
\newcommand{QBMC\xspace}{QBMC\xspace}
\newcommand{\robotframework}{StarL\xspace}

\newcommand{\ds}[1]{\left\llbracket#1\right\rrbracket}

\def\A(i){{\cal A}_i}
\def\A(j){{\cal A}_j}

\def\A^{\act{N}}{{\cal A}^N}

\defthis{this}

\def\mathbf{b^r}{\mathbf{b^r}}
\def\mathbf{b^l}{\mathbf{b^l}}

\def\mathbf{m^r}{\mathbf{m^r}}
\def\mathbf{m^l}{\mathbf{m^l}}

\def\mathbf{h3^r}{\mathbf{h3^r}}
\def\mathbf{h2^r}{\mathbf{h2^r}}
\def\mathbf{h3^l}{\mathbf{h3^l}}
\def\mathbf{h2^l}{\mathbf{h2^l}}

\def\mathbf{fly}{\mathbf{fly}}

\def\mathbf{fin}{\mathbf{fin}}
\def\mathbf{run}{\mathbf{run}}

\def\mathbf{taxi}{\mathbf{taxi}}

\def\mathit{left}{\mathit{left}}
\def\mathit{right}{\mathit{right}}

\newcommand{{\mathop{\mathsf {dom}}}}{\mathop{\mathsf {dom}}}

\def\Agenti{{\auto{Agent_i}}}
\def\Agentj{{\auto{Agent_j}}}
\def\System{{\auto{System}}}

\def\suspect{{\operatorname{\mathsf {act}}{suspect}}}
\def\update{{\operatorname{\mathsf {act}}{update}}}

\def\l{{L}}
\def\r{{R}}

\def\Xq{\X_{\backslash \sim}}
\def\Mq{\M_{\backslash \sim}}

\def{\mathop{\mathsf {dom}}}{{\mathop{\mathsf {dom}}}}

\def\zerov{\mathbf{0}}

\def\Terminable{\Lambda}
\def\Terminated{\Omega}

\def\dot{\forall}{\dot{\forall}}
\def\dot{\exists}{\dot{\exists}}

\newcommand{{\bf ugrd}}{{\bf ugrd}}

\def\auto{MUX-SEM}{\auto{MUX-SEM}}
\def\auto{MUX-SEM-RA}{\auto{MUX-SEM-RA}}
\def\auto{MUX-INDEX-RECT}{\auto{MUX-INDEX-RECT}}
\def\auto{TMUX}{\auto{TMUX}}
\def\auto{Fischer}{\auto{Fischer}}
\def\auto{Fischer-Timed}{\auto{Fischer-Timed}}
\def\auto{Fischer-Aux-Timed}{\auto{Fischer-Aux}}
\def\auto{Fischer-Aux-Timed}{\auto{Fischer-Aux-Timed}}
\def\auto{SATS}{\auto{SATS}}
\def\auto{SSATS}{\auto{SSATS}}
\def\auto{SSATS-Timed}{\auto{SSATS-Timed}}

\def\mathtt{S}{\mathtt{S}}
\def\mathtt{G}{\mathtt{G}}
\def\mathtt{Classes}{\mathtt{Classes}}
\def\mathtt{N}{\mathtt{N}}
\def\mathtt{C}{\mathtt{C}}
\def\mathtt{Form}{\mathtt{Form}}
\def\mathtt{Inst}{\mathtt{Inst}}
\def\mathtt{Count}{\mathtt{Count}}
\def\mathtt{I}{\mathtt{I}}

\newcommand{\symconcretization}[1]{\ds{#1}}

\def\sf AnonReach{\sf AnonReach}
\def\symreach{\sf AnonReach}
\def\symreach(\AN){\sf AnonReach(\A^{\act{N}})}

\def\mathtt{ReachForms}{\mathtt{ReachForms}}

\def\pi{\pi}
\def{\sf Frontier}{{\sf Frontier}}
\def{\SymFrontier_{\mathtt{New}}}{{{\sf Frontier}_{\mathtt{New}}}}
\def{\SymState_{\mathtt{New}}}{{\mathtt{S}_{\mathtt{New}}}}
\def{\SymClass_{\mathtt{New}}}{{\mathtt{C}_{\mathtt{New}}}}

\def\sf States_{\mathtt{New}}{\sf States_{\mathtt{New}}}

\def\auto{mergeClasses}{\auto{mergeClasses}}

\newcommand{\mergeclasses}[1]{\auto{mergeClasses}(#1)}
\newcommand{\mathit{post}}{\mathit{post}}
\newcommand{\mathit{post_{time}}}{\mathit{post_{time}}}
\newcommand{\PostDiscrete}[3]{\mathit{post}(#1, #2, #3)}
\newcommand{\PostDiscreteClass}[2]{\mathit{post_{class}}(#1, #2)}
\newcommand{\PostTime}[1]{\mathit{post_{time}}(#1)}
\newcommand{\symid}[1]{\pi(#1)}
\newcommand{\symclass}[2]{\left\langle#1, #2\right\rangle}
\newcommand{\symclassfull}[3]{\left\langle#1, #2, #3\right\rangle}
\newcommand{\symstatenoglobal}[1]{\left\{#1\right\}}
\newcommand{\symstate}[2]{\left\langle\symstatenoglobal{#1}, #2\right\rangle}
\def\auto{discreteSuccessors}{\auto{discreteSuccessors}}
\newcommand{\succdiscrete}[3]{\auto{discreteSuccessors}(#1, #2, #3)}
\def\auto{contSuccessors}{\auto{contSuccessors}}
\newcommand{\succcont}[3]{\auto{contSuccessors}(#1, #2, #3)}

\def\auto{RemapIndices}{\auto{RemapIndices}}

\defq[j]{q[j]}

\def\act{P}{\operatorname{\mathsf {act}}{P}}
\def\act{N}{\operatorname{\mathsf {act}}{N}}
\def\mathit{ID}{[\act{N}]}
\def\mathcal{N}{\mathcal{N}}
\def[\NArb]{[\mathcal{N}]}
\def[\Projected]{[\act{P}]}
\def[n]{[n]}

\def\ID_{\bot}{\mathit{ID}_{\bot}}
\def\IDArb_{\bot}{[\NArb]_{\bot}}

\def\operatorname{\mathsf {act}}{Init}{\operatorname{\mathsf {act}}{Init}}
\def\act{Init}_i{\operatorname{\mathsf {act}}{Init}_i}
\def\Theta^{\NArb}{\Theta^{\mathcal{N}}}

\def\act{X}{\operatorname{\mathsf {act}}{X}}
\def\act{X}[i]{\operatorname{\mathsf {act}}{X}[i]}
\def\act{X}[j]{\operatorname{\mathsf {act}}{X}[j]}
\def\operatorname{\mathsf {act}}{V}{\operatorname{\mathsf {act}}{V}}
\def\Var^{\N}{\operatorname{\mathsf {act}}{V}^{\act{N}}}
\def\Var^{\NArb}{\operatorname{\mathsf {act}}{V}^{\mathcal{N}}}
\def\Var_n{\operatorname{\mathsf {act}}{V}_n}
\def\Var_i{\operatorname{\mathsf {act}}{V}_i}
\def\Var_P{\operatorname{\mathsf {act}}{V}_P}
\def\Var_j{\operatorname{\mathsf {act}}{V}_j}
\def\Var_G{\operatorname{\mathsf {act}}{V}_G}

\def\Var_L{\operatorname{\mathsf {act}}{V}_L}
\def\VarL[i]{\Var_L[i]}
\def\VarL[j]{\Var_L[j]}
\def\VarG[i]{\Var_G[i]}
\def\VarP[i]{\Var_P[i]}

\def\Var_h{\operatorname{\mathsf {act}}{V}_h}

\defQ^{\N}{Q^{\act{N}}}
\defQ^{\Projected}{Q^{\act{P}}}
\defD^{\N}{D^{\act{N}}}
\defT^{\N}{T^{\act{N}}}
\def\Theta^{\N}{\Theta^{\act{N}}}

\defQ^{\NArb}{Q^{\mathcal{N}}}
\defT^{\NArb}{T^{\mathcal{N}}}
\def\D^{\NArb}{\D^{\mathcal{N}}}
\def\D^{\N}{\D^{\act{N}}}
\def\T^{\NArb}{\mathit{true}^{\mathcal{N}}}
\def\T^{\N}{\mathit{true}^{\act{N}}}
\def\Theta^{\NArb}{\Theta^{\mathcal{N}}}

\def\act{Act}{\operatorname{\mathsf {act}}{Act}}
\def{\Act}_i{{\act{Act}}_i}

\def\act{Loc}{\operatorname{\mathsf {act}}{Loc}}
\def\act{Mode}_i{\act{Loc}_i}

\def\act{Mode}{\operatorname{\mathsf {act}}{Mode}}
\def\act{Mode}_i{\act{Mode}_i}

\def\Loc_i{\act{Loc}_i}

\def\act{Trans}_i{\operatorname{\mathsf {act}}{Trans}_i}
\def\act{Trans}_h{\operatorname{\mathsf {act}}{Trans}_h}
\def\act{Flow}_i{\operatorname{\mathsf {act}}{Flow}_i}

\newcommand{\loc}[1]{{\operatorname{\mathsf {act}}{#1}}}

\newcommand{\trans}[1]{{\operatorname{\mathsf {act}}{#1}}}
\newcommand{\transfromto}[3]{{\operatorname{\mathsf {act}}{#1}(\loc{#2}, \loc{#3})}}
\newcommand{\mathit{v}}[1]{{\mathit{val}(#1)}}
\newcommand{\vars}[1]{{\mathit{vars}(#1)}}
\newcommand{\mathcal{FV}}[1]{{\mathit{free}(#1)}}
\newcommand{\boundvars}[1]{{\mathit{bound}(#1)}}
\newcommand{\qbody}[1]{{\mathit{body}(#1)}}
\newcommand{\indexvars}[1]{{\mathit{ivars}(#1)}}
\newcommand{\localvar}[2]{{{#1_{#2}}}}
\newcommand{\localvardot}[2]{{\dot{#1}_{#2}}}
\newcommand{\localvarprime}[2]{{\dot{#1}_{#2}}}
\newcommand{\localvardotsyntax}[2]{{\localvar{#1}{#2}\_\mbox{dot}}}
\newcommand{\arrayvar}[1]{\bar{#1}}
\newcommand{\arrayvars}[1]{\langle#1\rangle}
\newcommand{\guardft}[2]{{{\mathit{Grd}}(#1,~#2)}}
\newcommand{\uguard}[1]{{{\bf ugrd}(#1)}}
\newcommand{\uguardft}[2]{{{\bf ugrd}(#1,~#2)}}
\newcommand{\effect}[1]{{\mathit{Eff}(#1)}}
\newcommand{\effectft}[2]{{\mathit{Eff}(#1,~#2)}}

\newcommand{\passelformulas}[1]{{\Lambda(#1)}}

\def\localvar{q}{h}{\localvar{q}{h}}
\def\localvar{m}{h}{\localvar{m}{h}}
\def\localvar{s}{h}{\localvar{s}{h}}
\def\bar{q}{\bar{q}}
\def\localvar{x}{i}{\localvar{x}{i}}
\def\localvar{x}{h}{\localvar{x}{h}}
\def\localvar{s}{i}{\localvar{s}{i}}
\def\localvar{m}{i}{\localvar{m}{i}}
\def\localvar{m}{j}{\localvar{m}{j}}
\def\localvar{s}{j}{\localvar{s}{j}}
\def\localvardot{x}{i}{\localvardot{x}{i}}
\def\localvar{x}{j}{\localvar{x}{j}}
\def\localvardot{x}{j}{\localvardot{x}{j}}
\def\bar{x}{\bar{x}}
\def\localvar{y}{i}{\localvar{y}{i}}
\def\localvar{y}{j}{\localvar{y}{j}}
\def\localvar{a}{i}{\localvar{a}{i}}
\def\localvar{q}{i}{\localvar{q}{i}}
\def\localvar{q}{k}{\localvar{q}{k}}
\def\localvar{q}{c}{\localvar{q}{c}}
\def\localvar{q}{n}{\localvar{q}{n}}
\def\localvar{\ell}{k}{\localvar{\ell}{k}}
\def\localvar{\mathit{v}}{k}{\localvar{\mathit{v}}{k}}
\def\localvar{\ell}{0}{\localvar{\ell}{0}}
\def\localvar{\mathit{v}}{0}{\localvar{\mathit{v}}{0}}
\def\localvar{f}{i}{\localvar{f}{i}}
\def\localvar{inv}{i}{\localvar{inv}{i}}
\def\localvar{q}{k-1}{\localvar{q}{k-1}}
\def\localvar{q}{i + 1}{\localvar{q}{i + 1}}
\def\localvar{f}{i + 1}{\localvar{f}{i + 1}}
\def\localvar{inv}{i + 1}{\localvar{inv}{i + 1}}
\def\localvar{g}{i + 1}{\localvar{g}{i + 1}}
\def\localvar{r}{i + 1}{\localvar{r}{i + 1}}
\def\localvar{T}{i}{\localvar{T}{i}}
\def\localvar{t}{i}{\localvar{t}{i}}
\def\localvar{t}{i+1}{\localvar{t}{i+1}}
\def\localvar{T}{k}{\localvar{T}{k}}
\def\localvar{T}{i + 1}{\localvar{T}{i + 1}}
\def\localvar{T}{1}{\localvar{T}{1}}
\def\localvar{T}{2}{\localvar{T}{2}}
\def\localvar{S}{i}{\localvar{S}{i}}
\def\localvar{S}{k}{\localvar{S}{k}}
\def\localvar{S}{c}{\localvar{S}{c}}
\def\localvar{S}{n}{\localvar{S}{n}}
\def\localvar{S}{i + 1}{\localvar{S}{i + 1}}
\def\localvar{S}{k-1}{\localvar{S}{k-1}}
\def...{...}
\defS{S}
\defA{A}
\defT{T}
\defI{I}
\defP{P}
\def\Phi(k){\Phi(k)}
\def\Omega(k){\Omega(k)}
\def\Omega(3){\Omega(3)}
\defFS\xspace{FS\xspace}
\defFU\xspace{FU\xspace}
\defFS-2\xspace} % Taylor2Luan: probably this would be simpler with a \newcommand that takes an argument, e.g. \fischerunsafe{2{FS-2\xspace}
\defFU-2\xspace{FU-2\xspace}
\defFS-3\xspace{FS-3\xspace}
\defFU-3\xspace{FU-3\xspace}
\defFS-4\xspace{FS-4\xspace}
\defFU-4\xspace{FU-4\xspace}
\defFS-5\xspace{FS-5\xspace}
\defFU-5\xspace{FU-5\xspace}

\defv_{min}{v_{min}}
\defv_{max}{v_{max}}

\def\mathit{next}{\mathit{next}}
\def\next[i]{\mathit{next}[i]}
\def\mathit{last}{\mathit{last}}

\def\mathsf{ITerm}{\mathsf{ITerm}}
\def\mathsf{DTerm}{\mathsf{DTerm}}
\def\mathsf{RTerm}{\mathsf{RTerm}}
\def\mathsf{Formula}{\mathsf{Formula}}
\def\mathsf{Atom}{\mathsf{Atom}}
\def\mathsf{Sent}{\mathsf{Sent}}

\def\A(i){{\cal A}(i)}
\def\B(i){{\cal B}(i)}
\def\C(i){\C(i)}
\def\A(\N, i){{\cal A}(\act{N}, i)}
\def\A(\NArb, i){{\cal A}(\mathcal{N}, i)}
\def\A(j){{\cal A}(j)}
\def\A^{\act{N}}{{\cal A}^{\act{N}}}
\def{\sf Reach}{{\sf Reach}}
\def\reach(\AN){{\sf Reach}(\A^{\act{N}})}
\def\A^{\NArb}{{\cal A}^{\mathcal{N}}}
\def\A^{\N_0}{{\cal A}^{\N_0}}
\def\A^{\Projected}{{\cal A}^{\act{P}}}
\def\reach(\ANArb){{\sf Reach}(\A^{\NArb})}
\def\A^n{{\cal A}^n}
\def\F_{\N}{\mathit{false}_{\act{N}}}
\def\F_n{\mathit{false}_n}

\def\mathit{post}{\mathit{post}}

\def\vx_i{{\bf x}_i}

\def\dot{\forall}{\dot{\forall}}
\def\dot{\exists}{\dot{\exists}}

\def\act{L}{\operatorname{\mathsf {act}}{L}}

\def\upsilon{\upsilon}
\def\upsilon(\N){\upsilon(\act{N})}
\def\upsilon(\NArb){\upsilon(\mathcal{N})}
\def\zeta{\zeta}
\def\zeta(\N){\zeta(\act{N})}
\def\SafetyProperty(\N_0){\zeta(\N_0)}
\def\SafetyProperty(\NArb){\zeta(\mathcal{N})}
\def\Gamma(\N){\Gamma(\act{N})}
\def\Gamma(n){\Gamma(n)}
\def\Gamma(\NArb){\Gamma(\mathcal{N})}

\def\mathcal{I}{\mathcal{I}}

\def\mathcal{S}{\mathcal{S}}
\def\mathcal{C}{\mathcal{C}}
\def\Theta{\Theta}
\def\Theta_\N{\Theta_\act{N}}
\def\mathcal{T}{\mathcal{T}}
\def\tau{\tau}
\def\tau_D{\tau_D}
\def\tau_T{\tau_T}
\def\tau^{\ast}{\tau^{\ast}}
\def\tau_\N{\tau_\act{N}}
\def\tau_\N^D{\tau_\act{N}^D}
\def\tau_\N^T{\tau_\act{N}^T}
\def\tau_\N^{\ast}{\tau_\act{N}^{\ast}}
\def\ConcreteS_\N{\mathcal{S}_\act{N}}
\def\ConcreteS_i{\mathcal{S}_i}
\def\ConcreteD_\N{\mathcal{C}_\act{N}}

\def\mathcal{S}{\mathcal{S}}
\def\mathcal{L}{\mathcal{L}}
\def\AbstractDN{\mathcal{L}}
\def\tau{\tau}
\def\tau_\N{\tau_\act{N}}
\def\tau_\N^{\ast}{\tau_\act{N}^{\ast}}
\def\tau^{\sharp}{\tau^{\sharp}}
\def\tau^{\sharp\ast}{\tau^{\sharp\ast}}
\def\AbstractXformN^{\sharp}{\tau_\N^{\sharp}}
\def\AbstractXformN^{\sharp\ast}{\tau_\N^{\sharp\ast}}

\def\gamma{\gamma}
\def\concretization_\N{\gamma_\act{N}}
\def\alpha{\alpha}
\def\abstraction_\N{\alpha_\act{N}}

\def\act{rem}{\operatorname{\mathsf {act}}{rem}}
\def\act{try}{\operatorname{\mathsf {act}}{try}}
\def\act{wait}{\operatorname{\mathsf {act}}{wait}}
\def\act{cs}{\operatorname{\mathsf {act}}{cs}}
\def\act{idle}{\operatorname{\mathsf {act}}{idle}}
\def\act{start}{\operatorname{\mathsf {act}}{start}}

\def\act{rem}{\operatorname{\mathsf {act}}{rem}}
\def\act{try}{\operatorname{\mathsf {act}}{try}}
\def\act{wait}{\operatorname{\mathsf {act}}{wait}}
\def\act{cs}{\operatorname{\mathsf {act}}{cs}}
\def\act{set}{\operatorname{\mathsf {act}}{set}}
\def\act{idle}{\operatorname{\mathsf {act}}{idle}}
\def\act{check}{\operatorname{\mathsf {act}}{check}}
\def\act{start}{\operatorname{\mathsf {act}}{start}}
\def\act{loop}{\operatorname{\mathsf {act}}{loop}}
\def\act{fly}{\operatorname{\mathsf {act}}{fly}}
\def\act{hold}{\operatorname{\mathsf {act}}{hold}}
\def\act{base}{\operatorname{\mathsf {act}}{base}}
\def\act{runway}{\operatorname{\mathsf {act}}{runway}}

\def\act{low}{\operatorname{\mathsf {act}}{low}}
\def\act{med}{\operatorname{\mathsf {act}}{med}}
\def\act{high}{\operatorname{\mathsf {act}}{high}}

\deff^{*}_{\N,\Projected}{f^{*}_{\act{N},\act{P}}}
\def\N_0{\act{N}_0}

\def\mathit{off}{\mathit{off}}
\def\mathit{on}{\mathit{on}}

\defPow(\QN){Pow(Q^{\N})}
\defPow(\QP){Pow(Q^{\Projected})}

\newcommand{\rotatebox{90}{$\,=$}}{\rotatebox{90}{$\,=$}}
\newcommand{\rotatebox{90}{$\,\equiv$}}{\rotatebox{90}{$\,\equiv$}}

\def\auto{pg}{\auto{pg}}

\def\localvar{\theta}{i}[k]{\localvar{\theta}{i}[k]}
\def\localvar{\theta}{i}[k+1]{\localvar{\theta}{i}[k+1]}
\def\localvar{\theta}{j}[k]{\localvar{\theta}{j}[k]}

\def\mathit{r_f}{\mathit{r_f}}
\def\mathit{r_s}{\mathit{r_s}}
\def\xi[k]{\localvar{x}{i}[k]}
\def\xj[k]{\localvar{x}{j}[k]}
\def\xi[k+1]{\localvar{x}{i}[k+1]}
\def\localvar{\hat{x}}{i}[k]{\localvar{\hat{x}}{i}[k]}
\def\localvar{\hat{x}}{i}[k+1]{\localvar{\hat{x}}{i}[k+1]}
\def\localvar{\hat{x}}{j}[k]{\localvar{\hat{x}}{j}[k]}
\def\localvar{y}{i}{\localvar{y}{i}}
\def\yi[k]{\localvar{y}{i}[k]}
\def\yi[k+1]{\localvar{y}{i}[k+1]}
\def\localvar{\hat{y}}{i}[k]{\localvar{\hat{y}}{i}[k]}
\def\localvar{\hat{y}}{i}[k+1]{\localvar{\hat{y}}{i}[k+1]}
\def\localvar{A}{i}[k]{\localvar{A}{i}[k]}
\def\localvar{A^{\theta}}{i}[k+1]{\localvar{A^{\theta}}{i}[k+1]}
\def\localvar{A^{\theta}}{i}[k]{\localvar{A^{\theta}}{i}[k]}
\def\localvar{A^{-\theta}}{i}[k]{\localvar{A^{-\theta}}{i}[k]}
\def\localvar{A^{-\theta}}{i}[k+1]{\localvar{A^{-\theta}}{i}[k+1]}

\def\zeta(\N){\zeta(\act{N})}
\def\phi(\N){\phi(\act{N})}
\def\phi(G){\phi(G)}

\def\zeta_{\N}(k){\zeta_{\act{N}}(k)}
\def\zeta(G,k){\zeta(G,k)}
\def\phi_{\N}(k){\phi_{\act{N}}(k)}
\def\phi(G,k){\phi(G,k)}

\def\bf{x}{\bf{x}}
\def\localvar{\xvec}{i}[k]{\localvar{\bf{x}}{i}[k]}
\def\localvar{\bf{\hat{x}}}{i}[k]{\localvar{\bf{\hat{x}}}{i}[k]}
\def\localvar{\xvec}{j}[k]{\localvar{\bf{x}}{j}[k]}

\newcommand{\nbrleft}[1]{\localvar{L}{#1}}
\newcommand{\nbrright}[1]{\localvar{R}{#1}}

\def\nbrleft{i}{\nbrleft{i}}
\def\nbrright{i}{\nbrright{i}}

\newcommand{\localvarsup}[3]{{{#1_{#2}^{#3}}}}

\def\localvarsup{V}{i}{sp}{\localvarsup{V}{i}{sp}}
\def\localvarsup{I}{i}{sp}{\localvarsup{I}{i}{sp}}
\def\localvarsup{V}{i}{\mathit{dc}}{\localvarsup{V}{i}{\mathit{dc}}}
\def\localvarsup{V}{i}{\mathit{ref}}{\localvarsup{V}{i}{\mathit{ref}}}
\def\localvarsup{I}{i}{\mathit{dc}}{\localvarsup{I}{i}{\mathit{dc}}}
\def\localvarsup{V}{i}{\mathit{ac}}{\localvarsup{V}{i}{\mathit{ac}}}
\def\localvarsup{I}{i}{\mathit{ac}}{\localvarsup{I}{i}{\mathit{ac}}}

\defV^{\mathit{ac}}{V^{\mathit{ac}}}
\defV^{\mathit{p}}{V^{\mathit{p}}}
\defV^{\mathit{grid}}{V^{\mathit{grid}}}
\defV^{\mathit{rms}}{V^{\mathit{rms}}}

\def\localvarsup{T}{i}{\mathit{ac}}{\localvarsup{T}{i}{\mathit{ac}}}

\newcommand{\tclock}[1]{\localvarsup{u}{#1}{\mathit{ac}}}
\def\tclock{i}{\tclock{i}}
\def\localvarsup{\dot{u}}{i}{\mathit{ac}}{\localvarsup{\dot{u}}{i}{\mathit{ac}}}

\newcommand{\Ahbridge}[1]{{\cal A}_{#1}^{ac}}
\def\Ahbridge{i}{\Ahbridge{i}}
\newcommand{\Abuck}[1]{{\cal A}_{#1}^{dc}}
\def\Abuck{i}{\Abuck{i}}

\def\localvarsup{\tau}{i}{\mathit{dc}}{\localvarsup{\tau}{i}{\mathit{dc}}}
\def\localvarsup{\delta}{i}{\mathit{dc}}{\localvarsup{\delta}{i}{\mathit{dc}}}
\def\localvarsup{T}{i}{\mathit{dc}}{\localvarsup{T}{i}{\mathit{dc}}}

\def\localvarsup{\Delta}{i}{ac}{\localvarsup{\Delta}{i}{ac}}
\newcommand{\twaitzp}[1]{\localvarsup{\delta}{#1}{\mathit{z+}}}
\def\localvarsup{\delta}{i}{\mathit{z+}}{\localvarsup{\delta}{i}{\mathit{z+}}}
\def\localvarsup{\delta}{i}{\mathit{p}}{\localvarsup{\delta}{i}{\mathit{p}}}
\def\localvarsup{\delta}{i}{\mathit{z-}}{\localvarsup{\delta}{i}{\mathit{z-}}}
\def\localvarsup{\delta}{i}{\mathit{n}}{\localvarsup{\delta}{i}{\mathit{n}}}

\def\localvar{\mathit{Nbrs}}{i}{\localvar{\mathit{Nbrs}}{i}}

\def\localvar{\mathit{F}}{i}{\localvar{\mathit{F}}{i}}
\def\localvar{\mathit{F}}{j}{\localvar{\mathit{F}}{j}}
\def\localvar{\mathit{id}}{i}{\localvar{\mathit{id}}{i}}

\def\localvarsup{\mathit{L}}{i}{F}{\localvarsup{\mathit{L}}{i}{F}}
\def\localvarsup{\mathit{R}}{i}{F}{\localvarsup{\mathit{R}}{i}{F}}

\def\mathit{ID}{\mathit{ID}}
\def\ID_{\bot}{\mathit{ID}_{\bot}}

\newcommand{\IDdef}[1]{\mathit{ID}_{#1}}
\def\IDdef{\act{F}}{\IDdef{\operatorname{\mathsf {act}}{F}}}
\def\N_{\act{F}}{\act{N}_{\operatorname{\mathsf {act}}{F}}}
\def\IDdef{\act{O}}{\IDdef{\operatorname{\mathsf {act}}{O}}}
\def\N_{\act{O}}{\act{N}_{\operatorname{\mathsf {act}}{O}}}

\defT^{ac}{T^{ac}}
\deff^{ac}{f^{ac}}

\newcommand{\poststate}[1]{#1[k+1]}
\newcommand{\prestate}[1]{#1[k]}

\newcommand{\contstate}[1]{#1(t)}

\def\mathit{Edg}{\mathit{Edg}}
\def\mathit{Rst}{\mathit{Rst}}

\newcommand{{\mathit{Grd}}}{{\mathit{Grd}}}
\def\Inv_i{Inv_i}
\newcommand{{\mathit{Inv}}}{{\mathit{Inv}}}
\newcommand{{\mathit{Init}}}{{\mathit{Init}}}
\newcommand{{\mathit{Flow}}}{{\mathit{Flow}}}
\newcommand{{\mathit{f}}}{{\mathit{f}}}
\newcommand{{\mathit{Loc}}}{{\mathit{Loc}}}
\newcommand{{\mathit{Var}}}{{\mathit{Var}}}
\newcommand{{\mathit{Trans}}}{{\mathit{Trans}}}
\newcommand{T}{T}
\newcommand{D}{D}
\newcommand{\T}{\mathit{true}}
\newcommand{g}{g}
\newcommand{u}{u}
\newcommand{\T_i}{\mathit{true}_i}
\newcommand{D_i}{D_i}

\def\mathit{Var_i}{\mathit{Var_i}}
\def\mathit{X_i}{\mathit{X_i}}
\defQ_i{Q_i}
\defq{q}
\def\mathit{v}{\mathit{v}}
\defD_i{D_i}

\def\H{\H}
\newcommand{\mathbb{R}}{\mathbb{R}}
\newcommand{\nnReal}{{\nnnum \mathbb{R}}}
\newcommand{\mathbb{R}^n}{\mathbb{R}^n}
\newcommand{\Delta}{\Delta}
\newcommand{t_{\alpha}}{t_{\alpha}}
\newcommand{t_{\beta}}{t_{\beta}}
\newcommand{\ell\mathit{oc_{1}}}{\ell\mathit{oc_{1}}}
\newcommand{\ell\mathit{oc_{2}}}{\ell\mathit{oc_{2}}}

\newcommand{\mathrm{T}}{\mathrm{T}}
\newcommand{\eglabel}[1]{\label{def:#1}}
\newcommand{\egref}[1]{Example~\ref{def:#1}}
\section{Related Work}
\seclabel{rw}
When defining the semantics of hybrid automata, first-order or higher logic is typically used and quantifiers typically show up in several places.
Existential quantifiers over reals are used to specify that some amount of real time may elapse in a given location of the hybrid automaton.
Universal quantifiers over reals representing real time are used to construct invariants that are enforced at all times, while in a given location of the hybrid automaton; otherwise real time is not allowed to advance, and a discrete transition must be taken, if any are enabled based on the current state and guards of the transitions.
Alternative approaches to the one described in this paper have previously been developed, where the universal quantifiers used to define invariant semantics are explicitly removed from the SMT expressions to create quantifier-free formulas.
That allows the use of existing SMT-based procedures and avoids quantifier-elimination and other quantifier-handling procedures~\cite{johnson2012forte,cimatti2013fmsd}.
We note those approaches do not use quantifiers on the number of steps $k \geq 0$ in the BMC computation, which we do in this paper.
Specifically, we suggest that effectively encoding the BMC problem in a quantified form over the number of steps $k$ may provide a more scalable approach in the future as quantifier handling procedures are improved in the underlying solvers.
We accomplish this by extending existing results for the BMC of discrete systems with QBF solvers~\cite{mangassarian2010tc} to timed and hybrid automata, specifically RHA.

Typical approaches that analyze timed and hybrid automata use symbolic representations of states such as difference bound matrices (DBMs) to represent clock regions in Uppaal~\cite{bengtsson1995}, HybridSAL~\cite{tiwari2012cav}, or polyhedra in HyTech~\cite{henzinger1997sttt}.
Several other formal verification tools for hybrid automata focus on performing reachability computations, and overapproximate the set of reachable states using various data structures to symbolically represent geometric sets of states, such as Taylor models in Flow*~\cite{chen2013cav} and support functions in SpaceEx~\cite{frehse2011cav}.
Reachability analysis tools like Flow* and SpaceEx focus on computing reachable states, although there is a direct equivalence between time-bounded reachability computations and BMC.

Several SMT-based approaches can verify properties of timed and hybrid automata.
dReal is an SMT-solver for first-order logic formulas over the reals, and uses a $\delta$-complete decision procedure~\cite{gao2012lics}.
dReach is a BMC tool that queries dReal to check satisfiability of SMT formulas encoding the transitions and trajectories for hybrid automata~\cite{gao2013fmcad}.
HyComp is a verification tool for networks (parallel compositions) of hybrid automata with polynomial and other dynamics~\cite{cimatti2015tacas} and is built on top of nuXmv~\cite{cavada2014cav}.
HyComp supports several verification modes, including a BMC analysis mode, $k$-induction, and IC3.
For $k$-induction and IC3, HyComp may perform unbounded model checking, but in the BMC mode, it also allows a limit on the number of steps, and also encodes the semantics of the network of hybrid automata's transition relation and trajectories. In this paper, we will compare our QBMC approach to dReach and HyComp in terms of  performing BMC for hybrid systems.

A very closely related approach to this paper also encodes BMC problems for timed automata using quantified formulas, but this quantification is to encode unknown or incomplete components, and is not a quantification over the BMC length~\cite{miller2011mtv}.
Passel is a parameterized verification tool for networks of RHA that may prove properties regardless of the number $N$ of automata in the network~\cite{johnson2012forte}.
Passel implements an extension to hybrid automata of the invisible invariants approach for parameterized verification, and consists of an invariant synthesis procedure~\cite{johnson2013infotech} that relies on reachability computations~\cite{johnson2014formats}.
Passel encodes the semantics of networks of hybrid automata as SMT formulas and checks satisfiability and validity using the Z3 SMT solver.
When performing reachability computations, Passel makes use of quantifier elimination procedures over the reals and bit-vectors~\cite{johnson2014formats}.
MCMT is another SMT-based verification tool equipped with an extensive quantifier instantiation to verify the safety properties of parametrized systems~\cite{ghilardi2010mcmt}.
In contrast, our proposed approach straightforwardly deals with quantified SMT formulas.