Dmi abstraction edits

notes/abstraction/abstraction.tex

@@ -2,7 +2,7 @@
 
 Abstraction involves defining which state variables to group.  These in turn allow us to combine transitions and their rates.  For example, we can abstract the stratified \Petrinet{} from the previous section by specifying the set of state variables $\{(S, \{(vac=F)\}), (S, \{(vac=T)\})\}$ to abstract.  The result is a state variable $(S, \{(vac=F),(vac=T)\})$.  After replacing the abstracted state variables with the result, the transitions $inf_{vac=T}$ and $inv_{vac=F}$ become isomorphic (differing only in parameters in their rates).  We replace those transitions with an abstract transition.
 
-The rates of the stratified transitions are $S_{vac=F}I\beta_{vac=F}$ and $S_{vac=T}I\beta_{vac=T}$.  We preserve to total flow through these transitions by defining the rate of the abstract transition as the sum $S_{vac=F}I\beta_{vac=F}+S_{vac=T}I\beta_{vac=T}$.  If we let $\beta_*$ denote an aggregate parameter (to be replaced by a lower or upper bound in the next section) and substitute it for $\beta_{vac=F}$ and $\beta_{vac=T}$, then $S_{vac=F}I\beta_*+S_{vac=T}I\beta_* = (S_{vac=F}+S_{vac=T})I\beta_* = SI\beta_*$.  In this manner, we can abstract transitions that were previously stratified.
+The rates of the stratified transitions are $S_{vac=F}I\beta_{vac=F}$ and $S_{vac=T}I\beta_{vac=T}$.  We preserve to total flow through these transitions by defining the rate of the abstract transition as the sum $$S_{vac=F}I\beta_{vac=F}+S_{vac=T}I\beta_{vac=T}$$.  If we let $\beta_*$ denote an aggregate parameter (to be replaced by a lower or upper bound in the next section) and substitute it for $\beta_{vac=F}$ and $\beta_{vac=T}$, then $$S_{vac=F}I\beta_*+S_{vac=T}I\beta_* = (S_{vac=F}+S_{vac=T})I\beta_* = SI\beta_*$$.  In this manner, we can abstract transitions that were previously stratified.
 
 \begin{definition} (State Abstraction)
 	The state abstraction operator $A_X((\Theta, \Omega), \{(x,g_1), \ldots, (x, g_N)\})$ defines a new set of states $X^A = X \backslash \{(x,g_1), \ldots, (x, g_N)\} \cup \{(x, g)\}$, where $g = \bigcup_{i=1}^N g_i$.  The set of abstract model state variable vertices $V_X^A$ is defined as $V_X^A=V_X\backslash \{v\in V_X|({\cal X}(v), {\cal D}(v)) \in \{(x,g_1), \ldots, (x, g_N)\} \} \cup \{v^A \}$, where $({\cal X}^A(v^A), {\cal D}^A(v^A)) = (x, g)$ and $({\cal X}^A(v), {\cal D}^A(v)) = ({\cal X}(v), {\cal D}(v))$ for all $v \in V_X^A\backslash \{v^A\}$.
@@ -25,7 +25,7 @@
 
 
 \begin{definition} (Edge Abstraction)
-	The abstract edges are defined as $E^A = E\backslash\{e \in E(v_z) | z \in Z_1' \cup \ldots Z_M'\} \cup \{(v_{xg}, v_z)| z \in Z^A\backslash Z, ((x, g), z, (x_b, g_b)) \in T(z)\} \cup \{(v_z, v_{xg})| z \in Z^A\backslash Z, ((x_a, g_a), z, (x, g)) \in T(z)\}$.
+	The abstract edges are defined as $$E^A = E\backslash\{e \in E(v_z) | z \in Z_1' \cup \ldots Z_M'\} \cup \{(v_{xg}, v_z)| z \in Z^A\backslash Z, ((x, g), z, (x_b, g_b)) \in T(z)\} \cup \{(v_z, v_{xg})| z \in Z^A\backslash Z, ((x_a, g_a), z, (x, g)) \in T(z)\}.$$
 \end{definition}
 
 \begin{definition} (Transition Rate Abstraction)
@@ -154,6 +154,6 @@
 expresses the transition rates in terms of the base states.  As such, the
 abstraction compresses the \Petrinet{} graph structure, but at the cost of
 expanding the expressions for transition rates. Moreover, the transition
-rates refer to state variables and parameters (e.g., $\beta_{vac=T}$, $S_{vac=T}$, $\beta_{vac=F}$,  ans $S_{vac=F}$) that are not expressed
+rates refer to state variables and parameters (e.g., $\beta_{vac=T}$, $S_{vac=T}$, $\beta_{vac=F}$,  and $S_{vac=F}$) that are not expressed
 directly by the abstract \Petrinet{} and semantics (e.g., as $\beta$ and $S$), and by extension, the gradient. We address this in the next section.
 

notes/abstraction/background.tex

@@ -10,7 +10,7 @@
 \begin{definition}
 	Let $E(v) = \edgesIn{}(v) \cup \edgesOut{}(v)$, and for all $e = (v, v') \in E$,
 	$e \in \edgesOut{}(v)$ and  $e \in \edgesIn{}(v')$.
-	We define the \emph{parent} and \emph{child} of an edge, $\parent( (v, v') ) = v$ and $\child( (v, v') ) = v'$.
+	We define the \emph{parent} of an edge $$\parent( (v, v') ) = v$$  and \emph{child} of an edge $$\child( (v, v') ) = v'$$
 	We define the parents (descendents) of a vertex, $\parents(v)$ ($\children(v)$) as the set of parents (children) of the edges in and out, respectively.
 	Further, % for all $(v, v') \in E$,
 	if $v \in
@@ -48,15 +48,15 @@
 
 We facilitate this by annotating the state description with discrete variables.
 Each assignment to the discrete variables describes a different subpopulation.
-For example, $(I, \{(vac=T,
-	gender=M, age=child)\})$ and $(I, \{(vac=T, gender=F, age=child)\})$ refer to
+For example, $$(I, \{(vac=T,
+	gender=M, age=child)\})$$ and $$(I, \{(vac=T, gender=F, age=child)\})$$ refer to
 the number of infected, vaccinated male children and female children, respectively.  We could
 capture fully-specified discrete states by indexing the state variables to give, for example,
 $I_{TMC}$, and $I_{TFC}$.
 However, later when construct abstractions, it will be more convenient to refer to \emph{sets} of assignments to the discrete variables, of the form $(x, g)$, where $g$ is a \emph{set} of assignments to the discrete variables.
 For example, if gender is not relevant to infection
-rates, we could define the set of susceptible, vaccinated children as $(S, g)$, where $g=
-	\{(vac=T, gender=M, age=child), (vac=T, gender=F, age=child)\}$.
+rates, we could define the set of susceptible, vaccinated children as $(S, g)$, where $$g=
+	\{(vac=T, gender=M, age=child), (vac=T, gender=F, age=child)\}$$.
 
 \begin{definition}
 	The ODE semantics $\Theta$ of the \Petrinet{} $\Omega$ defines a tuple $(P, D, X,
@@ -155,7 +155,7 @@
 defining \Petrinet{} stratification, as described in the following section.
 For example, in Figure \ref{fig:sir_model}, flow through the ``infection'' node is entirely from susceptible to infected, S $\rightarrow$ inf $\rightarrow$ I in the figure.  There is also an edge from infected to infection (I $\rightarrow$ inf), but this reflects only the influence of the number already infected on the rate of flow from S to I: there is no flow backwards.
 
-\textcolor{red}{I edited the above a little bit.  Did I get it right?}
+% \textcolor{red}{I edited the above a little bit.  Did I get it right?}
 
 %  We drop
 % the vertex terminology by assuming the following:

notes/abstraction/main.tex

@@ -61,11 +61,11 @@
 
 \section{Introduction}
 
-We describe methods to stratify (refine) and de-stratify (abstract) \Petrinets{} for compartmental models.  The motivation for abstracting a \Petrinet{} is to reduce its size, which can become exponential in the number of stratified variables.  Reducing the size of the model can have a significant impact on runtime, while it may still be possible to answer useful queries (more efficiently) with an abstracted model.  The following sections include background (defining the models), a description of stratification and abstraction, an approach to bound the abstracted models (or to perform parameter synthesis directly in a simulator), and then a comparison of simulation results for several variations of a baseline model that applies stratification, bounding, and abstraction.  
+We describe methods to stratify (refine) and de-stratify (abstract) \Petrinets{} for compartmental epidemiology models.  The motivation for abstracting a \Petrinet{} is to reduce its size, which can become exponential in the number of stratified variables.  Reducing the size of the model can have a significant impact on runtime, while it may still be possible to answer useful queries (more efficiently) with an abstracted model.  The following sections include background (defining the models), a description of stratification and abstraction, an approach to bound the abstracted models (or to perform parameter synthesis directly in a simulator), and then a comparison of simulation results for several variations of a baseline model that applies stratification, bounding, and abstraction.  
 
-\rpg{In the above, do we need a definition of compartmental models?  If this goes only to people who know a little about epidemiology, probably not, but if it goes to a CS audience, maybe we do.  If so, we could add it to background; LMK if you want me to do this.}
-
-\textcolor{blue}{Note from Drisana: I think if we don't provide a definition, maybe saying "compartmental epidemiology models" would get the point across}
+%\rpg{In the above, do we need a definition of compartmental models?  If this goes only to people who know a little about epidemiology, probably not, but if it goes to a CS audience, maybe we do.  If so, we could add it to background; LMK if you want me to do this.}
+%
+%\textcolor{blue}{Note from Drisana: I think if we don't provide a definition, maybe saying "compartmental epidemiology models" would get the point across}
 
 \section{Background}
 \input{background}

notes/abstraction/stratification.tex

@@ -13,7 +13,7 @@
 	The state stratification operator $St_{XG}((x, g), (g_1, \ldots, g_N))$ maps a state variable $(x, g)$ and partition $(g_1, \ldots, g_N)$ of $g$ to a set of states $\{(x, g_1), \ldots, (x, g_N)\}$.  The stratified state variables and annotations are defined so that $X' = X$ and $D'=D$.  If $({\cal X}(v_{xg}),{\cal D}(v_{xg})) = (x, g)$ in $\Omega, \Theta$ for some $v_{xg} \in V$, then in $\Omega', \Theta'$, the state vertex mapping is $({\cal X}'(v_{xg_i}),{\cal D}'(v_{xg_i})) = (x, g_i)$ for each $g_i$ and some $v_{xg_i} \in V'$.  For all other states, ${\cal X}' = {\cal X}$ and ${\cal D}' = {\cal D}$.  The stratified vertices define $V' = V\backslash\{v_{xg}\} \cup \{v_{xg_i} | (x, g_i) \in X'\}$.
 \end{definition}
 
-For example, the result of $St_{XG}((S, \{(vac=T), (vac=F)\}), (\{(vac=T)\}, \{(vac=F)\}))$ is $\{(S, \{(vac=T)\}), (S, \{(vac=F)\})\}$.  In the stratified model, ${\cal X}'$ and ${\cal D}'$ map the unique vertices $v_{ST}$ and $v_{SF}$ to these respective state variables.
+For example, the result of $$St_{XG}((S, \{(vac=T), (vac=F)\}), (\{(vac=T)\}, \{(vac=F)\}))$$ is $$\{(S, \{(vac=T)\}), (S, \{(vac=F)\})\}$$.  In the stratified model, ${\cal X}'$ and ${\cal D}'$ map the unique vertices $v_{ST}$ and $v_{SF}$ to these respective state variables.
 
 \begin{definition} (Stratified Transition Components)
 	The  stratification operator $St_{T}((x, g), (g_1, \ldots, g_N), t_k)$ for a transition component $t_k \in T(z)$ and $z \in Z$ defines a set of transition components $T_k'(z)$.  If $t_k = ((x_a, g_a), z, (x_b, g_b))$, then $T_k'(z)$ corresponds to one of the following: