Hybrid Automata and $\epsilon$-Analysis on a Neural Oscillator\thanks{ This work has been partially supported by Istituto Nazionale di Alta Matematica (INdAM).}
In this paper we propose a hybrid model of a neural oscillator, obtained by partially discretizing a well-known continuous model. Our construction points out that in this case the standard techniques, based on replacing sigmoids with step functions, is not satisfactory. % Then, we study the hybrid model through both symbolic methods and approximation techniques. This last analysis, in particular, allows us to show the differences between the considered approximation approaches. % Finally, we focus on approximations via $\epsilon$-semantics, proving how these can be computed in practice.
analysis.tex
% !TEX root = main.tex
\section{Approximated Analysis over Neural Oscillator}\label{sec:analysis}
In this section we try to understand what happens when we apply the approximation techniques described in Section~\ref{sec:approx} to our neural oscillator
hybrid model $H_{\tilde{f}}$ presented in Section~\ref{sec:model}. 
\input{franzle_analysis.tex}
\input{girard_analysis.tex}
\input{epsilon_analysis.tex}

conclusions.tex
% !TEX root = main.tex
\section{Conclusions}\label{sec:conclusions}

%\begin{itemize}
%	\item	composizione di pi� oscillatori
%	\item	implementare metodi
%	\item	altre tecniche e frame work generale con topologia
%\end{itemize}

In this paper we have modeled a neural oscillator constructing a hybrid automaton
whose components derive from the approximation of the continuous model presented in~\cite{Tonnelier19991213}.
We have analyzed its behaviours considering the application of some approximation techniques for the introduction of noise, as
already advocated in ~\cite{Tonnelier19991213}.
In particular, we focused on the approach based on the $\epsilon$-semantics.

The simulation based on the application of the $\epsilon$-semantics has revealed the any point which begins its 
evolution from a distance of at least $2\epsilon$ from the limit cycle, converges to a flow tube 
which possesses a diameter equal to $2\epsilon$ and that includes the limit cycle. 
Due to size of the formul\ae\ which compose the hybrid automaton and the growth of such formal\ae\ introduced 
by the translation of the $\epsilon$-semantics evaluations, a direct computation of the reachable set would have
high complexity and eventually returns results of difficult interpretation.
For this reason, we have reformulated the problem 
in form of a closed property which guarantees the convergence of any point towards the limit cycle of the modeled system.

During the construction of the formula that describes the convergence to the 
limit cycle, some steps of simplification of the formul\ae\ have been applied. In particular, 
we have reduced the complexities of translated formul\ae, 
relying on the convexity of the sets characterized by some of their subformul\ae.
An interesting aspect to investigate is whether these simplification steps 
can be automatically performed. 

As future work, in order to analyze the behaviour of a group of neural oscillators, we plan 
to combine several hybrid automata and to study their evolutions always adopting
%the approximation approach based on the 
$\epsilon$-semantics. 
epsilon-sem.tex
% !TEX root = main.tex
\subsection{$\epsilon$-Semantics}\label{sec:epsilon}

The undecidability of the reachability problem over hybrid automata having bounded invariants is a direct
consequence of the ability of characterizing dense regions of arbitrarily small size. 
As noticed in~\cite{DBLP:journals/deds/CasagrandePP09}, especially in the study of biological systems,
such ability may result misleading. As a matter of the fact, the continuous quantities used in hybrid automata
are very often abstractions of large, but discrete, quantities. 
In such cases, the ability of handling values with infinite precision is a model artifact rather than 
a real property of the original system. 

In order to discretize the continuous space, we introduce the concept of
\emph{$\epsilon$-sphere}. Given a set $\mathbb{S} \subseteq \mathbb{R}^n$, the
$\epsilon$-sphere $B(\mathbb{S},\epsilon)$ is the subset of $\mathbb{R}^n$
of points at distance less than $\epsilon$ from $\mathbb{S}$, i.e.,
$B(\mathbb{S},\epsilon) = \{ q \in \mathbb{R}^n \mid \exists p \in \mathbb{S}( \edist(p,q) < \epsilon) \}$,
where $\edist$ is a %the standard euclidean 
distance 
function 
over $\mathbb{R}^n$ (e.g., the standard euclidean distance). Moreover, given a hybrid
automaton $H$ and an initial set of points $\mathbb{I} \subseteq \bbbr^{\dims{H}}$, the
set of points reachable from the set $\mathbb{I}$ by $H$, denoted by $RSet_H(\mathbb{I})$, is
characterized by
%\begin{equation*}
$\ReachSet{H}{\mathbb{I}} = \bigcup_{i \in \mathbb{N}} \ReachSet[i]{H}{\mathbb{I}} = \lim_{i \rightarrow +\infty} \ReachSet[i]{H}{\mathbb{I}}$
%\end{equation*}
where $\ReachSet[i]{H}{\mathbb{I}}$ is the set of points reachable from $\mathbb{I}$ in at
most $i$ discrete transitions.

\begin{theorem}[\cite{DBLP:journals/deds/CasagrandePP09}]
	Let $\mathcal{T}$ be a decidable first-order theory over reals and $H$ be a $\mathcal{T}$
	hybrid automaton with bounded invariants. If there exists $\epsilon \in \mathbb{R}_{> 0}$
	such that, for each $\mathbb{I} \subseteq \bbbr^{\dims{H}}$ and for each $i \in \mathbb{N}$,
	either $\ReachSet[i+1]{H}{\mathbb{I}} = \ReachSet[i]{H}{\mathbb{I}}$ or there exists an $a_i \in \mathbb{R}^{d(H)}$
	such that $B(\{a_i\},\epsilon) \subseteq \ReachSet[i+1]{H}{\mathbb{I}} \setminus \ReachSet[i]{H}{\mathbb{I}}$,
	then there exists $j \in \mathbb{N}$ such that $\ReachSet[i]{H}{\mathbb{I}} = \ReachSet[j]{H}{\mathbb{I}}$ and
	the reachability problem over $H$ is decidable.
\end{theorem}

This result finds applications when it makes no sense to distinguish measurements smaller than $\epsilon$.
Hence, since hybrid automata characterization is based on first-order fromul\ae, it seems reasonable to reinterpret the 
semantics of semi-algebraic automata by giving to each formula a semantics of \lq\lq dimension
of at least $\epsilon$\rq\rq. 
In~\cite{DBLP:journals/deds/CasagrandePP09} the authors introduce a new class of semantics, 
called \emph{$\epsilon$-semantics}, which guarantee the decidability of reachability
in the case of hybrid automata with bounded invariants.

%\begin{definition}[$\epsilon$-Semantics]\label{def:eps_semantics}	
%	Let $\mathcal{T}$ be a first order theory and let $\epsilon \in \mathbb{R}_{\geq 0}$.
%	For each formula $\psi$ on $\mathcal{T}$ let $\{| \psi |\}_\epsilon \subseteq \mathbb{R}^d$,
%	where $d$ is the number of free variables of $\psi$, be such that:\\
%	\\
%	\begin{tabular}{l l}
%		$(\epsilon)$	&	either $\epssem{\psi} = \emptyset$ or there exists 
%						$p \in \mathbb{R}^d$ such that $B(\{ p \}, \epsilon) \subseteq \gsems{\psi}$; \\
%		$(\cap)$		&	$\epssem{\phi \wedge \varphi } \subseteq \epssem{\psi} \cap \epssem{ \varphi}$ \\
%		$(\cup)$		&	$\epssem{ \phi \vee \varphi } = \epssem{ \phi } \cup \epssem{ \varphi }$ \\
%		$(\forall)$		&	$\epssem{ \forall X \psi[X,Z] } = \epssem{ \bigwedge_{r \in \mathbb{R}} \psi[r,Z] }$\\
%		$(\exists)$	&	$\{| \exists X \psi[X,Z] |\}_\epsilon = \bigcup_{r \in \mathbb{R}} \epssem{ \psi[r,Z] }$\\	
%		$(\neg)$		&	$\{| \psi |\}_\epsilon \cap \{| \neg\psi |\}_\epsilon = \emptyset$	\\
%	\end{tabular}\\
%	\\
%	Any semantics satisfying the above conditions is said
%	to be an \emph{$\epsilon$-semantics for $\mathcal{T}$}.
%	
%\end{definition}

\begin{definition}\label{gen:schema}
Let  $\Theory$ be a first-order theory and let $\epsilon \in \bbbr_{>0}$.
For each formula $\psi$ on $\Theory$ let $\epssem{ \psi }\subseteq \bbbr^d$, where $d$ is the number of free variables of $\psi$, be such that:
\begin{itemize}
 \item[($\epsilon$)] either $\epssem{ \psi }=\emptyset$ or there exists $p\in \mathbb R^d$ such that $\eball{\{p\}}\subseteq \epssem{ \psi }$;
 \end{itemize}
\begin{minipage}[b]{0.5\linewidth}
\begin{itemize}
\item[($\cap$)] $\epssem{ \phi\land \varphi} \subseteq \epssem{ \phi} \cap \epssem{\varphi}$;
\item[($\cup$)] $\epssem{ \phi\lor \varphi} = \epssem{ \phi} \cup \epssem{\varphi}$;
\end{itemize}
\end{minipage}
\begin{minipage}[b]{0.5\linewidth}
\begin{itemize}
\item[($\forall$)] $\epssem{ \forall \X{} \NotBoundIn{\psi}{\X{},\vX{}} } = 
\epssem{\bigwedge_{r \in \bbbr} \VarSSub{\psi}{r,\vX{}}}$;
\item[($\exists$)] $\epssem{ \exists \X{} \NotBoundIn{\psi}{\X{},\vX{}} } = 
\epssem{\bigvee_{r \in \bbbr} \VarSSub{\psi}{r,\vX{}} }$;
\end{itemize}
\end{minipage}
\begin{itemize}
\item[($\neg$)] $\epssem{ \psi }\cap \epssem{ \neg \psi }=\emptyset$.
\end{itemize}
Any semantics satisfying the above conditions is said to be an 
\emph{$\epsilon$-semantics for $\Theory$}. 
%A semantics which satisfies conditions $(\epsilon)$, $(\cap)$, $(\neg)$
%is said to be a \emph{quasi-$\epsilon$-semantics}.
\end{definition}

Let us notice that 
%due to the ($\neg$)-rule, 
no $\epsilon$-semantics can over-approximate 
the standard semantics. Infact, 
for any theory $\Theory$, if $\stdsem{\phi} \subset \epssem{\phi}$, 
where $\stdsem{\cdot}$ is the semantics 
associated to $\Theory$, then $\stdsem{\neg \phi} \supset \epssem{\neg \phi}$ due to the ($\neg$)-rule.

\begin{example}[The sphere semantics]
%\begin{definition}[Sphere Semantics]
\label{spheresemantics}%[First-order $\epsilon$-semantics]
Let $\Theory$ be a first-order theory over the reals and let $\epsilon >0$. 
%Moreover,
%let $\ssem{\psi}{}$ be the 
%set of points satisfying $\psi$, for each formula $\psi$ in a theory $\Theory$, 
%with the standard semantics of $\Theory$. 
The \emph{sphere semantics} of $\psi$, $\sphsem{\psi}$, is defined by structural induction on $\psi$ as 
follows:

\begin{minipage}[b]{0.5\linewidth}
\begin{itemize}
\item $\sphsem{t_1 \circ t_2}\defeq\eball{\stdsem{t_1\circ t_2}}$, for $\circ \in \{=,<\}$;
\item $\sphsem{ \psi_1\wedge \psi_2}\defeq\bigcup_{\eball{\{p\}}\subseteq \sphsem{ \psi_1}\cap \sphsem{\psi_2}}\eball{\{p\}}$;
\item $\sphsem{ \psi_1\vee \psi_2}\defeq\sphsem{ \psi_1}\cup \sphsem{ \psi_2}$;
 \end{itemize}
 \end{minipage}
\begin{minipage}[b]{0.5\linewidth}
\begin{itemize}
\item $\sphsem{ \forall \X{} \VarSSub{\psi}{\X{},\vX{}} } \defeq
\sphsem{\bigwedge_{r \in \bbbr}  \VarSSub{\psi}{r,\vX{}}}$;
\item $\sphsem{ \exists \X{} \VarSSub{\psi}{\X{},\vX{}{}} } \defeq
\sphsem{\bigvee_{r \in \bbbr} \VarSSub{\psi}{r,\vX{}{}} }$;
\item $\sphsem{ \neg \psi }\defeq \bigcup_{\eball{\{p\}}\cap \sphsem{ \psi}=\emptyset}\eball{\{p\}}$.
 \end{itemize}
\end{minipage}
\end{example}

%In the above definition, with a slight abuse of notation, we
%use $\bigwedge_{r\in \mathbb R}\psi$ to treat an infinite conjunction of formul\ae~as a formula.
	
$\epsilon$-semantics are exploited in the reachability algorithm defined in~\cite{DBLP:journals/deds/CasagrandePP09}.
%
%In particular, describing sets of points through formul\ae~and, given a hybrid automaton $H$ and an $\epsilon$-semantics
%$\epssem{\cdot}$, the computation of the algorithm proceeds as follows:
%\begin{enumerate}
%	\item
%		Given an initial set of points represented by a formula $\NotBoundIn{I}{\vX{}}$, the formula $\NotBoundIn{R}{\vX{}}$ is initialized putting 
%		$\NotBoundIn{I}{\vX{}}$ in conjunction with the invariant conditions of $H$, while the formula $\NotBoundIn{N}{\vX{}}$ is initialized as $\False$;
%	\item\label{step2}
%		$\NotBoundIn{R}{\vX{}}$ is replaced with $\NotBoundIn{R}{\vX{}}\lor \NotBoundIn{N}{\vX{}}$ and  
%		$\NotBoundIn{N}{\vX{}}$ becomes $\exists \vX{}' (\VarSSub{\oReachDef_{H}}{\vX{}',\vX{}}\land \VarSSub{R}{\vX{}'})$, where the formula $\NotBoundIn{\oReachDef_{H}}{\vX{},\vX{}'}$
%		denotes automaton evolutions which perform at most one discrete transition, i.e., if $\VarSSub{\oReachDef_{H}}{s,d}$, then $H$ reaches $d$ from $s$ with at most one discrete transition;
%    	\item
%    		Step~\ref{step2} is repeated until $\epssem{ N[\vX{}]\land \neg R[\vX{}] }$ is not empty.	
%\end{enumerate}
%
%\begin{algorithm}
%	\caption{Reachability($H,\NotBoundIn{I}{\vX{}},\epssem{\cdot}$)}
%	\label{algo:reachability}
%	\begin{algorithmic}[1]
%	    \STATE $\NotBoundIn{R}{\vX{}}\leftarrow \NotBoundIn{I}{\vX{}}$
%	    \STATE $\NotBoundIn{N}{\vX{}}\leftarrow \False$
%		\REPEAT 
%		\STATE $\NotBoundIn{R}{\vX{}}\leftarrow \NotBoundIn{R}{\vX{}}\lor \NotBoundIn{N}{\vX{}}$
%		\STATE $\NotBoundIn{N}{\vX{}}\leftarrow \exists \vX{}' (\VarSSub{\oReachDef_{H}}{\vX{}',\vX{}}\land \VarSSub{R}{\vX{}'})$
%		\UNTIL {$\epssem{\NotBoundIn{N}{\vX{}}\land \neg \NotBoundIn{R}{\vX{}} } \neq \emptyset$} 
%		\RETURN $\epssem{\NotBoundIn{R}{\vX{}}}$
%	\end{algorithmic}
%\end{algorithm}
%
Intuitively, the algorithm computes reachability incrementing the number
of allowed discrete transitions at each iteration. New reachable sets of points are computed until
they became too small to be captured by the $\epsilon$-semantics.	
In the case of hybrid automata with bounded invariants, it 
always terminates. 
Finally, notice that replacing the $\epsilon$-semantics with the standard one,
the above algorithm could not terminate even with bounded invariants, due to Zeno behaviours.
%Let us notice that, %, any differentiable function $f$ can be approximated 
%on a given interval $I$ with a maximum error $\gamma$ 
%by a polynomial $p$. Hence, 

To conclude, let us notice that, by Taylor's approximation, for any $\epsilon$ and any differentiable function $f(t)$, 
if we fix a time horizon $t_{h}$, we can approximate $f(t)$ 
by a polynomial $p(t)$ such that $\|f(t)-p(t)\|<\epsilon$ for all 
$t\in [0,t_{h}]$. Hence, there are $\epsilon$-semantics that are not able to distinguish 
$p(t)$ and $f(t)$ and, according to such $\epsilon$-semantics, we can use $p(t)$ in place of $f(t)$ for all $t \in [0,t_{h}]$.
It follows that, adopting an opportune $\epsilon$-semantics, the Tarski's theory (i.e., the first order theory of 
the inequalities over the reals) is enough to represent any differentiable function 
$f(t)$. 




epsilon_analysis.tex
% !TEX root = main.tex
\subsection{$\epsilon$-semantics}\label{subsec:epsilon_analysis}
In order to exploit $\epsilon$-semantics for the study of $H_{\tilde{f}}$ the
first step we have to perform is that of approximating through polynomials
the solutions of the differential equations defining the semantics.
This can be done, for instance, by using Taylor polynomials or more sophisticated
numerical integration techniques.
We do this in the next section, where we also apply cylindrical algebraic decomposition
tools to automatically prove properties of our model.
Here instead we try to infer some general results about the use of $\epsilon$-semantics on
$H_{\tilde{f}}$.

$H_{\tilde{f}}$ has an unstable equilibrium in $\tuple{0,0}$. This means that
$\tuple{0,0}$ reaches $\{\tuple{0,0}\}$. However, when we compute the set of points
reachable from $\tuple{0,0}$ through an $\epsilon$-semantics we get either 
the empty set or a set having diameter at least $\epsilon$.
In particular, if our $\epsilon$-semantics under-approximates the standard
one (i.e., if $\stdsem{\phi} \supset \epssem{\phi}$, 
where $\stdsem{\cdot}$ is the semantics 
associated to chosen theory, for each formula $\phi$), then we get the empty set. Otherwise, both cases are possible, depending
on the $\epsilon$-semantics. For instance, in the case of sphere semantics,
no matter how we approximate the dynamics, we get that $\tuple{0,0}$ reaches
a set having diameter at least $\epsilon$.
%
Similarly, unless we use an under-approximation $\epsilon$-semantics or 
some unusual metrics, the limit cycle is transformed into a limit flow tube.
This means that, if we consider a point on the limit cycle and we compute the
set of points reachable from such point, then we do not only obtain the limit cycle, but
at least a flow tube which includes the limit cycle. We will see some more
details on this in the case of sphere semantics in Section~\ref{sec:computing}.
%
All the other points, again, will reach either the empty set or a set having diameter
at least $\epsilon$. The result we would expect in this second case is that each point in the
space reaches the flow tube including the limit cycle. We will see that this is true in the case
of sphere semantics, even when we use the simplest Taylor polynomials of degree one. 

These considerations already allow us to point out that sphere semantics better reflects 
the real system behaviour than the standard one. 
eptcsdata.tex
\providecommand{\firstpage}{58}
\providecommand{\publicationstatus}{Ezio Bartocci and Luca Bortolussi (Eds.): HSB 2012\\
EPTCS 92, 2012, pp.\ \pageref*{FirstPage}--\pageref{LastPage},
doi:\href{http://dx.doi.org/10.4204/EPTCS.92.5}{10.4204/EPTCS.92.5}}
\pdfoutput=1

franzle.tex
% !TEX root = main.tex
\section{Approximation Techniques}\label{sec:approx}
\subsection{Noise and Disturbed Automata}\label{sec:franzle}
The density of continuous variables provide an unbounded quantity of memory within a bounded region.
As a matter of fact, the undecidability results proved in \cite{undecidable} are based on 
the possibility of embedding $\mathbb{N}$ in $(0,1]\subseteq \bbbr$ through the function $f(n)=2^{-n}$.

However, Fr\"anzle in \cite{franzle99} observed that noise disturbes the trajectiories of real hybrid systems,
augmenting the set of reachable points. %Hence, in 
Hence, in \cite{franzle99} a model of noise has been presented over hybrid automata.
Remarkably, the introduction of noise ensures in many cases the (semi-)decidability of the reachability problem.

Our definitions of hybrid automata slightly differ from the ones in \cite{franzle99}. In particular, as far as the syntax is concerned, the formul\ae\ $\ActDef{e}$ and $\HResetDef{e}$ are glued together in a formula called $trans_{e}[\vX{},\vX{}']$. Moreover, our formul\ae\ $\InvDef{v}$ and $\DynDef{v}$ are replaced by a single formula $act_{v}[\vX{},\vX{}']$ whose meaning in our framework is:
$$\begin{array}{l}\exists T(T\geq 0\wedge \vX{}'=\vfFunct{v}(\vX{})(T)\wedge \forall T'(0\leq T'\leq T \rightarrow \Inv{v}{\vfFunct{v}(\vX{})(T')})), 
\end{array}$$
i.e., the formula $act_{v}[\vX{},\vX{}']$ syntactically ensures the existence of a continuous transition.
Exploiting these relationships between our hybrid automata and the hybrid automata defined through the formul\ae\ 
$act_{v}[\vX{},\vX{}']$ and $trans_{e}[\vX{},\vX{}']$, we can reformulate the results presented in \cite{franzle99} in our framework.

\begin{definition}
Given a hybrid automaton $H=\langle\vX{}$, $\vX{}'$, $\Loc$, $\Edg$, $\InvSymb$,
   $\vfFunct{\cdot}$,  $\ActSymb$, $\ResetSymb\rangle$ we say that the hybrid automaton $\widetilde{H}=\langle\vX{}$, $\vX{}'$, $\Loc$, $\Edg$, $\widetilde{\InvSymb}$,
   $\widetilde{\vfFunct{\cdot}}$,  $\ActSymb$, $\ResetSymb\rangle$ is a \emph{disturbed variant} of $H$ if for each pair of states $\hstate{},\hstate{}'$ if $\hstate{}\actrans\hstate{}'$ in $H$, then $\hstate{}\actrans\hstate{}'$ in $\widetilde{H}$. 

Moreover, let $\edist$ be a distance over $\bbbr^{\dims{H}}$ and $\epsilon\in \bbbr_{>0}$.
$\widetilde{H}$ is a \emph{disturbance of noise level $\epsilon$ or more} if for each $s,s'$ such that $\edist(s,s')<\epsilon$ it holds that if $\state{v}{r}\actrans \state{v}{s}$ in $H$, then $\state{v}{r}\actrans \state{v}{s'}$ in $\widetilde{H}$.
\end{definition}

Intuitively, when there are no bifurcation behaviours, a small $\epsilon$ ensures that the dynamics of 
$\widetilde{H}$ are close to those of $H$.

In \cite{franzle99} it has been proved that in the case of bounded invariants there exists a finite computable index $i\in \mathbb N$ such that the reachability over $H$ can be over-approximated with reachability within $i$ discrete jumps over a disturbance of noise level $\epsilon$ or more of $H$. 

\begin{theorem}{\cite{franzle99}}
Let $\Theory$ be a decidable first-order theory.
Let $H,\widetilde{H}$ be $\Theory$ hybrid automata, with $\widetilde{H}$ disturbance of noise level $\epsilon$ or more of $H$ for some $\epsilon\in \bbbr_{>0}$. There exists $i$ such that for all pairs of states $\hstate{},\hstate{}'$ if $\hstate{}$ reaches $\hstate{}'$ in $H$, then $\hstate{}$ reaches $\hstate{}'$ in $\widetilde{H}$ within $i$ discrete transitions.
Moreover, $i$ can be effectively computed. 
\end{theorem}

%In particular, this result can be algorithmically stated has follows:
%\begin{itemize}
%\item[(1)] start from an initial set of points $I$
%\item[(2)] compute the set of points $C$ reachable from $I$ through a continuos transition
%\item[(3)] expand $C$ of $\epsilon$
%\item[(4)] compute the set of points $D$ reachable from $C$ through a discrete transition
%\item[(5)] it the set of points reachable from $D$ through a continuous and a discrete transition is included in $D$, then halt, otherwise replace $I$ with $D$ and go back to (2)
%\end{itemize}

Unfortunately, there are cases in which the over-approximation is always strict, no matter how small $\epsilon$ is. Such automata are called \emph{fragile}, in contrast with \emph{robust} automata, where if $\hstate{}$ does not reach $\hstate{}'$ in $H$, there exist $\epsilon \in \bbbr_{>0}$ and $\widetilde{H}$ disturbance of noise level $\epsilon$ such that $\hstate{}$ does not reach $\hstate{}'$ in $\widetilde{H}$. As a consequence, reachability is decidable over robust automata, while it is only semi-decidable over fragile automata. It is not possible to decide whether a hybrid automaton is robust or fragile. 
Intuitively, since real world systems are always subject to noise, a hybrid automaton is a reliable model of the real system only if it is robust. So, it is fundamental to develop and exploit design techniques which ensure robustness of the resulting hybrid automata.

franzle_analysis.tex
% !TEX root = main.tex
\subsection{$\epsilon$-disturbance}\label{subsec:franzle_analysis}
The automaton $H_{\tilde{f}}$ presents two main behaviours: $\tuple{0,0}$ is an unstable equilibrium;
each starting point different from $\tuple{0,0}$ reaches the limit cycle.
For this reason we can prove that $H_{\tilde{f}}$ is fragile. As a matter of fact, if $\widetilde{H_{\tilde{f}}}$ is
a disturbance of noise level $\epsilon$ of $H_{\tilde{f}}$, then $(0,0)$ in $\widetilde{H_{\tilde{f}}}$ reaches points 
different from $\tuple{0,0}$, while in $H_{\tilde{f}}$ it does not. In other words, if we consider backward reachability, $\tuple{0,0}$ is backward
reachable in $\widetilde{H_{\tilde{f}}}$  from a region $R\neq \{(0,0)\}$, while in $H_{\tilde{f}}$ it is backward reachable from
$\{\tuple{0,0}\}$.
This is not due to the fact that $\tuple{0,0}$ is unstable, but to the presence of two limit behaviours over a connected region.
We recall that in a piecewise hybrid automaton the invariants are connected disjoint regions whose union is connected and the resets are identities, i.e., 
the trajectories are continuos. We use the term \emph{limit behaviour} of a hybrid automaton to denote both equilibria and limit 
cycles.
\begin{theorem}
Let $H$ be a piecewise hybrid automaton presenting at least two different limit behaviours. 
If from each point there is a unique possible evolution, then $H$ is fragile.
\end{theorem}
%\begin{proof}
%Let $b_1$ and $b_2$ be two different limit behaviours.
%Let $I$ be the union of the invariants of $H$. 
%Let $R_1=\{r\:|\: r \mbox{ reaches } b_1 \mbox{ but not }b_2\}$ and $R_2=\complement_I(R_1)=I\setminus R_1$.
%Moreover, let $b_2$ be the unsafe set and $R_1$ be the init set. $H$ is safe since the points in $R_1$ do not reach
%$b_2$. 
%
%We have that $R_1\neq \emptyset$, since the points belonging to $b_1$ reach $b_1$ and they cannot reach $b_2$, 
%since the evolutions are uniquely defined from each starting point. Similarly $R_2\neq \emptyset$. Hence, $\{R_1,R_2\}$ is 
%a partition of $I$. Since $I$ is connected, for each $\epsilon\in \mathbb R_{>0}$ there are $p_1\in R_1$ and $p_2\in R_2$, 
%such that $\delta(p_1,p_2)<\epsilon$. So, $p_1$ reaches $p_1$ in $H$, implies that $p_1$ reaches $p_2$ in $\widetilde{H}$ 
%disturbance of noise level $\epsilon$ or more of $H$. So, since $p_2\in R_2$ reaches $b_2$ in $H$, we get that 
%$p_1$ reaches $b_2$ in $\widetilde{H}$. Since, we made no assumption on $\epsilon$, we get that all the disturbances 
%of noise level $\epsilon$ or more of $H$ are unsafe, this means that $H$ is fragile.
%\end{proof}
The above result points out that there are systems for which it is not possible to define robust models.
In~\cite{DBLP:conf/tamc/Ratschan10} a model is said to be safe only if it remains safe under small disturbances. In this 
terms our result shows that
there are systems which do not admit a safe model. This does not means that they are not interesting or that we need to 
remove
some of their behaviours. This simply means that such systems have to be studied applying some form of disturbance or 
approximation. As the matter of facts, if we study them by applying standard semantics, we define a precise border between 
the points reaching different
behaviours. Such precise border is not realistic. 
 
girard.tex
% !TEX root = main.tex
\subsection{Approximate Bisimulations and Simulations}\label{sec:girard}

Since the 90's, simulation and bisimulation have been successfully used to investigate hybrid automata. 
However, due to the infinite precision required to relate different evolutions, these tools are able to 
remove neither the complexity nor the undecidability issues that may affect the analysis of the 
investigated model. 
The $\epsilon$-(bi)simulation relations~\cite{Girard:2007fk} relaxes these infinite precision requirements  by 
relating system evolutions whose maximal distance is less than a given $\epsilon$. 
This enables us to simplify both the dynamics and the resets of the investigated automaton. 
Moreover, provided an \emph{observation map} 
 $\obmap{\cdot}:\bbbr^{\dims{H}} \longrightarrow \bbbr^{d}$ that associates the internal status of an automaton $H$  
 to the values measurable by an external observer, $\epsilon$-(bi)simulations 
 allow to relate the ``visible'' behaviours of $H$ to 
 the behaviours of an automaton whose dimension is smaller than $\dims{H}$. 

%Since there exists a simulation from $H_1$ to $H_2$ if and only if they have the same discrete structure, 
%we always assume that $H_1$ and $H_2$ 
Any pair of hybrid automata $H_1$ to $H_2$ 
related by an $\epsilon$-simulation must have the same discrete structure and share the same 
locations $\Loc$ and edges $\Edg$ by definition. 

\begin{definition}
Let $H_i=\langle\vX{i}$, $\vX{i}'$, $\Loc$, $\Edg$, $\InvSymb_i$,
   $\vfFunct{\cdot,i}$,  $\ActSymb_i$, $\ResetSymb_i\rangle$ be a hybrid automaton
    %and $\obmap{\cdot}_i$ an observation map for $H_i$ 
    for each $i \in \{1,2\}$. 
   Moreover, let $\epsilon$ be in $\bbbr_{\geq 0}$. 
A relation $\mathcal{S}_{\epsilon} \subseteq  (\Loc \times \bbbr^{\dims{H_1}}) \times 
   (\Loc \times \bbbr^{\dims{H_2}})$ is an \emph{approximate simulation relation of 
  $H_1$ %, $\obmap{\cdot}_1$ 
  by $H_2$ %, $\obmap{\cdot}_2$ 
  of precision $\epsilon$}
  if, for all $\tuple{\state{\hloc{1}}{r_1}, \state{\hloc{2}}{r_2}} \in \mathcal{S}_{\epsilon}$: 
  \begin{enumerate}
  \item $\hloc{1}=\hloc{2}=\hloc{}$;
  \item $\|\obmap{r_1}_1-\obmap{r_2}_2\| \leq \epsilon $;
  \item if  $\state{\hloc{}}{r_1} \ctrans{t} \state{\hloc{}}{r_1'}$ in $H_1$, 
  there exists $r_2'$ s.t.~$\state{v}{r_2} \ctrans{t} \state{v}{r_2'}$ in $H_2$ and 
  $\tuple{\state{\hloc{}}{r_1'}, \state{\hloc{}}{r_2'}} \in \mathcal{S}_{\epsilon}$;
  \item  if  $\state{\hloc{}}{r_1} \dtrans{e} \state{\hloc{}'}{r_1'}$ in $H_1$, 
  there exists $r_2'$ s.t.~$\state{\hloc{}}{r_2} \dtrans{e} \state{\hloc{}'}{r_2'}$ in $H_2$ and 
  $\tuple{\state{\hloc{}'}{r_1'}, \state{\hloc{}'}{r_2'}} \in \mathcal{S}_{\epsilon}$.
   \end{enumerate}
\end{definition}

The automaton $H_2$ %,$\obmap{\cdot}_2$ 
approximately simulates $H_1$ %,$\obmap{\cdot}_1$ 
with precision $\epsilon$ if there exists an approximate simulation relation of 
  $H_1$ %, $\obmap{\cdot}_1$ 
  by $H_2$ %, $\obmap{\cdot}_2$ 
  of precision $\epsilon$. 
%  
%\begin{definition}
An approximate simulation relation $\mathcal{S}_{\epsilon}$ of 
  $H_1$ %, $\obmap{\cdot}_1$ 
  by $H_2$ %, $\obmap{\cdot}_2$ 
  of precision $\epsilon$ is an 
  \emph{approximate bisimulation relation between 
  $H_1$ %, $\obmap{\cdot}_1$ 
  and $H_2$ %, $\obmap{\cdot}_2$ 
  of precision $\epsilon$}
  if the relation $\mathcal{S}_{\epsilon}^{-1}=\{\tuple{\hstate{2},\hstate{1}} \, |\, \tuple{\hstate{1},\hstate{2}} \in \mathcal{S}_{\epsilon}\}$ 
  is an approximate simulation relation  of 
  $H_2$ %, $\obmap{\cdot}_2$ 
  by $H_1$ %, $\obmap{\cdot}_1$ 
  of precision $\epsilon$.
%\end{definition}  

Many methods have been developed 
to automatically compute approximate simulation relations 
between systems such as 
constrained linear systems, 
autonomous nonlinear systems, and 
hybrid systems.
%, and  
%\cite{Julius:2009:Approximation} for stochastic hybrid systems.





girard_analysis.tex
% !TEX root = main.tex
\subsection{$\epsilon$-(bi)simulations}\label{subsec:girard_analysis}


The automaton $H_{\tilde{f}}$ has both an unstable equilibrium in $\tuple{0,0}$ and a single limit 
cycle encompassing the origin of the axes. 
Because of that we are guaranteed that,  during its evolutions, 
$H_{\tilde{f}}$ decreases the 
distance of its state from the limit cycle 
regardless of the starting state $s\neq \state{v_0}{\tuple{0,0}}$. 
Since all the differential equations defining the dynamics of $H_{\tilde{f}}$ are continuous,  
we can define an $\epsilon$-simulation between states whose distance 
from the limit cycle is smaller than $\epsilon$. 
%
%there exist $\epsilon_i$ and $\epsilon_e$, where  $\epsilon_e$ is bigger $\epsilon_i$ and depends on it, 
%such that the relation that associates each states $\state{v_i}{q}$ in the limit cycles 
%with all the states $\state{v_i}{r}$ in the $\epsilon_i$-expansion of 
%the limit cycle is a time-abstract $\epsilon_e$-simulation of $H_{\tilde{f}}$.
This enables us to both approximate the non-linear differential System (\ref{eq:origsystem})
 with a linear differential system and reduce  the complexity of 
the analysis. 

However, if $d$ is the maximum 
Euclidean distance between $\tuple{0,0}$ and the cycle limit,  
no $\epsilon$-(bi)si\-mu\-la\-tion, 
%between states of $H_{\tilde{f}}$, 
with $\epsilon<d$,   
can relate $\state{v_0}{\tuple{0,0}}$ with any other state 
of $H_{\tilde{f}}$. As a matter of fact, the points belonging to any 
neighborhood of $\tuple{0,0}$ eventually converge to 
the limit cycle.
It follows that $\state{v_0}{\tuple{0,0}}$ is 
a singularity of the model and, despite the original system 
always reaches a periodic evolution, any approximation of the proposed 
model by mean of $\epsilon$-(bi)simulation does not manifest this 
property. 

hybrid.tex
% !TEX root = main.tex
\subsection{Syntax, Semantics, and Reachability}\label{sec:hybrid}

%
%In order to formally define hybrid automata, 
%we first need to introduce some conventions. %we use on hybrid automata.
%Capital letters 
%$\X{}$ and $\Xp{}$, where $m \in\bbbn$, denote 
%variables ranging over $\bbbr$. 
%%Analogously, the bold letters $\vX{}{}$ and $\vX{}'$ 
%%represent vectors of real variables. 
%The temporal variable $T$ model time and ranges over $\bbbr_{\geq 0}$. We use the lowercase letters $p$,
%$q$, $r$, $s$, 
% $\dots$ to denote vectors of real values.

A hybrid automaton is an infinite state automaton that consists in a 
set of continuos variables and a finite directed graph. 
Each node of a graph is labelled by both an invariant condition and a
dynamic law, while all the edges are tagged with an activation region and 
a reset map. 
The continuous variables evolve according to the dynamic law 
of the current node of the graph and the node's 
invariant condition must be satisfied along all the evolution. 
An edge is crossable if and only if the variable values are included the 
activation region and, when a hybrid automata jumps over it, 
the associated reset map is applied. 

\begin{definition}[Hybrid Automata - Syntax]\label{def:hyau}
   A \emph{hybrid automaton} $H$ of dimension $\dims{H} \in \bbbn$ is a tuple 
   $\langle\vX{}{}$, $\vX{}'$, $\Loc$, $\Edg$, $\InvSymb$,
   $\vfFunct{\cdot}$,  $\ActSymb$, $\ResetSymb\rangle$ where:
   \begin{itemize}
   \item $\vX{}{}=\langle\X{1}$, $\ldots$, $\X{n}\rangle$ and
   $\vX{}'=\langle\X{1}'$, $\ldots$, $\X{n}'\rangle$ are two vectors of
   variables ranging over the reals $\bbbr$;
   \item $\langle \Loc$,  $\Edg\rangle$ is a directed finite graph, i.e., $\Edg\subseteq \Loc\times \Loc$. Each element
   of $\Loc$ will be dubbed \emph{location};
   %For each $e \in \Edg$, $\eSrc{e}$ and $\eDst{e}$ denote the 
   %source and the destination of $e$, respectively; 
   \item Each location $v\in \Loc$ is labelled by both a formula
   $\InvDef{\hloc{}}$, called \emph{invariant}, and a continuous function 
   $\vfFunct{\hloc{}}: \bbbr^{n} \longrightarrow (\bbbr_{\geq 0} \longrightarrow \bbbr^{n})$, 
   called  \emph{dynamics} or \emph{flow function}. The dynamics may be specified either by differential equations, i.e., $\vfFunct{\hloc{}}$ is the solution 
of a given Cauchy problem, or by a logic formula. We use the formula 
$\DynDef{\hloc{}}$, where $T$ is a temporal variable ranging in $\bbbr_{\geq 0}$, to denote the dynamics on
$v$, i.e., $\DynDef{\hloc{}}\defeq \vX{}'=\vfFunct{\hloc{}}(\vX{}{})(T)$;
   \item Each $e\in \Edg$ is labelled by the formul\ae\
   $\ActDef{e}$ and $\HResetDef{e}$ which are
   called \emph{activation} and \emph{reset}, respectively.
%;
%   $\RSetF{e}[\vX{}'] \defeq \exists \vX{}{} \ \HReset{e}{\vX{}{},\vX{}'}$.
\end{itemize}
\end{definition}

%Whenever the dynamics are given as 
%differential equations, they benefit from the properties of the differential equations themselves.
%For instance, the solutions of a vector field are derivable and transitive.

%We may write $\dims{H}$ to denote the dimensions of $H$. 
%
If %$\DynDef(v)$, $\InvDef(v)$, $\ActDef(e)$, and $\ResetDef(e)$ are formul\ae\ belonging 
all the formul\ae\ that define a hybrid automaton $H$ belong
to
the same logical theory $\Theory$, then
we say 
%equivalently 
that $H$ is \emph{definable in $\Theory$} or that $H$ is a
\emph{$\Theory$ hybrid automaton}.

%If a reset does not depend on the $\vX{}{}$ interpretation (i.e., 
%for any $p$, $q$, and $p'$ in $\bbbr^{\dims{H}}$,  
%if both $\HReset{e}{p,q}$ holds, then $\HReset{e}{p',q}$ holds too), 
%we say that the reset is \emph{constant}.


%We present hybrid automaton semantics as transition systems: 
%Given a hybrid automaton and an initial state for it (i.e., a pair mode-values for the real 
%variables), 
%the evolution of the automaton corresponds to the iterative application of the transition relation 
%associated to the automaton itself. 
The semantics of any hybrid automaton can be specified as a transition system that 
 is composed by two different relations 
miming the double nature of the hybrid automaton itself: the 
\emph{continuous reachability transition relation} and the \emph{discrete reachability transition 
relation}.

\begin{definition}[Hybrid Automaton - Semantics]\label{def:semantics}
A \emph{state} $\hstate{}$ of $H$ is a pair $\state{\hloc{}}{r}$, where $v\in \Loc$
is a location and $r\in \bbbr^{\dims{H}}$ 
is an assignment of values for the variables of $\vX{}{}$.
A state $\state{\hloc{}}{r}$ is said to be \emph{admissible} if
$\InvVal{\hloc{}}{r}$ holds.

The \emph{continuous transition relation} $\ctrans{t}$ between admissible states, 
where $t\geq 0$ denotes the transition elapsed time, is defined as follows:
%\noindent $\state{\hloc{}}{r} \ctrans{t} \state{\hloc{}}{s}  \:\:\mbox{ iff }\:\: $
%it holds that $s=\vfFunct{\hloc{}}(r,t)$, %(see~\ref{def:hyau}),
%and for each $t'\in[0,t]$ the formula  $\Inv{\hloc{}}{\vfFunct{\hloc{}}(r,t')}$ is true.

\vskip0.0cm
%\mbox{}\\
\noindent
\begin{tabular}{lcl}
$\state{\hloc{}}{r} \ctrans{t} \state{\hloc{}}{s}$& $\iff$  &
%\begin{minipage}{10cm}
$r=\vfFunct{\hloc{}}(r)(0)$, 
$s=\vfFunct{\hloc{}}(r)(t)$, and 
$\InvVal{\hloc{}}{\vfFunct{\hloc{}}(r)(t')}$ hold for each  $t'\in[0,t]$. 
%\end{minipage}
\end{tabular}

The \emph{discrete transition relation} $\dtrans{e}$ among
admissible states is:

%\noindent $\state{\hloc{}}{r} \dtrans{e} \state{u}{s} \:\:\mbox{ iff }\:\:$
%it holds $e \in \Edg$, with $v$ and $u$ source and destination of $e$, respectively, and both $\Act{e}{r}$ and $\HReset{e}{r,s}$ are true.
\vskip0.15cm
\noindent
\begin{tabular}{lcl}
$\state{\hloc{}}{r} \dtrans{e} \state{\hloc{}}{s}$& $\iff$  &
%\begin{minipage}{4.3cm}
%$e \in \Edg$, with $v$ and $u$ source and destination of $e$, respectively, 
$e=\tuple{\hloc{},\hloc{}'}$ 
and both 
%both formul\ae\ 
$\ActVal{e}{r}$ and $\HResetVal{e}{r,s}$ hold.
%\end{minipage}
\end{tabular}
\end{definition}
We write $\hstate{}\actrans \hstate{}'$ and $\hstate{}\adtrans \hstate{}'$ to mean 
that there exists a $t \in \bbbr_{\geq0}$ such that
$\hstate{}\ctrans{t} \hstate{}'$ and that there exists an $e \in \Edg$ such that
$\hstate{}\dtrans{e} \hstate{}'$, respectively.
%Moreover, we write $\hstate{}\trans{}\hstate{}'$ to denote that either
%$\hstate{}\actrans \hstate{}'$ or $\hstate{}\adtrans \hstate{}'$.

%Building upon a combination of both
%continuous and discrete transitions, 
%we can
%formulate the notion of %of \emph{trace} as well as a resulting notion of
%\emph{reachability}.

%
%\begin{definition}[Hybrid Automata - Reachability]\label{semantics2}
%The hybrid automaton $H$ \emph{reaches} a state $\hstate{}$ from a state 
%$\hstate{}'$ if
%there exists a sequence of admissible states $\hstate{}_0,\dots,\hstate{}_n$, with 
%$\hstate{}=\hstate{}_0$ and $\hstate{}'=\hstate{}_n$, such that
%$\hstate{}_{i-1}\rightarrow \hstate{}_{i}$ holds for each 
%$i\in [1,n]$. 
%In such a case, we also say that $\hstate{}'$ is \emph{reachable} 
%from $\hstate{}$ in $H$.
%\end{definition}

%\begin{definition}[Hybrid Automata - Reachability]\label{semantics2}
\begin{definition}[Reachability]\label{semantics2}
%The hybrid automaton $H$ \emph{reaches} a state $\hstate{}_n$ from a state 
%$\hstate{}_0$ if
%there exists a sequence of admissible states $\hstate{}_0,\dots,\hstate{}_n$
%such that  
%$\hstate{}_{i-1}\rightarrow \hstate{}_{i}$ holds for all $i \in [1,n]$ and 
%either $\hstate{}_{i-2}\actrans \hstate{}_{i-1}\adtrans\hstate{}_{i}$,
%$\hstate{}_{i-2}\adtrans \hstate{}_{i-1}\adtrans\hstate{}_{i}$,
%or $\hstate{}_{i-2}\adtrans \hstate{}_{i-1}\actrans\hstate{}_{i}$ for all $i \in [2,n]$\footnote{This last condition 
%supports not transitive dynamics. See~\cite{focore2008} for a complete discussion.}. 
%In such a case, we also say that $\hstate{}_n$ is \emph{reachable} 
%from $\hstate{}_0$ in $H$.
Let $\mathcal{I}$ be either $\bbbn$ or an initial finite interval of $\bbbn$.
A \emph{trace} of $H$ is a sequence of admissible states $\hstate{0},\hstate{1},\dots,
\hstate{j},\dots$, with $j\in \mathcal{I}$, such that
$\hstate{i-1}\rightarrow \hstate{i}$ holds for all $i \in [1,n]$ and 
either $\hstate{i-2}\actrans \hstate{i-1}\adtrans\hstate{i}$,
$\hstate{i-2}\adtrans \hstate{i-1}\adtrans\hstate{i}$,
or $\hstate{i-2}\adtrans \hstate{i-1}\actrans\hstate{i}$ for each $i\in I\setminus \{0\}$\footnote{This last condition 
supports not transitive dynamics. See~\cite{focore2008} for a complete discussion.}.

The automaton $H$ \emph{reaches} a state $\hstate{n}$ from a state 
$\hstate{0}$ if
there exists a trace $\hstate{0},\dots,\hstate{n}$.
In such a case, we also say that $\hstate{n}$ is \emph{reachable} from $\hstate{0}$ in $H$.
\end{definition}

The problem of deciding whether a hybrid automaton $H$ 
reaches a set of states $S$ from a set of states $R$ is known
as the \emph{reachability problem} of $S$ from $R$ over $H$. 
A trace produced by an infinite sequence of discrete transitions during
a bounded amount of time is called \emph{Zeno trace} and
every hybrid automaton allowing such kind of trace is said to have a
\emph{Zeno behaviour}.

\begin{example}\label{example:ball}
Let us consider a hybrid automaton $H_b$ modeling a
\emph{bouncing ball} whose collisions are inelastic.
%
\begin{figure}[!h]
\begin{center}
\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=2.8cm,
                    semithick,scale=0.75, transform shape]
  \tikzstyle{every state}=[fill=blue!20!white,draw,text=black]

  \node[state]   (S0)  {\begin{tabular}{c}
                                   $\dot{X}_1=\X{2}$ \\ 
                                   $\dot{X}_2=-g$
                                   \end{tabular}};

  \path (S0) edge [loop right] node {
                                   \begin{tabular}{l}
                                   $\X{1}'=\X{1}$ \\ 
                                   $\X{2}'=-\gamma \X{2}$
                                   \end{tabular}} (S0);
\end{tikzpicture}
\caption{Bouncing ball hybrid automaton.}\label{fig:bouncing}
\end{center}
\end{figure}
%
The automaton is equipped with two continuous variables $\X{1}$ and $\X{2}$ 
that represent ball's elevation and 
velocity, respectively.
The dynamics, resets, and discrete structure of
$H_b$ are presented in Fig.~\ref{fig:bouncing}.
The two coefficients $g$ and $\gamma$ are the standard gravity
and the coefficient of restitution, respectively. The activation
formula of the automaton edge is ``$\X{1} = 0$''.

%It is easy to see that, if we compute reachability by using standard semantics,
%we get a Zeno behaviour. In particular,
Imposing as starting height $h_0=10m$ and as  coefficient of restitution $\gamma=0.86$, 
the 
%ball's elevation evolves along time as depicted in 
%Fig.~\ref{fig:bouncing_trace}.
%The 
bounce peaks decrease 
at each iteration and 
the automaton $H_b$ has a Zeno behaviour. 
%
%\begin{figure}[!h]
%\begin{center}
%\includegraphics[width=0.43\textwidth]{figures/figures.3}
%\caption{Zeno behaviour of a bouncing ball.}\label{fig:bouncing_trace}
%\end{center}
%\end{figure}
\end{example}


As the halting problem for the two counter machine can be reduced to 
the reachability problem of a particular class of hybrid automata, 
the reachability problem for hybrid automata itself is not always decidable \cite{alur95}. 
However, if $H$ is a $\Theory$-hybrid automaton and $\Theory$ is a first-order 
decidable theory, then the reachability through a bounded number of discrete transitions 
can be characterized with a first-order decidable formula (see e.g.,~\cite{focore2008}). In particular, 
in the case of automata defined through polynomials over the reals, we can use 
cylindrical algebraic decomposition tools to decide bounded reachability. 


introduction.tex
% !TEX root = main.tex
\section*{Introduction}\label{sec:intro}

%\begin{itemize}
%	\item Presentazione Neural oscillator 
%	\item Modello continuo 
%	\item	Verifica automatica di propriet�
%	\item	Sgn non funziona
%	\item	Modello neural con HA
%	\item Cosa succede con tecniche di approssimazione?
%	\item	 Citare le varie tecniche ( vedi anche review ATVA )
%	\item Ci concentriamo su una a caso di queste
%	\item	Dimostriamo come pu� essere effettivamente calcolata
%\end{itemize}

Neural oscillations are rhythmic and repetitive electrical stimuli which play an important role in 
the activities of several brain regions. Some examples of brain locations in which it has been demonstrated 
the central role of neural oscillations are %the hippocampus~\cite{Traub:1991:NNH:574330},
the cortex~\cite{1824881}, the thalamus~\cite{citeulike:4043128}, and the olfactory information processing~\cite{citeulike:762104}. 
With the aim of understanding neurophysiological activities, we propose the modeling 
of oscillatory phenomena exploiting hybrid automata. 

A continuous model of a single oscillator based on an ordinary differential system has been proposed
in~\cite{Tonnelier19991213}. Even if this is a simple model, its analysis and the analysis of its composition in multiple
copies is limited due to the non-linearity of the ordinary differential system involved. For this reason, 
we are interested in the development of a piecewise affine hybrid automaton which correctly approximates 
the continuous model and on which automatic analysis and composition can be made.

Trying to linearize the non-linear components of the original continuous model, we first replace in the 
standard way the sigmoidal behaviours with sign functions~\cite{tomlinmodel,springerlink:10.1016/j.bulm.2003.08.010}, approximating 
continuos signals with discrete off-on signals. Unfortunately, the behaviour of this model differs from the original one. For 
this reason, we propose a more sophisticated approximation of sigmoidals based on a piecewise 
linear function exploited in the development of a hybrid automaton which simulates a single oscillator.

It is well known that the reachability problem over hybrid automata
is source of undecidability.
Moreover, the exact computation of the reachable sets of hybrid automata, which represents the basis of 
the automatic analysis of the models, does not always reflect the behaviour of the real modeled systems. This is 
due to the fact that real systems are often subject to noise, thus their evolutions do not correspond to 
a single precise formalization. This has been noticed already in~\cite{Tonnelier19991213} in the specific case of the continuous model of 
the neural oscillator. For these reasons, we study our hybrid automaton exploiting different 
approximation techniques that introduce noise. 

In the literature, several approximation techniques have been proposed (see, e.g.,~\cite{franzle99,DBLP:conf/tamc/Ratschan10,Girard:2007fk,%tiwari,
DBLP:journals/deds/CasagrandePP09,Prabhakar:2009:VTS:1683310.1684907}). 
Fr\"anzle in~\cite{franzle99}
presents a model of noise over hybrid automata. The introduction of noise ensures
in many cases the (semi-)decidability of the reachability problem. Another result of 
(semi-)decidability always based on the concept of perturbation and concerning the safety
verification of hybrid systems is given by Ratschan in~\cite{DBLP:conf/tamc/Ratschan10}. Furthermore,
$\epsilon$-(bi)simulation~\cite{Girard:2007fk}
relations, which are essentially relaxations on the infinite precision required by simulation and bisimulation, 
represent tools able to remove complexity and undecidability issues related to the analysis of the
investigated model. Moreover, in~\cite{DBLP:journals/deds/CasagrandePP09} it is presented a different approach based
on the reinterpretation of the standard semantics of the formul\ae~which compose hybrid automata.
Exploiting this new class of semantics, called $\epsilon$-semantics, the authors provide a 
result of decidability of the reachability problem over hybrid automata with bounded invariants.

In this paper, we focus precisely on the approximation approach based on the $\epsilon$-semantics.
In particular, we propose a translation that allows us to reduce the  
$\epsilon$-semantics evaluation to the standard semantics evaluation, computable by exploiting 
tools for cylindrical algebraic decomposition. Then, we present some properties which have been automatically 
tested on the neural oscillator by applying such translation. Hence, in this work, we prove both that 
$\epsilon$-semantics better represents the real behaviour of the neural oscillator, than the standard one, 
and that the approach is effective. 

The paper is organized as follows: Section~\ref{sec:ha} gives some basic definitions concerning logics and
hybrid automata; Section~\ref{sec:model} is dedicated to the mathematical modeling of the neural oscillator;
in Section~\ref{sec:approx} we present different approximation techniques based on noise, perturbation,
approximate (bi)simulations, and $\epsilon$-semantics. Section~\ref{sec:analysis} exposes some considerations regarding 
the application of the previously presented  approximation approaches to the investigated model.
Finally, in Section~\ref{sec:computing}, we first define a translation which make effectively computable the
$\epsilon$-semantics, then we experimentally exploit it in the analysis of the hybrid automaton
which models the neural oscillator. All the proofs can be found at \url{http://www.dimi.uniud.it/piazza/hsb2012_extended.pdf}.



















logics.tex
% !TEX root = main.tex
\section{Hybrid Automata}\label{sec:ha}
\subsection{Preliminaries}\label{sec:logics}

We formally define hybrid automata by using first-order languages and, 
because of that, we first need to introduce some basic notions and our notation.

We use $\X{}$, $\X{i}$, $\Y{}$,  $\Y{i}$,  $\W{}$,  and $\W{i}$ to denote real variables and 
 $\vX{}$, $\vX{i}$, $\vY{}$,  $\vY{i}$,  $\vW{}$,  and $\vW{i}$ to denote tuple 
 of real variables. 
We always assume that all the variables that occur bound in a formula do
not occur free and vice versa. This enables us to label variables, rather than occurrences,  
as free or bound.
We write 
$\NotBoundIn{\formul}{\X{1}, \dots, \X{m}}$ to 
stress the fact that %all the variables 
$\X{1}$, $\ldots$, $\X{m}$ are free in $\formul$.
By extension, %the notation 
$\NotBoundIn{\formul}{\vX{1}, \ldots, \vX{n}}$ 
indicates that  
 the components of vectors 
$\vX{1}$, $\ldots$, $\vX{n}$ are free in $\formul$.

%A \emph{model} of a language is an interpretation for it that 
%maps all the constants into a set named \emph{support}.
%
%Let %$\ModelT$ be a model, with support $\ValVar$, of a language $\Lang$,
%$\NotBoundIn{\formul}{\X{1}, \ldots,\X{m}}$ be a formula of $
%\Lang$, and $s_0, \ldots, s_n$ be either constants or variables of $\Lang$.
The formula obtained from $\NotBoundIn{\formul}{\X{1}, \ldots,\X{m}}$ by replacing $\X{i}$ by $s_0$, 
where $s_0$ is either a constant or a variable,  is
denoted by $\VarSub{\formul}{\X{i}}{s_0}$.
By extension, $\VarSub{\formul}{\X{i}\ldots\X{i+n}}{s_{0}\ldots s_{n}}$ 
indicates the formula obtained from $\NotBoundIn{\formul}{\X{1}, \ldots,\X{m}}$
by simultaneously replacing all the variables $\X{i}\ldots\X{i+n}$ by $s_{0}\ldots s_{n}$. 
If $\vX{}=\tuple{\X{i},\ldots,\X{i+n}}$, $\vec{s_0}=\tuple{s_{0},\ldots,s_{n}}$, 
$\vec{s_1}=\tuple{s_{n+1},\ldots,s_{2\mult{}n+1}}$, and 
$\relation$ is a relational symbol (e.g., $=$ or $\geq$), then we may write 
$\VarSub{\formul}{\vX{}}{\vec{s_0}}$ in place of 
$\VarSub{\formul}{\X{i}\ldots\X{i+n}}{s_{0}\ldots s_{n}}$ and 
$\vec{s_0}\relation\vec{s_1}$ in place of 
$\bigwedge_{j \in [0,n]} \left( {s_{j}\relation s_{j+k\mult{}n}} \right)$ (e.g., 
$\tuple{7,\X{}} = \tuple{2,3}$ means $7=2 \land \X{}=3$). 
Finally, if $\NotBoundIn{\formul}{\vX{1}, \ldots, \vX{i}, \ldots, \vX{n}}$ then we may denote the 
formula $\VarSub{\formul}{\vX{i}}{\vec{s}}$ by writing  
$\VarSSub{\formul}{\vX{1}, \ldots, \vec{s}, \ldots, \vX{n}}$.

The semantics of a formula 
%with respect to a model $\ModelT$ 
is defined in the standard way (see. e.g.,~\cite{ender}).
%We say that a formula $\NotBoundIn{\formul_1}{\X{1},\dots,\X{m}}$ in $\Lang$ is
%\emph{satisfiable} in $\ModelT$ if there exist $p_1, \ldots, p_m$ such that 
%$\VarSSub{\formul_1}{p_1,\dots,p_m}$ holds in $\ModelT$.
%Moreover, we say that $\NotBoundIn{\formul_1}{\X{1},\dots,\X{m}}$ is \emph{valid} if
%$\VarSSub{\formul_1}{p_1,\dots,p_m}$ holds in $\ModelT$ for all $p_1, \ldots,
%p_m$. When the model $\ModelT$ is clear from the context
%we will simply say that a formula holds (is satisfiable or is valid,
%respectively).
%
Given a set $\Gamma$ of sentences and a sentence $\formul$, we say
that $\formul$ is a \emph{logical consequence} of $\Gamma$ (denoted,
$\Gamma\models\formul$) if 
%for each model $\ModelT$ it holds that if each
%formula of $\Gamma$  is valid in $\ModelT$ 
%then $\formul$ is valid in $\ModelT$. 
$\formul$ is valid in any model $\ModelT$  in which each formula of $\Gamma$ is valid  too
($\ModelT \models \Gamma$).
A \emph{theory} $\Theory$ is a set of sentences such that if
$\Theory\models \formul$, then $\formul\in\Theory$.
% If $\Lang$ language and 
%$\ModelT$ a model of it, then the \emph{complete theory}
%$\Theory(\ModelT)$ of $\ModelT$ is the set of all the sentences of
%$\Lang$ which are valid in $\ModelT$.
A theory $\Theory$
admits the so-called \emph{elimination of quantifiers}, if, for any
formula $\formul$, there exists in $\Theory$ a quantifier free formula $\varrho$  
such that $\formul$ is equivalent to $\varrho$ with respect to
$\Theory$. If there exists an algorithm for deciding whether a
sentence $\formul$ belongs to $\Theory$ or not, we say that
$\Theory$ is \emph{decidable}. 
%Notice that given a model $\ModelT$,
%its complete theory $\Theory(\ModelT)$ is decidable if and only if
%both the satisfiability and the validity of formul\ae\ in $\ModelT$
%are decidable.

\begin{example}
Consider the formula 
$\formul \defeq \exists \X{}\, (a \mult \X{}^2 + b\mult \X{} + c = 0)$. 
It is well known that $\formul$ is in the theory of reals with $+$, $\mult{}$, 
and $\geq$ if and only if the unquantified formula $b^2 - 4 ac \geq 0$ holds.
\end{example}

%
%Given a language $\Lang$ and
%a model $\ModelT$ of it, we say that a set
%$S$ is 
%\emph{definable} in or by $\ModelT$ if there exists a formula
%$\NotBoundIn{\formul}{\X{1},\dots,\X{k}}$ such that $\ModelT \models \VarSSub{\formul}{p_1,\dots,p_k}$  
%if and only if $\tuple{p_1,\dots,p_k}\in S$.

macro.tex
% !TEX root = main.tex
\newtheorem{definition}{Definition}
\newtheorem{example}{Example}
\newtheorem{theorem}{Theorem}
\newtheorem{corollary}{Corollary}

\def\bbbr{\mathbb{R}} %reelle Zahlen
\def\bbbn{\mathbb{N}} %natuerliche Zahlen
\def\bbbq{\mathbb{Q}} 
\def\bbbz{\mathbb{Z}} 

\newcommand{\added}[1]{\textbf{\textit{#1}}}
\newcommand{\todo}[1]{\textbf{TO DO:}\ {#1}\ \textbf{END TO DO}}

%\newcommand{\Sat}[1]{\mathscr{S}_{#1}}
\newcommand{\ltrue}{\textrm{True}}

\newcommand{\Lang}{\mathcal{L}}
\newcommand{\Theory}{\mathcal{T}}
\newcommand{\ModelT}{\mathcal{M}}

\newcommand*{\llangle}{\left\langle\kern-2\nulldelimiterspace\left
\langle}
\newcommand*{\rrangle}{\right\rangle\kern-2\nulldelimiterspace\right
\rangle}

\newcommand{\Model}{\mathcal{M}}

\newcommand{\Kripke}{\mathcal{K}}

\newcommand{\Sat}[1]{\mathit{Sat}({#1})}

\newcommand{\VarSub}[3]{{#1}\llbracket{#2}/{#3}\rrbracket}
\newcommand{\VarSSub}[2]{{#1}\llbracket{#2}\rrbracket}
\newcommand{\NotBoundIn}[2]{{#1}[{#2}]}

\newcommand{\VSetName}{\mathbb{V}}
\newcommand{\VSet}[1]{\VSetName_{#1}}

\newcommand{\Var}{\mathit{V}}
\newcommand{\Const}{\mathit{C}}
\newcommand{\Fun}{\mathit{F}}
\newcommand{\Rel}{\mathit{R}}
\newcommand{\Oper}{\mathit{O}}
%\newcommand{\PropOp}{\mathrm{PropOp}}
\newcommand{\Sort}{\mathit{S}}
\newcommand{\pureSort}{\mathit{pS}}


\newcommand{\termin}{\mathit{term}}
\newcommand{\formul}{\varphi}
\newcommand{\aformul}{\formul_\mathrm{a}}

\newcommand{\True}{\top}
\newcommand{\False}{\bot}

\newcommand{\liff}{\leftrightarrowtriangle}
\newcommand{\limply}{\rightarrowtriangle}

\newcommand{\imply}{\Longrightarrow}

\newcommand{\CAD}{\mbox{CAD}}

\newcommand{\quantif}{\mathcal{Q}}

\newcommand{\SAModel}{\tuple{\bbbr, 0, 1, +, *, <}}

\newcommand{\VarNotation}[3]{{#1}%
\ifthenelse{\equal{#3}{}}{%
\ifthenelse{\equal{#2}{}}%
{}%
{_{#2}}}%
{_{({#3}){#2}}}}

\newcommand{\Vname}{V}
\newcommand{\V}[2][]{\VarNotation{\Vname}{#2}{#1}}
%\newcommand{\vV}[1]{\vec{\Vname_{#1}}}
\newcommand{\vV}[1]{\mathbf{\V{#1}}}

\newcommand{\Nname}{N}
\newcommand{\N}[2][]{\VarNotation{\Nname}{#2}{#1}}
%\newcommand{\vN}[1]{\vec{\Nname_{#1}}}
\newcommand{\vN}[1]{\mathbf{\N{#1}}}
  
\newcommand{\Xname}{X} 
\newcommand{\X}[2][]{\VarNotation{\Xname}{#2}{#1}}   
\newcommand{\vX}[1]{\mathbf{\X{#1}}}

\newcommand{\Yname}{Y} 
\newcommand{\Y}[2][]{\VarNotation{\Yname}{#2}{#1}}   
%\newcommand{\vY}[1]{\vec{\Yname_{#1}}}
\newcommand{\vY}[1]{\mathbf{\Y{#1}}}

\newcommand{\Wname}{W} 
\newcommand{\W}[2][]{\VarNotation{\Wname}{#2}{#1}}   
%\newcommand{\vW}[1]{\vec{\Wname_{#1}}}
\newcommand{\vW}[1]{\mathbf{\W{#1}}}

\newcommand{\itvlName}{I} 
\newcommand{\itvl}[2][]{\VarNotation{\itvlName}{#1}{#2}}

\newcommand{\Ts}[1]{\mathscr{T}_{#1}}
\newcommand{\F}[2]{F^{#1}_{#2}}
\newcommand{\Fdom}[2]{I^{#1}_{#2}}

\newcommand{\LocM}{\mathcal{Q}}

\newcommand{\Loc}{\mathscr{V}}
\newcommand{\Edg}{\mathscr{E}}
\newcommand{\SubLoc}{\mathscr{W}}
\newcommand{\Label}{\mathscr{L}}

\newcommand{\eSrcDef}{\texttt{Source}}
\newcommand{\eDstDef}{\texttt{Dest}}
\newcommand{\eLblDef}{\texttt{Label}}
\newcommand{\eCmpDef}{\texttt{Comp}}

%\newcommand{\eSrc}[1]{\eSrcDef\left({#1}\right)}
%\newcommand{\eDst}[1]{\eDstDef\left({#1}\right)}
\newcommand{\eSrc}[1]{{#1}\rightarrow}
\newcommand{\eDst}[1]{\rightarrow{#1}}
\newcommand{\eLbl}[1]{\eLblDef\left({#1}\right)}
\newcommand{\eCmp}[2]{\eCmpDef\left({#1},{#2}\right)}

\newcommand{\ActSymb}{\mathit{Act}}
\newcommand{\ResetSymb}{\mathit{Res}}
\newcommand{\DynSymb}{\mathit{Dyn}}
\newcommand{\InvSymb}{\mathit{Inv}}

\newcommand{\FV}[1]{\mathit{Free}({#1})}

\newcommand{\Tvar}[1]{T_{#1}}

%\newcommand{\iReachSet}[3]{{\mathit{RSet}_{#1}^{#2}\left({#3}\right)}}
\newcommand{\ReachSet}[3][]{{\mathit{RSet}_{#2}^{#1}\!\left({#3}\right)}}
\newcommand{\ReachTimeSet}[2]{\mathit{Rh}_{#1}({#2})}
\newcommand{\ReachDef}{\overline{\mathit{Reach}}}
\newcommand{\Reach}[3]{\ReachDef({#3})({#1})[{#2}]}
\newcommand{\oReachDef}{\mathit{Reach}}
\newcommand{\oReach}[3]{\oReachDef({#3})({#1})[{#2}]}
\newcommand{\ooReach}[2]{\oReachDef({#1})[{#2}]}
\newcommand{\eReach}[3]{\widetilde{\oReachDef}({#3})({#1})[{#2}]}
\newcommand{\niReach}[4]{\oReachDef^{#2}_{#1}({#3},{#4})}
\newcommand{\iReach}[6]{\niReach{#1}{#2}{#3}{#4}[#5,#6]}

\newcommand{\ActFormulaeSet}{\mathit{ActSet}}
\newcommand{\ActSet}[2][]{\mathscr{A}_{#1}({#2})}
\newcommand{\Act}[2][]{\ActSymb_{#1}{(#2)}}
\newcommand{\ActDef}[2][]{\NotBoundIn{\Act[#1]{#2}}{\vX{}}}
\newcommand{\ActVal}[3][]{\VarSSub{\Act[#1]{#2}}{#3}}

\newcommand{\ResetFormulaeSet}{\mathit{ResetSet}}
\newcommand{\ResetSet}[3][]{\mathscr{R}_{#1}({#2})({#3})}
\newcommand{\HReset}[2][]{\ResetSymb_{#1}({#2})}
\newcommand{\HResetDef}[2][]{\NotBoundIn{\HReset[#1]{#2}}{\vX{},\vX{}'}}
\newcommand{\HResetVal}[3][]{\VarSSub{\HReset[#1]{#2}}{#3}}

\newcommand{\RSetF}[1]{\overline{\ResetSymb}({#1})}

\newcommand{\InvFormulaeSet}{\mathit{InvSet}}
\newcommand{\InvSet}[2][]{\mathscr{I}_{#1}({#2})}
\newcommand{\Inv}[2][]{\InvSymb_{#1}({#2})}
\newcommand{\InvDef}[2][]{\NotBoundIn{\Inv[#1]{#2}}{\vX{}}}
\newcommand{\InvVal}[3][]{\VarSSub{\Inv[#1]{#2}}{#3}}

\newcommand{\DynFormulaeSet}{\mathit{DynSet}}
\newcommand{\Dyn}[2][]{\DynSymb_{#1}({#2})}
\newcommand{\DynDef}[2][]{\NotBoundIn{\Dyn[#1]{#2}}{\vX{},\vX{}',T}}
\newcommand{\DynVal}[3][]{\VarSSub{\Dyn[#1]{#2}}{#3}}

\newcommand{\VectorFDef}{\mathcal{F}}
\newcommand{\VectorF}[2][]{\VectorFDef_{#1}({#2})}

\newcommand{\VectorFIDef}{\mathcal{P}}
\newcommand{\VectorFI}[1]{\VectorFIDef({#1})}

\newcommand{\vfFunct}[1]{{f}_{#1}}

\newcommand{\vfiFunct}[1]{{p}_{#1}}

\newcommand{\obmap}[1]{\llangle{#1}\rrangle}

\newcommand{\trans}[2][]{\xrightarrow{#2}_{#1}}
\newcommand{\ctrans}[1]{\trans[C]{#1}}
\newcommand{\dtrans}[1]{\trans[D]{#1}}
\newcommand{\actrans}{\rightarrow_{C}}
\newcommand{\adtrans}{\rightarrow_{D}}

\newcommand{\up}[1]{\textrm{up}\left[{#1}\right]}
\newcommand{\upr}[1]{\textrm{up}'\left[{#1}\right]}

\newcommand{\equationC}[1]{\textrm{C}\left({#1}\right)}
\newcommand{\equationCr}[1]{\textrm{C}'\left({#1}\right)}

\newcommand{\Pre}[2]{\mathit{Pre}_{#1}\left({#2}\right)}
\newcommand{\barP}[2]{\widetilde{P}_{#1}\left({#2}\right)}

\newcommand{\succS}[2]{S_{{#1},{#2}}}
\newcommand{\dS}[2]{d_{{#1},{#2}}}

\newcommand{\Hinfbis}{H_\textrm{inf}}

\newcommand{\Tp}[2]{\textrm{Tp}({v})\left[{#2}\right]}

\newcommand{\frulfdef}{\rho}
\newcommand{\funrfdef}{\sigma}

\newcommand{\notreachdef}{\mathit{NotFlow}}
\newcommand{\notreachdefin}{\mathit{NotEFlow}}
\newcommand{\notreach}[3]{\notreachdef({#3},{#1},{#2})}
\newcommand{\notreache}[2]{\notreachdefin({#1},{#2})}

\newcommand{\globnotreachdef}{\mathit{NotRFlow}}
\newcommand{\globnotreach}[3]{\globnotreachdef({#1},{#2},{#3})}

\newcommand{\pruldef}[1]{\frulfdef_{#1}}
\newcommand{\punrdef}[1]{\funrfdef_{#1}}

%\newcommand{\prul}[3]{\pruldef{#3}}
%\newcommand{\punr}[3]{\punrdef{#3}}

\newcommand{\prul}[3]{\pruldef{#1}({#3})}
\newcommand{\punr}[3]{\punrdef{#1}({#3})}

\newcommand{\vrulf}[1]{\mathring{\frulfdef}({#1})}
\newcommand{\vunrf}[1]{\mathring{\funrfdef}({#1})}

\newcommand{\erulf}[1]{\overrightarrow{\frulfdef}({#1})}
\newcommand{\eunrf}[1]{\overrightarrow{\funrfdef}({#1})}

\newcommand{\partit}[2]{\mathcal P({#1})}

\newcommand{\defeq}{\stackrel{\text{\tiny def}}{=}}

%\newcommand{\tuple}[1]{\left\langle{#1}\right\rangle}
\newcommand{\tuple}[1]{\langle{#1}\rangle}
\newcommand{\pair}[1]{\left({#1}\right)}
\newcommand{\edge}[3]{\left\langle{#1},{#2},{#3}\right\rangle}
\newcommand{\tpath}[1]{`{#1}'}
\newcommand{\state}[2]{\left\langle{{#1},{#2}}\right\rangle}
\newcommand{\varset}{\Gamma}
\newcommand{\vars}[1]{\Gamma({#1})}
\newcommand{\varv}[1]{Z_{#1}}
\newcommand{\indvar}{\mathcal{I}}
\newcommand{\dipvar}{\mathcal{C}}

\newcommand{\ZS}[1]{Z^{#1}}
\newcommand{\ZI}{\mbox{X}}
\newcommand{\ZC}{\mbox{Y}}

\newcommand{\ZIP}{\ZI'}
\newcommand{\ZCP}{\ZC'}

\newcommand{\fiv}{\mbox{fi}}
\newcommand{\fcv}[1]{\mbox{fc}({#1})}

%\newcommand{\screset}[2]{\widehat{\ResetSymb}({#1})[{#2}]}
\newcommand{\screset}[2]{c\ResetSymb({#1})[{#2}]}
%\newcommand{\scact}[2]{\widehat{\ActSymb}({#1})[{#2}]}
\newcommand{\scact}[2]{c\ActSymb({#1})[{#2}]}
%\newcommand{\siinv}[1]{\widetilde{\InvSymb}[{#1}]}
\newcommand{\siinv}[1]{i\InvSymb[{#1}]}
%\newcommand{\scinv}[2]{\widehat{\InvSymb}({#1})[{#2}]}
\newcommand{\scinv}[2]{c\InvSymb({#1})[{#2}]}
%\newcommand{\sidyn}[1]{\widetilde{\DynSymb}[{#1}]}
\newcommand{\sidyn}[1]{i\DynSymb[{#1}]}
%\newcommand{\scdyn}[2]{\widehat{\DynSymb}({#1})[{#2}]}
\newcommand{\scdyn}[2]{c\DynSymb({#1})[{#2}]}


\newcommand{\SiCyPHA}{\mbox{SiCyPHA}}
\newcommand{\IDA}{\mbox{IDA}}
\newcommand{\NEIDA}{\mbox{NEIDA}}
\newcommand{\tpc}{\mathcal{T}}

\newcommand{\rflowfdef}{\mathit{RFlow}}
\newcommand{\rflowf}[3]{\rflowfdef({#1},{#2},{#3})}

\newcommand{\uflowfdef}{\mathit{Flow}}
\newcommand{\tuflowfdef}{\mathit{EFlow}}

\newcommand{\uflowf}[3]{\uflowfdef({#3},{#1},{#2})}
\newcommand{\uflowfe}[2]{\tuflowfdef({#1},{#2})}

%\newcommand{\rdynf}[1]{{\varrho}({#1})}
\newcommand{\rinvf}[1]{{\mathit{SInv}}({#1})}
%\newcommand{\uresf}[1]{{\varsigma}({#1})}

\newcommand{\lmindef}{{\mathit{InfFlow}}}
\newcommand{\lmindefin}{{\mathit{InfEFlow}}}
\newcommand{\mininfdef}{{\mathit{MinInfFlow}}}

\newcommand{\lminf}[3]{{\lmindef}({#1},{#2},{#3})}
\newcommand{\lminfe}[2]{{\lmindefin}({#1},{#2})}
\newcommand{\mininf}[1]{{\mininfdef}({#1})}

\newcommand{\tminf}[1]{{\lambda}^{\textrm{Tot}}_{#1}}


\newcommand{\msub}[1]{{\mathit{Sb}}({#1})}

\newcommand{\maxf}[3]{{\mathit{SupRFlow}}({#1},{#2},{#3})}

\newcommand{\arcnumf}[4]{{\theta}({#1},{#2},{#3},{#4}) }

\newcommand{\commvert}{\mathcal{C}}

\newcommand{\dims}[1]{d({#1})}

\newcommand{\SPart}{\tilde{\mathcal{P}}}
\newcommand{\IR}{\mbox{IR}}
\newcommand{\CR}{\mbox{CR}}

\newcommand{\SCC}{\mbox{s.c.c.}}

\newcommand{\PSet}[1]{\mathcal{P}_{#1}}
\newcommand{\simul}[1]{\preccurlyeq_{#1}}
\newcommand{\bisim}[1]{\approx_{#1}}
%\newcommand{\sclass}[2]{\left[{#2}\right]_{\simeq_{#1}}}
%\newcommand{\bclass}[2]{\left[{#2}\right]_{\bisim_{#1}}}

\newcommand{\sclass}[2]{[{#2}]_{\simeq_{#1}}}
\newcommand{\bclass}[2]{[{#2}]_{\bisim_{#1}}}

\newcommand{\synchr}[1]{\mu\left({#1}\right)}
\newcommand{\ftime}[2]{\rho\left({#1}\right)\left[{#2}\right]}

\newcommand{\arityDef}{\textrm{Ar}}
\newcommand{\arity}[1]{\arityDef({#1})}

\newcommand{\code}[1]{\ensuremath{\mbox{\sc {#1}}}}

\newcommand{\dsem}[2][]{\left\{\kern-2\nulldelimiterspace\left|{#2}\right|\kern-2\nulldelimiterspace\right\}_{#1}}

\newcommand{\sphseml}{\left(\kern-2\nulldelimiterspace\left|}
\newcommand{\sphsemr}{\right|\kern-2\nulldelimiterspace\right)}
\newcommand{\sphsem}[2][\epsilon]{\sphseml{#2}\sphsemr_{#1}}

\newcommand{\seml}{\left\{\kern-2\nulldelimiterspace\left|}
\newcommand{\semr}{\right|\kern-2\nulldelimiterspace\right\}}
\newcommand{\epssem}[2][\epsilon]{\seml{#2}\semr_{#1}}
\newcommand{\stdsem}[1]{\seml{#1}\semr}

\newcommand{\ball}[2]{B\left({#1},{#2}\right)}
\newcommand{\eball}[1]{\ball{#1}{\epsilon}}

\newcommand{\ReallyNewVar}{\textit{C}}
\newcommand{\ReachedVar}{\textit{R}}
\newcommand{\NewVar}{\textit{N}}
\newcommand{\MayVar}{\textit{M}}

\newcommand{\ReallyNew}[2]{\ReallyNewVar({#1})\left[{#2}\right]}
\newcommand{\Reached}[2]{\ReachedVar({#1})\left[{#2}\right]}
\newcommand{\New}[2]{\NewVar({#1})\left[{#2}\right]}
\newcommand{\May}[2]{\MayVar({#1})\left[{#2}\right]}

\newcommand{\iReallyNew}[1]{\mathcal{\ReallyNewVar}_{#1}}
\newcommand{\iReached}[2]{\mathcal{\ReachedVar}_{#1}({#2})}
\newcommand{\iNew}[2]{\mathcal{\NewVar}_{#1}({#2})}
\newcommand{\iMay}[2]{\mathcal{\MayVar}_{#1}({#2})}

\newcommand{\MaySet}[1]{\mathcal{\MayVar}({#1})}

\newcommand{\LTL}{\mbox{LTL}}
\newcommand{\CTL}{\mbox{CTL}}
\newcommand{\CTLS}{\mbox{CTL*}}
\newcommand{\ACTLS}{\mbox{ACTL*}}
\newcommand{\TCTL}{\mbox{TCTL}}
\newcommand{\CTLSX}{\CTLS$_{-\Next}$}
\newcommand{\CTLX}{\CTL$_{-\Next}$}
\newcommand{\LTLX}{\LTL$_{-\Next}$}

\newcommand{\fract}[1]{\textrm{fract}\left({#1}\right)}
\newcommand{\proj}[2]{{#2}_{#1}}
\newcommand{\lcd}{d}

\newcommand{\upcell}[2]{{{#1}\uparrow}^{#2}}
\newcommand{\downcell}[2]{{{#1}\downarrow}_{#2}}
\newcommand{\updowncell}[3]{{{#1}\updownarrow}_{#3}^{#2}}
\newcommand{\graphcell}[2]{{{#1}_{#2}}}

\newcommand{\Part}[1]{2^{#1}}

\DeclareMathAlphabet{\mathpzc}{OT1}{pzc}{m}{it}
\newcommand{\LabelSet}{\Delta}
\newcommand{\CLabel}{\LabelSet_{C}}
\newcommand{\DLabel}{\LabelSet_{D}}
\newcommand{\PropSym}{\mathpzc{S}}

\newcommand{\Next}{\circ}
%\newcommand{\Next}{\mathscr{X}}
\newcommand{\Until}{\mathscr{U}}
\newcommand{\Eventually}{\Diamond}
%\newcommand{\Eventually}{\mathscr{F}}
\newcommand{\Globally}{\Box}
%\newcommand{\Globally}{\mathscr{G}}
\newcommand{\Release}{\mathscr{R}}

%\renewcommand{\nmodels}{\nvDash}

\newcommand{\AllPaths}{\mathtt{A}}
\newcommand{\SomePaths}{\mathtt{E}}

\DeclareRobustCommand{\SACoRe}{%
\raisebox{0pt}[0pt][0pt]{%
S{\hskip-0.2ex}\raisebox{-0.3ex}{A}{\hskip-0.2ex}Co\raisebox{-0.3ex}{Re}%
}}

\newcommand{\sgn}{\operatorname{sgn}}

\newcommand{\ath}[2][\lambda,\alpha]{h_{#1}({#2})}

%\pgfmathdeclarefunction{h}{3}{%
% % \pgfmathparse{(#1<-#3/#2)*tanh(-#3) + ({#1}>{#3}/{#2})*tanh({#3}) + (and({#1}<={#3}/{#2},{#1}>=-1*{#3}/{#2}))*(tanh({#3}*{#2}*{#1})/{#3})}
% \pgfmathparse{(#1<-#3/#2)*-1+ (#1>#3/#2)*1 + (and(#1<=#3/#2,#1>=-#3/#2))*(#2*#1)/#3)}
%}
%
%\pgfmathdeclarefunction{j}{1}{%
% % \pgfmathparse{(#1<-#3/#2)*tanh(-#3) + ({#1}>{#3}/{#2})*tanh({#3}) + (and({#1}<={#3}/{#2},{#1}>=-1*{#3}/{#2}))*(tanh({#3}*{#2}*{#1})/{#3})}
% \pgfmathparse{(#1<0)*-1+ (#1>=0)*1}
%}

\newcommand{\ls}{[|}
\newcommand{\rs}{|]}
\newcommand{\deq}{\stackrel{def}{=}}

\usepackage{xifthen}

%\newcommand{\hstatesymb}{a}
\newcommand{\hstate}[1]{%
\ifthenelse{\isempty{#1}}%
    {a}% if #1 is empty
    {a_{#1}}% if #1 is not empty
}

%\newcommand{\hlocsymb}{v}
%\newcommand{\hloc}[1]{%
%\ifthenelse{\isempty{#1}}%
%    {v}% if #1 is empty
%    {v_{#1}}% if #1 is not empty
%}

\newcommand{\hloc}[1]{v_{#1}}

\def\edist{\delta}


\newcommand{\MFOL}{\textbf{MFO}}
\newcommand{\SFOL}{\textbf{SFO}}

\newcommand{\typeDef}{\mathit{T}}
\newcommand{\type}[1]{{\typeDef({#1})}}

\newcommand{\otype}[1]{#1\Vdash}


\newcommand{\Supports}{\mathtt{Sup}}
\newcommand{\ValVar}{M}
\newcommand{\ValConst}{\mathtt{Const}}
\newcommand{\ValFun}{\mathtt{Funct}}
\newcommand{\ValRel}{\mathtt{Rel}}
%\newcommand{\ValPropOp}{\mathtt{PropOp}}

\newcommand{\ConstImg}{\mathcal{C}}

\newcommand{\asterm}{{\tt a}}

\newcommand{\BV}[1]{\mathit{Bound}({#1})}
\newcommand{\NBV}[1]{\mathit{NotBound}({#1})}
\newcommand{\NV}[1]{\mathit{NotIn}({#1})}

\newcommand{\function}{\mathbf{f}}
\newcommand{\relation}{\fallingdotseq}
\newcommand{\mult}{*}
\newcommand{\vmult}{\cdot}

%\newcommand\mitvl[1]{\llparenthesis{#1}\rrparenthesis}
\newcommand{\lbound}[2][]{\VarNotation{\llparenthesis}{#1}{#2}}
\newcommand{\rbound}[2][]{\VarNotation{\rrparenthesis}{#1}{#2}}
\newcommand{\mitvl}[3][]{\lbound{}{#3}\rbound[#1]{#2}}

\newcommand{\lineq}[2][]{\VarNotation{\preccurlyeq}{#1}{#2}}
\newcommand{\rineq}[2][]{\VarNotation{\curlyeqprec}{#1}{#2}}

\newcommand{\tostdsem}[2][\epsilon]{\widehat{\left(#2\right)}_{#1}}


main.tex
\documentclass[submission,copyright,creativecommons]{eptcs}
\providecommand{\event}{HSB 2012} % Name of the event you are submitting to
\usepackage{breakurl}             % Not needed if you use pdflatex only.

\usepackage{ifpdf} 
\ifpdf 
\usepackage{graphicx}

\DeclareGraphicsExtensions{.pdf,.png,.mps}
\usepackage{pgf}
\else
\usepackage[dvipdfm]{graphicx}
\fi 

\usepackage[cmex10]{amsmath}
\usepackage{amsfonts,amsthm,amssymb}
\usepackage{stmaryrd}
%\usepackage{pxfonts}
\usepackage[mathscr]{euscript}
\usepackage{pgf}
\usepackage{tikz}
\usepackage{subfigure}
\usepackage{algorithm,algorithmic} 
\usepackage{enumitem}

%\usepackage{pgfplots}
%\usepackage{tkz-fct}

\usetikzlibrary{arrows,automata}

\title{Hybrid Automata and $\epsilon$-Analysis on a Neural Oscillator\thanks{
This work has been partially supported by Istituto Nazionale di Alta Matematica (INdAM).}}
\author{Alberto Casagrande
\institute{Dept. of Matematics and Geoscience\\
University of Trieste, Italy}
\email{acasagrande@units.it}
\and
Tommaso Dreossi \qquad\qquad Carla Piazza
\institute{Dept. of Matematics and Computer Science\\
University of Udine, Italy}
\email{\quad dreossi.tommaso@spes.uniud.it \quad\qquad carla.piazza@uniud.it}
}
\def\titlerunning{Hybrid Automata and $\epsilon$-Analysis on a Neural Oscillator}
\def\authorrunning{A.~Casagrande, T.~Dreossi \& C.~Piazza}

\graphicspath{{./figures/}}

\input{macro}

\begin{document}
\maketitle

\begin{abstract}
In this paper we propose a hybrid model of a neural oscillator, obtained by partially discretizing a well-known continuous model.
Our construction points out that in this case the standard techniques, based on replacing sigmoids with step functions, is not 
satisfactory.
%
Then, we study the hybrid model through both symbolic methods and approximation techniques. This last analysis, in particular, allows
us to show the differences between the considered approximation approaches.
%
Finally, we focus on approximations via $\epsilon$-semantics, proving how these can be computed in practice. 
\end{abstract}

\input{introduction}
\input{logics}
\input{hybrid}
\input{neural}
\input{franzle}
\input{girard}
\input{epsilon-sem}
\input{analysis}
\input{new_results_epsilon}
\input{conclusions}

%\nocite{*}
\bibliographystyle{eptcs}
\bibliography{hybridbib}
%\bibliography{hybridbib,macsyma}
\end{document}

neural.tex
% !TEX root = main.tex
\section{Neural Oscillator: Continuous and Hybrid Models}\label{sec:model}

Oscillatory electrical stimuli have been considered central for the activities 
of  several brain regions since the begin of the '80s. It was shown that they play 
an important role in the olfactory information processing~\cite{citeulike:762104} 
and they were observed %in the hippocampus~\cite{Traub:1991:NNH:574330}, 
in 
the thalamus~\cite{citeulike:4043128}, and in the cortex~\cite{1824881}. 
Many studies suggested that, in the mammalian visual system, 
neurons signals may be group together through in-phase 
oscillations~\cite{citeulike:547881}. % (see e.g.,~\cite{citeulike:547881}). 
Because of this, the development and analysis of models representing 
oscillatory phenomena assume a great importance in 
%the understanding of neurophysiological activities. 
understanding  the neurophysiological activities.


A simple continuous model of a single oscillator has been proposed in~\cite{Tonnelier19991213}. 
The model describes the evolutions of one excitatory neuron ($N_e$) and one inhibitory neuron ($N_i$) 
by mean of the ordinary differential system.  
\begin{equation}\label{eq:origsystem}
f(\tau,\lambda):\; \left\{\begin{array}{l}
\dot{\X{e}}=-\frac{\X{e}}{\tau}+\tanh{(\lambda*\X{e})}-\tanh{(\lambda*\X{i})}\\
\dot{\X{i}}=-\frac{\X{i}}{\tau}+\tanh{(\lambda*\X{e})}+\tanh{(\lambda*\X{i})}
\end{array}\right., 
\end{equation}
where $\X{e}$ and $\X{i}$ are the output of $N_e$ and $N_i$, respectively, 
$\tau$ is a characteristic time constant, and $\lambda>0$ is the amplification gain.
%
Hopf bifurcation characterizes a qualitative change in the evolution of $f(\tau,\lambda)$: %In particular, 
if $\tau*\lambda\leq 1$, then the point $\tuple{0,0}$ is the unique global attractor of the system, if, otherwise, 
$\tau*\lambda>1$, the origin is an unstable equilibrium and all the evolutions converge to a limit cycle 
attractor% whose period is $T_{p}\approx \frac{2\pi}{\lambda}$
~\cite{DBLP:journals/ijns/AtiyaB89}.
A simulation of $f(3,1)$ is represented in Fig.~\ref{fig:origevo}.


\begin{figure}[!h]
\begin{center}
 \subfigure[The automaton %$H_{\hat{f}}$
  has 4 locations. 
The dashed lines denote both the boundaries of the invariants and the activation regions.  
The resets are identify functions.]
   {\includegraphics[width=0.41\textwidth]{automaton1.pdf}\label{fig:badapprox}}
    \hspace{5mm}
 \subfigure[Direction field and evolution of the automaton  %$\hat{f}(3)$ 
 from the two points $\tuple{-\frac{1}{2},-\frac{1}{2}}$ and 
 $\tuple{-1,6}$ when $\tau=3$. The automaton has four attractors, is not periodic, and   
its principal axes are stable.]
   {\includegraphics[width=0.50\textwidth]{hybrid_bad_evolution.pdf}\label{fig:badevo}}

\caption{The piecewise hybrid automaton associated to the function $\hat{f}(\tau)$.%
}%\label{fig:badapprox}
\end{center}
\end{figure}

Even if $f(\tau,\lambda)$ %System~\ref{eq:origsystem} 
is rather simple, the ability of analyzing a complex system obtained 
by composing multiple copies of this model is limited due to the non-linearity of $f(\tau,\lambda)$ itself. 
For this reason, we are interested in the development of a piecewise affine 
hybrid model whose behaviour fairly approximates System (\ref{eq:origsystem}) and that can be automatically 
analyzed and composed. 

Since the non-linear components in System~(\ref{eq:origsystem}) have the form $\tanh{(\lambda*\X{})}$, 
we try to linearize such function. 
In the case of genetic networks it is quite standard to approximate sigmoidal behaviours (e.g., $\tanh$) through 
the sign function $\sgn$~\cite{tomlinmodel,springerlink:10.1016/j.bulm.2003.08.010}. Such approximation replaces a continuous signal with a discrete 
off-on one. %(see Fig.~\ref{fig:badapproxtanh}). 
In our case, by replacing $\tanh{(\lambda*\X{})}$ 
with $\sgn{(\X{})}$ in System~(\ref{eq:origsystem}), we obtain the following differential 
system:
\begin{equation}
\hat{f}(\tau):\; \left\{\begin{array}{l}
\dot{\X{e}}=-\frac{\X{e}}{\tau}+\sgn{(\X{e})}-\sgn{(\X{i})}\\
\dot{\X{i}}=-\frac{\X{i}}{\tau}+\sgn{(\X{e})}+\sgn{(\X{i})}
\end{array}\right. ,
\end{equation}
which corresponds to the piecewise hybrid model depicted in Fig.~\ref{fig:badapprox}.
Unfortunately, the behaviour of this model is quite different from that of System~(\ref{eq:origsystem}), as 
we can see comparing the simulation in Fig.~\ref{fig:badevo} with that of Fig.~\ref{fig:origevo}. In particular, 
the model based on $\hat{f}(\tau)$ has four 
attractors with coordinates $\tuple{-2*\tau,0}$, $\tuple{0,-2*\tau}$, $\tuple{2*\tau,0}$, and $\tuple{0,2*\tau}$, it is 
not periodic, and  its principal axes are stable.  %(see Fig.~\ref{fig:badevo}).   
%
%\begin{figure}[!h]
%\begin{center}
% \subfigure[The automaton %$H_{\hat{f}}$
%  has 4 locations. 
%The dashed lines denote both the boundaries of the invariants and the activation regions.  
%The resets are identify functions.]
%   {
%\begin{tikzpicture}[cap=round,scale=0.75, transform shape]
%  \def\a{3.0}
%  \def\b{1.0}
%  \def\c{2.0}
%  \def\l{1.8}
%  
%  % Styles
%  \tikzstyle{axes}=[very thin, color=black!30]
%  \tikzstyle{boundary}=[very thick,dashed]
%
%  % The graphic
%  \draw[style=help lines,step=\c/\b*0.8,color=black!30] (-\l*\c/\b,-\l*\c/\b) grid (\l*\c/\b,\l*\c/\b);
%
%  \begin{scope}[style=axes]
%    \draw[->] (-1.1*\l*\c/\b,0) -- (1.1*\l*\c/\b,0) node[right] {$\X{e}$};
%    \draw[->] (0,-1.1*\l*\c/\b) -- (0,1.1*\l*\c/\b) node[above] {$\X{i}$};
%  \end{scope}
%
%  \begin{scope}[style=boundary]
%   \draw(0,\l*\c/\b) -- (0,-\l*\c/\b){};
%    \draw(\l*\c/\b,0) -- (-\l*\c/\b,0) {};
%  \end{scope}
%  
%    \def\up{{\l*\c/(2*\b)}}
%    \def\down{{-\up}}
%  
%    \node (S0) at (\up,\up) { 
%                                   \begin{tabular}{l}
%                                   $\dot{\X{e}}=-\frac{\X{e}}{\tau}$\\
%                                   $\dot{\X{i}}=-\frac{\X{i}}{\tau}+2$\\
%                                   \end{tabular}};
%   \node (L0) at (0,\l*\c/\b) [below right] {\Large${\hloc{0}}$};
%   
%    \node (S1) at (\down,\up) { 
%                                    \begin{tabular}{l}
%                                   $\dot{\X{e}}=-\frac{\X{e}}{\tau}-2$\\
%                                   $\dot{\X{i}}=-\frac{\X{i}}{\tau}$\\
%                                   \end{tabular}};
%   \node (L1) at ({-\l*\c/\b},\l*\c/\b) [below right] {\Large${\hloc{1}}$};
%   
%    \node (S2) at (\down,\down) { 
%                                    \begin{tabular}{l}
%                                   $\dot{\X{e}}=-\frac{\X{e}}{\tau}$\\
%                                   $\dot{\X{i}}=-\frac{\X{i}}{\tau}-2$\\
%                                   \end{tabular}};
%   \node (L2) at ({-\l*\c/\b},0) [below right] {\Large${\hloc{2}}$};
%
%    \node (S3) at (\up,\down) { 
%                                    \begin{tabular}{l}
%                                   $\dot{\X{e}}=-\frac{\X{e}}{\tau}+2$\\
%                                   $\dot{\X{i}}=-\frac{\X{i}}{\tau}$\\
%                                   \end{tabular}};
%   \node (L3) at (0,0) [below right] {\Large${\hloc{3}}$};
%
%\end{tikzpicture}\label{fig:badapprox}
%}
%    \hspace{5mm}
% \subfigure[Direction field and evolution of the automaton  %$\hat{f}(3)$ 
% from the two points $\tuple{-\frac{1}{2},-\frac{1}{2}}$ and 
% $\tuple{-1,6}$ when $\tau=3$. The automaton has four attractors, is not periodic, and   
%its principal axes are stable.]
%   {\includegraphics[width=0.50\textwidth]{hybrid_bad_evolution.pdf}\label{fig:badevo}}
%
%\caption{The piecewise hybrid automaton associated to the function $\hat{f}(\tau)$.%
%}%\label{fig:badapprox}
%\end{center}
%\end{figure}


A more sophisticated approximation of $\tanh{(\lambda*\X{})}$ 
is the piecewise linear function: 
\begin{equation}
\ath[{\lambda,\alpha}]{z} \defeq \left\{\begin{array}{l l}
-1 & \text{if }z< -\frac{\alpha}{\lambda}\\
\frac{\lambda}{\alpha}*z & \text{if }-\frac{\alpha}{\lambda} \leq z < \frac{\alpha}{\lambda}\\
1 & \text{if }z\geq \frac{\alpha}{\lambda}
\end{array}\right. ,
\end{equation}
where $\alpha$ is the approximation coefficient which determines the slope 
of the central segment. %(see Fig.~\ref{fig:goodapproxtanh}). 
The substitution of $\tanh{(\lambda*\X{})}$ with 
$\ath[{\lambda,\alpha}]{z}$ in System~(\ref{eq:origsystem}) leads to 
the system:  
\begin{equation}
\tilde{f}_{\alpha}(\tau,\lambda):\; \left\{\begin{array}{l}
\dot{\X{e}}=-\frac{\X{e}}{\tau}+\ath{\X{e}}-\ath{\X{i}}\\
\dot{\X{i}}=-\frac{\X{i}}{\tau}+\ath{\X{e}}+\ath{\X{i}}
\end{array}\right. ,
\end{equation}
whose corresponding hybrid automaton  is depicted in Fig.~\ref{fig:goodapprox}. 
A different %multi-step 
approximation could be obtained by using the technique 
proposed in~\cite{Grosu:2011fk}. %, however this is out of our interests. 


%\begin{figure}[!h]
%%\begin{minipage}[b]{7.5cm}
%\centering
% \subfigure[$\sgn{(\X{})}$ approximating $\tanh{(\lambda*\X{})}$.]
%   {
%   \begin{tikzpicture}[domain=-30:30,scale=0.70, transform shape]
%      \begin{scope}
%      %\pgfplotsset{x ticks=none}
%      \begin{axis}[grid=major,legend pos=north west,use fpu=false,xtick={0.0}]
%      \addplot[samples=300,style=dashed, ultra thick]{tanh(0.1*x)};
%        \addplot[samples=300,ultra thick]{j(x)};
%         \legend{$\tanh{(\lambda*\X{})}$,$\sgn{(\X{})}$}
%       %\draw ({rel axis cs:0,0}-|{axis cs:0,0}) -- ({rel axis cs:0,1}-|{axis cs:0,0});
%              \draw[dotted] ({rel axis cs:15,0}-|{axis cs:15,0}) -- ({rel axis cs:15,1}-|{axis cs:15,0}) node [pos=0.5,right] {$\X{}=\frac{\alpha}{\lambda}$};
%       \draw[dotted] ({rel axis cs:-15,0}-|{axis cs:-15,0}) -- ({rel axis cs:-15,1}-|{axis cs:-15,0}) node [pos=0.5,left] {$\X{}=-\frac{\alpha}{\lambda}$};
%      \end{axis}
%   \end{scope}
%\end{tikzpicture}\label{fig:badapproxtanh}
%   }
%    \hspace{7mm}
% \subfigure[$\ath{\X{}}$ approximating $\tanh{(\lambda*\X{})}$.]
%   {
%\begin{tikzpicture}[domain=-30:30,scale=0.70, transform shape]
%      \begin{scope}
%      %\pgfplotsset{x ticks=none}
%      \begin{axis}[grid=major,legend pos=north west,use fpu=false,xtick={0.0}]
%      \addplot[samples=300,style=dashed, ultra thick]{tanh(0.1*x)};
%      \addplot[samples=300,ultra thick]{h(x,0.1,1.5)};
%         \legend{$\tanh{(\lambda*X{})}$,$\ath[{\lambda,\alpha}]{\X{}}$}
%       %\draw ({rel axis cs:0,0}-|{axis cs:0,0}) -- ({rel axis cs:0,1}-|{axis cs:0,0});
%       \draw[dotted] ({rel axis cs:15,0}-|{axis cs:15,0}) -- ({rel axis cs:15,1}-|{axis cs:15,0}) node [pos=0.5,right] {$\X{}=\frac{\alpha}{\lambda}$};
%       \draw[dotted] ({rel axis cs:-15,0}-|{axis cs:-15,0}) -- ({rel axis cs:-15,1}-|{axis cs:-15,0}) node [pos=0.5,left] {$\X{}=-\frac{\alpha}{\lambda}$};
%      \end{axis}
%   \end{scope}
%\end{tikzpicture}\label{fig:goodapproxtanh}}
%
%\caption{Both $\ath[\lambda,\alpha]{\X{}}$ and $\sgn{(\X{})}$ can be used as piecewise linear approximations of $\tanh{(\lambda*\X{})}$.}\label{fig:tanhapprox}
%\end{figure}

\begin{figure}[!h]
\begin{center}
\includegraphics[width=0.67\textwidth]{automaton2.pdf}
\caption{A graphical representation of the hybrid automaton $H_{\tilde{f}}$ associated to the function $\tilde{f}_{\alpha}(\tau,\lambda)$.}\label{fig:goodapprox}
\end{center}
\end{figure}

 In the rest of the paper we present some general techniques for studying hybrid automata and
 then we apply them to $H_{\hat{f}}$ to formally prove its properties.

\begin{figure}[!ht]
 \centering
 \subfigure[An evolution of $f(3,1)$.]
   {\includegraphics[width=0.48\textwidth]{original_evolution.pdf}\label{fig:origevo}}
%    \hspace{5mm}
% \subfigure[An evolution of $\hat{f}(3)$]
%   {\includegraphics[width=0.30\textwidth]{hybrid_bad_evolution.pdf}\label{fig:badevo}}
 \hspace{3mm}
 \subfigure[An evolution of $\tilde{f}_{2}(3,1)$.]
   {\includegraphics[width=0.48\textwidth]{hybrid_good_evolution.pdf}\label{fig:goodevo}}
    \caption{Direction field and evolution of the models discussed in Section~\ref{sec:model}.}\label{fig:diamond_cycle}
 \end{figure}
 
% In the rest of the paper we present some general techniques for studying hybrid automata and
% then we apply them to $H_{\hat{f}}$ to formally prove its properties.

new_results_epsilon.tex
% !TEX root = main.tex
\section{Computing Sphere Semantics}\label{sec:computing}
In this section we show how sphere semantics can be computed exploiting tools for cylindrical algebraic decomposition.
In particular, we introduce a translation from sphere semantics to standard semantics.
Then, we apply the translation to study the ``sphere'' behaviour of our neural oscillator example.

\subsection{A translation into standard semantics}

If $\Theory$ is a first-order theory and $\edist$ is a distance definable in $\Theory$, then 
the sphere semantics of any formula in $\Theory$ is $\Theory$-definable in the standard semantics, i.e., 
for any formula $\NotBoundIn{\varphi}{\vX{}} \in \Theory$  
we can compute a formula $\NotBoundIn{\tostdsem{\varphi}}{\vX{}} \in \Theory$ such that 
$\sphsem{\NotBoundIn{\varphi}{\vX{}} } = \stdsem{ \NotBoundIn{\tostdsem{\varphi}}{\vX{}}  }$ for all $\epsilon \in \bbbr_{>0}$. 

In order to achieve this goal, we need to distinguish two kind 
of variables: the variables of the original formula (named $\W{}$, $\W{i}$, $\vW{}$ and $\vW{i}$), whose evaluations follow 
the rules of the sphere semantics, and the auxiliary variables (named $\Y{}$, $\Y{i}$, $\vY{}$ and $\vY{i}$)
that will be introduced to encode the sphere semantics into the standard one. From the point of view 
of the sphere semantics the later can seen as symbolic constants, even if they will be quantified in the formula 
$\tostdsem{\varphi}$. In particular, we will use them to %exclusively 
characterize sets of the form $\sphsem{\bigwedge_{r \in \bbbr} \VarSSub{\varphi}{r,\vW{}}}$ and 
$\sphsem{\bigvee_{r \in \bbbr} \VarSSub{\varphi}{r,\vW{}}}$ in the standard semantics. 

\begin{definition}[Translation]\label{def:tostdsem}
Let $\Theory$ be a first-order theory over the reals, $\NotBoundIn{\varphi}{\vY,\vW{}}$ be any first-order formula $\Theory$-definable, and $\epsilon \in  \mathbb{R}_{> 0}$.
We define $\NotBoundIn{\tostdsem{\varphi}}{\vY,\vW{}}$ by structural induction on $\NotBoundIn{\varphi}{\vY,\vW{}}$ itself.  
\begin{enumerate}
%\item	if $\NotBoundIn{\varphi}{\vY{},\vX{}}$ is an atomic formula, then  $\NotBoundIn{\tostdsem{\varphi}}{\vY{},\vX{}} \defeq  \exists \vX{0}(\VarSSub{\varphi}{\vY{},\vX{0}} \wedge \edist(\vX{0},\vX{}) < \epsilon)$;
\item\label{trans:atomic} $\tostdsem{\NotBoundIn{(t_1 \circ t_2)}{\vY{},\vW{}}} \defeq \exists \vW{0}(\VarSSub{(t_1 \circ t_2)}{\vY{},\vW{0}} \wedge \edist(\vW{0},\vW{}) < \epsilon)$, for $\circ \in \{=,<\}$;
%\item	if $\NotBoundIn{\varphi}{\vY{},\vX{}}$ has the form $\psi[\vY{},\vX{}] \land \psi[\vY{},\vX{}]$, then  
%$\NotBoundIn{\tostdsem{\varphi}}{\vY{},\vX{}} \defeq \exists \vX{0} \forall \vX{1} ((\edist(\vX{0},\vX{1}) < \epsilon \limply (\VarSSub{\tostdsem{\psi}}{\vY{},\vX{1}} \land \VarSSub{\tostdsem{\psi}}{\vY{},\vX{1}})) \land \edist(\vX{0},\vX{}) < \epsilon)$;
\item\label{trans:disjunction} 
%$\tostdsem{\NotBoundIn{\psi}{\vY{},\vW{}} \lor \NotBoundIn{\psi}{\vY{},\vW{}}} \defeq \tostdsem{\NotBoundIn{\psi}{\vY{},\vW{}}} \lor \tostdsem{\NotBoundIn{\psi}{\vY{},\vW{}}}$;
$\tostdsem{\phi\lor\psi} \defeq %
\tostdsem{\phi} \lor \tostdsem{\psi}$;
%\item if $\NotBoundIn{\varphi}{\vX{}}$ has the form $\NotBoundIn{\psi}{\vX{}} \lor \NotBoundIn{\psi}{\vX{}}$, then $\NotBoundIn{\tostdsem{\varphi}}{\vX{}} \defeq \NotBoundIn{\widehat{\psi}(\epsilon)}{\vX{}} \lor \NotBoundIn{\widehat{\psi}(\epsilon)}{\vX{}}$;
\item\label{trans:conj} $\tostdsem{\NotBoundIn{\phi}{\vY{},\vW{}} \land \NotBoundIn{\psi}{\vY{},\vW{}}} \defeq 
\exists \vW{0} (\forall \vW{1} (\edist(\vW{0},\vW{1}) < \epsilon \limply \VarSSub{(\tostdsem{\phi}\land \tostdsem{\psi})}{\vY{},\vW{1}})\land \edist(\vW{0},\vW{}) < \epsilon)$;
\item\label{trans:for} $\tostdsem{\forall \W{} \NotBoundIn{\phi}{\vY{},\W{},\vW{}}} \defeq 
\exists \vW{0} ( \forall \vW{1} (\edist(\vW{0},\vW{1}) < \epsilon \limply \forall \Y{} \tostdsem{\VarSSub{\phi}{\vY{},\Y{},\vW{1}}})\land \edist(\vW{0},\vW{}) < \epsilon)$;
\item\label{trans:exists} $\tostdsem{\exists \W{} \NotBoundIn{\phi}{\vY{},\W{},\vW{}}} \defeq  \exists \Y{} \tostdsem{\VarSSub{\phi}{\vY{},\Y{},\vW{1}}}$;
\item\label{trans:neg} $\tostdsem{\NotBoundIn{\neg \phi}{\vY{},\vW{}}} \defeq 
\exists \vW{0} ( \forall \vW{1} (\edist(\vW{0},\vW{1}) < \epsilon \limply \neg \tostdsem{\VarSSub{\phi}{\vY{},\vW{1}}})\land \edist(\vW{0},\vW{}) < \epsilon)$.
\end{enumerate}

\end{definition}

\begin{theorem}[Semantics Equivalence]
Let $\Theory$ be any first-order theory and $\edist$ be a  
$\Theory$-definable distance. 
The sphere semantics $\sphsem{.}$ of $\Theory$ is $\Theory$-definable in the standard semantics and,  
in particular, 
$\sphsem{\NotBoundIn{\varphi}{\vX{}} } = \stdsem{ \NotBoundIn{\tostdsem{\varphi}}{\vX{}}  }$ 
for any formula $\NotBoundIn{\varphi}{\vX{}} \in \Theory$ and all $\epsilon \in \bbbr_{>0}$.
\end{theorem}
%\begin{proof}
%By structural induction on $\varphi$. We follow the indexes of the $\tostdsem{\varphi}$'s definition.  
%
%%\begin{enumerate}
%\begin{description}
%\item
%$\NotBoundIn{\varphi}{\vY{},\vW{}}$ is atomic.\\
%%$\sphsem{\NotBoundIn{(t_1 \circ t_2)}{\vY{},\vW{}}}=\stdsem{\tostdsem{\NotBoundIn{(t_1 \circ t_2)}{\vY{},\vW{}}}}$, for $\circ \in \{=,<\}$
%%\begin{proof}
%By the definition of 
%$\sphsem{\cdot}$, 
%%$\sphsem{\NotBoundIn{(t_1 \circ t_2)}{\vY{},\vW{}}}=\eball{\stdsem{\NotBoundIn{(t_1 \circ t_2)}{\vY{},\vW{}}}}$. 
%$\sphsem{\NotBoundIn{\varphi}{\vY{},\vW{}}}=\eball{\stdsem{\NotBoundIn{\varphi}{\vY{},\vW{}}}}$.
%Since $\vY{}$ is a vector of auxiliary variables, we should threat them as symbolic constants 
%and we must not consider them as free variables. 
%Hence, $\tuple{\vec{y},\vec{w}} \in \sphsem{\NotBoundIn{\varphi}{\vY{},\vW{}}}$ if and only if there exists a $\vec{w_0}$ such that 
%$\edist(\vec{w},\vec{w_0})<\epsilon$ and 
% $\stdsem{\VarSSub{\varphi}{\vec{y},\vec{w_0}}}$. By the standard semantics, the later sentence holds if and only if 
% $\exists \vW{0}  (\VarSSub{\varphi}{\vY{},\vW{0}}\land \edist(\vW{0},\vW{}) < \epsilon)$ does the same. 
%%\end{proof}
%
%\item
%$\NotBoundIn{\varphi}{\vY{},\vW{}}$ has the form $\NotBoundIn{\phi}{\vY{},\vW{}} \lor \NotBoundIn{\psi}{\vY{},\vW{}}$.\\
%By the definition of sphere semantics, $\sphsem{\phi \lor \psi}=
%\sphsem{\phi} \cup \sphsem{\psi}$. By inductive hypothesis,  both 
%$\sphsem{\phi}=\stdsem{\tostdsem{\phi}}$ and 
%$\sphsem{\psi}=\stdsem{\tostdsem{\psi}}$. From the standard semantics and the definition of $\tostdsem{\cdot}$, 
%we deduce the thesis. %follows. % that 
%%$\sphsem{\NotBoundIn{\psi}{\vX{}} \lor \NotBoundIn{\psi}{\vX{}}}=\stdsem{\NotBoundIn{\widehat{\psi}(\epsilon)}{\vX{}} \lor \NotBoundIn{\widehat{\psi}(\epsilon)}{\vX{}}}$. 
%
%\item $\NotBoundIn{\varphi}{\vY{},\vW{}}$ has the form $\NotBoundIn{\phi}{\vY{},\vW{}} \land \NotBoundIn{\psi}{\vY{},\vW{}}$.\\
%By the definition, $\sphsem{\NotBoundIn{\phi}{\vY{},\vW{}} \land \NotBoundIn{\psi}{\vY{},\vX{}}} \defeq 
%\bigcup_{\eball{\{p\}}\subseteq \sphsem{\phi}\cap \sphsem{\psi}}\eball{\{p\}}$, while, by inductive hypotheses,  
%$\sphsem{\phi}=\stdsem{\tostdsem{\phi}}$ and 
%$\sphsem{\psi}=\stdsem{\tostdsem{\psi}}$.  
%From the standard semantics, we deduce that 
%$\sphsem{\NotBoundIn{\psi}{\vY{},\vX{}} \land \NotBoundIn{\psi}{\vY{},\vX{}}}=
%\bigcup_{\eball{\{p\}}\subseteq \stdsem{\tostdsem{\phi} \land \tostdsem{\psi}}}\eball{\{p\}}$. The 
%righter term of the last equation is the union of all the $\epsilon$-balls entirely included into 
%the standard semantics of $\tostdsem{\psi} \land \tostdsem{\psi}$. 
%Any $w$ is included into such a union if and only if there exists a $w_0$ such that all the points included into 
%the $\epsilon$-ball centered in $w_0$ satisfy $\NotBoundIn{\tostdsem{\phi}}{\vY{},\vW{}} \land 
%\NotBoundIn{\tostdsem{\psi}}{\vY{},\vW{}}$ and $w$ is included into the $\epsilon$-ball itself. 
%By the standard semantics, the later sentence holds if and only if 
% the formula $$\exists \vW{0} (\forall \vW{1} (\edist(\vW{0},\vW{1}) < \epsilon \limply 
% \VarSSub{(\tostdsem{\phi}\land \tostdsem{\psi})}{\vY{},\vW{1}})\land \edist(\vW{0},\vW{}) < \epsilon)
%$$ does the same.
%
%\item $\NotBoundIn{\varphi}{\vY{},\vW{}}$ has the form $\forall \W{} \NotBoundIn{\phi}{\vY{},\W{},\vW{}}$.\\
%By the definition, $\sphsem{ \forall \W{} \NotBoundIn{\phi}{\vY{},\W{},\vW{}} } \defeq 
%\sphsem{\bigwedge_{r \in \bbbr}  \VarSSub{\phi}{\vY,r,\vW{}}}$. Because of the 
%$\land$-rule, this means that  $\sphsem{ \forall \W{} \NotBoundIn{\phi}{\vY{},\W{},\vW{}} } = 
%\bigcup_{\eball{\{p\}}\subseteq \stdsem{\bigwedge_{r \in \bbbr} \tostdsem{\VarSSub{\phi}{\vY,r,\vW{}}}}}\eball{\{p\}}$. 
%The 
%righter term of the last equation is the union of all the $\epsilon$-balls entirely included into 
%the standard semantics of the formula $\bigwedge_{r \in \bbbr} \tostdsem{\VarSSub{\phi}{\vY,r,\vW{}}}$. 
%However, a point $\tuple{\vec{y},\vec{w}}$ belongs to $\stdsem{\bigwedge_{r \in \bbbr} \tostdsem{\VarSSub{\phi}{\vY{},r,\vW{}}}}$ 
%if and only if $\tuple{\vec{y},\vec{w}}$ itself belongs to $\stdsem{\tostdsem{\VarSSub{\phi}{\vY{},y,\vW{}}}}$ for all $y \in \bbbr$. 
%Hence, $\stdsem{\bigwedge_{r \in \bbbr} \tostdsem{\VarSSub{\phi}{\vY{},r,\vW{}}}}$ is equivalent to 
%$\stdsem{\forall \Y{} \tostdsem{\VarSSub{\phi}{\vY{},\Y{},\vW{}}}}$. Let us notice that the new quantified variable 
%$\Y{}$ should not be expanded %as it was an original variable of $\phi$ 
%since it was introduced exclusively to 
%characterize the set $\stdsem{\bigwedge_{r \in \bbbr} \tostdsem{\VarSSub{\phi}{\vY{},r,\vW{}}}}$. 
%By using  the same argument used in the proof of the $\land$-case, we can conclude that 
%$\sphsem{ \forall \W{} \NotBoundIn{\phi}{\vY{},\W{},\vW{}} }$ is defined in the standard semantics by the formula
%$$\exists \vW{0} (\forall \vW{1} (\edist(\vW{0},\vW{1}) < \epsilon \limply 
% \forall \Y{} \tostdsem{\VarSSub{\phi}{\vY{},\Y{},\vW{1}}})\land \edist(\vW{0},\vW{}) < \epsilon).$$
% 
%\item $\NotBoundIn{\varphi}{\vY{},\vW{}}$ has the form $\exists \W{} \NotBoundIn{\phi}{\vY{},\W{},\vW{}}$.\\
%By the definition, $\sphsem{ \exists \W{} \NotBoundIn{\phi}{\vY{},\W{},\vW{}} } \defeq 
%\sphsem{\bigvee_{r \in \bbbr}  \VarSSub{\phi}{\vY,r,\vW{}}}$. Because of the 
%$\lor$-rule, this means that  $\sphsem{ \exists \W{} \NotBoundIn{\phi}{\vY{},\W{},\vW{}} } = 
%\bigcup_{\eball{\{p\}}\subseteq \stdsem{\bigvee_{r \in \bbbr} \tostdsem{\VarSSub{\phi}{\vY,r,\vW{}}}}}\eball{\{p\}}$. 
%The 
%righter term of the last equation is the union of all the $\epsilon$-balls entirely included into 
%the standard semantics of the formula $\bigvee_{r \in \bbbr} \tostdsem{\VarSSub{\phi}{\vY,r,\vW{}}}$. 
%However, a point $\tuple{\vec{y},\vec{w}}$ belongs to $\stdsem{\bigvee_{r \in \bbbr} \tostdsem{\VarSSub{\phi}{\vY{},r,\vW{}}}}$ 
%if and only if there exists a $y$ such that $\tuple{\vec{y},\vec{w}}$  belongs also to $\stdsem{\tostdsem{\VarSSub{\phi}{\vY{},y,\vW{}}}}$. Hence, $\stdsem{\bigvee_{r \in \bbbr} \tostdsem{\VarSSub{\phi}{\vY{},r,\vW{}}}}$ is equivalent to 
%$\stdsem{\exists \Y{} \tostdsem{\VarSSub{\phi}{\vY{},\Y{},\vW{}}}}$. 
%Hence, we can conclude that  the two sets  
%$\sphsem{ \exists \W{} \NotBoundIn{\phi}{\vY{},\W{},\vW{}} }$ and 
%$\stdsem{\exists \vW{0} (\forall \vW{1} (\edist(\vW{0},\vW{1}) < \epsilon \limply 
% \exists \Y{} \tostdsem{\VarSSub{\phi}{\vY{},\Y{},\vW{1}}})\land \edist(\vW{0},\vW{}) < \epsilon)}$ 
% are the same.
%
%\item  $\NotBoundIn{\varphi}{\vY{},\vW{}}$ has the form $\neg \NotBoundIn{\phi}{\vY{},\vW{}}$.\\
%By the definition, $\sphsem{ \neg \NotBoundIn{\phi}{\vY{},\vW{}} }\defeq \bigcup_{\eball{\{p\}}\cap \sphsem{ \NotBoundIn{\phi}{\vY{},\vW{}} }=\emptyset}\eball{\{p\}}$. By using  the same argument used in %the proof of 
%the $\land$-case, 
%%we can conclude that the two sets
%the sets  
%$\stdsem{\exists \vW{0} (\forall \vW{1} (\edist(\vW{0},\vW{1}) < \epsilon \limply 
%\neg \tostdsem{\VarSSub{\phi}{\vY{},\vW{1}}})\land \edist(\vW{0},\vW{}) < \epsilon)}$ 
%and $\sphsem{  \neg \NotBoundIn{\phi}{\vY{},\vW{}} }$ 
%are the same.
%%\end{enumerate}
%\end{description}
%\end{proof}

%\begin{corollary}
%	Let $\NotBoundIn{\varphi}{\vY,\vW{}}$ be any first order formula definable in Tarski algebra, and $\epsilon \in  \mathbb{R}_{> 0}$.
%	Satisfiability of $\NotBoundIn{\tostdsem{\varphi}}{\vY,\vW{}}$ is decidable.
%\end{corollary}
%%\begin{proof}
%%	Since $\NotBoundIn{\tostdsem{\varphi}}{\vY,\vW{}}$ is a formula definable in Tarski algebra, and
%%	since it is well known that Tarski algebra is decidable, it immediately follows that 
%%	satisfiability of $\NotBoundIn{\tostdsem{\varphi}}{\vY,\vW{}}$ is decidable.
%%\end{proof}

\noindent Since $\NotBoundIn{\tostdsem{\varphi}}{\vY,\vW{}}$ is %a formula 
definable in Tarski theory, and
	this theory is decidable, the satiability of $\varphi$ in $\sphsem{}$ is decidable.

%\begin{example}
%	%Let $\epsilon = 1$ be a constant and $\edist$ be the standard Euclidean distance.
%	Let us consider the formula $\NotBoundIn{\varphi}{\X{}} \deq \X{} > 0 \wedge \X{} < 2$.
%	We have that $\tostdsem{\X{} > 0} \equiv \exists \X{0} ( \X{0} > 0 \wedge \edist(\X{0} ,\X{}) < \epsilon ) \equiv \X{0} + \epsilon > 0$.
%	By applying the same rule, $\tostdsem{\X{} < 2} \equiv \exists \X{0} ( \X{0} < 2 \wedge \edist(\X{0},\X{}) < \epsilon ) \equiv \X{} - 2-\epsilon < 0$.
%	Finally, since $\epsilon$ is a positive real, $\tostdsem{\X{} > 0 \land \\X{} < 2}
%	\equiv \exists \X{0}( \forall \X{1} (  \edist(\X{0},\X{1}) < \epsilon \limply \X{1} + \epsilon > 0 \land \X{1} - 2-\epsilon < 0) \land \edist(\X{0} ,\X{}) < \epsilon )
%	\equiv \X{}>-\epsilon \land \X{}\leq 2+\epsilon$.
%\end{example}

Let us notice that the application of the translation in Definition~\ref{def:tostdsem} to a formula, increases 
the evaluation complexity of such formula with respect to its untranslated version. This is mainly due to
the possible introduction of quantifier operator alternations.

\subsection{Experimental Results on the Neural Oscillator}

Let us consider the hybrid automaton $H_{\tilde{f}}$ described in Section \ref{sec:model} for modeling a neural oscillator. 
We intend to study its behaviour through sphere semantics, exploiting cylindrical algebraic decomposition tools to 
automatically compute it.

As we noticed in Section~\ref{sec:approx},  
%\ref{sec:epsilon}
any differentiable dynamics can be exactly represented, in terms of an opportune $\epsilon$-semantics, by a semi-algebraic function. 
%if their evolutions are evaluated by an opportune $\epsilon$-semantics. 
In particular, we can replace the dynamics of $H_{\tilde{f}}$ by the corresponding 
Taylor polynomials up to a certain degree which depends on $\epsilon$.
%both $\epsilon$ and the time horizon fixed for the analysis. 
%Since, in this paper, we are focusing on the qualitative behavior of the 
%investigated system, rather than on the exact evolution, 
In this paper, we decided to model the 
automaton dynamics by using their first-degree Taylor polynomials 
and we obtained 
%
%First, we have to replace the differential equations representing the dynamics with semi-algebraic functions. We do this by
%exploiting their first-degree Taylor polynomials and obtaining 
the automaton $H'_{\tilde{f}}$ depicted in Figure~\ref{fig:taylorapproxfunct}.
In order to keep the presentation simple, in this section we fix the parameters as follows 
$\tau=3$, $\lambda=1$, $\alpha=2$. Hence, the activations correspond to the axis $\X{i}=\pm 2$ and $\X{e}=\pm 2$.  

\begin{figure}[!h]
\begin{center}
\includegraphics[width=0.67\textwidth]{automaton3.pdf}
\caption{The piecewise hybrid automaton $H'_{\tilde{f}}$ associated to the function $f_{2}(3,1)$.}\label{fig:taylorapproxfunct}
\end{center}
\end{figure}

A simulation of $H'_{\tilde{f}}$ is presented in Figure \ref{fig:diamond_cycle}: %, where we can notice that 
a limit cycle is still present, 
but it has a diamond-like shape. We are interested in studying this limit cycle. In particular, we are interested in proving, exploiting tools for symbolic computation, that if we apply sphere semantics, each point in the space reaches a bounded region 
which includes the limit cycle. %Notice that 
In this example our automata have unbounded invariants, hence the termination of 
sphere semantics reachability algorithm is not guaranteed.

We start computing the intersections of the limit cycle with the activation regions. 
Consider for instance the intersection $Q_0=\tuple{x_{Q_0},2}$ of the limit cycle with $\X{i}=2$ and 
$\X{e}>0$.
We have that $x_{Q_0}$ is the unique solution of the equation which describes the intersection of the
diamond-like limit cycle with $\X{i}=2$. Similarly, consider point $Q_1=\tuple{2,y_{Q_1}}$
that in turn corresponds to the intersection of the limit cycle with $\X{e}=2$ and $\X{i}>0$. 
We effectively calculated all these intersections by using the computer algebra system
 {\tt Maxima}. %~\cite{maxima}. 
So, for instance, we get $x_{Q_0}=\frac{3526\,\sqrt{17}+14538}{495\,\sqrt{17}+2041}$ and 
$y_{Q_1}=\frac{190\,\sqrt{17}+786}{39\,\sqrt{17}+161}$.
The points 
$Q_0$ and $Q_1$ satisfy the activation formul\ae~wich regulate 
the discrete transitions between locations $\hloc{6}$ and $\hloc{5}$, and locations $\hloc{6}$ and $\hloc{7}$, 
respectively. Let us now consider a point $P_0$ located on $\X{i}=2$, but which is such
that its distance $d_0$ from $Q_0$ is at least $2\epsilon$, i.e., $P_0=\tuple{x_{P_0},2}$ and
$\edist(Q_0,P_0) = d_0 > 2\epsilon$. Consider now any point $P_1$ on $\X{e}=2$ resulting 
from the sphere semantics evaluation of the continuous evolution which starts in $P_0$
inside location $\hloc{6}$. Thus, let denote with $d_1$ the distance between such $P_1$ and $Q_1$.
%, i.e., $\edist(Q_1,P_1) = d_1$.

If we could prove that $d_1$ is always smaller than $d_0$, then we would be able to conclude that all the points 
which start from a distance of at least $2\epsilon$ from the limit cycle converge to a flow tube  
having diameter $2\epsilon$ that includes the limit cycle. Of course, to obtain such conclusion, we need to prove 
this property on all locations. 

We can formalize this concept through a first-order formula. We denote with $r$ and $s$ the straight lines $\X{i}=2$ 
and $\X{e}=2$, respectively, and with the notation $Q_0 \in r \cap C \cap \X{e}>0$ the membership of $Q_0$ to the 
intersection of straight line $r$ with limit cycle $C$ and positive $\X{e}$ semi-plane. Moreover, with the notation
$\sphsem{ P_0 \rightarrow_C P_1 }$ we denote the continuous transition from point $P_0$ to point 
$P_1$ performed exploiting sphere semantics. Thus, our desired property can be expressed as:
\begin{equation}\label{eq:epsilon_conv}
\begin{split}
\forall Q_0 Q_1 \forall P_0 P_1 \big( ( & Q_0 \in r \cap C \cap \X{e}>0 \wedge Q_1 \in s \cap C \cap \X{i}>0 \wedge P_0 \in r \cap \X{e}>0 \wedge  \\
		&P_1 \in s \cap \X{e}>0 \wedge \edist(Q_0,P_0) > 2\epsilon \wedge \sphsem{ P_0 \rightarrow_C P_1 }) \limply \edist(Q_1,P_1) < \edist(Q_0,P_0) \big)
\end{split}
\end{equation}
stating the convergence to the limit flow tube in location $\hloc{6}$. Such property can be 
easily rewritten for each location of the hybrid automaton, changing the roles of activation border lines 
$r$ and $s$.

\begin{figure}[!ht]
 \centering
   \includegraphics[width=0.50\textwidth]{newton_evolution.pdf}
    \caption{Two evolutions of the first degree approximation of the model proposed in Section~\ref{sec:model}.}\label{fig:newtonev}
 \end{figure}
 
We automatically expanded such formula by using a Perl script that implements the Definition~\ref{def:tostdsem} to translate sphere semantics into the standard one. 
In particular, $\sphsem{ P_0 \rightarrow_C P_1 }$, in the case of location $\hloc{6}$ becomes 
\begin{equation}\label{eq:full_formula}
%\begin{split}
\NotBoundIn{\psi}{\vX{}} \defeq \exists \Tvar{} (\exists \vX{0} ( 
\forall \vX{1} (  \edist{(\vX{0},\vX{1})}< \epsilon \limply (\Tvar{}>0 \land 
\VarSSub{\phi}{\vX{1},\Tvar{}}))) \land  \edist{(\vX{0},\vX{})}< \epsilon), 
%\end{split}
\end{equation}
where 
\begin{equation}
\begin{split}
\NotBoundIn{\phi}{\vX{},\Tvar{}} \defeq \exists \vX{0} (\forall \vX{1} ( \edist{(\vX{0},\vX{1})}< \epsilon &\limply 
( \exists \vX{2} (\VarSSub{\Pi_1}{\vX{2},\Tvar{}} \land \edist{(\vX{2},\vX{1})}< \epsilon ) \land  \\
&\exists \vX{2} (\VarSSub{\Pi_2}{\vX{2},\Tvar{}} \land \edist{(\vX{2},\vX{1})}<\epsilon))) \land \edist{(\vX{0},\vX{})}<\epsilon) ,
\end{split}
\end{equation} 
%\begin{align}
$\NotBoundIn{\Pi_1}{\X{0},\Y{0},\X{1},\Y{1},\Tvar{}} \defeq 6*\X{1}=6*\X{0}+(\X{0}-3*\Y{0})*\Tvar{}$, and 
$\NotBoundIn{\Pi_2}{\X{0},\Y{0},\X{1},\Y{1},\Tvar{}} \defeq 6*\Y{1}=6*\Y{0}+(\Y{0}+3*\X{0})*\Tvar{}$.
%\end{align}
%
However, we notice that, since $\Pi_1$ and $\Pi_2$ are closed and convex, $\phi$ can be simplified as: 
\begin{equation}
\NotBoundIn{\phi}{\vX{},\Tvar{}} \equiv \exists \vX{0} (\VarSSub{\Pi_1}{\vX{0},\Tvar{}} \land \VarSSub{\Pi_2}{\vX{0},\Tvar{}} \land \edist{(\vX{0},\vX{})}<\epsilon).
\end{equation}
 Similarly, $\psi$ becomes:
 \begin{equation}
\NotBoundIn{\psi}{\vX{}} \equiv \exists \Tvar{} (\Tvar{}>0 \land \exists \vX{0} (\VarSSub{\Pi_1}{\vX{0},\Tvar{}}
 \land \VarSSub{\Pi_2}{\vX{0},\Tvar{}} \land \edist{(\vX{0},\vX{})}<\epsilon)).
\end{equation}
So we plugged this last formula in Formula~\ref{eq:epsilon_conv} and used {\tt REDLOG}~\cite{Dolzmann:1997:RCA:261320.261324} to test it. 
The formula turns out to be true (the result is computed within few seconds), proving our conjectures. 

Notice that we used {\tt Maxima} to compute the exact coordinates of the points on the limit cycles since that computation 
does not require quantifier elimination. However, we could have used {\tt REDLOG}. 

As far as $\tuple{0,0}$ is concerned it is immediate to prove through a first-order formula that it reaches points different from 
itself and, hence, it reaches the limit flow tube. 

Other interesting properties that automatically verified express, for instance, the fact that applying the sphere semantics there are points that cross 
the limit cycle (in both directions). This is quite natural since points closer than $\epsilon$ to the limit cycle get expanded and cross it. 



main.bbl
\begin{thebibliography}{10}
\providecommand{\bibitemdeclare}[2]{}
\providecommand{\surnamestart}{}
\providecommand{\surnameend}{}
\providecommand{\urlprefix}{Available at }
\providecommand{\url}[1]{\texttt{#1}}
\providecommand{\href}[2]{\texttt{#2}}
\providecommand{\urlalt}[2]{\href{#1}{#2}}
\providecommand{\doi}[1]{doi:\urlalt{http://dx.doi.org/#1}{#1}}
\providecommand{\bibinfo}[2]{#2}

\bibitemdeclare{article}{alur95}
\bibitem{alur95}
\bibinfo{author}{R.~\surnamestart Alur\surnameend},
  \bibinfo{author}{C.~\surnamestart Courcoubetis\surnameend},
  \bibinfo{author}{N.~\surnamestart Halbwachs\surnameend},
  \bibinfo{author}{T.~A. \surnamestart Henzinger\surnameend},
  \bibinfo{author}{P.-H. \surnamestart Ho\surnameend},
  \bibinfo{author}{X.~\surnamestart Nicollin\surnameend},
  \bibinfo{author}{A.~\surnamestart Olivero\surnameend},
  \bibinfo{author}{J.~\surnamestart Sifakis\surnameend} \&
  \bibinfo{author}{S.~\surnamestart Yovine\surnameend} (\bibinfo{year}{1995}):
  \emph{\bibinfo{title}{The Algorithmic Analysis of Hybrid Systems}}.
\newblock {\sl \bibinfo{journal}{Theoret. Comput. Sci.}}
  \bibinfo{volume}{138}(\bibinfo{number}{1}), pp. \bibinfo{pages}{3--34},
  \doi{10.1016/0304-3975(94)00202-T}.

\bibitemdeclare{article}{DBLP:journals/ijns/AtiyaB89}
\bibitem{DBLP:journals/ijns/AtiyaB89}
\bibinfo{author}{A.~F. \surnamestart Atiya\surnameend} \&
  \bibinfo{author}{P.~\surnamestart Baldi\surnameend} (\bibinfo{year}{1989}):
  \emph{\bibinfo{title}{Oscillations and Synchronizations in Neural Networks:
  an Exploration of the Labeling Hypothesis}}.
\newblock {\sl \bibinfo{journal}{Int. J. Neural Syst.}}
  \bibinfo{volume}{1}(\bibinfo{number}{2}), pp. \bibinfo{pages}{103--124},
  \doi{10.1142/S0129065789000025}.

\bibitemdeclare{article}{DBLP:journals/deds/CasagrandePP09}
\bibitem{DBLP:journals/deds/CasagrandePP09}
\bibinfo{author}{A.~\surnamestart Casagrande\surnameend},
  \bibinfo{author}{C.~\surnamestart Piazza\surnameend} \&
  \bibinfo{author}{A.~\surnamestart Policriti\surnameend}
  (\bibinfo{year}{2009}): \emph{\bibinfo{title}{Discrete Semantics for Hybrid
  Automata}}.
\newblock {\sl \bibinfo{journal}{Discrete Event Dyn. Syst.}}
  \bibinfo{volume}{19}(\bibinfo{number}{4}), pp. \bibinfo{pages}{471--493},
  \doi{10.1007/s10626-009-0082-7}.

\bibitemdeclare{article}{focore2008}
\bibitem{focore2008}
\bibinfo{author}{A.~\surnamestart Casagrande\surnameend},
  \bibinfo{author}{C.~\surnamestart Piazza\surnameend},
  \bibinfo{author}{A.~\surnamestart Policriti\surnameend} \&
  \bibinfo{author}{B.~\surnamestart Mishra\surnameend} (\bibinfo{year}{2008}):
  \emph{\bibinfo{title}{Inclusion dynamics hybrid automata}}.
\newblock {\sl \bibinfo{journal}{Inform. and Comput.}}
  \bibinfo{volume}{206}(\bibinfo{number}{12}), pp. \bibinfo{pages}{1394--1424},
  \doi{10.1016/j.ic.2008.09.001}.

\bibitemdeclare{article}{Dolzmann:1997:RCA:261320.261324}
\bibitem{Dolzmann:1997:RCA:261320.261324}
\bibinfo{author}{A.~\surnamestart Dolzmann\surnameend} \&
  \bibinfo{author}{T.~\surnamestart Sturm\surnameend} (\bibinfo{year}{1997}):
  \emph{\bibinfo{title}{REDLOG: computer algebra meets computer logic}}.
\newblock {\sl \bibinfo{journal}{SIGSAM Bull.}}
  \bibinfo{volume}{31}(\bibinfo{number}{2}), pp. \bibinfo{pages}{2--9},
  \doi{10.1145/261320.261324}.

\bibitemdeclare{book}{ender}
\bibitem{ender}
\bibinfo{author}{H.~B. \surnamestart Enderton\surnameend}
  (\bibinfo{year}{2001}): \emph{\bibinfo{title}{{A Mathematical Introduction to
  Logic}}}, \bibinfo{edition}{{II}} edition.
\newblock \bibinfo{publisher}{Harcourt/Academic Press}.

\bibitemdeclare{inproceedings}{franzle99}
\bibitem{franzle99}
\bibinfo{author}{M.~\surnamestart Fr{\"{a}}nzle\surnameend}
  (\bibinfo{year}{1999}): \emph{\bibinfo{title}{Analysis of Hybrid Systems: An
  Ounce of Realism Can Save an Infinity of States}}.
\newblock In: {\sl \bibinfo{booktitle}{Int. Workshop on Computer, Science, and
  Logic (CSL 99)}}, {\sl \bibinfo{series}{LNCS}} \bibinfo{volume}{1683},
  \bibinfo{publisher}{Springer}, pp. \bibinfo{pages}{126--140}.

\bibitemdeclare{article}{citeulike:762104}
\bibitem{citeulike:762104}
\bibinfo{author}{W.~J. \surnamestart Freeman\surnameend} \&
  \bibinfo{author}{C.~A. \surnamestart Skarda\surnameend}
  (\bibinfo{year}{1985}): \emph{\bibinfo{title}{{Spatial EEG patterns,
  non-linear dynamics and perception: the neo-Sherringtonian view.}}}
\newblock {\sl \bibinfo{journal}{Brain Res}}
  \bibinfo{volume}{357}(\bibinfo{number}{3}), pp. \bibinfo{pages}{147--175}.

\bibitemdeclare{inproceedings}{tomlinmodel}
\bibitem{tomlinmodel}
\bibinfo{author}{R.~\surnamestart Ghosh\surnameend} \&
  \bibinfo{author}{C.~\surnamestart Tomlin\surnameend} (\bibinfo{year}{2001}):
  \emph{\bibinfo{title}{{L}ateral {I}nhibition through {D}elta-{N}otch
  signaling: {A} {P}iecewise {A}ffine {H}ybrid {M}odel}}.
\newblock In: {\sl \bibinfo{booktitle}{Proc. of Hybrid Systems: Computation and
  Control (HSCC'01)}}, {\sl \bibinfo{series}{LNCS}} \bibinfo{volume}{2034},
  \bibinfo{publisher}{Springer}, pp. \bibinfo{pages}{232--246},
  \doi{10.1007/3-540-45351-2\_21}.

\bibitemdeclare{article}{Girard:2007fk}
\bibitem{Girard:2007fk}
\bibinfo{author}{A.~\surnamestart Girard\surnameend} \& \bibinfo{author}{G.~J.
  \surnamestart Pappas\surnameend} (\bibinfo{year}{2007}):
  \emph{\bibinfo{title}{Approximation metrics for discrete and continuous
  systems}}.
\newblock {\sl \bibinfo{journal}{IEEE Trans. Automat. Control}}
  \bibinfo{volume}{52}(\bibinfo{number}{5}), pp. \bibinfo{pages}{782--798},
  \doi{10.1109/TAC.2007.895849}.

\bibitemdeclare{article}{citeulike:547881}
\bibitem{citeulike:547881}
\bibinfo{author}{C.~M. \surnamestart Gray\surnameend},
  \bibinfo{author}{P.~\surnamestart Konig\surnameend}, \bibinfo{author}{A.~K.
  \surnamestart Engel\surnameend} \& \bibinfo{author}{W.~\surnamestart
  Singer\surnameend} (\bibinfo{year}{1989}): \emph{\bibinfo{title}{{Oscillatory
  responses in cat visual cortex exhibit inter-columnar synchronization which
  reflects global stimulus properties}}}.
\newblock {\sl \bibinfo{journal}{Nature}}
  \bibinfo{volume}{338}(\bibinfo{number}{6213}), pp. \bibinfo{pages}{334--337},
  \doi{10.1038/338334a0}.

\bibitemdeclare{incollection}{Grosu:2011fk}
\bibitem{Grosu:2011fk}
\bibinfo{author}{R.~\surnamestart Grosu\surnameend},
  \bibinfo{author}{G.~\surnamestart Batt\surnameend},
  \bibinfo{author}{F.~\surnamestart Fenton\surnameend},
  \bibinfo{author}{J.~\surnamestart Glimm\surnameend},
  \bibinfo{author}{C.~\surnamestart Guernic\surnameend},
  \bibinfo{author}{S.~\surnamestart Smolka\surnameend} \&
  \bibinfo{author}{E.~\surnamestart Bartocci\surnameend}
  (\bibinfo{year}{2011}): \emph{\bibinfo{title}{From Cardiac Cells to Genetic
  Regulatory Networks}}.
\newblock In: {\sl \bibinfo{booktitle}{Proc. of Computer Aided Verification
  (CAV'11)}}, {\sl \bibinfo{series}{LNCS}} \bibinfo{volume}{6806},
  \bibinfo{publisher}{Springer}, pp. \bibinfo{pages}{396--411},
  \doi{10.1007/978-3-642-22110-1\_31}.

\bibitemdeclare{inproceedings}{undecidable}
\bibitem{undecidable}
\bibinfo{author}{T.~A. \surnamestart Henzinger\surnameend},
  \bibinfo{author}{P.~W. \surnamestart Kopke\surnameend},
  \bibinfo{author}{A.~\surnamestart Puri\surnameend} \&
  \bibinfo{author}{P.~\surnamestart Varaiya\surnameend} (\bibinfo{year}{1995}):
  \emph{\bibinfo{title}{What's decidable about hybrid automata?}}
\newblock In: {\sl \bibinfo{booktitle}{Proc. of ACM Symposium on Theory of
  Computing (STOCS'95)}}, pp. \bibinfo{pages}{373--382},
  \doi{10.1145/225058.225162}.

\bibitemdeclare{article}{springerlink:10.1016/j.bulm.2003.08.010}
\bibitem{springerlink:10.1016/j.bulm.2003.08.010}
\bibinfo{author}{H.~\surnamestart de~Jong\surnameend}, \bibinfo{author}{J.-L.
  \surnamestart Gouz{\'e}\surnameend}, \bibinfo{author}{C.~\surnamestart
  Hernandez\surnameend}, \bibinfo{author}{M.~\surnamestart Page\surnameend},
  \bibinfo{author}{T.~\surnamestart Sari\surnameend} \&
  \bibinfo{author}{J.~\surnamestart Geiselmann\surnameend}
  (\bibinfo{year}{2004}): \emph{\bibinfo{title}{Qualitative simulation of
  genetic regulatory networks using piecewise-linear models}}.
\newblock {\sl \bibinfo{journal}{Bulletin of Math. Biology}}
  \bibinfo{volume}{66}, pp. \bibinfo{pages}{301--340},
  \doi{10.1016/j.bulm.2003.08.010}.

\bibitemdeclare{inproceedings}{Prabhakar:2009:VTS:1683310.1684907}
\bibitem{Prabhakar:2009:VTS:1683310.1684907}
\bibinfo{author}{P.~\surnamestart Prabhakar\surnameend},
  \bibinfo{author}{V.~\surnamestart Vladimerou\surnameend},
  \bibinfo{author}{M.~\surnamestart Viswanathan\surnameend} \&
  \bibinfo{author}{G.~E. \surnamestart Dullerud\surnameend}
  (\bibinfo{year}{2009}): \emph{\bibinfo{title}{Verifying Tolerant Systems
  Using Polynomial Approximations}}.
\newblock In: {\sl \bibinfo{booktitle}{Proceedings of the 2009 30th IEEE
  Real-Time Systems Symposium}}, \bibinfo{series}{RTSS '09},
  \bibinfo{publisher}{IEEE Computer Society}, \bibinfo{address}{Washington, DC,
  USA}, pp. \bibinfo{pages}{181--190}, \doi{10.1109/RTSS.2009.28}.

\bibitemdeclare{inproceedings}{DBLP:conf/tamc/Ratschan10}
\bibitem{DBLP:conf/tamc/Ratschan10}
\bibinfo{author}{S.~\surnamestart Ratschan\surnameend} (\bibinfo{year}{2010}):
  \emph{\bibinfo{title}{Safety Verification of Non-linear Hybrid Systems Is
  Quasi-Semidecidable}}.
\newblock In: {\sl \bibinfo{booktitle}{Theory and Applications of Models of
  Computation (TAMC10)}}, {\sl \bibinfo{series}{lncs}} \bibinfo{volume}{6108},
  \bibinfo{publisher}{springer}, pp. \bibinfo{pages}{397--408},
  \doi{10.1007/978-3-642-13562-0\_36}.

\bibitemdeclare{article}{1824881}
\bibitem{1824881}
\bibinfo{author}{L.~R. \surnamestart Silva\surnameend},
  \bibinfo{author}{Y.~\surnamestart Amitai\surnameend} \&
  \bibinfo{author}{B.~W. \surnamestart Connors\surnameend}
  (\bibinfo{year}{1991}): \emph{\bibinfo{title}{Intrinsic oscillations of
  neocortex generated by layer 5 pyramidal neurons.}}
\newblock {\sl \bibinfo{journal}{Science}}
  \bibinfo{volume}{251}(\bibinfo{number}{4992}), pp. \bibinfo{pages}{432--5},
  \doi{10.1126/science.1824881}.

\bibitemdeclare{article}{citeulike:4043128}
\bibitem{citeulike:4043128}
\bibinfo{author}{M.~\surnamestart Steriade\surnameend} \&
  \bibinfo{author}{R.~R. \surnamestart Llin\'{a}s\surnameend}
  (\bibinfo{year}{1988}): \emph{\bibinfo{title}{{The functional states of the
  thalamus and the associated neuronal interplay.}}}
\newblock {\sl \bibinfo{journal}{Physiological reviews}}
  \bibinfo{volume}{68}(\bibinfo{number}{3}), pp. \bibinfo{pages}{649--742}.

\bibitemdeclare{article}{Tonnelier19991213}
\bibitem{Tonnelier19991213}
\bibinfo{author}{A.~\surnamestart Tonnelier\surnameend},
  \bibinfo{author}{S.~\surnamestart Meignen\surnameend},
  \bibinfo{author}{H.~\surnamestart Bosch\surnameend} \&
  \bibinfo{author}{J.~\surnamestart Demongeot\surnameend}
  (\bibinfo{year}{1999}): \emph{\bibinfo{title}{Synchronization and
  desynchronization of neural oscillators}}.
\newblock {\sl \bibinfo{journal}{Neural Networks}}
  \bibinfo{volume}{12}(\bibinfo{number}{9}), pp. \bibinfo{pages}{1213 -- 1228},
  \doi{10.1016/S0893-6080(99)00068-4}.

\end{thebibliography}
