discrete-time trajectories. The state $x$ (e.g., representing the susceptible, exposed, infectious, recovered population of a certain region) belongs to the domain $\mathcal{X}\subset\mathbb{R}^n$. The time set is $\mathbb{T} = \mathbb{R}_{\ge0}$. The domain $\mathbb{B} = \{\textrm{True}, \textrm{False}\}$ is the Boolean domain, and the time index set is $\mathbb{I} = \{0,1,\dots\}$. We use $t[k]\in\mathbb{T}$ to denote the time instant at time index $k\in\mathbb{I}$ and $x[k]\triangleq x(t[k])$ to denote the value of $x$ at time $t[k]$. With slight abuse of notation, we use $\xi$ to denote a trajectory as a function from $\mathbb{T}$ to $\mathcal{X}$. A set $AP$ is a set of atomic propositions, each mapping $\mathcal{X}$ to $\mathbb{B}$. The syntax of MTL is defined recursively as follows: $$\varphi:=\top\mid \pi\mid\lnot\varphi\mid\varphi_{1}\wedge\varphi_{2}\mid\varphi_{1}\vee
\varphi_{2}\mid\varphi_{1}\mathcal{U}_{\mathcal{I}}\varphi_{2},$$ where $\top$ stands for the Boolean constant True, $\pi\in AP$ is an atomic proposition, $\lnot$ (negation), $\wedge$ (conjunction), $\vee$ (disjunction) are standard Boolean connectives, $\mathcal{U}$ is a temporal operator representing until, $\mathcal{I}$ is a time index interval of the form $\mathcal{I}=[i_{1},i_{2}]$ ($i_1\le i_2$, $i_1, i_2\in\mathbb{I}$). We can also derive two useful temporal operators from until ($\mathcal{U}$), which are eventually $\Diamond_{\mathcal{I}}\varphi=\top\mathcal{U}_{\mathcal{I}}\varphi$ and always $\Box_{\mathcal{I}}\varphi=\lnot\Diamond_{\mathcal{I}}\lnot\varphi$. For example, the MTL formula $\Box_{[0,100]} (DeathsPerDay\le 0.001)\wedge\Diamond_{[40, 60]}(Recovered\ge6)$ means “the deaths from infection should never exceed 0.001 million (one 