Timed event system

A timed event system is a structure

${\displaystyle {\mathcal {G}}=<Z,Q,Q_{0},Q_{A},\Delta >}$

where

• ${\displaystyle \,Z}$ is the set of events;
• ${\displaystyle \,Q}$ is the set of states;
• ${\displaystyle \,Q_{0}\subseteq Q}$ is the set of initial states;
• ${\displaystyle Q_{A}\subseteq Q}$ is the set of accepting states;
• ${\displaystyle \Delta \subseteq Q\times \Omega _{Z,[t_{l},t_{u}]}\times Q}$ is the set of state trajectories in which ${\displaystyle (q,\omega ,q')\in \Delta }$ indicates that a state ${\displaystyle q\in Q}$ can change into ${\displaystyle q'\in Q}$ along with an event segment ${\displaystyle \omega \in \Omega _{Z,[t_{l},t_{u}]}}$. If two state trajectories ${\displaystyle (q_{1},\omega _{1},q_{2})}$ and ${\displaystyle (q_{3},\omega _{2},q_{4})\in \Delta }$ are called contiguous if ${\displaystyle q_{2}=q_{3}}$, and two event trajectories ${\displaystyle \omega _{1}}$ and ${\displaystyle \omega _{2}}$ are contiguous. Two contiguous state trajectories ${\displaystyle (q,\omega _{1},p)}$ and ${\displaystyle (p,\omega _{2},q')\in \Delta }$ implies ${\displaystyle (q,\omega _{1}\omega _{2},q')\in \Delta }$.

Given a timed event system ${\displaystyle {\mathcal {G}}=<Z,Q,Q_{0},Q_{A},\Delta >}$, the set of its behaviors is called its language depending on the observation time length. Let ${\displaystyle t}$ be the observation time length. If ${\displaystyle 0\leq t<\infty }$, ${\displaystyle t}$-length observation language of ${\displaystyle {\mathcal {G}}}$ is denoted by ${\displaystyle L({\mathcal {G}},t)}$, and defined as

${\displaystyle L({\mathcal {G}},t)=\{\omega \in \Omega _{Z,[0,t]}:\exists (q_{0},\omega ,q)\in \Delta ,q_{0}\in Q_{0},q\in Q_{A}\}.}$

We call an event segment ${\displaystyle \omega \in \Omega _{Z,[0,t]}}$ a ${\displaystyle t}$-length behavior of ${\displaystyle {\mathcal {G}}}$, if ${\displaystyle \omega \in L({\mathcal {G}},t)}$.

By sending the observation time length ${\displaystyle t}$ to infinity, we define infinite length observation language of ${\displaystyle {\mathcal {G}}}$ is denoted by ${\displaystyle L({\mathcal {G}},\infty )}$, and defined as

${\displaystyle L({\mathcal {G}},\infty )=\{\omega \in {\underset {t\rightarrow \infty }{\lim }}\Omega _{Z,[0,t]}:\exists \{q:(q_{0},\omega ,q)\in \Delta ,q_{0}\in Q_{0}\}\subseteq Q_{A}\}.}$

We call an event segment ${\displaystyle \omega \in {\underset {t\rightarrow \infty }{\lim }}\Omega _{Z,[0,t]}}$ an infinite-length behavior of ${\displaystyle {\mathcal {G}}}$, if ${\displaystyle \omega \in L({\mathcal {G}},\infty )}$.

State Transition System