

\section{Introduction}
\label{sec:intro}

In the last decade there has been increasing interest in capturing
stochastic behaviour in models of computational systems.  The
motivations for this work range from being able to capture probabilistic
algorithms, which gain efficiency through non-determinism, to
abstraction over an uncertain environment, where a complex variety of
possible responses may be represented as a probability distribution
rather than a single response.  In this paper we introduce
stochastic behaviour to HYPE, a formalism previously proposed to model
hybrid systems \cite{HYPE-journal}.  Our motivation is to capture uncertain
response events in a quantified manner.

Hybrid systems mix discrete control and continuous evolution, and can
arise in a number of natural and engineering contexts.  A number of
process algebras for modelling hybrid systems have emerged in recent
years including $\smash{\mathit{ACP}_{hs}^{srt}}$ \cite{BergBM:05a},
hybrid $\smash{\Chi}$ \cite{BeekBMRRS:06a}, $\phi$-calculus
\cite{RounRS:03a}
and HyPA \cite{CuijCR:05a}. 
\cite{KhadK:08a} shows
in her thesis that there are
substantial differences in the approaches taken by these process
algebras relating to syntax, semantics, discontinuous behaviour,
flow-determinism, theoretical results and availability of tools.
Nevertheless there are also strong similarities in their approaches to
capturing the continuous evolution of the system: the dynamic behaviour
of each continuous variable must be fully described by ordinary
differential equations (ODEs) given explicitly in the syntax of the
process algebra.  Furthermore, they all adopt a notion of state which
incorporates an evaluation of continuous variables.  

HYPE adopts a different approach which supports a finer-grained view on
the dynamics of the system.  As it is a process algebra, models are
constructed compositionally, but here each subcomponent is itself
constructed from a number of \emph{flows} or influences, represented
abstractly.  Ultimately each flow will correspond to a term in the ODEs
governing the evolution of a continuous variable, but at the process
algebra level the details of the mathematical form of this influence are
left unspecified.  This separation of concerns allows us to consider the
logical structure of the model (the process algebra description) as
distinct from any particular dynamic realisation.    We believe that the
use of flows as the basic elements of model construction has advantages
such as ease and simplification of modelling. This approach assists the
modeller, allowing them to identify smaller or local descriptions of the
model and then to combine these descriptions to obtain the larger
system.

Discrete changes within a system are captured as \emph{events}.
Each event may change the dynamic nature of a flow, possibly also
resetting the current value of continuous variables.  Each event
has a triggering condition which may be dependent on the current
value of the continuous variables.  In HYPE as presented by
\cite{HYPE-journal}, events are either \emph{urgent} or \emph{non-urgent}.
Urgent events are forced to occur as soon as their trigger becomes
true, and if multiple urgent events become true simultaneously, one
of them occurs, and the remaining events may or may not occur after
this event depending on whether their trigger condition remains
true.  In contrast, non-urgent actions may delay indefinitely.

HYPE can be viewed as belonging to the class of quantified process
algebras, including probabilistic, stochastic and timed process algebras
which support reasoning over models to quantitatively analyse the
behaviour of a system, for example considering the relative likelihood
of particular sub-behaviours, or the expected time until a condition is
met.  However, the inclusion of non-urgent events within the model left
some unspecified behaviour that could not be quantified and therefore
limited the extent to which quantified analysis could be applied.  
Thus in this paper we define an extension of HYPE, stochastic HYPE, in
which the non-urgent events of HYPE are replaced by stochastic events.
Such events remain non-urgent, as in not occurring immediately, but now
their delay is governed by an exponential distribution. 
Additionally through the use of random variables in resets, other
forms of stochasticity can be included in models, and timers can
be used to achieve random delays from an arbitrary distribution.  So the
non-urgent events of HYPE are effectively replaced in stochastic
HYPE by random events based on any distribution. The underlying
mathematical model used by stochastic HYPE is Transition Driven
Stochastic Hybrid Automata (TDSHA)
\cite{PA:Bortolussi:2010:HybridDynamicsStochProg:TCS}, based on
piecewise deterministic Markov process (PDMP) \cite{Davis93}.
We work with TDSHA because they are a better than operational match with
stochastic HYPE than PDMPs.

The contributions of this paper include a compositional language
to describe the dynamics of systems with stochastic, instantaneous
and continuous behaviour, in a modular fashion to ensure models are
straightforward to modify. This requires mapping to a mathematical
model of these three behaviour types to TDSHA, related to PDMP.
Furthermore, a new bisimulation is defined to enable formal reasoning
about differences and similarities in model behaviour. These
contributions are illustrated through a non-trivial example of an
assembly line.

The remainder of this paper is structured as follows.  In Section 2 we
illustrate the stochastic HYPE modelling language,
through the description of a simple network example, and the formal
syntax of stochastic HYPE.  The operational
semantics is defined in terms of \emph{configurations}
which capture the influences at play within the system rather than
explicit values of continuous variables, is presented in Section 3.
The
dynamic interpretation of stochastic HYPE models is given in terms of a
class of hybrid automata called Transition-Driven Stochastic Hybrid
Automata (TDSHA) \cite{PA:Bortolussi:2010:HybridDynamicsStochProg:TCS}
which can themselves be mapped to PDMPs
\cite{Davis93}.  The TDSHA formalism is presented in Section 4 and the
mapping from stochastic HYPE to TDSHA is defined in Section 5.  This
section also considers the impact of stochastic events on the notion
of well-behavedness.  A HYPE model is well-behaved if it cannot
execute an infinite number of simultaneous instantaneous events.
Introducing stochastic events to a model
that was previously not well-behaved, can lead to well-behavedness. Section 6 introduces
the main example of the paper and illustrates the expressiveness of
stochastic HYPE through an optimisation problem.
Semantic equivalences play an important
role in reasoning about process algebra models, and a major contribution
of this paper is a suitable bisimulation for stochastic HYPE models.
In Section 7, we show why existing bisimulations are not sufficient and
present a bisimulation
for stochastic HYPE that captures the notions that two models share the
same behaviours for all three behaviour types.
In Section 8, the use 
of this bisimulation and associated results are demonstrated on the
example from Section 6.
Then Section 9 presents related work and we conclude in Section 10.
Online appendices contain proofs and supplementary material.

Preliminary work on stochastic HYPE has been published by
\cite{BortBGH:11a}; here we define a more elegant mapping to TDSHA, add
random resets
and present new results on bisimulation equivalences.

\section{Stochastic HYPE Definition}
\label{sec:HYPE}

\begin{figure}[!t]
{\renewcommand{\arraystretch}{1.00}
$$\begin{array}{rcl}
\mathit{Input} & \rmdef & 
 \sev{on}_{in}{\,:\,}(in,r_{in},\mathit{const}).\mathit{Input} +
 \sev{off}_{in}{\,:\,}(in,0,\mathit{const}).\mathit{Input} +\\
 & & \ev{full}{\,:\,}(in,0,\mathit{const}).\mathit{Input} +
 \ev{init}{\,:\,}(in,0,\mathit{const}).\mathit{Input}               \\
\mathit{Output} & \rmdef &   
 \sev{on}_{out}{\,:\,}(out,-r_{out},\mathit{const}).\mathit{Output} +
 \sev{off}_{out}{\,:\,}(out,0,\mathit{const}).\mathit{Output} +\\
 & &  \ev{empty}{\,:\,}(out,0,\mathit{const}).\mathit{Output} +
 \ev{init}{\,:\,}(out,0,\mathit{const}).\mathit{Output} \\
\mathit{Drop} & \rmdef & \ev{init}{\,:\,}(f,0,\mathit{const}).\mathit{Drop} +
                    \ev{fail}{\,:\,}(f,0,\mathit{const}).\mathit{Drop} \\
\mathit{Timer} & \rmdef & \ev{init}{\,:\,}(t,1,\mathit{const}).\mathit{Timer} \\
\\
\mathit{Con}_{in} & \rmdef & \sev{on}_{in}.\mathit{Con}_{in}' \qquad \mathit{Con}_{in}' \:\rmdef\:
\sev{off}_{in}.\mathit{Con}_{in} + \ev{full}.\mathit{Con}_{in}\\
\mathit{Con}_{out} & \rmdef & \sev{on}_{out}.\mathit{Con}_{out}' \quad\, \mathit{Con}_{out}' \:\rmdef\:
\sev{off}_{out}.\mathit{Con}_{out} + \ev{empty}.\mathit{Con}_{out}\\
\mathit{Con}_\mathit{fail} & \rmdef & \ev{fail}.\mathit{Con}_\mathit{fail} \\
& & \\
\mathit{Buffer} & \rmdef & (\mathit{Input} \syncstar \mathit{Output} \syncstar \mathit{Drop}
\syncstar \mathit{Timer}) \syncstar \ev{init}.(\mathit{Con}_{in} \parallel
\mathit{Con}_{out}
\parallel \mathit{Con}_\mathit{fail}) \\
\end{array}$$

{\renewcommand{\arraystretch}{1.2}
$$\begin{array}{rclrcl}
\mathcal{V} & = & 
\multicolumn{4}{c}{\{B,T,C,D\} \quad
\mathop{\mathit{iv}}(in) \: = \: B \quad \mathop{\mathit{iv}}(out) \: = \: B \quad
\mathop{\mathit{iv}}(f) \: = \: B \quad \mathop{\mathit{iv}}(t) \: = \: T} \\
\\
\mathit{ec}(\ev{init}) & = & \multicolumn{4}{l}{(true,\;\rsdefa{B}{b_0} \:\wedge\:
\rsdefa{T}{0} \:\wedge\: \rsdefa{C}{0}
\:\wedge\: \rsdefa{D}{\mathrm{ln\ }\mathcal{N}(\Delta,\xi)})} \\
\mathit{ec}(\ev{fail}) & = & \multicolumn{4}{l}{(T=C\!+\!D,
\;\rsdefa{C}{T} \:\wedge\: \rsdefa{D}{\mathrm{ln\ }\mathcal{N}(\Delta,\xi)})
\:\wedge\: \rsdefa{B}{B\!-\!\mathcal{U}(0,B)})}\\
\mathit{ec}(\ev{full}) & = & (B = max_B,true) \qquad \qquad & 
\mathit{ec}(\ev{empty}) & = & (B = 0,true) \\
\mathit{ec}(\sev{on}_{in}) & = & (k_{in}^{on},\;true) \quad & \mathit{ec}(\sev{off}_{in})
& = & (k_{in}^{\mathit{off}},\;true) \\
\mathit{ec}(\sev{on}_{out}) & = & (k_{out}^{on},\;true) \quad &
\mathit{ec}(\sev{off}_{out}) & = & (k_{out}^{\mathit{off}},\;true) \\
\end{array}$$}
}
\caption{Simple network node model in stochastic HYPE.}\label{simpleNetwork}
\end{figure}

In this section we present the definition  of stochastic HYPE by
means of a small example.  More details about the process algebra
HYPE can be found in an earlier paper \cite{HYPE-journal}.  We
consider a basic model of a network node with a single buffer, which
can either receive packets from an input channel or send packets
to an output channel.  We assume that the number of packets that
travel through the node and that are stored in the buffer is large,
hence we describe them as a fluid quantity.  Received packets are
stored in the buffer, waiting to be sent. We allow reception and
sending of packets to happen concurrently, but enforcing a mutually
exclusive send/receive policy can be easily done as well.  We also
assume that uplinks and downlinks are not always working, but they
are activated and deactivated depending on the availability of a
connection.  These events are described as stochastic, with activation
and deactivation times governed by exponential distributions.
Incoming traffic has to be stopped if the buffer becomes full and
outgoing traffic has to be stopped when the buffer is empty. The
buffer also shows intermittent error behaviour in that after the
passage of a random time period, (drawn from a log normal distribution
with fixed mean and variance), it drops some of its packets (this
quantity is determined uniformly over the number of packets).

HYPE modelling is centred around the notion of \emph{flow}, which
represents some sort of influence continuously modifying one quantity
of the system, described by a variable taking continuous values.
Both the strength and form of a flow can be changed by the happening
of \emph{events}.  In our example, there are two flows modifying
the buffer level, modelled by the continuous variable $B$, namely
reception and sending of packets.  The inflow of packets is modelled
by the $\mathit{Input}$ \emph{subcomponent} shown in Figure~\ref{simpleNetwork}.
Each subcomponent is a summation of prefixes consisting of an
\emph{event} $\ssev{a}$ followed by an \emph{activity} $\alpha$.
\emph{Events} ($\ssev{a} \in \mathcal{E}_d\cup\mathcal{E}_s$) are actions which
trigger discrete changes.  They can be caused by a controller, which
triggers them depending on the global state of the system, specifically
on values of variables (instantaneous events $\ev{a}\in\mathcal{E}_d$), or
happen at exponentially distributed time instants (stochastic events
$\sev{a}\in\mathcal{E}_s$). In the description of the example, non-exponential
durations are mentioned but these are constructed explicitly with
timers. We show later in the paper how we use a syntactic shorthand
for events that have a duration from any distribution.

The $\mathit{Input}$ subcomponent reacts to three
different events: two stochastic ones, activation $\sev{on}_{in}$
and deactivation $\sev{off}_{in}$ of the uplink, and one instantaneous
event, $\ev{full}$, triggered when the buffer level is at its maximum
capacity. The event $\ev{init}$ serves to initialize the system.

\emph{Activities} ($\alpha \in \Ac$) are \emph{influences} on the
evolution of the continuous part of the system and define flows.
An activity is defined as a triple and can be parameterised by a
set of variables, $\alpha(\mathcal{W}) = (\iota,r,I(\mathcal{W}))$.  This triple
consists of an \emph{influence name} $\iota$, a rate of change (or
\emph{influence strength}) $r$ and an \emph{influence type name}
$I(\mathcal{W})$ which describes how that rate is to be applied to the
variables involved, or the actual form of the flow\footnote{For
convenience, we will use $I$ for $I(\mathcal{W})$ when $\mathcal{W}$ can be inferred.}.
In $\mathit{Input}$, there are two distinct activities: $(in,r_{in},\mathit{const})$
and $(in,0,\mathit{const})$.  The first one gives the effect of the incoming
link being active on the buffer level $B$: the influence name is
$in$, which uniquely identifies the effect of the input link on
$B$, $r_{in}$ is the strength of the inflow of packets (here it can
be seen as the amount of received data per time unit), which is
associated with the function $\mathit{const}$.  The second activity captures
the effect of the link being down. It again affects influence $in$,
but has strength $0$ and the form it takes is again $\mathit{const}$.

The interpretation of influence types will be specified separately,
in order to experiment with different functional forms of the packet
inflow without modifying the subcomponent. In this case, we will
obviously interpret $\mathit{const}$ as the constant function 1.  Hence,
in HYPE we separate the description of the logical structure of
flows from their mathematical interpretation.

A second subcomponent affecting buffer level is the output component
$\mathit{Output}$ in Figure~\ref{simpleNetwork}, modelling the sending of
packets, which is defined similarly to $\mathit{Input}$.  The third
subcomponent $\mathit{Drop}$ has no effect on the contents of the
buffer, since its influence strength is always 0, but it does
introduce the event $\smash{\ev{fail}}$ that corresponds to the
dropping of packets. This event will be described below.  Finally,
since the dropping of packets occurs with a frequency, a time
subcomponent and a time variable are required to describe the passing
of time.  It is not affected by any event apart from $\ev{init}$.
These subcomponents can be combined to give the overall uncontrolled
system
\begin{eqnarray*}
\mathit{Input} \syncstar \mathit{Output} \syncstar \mathit{Drop}
\syncstar \mathit{Timer}
\end{eqnarray*}
Here {$\syncstar$} represents parallel cooperation where all shared
events must be synchronised (we use $\!\smsync{L}\!$ to specify that the
events in $L$ are to be synchronised on and ${\parallel}$ when no events are to
be synchronised on).  This cooperation of subcomponents is
called the \emph{uncontrolled system} because it only specifies how
flows react to events, without imposing any causal or temporal
constraints on them.

Causality on events, reflecting natural constraints or design
choices, is specified separately in the controller $\mathit{Con}$. For the
system at hand, the controller is defined as shown in
Figure~\ref{simpleNetwork}.
The subcontroller
$\mathit{Con}_{in}$ models the fact that the reception of packets can be
turned off only after being turned on. Furthermore, it describes
termination of the input if the buffer becomes full, but only if
the uplink is active. $\mathit{Con}_{out}$ is similar.
The $\smash{\ev{fail}}$ event happens without reference to other
events, and is determined by a timer as will be shown below.  However,
a simple controller is added for this event so that the same events
appear both in the controller and the uncontrolled system.

The uncontrolled system and the controller are then combined together
to define the \emph{controlled system} $\mathit{Buffer}$.

\emph{Controllers} have only event prefixes, and we need to specify
when events are activated. This is achieved by assigning to each
event a set of event conditions, which differ between
\emph{stochastic} and \emph{deterministic} events.

Deterministic events $\ev{a}\in \mathcal{E}_d$ happen when certain conditions
are met by the system.  These \emph{event conditions} are specified
by a function $ec$, assigning to each event a \emph{guard} or
\emph{activation condition} (a boolean combination of predicates
depending on system variables, stating when a transition can fire)
and a \emph{reset} (specifying how variables are modified by the
event).  For example, $\mathit{ec}(\ev{full}) = (B = max_B,true)$ states
that the uplink is shut down when the buffer reaches its maximum
capacity $max_B$, and no variable is modified. An event condition
that involves resets is that of the event $\ev{fail}$\footnote{In
the original definition of HYPE, resets were deterministic and were
defined using standard functional notation. This notation must be
modified to allow for random resets and is defined formally later
in this section.}.
\begin{eqnarray*}
\mathit{ec}(\ev{fail}) & = & {(T=C\!+\!D,
\;\rsdefa{C}{T} \:\wedge\: \rsdefa{D}{\mathrm{ln\ }\mathcal{N}(\Delta,\xi)})
\:\wedge\: \rsdefa{B}{B\!-\!\mathcal{U}(0,B)})}
\end{eqnarray*}
The activation condition requires the time variable to be the sum
of $C$ and $D$, and when this is true, $C$ is assigned the value
of the current time, and a new random duration $D$ is drawn from a
log normal distribution with mean $\Delta$ time units and variance $\xi$
thus determining how long until the next failure.  The value of $B$
is also decreased by a random variable drawn from the uniform
distribution for all non-negative values less than or equal to $B$
and this modification of variable $B$ represents the dropping of
packets.

The symbol $\sim$ indicates that there may be random values in the
reset. When no distribution is indicated, such as $\rsdefa{C}{T}$,
this is equivalent to $C'=T$. Multiple resets are combined using
$\wedge$ indicating that all resets must occur.  The notation $V'$
is used to denote the value of $V$ after the reset occurred.
Deterministic events in HYPE are \emph{urgent}, meaning that they
fire as soon as their guard becomes true.

Stochastic events $\sev{a}\in \mathcal{E}_s$ have an event condition composed
of a stochastic rate (replacing the guard of deterministic events)
and a reset the same as above. For instance, $\mathit{ec}(\sev{on}_{in}) =
(k_{in}^{on},true)$ states that the duration of packet reception
is a stochastic event happening at times exponentially distributed
with constant rate $k_{in}^{on}$.  Rates define exponential
distributions and can be functions of the variables of the system.
We choose to restrict delays for stochastic events to those that
are exponential distributed to avoid the issue of residual clocks
when there is no explicit timer associated with the delays. The
event condition for $\ev{fail}$ shows how delays with other distributions
can be modelled with the use of timers, and we generalise this
approach later.

We also need to link each influence with an actual variable. This
is done using the function $\mathop{\mathit{iv}}$. For the example,
$\mathop{\mathit{iv}}(in)\!=\!\mathop{\mathit{iv}}(out)\!=\!\mathop{\mathit{iv}}(f)\!=\!B$, where $B$ is the buffer
level.  The same variable can be modified by many influences. Note
also that in order to model situations in which an event modifies
the flow of more than one variable (in the example, the activation
of a link might modify, for instance, battery consumption), we can
simply define more subcomponents and combine them into structured
components, synchronizing them on shared events.

Finally, we need to interpret influence types, mapping them to
proper functions. In the example, we set $\assign{\mathit{const}} = 1$, so
that $\mathit{const}$ defines a constant flow. However, influence types can
be mapped to linear and non-linear functions as well, as shown in
other HYPE examples \cite{GHB08a,HYPE-journal}.

In the preceding informal discussion, we have introduced the main
constituents of a stochastic HYPE model including the combination
of flow components with a controller component, variables, association
between influences and variables, conditions that specify when
events occur, and definitions for the influence type functions.  To
understand the dynamics of this system, we need to derive ODEs to
describe how the variables change over time, and to further specify
how the discrete and the continuous dynamics interact.  We will do
this by defining an operational semantics, which will specify
qualitatively the behaviour of a controlled system, and then mapping
the so-obtained labelled transition system into a special class of
Stochastic Hybrid Automata.  Before that we give the formal definition
of stochastic HYPE.  In the rest of the paper, $\mathcal{V}$ is a set or
tuple of variables with $\mathcal{W} \subseteq \mathcal{V}$ denoting an arbitrary
subset of $\mathcal{V}$.

\begin{definition}
\label{def:sHYPE}
A \emph{stochastic HYPE model} is a tuple 
$(\mathit{ConSys},\mathcal{V},\mathit{IN},\mathit{IT},\mathcal{E}_d,\mathcal{E}_s,\Ac,\mathit{ec},\mathop{\mathit{iv}},\mathit{EC},\mathit{ID})$ where
\begin{itemize}
\item $\mathit{ConSys}$ is a well-defined controlled system as defined below.
\item $\mathcal{V}$ is a finite set of variables.
\item $\mathit{IN}$ is a set of influence names and $\mathit{IT}$ is a set of influence
type names.
\item $\mathcal{E}_d$ is the set of instantaneous events of the form $\ev{a}$ and $\ev{a}_i$.
\item $\mathcal{E}_s$ is the set of stochastic events of the form  $\sev{a}$ and
$\sev{a}_i$.
\item $\mathcal{E} = \mathcal{E}_d \cup \mathcal{E}_s$ is the set of all events for which the 
notation
$\ssev{a}$ and $\ssev{a}_i$ is used.
\item $\Ac$ is a set of activities of the form
$\alpha(\mathcal{W}) = (\iota,r,I(\mathcal{W})) \in (\mathit{IN} \times
\mathbb{R} \times \mathit{IT})$ where $\mathcal{W} \subseteq \mathcal{V}$.
\item $\mathit{ec}:\mathcal{E} \rightarrow \mathit{EC}$ maps events to event conditions. Event
conditions are pairs of activation conditions and resets. 
\begin{itemize}
\item Activation
conditions for the instantaneous events in $\mathcal{E}_d$ are formulae  with
free variables in $\mathcal{V}$ and for the stochastic
events in $\mathcal{E}_s$, they are functions
$f:\mathbb{R}^{|\mathcal{V}|}\rightarrow\mathbb{R}^+$.
\item Resets are conjunctions of formulae of the form 
$\rsdefa{V}{\theta(\mathcal{V})}$ where
$\theta(\mathcal{V})$ is an expression that may also include random
variables which are described by $\mathcal{X}(p_1,\ldots,p_m)$ where $\mathcal{X}$
is a distribution and the $p_i$ are the parameters for the distribution
which can themselves be expressions involving variables and random variables.
\end{itemize}
\item $\mathop{\mathit{iv}}: \mathit{IN} \rightarrow \mathcal{V}$ maps influence names to
variable names.
\item $\mathit{EC}$ is a set of event conditions.
\item $\mathit{ID}$ is a collection of definitions consisting
of a real-valued function for each influence type name
$\assign{I(\mathcal{W})} = f(\mathcal{W})$ where the variables in
$\mathcal{W}$ are from $\mathcal{V}$.
\item $\mathcal{E}$, $\Ac$, $\mathit{IN}$ and $\mathit{IT}$ are pairwise disjoint.
\end{itemize}
\end{definition}

In \cite{HYPE-journal}, \emph{well-defined HYPE models} are introduced
and the rationale behind the definition is to enforce a policy in
the way models are specified, forcing the modeller to separate the
description of the logical blocks constituting a HYPE model.
Subcomponents are ``flat'' (i.e. they always call themselves
recursively) and there is a one-to-one correspondence between
influences and subcomponents: each subcomponent describes how a
specific influence is modified by events. Furthermore, synchronization
must involve all shared events.  This notion extends straightforwardly
to stochastic HYPE models, and here we choose to define stochastic
HYPE systems in their well-defined form immediately rather than
having separate definitions.

\begin{definition}
A \emph{well-defined controlled system} has the form $\Sigma
\smash{\syncstar} \ev{init}.\mathit{Con}$ where $\Sigma$ is a well-defined
uncontrolled system and $\mathit{Con}$ is a well-defined controller, and
the synchronisation is on all shared events, in particular $\ev{init}$,
the initial event which must occur first (and has $\mathit{true}$ as its
activation condition).  Furthermore, all events that appear in the
controller must appear in the uncontrolled system and \emph{vice versa}.
The set of well-defined controlled systems is denoted by $\mathcal{C}$.

A \emph{well-defined controller} is defined by the two-level grammar
$M ::= \ssev{a}.M\ |\ 0 \ |\ M + M$ and $\mathit{Con} ::= M\ |\ \mathit{Con}
\smash{\sync{L}}\mathit{Con}$ with $\ssev{a} \in \mathcal{E}$
and with $L \subseteq \mathcal{E}$.

The \emph{well-defined uncontrolled system} consists of well-defined
subcomponents in cooperation over shared events where each subcomponent
appears at most once and $\mathcal{W}_i \subseteq \mathcal{V}$.
\begin{eqnarray*}
\Sigma & \rmdef & S_1(\mathcal{W}_1) \syncstar \ldots \syncstar S_s(\mathcal{W}_s)
\end{eqnarray*}

\emph{Well-defined subcomponents} represent the uncontrolled
capabilities of the system and each is a choice over events
such that $\ssev{a}_j \neq \ssev{a}_k$ for $j \neq k$,
$\ssev{a}_j \neq \ev{init}$ for all $j$, and 
$\mathcal{W} \subseteq \mathcal{V}$.
\begin{eqnarray*} S(\mathcal{W})
& \rmdef & {\sum}_{j=1}^n \ssev{a}_j{:}(\iota,r_j,I_j(\mathcal{W})).S(\mathcal{W}) +
\ev{init}{:}(\iota,r,I(\mathcal{W})).S(\mathcal{W})
\end{eqnarray*}
\end{definition}

A subcomponent is ready to react whenever any of its events'
activation condition becomes true or completes, after which the
influence associated with that event comes into force, replacing
any previous influence. By considering all the influences mapped
to a particular variable for a particular configuration of the
system, an ODE can be constructed using the definitions in $\mathit{ID}$
to describe the evolution of that variable whenever the system is
in that configuration. We assume well-defined stochastic HYPE models in
the rest of this paper. With the syntax of stochastic HYPE models
defined, the next three sections show how the dynamic behaviour of
stochastic HYPE models can be defined before illustrating this dynamic
behaviour with an substantial example of an assembly line.

\section{Operational Semantics}
\label{sec:SOS}

We now introduce the behaviour of stochastic HYPE models by defining
an appropriate semantics.  We will proceed in a different way to
that presented in the preliminary research \cite{BortBGH:11a}:
instead of mapping each subcomponent and each controller to a
stochastic hybrid automaton, and then composing them together with
a product construction, we will construct a labelled (multi)transition
system (LTS), similarly to \cite{Hill96}, and then map the LTS to
a stochastic hybrid automaton.

To construct the LTS, we need a notion of state. Proceeding in the
same manner as HYPE \cite{HYPE-journal}, states will record for
each influence its current strength and influence type. States
essentially capture the continuous behaviour, while the structure
of the LTS describes the discrete behaviour, both instantaneous and
stochastic.

\begin{definition}
An \emph{operational state} is a function $\sigma:\mathit{IN}
\rightarrow (\mathbb{R} \times \mathit{IT})$. The set of all operational
states is $\mathcal{S}$.  A \emph{configuration} consists of a controlled
system together with an operational state $\bigl\langle \mathit{ConSys}, \sigma
\bigr\rangle$ and the set of configurations is $\mathcal{F}$.
\end{definition}

In the following, we will usually refer to `operational states' as
`states'.  States can also be viewed as a set of triples
$(\iota,r,I(\mathcal{W}))$, where there is at most one triple containing
$\iota$. In this form, it is evident that states are simply collections
of enabled activities.  We stress that states describe flows, not
the values of continuous variables. As such, the LTS semantics of
stochastic HYPE is different to that of stochastic hybrid automata,
similarly to the way that the LTS semantics of HYPE differs from
those of hybrid automata \cite{HYPE-journal}.

The operational semantics give a labelled multitransition system
over configurations $(\mathcal{F},\mathcal{E},{\rightarrow} \subseteq \mathcal{F} \times
\mathcal{E} \times \mathcal{F})$. As customary, we  write $E\;
\lxrightarrow{\mathrm{\scriptstyle \:a\:}}\; F$, for $E, F \in \mathcal{F}$.
The rules are given in Figure~\ref{opersem} and are essentially
those of non-stochastic HYPE\@. The only formal difference is that
we consider in the rules both instantaneous and stochastic events,
treating them in the same way. The fact that the operational semantic
rules are essentially the same is because the LTS describes the
syntactic structure of the target hybrid automaton.  The proper
dynamics will be attached to a (stochastic) HYPE model by converting
its LTS to a (stochastic) hybrid automaton. This second step of the
semantics construction differs significantly from that used for
HYPE \cite{HYPE-journal}.

\begin{figure}[t]
\begin{center}
{\renewcommand{\arraystretch}{0.5}
$\begin{array}{ll}
\textbf{Prefix with influence:} & \textbf{Prefix without influence:} \\ \\
\displaystyle \frac{}{\bigl\langle \ssev{a}:(\iota,r,I).P,
           \sigma \bigr\rangle
           \lsexrightarrow{a} \bigl\langle P, \sigma[\iota \mapsto
           (r,I)] \bigr\rangle}\;(\ssev{a} \in \mathcal{E})  &
\displaystyle \frac{}{\bigl\langle \ssev{a}.P, \sigma \bigr\rangle
   \lsexrightarrow{a} \bigl\langle P, \sigma \bigr\rangle}\;(\ssev{a} \in \mathcal{E}) \\
\\
\\
\textbf{Choice:} & \textbf{Constant:} \\
\\
\displaystyle \frac{\bigl\langle P, \sigma \bigr\rangle \lsexrightarrow{a} \bigl\langle P', \sigma' \bigr\rangle}
  {\bigl\langle P + Q, \sigma \bigr\rangle \lsexrightarrow{a} \bigl\langle P', \sigma' \bigr\rangle}
\qquad
\displaystyle \frac{\bigl\langle Q, \sigma \bigr\rangle \lsexrightarrow{a} \bigl\langle Q', \sigma' \bigr\rangle}
  {\bigl\langle P + Q, \sigma \bigr\rangle \lsexrightarrow{a} \bigl\langle Q', \sigma' \bigr\rangle}
\qquad \qquad
&
\displaystyle \frac{\bigl\langle P, \sigma \bigr\rangle \lsexrightarrow{a} \bigl\langle P',\sigma' \bigr\rangle}
      {\bigl\langle A, \sigma \bigr\rangle \lsexrightarrow{a} \bigl\langle P', \sigma' \bigr\rangle}      (A \smash{\raisebox{-2.0pt}[0pt][0pt]{$\,\rmdef\,$}} P) \\
\\
\\
\multicolumn{2}{l}{
\hspace*{-0.16cm}
\begin{array}{l}
\textbf{Cooperation without synchronisation:} \\
\\
\displaystyle \frac{\bigl\langle P, \sigma \bigr\rangle \lsexrightarrow{a} \bigl\langle P', \sigma'
\bigr\rangle}
      {\bigl\langle P \sync{L} Q, \sigma \bigr\rangle \lsexrightarrow{a}
       \bigl\langle P' \sync{L} Q, \sigma' \bigr\rangle} (\ssev{a} \not\in L) \qquad
\displaystyle \frac{\bigl\langle Q, \sigma \bigr\rangle \lsexrightarrow{a} \bigl\langle Q', \sigma' \bigr\rangle}
      {\bigl\langle P \sync{L} Q, \sigma \bigr\rangle \lsexrightarrow{a}
       \bigl\langle P \sync{L} Q', \sigma' \bigr\rangle} (\ssev{a} \not\in L) \\
\\ \\
\textbf{Cooperation with synchronisation:} \\
\\
\displaystyle \frac{\bigl\langle P, \sigma \bigr\rangle \lsexrightarrow{a} \bigl\langle P', \tau \bigr\rangle
 \quad \bigl\langle Q, \sigma \bigr\rangle \lsexrightarrow{a} \bigl\langle Q', \tau' \bigr\rangle}
 {\bigl\langle P \sync{L} Q, {\sigma} \bigr\rangle \lsexrightarrow{a}
 \bigl\langle P' \sync{L} Q', \Gamma(\sigma,\tau,\tau') \bigr\rangle}
 (\ssev{a} \in L, \Gamma \text{ defined})
\end{array}}
\end{array}$}
\end{center}

\caption{Operational semantics for stochastic HYPE}
\label{opersem}
\end{figure}

Inspecting the rules of Figure \ref{opersem}, we can see that the
only rules updating the state are  Prefix with influence and
Cooperation with synchronisation.

In this latter case, in particular, we need to enforce consistency
in the way influences are updated by the cooperating components.
This is done by the function $\Gamma$.  The updating function
$\sigma[\iota\mapsto(r,I)]$ is defined as
\[ \sigma[\iota\mapsto(r,I)](x)= \begin{cases}
(r,I) & \text{if\ } x=\iota \\
\sigma(x) & \text{otherwise.}
\end{cases} \]
The notation $\sigma[u]$ will also be used for an update, with
$\sigma[u_1\ldots u_n]$ denoting $(\ldots((\sigma[u_1])[u_2])\ldots)[u_n]$.  The
partial function $\Gamma:\mathcal{S} \times \mathcal{S} \times \mathcal{S} \rightarrow \mathcal{S}$
is defined as follows.
\begin{eqnarray*}
{(\Gamma(\sigma,\tau,\tau'))}(\iota) & = &
\begin{cases}
\tau(\iota)  & \text{if $\sigma(\iota)=\tau'(\iota)$},\\
\tau'(\iota) & \text{if $\sigma(\iota)=\tau(\iota)$},\\
\text{undefined} & \text{otherwise}.
\end{cases}
\end{eqnarray*}
$\Gamma$ is undefined if both agents in a cooperation try to update
the same influence. See \cite{HYPE-journal} for further details.
In the following, we will also need some additional notions.

\begin{definition}
Given a controlled system $P$, define structurally the following sets:
\begin{itemize}
\item the \emph{set of events}, $\mathsf{ev}(P)$:
$\mathsf{ev}(\ssev{a}{\,:\,}\alpha.S) = \{ \ssev{a} \}$,  $\mathsf{ev}(\ssev{a}.S) = \{
\ssev{a} \}$, $\mathsf{ev}(S_1+S_2) = \mathsf{ev}(S_1) \cup \mathsf{ev}(S_2)$,\linebreak  $\mathsf{ev}(P_1
\smash{\sync{L}} P_2) = \mathsf{ev}(P_1) \cup \mathsf{ev}(P_2)$;
\item the \emph{set of influences}, $\mathsf{in}(P)$:
$\mathsf{in}(\ssev{a}{\,:\,}(\iota,r,I(\mathcal{W})).S) = \{ \iota \}$ $\mathsf{in}(\ssev{a}.S)
= \emptyset$, $\mathsf{in}(S_1+S_2) = \mathsf{in}(S_1) \cup \mathsf{in}(S_2)$, $\mathsf{in}(P_1
\smash{\sync{L}} P_2) = \mathsf{in}(P_1) \cup \mathsf{in}(P_2)$; \item the \emph{set
of prefixes}: $\mathsf{pr}(\ssev{a}{\,:\,}\alpha.S) = \{ \ssev{a}{\,:\,}\alpha
\}$, $\mathsf{pr}(\ssev{a}.S) = \emptyset$, $\mathsf{pr}(S_1+S_2) = \mathsf{pr}(S_1)
\cup \mathsf{pr}(S_2)$, $\mathsf{pr}(P_1 \smash{\sync{L}} P_2) = \mathsf{pr}(P_1) \cup
\mathsf{pr}(P_2)$.  \end{itemize} \end{definition}

\begin{definition}
The \emph{derivative
set} of a controlled system $P$, $\mathop{\mathrm{ds}}(P)$, is defined as the
smallest set satisfying
\begin{itemize}
\item if $\cf{P,\sigma} \lsexrightarrow{init} \cf{P',\sigma'}$ then
$\cf{P',\sigma'} \in \mathop{\mathrm{ds}}(P)$
\item if $\cf{P',\sigma'} \in \mathop{\mathrm{ds}}(P)$ and $\cf{P',\sigma'}
\lsexrightarrow{a}
\cf{P'',\sigma''}$ then $\cf{P'',\sigma''} \in \mathop{\mathrm{ds}}(P)$.
\end{itemize}
Furthermore, we indicate with $\mathop{\mathrm{st}}(P) = \{ \sigma \mid \cf{Q,\sigma}
\in \mathop{\mathrm{ds}}(P) \}$ the set of \emph{states} of the derivative set of a
controlled system $P$.
\end{definition}

In the $\mathit{Buffer}$ model, there are four states in the LTS, corresponding
to the four possible combinations of activation of input and output
channels. The influences $f$ and $t$ are the same in all states.
For instance, the state in which the input link is active
and the output is not active is
\begin{eqnarray*}
\sigma & = & \{ in \mapsto (r_{in},\mathit{const}), \:\: 
                     out \mapsto (0,\mathit{const}), \:\:
                     f \mapsto (0,\mathit{const}), \:\: 
                     t \mapsto (1,\mathit{const})\} 
\end{eqnarray*}

Propositions 5.1 to 5.5 proved for HYPE \cite{HYPE-journal}, hold
for well-defined stochastic HYPE models. In particular, the function
$\Gamma$ used in the Cooperation with synchronisation rule, is
always defined for well-defined stochastic HYPE systems. The $\mathit{Buffer}$
system is well-defined, and hence $\Gamma$ is always defined.

\section{Transition-Driven Stochastic Hybrid Automata}
\label{sec:TDSHA}

Because stochastic HYPE considers three distinct types of behaviour,
whereas HYPE considers only two, we need a different target for our
semantics. The semantics for HYPE are provided by hybrid automata which
covers continuous and instantaneous behaviour but not stochastic
behaviour.
We  now present Transition-Driven Stochastic Hybrid Automata,
introduced by Bortolussi and Policriti
\cite{PA:Bortolussi:2010:HybridDynamicsStochProg:TCS,BorP11},
a formalization of stochastic hybrid automata putting emphasis on
transitions, which can be either discrete (corresponding to
instantaneous or stochastic jumps) or continuous (representing flows
acting on system variables).  This formalism can be seen as an
intermediate layer in defining the stochastic hybrid semantics of
stochastic HYPE\@. In fact, TDSHA are themselves mapped to Piecewise Deterministic
Markov Processes~\cite{Davis93}, so that their dynamics can be
formally specified in terms of the latter.  Due to space constraints,
we will not provide a formal treatment of this construction, and
refer the reader papers by Bortolussi and Policriti
\cite{PA:Bortolussi:2010:HybridDynamicsStochProg:TCS,BorP11}
and \cite{BortB:12} for further details. We choose to work with TDSHA
rather than PDMPs because their definition is more operational in
nature, and hence this leads to a more straightforward mapping.


\begin{definition}\label{def:TSHS}
A Transition-Driven Stochastic Hybrid Automaton (TDSHA) is a tuple
$\TDSHA{} =
(Q,\vr{X},\TC,\TD,$ $\TS,\mathrm{init},\mathcal{E})$, where
\begin{itemize}
\item $\modes{}$ is a finite set of \emph{control modes}.

\item $\vrX{} = \{X_1,\ldots,X_n\}$ is a set of real valued
\emph{system variables} with the time derivative of $X_j$ denoted
by $\dot{X_j}$ and the value of $X_j$ after a change of mode denoted
by $X_j'$.

\item $\TC{}$ is the \emph{multiset} of \emph{continuous transitions
or flows}, whose elements $\tau$ are triples
$(\mode{\tau},\stoich{\tau},\rf{\tau})$, where $\mode{\tau}\in
\modes{}$ is a mode, $\stoich{\tau}$ is a vector of size $|\vrX{}|$,
and $\rf{\tau}:\mathbb{R}^n\rightarrow \mathbb{R}$ is a \emph{Lipschitz continuous}
function.

\item $\TD{}$ is the \emph{set} of \emph{instantaneous transitions},
whose elements $\delta$ are tuples of the form
$(\exit{\delta},\enter{\delta},\guard{\delta},\res{\delta},$
$\priority{\delta},\e{\delta})$.  The transition goes from mode
$\exit{\delta}$ to mode $\enter{\delta}$.

\begin{itemize}
\item The \emph{guard} $\guard{\delta}$ is a first-order formula
with free variables from $\vr{X}$, representing the \emph{closed
set} $G_{\delta} = \{\vr{x}\in\mathbb{R}^n~|~\guard{}[\vr{x}]\}$.  \item
The \emph{reset} $\res{\delta}$ is a conjunction of atoms of the
form $X'=r(\mathbf{X},\mathbf{W})$ where
$r:\mathbb{R}^n\times\mathbb{R}^h\rightarrow\mathbb{R}$ is the reset
function of $X$ dependent on the variables $\mathbf{X}$ as well as
a random vector $\mathbf{W}$. Variables not appearing in the reset
remain unchanged and a reset with value $\mathit{true}$ is the identity
function on each variable.

\item The \emph{weight (priority)} of the edge is $\priority{\delta}\in
\mathbb{R}^+$ and is used to solve non-determinism among two or more
active transitions.

\item The \emph{label} of the edge is $\e{\delta}\in\events{}$.
\end{itemize}

\item $\TS{}$ is the \emph{multiset} of \emph{stochastic transitions},
whose elements $\eta$ are tuples of the form $\eta =
(\exit{\eta},\enter{\eta},$ $\guard{\eta},\res{\eta},\linebreak\rf{\eta},\e{\eta})$,
where $\exit{\eta}$, $\enter{\eta}$, $\guard{\eta}$, $\e{\eta}$,
and $\res{\eta}$ are as for transitions in $\TD{}$.
\begin{itemize}
\item The \emph{rate} of the edge is 
$\rf{\eta}:\mathbb{R}^n\rightarrow \mathbb{R}^+$, a rate
function giving the instantaneous probability of taking transition
$\eta$. It is locally \emph{integrable} along any continuous differentiable
curve.  Additionally, transitions labelled by the same event are
required to have 
\emph{consistent} rates: if $\e{\eta_1} = \e{\eta_2}$, then
$\rf{\eta_1}=\rf{\eta_2}$.  
\end{itemize}

\item $\events{}$ is a finite set of event names, labelling discrete
transitions.  $\events{}$ can be partitioned into
$\events{d}\cup\events{s}$, such that all events labelling instantaneous
transitions belong to $\events{d}$, while all events labelling
stochastic transitions are from $\events{s}$.  

\item $\initial{}$ is a pair $(\initmode{},\mathbf{W})$, with
$\initmode{}\in\modes{}$ and $\mathbf{W}$ is a random vector of $n$
variables representing a point in
$\mathbb{R}^n$ and providing the initial values for $\vrX{}$.
$\initial{}$ describes the initial state of the system.

\end{itemize}
\end{definition}

Note that in the previous definition, we consider sets of instantaneous
transitions and multisets of stochastic and continuous transitions.
This is justified by the fact that multiplicity plays a relevant
role only in quantified behaviours (i.e. flows and stochastic
events), but it is not really relevant for instantaneous events,
which are triggered by a boolean condition, whose truth is insensitive
to the presence of multiple transitions of the same kind.

In order to formally define the dynamical evolution of TDSHA, we
can map them into a well-studied model of Stochastic Hybrid Automata,
namely Piecewise Deterministic Markov Processes~\cite{Davis93}.
Here we sketch basic ideas about the dynamical behaviour of TDSHA.
\begin{itemize}
\item Within each discrete mode $\mode{}\in \modes{}$, the system
follows the solution of a set of ODEs, constructed combining the
effects of the continuous transitions $\tau$ acting on mode $q$.
The function $\rf{\tau}(\vr{X})$ is multiplied by the vector
$\stoich{\tau}$ to determine its effect on each variable and then
all such functions are added together, so that the ODEs in mode $q$
are $\dot{\vr{X}} = \sum_{\tau~|~\mode{\tau} = q}  \stoich{\tau}\cdot
\rf{\tau}(\vr{X})$. 


\item Two kinds of discrete jumps are possible. Stochastic transitions
are fired according to their rate, similarly to standard Markovian
Jump Processes. Instantaneous transitions, by contrast, are fired
as soon as their guard becomes true.  In both cases, the state of
the system is reset according to the specified reset policy which
is not necessarily deterministic.  Choice among several active
stochastic or instantaneous transitions is performed probabilistically
proportionally to their rate or weight.

\item A trace of the system is therefore a sequence of instantaneous
and random jumps interleaved by periods of continuous evolution.
\end{itemize}

Previously \cite{BortBGH:11a}, we defined a synchronization product
between TDSHA which is presented in Appendix~\ref{sec:SOSmapping} where it
is used to define the mapping used in our previous work on
stochastic HYPE \cite{BortBGH:11a}.

\section{Mapping stochastic HYPE to TDSHA}
\label{sec:HYPEtoTDSHA}

We present now a mapping from stochastic HYPE to TDSHA which is
based on the LTS obtained by the operational semantics. As mentioned
before, this construction is different from the one defined 
previously in \cite{BortBGH:11a}, in which we converted each subcomponent
and each controller of stochastic HYPE to TDHSA, and then combined these TDSHA
with a synchronization product. Essentially, the operational semantics
takes care of this synchronization, and avoids the complications
of the TDSHA product construction.

The mapping from LTS to TDSHA is quite straightforward: modes are
given by the derivative set of the controlled system $\mathit{ConSys}$,
namely by the set of reachable configurations, continuous transitions
are extracted from the state in each configuration, and instantaneous
and stochastic transitions correspond to the LTS transitions.
Multiplicities of transitions labelled with stochastic events
have to be respected to properly
account for the quantitative behaviour of stochastic events, but as
mentioned previously, we ignore multiplicity of instantaneous
transitions, choosing to have a single transition with weight one.
We assume that
multiplicity of elements in a multiset is always respected in the
definitions below.
 
Consider a stochastic HYPE model
$(\mathit{ConSys},\mathcal{V},\mathit{IN},\mathit{IT},\mathcal{E}_d,\mathcal{E}_s,\Ac,\mathit{ec},\mathop{\mathit{iv}},\mathit{EC}\!,\mathit{ID})$, and let
$\bigl\langle P_0, \sigma_0 \bigr\rangle$ be the configuration in the LTS
obtained from $\mathit{ConSys}$ after the execution of the initial event,
$\ev{init}$,
namely
$\bigl\langle \mathit{ConSys}, \sigma \bigr\rangle \mlsxrightarrow{\ev{init}}
\bigl\langle P_0, \sigma_0 \bigr\rangle$. In the case of a well-defined
HYPE model $\sigma_0$ does not depend on $\sigma$, as shown by
\cite{HYPE-journal} and this applies to stochastic HYPE models as well.  We also let $\vr{v_0}$  be the value of
variables $\mathcal{V}$ after initialisation.

In the following, we will refer to the activation condition and the
reset of an event $\ssev{a}\in\mathcal{E}$ by $\mathit{act}(\ssev{a})$ and
$\mathit{res}(\ssev{a})$, respectively; hence $\mathit{ec}(\ssev{a}) =
(\mathit{act}(\ssev{a}),\mathit{res}(\ssev{a}))$. Recall that, for an instantaneous
event $\ev{a}$, $\mathit{act}(\ev{a})$ is  a boolean formula  while, for a
stochastic event $\sev{a}$, $\mathit{act}(\sev{a})$ is a function taking
values in the positive reals.  Given a state $\sigma = \{
\iota_i\mapsto (r_i,I_i)~|~i=1,\ldots k\}$, we indicate with
$\vr{1}_{\mathop{\mathit{iv}}(\iota_i)}$ the $k$-vector equal to 1 in the coordinate
corresponding to variable $\mathop{\mathit{iv}}(\iota_i)$ and zero elsewhere.

The reset $\mathit{res}(\ssev{a})$ is defined as the conjunction of atoms
of the form $V \sim \theta(\mathcal{V})$. To obtain a reset in the TDHSA,
each distribution $\mathcal{X}_i$ mentioned in $\theta(\mathcal{V})$ must be
associated with a distinct variable $W_i$, then the reset function for
a transition labelled with $\ssev{a}$ is $R_{\ssev{a}}(\mathcal{V},\mathbf{W})$
such that each random variables $W_i$ is drawn from its associated
distribution.  

The mapping now defined differs from the approach we took for
standard HYPE, since it requires stochastic transitions.

\newpage

\begin{definition}
\label{def:shypetotdsha}
Let $\mathcal{H} = (\mathit{ConSys},\mathcal{V},\mathit{IN},\mathit{IT},\mathcal{E}_d,\mathcal{E}_s,\Ac,\mathit{ec},\mathop{\mathit{iv}},\mathit{EC}\!,\mathit{ID})$
be a stochastic HYPE model. The TDSHA $\TDSHA{}(\mathcal{H}) = \TDSHAtuple{}$
associated with $\mathcal{H}$ is defined by:
\begin{itemize}
\item the set of discrete modes is the derivative set of $\mathit{ConSys}$: 
$Q = ds(\mathit{ConSys})$;  
\item the set of continuous variables is $\vr{X} = \mathcal{V}$; 
\item the initial state is 
$\mathrm{init} = (\bigl\langle P_0, \sigma_0 \bigr\rangle,R_{\ev{init}})$;
\item the set of events is $\mathcal{E} = \mathcal{E}_d\cup\mathcal{E}_s$;
\item the multiset of continuous transitions $\TC{}$ is constructed as
follows: \newline with each $\bigl\langle P, \sigma \bigr\rangle \in Q$, $\sigma = \{
\iota_i\mapsto (r_i,I_i)~|~i=1,\ldots k\}$, we associate the
continuous transitions $(\bigl\langle P, \sigma
\bigr\rangle,\vr{1}_{\mathop{\mathit{iv}}(\iota_i)},r_i.\assign{I_i})$, $i=1,\ldots k$;
\item the set of instantaneous transitions $\TD{}$ is obtained as
follows: \newline with each $\bigl\langle P_1, \sigma_1 \bigr\rangle \mlsxrightarrow{\ev{a}}
\bigl\langle P_2, \sigma_2 \bigr\rangle$ we associate the instantaneous transition
\newline $(\bigl\langle P_1,
\sigma_1 \bigr\rangle,\bigl\langle P_2, \sigma_2
\bigr\rangle,\mathit{act}(\ev{a}),R_{\ev{a}},p,\ev{a})$ with weight
$p=1$. We ignore multiplicity in
the LTS.
\item the multiset of stochastic transitions $\TS{}$ is constructed as
follows: \newline with each $\bigl\langle P_1, \sigma_1 \bigr\rangle \mlsxrightarrow{\sev{a}}
\bigl\langle P_2, \sigma_2 \bigr\rangle$ 
taking into account multiplicity in the LTS
we associate the stochastic transition \newline $(\bigl\langle P_1,
\sigma_1 \bigr\rangle,\bigl\langle P_2, \sigma_2
\bigr\rangle,true,R_{\sev{a}},\mathit{act}(\sev{a}),\sev{a})$ with 
guard $\mathit{true}$ and rate function $\mathit{act}(\sev{a})$ and thus preserve
multiplicity.
\end{itemize}
\end{definition}

This definition gives the same TDSHA as that in the earlier work
on stochastic HYPE \cite{BortBGH:11a} which used a product construction
(the compositional mapping);
however, we prefer to work first with a labelled transition system
before mapping to a TDHSA as it allows us to define bisimulation
at the level of stochastic HYPE models. 
We can prove that the semantics defined above and those presented
in \cite{BortBGH:11a} map a stochastic HYPE model to the same TDSHA
and this theorem and its proof can be found in
Appendix~\ref{sec:SOSmapping}.

\begin{figure}
\begin{center}
\includegraphics[width=12.5cm]{nn.pdf}
\end{center}
\caption{A single trace for the network node with
$\mathit{max}_B=200$, $k_\mathit{in}^\mathit{on}=0.4$, 
$k_\mathit{in}^\mathit{off}=k_\mathit{out}^\mathit{off}=
k_\mathit{out}^\mathit{on}=0.2$, $r_\mathit{in}=20$, 
$r_\mathit{out}=10$, $\Delta=2.5$, $\xi=0.5$ and $b_0=100$.
The variable $B$ represents the quantity of packets in the buffer,
$T$ the time, $C$ the variable that records the time, and $D$ the
duration.}
\label{fig:node}
\end{figure}

A single trajectory of the node example from Section~\ref{sec:HYPE}
is given in Figure~\ref{fig:node}. The proportion of time that the
input connection is up and the rate of input are both higher than
that of the output node, and this can be seen in the fact that the
slopes for input  are steeper, and the buffer is hitting its maximum
capacity frequently. The failure that causes packets to be dropped
does, paradoxically, enable the buffer to accept more packets when
there is a connection.

We next consider some technical issues of model behaviour, as well a
syntactic abbreviation for events with non-exponential durations.
After this, the example of an assemble line shows the versatility of
stochastic HYPE and this is followed by the definition of an equivalence
over stochastic HYPE models that provides reasoning about when two
models have the same behaviour.

\subsection{Well-behaved models}

In the paper that defines HYPE \cite{HYPE-journal}, a notion of
well-behavedness is introduced. This notion ensures that the model
can never execute an infinite number of simultaneous instantaneous
events (called instantaneous Zeno behaviour), hence ensuring that
models can be simulated. We want stochastic HYPE models to be 
similarly well-behaved, so that models can be simulated and additionally
so that the TDHSA that a stochastic HYPE model is mapped to, can
be interpreted as piecewise deterministic Markov process (PDMP)
\cite{Davis93}.  The definition of PDMPs require that an instantaneous
event is not immediately followed by another one, and if the behaviour
of the stochastic HYPE model is such that in its TDHSA there are
only finite sequences of simultaneous events, then each finite
sequence can be mapped to a single event and thus satisfy the PDMP
definition. 

\begin{definition}
\label{def:well-behaved}
A stochastic HYPE model $P$ is well-behaved if it has a finite
number of finite sequences of simultaneous instantaneous events and
these sequences are independent of the initial state of the system.
\end{definition}

To ensure well-behavedness for a HYPE model (as defined in
\cite{HYPE-journal}, so without stochastic events), it is sufficient to
show that the instantaneous activation graph, or I-graph, of a HYPE
model is acyclic. This graph is constructed by considering the
instantaneous transitions of the labelled transition systems obtained
from a HYPE model. The I-graph gives an overapproximation of a HYPE
model's behaviour. If there are no cycles then the model is
well-behaved, but the I-graph of a well-behaved model is not necessarily
acyclic.

Considering stochastic HYPE models,
the addition of random resets has a minor effect on the construction
on the I-graph
in that for each event the possible set of values after a reset
must take into account the support of any distribution involved in
the reset, which can lead to additional overapproximation.  The
extension to stochastic events does not alter this construction and
all results from \cite{HYPE-journal} hold for stochastic HYPE models.
The addition of a stochastic event between two instantaneous events,
or alternatively, the modification of an instantaneous event to a
stochastic one may break the cyclicity of an I-graph thus leading
to a well-behaved model. Hence, both Theorem 6.1 and Theorem 6.2
proved by \cite{HYPE-journal} hold for stochastic HYPE, as well
as Propositions 6.1 to 6.4.  which describe specific conditions on
controllers that lead to well-behaved models. A new proposition can
be proved in the stochastic setting.

\begin{proposition}
\label{prop:well-behavedness}
Let $P$ be a stochastic HYPE model with $\mathit{Con} \rmdef
\ssev{a}_1\ldots\ssev{a}_n.Con$. If there exists $i$ such that
$\sev{a}_i$ is a stochastic event then $P$ is well-behaved.
\end{proposition}
\begin{proof}
Since $\mathit{Con}$ cycles through $n$ events, if one of these events is
not instantaneous and therefore has a duration then it is not possible 
for there to be an infinite sequence of instantaneous events.
\end{proof}

This proposition cannot be applied to the $\mathit{Buffer}$ example, because
the controllers are not cyclical, but a similar argument can be
made. For the one instantaneous event in each controller ($\ev{full}$
or $\ev{empty}$), a stochastic event must occur before the instantaneous
event can reoccur, hence preventing the unwanted behaviour. Considering
the two controllers in cooperation, they have disjoint events and
hence the overall controller consists of interleavings of these
events. It is not possible for a sequence to occur consisting only
of $\ev{full}$ and $\ev{empty}$ since there must be interleaving
stochastic events. Hence $\mathit{Buffer}$ is well-behaved. This can also
be proved using Proposition 6.4 from \cite{HYPE-journal} since
neither $\ev{full}$ nor $\ev{empty}$ activate each other, so one
cannot immediately proceed the other. Considering the controller
$\mathit{Con}_\mathit{fail}$, the only way in which multiple $\ev{fail}$
events can happen simultaneously is if the random value for the
next duration is repeatedly zero. The probability of this is zero
and hence the controller is well-behaved. Proposition 6.4 can be
used again to show that the composition of all three controllers
is well-behaved.

\subsection{Non-exponential durations}

We also introduce some syntax that will allow us to write more compact
models. Currently the duration of stochastic events is specified by
exponential distributions because this is a good match with TDSHA and
PDMPs and more particularly because it avoids the need for residual
clocks. However, we can allow a notation whereby any expression involving
random variables can appear as the first element of an event condition.
This provides a way to express any random duration directly in an
event condition.  This will then be expanded to two events, and
requires the introduction of two variables, one to record the current
time and one to record the duration of the event. This introduces a
specific timer to track how much time is left of a duration.
To illustrate this, consider the following event.
\begin{eqnarray*}
\mathit{ec}(\ev{fail}) & = & {(T=C\!+\!D,
\;\rsdefa{C}{T} \:\wedge\: \rsdefa{D}{\mathcal{N}(\Delta,\xi)})
\:\wedge\: \rsdefa{B}{B\!-\!\mathcal{U}(0,B)})}
\end{eqnarray*}
This can be written as 
\begin{eqnarray*}
\mathit{ec}(\sev{fail}) & = & {(\mathcal{N}(\Delta,\xi),
\rsdefa{B}{B\!-\!\mathcal{U}(0,B)})}
\end{eqnarray*}
If there is no Timer
subcomponent with an influence affecting a time variable $T$, then these
must also be added. Since an expression that contains no random
variables is interpreted as the rate of an exponential distribution, the
notation $\delta(p)$ where $p$ contains no random variables will be used
to denote a fixed-time duration of $p$ time units.

We have now defined the dynamics of stochastic HYPE system as well
as highlight how models can have desirable behaviour. We assume
well-behavedness in the rest of the paper.  We proceed with an
example after which we consider how we can formally compare two
systems in terms of their behaviour.

\section{Example: a manufacturing system}
\label{sec:assemblyline}

\begin{figure}
\vspace*{-0.3cm}
\begin{center}
\input{machines}
\end{center}
\vspace*{-0.3cm}
\caption{Schematic of the assembly system}
\label{fig:assembler}
\end{figure}

\begin{figure
{\renewcommand{\arraystretch}{1.10}
$$\begin{array}{rcl}
\\
\\
\mathit{Assembler} & \rmdef & Sys \syncstar \ev{init}.\mathit{Con}_j \\
& & \\
Sys & \rmdef & (\mathit{Feed}_1 \syncstar \mathit{Feed}_2 \syncstar Feed_3) \syncstar 
               \mathit{Inspect} \syncstar \\
    &        & (\mathit{Timer}_1 \syncstar \mathit{Machine}_1(W_1)) \syncstar \\
    &        & (\mathit{Timer}_2 \syncstar \mathit{Machine}_2(W_2)) \\
& & \\
\mathit{Feed}_i    & \rmdef & \ev{init}{\,:\,}(p_i,\mathit{arrivals}_i,\mathit{const}).\mathit{Feed}_i\:+\\
           &        & \ev{overflow}{\,:\,}(p_i,0,\mathit{const}).\mathit{Feed}_i\\
\\
\mathit{Inspect}   & \rmdef & \ev{init}{\,:\,}(b,-\mathit{departures},\mathit{const}).\mathit{Inspect}\:+\\
           &        & \sev{scan}{\,:\,}(b,-\mathit{departures},\mathit{const}).\mathit{Inspect} \\
           &        & \sev{resume}{\,:\,}(b,0,\mathit{const}).\mathit{Inspect} \\
           &        & \ev{overflow}{\,:\,}(b,0,\mathit{const}).\mathit{Inspect} \\
\\
\mathit{Machine}_i(W_i) & \rmdef &
    \ev{init}{\,:\,}(w_i,\mathit{wa}_i,\mathop{\mathit{linear}}(W_i)).\mathit{Machine}_i(W_i)\:+\\
& & \ev{check}_i{\,:\,}(w_i,0,\mathit{const}).\mathit{Machine}_i(W_i)\:+\\
& & \sev{remove}_i{\,:\,}(w_i,\mathit{wt}_i,\mathop{\mathit{linear}}(W_i)).\mathit{Machine}_i(W_i)\:+ \\
& & \ev{assem}_i{\,:\,}(w_i,\mathit{wa}_i,\mathop{\mathit{linear}}(W_i)).\mathit{Machine}_i(W_i) \\
& & \ev{overflow}_i{\,:\,}(w_i,0,\mathop{\mathit{linear}}(W_i)).\mathit{Machine}_i(W_i) \\
\\
\mathit{Timer}_i   & \rmdef & \ev{init}{\,:\,}(t_1,0,\mathit{const}).\mathit{Timer}_i\:+ \\
           &        & \ev{remove}_i{\,:\,}(t_1,1,\mathit{const}).Timer_i\:+ \\
           &        & \ev{assem}_i{\,:\,}(t_1,0,\mathit{const}).\mathit{Timer}_i\\
\\
\mathop{\mathit{iv}}(p_i)   & = & P \quad \mathop{\mathit{iv}}(t_i) \: = \: T_i \quad \mathop{\mathit{iv}}(w_i) \: = \: W_i
\quad \mathop{\mathit{iv}}(b) \: = \: B \\
\\
\mathit{ec}(\ev{init}) & = & (true,\;\rsdefa{P}{P_0} \:\wedge\: \rsdefa{T_1}{0}
\:\wedge\: \rsdefa{T_2}{0} \:\wedge\: \rsdefa{B}{B_0}) \\
\mathit{ec}(\ev{overflow}) & = & (B \geq B_f,\;\mathit{true}) \\
\mathit{ec}(\ev{check}_i) & = & (P\geq n_i,\;\mathit{true}) \\
\mathit{ec}(\ev{assem}_i) & = & (T_i \geq \mathit{atime}_i,\; \rsdefa{B}{B\!+\!m_i}) \\
\\
\mathit{ec}(\sev{remove}_i) & = & (\mathit{ttime}_i,\;\rsdefa{P}{P\!-\!n_i} \:\wedge\:
\rsdefa{T_i}{0}) \\
\mathit{ec}(\sev{scan}) & = &
(\mathit{etime},\;\rsdefa{B}{B-min(B,\Gamma(S_c,S_h))}) \\
\mathit{ec}(\sev{resume}) & = & (\mathcal{F}(\mathit{rtime}),\;\mathit{true}) \\
\\
\eval{const} & = & 1 \qquad \eval{linear(X)} \: = \: X \\
\end{array}$$
}
\caption{Model for assembler with two machines (controller omitted)}
\label{fig:assemuncontrolled}
\end{figure}

\begin{figure}
{\renewcommand{\arraystretch}{1.20}
$$\begin{array}{rcl}
\\
\mathit{Con} & \rmdef & ((C_1 \parallel C_2) \syncstar C_m) \parallel 
C_e \parallel C_f \\
\\
C_i & \rmdef & \ev{check}_i.C'_i \\
C'_i & \rmdef & \sev{remove}_i.C''_i \\
C''_i & \rmdef & \ev{assem}_i.C_i \\
\\
C_m & \rmdef & \ev{check}_1.C'_{m} +
               \ev{check}_2.C''_{m} \\
C'_m & \rmdef & \sev{remove}_1.C_m \\
C''_m & \rmdef & \sev{remove}_2.C_m \\
\\
C_e & \rmdef & \sev{scan}.\sev{resume}.C_e \\
\\
C_f & \rmdef & \ev{overflow}.0 
\end{array}$$}

\caption{Controller for the assembly system}
\label{fig:assemcontroller}
\end{figure}

The example considers automated machines for assembling together
groups of identical items, for example, putting matches into
matchboxes. A schematic of the system is presented in
Figure~\ref{fig:assembler}. Each machine determines if there are
sufficient items in the pool ($\ev{check}_i$), then it takes these
$n_i$ items. Since this action can vary in duration it is modelled
as a stochastic event ($\sev{remove}_i$) with a exponentially
distributed duration.  The next step is assembly and the event
$\ev{assem}_i$ indicates the end of this fixed duration process
when the machine places $m_i$ finished items onto an output conveyor
belt. Only one machine is allowed to take items from the pool at a
time and this is enforced by a controller.

There are three lines of items that feed into the pool. Completed
items are removed from the conveyer belt. At the conveyer belt, there
is an agent that stops the belt, inspects the items near to it,
removes incorrectly assembled items and restarts the belt. If the
beginning of the conveyer belt becomes congested and starts to
overflow, the system moves to a failsafe state where everything
stops.

Here, we treat both the input feed into the pool ($P$) and the output
belt ($B$) as continuous.
We also track the power consumption of each machine ($W_i$).
The uncontrolled system is defined in Figure~\ref{fig:assemuncontrolled}
and its controller are presented in Figure~\ref{fig:assemcontroller}.
$\mathit{Con}$ consists of five controllers: one for each
machine, a controller that controls access to the pool,
a controller for inspection of assembled items, and 
a controller that determines the congestedness of the
output belt and shuts down the whole system if necessary.  
Figure~\ref{fig:parrun} provides a single run of the system.

We now consider a more complex scenario to show the potential of
stochastic HYPE. This example involves the following cost optimisation
problem. The manufacturer receives an order for $K$ products that
have to be produced within a certain deadline.  Failure to meet the
deadline will result in a penalty proportional to the delay. We
assume that the assembly machines can be tuned by changing the batch
size of a single assembly: the machine can take more items from the
pool and put more assembled items on the belt. This has a cost in
terms of assembly time and energy consumption. However, we assume
that the production time increases as the square root of the batch
size, while the energy increases quadratically.  This models the
fact that increasing the batch size reduces the production time but
at an increased energy cost. Energy itself contributes to the total
cost at a given price per unit. The goal of the manufacturing is
to find the batch size that minimises the average cost, defined as
the energy cost plus the penalty to miss the deadline. This design
problem can be solved by exploring parameters in a feasible range
and looking for the minimum value of the average cost, and results
are reported in Figure ~\ref{fig:intrun}  (taking the average over
1000 runs per point), suggesting an optimal batch size of 2. The model
for this optimisation requires minor changes to the model in
Figure~\ref{fig:assemuncontrolled} and these are easy to make because
of the structured form of the model. Assembly times and the flows
describing energy consumption are modified, and for the purposes
of the example, the area where the manufactured items are placed
is made much larger because the focus is on production, rather than
problems related to overflow. No changes are required for the
controllers.

\begin{figure}
\begin{center}
\begin{tabular}{cc}
\includegraphics[width=12.5cm]{mPB.pdf} \\
\includegraphics[width=12.5cm]{mPBWT.pdf}
\end{tabular}
\end{center}
\caption{A single trace for the assembly system showing
variables $P$ and $B$ (top) and variables $B$, $T_i$ and $W_i$
(bottom) using the parameters $\mathit{arrivals}_i=20$, $\mathit{departures}=0.2$, $\mathit{atime}_i=2$,
$\mathit{ttime}=0.8$, $n_i=100$, $m_i=2$, $\mathit{wt}_i=0.03$,
$\mathit{wa}_i=0.05$, $\mathit{etime}=2$, $\mathit{rtime}=20$, $S_c=4$ $S_h=0.5$ and
$B_f = 25$}
\label{fig:parrun}
\end{figure}

\begin{figure}
\begin{center}
\begin{tabular}{cc}
\includegraphics[width=12.5cm]{manplM.pdf} \\
\includegraphics[width=12.5cm]{manplC.pdf}
\end{tabular}
\end{center}
\caption{
Energy plus penalty cost for various values of batch size $m$,
assuming both machines are configured to the same value. Two
trajectories for different values of $m$ (top) and average cost for a range of
values for $m$ over 1000 trajectories (bottom).
Energy cost per
unit of energy is 0.5, while penalty cost is 2 per time unit.  Energy
rate consumption in the assembly phase is equal to $1/3*m^2 + 2/3$,
while the duration of the assembly equals $\alpha*(\sqrt{m}-1) + 1.5$,
for $\alpha = 1/(2*sqrt(2) - 2)$. The number of items taken from the
pool is $50 m$.  We assume the order is of 100 items with a
deadline of 100 time units.}
\label{fig:intrun}
\end{figure}

\section{Bisimulations for stochastic HYPE}
\label{sec:bisimHYPE}

We now consider behavioural equivalences for well-behaved stochastic
HYPE models. First, we
show that how the natural extension of the bisimulation defined for HYPE
is not a useful definition when stochastic hybrid models are considered.
Next, we define an equivalence that is more
suited to capture the notion of same behaviour both stochastically
and instantaneously.

\subsection{System bisimulation}

We have previously defined system bisimulation for HYPE \cite{HYPE-journal}
and shown that it is the same as ic-bisimulation
\cite{CuijCR:03a,BergBM:05a}. The definition of system bisimulation
along these lines for stochastic HYPE only requires the modification
of the labels on the transitions so that they can either be stochastic
or instantaneous.

\begin{definition}
A relation $B \subseteq \mathcal{C} \times \mathcal{C}$
is a \emph{system bisimulation} if for all $(P,Q) \in B$, for all
$\ssev{a}
\in \mathcal{E}_d \cup \mathcal{E}_s$, for all $\sigma \in \mathcal{S}$ whenever
\begin{enumerate}
\item $\cf{P,\sigma} \xrightarrow{\ssev{a}} \cf{P',\sigma'}$, there exists
$\cf{Q',\sigma'}$ with $\cf{Q,\sigma} \xrightarrow{\ssev{a}}
\cf{Q',\sigma'}$,
$(P'\!,Q') \in B$.
\item $\cf{Q,\sigma} \xrightarrow{\ssev{a}} \cf{Q',\sigma'}$, there exists
$\cf{P',\sigma'}$ with $\cf{P,\sigma} \xrightarrow{\ssev{a}}
\cf{P'\!,\sigma'}$,
$(P',Q') \in B$.
\end{enumerate}
$P$ and $Q$ are \emph{system bisimilar},
$P \sim_s Q$ if they are in a system
bisimulation.
\end{definition}

The results that held for HYPE also hold for stochastic HYPE, as
dealing with stochastic events in the proofs is straightforward.
Hence, system bisimulation is a congruence for Prefix, Choice and
Parallel, and if two uncontrolled systems have the
same set of prefixes, and are put in cooperation with the same
controller, then the two controlled systems are bisimilar. System
bisimulation can be lifted to the model level and congruence can
be shown for stochastic HYPE model product.  
As these are all straightforward
modifications of existing proofs, we omit presenting them formally
for reasons of space. The reader is referred to \cite{HYPE-journal}
for further details.

System bisimulation is a static bisimulation in the sense that it
does not consider the detailed behaviour of the model. It considers
which events can occur, matches on them and also matches strictly
on state. However, for stochastic events it requires exact matching
of rates, rather than of the overall rate to processes with the
same behaviour.  In the next section, we consider a less strict and
more useful equivalence.

\subsection{An equivalence based on stochastic bisimulation}

We now consider a bisimulation that takes conditions on dynamics
into account and relaxes the strict matching on states.  Furthermore,
we wish to relax the requirements for matching of stochastic
transitions, and move to a definition that is similar to stochastic
bisimulation \cite{Hill96,BuchB95a} where the combined rate to an equivalence
class for each action is considered. For this, we require additional
definitions. The sum in the definition is taken over a multiset.

\begin{definition}
For the transitions $\bigl\langle P_1, \sigma_1 \bigr\rangle
\lsxrightarrow{\:\ssev{a}\:}
\bigl\langle P_2, \sigma_2 \bigr\rangle$ let $\mathop{\mathit{mult}}(\bigl\langle P_1, \sigma_1
\bigr\rangle \lsxrightarrow{\:\ssev{a}\:} \bigl\langle P_2, \sigma_2 \bigr\rangle)$ be the
number of such transitions.
\end{definition}


\begin{definition}
Given a stochastic HYPE controlled system $P = \Sigma \syncstar \mathit{Con}$,
the function $r: \mathcal{F} \times \mathcal{E}_s \times \mathcal{C} \rightarrow \mathbb{R}^+$ is defined
as
\[ r(\cf{P,\sigma},\sev{a},\Sigma \syncstar \mathit{Con}') = \begin{cases}
      \mathit{act}(\sev{a})\cdot\mathop{\mathit{mult}}(\bigl\langle P, \sigma
\bigr\rangle \mlsxrightarrow{\sev{a}} \bigl\langle \Sigma \syncstar \mathit{Con}', \sigma' \bigr\rangle)
 & \text{if\ } \mathit{Con} \xrightarrow{\sev{a}} \mathit{Con}' \\
      0             & \text{otherwise}
      \end{cases}
\]
Furthermore, this function can be extended to sets $C \subseteq \mathcal{C}$,
$r(\cf{P,\sigma},\sev{a},C) = \sum \{ r(\cf{P,\sigma},\sev{a},Q) \mid Q
\in C \}$.
\end{definition}

\begin{definition}
Given $\equiv$, an equivalence relation over states,
an equivalence relation $B \subseteq \mathcal{C} \times \mathcal{C}$
is a \emph{stochastic system bisimulation with respect to $\equiv$} if 
for all $(P,Q) \in B$, for all
$\sigma \equiv \tau$, for all $C \in (\mathcal{F}/B)/\equiv$,
\begin{enumerate}
\item for all $\ev{a} \in \mathcal{E}_d$, 
whenever
\begin{enumerate}
\item $\cf{P,\sigma} \xrightarrow{\ev{a}} \cf{P',\sigma'} \in C$, there exists
$\cf{Q',\tau'} \in C$ such that $\cf{Q,\tau} \xrightarrow{\ev{a}}
\cf{Q',\tau'}$. 
\item $\cf{Q,\tau} \xrightarrow{\ev{a}} \cf{Q',\tau'} \in C$, there exists
$\cf{P',\sigma'} \in C$ such that $\cf{P,\sigma} \xrightarrow{\ev{a}}
\cf{P'\!,\sigma'}$.
\end{enumerate}
\item for all $\sev{a} \in \mathcal{E}_s$, 
$r(\cf{P,\sigma},\sev{a},C) = r(\cf{Q,\tau},\sev{a},C)$. 
\end{enumerate}
$P$ and $Q$ are \emph{stochastic system bisimilar with respect to $\equiv$},
$P \sim_s^\equiv Q$ if they are in a stochastic system
bisimulation with respect to $\equiv$.
\end{definition}

Note that even in the case that $\equiv$ is equality, stochastic system
bisimulation with respect to $\equiv$ is less
strict than isomorphism over the instantaneous transitions.  Next,
we consider under which conditions $\sim_s^\equiv$ is a congruence.
We need two definitions to characterise the interaction of $\equiv$
and functions used in the operational semantics.

\begin{definition}
An equivalence $\equiv$ over states \emph{is preserved by
updates} if $\sigma \equiv \tau$ implies that
$\sigma[\iota \mapsto (r,I)]\equiv\tau[\iota \mapsto (r,I)]$.
\end{definition}

\begin{definition}
An equivalence relation $\equiv$ over states \emph{is preserved by $\Gamma$}
if $\sigma_i \equiv \tau_i$ for $i=1,2,3$ implies that
$\Gamma(\sigma_1,\sigma_2,\sigma_3) \equiv
\Gamma(\tau_1,\tau_2,\tau_3)$.  
\end{definition}

\begin{theorem}
\label{congruence}
$\sim_s^\equiv$ is a congruence for Influence, Choice and 
Cooperation, if $\equiv$ is preserved by updates and $\Gamma$.
\end{theorem}
\begin{proof} Please refer to Appendix~\ref{sec:congruence}.
\end{proof}

This theorem describes the conditions on the equivalence over states
for congruence. Both preservation by updates and by $\Gamma$ are
strong conditions, but as we will see later in this section, not
always necessary.

Because of the specific form of well-defined stochastic HYPE models,
congruence with respect to some operators is less important.  It
is not possible to obtain a well-defined stochastic HYPE model by
applying Prefix with Influence or Choice to an existing well-defined
stochastic HYPE model. However Cooperation and Prefix are used to
construct a controlled system from an uncontrolled system and
controller, hence congruence can be used to prove further results
as in the next theorem.

\begin{theorem}
\label{thm:equivcon}
Given an uncontrolled system $\Sigma$ and two controllers
such that $\mathit{Con}_1 \sim_s^{\equiv} \mathit{Con}_2$ and let $\equiv$
be preserved by $\Gamma$ then $\Sigma \syncstar \ev{init}.Con_1
\sim_s^{\equiv} \Sigma \syncstar \ev{init}.Con_2$ \end{theorem}
\begin{proof} By congruence.  \end{proof}

Next, we introduce a specific equivalence over states, and prove
that it gives the same ODEs for models that are stochastically
system bisimilar with respect to it.

\begin{definition} Two states are equivalent, $\sigma \doteq \tau$,
when for all $V \in \mathcal{V}$ and $f(\mathcal{W})$, $\mathsf{sum}(\sigma,V,f(\mathcal{W})) =
\mathsf{sum}(\tau,V,f(\mathcal{W}))$ where \[\mathsf{sum}(\sigma,V,f(\mathcal{W})) = \sum \{\hspace*{-2.8pt}|\, r \mid
\mathop{\mathit{iv}}(\iota)=V, \sigma(\iota)=(r,I(\mathcal{W})), f(\mathcal{W})=\assign{I(\mathcal{W})}\,|\hspace*{-2.7pt}\}\]
\end{definition}

This equivalence abstracts from individual influences by requiring
that the sum of strengths for each variable and influence type is
preserved. It is not preserved by updates or $\Gamma$; however, as
will be seen in the example section, it still provides a useful
equivalence.  This is because, for certain models, it is the case
that $\sigma \doteq \tau$ implies $\Gamma(\sigma,\sigma',\sigma'')
\doteq \Gamma(\tau,\tau',\tau'')$ even though $\sigma' \not\doteq
\tau'$ and $\sigma'' \not\doteq \tau''$. This can be achieved by
imposing additive conditions on the rates in a model for specific
events.  To illustrate this, consider the subcomponents
\begin{eqnarray*}
A_i & \rmdef & \ev{a}{\,:\,}(k_i,r_i,I).A_i + \ev{init}{\,:\,}(k_i,0,I).A_i \\
B_i & \rmdef & \ev{a}{\,:\,}(j_i,s_i,I).B_i + \ev{init}{\,:\,}(j_i,t,I).B_i
\end{eqnarray*}
with $\mathop{\mathit{iv}}(k_i) = X = \mathop{\mathit{iv}}(j_i)$. After the $\ev{init}$ event, we
have states $\sigma_i = \{ k_i \mapsto (0,I), j_i \mapsto (t,I)\}$
and therefore $\mathsf{sum}(\sigma_i,X,I) = t$. Clearly, $\sigma_1 \doteq \sigma_2$.
However, after an $\ev{a}$ event, we have states $\tau_i = \{ k_i
\mapsto (r_i,I), j_i \mapsto (s_i,I)\}$ and $\mathsf{sum}(\tau_i,A_i \syncstar
B_i,I) = r_i + s_i$.  Hence $\tau_1 \doteq \tau_2$ if and only if
$r_1 + s_1 = r_2 + s_2$. This does not require that $r_1 = r_2$ and
$s_1 = s_2$ which are the conditions required for equivalent states
for $A_1$ and $B_1$, and $A_2$ and $B_2$.

Next, we wish to lift stochastic system bisimulation with respect to an
equivalence,  from controlled system level to model level, both to
consider congruence of model product and to impose conditions on
the elements of the tuples.

\begin{definition}
\label{def:systemBisim}
Let $(P_i,\,\mathcal{V},\,\mathit{IN},\,\mathit{IT},\mathcal{E}_d,\mathcal{E}_s,\,\Ac,
\mathit{ec},\,\mathop{\mathit{iv}},\,\mathit{EC},\,\mathit{ID})$ for $i=1,2$ 
be two stochastic HYPE models. They are \emph{stochastic system bisimilar
with respect to an equivalance $\equiv$ over states}
(denoted $P_1 \thicksim^{\equiv}_\mathbf{sm} P_2$) if $P_1 \sim^{\equiv}_s P_2$.
\end{definition}

Let the notation $P_\sigma$ denote the collection of ODEs for model
$P$ in state $\sigma$. The next results shows that models that are
stochastic system bisimilar with respect to $\doteq$ have the same ODEs.

\begin{theorem}
\label{thm:doteqODES}
Given two stochastic HYPE models
$(P,\,\mathcal{V},\,\mathit{IN},\,\mathit{IT},\mathcal{E}_d,\mathcal{E}_s,\,\Ac,
\mathit{ec},\,\mathop{\mathit{iv}},$ $\mathit{EC},\,\mathit{ID})$ and $(Q,\,\mathcal{V},\,\mathit{IN},\linebreak\mathit{IT},\mathcal{E}_d,\mathcal{E}_s,\,\Ac,
\mathit{ec},\,\mathop{\mathit{iv}},\,\mathit{EC},\,\mathit{ID})$, if
$P \thicksim_\mathbf{sm}^{\doteq} Q$, then
for every configuration $\cf{P',\sigma_1} \in \mathop{\mathrm{ds}}(P)$ and
$\cf{Q',\sigma_2} \in \mathop{\mathrm{ds}}(Q)$ such that $P' \thicksim_\mathbf{sm}^{\doteq} 
Q'$, $P_{\sigma_1} = Q_{\sigma_2}$.
\end{theorem}
\begin{proof} Please refer to Appendix~\ref{sec:equiv}.
\end{proof}

We can also define bisimulation at the TDSHA level and relate the
stochastic HYPE bisimulation to that of the bisimulation over TDSHA.
In Appendix \ref{sec:bisimforTDSHA}, we show that two stochastic HYPE models
that are stochastic system bisimilar with respect to ${\doteq}$
have TDSHAs that are bisimilar but the converse does not necessarily
hold.


\section{Example revisited: equivalence}

\begin{figure}[t]
{\renewcommand{\arraystretch}{1.20}
$$\begin{array}{rcl}
\mathit{Con}_D & \rmdef & D \parallel C_e \parallel C_f \\
\\
D       & \rmdef & \ev{check}_1.D_{1,1} + \ev{check}_2.D_{1,2} \\
D_{1,i} & \rmdef & \sev{remove}_i.D_{2,i} \\
D_{2,i} & \rmdef & \ev{assem}_i.D + \ev{check}_i.D_{3,i} \\
D_{3,i} & \rmdef & \ev{assem}_i.D_{1,i+1} + \sev{remove}_i.D_{4} \\
D_{4}   & \rmdef & \ev{assem}_1.D_{2,2} + \ev{assem}_2.D_{2,1} \\
\end{array}$$}

\caption{Controller for the assembly system with a single controller
for the two assembly machines (addition is modulo 2)}
\label{fig:Dcontroller}
\end{figure}

We can now consider equivalence in the context of the manufacturing
system. We can define
$\mathit{Con}_D$, a composite controller for two machines and access to the pool
as given in Figure \ref{fig:Dcontroller}, to replace the controllers $C_1$,
$C_2$ and $C_m$.

First, we show that ${\mathit{Sys} \syncstar \ev{init}.\mathit{Con}} \sim_s^{\equiv}
{\mathit{Sys} \syncstar \ev{init}.\mathit{Con}_D}$ for a suitable $\equiv$. This
can be done by Theorem \ref{thm:equivcon} and requires that a
suitable equivalence relation be identified over the two controllers.
We can ignore states inf configurations since they are not affected
by the events in the controller. The relation $B$ that follows is
a stochastic system bisimulation with respect to $=$, and illustrates that
therefore $(C_1 \parallel C_2) \syncstar C_m)
\sim_s^{=} D$ and by congruence $\mathit{Con} \sim_s^{=} Con_D$,
since equality preserves $\Gamma$.
Hence ${\mathit{Sys} \syncstar
\ev{init}.\mathit{Con}} \sim_s^{=} {\mathit{Sys} \syncstar \ev{init}.\mathit{Con}_D}$.
\begin{eqnarray*}
B & = & \bigl\{ 
((C_1 \parallel C_2) \syncstar C_m, D), 
    ((C''_1 \parallel C''_2) \syncstar C_m, D_{4}), \\
& & ((C'_1 \parallel C_2) \syncstar C'_m, D_{1,1}), 
    ((C_1 \parallel C'_2) \syncstar C''_m, D_{1,2}), \\
& & ((C''_1 \parallel C_2) \syncstar C_m, D_{2,1}), 
    ((C_1 \parallel C''_2) \syncstar C_m, D_{2,2}), \\
& & ((C''_1 \parallel C'_2) \syncstar C_m, D_{3,1}), 
    ((C'_1 \parallel C''_2) \syncstar C_m, D_{3,2})
\bigr\}
\end{eqnarray*}
Figure~\ref{fig:SimCon2} shows the average for these two assembly systems
over 5000 simulations. The similarity between these averages suggest that
our definition of bisimulation has captured the similarities between the
two systems.

We note here that the stochastic HYPE system $\mathit{Assembler}$ (which uses the
five
subcontrollers) is well-behaved,
according to Definition \ref{def:well-behaved}. This holds because
each component of the controller is of the form required by Proposition
\ref{prop:well-behavedness}, and contains a stochastic event
($\sev{remove}_i$). To show that $\mathit{Assembler}_D$ (which uses three
subcontrollers one of which is 
$\mathit{Con}_D$) is well-behaved, we can
simply invoke bisimilarity of the two systems, noticing that
well-behavedness, being a condition on sequences of events, is
preserved by bisimulation.

As mentioned above, the subcontrollers $(C_1 \parallel C_2) \syncstar C_m$
and $D$ both ensure that only one machine has access to the pool at a
time. Another approach is to use only the controller $(C_1 \parallel
C_2)$ and modify the event conditions for each machine. We add a new
variable $M$ and redefine some event conditions.

\begin{eqnarray*}
\mathit{ec}(\ev{init}) & = & (true,\;\rsdefa{P}{P_0} \:\wedge\: \rsdefa{T_1}{0}
\:\wedge\: \rsdefa{T_2}{0} \:\wedge\: \rsdefa{B}{B_0} \:\wedge\:
\rsdefa{M}{0}) \\
\mathit{ec}(\ev{check}_i) & = & (P\geq n_i \:\wedge\: M=0,\; \rsdefa{M}{1}) \\
\mathit{ec}(\sev{remove}_i) & = & (\mathit{ttime}_i,\;\rsdefa{P}{P\!-\!n_i} \:\wedge\:
\rsdefa{T_i}{0} \:\wedge\: \rsdefa{M}{0}) \\
\mathit{ec}(\ev{assem}_i) & = & (T_i \geq \mathit{atime}_i,\; \rsdefa{B}{B\!+\!m_i}) 
\end{eqnarray*}
This modifies the system from one where mutual exclusion is determined
by explicit sequencing of actions in the controller to one where a
semaphore is used. Since the definition of stochastic system
bisimulation has a requirement for events conditions to be equal for
each event, we can no longer directly use this. Instead we can reason
about the behaviour of the controllers from each system and show that
the beahviour are the same, taking into account the different event
conditions. We can then use Theorem~\ref{thm:equivcon} to argue for
the stochastic system bisimilarity of the two controlled systems.

We wish to show that $C_1 \parallel C_2$ with these event conditions
has the same behaviour as $(C_1 \parallel C_2) \syncstar C_m$. The
labelled transition system of $C_1 \parallel C_2$ has nine derivatives
(including itself).
Eight of these derivatives have the same derivatives in the labelled
transition systems of $(C_1 \parallel C_2) \syncstar C_m$, if we
drop the contribution by derivatives of $C_m$. The derivative that
does not appear is $C'_1 \parallel C'_2$ where each controller has
performed an $\ev{check}_i$ action and can then perform a $\ev{remove}_i$
action.  If we can show that the value of the variable $M$ ensures
that this derivative cannot occur, then it is possible to contruct an
isomorphism between the two LTSs and also to conclude that the two
systems (one using $(C_1 \parallel C_2) \syncstar C_m$ as the
controller, and one using $C_1 \parallel C_2$ with additional
modification to the new variable $M$) are stochastic system bisimilar
with respect to equality. To see that the derivative $C'_1 \parallel
C'_2$ is not reachable from the initial state, consider that if the
first machine has performed $\ev{check}_1$ then $M$ now has value
1, and it is not possible for the second machine to perform
$\ev{check}_1$ because it has the guard that requires $M$ to be
zero. $M$ is only reset to zero when the event $\sev{remove}_1$
ends. Hence it is not possible for $C_2$ to become $C'_2$ until
$C'_1$ has become $C''_1$. This ensures $C'_1 \parallel C'_2$
cannot happen. A similar argument applies if the second machine
executes $\ev{check}_2$ first. Thus the bisimilarity is established.


Next, we consider the use of the bisimulation $\sim_s^{\doteq}$
where by using $\doteq$ we require that flows in state have a weaker
form of equivalence than equality. We illustrate this through
allowing different arrival rates for the feeds into the pool.  Let
$Sys_{a_1,a_2,a_3}$ be the system such that \begin{eqnarray*} \mathit{Feed}_1
& \rmdef & \ev{init}{\,:\,}(p_1,a_1,\mathit{const}).\mathit{Feed}_1 +
		 \ev{full}{\,:\,}(p_1,0,\mathit{const}).\mathit{Feed}_1 \\
\mathit{Feed}_2 & \rmdef & \ev{init}{\,:\,}(p_2,a_2,\mathit{const}).\mathit{Feed}_2 +
		 \ev{full}{\,:\,}(p_2,0,\mathit{const}).\mathit{Feed}_2  \\
\mathit{Feed}_3 & \rmdef & \ev{init}{\,:\,}(p_3,a_3,\mathit{const}).\mathit{Feed}_3 +
		 \ev{full}{\,:\,}(p_3,0,\mathit{const}).\mathit{Feed}_3
\end{eqnarray*} Then ${\mathit{Sys}_{a_1,a_2,a_3} \syncstar \ev{init}.\mathit{Con}_1}
\sim_s^{\doteq} {\mathit{Sys}_{b_1,b_2,b_2} \syncstar \ev{init}.\mathit{Con}_1}$
whenever $a_1 + a_2 + a_3 = b_1 + b_2 + b_3$. The ODE that describes
the change in the amount of items in the pool is $dP/dt =  a_1 +
a_2 + a_3 = k$ and $\mathsf{sum}(\sigma,P,\mathit{const}) = \mathsf{sum}(\tau,P,\mathit{const})$.
Hence as long as the systems being compared have the same value for
$k$, the behaviour will be bisimilar. Replacing the $Feed_i$ by a
single subcomponent \begin{eqnarray*} \mathit{Feed} & \rmdef &
\ev{init}{\,:\,}(p,a,\mathit{const}).\mathit{Feed} +
		 \ev{full}{\,:\,}(p,0,\mathit{const}).\mathit{Feed}
\end{eqnarray*} with $\mathop{\mathit{iv}}(p)=P$, also provides a bisimilar model
with respect to $\doteq$ as long as $a=k$.



\begin{figure}
\begin{center}
\begin{tabular}{cc}
\hspace*{-0.9cm}
\includegraphics[width=8.5cm]{S10K.pdf}
&
\hspace*{-0.75cm}
\includegraphics[width=8.5cm]{D10K.pdf}
\end{tabular}
\end{center}
\caption{Average values for $P$ and $B$ for $\mathit{Assembler}$ over 10000
simulations
(left) and average values for $P$ and $B$ for $\mathit{Assembler}_D$ over 10000
simulations
(right) using the same parameters as in Figure~\ref{fig:parrun}.}
\label{fig:SimCon2}
\end{figure}

\section{Related work}

As described previously \cite{HYPE-journal}, HYPE takes a finer
grained, less monolithic approach than the other process algebras
for hybrid systems \cite{BergBM:05a,BeekBMRRS:06a,RounRS:03a,CuijCR:05a}
because it enables the modelling of individual flows. \cite{KhadK:06a}
compares these other process algebras based on the train gate
controller example and for each of these process algebras, complete
ODEs appear in the syntactic description of the system.  Likewise,
hybrid automata \cite{HenzH:96a} require explicit definition of
ODEs, and are less compositional than HYPE since the product of
hybrid automata, requires disjoint variable sets. By contrast, HYPE
product \cite{HYPE-journal} does not require this and hence product
construction allows shared variables in each component and hence
richer behaviour through interaction. Other compositional hybrid
formalisms such as \textsc{Charon} \cite{AlurAGLS:06b}, \textsc{Shift}
\cite{DeshDGV:96a}, and HyCharts \cite{GrosGS:02a} do not map
directly to hybrid automata, compared to HYPE.  Hybrid action systems
\cite{RonkRRS:03a}, Hybrid Interacting Maude \cite{FadlFOA:11a} and
bond graphs \cite{Paynter61,Cuijpers08} are other approaches that
take a less monolithic approach.

Stochastic HYPE retains the fine grained approach to modelling
flows, and the more expressive product construction, as well as
adding the ability to model stochastic events. To the best of our
knowledge, it is the only process algebra with these modelling
capabilities.

Other formalisms for stochastic hybrid modelling include TDSHA
\cite{PA:Bortolussi:2010:HybridDynamicsStochProg:TCS,BorP11}, PDMP
\cite{Davis93}, stochastic hybrid automata (SHA) \cite{BujoBL:04a}
and the recent stochastic extension of UPPAAL \cite{DaviDDLLMPS:12a}.
Stochastic HYPE provides a language for reasoning about some of these
formalisms since these are the semantic objects described by the
stochastic HYPE syntax. TDSHA were developed to provide a
transition-focussed approach to PDMP and hence providing a more
consistent manner of treating the three different types of behaviour
considered: continuous, stochastic and instantaneous behaviour.

Research into making stochastic hybrid systems modelling compositional
has been considered \cite{StruSJS:03a},
where Communicating Piecewise Deterministic Markov Processes (CPDP)
are introduced.  This is an automata-based formalism which models
a system as interacting automata.  Their chosen level of abstraction
is somewhat lower level than ours, comparable with TDSHA. In CPDP,
as in stochastic HYPE, instantaneous transitions may be triggered
either by conditions of the continuous variables (boundary-hit
transitions) or by the expiration of a stochastically determined delay
(Markov transitions).  Interaction between automata is based on
\emph{one-way} synchronisation: in each interaction one partner is
active while the other is passive. In stochastic HYPE, instead, all
components may be regarded as active with respect to each transition
in which they participate, as activation conditions are specified
uniquely in the model. Components participating in a discrete
transition are determined by the construction of the stochastic
HYPE model, where the synchronisation set $L$ in $\!\!{\smsync{L}}\!\!$
specifies which actions must be shared.

The synchronization mechanics of CPDP has been extended by
\cite{StruSS:05b}, introducing an  operator which  exploits all
possible interactions of active and passive actions. \cite{StruSS:05a}
define a notion of bisimulation for both PDMPs and CPDPs and show
that if CPDPs are bisimilar then they give rise to bisimilar PDMPs.
Furthermore the equivalence relation is a congruence with respect
to the composition operator of CPDPs. The definition of bisimilarity
presented in Appendix~\ref{sec:bisimforTDSHA} is based on these
definitions for PDMPs and CPDPs.

Stochastic HYPE has been used to model various systems, including
an orbiter \cite{BortBGH:11a}, a stochastic version of the train
gate \cite{HYPE-journal} and opportunistic networks \cite{BortBGH:12a}.
More recently, a large scale model of ZebraNet \cite{JuanJOWMPR:02a},
a wildlife monitoring project where individual zebra are nodes in
an opportunistic network, has been developed which includes
2-dimensional animal movement, animal behaviour, and different
opportunistic network protocols \cite{FengF:12a}. Stochastic HYPE
has also been used to provide hybrid semantics for the biological
process algebra Bio-PEPA \cite{GalpG:13a} where reactions are treated
stochastically or deterministically depending on species quantities
or reaction rates.

\section{Conclusion}

In this paper we have presented an extension of the hybrid process
algebra HYPE, in which non-urgent events fire at exponentially
distributed random times.  Although syntactically the modification
that this entails is minimal with respect to the original version
of HYPE, the semantics of the language is considerably enriched and
quantified analysis of the modelled behaviour becomes available
purely based on the model.  The stochastic hybrid systems obtained
from stochastic HYPE models fall in the class of Piecewise Deterministic
Markov Processes (PDMP) \cite{Davis93}.  Here we have shown how
such a semantics can be derived through the intermediary of
Transition-Driven Stochastic Hybrid Automata (TDSHA)
\cite{PA:Bortolussi:2010:HybridDynamicsStochProg:TCS}.  The mapping
that we present from stochastic HYPE to TDSHA differs from that
originally presented in \cite{BortBGH:11a}, as we work at the level
of the labelled transition system generated by the operational
semantics.  Nevertheless we show that the obtained TDSHA in each
case is equivalent (in Appendix~\ref{sec:SOSmapping}).  We have discussed a
number of bisumulation equivalences for stochastic HYPE with a
particular focus on notions that are pragmatic and coincide with
intuitive ideas of when behaviours coincide.  Furthermore we have
illustrated these with a case study based on an assembly line.

\paragraph{Acknowledgments:}
This work is partially supported by the EU project QUANTICOL, 600708.

\bibliographystyle{../eptcs}
