Title: Theory / Unimportant / CS / Fundamental / Model Checking / MTL / A clock-optimal hierarchical monitoring automaton construction for MITL

Name: The continuous representation of \(\sigma\)
Definition: [$]\defFun{\mathbb R_{\ge0}}{\Sigma\cup\{\delta\}}{t}{\begin{array}{ll}a_i&\text{ if }t=t_i\\\delta&\text{ otherwise}\end{array}}[/$]
Variables: \(\Sigma\) an alphabet
\(\sigma=((a_i,t_i))_i\) a timed word

Question: How to rewrite \(\psi_1\mathcal U_{\mid a,b\mid}\psi_2\) with monadic operators and untimed until.
Answer: \(\diamond_{\mid a,b\mid}\psi_2\land\square_{[0,a\mid}(\psi_1\land(\psi_1\mathcal U\psi_2))\)
Page: 3
Variables: \(\Sigma\) an alphabet
\(\psi_1,\psi_2\) MITL-formula
\(0<a<b\)

Question: How to rewrite \(\psi_1\mathcal U_{\mid0,b\mid}\psi_2\) with monadic operators and untimed until
Answer: \((\diamond_{\mid0,b\mid}\psi_2)\land(\psi_1\land(\psi_1\mathcal U\psi_2))\)
Variables: \(\Sigma\) an alphabet
\(\psi_1,\psi_2\) MITL-formula
\(0<b\)

Name: Timed edge Büchi automaton
Definition: \(Q\) a finite set of states
Page: 4
Definition2: \(\Sigma\) the alphabet
Conjdef: The tuple
Definition3: \(C\) a finite set of clocks
Definition4: \(E\subseteq Q\times(\Sigma\cup\{\epsilon\})\times\Phi(C)\times2^C\times Q\) a finite set of edgse
Definition5: \(S\subseteq E\) a set of initial edges
Definition6: \(F\subseteq E\) a set of final edges
Definition7: \(tcp:C\to\Phi(C)\) the "Time can progress" condition on states

Name: A (non necessarily valid) run of \(\mathcal A\)
Definition: \(\rho:\mathbb R_{\ge0}\to Q\cup E\)
Page: 4
Variables: \(\mathcal A=(Q,\Sigma,C,E,S,F,tcp)\) a timed edege Büchi automaton
\(\sigma=((a_i,t_i))_i\)
Definition2: \(\nu:\mathbb R_{\ge0}\to\Phi_C\)
Conjdef: both
DefType: The pair

Name: A valid run of \(\mathcal A\) on \(\sigma\)
Definition: \(T\subseteq U\)
Page: 4
Variables: \(\mathcal A=(Q,\Sigma,C,E,S,F,tcp)\) a timed edege Büchi automaton
\(\sigma=((a_i,t_i))_i\)
\((\rho:\mathbb R_{\ge0}\to Q\cup E, \nu:\mathbb R_{\ge0}\to\Phi(C))\) a (non necessarily valid) run of \(\mathcal A\)
Definition2: \(\rho(t)\in E\) iff \(t\in U\)
Conjdef: There exists \(U=\{u_0,u_1,\dots,\}\) increasing
Definition3: \(\rho(t)\) is of the form \((q,a_i,g,X,q')\) iff \(t=t_i\)
Definition4: \(\rho(t)\) is of the form \((q,\epsilon,g,X,q')\) iff \(t\in U-T\)
Definition5: \(\rho(u_0)\in S\)
Definition6: if \(t\not\in U\) then \(\nu(t)\models tcp(\rho(t))\)
Definition7: if \(\rho(u_i)=(q,a,g,X,q')\) then \(\rho(t)=q'\) for \(t\in(u_i,u_{i+1})\) and \(\rho(u_{i+1}=(q',a',g',X',q'')\)