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

• [Zeigler76] Bernard Zeigler (1976). Theory of Modeling and Simulation (first ed.). Wiley Interscience, New York.
• [ZKP00] Bernard Zeigler; Tag Gon Kim; Herbert Praehofer (2000). Theory of Modeling and Simulation (second ed.). Academic Press, New York. ISBN 978-0-12-778455-7.
• [Hwang2012] Moon H. Hwang. "Qualitative Verification of Finite and Real-Time DEVS Networks". Proceedings of 2012 TMS/DEVS. Orlando, FL, USA. pp. 43:1–43:8. ISBN 978-1-61839-786-7.