\section{Introduction}
Wireless networked controlled systems (WNCS's) represent a class of spatially distributed control systems for which the feedback loops are closed via shared communication components possessing limited bandwidth. Several advantages of WNCS’s, such as the ease of maintenance and the flexibility of implementation, make them attractive to industrial environments. Meanwhile, WNCS's are burdened with characteristics, such as limited battery life and communication bandwidth. Under these circumstances, the resource over-utilization caused by (traditional) periodic implementations, the so-called time-driven control (TDC), makes such implementations less appealing for WNCS's.

To address the aforementioned issues, control researchers have proposed \emph{event-driven control} (EDC) strategies that are aperiodic, such as \emph{event-triggered control} (ETC) \cite{Tabuada} and \emph{self-triggered control} (STC) \cite{Velasco}. In EDC strategies, the core idea relies on the fact that the dynamics of the control system during the inter-sample interval determine the next sampling instant to attenuate the usage of resources, particularly the communication bandwidth. In these strategies, control task executions only happen when a pre-specified condition is violated. Such condition is called the \emph{triggering mechanism} (TM). It is derived based on stability and/or performance of the closed-loop system. On the other hand, the \emph{schedulability} of ETC strategies, due to their aperiodic nature, is more arduous compared to TDC strategies. In fact, in TDC strategies, the control and scheduler designs are naturally decoupled via the (pre-defined) fixed sampling period. This phenomenon is called the \emph{separation-of-concerns} in the real-time systems community \cite{dijkstra1982role}. It is worth mentioning that ETC strategies are almost always equipped with a \emph{minimum inter-execution time} (MIET) to prevent the occurrence of \emph{Zeno} behavior in the sampling process. This quantity can be technically used in the synthesis of task scheduling. However, it is a conservative approximation of the lower bound on all the possible generated sampling periods. Thus, such synthesis does not make use of the beneficiary characteristics of ETC strategies in an efficient manner. To address this shortcoming, researchers have proposed another class of approaches, the so-called \emph{co-design} approaches. In this class, the problem of controller and scheduler synthesis for real-time systems is tackled in a unified framework, see e.g.\ feedback modification to task attributes \cite{Buttazzo1998,Caccamo2000}, \cite{Lu2002,Cervin2004}, anytime controllers \cite{Bhattacharya2004,Fontanelli2008_short}, and event-based control and scheduling \cite{AlAreqi2013,AlAreqi2014}. Recently, alternative to the unified frameworks mentioned above, \cite{Arman2015,ArmanTCoN} have proposed a decoupling framework to capture the sampling behavior of LTI systems with ISS-based TM's using timed safety automata (TSA's).

Generally speaking, TSA is a simplified version of timed automaton (TA) \cite{alur1996timing,henzinger1994symbolic}. It is a powerful tool to model the timing behavior of real-time systems for scheduling purposes since its reachability analysis is decidable \cite{alur1994theory,larsen1997uppaal}. In this study, following the same path as in \cite{Arman2015,ArmanTCoN}, we propose a framework to capture the sampling behavior of perturbed LTI systems with the $\mathcal{L}_2$-based TM proposed by \cite{WangLem2009}. We show that the derived TSA $\varepsilon$-approximately simulates the sampling behavior of the $\mathcal{L}_2$-based ETC system. It is evident that such characterizations can be analyzed independently for scheduling purposes, thus providing a scalable and versatile event-triggered WNCS design procedure.

\section{Preliminaries}
$\mathbb{R}^n$ denotes the $n$-dimensional Euclidean space, $\mathbb{R}^+$ denotes the positive reals. $\mathbb{N}_0$ is the set of nonnegative integers, and $\mathbb{IR}^+$ is the set of all closed intervals $[a,b]$ such that $a,b \in \mathbb{R}^+$ and $a \leq b$. For any set $S$, $2^S$ denotes the set of all subsets of $S$, i.e.\ the power set of $S$. $\mathcal{S}_{m \times n}$ and $\mathcal{S}_n$ are the set of all $m \times n$ real-valued matrices and the set of all $n \times n$ real-valued symmetric matrices, respectively. For a matrix $M$, $M \preceq 0$ (or $M \succeq 0$) means $M$ is a negative (or positive) semidefinite matrix and $M\prec 0$ ($M \succ 0$) indicates $M$ is a negative (positive) definite matrix. $\mathcal{S}_n^+$ is the cone of all $n\times n$ symmetric positive definite matrices. $\lfloor x \rfloor$ indicates the largest integer not greater than $x \in \mathbb{R}$. $|y|$ and $\|M \|$ denote the Euclidean norm of a vector $y \in \mathbb{R}^n$ and the Frobenius norm of a matrix $M \in \mathcal{S}_{m \times n}$, respectively. For a matrix $M \in \mathcal{S}_n$, $\lambda(M)$ and $\lambda_{\max}(M)$ denote the set of eigenvalues and the largest eigenvalue of $M$. Consider two sets $X,Y\subseteq\mathbb{R}^n$, their Minkowski sum is given by $X\oplus Y:= \{x+y| x\in X\mbox{~and~}y \in Y\}$. We state the following known results that will be used in Subsection~\ref{sec::control_pre}.

\begin{mylemma}{(\cite{GuKhCh2003})}
\label{lem_1}
For any real matrices $E$, $G$ and real symmetric positive definite matrix $P$, with compatible dimensions,
\begin{equation*}
EG+G^TE^T \preceq EPE^T+G^TP^{-1}G.
\end{equation*}
\end{mylemma}

\begin{mylemma}{(\cite{Loan1977})}
\label{lem_2}
For all $A \in \mathcal{S}_{n\times n}$, if $\mu(A)= \max \{ \mu \in \mathbb{R}| \; \mu\in \lambda\left(\frac{A^T +A}{2}\right) \}$, then, $|e^{At}| \leq e^{\mu(A)t}$.
\end{mylemma}

\begin{myproposition}{(Jensen Inequality \cite{GuKhCh2003})}
\label{prop_1} For any matrix $M \in \mathcal{S}_m^+$ with constant entries, scalar $\gamma > 0$, vector function $\omega: [0,\gamma] \rightarrow \mathbb{R}^m$ such that the integrations concerned are well defined, then:
\begin{equation*}
\gamma \int_0^{\gamma} \omega^T(\beta)M\omega(\beta)d\beta \geq \left(\int_0^{\gamma}\omega(\beta)d\beta\right)^T M \int_0^{\gamma}\omega(\beta)d\beta.
\end{equation*}
\end{myproposition}

\subsection{$\mathcal{L}_2$-Based ETC System:}
\label{sec::control_pre}
In this subsection, an overview of the ETC strategy proposed by \cite{WangLem2009} along with a new result (see Theorem \ref{theor_1}) are presented. Consider a sampled-data system that is given by:
\begin{equation}
\label{eq_1}
\begin{array}{l}
\dot{\xi}(t)=A \xi (t)+B \nu (t)+E \omega (t), \forall t \in [0, \tau(x)),\\
\xi(0)=x,
\end{array}
\end{equation}
where $ \xi(t) \in \mathbb{R}^n$, $\nu(t) \in \mathbb{R}^m$, $\omega(t) \in \mathbb{R}^p$, $\tau(x)$ denotes the sampling period associated with $\xi(0)$, and $A$, $B$, and $E$ have compatible dimensions. The control law is implemented in a sample-and-hold manner as follows:
\begin{equation}
\label{eq_2}
\nu(t)=-Kx.
\end{equation}

Furthermore, assume that the disturbance $\omega$ is a vanishing type disturbance \cite{WangLem2009}, i.e.,
\begin{equation}
\label{eq_3}
\exists W \geq0 \mbox{~such that~} |w(t)|^2 \leq W |x|^2, \forall t \in [0, \tau(x)).
\end{equation}

Denote by $\epsilon$, the error signal endured by the system (\ref{eq_1})-(\ref{eq_2}), $\epsilon (t) = x - \xi_x (t)$ where $\xi_x(t)$ is the solution of (\ref{eq_1}). Reformulating (\ref{eq_1}), the evolution of state and error signals can be rewritten in a compact form as follows:
\begin{equation}
\label{eq_5}
\xi_x (t) = \Lambda (t) x+\Omega (t)
\end{equation}
and
\begin{equation}
\label{eq_7}
\epsilon (t)= \left( I- \Lambda(t)\right) x - \Omega(t)
\end{equation}
where
\begin{equation}
\label{eq_6}
\left\{
\begin{array}{l}
\Lambda (t) = I+\int_0^t e^{As}ds(A-BK),\\
\Omega (t) = \int_0^t e^{A(t-s)}E \omega(s) ds.
\end{array} \right.
\end{equation}

Assume that there exists a quadratic Lyapunov function $V(\xi)=\xi^TP\xi$ such that $P$ is the solution to the Algebraic Riccati Equation (ARE) given by:
\begin{equation}
\label{are_1}
PA+A^TP-Q+R=0
\end{equation}
where
\begin{equation}
\label{are_2}
Q=PBB^TP,\quad R=\frac{1}{\gamma^2}PEE^TP,\quad \gamma>0.
\end{equation}

The existence of $V$ guarantees that the system (\ref{eq_1}) with the full-state feedback $\nu(t)=-K\xi(t)=-B^TP\xi(t)$ is finite-gain $\mathcal{L}_2$ stable from $\omega$ to $(x^T,u^T)$ with an induced gain less than $\gamma$ \cite{WangLem2009}. Then, the state-dependent TM, proposed by \cite{WangLem2009}, is given by:
\begin{equation}
\label{eq_8}
\tau(x):=\inf\{t>0|\;\epsilon^T(t)M\epsilon(t) \geq x^T N x\}
\end{equation}
where
\begin{equation}
\label{eq_9}
\begin{array}{lll}
M=(1-\beta^2)I+PBB^TP,\\
N=\frac{1}{2}(1-\beta^2)I+PBB^TP,
\end{array}
\end{equation}
and $\beta >0$ is a user-defined scalar related to the TM (\ref{eq_8}).

\begin{mytheorem}
\label{theor_1}
Consider the system (\ref{eq_1})-(\ref{eq_2}) with the triggering mechanism (\ref{eq_8}). Assume there exist a scalar $\mu$ and a symmetric matrix $\Psi$ such that
\begin{equation}
\label{eq_17_1_a}
\mu\geq0,\quad \Psi\succ0,\quad M+\Psi\preceq \mu I,
\end{equation}
\begin{equation}
\label{eq_17_1_b}
\Phi(t) \succeq 0,
\end{equation}
where
\begin{equation}
\label{eq_17_123}
\Phi(t) = \left[
\begin{array}{lr}
\Phi_1(t) & \Phi_2(t)\\
\Phi_3(t) & \Phi_4(t)
\end{array}
\right],
\end{equation}
\begin{equation*}
\begin{array}{l}
\Phi_1(t)=(\Lambda(t)-I)^T M (\Lambda(t)-I)\\
\quad\quad\;\;+t W \mu\lambda_{\max}(E^TE)d_A(t)I- N,\\
\Phi_2(t)=\Phi_3^T(t)=(\Lambda(t)-I)^T M^T,\\
\Phi_4(t)=- \Psi,
\end{array}
\end{equation*}
are satisfied. Then, the sampling period $\tau(x)$ generated by (\ref{eq_8}) is lower bounded by:
\begin{equation}
\label{eq_17_4}
\tau'(x):=\inf\{t>0|\;\Phi(t)\succeq0 \}.
\end{equation}
\end{mytheorem}

\begin{proof}
Substitute (\ref{eq_7}) into (\ref{eq_8}). Then, the TM (\ref{eq_8}) can be rewritten by:
\begin{equation}
\label{eq_17}
\tau(x)=\min\{t>0|\; \mathcal{F}_{\omega}(x,t) \geq0\}, \forall x \in \mathbb{R}^n,
\end{equation}
where
\begin{equation}
\label{eq_10}
\begin{array}{ll}
\mathcal{F}_{\omega}(x,t)&= x^T [(\Lambda(t)-I)^TM(\Lambda(t)-I)- N]x \\
&+ x^T(\Lambda(t)-I)^T M \Omega(t)+\Omega^T(t) M (\Lambda(t)-I)x \\
&+ \Omega^T(t)M\Omega(t).
\end{array}
\end{equation}

Let $\lambda_{\max}^A$ denote $\lambda_{\max}(A+A^T)$ for the sake of compactness. Using Lemma \ref{lem_1} the terms that are dependent on both $x$ and $\Omega(t)$ in $\mathcal{F}_{\omega}(x,t)$ can be decoupled into:
\begin{equation}
\label{eq_11}
\begin{array}{l}
x^T(\Lambda(t)-I)^T M \Omega(t)+\Omega^T(t) M (\Lambda(t)-I)x \leq \\
\Omega^T(t) \Psi \Omega(t) + x^T(\Lambda(t)-I)^T M \Psi^{-1} M (\Lambda(t)-I)x,
\end{array}
\end{equation}
where $\Psi=\Psi^T \succ0$. Then, it follows that:
\begin{equation}
\label{eq_13}
\begin{array}{l}
\begin{array}{ll}
\Omega^T(t)(M+\Psi)\Omega(t)&
\end{array}\\
\begin{array}{l}
\leq \mu (\int_0^t e^{A(t-s)}E\omega(s)ds)^T (\int_0^t e^{A(t-s)}E\omega(s)ds) \\
 \mbox{(assuming~}M+\Psi\preceq \mu I\mbox{~and~}\mu\geq 0\mbox{)}\\
\leq t \mu \int_0^t e^{(t-s)\lambda_{\max}^A}\omega^T(s)E^TE\omega(s)ds\\
 \mbox{(using Jensen's inequality and Lemma \ref{lem_2})}\\
\leq t W \mu \lambda_{\max}(E^TE) (\int_0^t e^{\lambda_{\max}^A(t-s)}ds) |x|^2\\
 \mbox{(using (\ref{eq_3}))}\\
=tW\mu \lambda_{\max}(E^TE)d_A(t)x^Tx,
\end{array}
\end{array}
\end{equation}
where
\begin{small}
\begin{equation}
\label{eq_14}
d_A(t)=\left\{
\begin{array}{l}
\frac{1}{\lambda_{\max}^A}(e^{\lambda_{\max}^At}-1),\lambda_{\max}^A\neq 0 \\
t,\lambda_{\max}^A= 0.
\end{array}\right.
\end{equation}
\end{small}

Based on the aforementioned procedure, one concludes that:
\begin{equation}
\label{eq_15}
\mathcal{F}_{\omega}(x,t) \leq x^T \Theta(t)x
\end{equation}
where
\begin{equation}
\label{eq_16}
\begin{array}{ll}
\Theta(t)&= (\Lambda(t)-I)^T(M+M \Psi^{-1} M)(\Lambda(t)-I)\\
&+tW\mu \lambda_{\max}(E^TE)d_A(t)I- N.
\end{array}
\end{equation}

Then, we employ the Schur complement in order to transform (\ref{eq_16}) into (\ref{eq_17_123}). Note that (\ref{eq_16}) is not linear in $\Psi$ while (\ref{eq_17_123}) is linearly dependent on $\Psi$. Considering (\ref{eq_15}), since $\Phi(t)\succeq 0$ implies $x^T \Theta(t)x\geq 0$ by the Schur complement, it follows that $\tau(x)\geq \tau'(x)$. This concludes the proof.
\end{proof}

Thus, Theorem \ref{theor_1} enables us to avoid the unknown behavior of perturbation $\omega(t)$ in analyzing the sampling begavior of (\ref{eq_8}). However, it is still intractable to use (\ref{eq_17_4}) for the analysis since it has to be checked for an infinite number of instants $t$ and it clearly lacks any insight on how the state $x$ at the sampling instant affects the sampling period $\tau(x)$.

\subsection{Systems and Relations}
\label{sec:modelprel-systems}
In what follows, we review some notions from the field of system theory to formally characterize the outcome of the proposed framework. Let $Z$ be a set and $Q\subseteq Z\times Z$ be an equivalence relation on $Z$. Then, $[z]$ denotes the equivalence class of $z \in Z$ and $Z/Q$ denotes the set of all equivalence classes. A metric (or a distance function) $d:Z \times Z \rightarrow \mathbb{R} \cup \{ + \infty\}$ on $Z$ satisfies, $\forall x, y, z \in Z$: i) $d(x,y)=d(y,x)$, ii) $d(x,y)=0 \leftrightarrow x=y$, and ii) $d(x,y) \leq d(x,z)+d(y,z)$. The ordered pair $(Z,d)$ is said to be a metric space.

\begin{mydefinition}{(Hausdorff Distance \cite{ewald2012combinatorial})}
\label{def_haus}
Assume $X$ and $Y$ are two non-empty subsets of a metric space $(Z,d)$. The Hausdorff distance $d_{H}(X,Y)$ is given by:
$$\max \{ \underset{x \in X}{\sup} \underset{y \in Y}{\inf} d(x,y), \underset{y \in Y}{\sup} \underset{x \in X}{\inf} d(x,y) \}.$$
\end{mydefinition}

It follows that the ordered pair $(\mathbb{IR}^+,d_H)$ is a metric space. Now, we introduce some concepts from system theory and particularly a modified notion of \emph{quotient system} adopted from \cite{Arman2015} (see e.g.\ \cite{Tabuada2009} for the traditional definition).
\begin{mydefinition}[System {\cite{Tabuada2009}}]
\label{def_sys}
A system is a sextuple $(X,X_0,U,\rTo,Y,H)$ consisting of:
\begin{itemize}
\item a set of states $X$;
\item a set of initial states $X_0 \subseteq X$;
\item a set of inputs $U$;
\item a transition relation $\rTo \subseteq X \times U \times X$;
\item a set of outputs $Y$;
\item an output map $H: X \rightarrow Y$.
\end{itemize}
\end{mydefinition}

When the set of outputs $Y$ of a system is endowed with a metric, it is called a metric system. An autonomous system is a system for which the cardinality of its input set is at most one.

\begin{mydefinition}[Approximate Simulation Relation {\cite{Tabuada2009}}]
\label{def_asr}
Consider two metric systems $S_a=(X_{a},X_{a0},U_{a},\rTo_{a},Y_a,H_{a})$ and $S_b=(X_{b},X_{b0},U_{b},\rTo_{b},Y_b,H_{b})$ with $Y_a=Y_b$, and let $\varepsilon \in \mathbb{R}^+_0$, where $\mathbb{R}^+_0$ represents  the set of nonnegative real numbers. A relation $R \subseteq X_a \times X_b$
is an $\varepsilon$-approximate simulation relation from $S_a$ to $S_b$ if the following three
conditions are satisfied:
\begin{enumerate}
\item $\forall x_{a0} \in X_{a0}, \exists x_{b0} \in X_{b0} \text{ such that } (x_{a0},x_{b0}) \in R$;
\item $\forall (x_a,x_b) \in R, \text{ we have } d(H_a(x_a),H_b(x_b)) \leq \varepsilon$;
\item $\forall (x_a,x_b) \in R, (x_a,u_a,x'_a) \in \underset{a}{\rTo}$ in $S_a$  $\exists (x_b,u_b,x'_b) \in \underset{b}{\rTo}$ in $S_b$ satisfying $(x'_a,x'_b) \in R$.
\end{enumerate}
We say that $S_b$ $\varepsilon$-approximately simulates $S_a$, denoted by $S_a\preceq^\varepsilon_\mathcal{S} S_b$, if there exists an $\varepsilon$-approximate simulation relation $R$ from $S_a$ to $S_b$.
\end{mydefinition}

\begin{mydefinition}[Power Quotient System {\cite{Arman2015}}]
\label{def_quo}
Let $S=(X,X_0,\varnothing,\rTo,Y,H)$ be an autonomous system and $R$ be an equivalence relation on $X$.
The power quotient of $S$ by $R$, denoted by $S_{/R}$, is the autonomous system $(X_{/R},X_{/R,0},\varnothing,\rTo_{/R},Y_{/R},H_{/R})$ consisting of:
\begin{itemize}
\item $X_{/R}=X/R$;
\item $X_{/R,0}=\{ x_{/R} \in X_{/R} | x_{/R} \cap X_0 \neq \varnothing \}$; %
\item $(x_{/R},u,x'_{/R}) \in \rTo_{/R}$ if $\exists (x,u,x') \in \rTo$ with $x \in x_{/R}$ and $x' \in x'_{/R}$;
\item $Y_{/R} \subset 2^Y$;
\item $H_{/R}(x_{/R})=\underset{x \in x_{/R}}{\cup}H(x)$.
\end{itemize}
\end{mydefinition}

\begin{mylemma}[{\cite{Arman2015}}]
\label{lem_app_sim}
Let $S$ be an autonomous metric system, $R$ be an equivalence relation on $X$, and let the autonomous metric system $S_{/R}$ be the power quotient system of $S$ by $R$. For any
$$\varepsilon\geq\max_{\substack{x \in x_{/R} \\ x_{/R}\in X/R}} d(H(x),H_{/R}(x_{/R})),$$
with $d$ the Hausdorff distance over the set $2^Y$,
$S_{/R}$ $\varepsilon$-approximately simulates $S$,
i.e.\ $S\preceq^\varepsilon_\mathcal{S} S_{/R}$.
\end{mylemma}

Now, we appropriately modify Definition \ref{def_quo} and Lemma \ref{lem_app_sim} for the case that one can construct an over approximation of the power quotient system, namely $\bar{S}_{/R}$.

\begin{mydefinition}{(Approximate Power Quotient System {\cite{ArmanTCoN}})}
\label{def_quo_app}
Let $\mathcal{S}=(X,X_0,U,\rTo,Y,H)$ be a system, $R$ be an equivalence relation on $X$, and $\mathcal{S}_{/R}=(X_{/R},X_{/R,0},U_{/R},\rTo_{/R},Y_{/R},H_{/R})$ be the power quotient of $\mathcal{S}$ by $R$. An approximate power quotient of $\mathcal{S}$ by $R$, denoted by $\bar{\mathcal{S}}_{/R}$, is a system $(X_{/R},X_{/R,0},U_{/R},\rTo_{\bar{/R}},\bar{Y}_{/R},\bar{H}_{/R})$ such that, $ \underset{\bar{/R}}{\rightarrow} \supseteq \underset{/R}{\rightarrow}$, $\bar{Y}_{/R} \supseteq Y_{/R} $, and $\bar{H}_{/R}(x_{/R}) \supseteq H_{/R}(x_{/R})$, $\forall x_{/R}\in X_{/R}$.
\end{mydefinition}

\begin{mycorollary}[{\cite{ArmanTCoN}}]
\label{cor_1}
Let $S$ be a metric system, $R$ be an equivalence relation on $X$, and let the metric system $\bar{S}_{/R}$ be the approximate power quotient system of $S$ by $R$. For any
$$\varepsilon\geq\max_{\substack{x \in x_{/R} \\ x_{/R}\in X_{/R}}} d(H(x),\bar{H}_{/R}(x_{/R})),$$
with $d$ the Hausdorff distance over the set $2^Y$,
$\bar{S}_{/R}$ $\varepsilon$-approximately simulates $S$,
i.e.\ $S\preceq^\varepsilon_\mathcal{S} \bar{S}_{/R}$.
\end{mycorollary}

\subsection{Timed Safety Automaton}

In what follows, we present a formal definition for TSA. A TSA \cite{Alur1994} is a directed graph extended with real-valued variables (called clocks) that model the logical clocks. We define $C$ as a set of finitely many clocks. Clock constraints are used to restrict the behavior of the automaton. A clock constraint is a conjunctive formula of atomic constraints of the form $x \bowtie n$ or $x - y \bowtie n$ for $x,y \in  C$, $\bowtie \in \{\leq,<,=,>,\geq\}$ and $n \in \mathbb N$. We use $\mathcal B(C)$ to denote the set of clock constraints.

\begin{mydefinition}\label{def:ta}(Timed Safety Automaton \cite{henzinger1994symbolic})
A \emph{timed safety automaton} $\mathsf{TSA}$ is a sextuple $(L,\ell_0,\mathsf{Act},C,E,\mathsf{Inv})$ where:
\begin{itemize}
\item $L$ is a set of finitely many locations (or vertices);
\item $\ell_0 \in L$ is the initial location;
\item $\mathsf{Act}$ is the set of actions;
\item $C$ is a set of finitely many real-valued clocks;
\item $E \subseteq L \times \mathcal B(C) \times \mathsf{Act} \times 2^{C} \times L$ is the set of edges;
\item $\mathsf{Inv} : L \to \mathcal B(C)$ assigns invariants to locations.
\end{itemize}

The location invariants are restricted to constraints of the form: $c \leq n$ or $c < n$ where $c$ is a clock and $n$ is a natural number.
\end{mydefinition}

\subsection{Problem Statement}
\label{sec:abs-problem}
Consider the system
$S=(X,X_0,\varnothing,\rTo,Y,H)$:
\begin{itemize}
\item $X=\mathbb{R}^n$;
\item $X_0=\mathbb{R}^n$;
\item $(x,x') \in \rTo$ iff $\xi_x(\tau(x))=x'$ given by \eqref{eq_1}-\eqref{eq_2}, and \eqref{eq_8};
\item $Y \subset \mathbb{R}^+$
\item $H: \mathbb{R}^n \rightarrow \mathbb{R}^{+}$ where $H(x)=\tau(x)$.
\end{itemize}
The output of the above system generates all possible sequences of inter-sample intervals of the concrete system \eqref{eq_1}-\eqref{eq_2} with the TM~\eqref{eq_8}.

\begin{myproblem}
\label{prob_1}
Provide a construction of power quotient systems $S_{/\mathcal{P}}$ of systems $S$ as defined above.
\end{myproblem}

Based on Definition \ref{def_quo}, we propose to construct the system
$S_{/\mathcal{P}}=(X_{/\mathcal{P}},X_{/\mathcal{P},0},\varnothing, \underset{/\mathcal{P}}{\rTo},Y_{/\mathcal{P}},H_{/\mathcal{P}})$
where
\begin{itemize}
\item $X_{/\mathcal{P}}= \mathbb{R}_{/\mathcal{P}}^n:= \{\mathcal{R}_1,\dots,\mathcal{R}_q \}$;
\item $X_{/\mathcal{P},0}=\mathbb{R}_{/\mathcal{P}}^n$;
\item $(x_{/\mathcal{P}},x'_{/\mathcal{P}}) \in
\underset{/\mathcal{P}}{\rTo} $ if $\exists x \in x_{/\mathcal{P}}$, $\exists x' \in x'_{/\mathcal{P}}$ such that $\xi_x(H(x))=x'$ as determined by \eqref{eq_1}-\eqref{eq_2};
\item $Y_{/\mathcal{P}} \subset 2^Y \subset \mathbb{IR}^{+}$, where $\mathbb{IR}^{+}$ represents the set of closed intervals $[a,b]$ such that $0 < a \leq b$;
\item \small{$H_{/\mathcal{P}}(x_{/\mathcal{P}})= [\underset{x \in x_{/\mathcal{P}}}{\min}H(x),\underset{x \in x_{/\mathcal{P}}}{\max}H(x)]:=[\ubar{\tau}_{x_{/\mathcal{P}}},\bar{\tau}_{x_{/\mathcal{P}}}]$}.
\end{itemize}

The equivalence relation $\mathcal{P}$ on $\mathbb{R}^n$ partitions the state space of $S$ (i.e. the ETC system) into the set $X_{/\mathcal{P}}$ with a finite cardinality. However, since the exact construction of $\mathcal{S}_{/\mathcal{P}}$ is in general impossible, we construct instead $\bar{\mathcal{S}}_{/\mathcal{P}}$ (see Definition~\ref{def_quo_app}). Later on, it will be shown that the constructed $\bar{S}_{/\mathcal{P}}$ is equivalent to a TSA.

\section{Abstractions of event-triggered LTI systems}
\label{sec:abs}

In this section, we introduce the framework to solve Problem~\ref{prob_1} in the following order: 1) a proper definition of an equivalence relation $\mathcal{P}$ on $\mathbb{R}^n$, 2) a tractable approach to compute the output map $\bar{H}_{/\mathcal{P}}$ and its corresponding output set $\bar{Y}_{/\mathcal{P}}$, and 3) a reachability-based analysis to derive the discrete transitions among abstract states $x_{/\mathcal{P}}$.

\subsection{State set}
\label{sec:abs-construction-states}

The type of state set construction approach mainly relies on an intuitive observation from \eqref{eq_15}.

\begin{myremark}
\label{rem_1}
Consider that the right-hand side of (\ref{eq_15}) is used to analyze the sampling behavior of (\ref{eq_17}) instead of $\mathcal{F}_{\omega}(x,t)$. Then, the sampling periods of all states, located on a line that passes through the origin excluding the origin itself, are lower bounded by the same sampling period, i.e.\ $\tau'(x)=\tau'(\lambda x)$, $\forall \lambda \neq 0$.
\end{myremark}

It follows that a proper approach to abstract the state space is via partitioning it into a finite number of convex polyhedral cones (pointed at the origin) $\mathcal{R}_s$ where $s \in \{1,\dots,q \}$ and $\bigcup_{s=1}^q \mathcal{R}_s = \mathbb{R}^n$. This state space abstraction technique is proposed by \cite{Fiter2012}, dividing each of the angular spherical coordinates of $x \in \mathbb{R}^n$: $\theta_1, \dots,\theta_{n-2} \in [0,\pi]$, $\theta_{n-1} \in [-\pi,\pi]$ into $\bar{m}$ (not necessarily equidistant) intervals resulting in $q=\bar{m}^{(n-1)}$ conic regions. Furthermore, since the term $x^T \Theta(t)x$ is quadratic in $x$, it is sufficient to only analyze half of the state space (e.g.\ by taking $\theta_{n-1} \in [0,\pi]$). Thus, the equivalence relation $\mathcal{P}$ to construct the abstraction is given by:
$$
(x,x')\in\mathcal{P} \Leftrightarrow \exists\, s \in  \{1,\dots,q \}\, \text{s.t.}\,  x,x'\in \mathcal{R}_s,
$$
where $q$ is the number of equivalence classes. Hence, the equivalence classes of $\mathcal{P}$ are defined by polyhedral cones pointed at the origin given by $\mathcal{R}_s=\{ x \in \mathbb{R}^2| \; x^T Q_s x \geq 0 \},\; Q_s\in \mathcal{S}_2$ whenever $n=2$ or $\mathcal{R}_s=\{ x \in \mathbb{R}^n| \; E_s x \geq 0\}$, $E_s \in \mathcal{S}_{n\times p}$ otherwise.

\subsection{Output Map}
\label{sec:abs-construction-output}

In this subsection, we present how to construct $\bar{H}_{/\mathcal{P}}$ and $\bar{Y}_{/\mathcal{P}}$. For all $x \in \mathcal{R}_s$, the output $\bar{Y}_{/\mathcal{P}}=\bar{H}_{/\mathcal{P}}(x)$ is equal to the time interval $[\ubar{\tau}_s,\bar{\tau}_s]$ indicating $\tau(x) \in [\ubar{\tau}_s,\bar{\tau}_s]$. We make use of the polytopic embedding technique proposed by \cite{hetel2006stabilization}. In the space of real matrices, a sequence of convex polytopes is constructed around the matrix $\Phi(t)$. Doing so replaces the evaluation of (\ref{eq_17_4}) at infinitely many instants $t$ by the evaluation of $\Phi_{\kappa,s}$ at finitely many vertices in the sequence of polytopes generated by $\Phi_{\kappa,s}$. Assume a scalar $\sigma>0$ denoting a time instant for which the TM \eqref{eq_8} is enabled in the whole state space, i.e.\ $\Phi(t)\succeq 0$. Consider $N_{\text{conv}}+1$ is the number of vertices employed to define the polytope containing $\Phi(t)$ in a given time interval,  and $l\geq1$ denotes the number of time subdivisions considered in the time interval $[0,\sigma]$.

\begin{mylemma}
\label{lem3}
Let  $s \in \{1,\dots,q\}$. Consider a time instant $\ubar{\tau}_s \in (0,\sigma]$, a scalar $\mu$ and a symmetric matrix $\Psi$ satisfying (\ref{eq_17_1_a}). If $ \ubar{\Phi}_{(i,j),s}  \preceq 0$ holds $\forall(i,j) \in \mathcal{K}_s=(\{0,\dots,N_{\text{conv}} \} \times \{0,\dots,\lfloor \frac{\ubar{\tau}_s l}{\sigma} \rfloor \})$, then, it follows that $ \Phi(t)\preceq 0$, $\forall t \in [0,\ubar{\tau}_s]$ with $\Phi$ defined in \eqref{eq_17_123} and
\begin{equation*}
\label{eq_34}
\ubar{\Phi}_{(i,j),s}=\tilde{\ubar{\Phi}}_{(i,j),s}+\eta I
\end{equation*}
\begin{equation}
\label{eq_24}
\tilde{\ubar{\Phi}}_{(i,j),s}=\left\{
\begin{array}{lll}
\Sigma_{k=0}^i \hat{\ubar{\Phi}}_{(i,j),s} (\frac{\sigma}{l})^k &,&j<\lfloor \frac{\ubar{\tau}_s l}{\sigma} \rfloor \\
\Sigma_{k=0}^i \hat{\ubar{\Phi}}_{(i,j),s} (\ubar{\tau}_s-j\frac{\sigma}{l})^k&,&j=\lfloor \frac{\ubar{\tau}_s l}{\sigma} \rfloor,
\end{array}\right.
\end{equation}
\begin{equation}
\label{eq_24_1}
\begin{array}{l}
\hat{\ubar{\Phi}}_{(0,j),s}=\left[ \begin{array}{lr}
\ubar{L}_{0,j} & \check{\Pi}_j^T M^T\\
M \check{\Pi}_j & -\Psi
\end{array}\right],\\
\hat{\ubar{\Phi}}_{(k\geq 1,j),s}=\left[ \begin{array}{lr}
\ubar{L}_{k,j} & \hat{\Pi}_j^T \frac{(A^{k-1})^T}{k!} M^T\\
M \frac{A^{k-1}}{k!} \hat{\Pi}_j & 0
\end{array}\right],
\end{array}
\end{equation}
and
\begin{equation}
\label{eq_25}
\ubar{L}_{0,j}=\check{\Pi}_j^T M \check{\Pi}_j- N+\tilde{L}_{0,j}
\end{equation}
with
\begin{equation}
\label{eq_26}
\tilde{L}_{0,j}=\left\{
\begin{array}{l}
W\mu \frac{\lambda_{\max}(E^TE)}{\lambda_{\max}^A}(j\frac{\sigma}{l})(e^{\lambda_{\max}^Aj\frac{\sigma}{l}}-1)I \\
\quad \mbox{for~}\quad\lambda_{\max}^A\neq 0, \\
W\mu \frac{\lambda_{\max}(E^TE)}{\lambda_{\max}^A}(j\frac{\sigma}{l})^2I\\
\quad \mbox{for~}\quad\lambda_{\max}^A= 0,
\end{array}\right.
\end{equation}
\begin{equation}
\label{eq_27}
\ubar{L}_{1,j}=\check{\Pi}_j^T M \hat{\Pi}_j+ \hat{\Pi}_j^T M \check{\Pi}_j+\tilde{L}_{1,j}
\end{equation}
with
\begin{small}
\begin{equation}
\label{eq_28}
\tilde{L}_{1,j}=\left\{
\begin{array}{l}
W\mu \frac{\lambda_{\max}(E^TE)}{\lambda_{\max}^A}[(j\frac{\sigma}{l})e^{\lambda_{\max}^Aj\frac{\sigma}{l}} \lambda_{\max}^A\\
+e^{\lambda_{\max}^Aj\frac{\sigma}{l}}-1]I \mbox{~ for ~} \lambda_{\max}^A\neq 0, \\
W\mu (2j\frac{\sigma}{l}) \lambda_{\max}(E^TE) I \mbox{~ for ~} \lambda_{\max}^A= 0,
\end{array}\right.
\end{equation}
\end{small}
\begin{equation}
\label{eq_29}
\ubar{L}_{2,j}=\check{\Pi}_j^T M \frac{A}{2!} \hat{\Pi}_j+ \hat{\Pi}_j^T \frac{A^T}{2!} M \check{\Pi}_j+\hat{\Pi}_j^T M\hat{\Pi}_j+\tilde{L}_{2,j}
\end{equation}
with
\begin{small}
\begin{equation}
\label{eq_30}
\tilde{L}_{2,j}=\left\{
\begin{array}{l}
W\mu \frac{\lambda_{\max}(E^TE)}{\lambda_{\max}^A}[(j\frac{\sigma}{l})e^{\lambda_{\max}^Aj\frac{\sigma}{l}} \frac{(\lambda_{\max}^A)^2}{2!}\\+e^{\lambda_{\max}^Aj\frac{\sigma}{l}} \lambda_{\max}^A]I\\
\quad \mbox{~for~}\quad \lambda_{\max}^A\neq 0, \\
W\mu \lambda_{\max}(E^TE)I \quad \mbox{~for~}\quad \lambda_{\max}^A= 0,
\end{array}\right.
\end{equation}
\end{small}
\begin{equation}
\label{eq_31}
\begin{array}{ll}
\ubar{L}_{k\geq3,j}&=\check{\Pi}_j^T M \frac{A^{k-1}}{k!} \hat{\Pi}_j+\hat{\Pi}_j^T \frac{(A^{k-1})^T}{k!} M\check{\Pi}_j\\
&+ \hat{\Pi}_j^T (\Sigma_{i=1}^{k-1} \frac{(A^{i-1})^T}{i!} M\frac{A^{k-i-1}}{(k-i)!}) \hat{\Pi}_j+\tilde{L}_{k,j}
\end{array}
\end{equation}
with
\begin{small}
\begin{equation}
\label{eq_32}
\tilde{L}_{k\geq3,j}=\left\{
\begin{array}{l}
W\mu \frac{\lambda_{\max}(E^TE)}{\lambda_{\max}^A}[(j\frac{\sigma}{l})e^{\lambda_{\max}^Aj\frac{\sigma}{l}} \frac{(\lambda_{\max}^A)^k}{k!}\\
+e^{\lambda_{\max}^Aj\frac{\sigma}{l}} \frac{(\lambda_{\max}^A)^{k-1}}{(k-1)!}]I\\ \quad \mbox{~for~}\quad  \lambda_{\max}^A\neq 0, \\
0 \quad \mbox{~for~}\quad  \lambda_{\max}^A= 0,
\end{array}\right.
\end{equation}
\end{small}
\begin{small}
\begin{equation}
\label{eq_33}
\eta \geq \underset{t' \in [0,\frac{\sigma}{l}],r \in \{0,...,l-1 \}}{\max} \lambda_{\max} \left( \Phi(t'+r\frac{\sigma}{l})-\Sigma_{k=0}^N \hat{\ubar{\Phi}}_{k,r}(t')^k \right),
\end{equation}
\end{small}
and
\begin{equation}
\label{my_etc25}
\begin{array}{l}
\tilde{\ubar{\Phi}}_{(N_{\text{conv}},j)}(t')=\Sigma_{k=0}^{N_{\text{conv}}} \hat{\ubar{\Phi}}_{k,j}(t')^k.
\end{array}
\end{equation}
\end{mylemma}

\begin{proof}
See Appendix.
\end{proof}

Then, using the S-procedure, the following theorem provides an approach to regionally reduce the conservatism involved in the $\ubar{\tau}_s$ estimates obtained from Lemma~\ref{lem3}.

\begin{mytheorem}[Regional Lower Bound Approximation]
\label{them3}
Consider a scalar $\ubar{\tau}_s\in(0, \sigma]$, a scalar $\mu$ and a symmetric matrix $\Psi$ satisfying (\ref{eq_17_1_a}), and matrices $\ubar{\Phi}_{\kappa,s}$, $\kappa=(i,j)\in\mathcal{K}_s$, defined as in Lemma~\ref{lem3}. If there exist scalars $\ubar{\alpha}_{\kappa,s}\geq 0$ (for $n=2$) or symmetric matrices $\ubar{U}_{\kappa,s}$ with nonnegative entries (for $n \geq 3$) such that for all $\kappa\in\mathcal{K}_s$ the following LMIs hold:
\begin{equation}
\label{eq_them_un}
\begin{array}{l}
\left\{\begin{array}{ll}
\ubar{\Phi}_{(i,j),s}+\left[\begin{array}{lr}
\ubar{\alpha}_{(i,j),s} Q_s &0\\
0&0
\end{array}\right]
 \preceq 0 & \mbox{if } n=2,\\
\ubar{\Phi}_{(i,j),s}+\left[\begin{array}{lr}
E_s^{T} \ubar{U}_{(i,j),s} E_s &0\\
0&0
\end{array}\right] \preceq 0  & \mbox{if } n\geq 3,
\end{array}\right.
\end{array}
\end{equation}
then, the inter-sample time \eqref{eq_8} of the system \eqref{eq_1}-\eqref{eq_2} is regionally bounded from below by $\ubar{\tau}_s,\; \forall x \in \mathcal{R}_s$.
\end{mytheorem}

\begin{proof}
See Appendix.
\end{proof}

One can follow a similar approach to find the upper bounds $\bar{\tau}_s$ on the inter-sample times that is outlined in Lemma \ref{lemm_u1} and Theorem \ref{them4}.

\begin{mylemma}
\label{lemm_u1}
Let $s \in \{ 1, \ldots, q \}$. Consider a time instant $\bar{\tau}_s \in [\ubar{\tau}_s,\sigma]$, a scalar $\mu$ and a matrix $\Psi$ satisfying the LMI conditions given in Lemma \ref{lem3}. If
$\bar{\Phi}_{(i,j),s} \preceq 0$ holds $\forall (i,j) \in \mathcal{K}_s=(\{0,\dots,N_{\text{conv}} \} \times \{ \lfloor \frac{\bar{\tau}_s l}{\sigma} \rfloor ,\dots, l-1 \})$,
then, it follows that $ \Phi(t) \succeq 0$, $\forall t \in [\bar{\tau}_s,\sigma]$ with $\Phi$ defined in \eqref{eq_17_123} and
\begin{equation*}
\begin{array}{l}
\bar{\Phi}_{(i,j),s}=-\bar{\tilde{\Phi}}_{(i,j),s}- \eta I,
\end{array}
\end{equation*}
\begin{equation*}
\begin{array}{l}
\bar{\tilde{\Phi}}_{(i,j),s}=\left\{\begin{array}{ll}
\sum_{k=0}^i \; L_{k,j} (\frac{(j+1) \sigma}{l} - \bar{\tau}_s)^k & \text{if}  \; j = \lfloor \frac{\bar{\tau}_s l}{\sigma} \rfloor, \\
\sum_{k=0}^i \; L_{k,j} (\frac{\sigma}{l})^k  & \text{if} \; j > \lfloor \frac{\bar{\tau}_s l}{\sigma} \rfloor,
\end{array}\right.
\end{array}
\end{equation*}
where $L_{k,j}$ are given by \eqref{eq_25}-\eqref{eq_32} and $\eta$ is defined in (\ref{eq_33}).
\end{mylemma}

\begin{proof}
See Appendix.
\end{proof}

\begin{mytheorem}[Regional Upper Bound Approximation]
\label{them4}
Consider a scalar $\bar{\tau}_s\in [\ubar{\tau}_s,\sigma]$, a scalar $\mu$ and a symmetric matrix $\Psi$ satisfying (\ref{eq_17_1_a}), and matrices $\bar{\Phi}_{\kappa,s}$, $\kappa=(i,j) \in \mathcal{K}_s$, defined as in Lemma~\ref{lemm_u1}. If there exist scalars $\bar{\alpha}_{\kappa,s}\geq 0$ (for $n=2$) or symmetric matrices $\bar{U}_{\kappa,s}$ with nonnegative entries (for $n \geq 3$) such that for all $\kappa\in\mathcal{K}_s$ the following LMIs hold:
\begin{equation}
\begin{array}{l}
\left\{\begin{array}{ll}
\bar{\Phi}_{(i,j),s}-\left[\begin{array}{lr}
\bar{\alpha}_{(i,j),s} Q_s &0\\
0&0
\end{array}\right]
 \preceq 0 & \mbox{if } n=2,\\
\bar{\Phi}_{(i,j),s}-\left[\begin{array}{lr}
E_s^{T} \bar{U}_{(i,j),s} E_s &0\\
0&0
\end{array}\right] \preceq 0  & \mbox{if } n\geq 3,
\end{array}\right.
\end{array}
\end{equation}
then, the inter-sample time \eqref{eq_8} of the system \eqref{eq_1}-\eqref{eq_2} is regionally bounded from above by $\bar{\tau}_s,\; \forall x \in \mathcal{R}_s$.
\end{mytheorem}

\begin{proof}
Analogous to the proof of Theorem~\ref{them3}. \end{proof}

\subsection{Transition Relations}
\label{sec:abs-construction-trans}
In order to find all the transitions in $\bar{S}_{/\mathcal{P}}$, it is required to compute the reachable set of each $\mathcal{R}_s$ over the time interval $[\ubar{\tau}_s,\bar{\tau}_s]$. In the sequel, we present how one is able to compute over approximations of the reachable set of each cone by the Minkowski sum of two sets. The evolution of states over this time interval is given by $\xi_x(\tau)=\Lambda(\tau)x+\Omega(\tau)$. Denote by $\mathcal{X}_{[\ubar{\tau}_s,\bar{\tau}_s]} (X_{0,s})$ the reachable set of $X_{0,s}$ during the time interval $[\ubar{\tau}_s,\bar{\tau}_s]$, that is given by:
\begin{equation*}
\{x'\in\mathbb{R}^n\,|\,\exists x\in X_{0,s}, \exists \tau\in [\ubar{\tau}_s,\bar{\tau}_s], x'=\xi_x(\tau)\}.
\end{equation*}

Furthermore, define
\begin{equation*}
\begin{array}{l}
\mathcal{X}^1_{[\ubar{\tau}_s,\bar{\tau}_s]}(X_{0,s})\\
:=\{x'\in\mathbb{R}^n\,|\,\exists x\in X_{0,s}, \exists \tau\in [\ubar{\tau}_s,\bar{\tau}_s], x'=\Lambda(\tau)x\},\\
\mathcal{X}^2_{[\ubar{\tau}_s,\bar{\tau}_s]}(X_{0,s})\\
:=\{x'\in\mathbb{R}^n\,|\,\exists x\in X_{0,s}, \exists \tau\in [\ubar{\tau}_s,\bar{\tau}_s], x'=\Omega(\tau)\}.
\end{array}
\end{equation*}
It follows that:

$\mathcal{X}_{[\ubar{\tau}_s,\bar{\tau}_s]}(X_{0,s}):=\mathcal{X}^1_{[\ubar{\tau}_s,\bar{\tau}_s]}(X_{0,s})\bigoplus\mathcal{X}^2_{[\ubar{\tau}_s,\bar{\tau}_s]}(X_{0,s})$.
\vspace{1mm}

In \cite[Section III.B.3]{Arman2015}, it has been shown that it is enough to consider subsets $X_{0,s}\subset \mathcal{R}_s$ being convex polytopes with each vertex placed on each of the extreme rays of $\mathcal{R}_s$ (excluding the origin) to compute $\mathcal{X}^1_{[\ubar{\tau}_s,\bar{\tau}_s]}(X_{0,s})$. Then, one can effectively compute an over approximation of the reachable set of a polytope under linear time invariants, denoted by $\hat{\mathcal{X}}_{[\ubar{\tau}_s,\bar{\tau}_s]}(X_{0,s})$, see e.g.\ \cite{Chutinan1998}. Furthermore, one has:
\begin{equation*}
\label{eq_reach}
\begin{array}{ll}
\|\Omega(\tau) \|&=\|\int_0^{\tau} e^{A(\tau-s)}E\omega(s)ds \|\\
&\leq \int_0^{\tau} \|e^{A(\tau-s)}E\omega(s) \|ds\\
&\leq \int_0^{\tau}\|e^{A(\tau-s)} \| \|E \| |\omega(s)|ds\\
&W|x | \|E \|\int_0^{\tau} |e^{\mu(A)(\tau-s)}|ds\\
&=\rho(\tau) |x |
\end{array}
\end{equation*}
where $\rho(\tau)= W \|E \|\int_0^{\tau} |e^{\mu(A)(\tau-s)}|ds$. Thus, it follows that $\mathcal{X}^2_{[\ubar{\tau}_s,\bar{\tau}_s]}(X_{0,s})$ can be over approximated by
a second order cone given by:
\begin{equation*}
\begin{array}{l}
\hat{\mathcal{X}}^2_{[\ubar{\tau}_s,\bar{\tau}_s]}(X_{0,s})\\
:=\{ x'\in \mathbb{R}^n| \; \exists x\in X_{0,s}, \exists \tau \in [\ubar{\tau}_s,\bar{\tau}_s],| x'|\leq \rho(\bar{\tau}_s)|x| \}.
\end{array}
\end{equation*}

To compute the transitions in $\bar{S}_{/\mathcal{P}}$, it thus suffices to derive the intersection between the over approximation $\hat{\mathcal{X}}_{[\ubar{\tau}_s,\bar{\tau}_s]}(X_{0,s})$ and all the conic regions $\mathcal{R}_{t}$ where $t\in\{1,\dots,q\}$. To compute transitions, it is required to check whether the following convex feasibility problem for each conic region $\mathcal{R}_{t}$ holds:
\begin{equation}
\mathcal{R}_t\cap\hat{\mathcal{X}}_{[\ubar{\tau}_s,\bar{\tau}_s]}(X_{0,s})\neq\varnothing,
\label{my_etc51}
\end{equation}
which can be solved by existing convex analysis tools. There exists a transition from abstract state $\mathcal{R}_s$ to $\mathcal{R}_t$ in $\bar{S}_{/\mathcal{P}}$ in the case that \eqref{my_etc51} is satisfied.

\subsection{Timed Safety Automata Representation}
\label{sec:abs-construction-ta}
In this subsection, first, we point out the connection between an abstract state $x_{/\mathcal{P}} \in X_{/\mathcal{P}}$ and its corresponding output $y_{/\mathcal{P}} \in \bar{Y}_{/\mathcal{P}}$ \cite{Arman2015}. The system $\bar{S}_{/\mathcal{P}}$:
\begin{enumerate}
\item remains at $x_{/\mathcal{P}}$ during the time interval $[0,\ubar{\tau}_{x_{/\mathcal{P}}})$,
\item possibly leaves $x_{/\mathcal{P}}$ during the time interval $[\ubar{\tau}_{x_{/\mathcal{P}}},\bar{\tau}_{x_{/\mathcal{P}}})$, and
\item is forced to leave $x_{/\mathcal{P}}$ at the time instant $\bar{\tau}_{x_{/\mathcal{P}}}$.
\end{enumerate}

Thus, the semantics of $\bar{S}_{/\mathcal{P}}$ is equivalent to a timed safety automaton given by $\mathsf{TSA} = (L,\ell_0,\mathsf{Act},C,E,\mathsf{Inv})$ where:
\begin{itemize}
\item $L=X_{\bar{/\mathcal{P}}}$;
\item $\ell_0 := \mathcal{R}_s$ such that $\xi(0) \in \mathcal{R}_s$;
\item $\mathsf{Act} = \{*\}$ is an arbitrary symbol;
\item $C=\{c\}$;
\item $E$ is given by all tuples $(\mathcal{R}_s,g,a,r,\mathcal{R}_t)$ such that $(\mathcal{R}_s,\mathcal{R}_t)\in \rTo_{\bar{/\mathcal{P}}}$, $g=\{c | \; c \in [\ubar{\tau}_s, \bar{\tau}_s] \}$, $a=*$, and $r$ is given by $c:=0$;
\item $\mathsf{Inv}(\mathcal{R}_s):=\{c| c \in [0,\bar{\tau}_s]\}, \forall s \in \{1,\dots,q\}$.
\end{itemize}

Finally, in this section, we state the following fact. Although the construction technique presented in this section is offline, it is  exponentially dependent on $n-1$ (where $n$ is the number of states) and hence it is computationally expensive for higher-order systems.

\section{Numerical Example}
We illustrate the theoretical results of this paper in a numerical example. Consider an LTI sytem, used as an example in \cite{Tabuada}, and add a perturbation term $\omega(t)$ as follows:
\begin{equation}
\begin{array}{l}
\dot\xi(t) =
\begin{bmatrix}
0 & 1\\
-2 & 3
\end{bmatrix}
\xi(t) +
\begin{bmatrix}
0 \\ 1
\end{bmatrix}
\nu(t)+
\begin{bmatrix}
0 \\ 1
\end{bmatrix}
\omega(t)
\end{array}
\label{eqn:lti-ex-1}
\end{equation}
with the perturbation bound $W=0.001$. We set the scalars, associated with $\mathcal{L}_2$-based TM's, $\gamma=100$, $\beta=0.25$, see (\ref{are_1})-(\ref{are_2}) and (\ref{eq_8})-(\ref{eq_9}). Then, solving the ARE associated with the $\mathcal{L}_2$ stability, the control update law (implemented in a sample-and-hold fashion) is computed, that is, $ \forall t\in[t_k,t_{k+1})$:
\begin{equation*}
\label{eqn:lti-ex-2}
\nu(t)=-K\xi(t_k)=-[0.2361\quad 6.2367]\xi(t_k),
\end{equation*}
where $t_k$ denotes the sampling instants and $k\in \mathbb{N}_0$. Now, we set the order of polynomial approximation $N_{\text{conv}}=7$, the number of polytopic subdivisions $l=800$, the upper bound of the inter-sample intervals $\sigma=8$, the number of angular sub-divisions $\bar{m}=10$, thus, $q=2\times 10^{(2-1)}=20$. Then, applying the results from Section \ref{sec:abs-construction-output}, we get the precision abstraction of $\varepsilon=6.100$. Compared to the results found in \cite{ArmanTCoN}, the derived $\varepsilon$ is large. However, one must take into account the possible stabilizing effect of disturbance on the dynamics in (\ref{eq_1}) can enlarge the derived $\bar{\tau}_s$ and a more thorough study is due in this regard. In Figure \ref{fig_1}, the derived lower and upper bounds are depicted. It is evident that the derived $\ubar{\tau}_s$ compared to the MIET are less conservative and can be effectively used for scheduling.

\begin{figure
\centering
\includegraphics[width=1\columnwidth]{fig_tau_up.eps}
\includegraphics[clip=true,width=1\columnwidth]{fig_tau_un.eps}
\caption{(Top plot) Upper bounds on regional inter-sample times. (Bottom plot) Lower bounds on regional inter-sample times.}
\label{fig_1}
\end{figure}

Figure \ref{fig_2} represents the conic regions $s$ and the associated $\ubar{\tau}_s$ and $\bar{\tau}_s$ (note that in order to show the lower bounds in a clear manner the lower and upper bounds are depicted, separately).

\begin{figure}[thpb]
\centering
\includegraphics[width=1\columnwidth]{spider.eps}
\caption{The radial distance from the origin of each asterisk indicates the regional lower bound of the indexed cone. Furthermore, in the case of circles, the distance indicates the regional upper bound of the indexed cone minus $6.2\sec$, i.e.\ $\bar{\tau}_s-6.2\sec$ (for the sake of clarity of the figure).}
\label{fig_2}
\end{figure}

Moreover, Figure~\ref{fig_3} represents the simulation of the control system for a simulation time of $15\sec$. It is clear that the bounds derived by the analysis given in Section \ref{sec:abs-construction-output} have been respected by the sampling periods generated by the control system.

\begin{figure}[thpb]
\centering
\includegraphics[width=1\columnwidth]{trig_Seq.eps}
\caption{Schematic representation of validation of lower bounds during the simulation period, the solid line (dashed line) represents the lower bounds on inter-sample intervals  (generated inter-sample intervals during simulation).}
\label{fig_3}
\end{figure}

Figure~\ref{fig_4} depicts the result of applying the procedure introduced in Section \ref{sec:abs-construction-trans}.

\begin{figure}[thpb]
\centering
\includegraphics[width=1\columnwidth]{trans_main.eps}
\caption{Schematic representation of set of edges in the timed automaton generated by \eqref{eqn:lti-ex-1}-\eqref{eqn:lti-ex-2}. A circle at the coordinate $(i,j)$ denotes an edge from location $i$ to location $j$.}
\label{fig_4}
\end{figure}

\section{Conclusions and Future Work}
We have presented an approach to capture the sampling behavior of perturbed LTI systems with $\mathcal{L}_2$-based triggering mechanisms by timed safety automata. It has been shown that the derived timed automaton $\varepsilon$-approximately simulates the ETC system. The main contribution of this study falls into the subject of synthezing scheduling policies for ETC feedback loops using timed automata. Because of the inherent robustness of ETC strategies to perturbations, they are more appealing in practical applications compared to STC strategies. However, most of the existing ETC strategies are equipped with the quantity of minimum inter-sample time that indicates the maximum utilization of communication bandwidth. Despite the fact that such quantity can practically be used in scheduling of ETC feedback loops, it does not enable the full exploitation of the beneficiary features of ETC strategies in scheduling feedback policies. In fact, using solely such quantity in scheduling policies results in TDC-like techniques. Furthermore, in most of decentralized ETC strategies in the literature, the existence of a minimum inter-sample time among different subsystems is absent, see e.g.\ \cite{donkers2012output}. Exploiting the already existing tools for the synthesis of timed automata, one can further extend the results of this study to synthesize conflict-free policies in WNCS's, see e.g.\ \cite{Arman2015} which proposed a centralized scheduling of feedback policies. Another promising direction to follow is to find a fully decentralized approach instead of the centralized approach proposed in \cite{Arman2015}. Moreover, a modification that can be made to the analysis given in this study is related to the regional upper bounds derived in Section \ref{sec:abs-construction-ta}. It has been observed that these bounds are relatively large since perturbations can have a stabilizing effect on the error dynamics and as a result cause the enlargement of inter-sample times. Since these large upper bounds can possibly result in a timed automaton with a large number of transitions, using these timed automata may suffer from scalability issues for scheduling purposes. Therefore, one may assume to arbitrate an upper bound on the triggering mechanism to facilitate the scheduling process. Considering the case of multiple WNCS's, this type of assumption is closely related to periodic-ETC strategies, see e.g.\ \cite{heemels2013periodic}, and the assumed bound can be seen as the network heartbeat forcing ETC feedback loops updates.

\section{ACKNOWLEDGMENTS}

The authors gratefully appreciate the fruitful discussions with Dieky Adzkiya and Nikolaos Kekatos.


\section{Introduction}

In 2010 Schernhammer and Gramlich~\cite{SG10} showed that quasi-decreasingness
of a DCTRS~$\RR$ is equivalent to $\mu$-termination of its context-sensitive
unraveling ${U_\msf{CS}(\RR)}$ on original terms. While the direction that
quasi-decreasingness of $\RR$ implies $\mu$-termination of ${U_\msf{CS}(\RR)}$ on original
terms is shown directly; the converse -- facilitating the use of
context-sensitive termination tools like \systemname{MU-TERM}~\cite{AGLN10} and
\systemname{VMTL}~\cite{SG09} -- employs the additional notion of context-sensitive
quasi-reductivity of $\RR$.
In the following, we give a direct proof of the fact that $\mu$-termination of
${U_\msf{CS}(\RR)}$ on original terms implies quasi-decreasingness of $\RR$.
Moreover, we report our experimental findings on DCTRSs from the confluence
problems database (Cops),\footnote{\url{http://cops.uibk.ac.at}} extending the
experiments of Schernhammer and Gramlich.

\subparagraph{Contribution.}
A direct proof that $\mu$-termination of a CSRS ${U_\msf{CS}(\RR)}$ on original terms implies
quasi-decreasingness of the DCTRS $\RR$. New experiments on a recent DCTRS
collection.

\section{Preliminaries}

We assume familiarity with the basic notions of (conditional and
context-sensitive) term
rewriting~\cite{BN98,L98,O02}, but shortly recapitulate terminology and notation
that we use in the remainder.
Given two arbitrary binary relations $\xr[\alpha]{}$ and $\xr[\beta]{}$,
we write $\xl[\alpha]{}$, $\xr[\alpha]{+}$, $\xr[\alpha]{*}$ for the
\emph{inverse},
the \emph{transitive closure}, and the \emph{reflexive transitive closure}
of $\xr[\alpha]{}$,
respectively.
The relation obtained by considering $\xr[\alpha]{}$ \emph{relative to}
$\xr[\beta]{}$, written $\xr[\alpha/\beta]{}$, is defined by
$\xr[\beta]{*}\cdot\xr[\alpha]{}\cdot\xr[\beta]{*}$.
We use $\vars(\cdot)$ to denote the set of variables occurring in a given
syntactic object, like a term, a pair of terms, a list of terms, etc.
The set of terms $\TT(\FF,\VV)$ over a given signature of function symbols $\FF$
and set of variables $\VV$ is defined inductively:
$x \in \TT(\FF, \VV)$ for all variables $x \in \VV$,
and for every $n$-ary function symbol $f \in \FF$ and terms $t_1,\ldots,t_n \in
\TT(\FF,\VV)$ also $f(t_1,\ldots,t_n) \in \TT(\FF,\VV)$.
A \emph{deterministic oriented 3-CTRS (DCTRS)} $\RR$ is a set of conditional
rewrite rules of the shape $\crule{}$ where $\ell$ and $r$ are terms and $c$ is
a possibly empty sequence of pairs of terms $s_1 \approx t_1, \ldots, s_n
\approx t_n$.
For all rules in $\RR$ we have that
$\ell \not\in \VV$,
$\vars(r) \subseteq \vars(\ell,c)$, and
$\vars(s_i) \subseteq \vars(\ell,t_1,\ldots,t_{i-1})$
for all $1 \leqslant i \leqslant n$.
The rewrite relation induced by a DCTRS~$\RR$ is structured into levels. For
each level $i$, a TRS~$\RR_ i$ is defined recursively by
$\RR_0 = \varnothing$ and
$\RR_{i+1} = \{
  \ell \sigma \approx r \sigma \mid
  \crule{} \in \RR
  \land
  \forall s \approx t \in c.~ s \sigma \xr[\RR_i]{*} t \sigma
\}$
where for a given TRS~$\mathcal{S}$, $\xr[\mathcal{S}]{}$ denotes the induced
rewrite relation (i.e., its closure under contexts and substitutions).
Then the rewrite relation of $\RR$ is $\xr[\RR]{} = \bigcup_{i \geqslant
0}\xr[\RR_i]{}$.
We have $\RR = \RR_\msf{c} \uplus \RR_\msf{u}$ where $\RR_\msf{c}$ denotes the
subset of rules with non-empty conditional part ($n > 0$) and $\RR_\msf{u}$ the
subset of unconditional rules ($n = 0$).
A DCTRS $\RR$ over signature $\FF$ is \emph{quasi-decreasing} if there is a
well-founded order $\succ$ on $\terms$ such that
${\succ} = ({\succ}\cup{\ensuremath{\mathrel{\vartriangleright}}})^+$,
${\xr[\RR]{}} \subseteq {\succ}$,
and for all rules
$\ell\to r\Leftarrow s_1\approx t_1,\ldots,s_n\approx t_n$ in $\RR$,
all substitutions $\sigma \colon \VV \to \terms$, and
$0\leqslant i < n$, if
$s_j\sigma \xr[\RR]{*} t_j \sigma$
for all $1 \leqslant j \leqslant i$
then $\ell \sigma \succ s_\text{i+1} \sigma$
.

Given a DCTRS $\RR$ its \emph{unraveling $U(\RR)$} (cf.~\cite[p. 212]{O02}) is
defined as follows.
For each conditional rule
$\rname\colon \ell\to r\Leftarrow s_1 \approx t_1, \ldots, s_n \approx t_n$
(where $n > 0$)
we introduce $n$ fresh function symbols $U^\rname_1,\ldots,U^\rname_n$
and generate the set of $n + 1$ unconditional rules $U(\rname)$ as follows
\begin{align*}
\ell &\to U^\rname_1(s_1,\varsseq(\ell)) \\
U^\rname_1(t_1,\varsseq(\ell)) &\to
U^\rname_2(s_2,\varsseq(\ell),\Evarsseq(t_1))\\
&\vdots\\
U^\rname_n(t_n,\varsseq(\ell),\Evarsseq(t_1,\ldots,t_{n-1})) &\to r
\end{align*}
where $\varsseq$ and $\Evarsseq$ denote functions that yield the respective
sequences of elements of $\vars$ and $\ensuremath{\EE\VV}$ in some arbitrary but fixed order,
and
$\ensuremath{\EE\VV}(t_i) = \vars(t_i) \setminus \vars(\ell,t_1,\ldots,t_{i-1})$
denotes the \emph{extra variables} of the right-hand side of the $i$th
condition.
Finally the unraveling of the DCTRS is $U(\RR) = {\RR_\msf{u}}\cup{\bigcup_{\rname \in
\RR_\msf{c}}U(\rname)}$
.

A \emph{context-sensitive rewrite system} (CSRS) is a TRS (over signature $\FF$)
together with a replacement map $\mu \colon \FF \to 2^\mathbb{N}$ that restricts
the argument positions of each function symbol in $\FF$ at which we are allowed
to rewrite.
A position $p$ is \emph{active} in a term $t$ if either $p = \epsilon$,
or $p = iq$, $t = f(t_1,\ldots,t_n)$, $i \in \mu(f)$, and $q$ is active in
$t_i$.
The set of active positions in a term $t$ is denoted by $\ensuremath{\PP\textsf{os}}\xspace_\mu(t)$.
Given a CSRS $\RR$ a term $s$ $\mu$-rewrites to a term $t$, written $s \to_\mu
t$, if $s \to_\RR t$ at some position $p$ and $p \in \ensuremath{\PP\textsf{os}}\xspace_\mu(s)$.
A CSRS is called \emph{$\mu$-terminating} if its context-sensitive rewrite
relation is terminating.
The (proper) subterm relation with respect to replacement map $\mu$, written
$\ensuremath{\mathrel{\vartriangleright}}_\mu$, restricts the ordinary subterm relation to active positions.

We conclude this section by recalling the notion of context-sensitive
quasi-reductivity in an attempt to further appreciation for a proof without this
notion.
\begin{definition}
A CSRS $\RR$ over signature $\FF$ is \emph{context-sensitively quasi-reductive}
if there is an extended signature $\FF' \supseteq \FF$, a replacement map
$\mu$ (with $\mu(f) = \{1, \ldots, n\}$ for every $n$-ary $f \in \FF$), and a
$\mu$-monotonic, well-founded partial order $\succ_\mu$ on $\TT(\FF',\VV)$ such
that for every rule~$\ell \to r \IF s_1 \EQ t_1,\ldots,s_k \EQ t_k$, every
substitution~$\sigma : \VV \to \TT(\FF,\VV)$, and every $0 \leqslant i \leqslant
k-1$:
\begin{itemize}
\item
$\ell\sigma \mathrel{({\succ_\mu}\cup{\ensuremath{\mathrel{\vartriangleright}}_\mu})}^+ s_{i+1}\sigma$ whenever
$s_j\sigma \succeq_\mu t_j\sigma$ for every $1\leqslant j\leqslant i$, and

\item
$\ell\sigma \succ_\mu r\sigma$ whenever $s_j\sigma \succeq_\mu t_j\sigma$
for every $1\leqslant j\leqslant k$.
\end{itemize}
\end{definition}

\section{Characterization}

In order to present our main result (the proof of \thmref{main} below) we first
restate some definitions and theorems which we will use in the proof.

The usual unraveling is extended by a replacement map in order to restrict
reductions in $U$-symbols to the first argument position~\cite[Definition
4]{SG10}.

\begin{definition}[Unraveling ${U_\msf{CS}(\RR)}$]
The \emph{context-sensitive unraveling ${U_\msf{CS}(\RR)}$} is the unraveling $U(\RR)$
together with the replacement map $\mu$ such that
$\mu(f) = \{1,\ldots,k\}$ if $f\in\FF$ with arity $k$ and
$\mu(f) = \{1\}$ otherwise.
We say that the resulting CSRS is \emph{$\mu$-terminating on original
terms}~\cite[Definition~7]{SG10}, if there is no infinite ${U_\msf{CS}(\RR)}$-reduction
starting from a term $t \in \terms$.
\end{definition}

Simulation completeness of ${U_\msf{CS}(\RR)}$ (i.e., that every $\RR$-step can be simulated
by a ${U_\msf{CS}(\RR)}$-reduction) can be shown by induction on the level of a
conditional rewrite step~\cite[Theorem~1]{SG10}.
\begin{theorem}[Simulation completeness]
\label{thm:simcomp}
  For a DCTRS $\RR$ we have ${\xr[\RR]{}}\subseteq{\xr[{U_\msf{CS}(\RR)}]{+}}$.
  \qed
\end{theorem}
Furthermore, we need the following auxiliary result.
\begin{lemma}
  \label{lem:one}
  For any context-sensitive rewrite relation $\xr[\mu]{}$ induced by the
  replacement map $\mu$, $\ensuremath{\mathrel{\vartriangleright}}_\mu$ commutes over $\xr[\mu]{}$, i.e.,
  ${\ensuremath{\mathrel{\vartriangleright}}_\mu}\cdot{\xr[\mu]{}} \subseteq {\xr[\mu]{}}\cdot{\ensuremath{\mathrel{\vartriangleright}}_\mu}$.

\end{lemma}
\begin{proof}
  Assume $s \ensuremath{\mathrel{\vartriangleright}}_\mu t \xr[\mu]{} u$ for some terms~$s$, $t$, and $u$. Then
  $s = {C[t]}\ensuremath{\mathrel{\vartriangleright}}_\mu{t} \xr[\mu]{} u$ for some nonempty context~$C$.  Thus
  we conclude by $C[t] \xr[\mu]{} C[u] \ensuremath{\mathrel{\vartriangleright}}_\mu u$.

\end{proof}

With this we are finally able to prove our main result.
\begin{theorem}
  \label{thm:main}
  If the CSRS ${U_\msf{CS}(\RR)}$ is $\mu$-terminating on original terms then the DCTRS $\RR$
  is quasi-decreasing.
\end{theorem}
\begin{proof}
Assume that ${U_\msf{CS}(\RR)}$ is $\mu$-terminating on original terms.
We define an order $\succ$ on $\terms$
\[
\textstyle
  {\succ}
  \defby
  {({\xr[{U_\msf{CS}(\RR)}]{}}\cup{\ensuremath{\mathrel{\vartriangleright}}_\mu})^+ \cap (\terms \times \terms)}
  \tag{$\star$}\label{eq:1}
\]
and show that it satisfies the four properties from the definition of
quasi-decreasingness:
\begin{enumerate}
  \item We start by showing that $\succ$ is well-founded on $\terms$.
    Assume, to the contrary, that $\succ$ is not well-founded. Then we have
    an infinite sequence
    \begin{equation}
    {t_1}\succ{t_2}\succ{t_3}\succ{\ldots}\tag{$\dagger$}\label{eq:inf}
    \end{equation}
    where all
    $t_i\in\terms$.
    By definition $\ensuremath{\mathrel{\vartriangleright}}_\mu$ is well-founded.
    Moreover, since ${U_\msf{CS}(\RR)}$ is $\mu$-terminating on original terms, $\xr[{U_\msf{CS}(\RR)}]{}$ is
    well-founded on $\terms$.
    Further note that every $\xr[{U_\msf{CS}(\RR)}]{}$-terminating element
    (hence every term in $\terms$) is
    ${\xr[{U_\msf{CS}(\RR)}/{\ensuremath{\mathrel{\vartriangleright}}_\mu}]{}}$-terminating, since
    by a repeated application of \lemref{one} every infinite reduction
    $
      t_1 \xr[{U_\msf{CS}(\RR)}/{\ensuremath{\mathrel{\vartriangleright}}_\mu}]{} t_2 \xr[{U_\msf{CS}(\RR)}/{\ensuremath{\mathrel{\vartriangleright}}_\mu}]{} \cdots
    $
    starting from a term $t_1 \in \terms$
    can be transformed into an infinite $\xr[{U_\msf{CS}(\RR)}]{}$-reduction, contradicting
    well-foundedness of $\xr[{U_\msf{CS}(\RR)}]{}$ on $\terms$.

    We conclude by analyzing the following two cases:
    \begin{itemize}
      \item
      Either \eqref{inf} contains $\xr[{U_\msf{CS}(\RR)}]{}$ only finitely often,
      contradicting well-foundedness of $\ensuremath{\mathrel{\vartriangleright}}_\mu$,
      \item
      or there are infinitely many $\xr[{U_\msf{CS}(\RR)}]{}$-steps in \eqref{inf}.
      But then we can construct a sequence
      ${s_1}{\xr[{U_\msf{CS}(\RR)}/{\ensuremath{\mathrel{\vartriangleright}}_\mu}]{}}
      {s_2}{\xr[{U_\msf{CS}(\RR)}/{\ensuremath{\mathrel{\vartriangleright}}_\mu}]{}}
      {s_3}{\xr[{U_\msf{CS}(\RR)}/{\ensuremath{\mathrel{\vartriangleright}}_\mu}]{}}
      \ldots$ with $s_1 = t_1$,
      contradicting the fact that all elements of $\terms$ are
      ${\xr[{U_\msf{CS}(\RR)}/{\ensuremath{\mathrel{\vartriangleright}}_\mu}]{}}$-terminating.
    \end{itemize}
  \item Next we show ${\succ}={\mathrel{({\succ}\cup{\subterm})^+}}$. The direction
    ${\succ}\subseteq{\mathrel{({\succ}\cup{\subterm})^+}}$ is obvious.
    For the other direction, ${\mathrel{({\succ}\cup{\subterm})^+}}\subseteq{\succ}$,
    assume we have ${s}\auxreln{n+1}{t}$.
    Then we proceed by induction on $n$.
    In the base case $s \mathrel{({\succ}\cup{\ensuremath{\mathrel{\vartriangleright}}})} t$.
    If $s \succ t$ we are done. Otherwise, $s \ensuremath{\mathrel{\vartriangleright}} t$ and thus also $s
    \ensuremath{\mathrel{\vartriangleright}}_\mu t$ since $s, t\in\terms$ and therefore $s \succ t$.
    In the step case $n = k + 1$ for some $k$, and $s \mathrel{({\succ}\cup{\ensuremath{\mathrel{\vartriangleright}}})} u
    \auxreln{k}{t}$. Then we obtain $s \succ u$ by a similar case-analysis as in
    the base case. Moreover $u \succ t$ by induction hypothesis, and thus $s
    \succ t$.

  \item Now we show that ${\xr[\RR]{}}\subseteq{\succ}$. Assume ${s}\xr[\RR]{}{t}$.
    Together with simulation completeness of ${U_\msf{CS}(\RR)}$, \thmref{simcomp}, we get ${s}\xr[{U_\msf{CS}(\RR)}]{+}{t}$
    which in turn implies ${s}\succ{t}$.
  \item Finally, we show that if for all $\ell \to r \IF s_1 \approx t_1, \ldots,
    s_n \approx t_n$ in $\RR$, substitutions $\sigma\colon \VV \to \terms$, and
    $0 \leqslant i < n$,
    if ${s_j\sigma}\xr[\RR]{*}{t_j\sigma}$ for all $1 \leqslant j \leqslant i$ then
    ${\ell\sigma}\succ{s_{i+1}\sigma}$.
    We have the sequence
    \[\textstyle
      {\ell\sigma}\xr[{U_\msf{CS}(\RR)}]{+}{U^\rname_{i+1}(s_{i+1},\varsseq(\ell),\Evarsseq(t_1,\ldots,t_i))\sigma}
      \ensuremath{\mathrel{\vartriangleright}}_\mu{s_{i+1}\sigma}
    \]
    using the definition of ${U_\msf{CS}(\RR)}$ together with simulation completeness (\thmref{simcomp}).
    But then also ${\ell\sigma}\succ{s_{i+1}\sigma}$ as wanted because
    $\ell\sigma,s_{i+1}\sigma\in\terms$.
\end{enumerate}
Hence $\RR$ is quasi-decreasing with the order $\succ$.
\end{proof}

The converse of \thmref{main} has already been shown by Schernhammer and
Gramlich~\cite[Theorem 4]{SG10}:
\begin{theorem}
  If a DCTRS $\RR$ is quasi-decreasing then the CSRS ${U_\msf{CS}(\RR)}$ is $\mu$-terminating
  on original terms.
  \qed
\end{theorem}
Thus the desired equivalence follows as an easy corollary.
\begin{corollary}
  Quasi-decreasingness of a DCTRS $\RR$ is equivalent to $\mu$-termination of
  the CSRS ${U_\msf{CS}(\RR)}$ on original terms.
\end{corollary}

\section{Experiments}
\label{sec:exps}

\begin{table}[t]
  \centering
  \caption{(Non-)quasi-decreasing DCTRSs out of 103 in Cops
  by transformation and tool.}
  \begin{tabularx}{\textwidth}{Xc@{\ }c@{\ }cc@{\ }c@{\ }cc@{\ }c@{\ }c@{\ }c@{\ }cc}
    \toprule
    & \multicolumn{3}{c}{conditional $\RR$}
    & \multicolumn{3}{c}{${U_\msf{CS}(\RR)}$}
    & \multicolumn{5}{c}{$U(\RR)$} & \\
    \cmidrule(lr){2-4}
    \cmidrule(lr){5-7}
    \cmidrule(lr){8-12}
    & \scriptsize \aprove & \scriptsize \systemname{MU-TERM} & \scriptsize \systemname{VMTL}
    & \scriptsize \aprove & \scriptsize \systemname{MU-TERM} & \scriptsize \systemname{VMTL}
    & \scriptsize \aprove & \scriptsize \systemname{MU-TERM} & \scriptsize \natt
    & \scriptsize \TTTT & \scriptsize \systemname{VMTL} & total \\
    \midrule
    YES & 80 & 78 & 80 & 78 & 78 & 79 & 81 & 78 & 77 & 78 & 78 & 84 \\
    NO & -- & 12 & -- & -- & -- & -- & -- & -- & -- & -- & -- & 12 \\
    \bottomrule
  \end{tabularx}
  \label{tab:exp}
\end{table}

In order to present up-to-date numbers for (non-)quasi-decreasingness we
conducted experiments on the 103 DCTRSs contained in the confluence problems
database using various automated termination tools.
Of these, \aprove~\cite{GBE14},
\systemname{MU-TERM}~5.13~\cite{AGLN10}, and \systemname{VMTL}~1.3~\cite{SG09} are able to directly show
quasi-decreasingness and
\systemname{MU-TERM} is the only tool that can show non-quasi-decreasingness~\cite{LMG14}.
\aprove, \systemname{MU-TERM}, and \systemname{VMTL} can also handle context-sensitive
systems and we used them in combination with ${U_\msf{CS}(\RR)}$.
Finally, we also ran the previous tools together with
\natt~\cite{YKS14} and \TTTT~1.16~\cite{KSZM09} on
$U(\RR)$.
The results for a timeout of one minute are shown in \tabref{exp}.
There are several points of notice.
The most yes-instances (81) we get if we use \aprove together with $U(\RR)$.
Interestingly, \aprove cannot show quasi-decreasingness of system 362 directly,
although it succeeds (like all other tools besides \natt) if provided with its
unraveling.
Moreover, systems 266, 278, and 279 can be shown to be quasi-decreasing by \aprove if
we use $U(\RR)$ but not if we use ${U_\msf{CS}(\RR)}$ (even if we increase the timeout to 5
minutes).
On system 363 only \systemname{MU-TERM} succeeds (in the direct approach).
If we compare \systemname{MU-TERM} on conditional systems to \systemname{MU-TERM} with ${U_\msf{CS}(\RR)}$,
the direct method succeeds on system 360 but not
on system 329. Conversely, when using ${U_\msf{CS}(\RR)}$ it succeeds on system 329
but not on system 360.
Moreover, \systemname{MU-TERM} seems to have some problems with systems 278 and 342,
generating errors in the direct approach.
With ${U_\msf{CS}(\RR)}$ \systemname{VMTL} succeeds on 79 systems, subsuming the results from \aprove and
\systemname{MU-TERM} (78 each). On system 357 only \systemname{VMTL} together with ${U_\msf{CS}(\RR)}$ succeeds.
With $U(\RR)$, \natt succeeds on 77 systems, this is subsumed by
\TTTT, succeeding on 78 systems, which in turn is subsumed by \aprove,
succeeding, as mentioned above, on 81 systems.
In total 84 systems are shown to be quasi-decreasing, 12 systems to be
non-quasi-decreasing, and only 7 remain open.
One of these, for example, is system 337 from Cops, for computing
Bubble-sort~\cite{SR06}
\begin{xalignat*}{2}
  x < 0 &\to \fs{false} &
  0 < \fs{s}(y) &\to \fs{true}\\
  \fs{s}(x) < \fs{s}(y) &\to x < y &
  x : y : \ys &\to y : x : \ys \IF x < y \EQ \fs{true}
\intertext{whose unraveling replaces the last (and only conditional) rule by the
two rules:}
  x : y : \ys &\to \fs{U}(x < y, x, y, \ys) &
  \fs{U}(\fs{true}, x, y, \ys) &\to y : x : \ys
\end{xalignat*}

\section{Conclusion}

We provide a direct proof
for one direction of a previous characterization of quasi-decreasingness, i.e.,
that $\mu$-termination of a CSRS
${U_\msf{CS}(\RR)}$ on original terms implies quasi-decreasingness of the DCTRS $\RR$ without
the need of a detour by using the notion of context-sensitive quasi-reductivity.
We believe that our proof could easily be adapted to any other context-sensitive
transformation as long as it is simulation complete.
Moreover, we provide experimental results on a recent collection of DCTRSs.
Knowing that a DCTRS is quasi-decreasing is, among other things, useful to
show confluence with the Knuth-Bendix criterion for CTRSs~\cite{AL94}.

\subparagraph*{Acknowledgments.}

We thank the Austrian Science Fund (FWF project P27502) for supporting
our work.
Moreover we would like to thank the anonymous reviewers for useful hints and
remarks and particularly for pointing out a flaw in an earlier version of
Section~\ref{sec:exps}.


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

In this talk, I discuss the mere 5\,\% of the energy pie (mainly of atoms composed of baryons) of the Universe shown in Fig. \ref{fig:Epie}.  At the most fundamental level of  the grand unification(GUT) scheme, it belongs to the problem on the chiral representation of quarks \cite{Georgi79,KimICHEP1,KimJHEP15}. In cosmology, it belongs to Sakharov's three conditions. The first one is the existence of baryon number ($B$) violating interaction, and the second is the existence of CP violation \cite{Sakharov67}. For example, at the red clover point of Fig. \ref{fig:Parity} let us calculate baryons moving forward/backward in time. The ratio is the number of baryons over the  number of antibaryons. Therefore, to have a nonzero $\Delta B$, we need T or CP violation. We also need to break C. To see this, firstly assume T violation and calculate $\Delta B$ at the red clover point in Fig. \ref{fig:Parity}. Second, integrate over solid angles. At the black clover point, if C is not broken then
\begin{figure}[!b]
  \begin{center}
  \begin{tabular}{c}
   \includegraphics[width=0.45\textwidth]{figEpie.eps}
   \end{tabular}
  \end{center}
 \caption{The energy pie of the Universe.
  }
\label{fig:Epie}
\end{figure}
$\Delta B$ is minus that of red clover point, because $P=-1$ is multiplied.  Then, integration over the solid angle gives $\Delta B=0$. Therefore, the needed T violation in the $\Delta B\ne 0$ processes must accompany the C violation also. The CP violation in  the standard model(SM) arises as the ``V-A'' form and hence also breaks C.  Sakharov's third condition on ``out of thermal equilibrium'' is satisfied by the decay of some heavy particle(s), which is usually assumed in most baryo- and lepto-genesis mechanisms.
\begin{figure}[!t]
  \begin{center}
  \begin{tabular}{c}
   \includegraphics[width=0.45\textwidth]{figCPop.eps}
   \end{tabular}
  \end{center}
 \caption{The ${B}$ number in the parity operated part in the Universe.
  }
\label{fig:Parity}
\end{figure}

The CP violation seems to work also in some models of dark matter in the Universe. The asymmetric dark matter scenario for this case follows the paradigm of baryogenesis and hence CP violation is the key here also. The axion scenario for dark matter \cite{Baer15} uses an oscillating axion field whose amplitude at present is of order $|\bar{\theta}_{\rm max}|\simeq 10^{-20}$ \cite{KimJeju16}. For nonzero $\bar{\theta}$ though oscillating, CP is violated  and hence CP violation is the key in the axionic dark matter scenario also. Only, the WIMP scenario for dark matter uses just the  cosmological freezeout temperature, not employing any kind of CP violation \cite{Baer15}.

In this talk I will briefly review the weak CP violation first and then present a new mechanism on the leptogenesis that we call `Type-II leptogenesis' with CP violation in the chiral theory \cite{CoviKim16}.

\section{CP violation and CKM matrix}

In the SM, CP violation is represented by $W_\mu^\pm$ couplings to SU(2)$_W$ doublet fermions which are parametrized by the unitary CKM and PMNS matrices \cite{KM73,PMNS}. In particular, the elements of the CKM matrix are well-known by now, and there are three classes of parametrizations, which we explain below.
Let the CP phase of the CKM matrix be $\delq$. Then, any Jarlskog triangle \cite{Jarlskog85} has an angle $\delq$ \cite{KimICHEP1}.  The Jarlskog invariant $J$  has a simple expression with Det.\,$V_{\rm CKM}=1$ \cite{KimMoNam15},
 \dis{
 J=|\textrm{Im\,}V_{31}V_{22}V_{13}|.
 }

There are six Jarlskog triangles. A triangle with the lengths of O($\lambda^3$) for all three sides, where $\lambda=\sin\theta_C$, is shown in Fig. \ref{fig:JTriBmeson}. Here we denoted the sides in the Kim-Seo (KS) parametrization  \cite{KimSeo11}.
In this figure, there are three angles, $\alpha,\beta$ and $\gamma$, any of which is not small. We can use any of these as $\delq$, which can be called, `$\alpha$-class', `$\beta$-class', and `$\gamma$-class', respectively. The KS parametrization and the Kobayashi-Maskawa parametrization \cite{KM73} belong to the $\alpha$-class, and the Chau-Keung-Maiani (CKM) parametrization \cite{CK84,Maiani76,PDG15}  belongs to the $\gamma$-class   \cite{KimICHEP1}.
\begin{figure}[!t]
  \begin{center}
  \begin{tabular}{c}
   \includegraphics[width=0.35\textwidth]{figJalsLarge.eps}
   \end{tabular}
  \end{center}
 \caption{The Jarlskog triangle of area O($\lambda^6$) from $B$ meson decays with three comparable sizes of O($\lambda^3$)  in the KS parametrization \cite{KimSeo11}.
  }
\label{fig:JTriBmeson}
\end{figure}
Note that the unitarity triangle in the PDG book gives \cite{PDG15}
\dis{
&\alpha=\left(85.4^{+3.9}_{-3.8}\right)^{\rm o},
~\beta=\left(21.50^{+0.76}_{-0.74}\right)^{\rm o}\\
&\gamma=\left( 68.0^{+8.0}_{-8.5}\right)^{\rm o}.\label{eq:PDGfit}
 }
 Since $\alpha$ is close to $90^{\rm o}$, we use the KS parametrization,
\dis{
&\left(
\begin{array}{ccc}
c_1 & s_1c_3 & s_1s_3  \\
-c_2s_1 & -e^{-i\delta'}s_2s_3+c_1c_2c_3 & e^{-i\delta'}s_2c_3+c_1c_2s_3  \\
e^{i\delta'}s_1s_2 & -c_2s_3-c_1s_2c_3 e^{i\delta'} & c_2c_3-c_1s_2s_3e^{i\delta'} \\
\end{array}\right),
 }
where $\delta'=\delq$, and   $c_i=\cos\theta_i$ and $s_i=\sin\theta_i$. With this parametrization, we can prove that the weak CP violation is maximal with the currently determined real CKM angles. Since any Jarlskog triangle gives the same $J$, consider the triangle with two long sides of O($\lambda$) as shown in Fig. \ref{fig:JTriMax}.
\begin{figure}[!t]
  \begin{center}
  \begin{tabular}{c}
   \includegraphics[width=0.30\textwidth]{figArea.eps}
   \end{tabular}
  \end{center}
 \caption{The Jarlskog triangle of  area O($\lambda^6$) with two long sides of O($\lambda$). This area must be exactly the same as that of Fig. \ref{fig:JTriBmeson}. The angle $\delta$ is rotated and $J$ is maximal with $\delta\simeq 90^{\rm o}$.
  }
\label{fig:JTriMax}
\end{figure}
The area of the triangle ($=\frac12 J$) is O($\lambda^6$). So, it is $\frac12 \lambda\cdot\lambda^5\cdot\sin\delta$ which is maximal with $\delta=90^{\rm o}$. With the measured real angles $\theta_{1,2,3}$, this maximality must be true in any parametrization. Even we use the CKM parametrization \cite{CK84}, it must be so but the proof may not be so
simple\footnote{To prove the maximality with the observed real angles in the CKM parametrization \cite{CK84}, one must slightly vary the real angles also since $\gamma$ is not close to $ \frac{\pi}{2}$.} as given in the KS parametrization where $\delq=\alpha$ is close to $\frac{\pi}{2}$.  This is based on the fact that in a given parametrization  all the six triangles give the identical area.

Note, however, that at present a specific parametrization is not better than others. If one finds a process to determine three real angles or $\delq$ itself, the measured value(s) for that process can choose a correct class of parametrization scheme.

\section{Maximal CP violation in the PMNS matrix?}

In the previous section, we observed that there is a possibility that $\delq=\frac{\pi}{2}$. It will be very interesting if the leptonic CP violation in the SM also gives  $\dell=\pm  \frac{\pi}{2}$. Then, one may look for a theory relating $\delq$ and $\dell$ as tried in  \cite{KimNam15}. Even though the significance is very low, there is a hint that $\dell\approx -\frac{\pi}{2}$ \cite{T2KCP}. But $\dell\ne 0$ is a more significant statement than fixing it as $\dell\approx -\frac{\pi}{2}$.

The PMNS lepton mixing angles in the SM is parametrized by
\dis{
 &\left(
\begin{array}{ccc}
C_1 & S_1C_3 & S_1S_3  \\
-C_2S_1 & -e^{-i\delta}S_2S_3+C_1C_2C_3 & e^{-i\delta}S_2C_3+C_1C_2S_3  \\
e^{i\delta}S_1S_2 & -C_2S_3-C_1S_2C_3 e^{i\delta} & C_2C_3-C_1S_2S_3e^{i\delta} \\
\end{array}\right)\label{eq:PMNS}
 }
where  $\delta=\dell$ \cite{PMNS}, and   $C_i=\cos\Theta_i$ and $S_i=\sin\Theta_i$.
Because $\dell$ is non-zero, let us look for leptogenesis mechanism which includes $\dell$ explicitly.

\section{Leptogenesis}
It is known that the sphaleron processes at the electroweak scale changes
$B$ and $L$ numbers but conserves $B-L$  \cite{EWgen}. At the electroweak scale, the sphaleron conversion of $L$ to $B$ or vice versa gives the final $B$ and $L$ proportional to the initial $B-L$. Since the SU(5)  GUT  conserves $B-L$, thus the early GUT idea \cite{BAgut} on baryogenesis seems not working.

 For non-zero final baryon number, generation  of  $B$ and $L$ at high temperature must occur through processes which generate nonzero $B-L$. In GUTs, therefore, we use the $B-L$ breaking interaction in
SO(10), for example. In the beyond SM (BSM) with singlets, we can use a singlet $N$, called ``heavy neutrino'' at high energy scale, to generate just $L$. The early idea was to define a right(left)-handed $N$ with lepton number $L=+1(-1)$ \cite{FY86}. In fact, the definition of lepton number, related to neutrino masses, is a combination of defining the lepton number  of the up-type Higgs doublets together with that of $N$. The leptogenesis with the definition of $L=+1$ for $N_R$ is called here `Type-I leptogenesis' \cite{FY86}.

\section{Type-II leptogenesis}

`Type-II leptogenesis' is proposed \cite{CoviKim16} under a different definition on $L$ from that of Type-I and the electroweak symmetry breaking at high temperature. There exists a finite region of parameter space in the multi-Higgs model that the electroweak symmetry is broken at high temperature  \cite{Senj79}. In SUSY, the electroweak symmetry breaking at high temperature is more probable since the temperature dependent terms in $V$ are SUSY breaking terms.

The lepton number is defined with the left-handed SM doublets $\ell_L(\ni\nu_{e,\mu,\tau})$ carrying $L=+1$. Weinberg's effective operator for neutrino masses is \cite{WeinbergNu79}
  \dis{
{\cal L}_Y\propto\frac{f_{ij}}{M}\ell_i\ell_j h_uh_u \label{eq:Wein}
  }
where $h_u$ is the up-type Higgs doublet. Non-zero neutrino masses break $L$. So, as far as $\langle h_u\rangle=0$, neutrinos do not obtain mass by the above operator. Therefore, $L$ can be properly defined below the scale of  $\langle h_u\rangle\ne 0$. One may argue that there is also $h_d$, which is exactly the reason that $h_u$ can carry a global quantum number, because both $h_u$ and $h_d$ can together define a gauge charge $Y$ and a global charge $L$.   To do so, in fact we need `inert' SU(2) doublets $H_{u,d}$.

  The effective interaction (\ref{eq:Wein}) is realized in terms of two renormalizable operators
 \dis{
 M_0NN,~\ell N h_u
 }
where $M_0$ in our jargon is the `messenger' mass, connecting $N$ and $\nu$,  which is the so-called ``seesaw'' mechanism, first suggested with a humdrum title in \cite{Minkowski77}. But, for neutrino masses at low energy, ``who cares about renormalizable interactions\,?'', as noticed in many mechanisms for neutrino masses of Type$_{I,II,III}$.

\begin{table}
\centerline{\begin{tabular}{|l| ccc|}
\hline  &&&\\[-1em]
  &$\ell_L$ &$h_u\,(H_u)$ & $N$\\ \hline\\[-1.4em]
&&&  \\[-1em]
Type-I leptogenesis  &  ~$+1$~ &~$0$~&~$-1$~\\[0.3em]
Type-II leptogenesis &  ~$+1$~ &~$0\,(-2)$~ &$-1$~\\[0.3em]
\hline
\end{tabular}}
\caption{Definition of lepton numbers, in Type-I and Type-II leptogeneses.}
\label{tab:DefQno}
\end{table}

 However, in cosmology it matters because in the cosmic history the cosmic temperature $T$ has swept all possible energy scales of particle physics. One can define the {\it lepton number} $L$ as shown in Table \ref{tab:DefQno}.

\begin{figure}[t!]
  \begin{center}
   \includegraphics[width=0.45\textwidth]{figIntabcde.eps}
  \end{center}
 \caption{The Feynman diagrams interfering in the $N$ decay: (a) the lowest order diagram, (b) the $W$ exchange diagram, (c) the wave function renormalization diagram, and (d)  the heavy neutral lepton exchange diagram.  There exist similar ${\cal N}$-decay diagrams.   In all figures, the final leptons can be both charged leptons and neutrinos.
 The lepton number violations are inserted with blue bullets and phases are inserted at red bullets. (a) and (b) interfere.  (c) and (d) give a vanishing contribution in $N_0$ domination with one complex VEV.} \label{fig:IntCP}
\end{figure}

In Type-I leptogenesis, Figs. \ref{tab:DefQno}\,(e), (c), and (d) are considered where both the $L$ violation and CP violation appear in blue bullets. We need at least two $N$'s for the interference of  Figs. \ref{tab:DefQno}\,(e), (c), and (d). So, if there is a hierarchy of masses such as $m_{N_0}/m_{N_1}\ll 1$, then the lepton asymmetry is suppressed by that factor.

\begin{table}
\centerline{\begin{tabular}{|c| c ccccc|}
\hline  &&&&&&\\[-1em]
  &~$\ell_L$~ &$H_u$&$H_d$ & $h_{u,d}$&$N$ & ${\cal N}$\\ \hline\\[-1.4em]
&&&&&&  \\[-1em]
 Type-II leptogen. &  ~$+1$~ &~$-2$~&~$+2$~ &~$0$~&~$-1$~&~$+1$~\\[0.3em]
 VEV &  ~$\times$~ &~\textrm{inert}~ & $ \textrm{inert}$  & ~$v_{\rm ew}\{s_\beta,c_\beta\}$ &~$\times$~&~$\times$~\\[0.3em]
\hline
\end{tabular}}
\caption{Definition of lepton numbers  in Type-II leptogeneses. We introduced an inert Higgs $H_u$ carrying $L=-2$ with zero VEV and singlet leptons ${\cal N}$ carrying $L=+1$.}
\label{tab:Type2}
\end{table}

In Type-II leptogenesis, the lepton number is defined differently as shown in Table \ref{tab:Type2}. We need an inert Higgs doublet $H_u$ carrying $L=-2$  and singlet leptons ${\cal N}$ carrying $L=+1$. The relevant leptogenesis diagrams are those given in  Figs. \ref{tab:DefQno}\,(a) and (b). Here, the lepton number violation  appears in blue bullets and the CP violation appears in red bullets. Anyway, the fields $H_{u,d}$ and ${\cal N}$ introduced at high energy scale are not visible at low energy scale. We  introduce interactions
\dis{
&N_0\,\ell_L h_u,~{\cal N}_0\,\ell_L H_u,~N_0\,{\cal N}_0,~H_uH_d,\cdots\\
&h_u^*H_u,~N_0\,N_0,~{\cal N}_0{\cal N}_0, \cdots
}
where the first line conserves $L$ and  the second line violates $L$.

For Fig. \ref{tab:DefQno}\,(b) to be useful for leptogenesis at a high temperature, we must have $W$ boson is not massless, \ie SU(2)$\times$U(1) symmetry is broken at the high temperature. Indeed, such possibility has been suggested long time ago \cite{Senj79}.
Furthermore, in models with only one CP phase in an ultraviolet completed theory, leptogenesis phase can be related to the
PMNS phase.  Even, phases of heavy neutrinos, $N_0,\cdots$, are expressible in terms of this fundamental phase \cite{KimNam15}.

Within this framework, we calculated the lepton asymmetry which turned out to be
consistent with the fact that in these diagrams
the lepton violation is on the left side of the cut diagram as discussed in \cite{Adhikari:2001yr}.
The lepton asymmetry we obtain is a form,
\dis{
\eL^{N_0}(W)&
\approx \frac{\alpha_{\rm em}}{2\sqrt{2}\sin^2\theta_W}  \frac{\Delta m_h^2 }{m_0^2}\\
&\cdot\sum_{i,j}{\cal A}_{ij}\sin[(\pm n_P+n'-n_i+n_j)\delx],
\label{eq:asymmExp4}
}
where ${\cal A}_{ij}$ are given by Yukawa couplings, $n_P,n',n_i,n_j$ are integers, and we assumed that only one phase $\delta_X$ appears in the full theory.  Two independent $n'$ are Majorana phases multiplied to the PMNS matrix.
Using the sphaleron calculation of  \cite{D'Onofrio:2014kta}, we obtain
\dis{
\frac{\Gamma_{\rm sph}^{\rm broken}}{T^3 H(T)} =
\kappa \alpha_W^4 \left(\frac{ 4\pi k}{g_W} \right)^7 e^{- 1.52 k \frac{4\pi}{g_W}} \sqrt{\frac{90}{\pi^2 g_*}}
\frac{M_P}{T} \geq 1,
 }
leading to the constraint
\dis{
C_2 C_3 \sin\delta_c + C_1 S_2 S_3 \sin (\delta_c +
\dell) \simeq  2.4 \times 10^{-2},
 }
where $\delta_c$ is a Majorana neutrino phase. So, there is an enough parameter space to allow an acceptable $\Delta L$.

\section{Conclusion}

Here, my talk on Type-II leptogenesis is centered on:
\begin{itemize}
\item[(1)] A short discussion on weak CP,
\item[(2)] Introduction of a new leptogenesis mechanism in theories with SU(2)$\times$U(1) breaking at high temperature,

\item[(3)] Relation of $\dell$  to the leptogenesis phase in certain CP violation models,
\item[(4)] Need of one light intermediate scale Majorana neutrino $N_0$ and another neutrino ${\cal N}$ toward the desired lepton number asymmetry $\epsilon_L$.
\item[(5)] Inert Higgs and the SM Higgs mix to provide $\Delta L\ne 0$ vertex in the loop diagram.

\end{itemize}

\acknowledgments{This work is supported in part by the National Research Foundation (NRF) grant funded by the Korean Government (MEST) (NRF-2015R1D1A1A01058449) and  the IBS (IBS-R017-D1-2016-a00).}