G. Hariharan, B. Kempa, T. Wongpiromsarn, P. H. Jones and K. Y. Rozier, MLTL Multi-type: A logic to reason over signals of different types, In Proceedings of the 15th International Workshop on Numerical Software Verification (NSV), August, 2022
[BibTeX] [PDF]

@inproceedings{Hariharan2022,
  author = {Gokul Hariharan, Brian Kempa, Tichakorm Wongpiromsarn, Phillip H. Jones, Kristin Y. Rozier},
  title = {MLTL Multi-type: A logic to reason over signals of different types},
  booktitle = {In Proceedings of the 15th International Workshop on Numerical Software Verification (NSV)},
  year = {2022},
  pdf = {//research.temporallogic.org/papers/NSV22.pdf}
}

MLTL Multi-type: A logic to reason over signals of different types

Full proof of Theorem 1

\[ \begin{equation}\label{eq:semantics} \sigma^\mathbb A[i] := \begin{cases} \pi_p^\mathbb{A}[i] &\text{if } \phi = p\\ \neg \sigma_1^\mathbb A[i] &\text{if } \phi = \neg \phi_1\\ \sigma_1^\mathbb{A}[i] \wedge \sigma_2^\mathbb{A}[i] &\text{if } \phi = \phi_1 \wedge \phi_2\\ \sigma_1^\mathbb{A}[i..]\; \mathrm U_{[lb,ub]} \sigma_2^\mathbb{A}[i..] &\text{if } \phi = \phi_1 \mathrm U_{[lb,ub,\mathbb{A}]} \phi_2\\ \end{cases} \end{equation} \]

\[ \begin{equation}\label{eq:projection} T_\mathbb{A}^\mathbb{B}(\sigma^\mathbb{A}) = \sigma^\B \end{equation} \]

The semantics are expressed in terms of signals, and we say that a formula \(\phi\) generates a signal, denoted by \(\phi \mapsto \sigma\).

As discussed in Section 3.2 of the paper, an MLTLM formula has many possible evaluations based on the placement of projections. We consider a specific placement of projections so that one formula has a single interpretation - the nearest ancestor type imposition as discussed in Section 4 of the paper. Furthermore, we consider a subset of MLTLM formulas that have a temporal operator at its AST's root (see Section 4 in the paper), and the output signal type is assumed to be the same as the type of this temporal operator.

Lemma 1 (Adequate set of MLTL) The operators \(\neg\), \(\wedge\) and \(\square\) form an adequate set, i.e., any MLTL formula can be equivalently expressed exclusively with these operators.

Proof: In propositional logic the adequate set is {\(\neg\),\(\wedge\)}, and this extends directly to temporal logic as well. We need to only show that any formula \(\phi_1 \mathcal U_{[lb,ub]} \phi_2\) can be equivalently expressed in MLTL using only the \(\square\) operator. It is trivial to show from the definition of the until operator that,

\[ \begin{align*} \phi_1 \mathcal U_{[lb,ub]} \phi_2 \;=\;& \square_{[lb,lb]}\phi_2 \\ \; \; \; \vee (&\square_{[lb,lb]} \phi_1 \wedge \square_{[lb+1,lb+1] }\phi_2)\\ \; \; \;\vee (&\square_{[lb,lb+1]} \phi_1 \wedge \square_{[lb+2,lb+2] }\phi_2)\\ \; \; \;\vee (&\square_{[lb,lb+2]} \phi_1 \wedge \square_{[lb+3,lb+3] }\phi_2)\\ &\; \; \; \vdots \\ \; \; \;\vee (&\square_{[lb,ub-1]} \phi_1 \wedge \square_{[ub,ub] }\phi_2),\\ \;=\;& \neg (\neg \square_{[lb,lb]}\phi_2 \\ \; \; \; \wedge \neg (&\square_{[lb,lb]} \phi_1 \wedge \square_{[lb+1,lb+1] }\phi_2)\\ \; \; \;\wedge \neg (&\square_{[lb,lb+1]} \phi_1 \wedge \square_{[lb+2,lb+2] }\phi_2)\\ \; \; \;\wedge \neg (&\square_{[lb,lb+2]} \phi_1 \wedge \square_{[lb+3,lb+3] }\phi_2)\\ &\; \; \; \vdots \\ \; \; \;\wedge \neg (&\square_{[lb,ub-1]} \phi_1 \wedge \square_{[ub,ub] }\phi_2)) \end{align*} \]

Definition 1 (Logical projection) Consider a formula \(\phi = \square_{[lb,ub,\mathbb D]} \phi_1 \) where \(\phi_1 \mapsto \sigma^t\), where \(t \neq \mathbb D\). Let there exist a projection \(T_{t}^\mathbb D\) to match type \(\mathbb D\). The projection is called a logical projection if there exists a function \(p: \Phi \rightarrow \Phi\) such that \((p(\phi) \mapsto \sigma^t) \Leftrightarrow (\phi \mapsto \sigma^{\mathbb D})\) and \(p(\phi)\) has the closest descendent type of \(t\), where \(\Phi\) is the set of MLTLM formulas.

The closest descendant type of a formula is the type on the closest child from the its AST's root (inclusive). For example, the closest descendant type of \(\square_{[1,2,\mathbb A]} (p \wedge q)\) is \(\mathbb A\). The closest descendant types of \(\square_{[1,2,\mathbb A]} (p) \wedge \square_{[1,2,\mathbb B]}(q)\) are \(\mathbb A\) and \(\mathbb B\).

Theorem 1 (Expressive Equivalence of MLTL and MLTLM with Logical Projections) Let \(F\) be a logical projection. Let \(\mathbb A\) be a type and \(\psi\) be an MLTL formula that outputs signals of type \(\mathbb A\). For every MLTLM formula \(\phi\) such that for every type \(t\) in \(\phi\) there exists a chain of logical projections from \(t\) to \(\mathbb A\), the signal generated by \(\phi\) is equivalent to another signal generated by \(\psi\).

The proof is completed by using induction on the structure of the formula in cunjunction with Lemma 1.

\[ (\phi \mapsto \sigma^\mathbb D) \Leftrightarrow (\psi \mapsto \sigma^\mathbb A) \]

i.e., an MLTLM formula \(\phi\) that generates a signal \(\sigma^\mathbb D\) is equivalent to an MLTL formula \(\psi\) that generates a signal of type \(\mathbb A\), given that we have a chain of logical projections, and that the all the atomic propositions generate signals of the same type, \(\mathbb A\).

Cases (a) and (b) directly follow from the MLTLM semantics. As for Case (c), we assumed the existence of a chain of logical projections. Which means for Case (c) any formula \(\phi = \square_{[lb,ub,t]} \phi_1\) where \(\phi_1\mapsto t'\), such that \(t’ \neq t\), there exists a function \(p(\phi)\) such that \((p(\phi) \mapsto t’) \Leftrightarrow (\phi \mapsto t)\). But from the hypothesis, it is clear that \(t’ = \A\).

\[ \begin{equation}\label{eq:qphi} q(\phi) := \begin{cases} \phi, & \text{if } \phi \text{ has only one type, \(\mathbb A\) in the entire formula},\\ p(\,\square_{[lb,ub,t]} q(\phi_1)\, ), & \text{if } \phi = \square_{[lb,ub,t]} \phi_1 \text{ and } t \neq \mathbb A,\\ \square_{[lb,ub,\mathbb A]} q(\phi_1), & \text{if } \phi = \square_{[lb,ub,\mathbb A ]} \phi_1,\\ \neg q(\phi_1), & \text{if } \phi = \neg \phi_1,\\ q(\phi_1) \wedge q(\phi_2), & \text{if } \phi = \phi_1 \wedge \phi_2. \end{cases} \end{equation} \]

where we use a slight abuse of notation for the function \(p\) to represent any of the different, but respective functions of corresponding logical projections. This completes the proof.

We derive the logical function for the modulo-reduction projection presented in the paper as an example. The modulo-reduction function \(f_s: \sigma^\mathcal{A} \rightarrow \sigma^\mathcal{B}\), where \(\sigma^\mathcal A\) and \(\sigma^\mathcal B\) are the sets of all signals of types \(\A\) and \(\B\) respectively, implements the projection \(T_\mathbb{A}^\mathbb{B}(\sigma^\mathbb{A})\) with positive integer stride \(s\) such that,

\[ \begin{align}\label{eq:moduloReduction} f_s(\sigma^\mathbb A) = \sigma^\mathbb B \text{ such that }\sigma^\mathbb B [i] = \sigma^\mathbb A [i \cdot s] \end{align} \]

Let, \(\phi = \square_{[lb,ub,\mathbb B]} \phi_1\) and \(\phi \mapsto \sigma^\mathbb B\) and let \(\phi_1 \mapsto \sigma^\mathbb A\), we have

\[ \begin{align*} &\sigma^\mathbb B [i] = \square_{[lb,ub,\B ]} \sigma^\B_1 [i ..],\\ \Leftrightarrow\;\; & \sigma^\mathbb B [i] = \tru \text{ if } \forall j \in [i+lb, i+ ub],\; \sigma^\B_1 [j] = \tru,\\ \Leftrightarrow\;\; & \sigma^\mathbb B [i] = \tru \text{ if } \forall j \in [i+lb, i+ ub],\; \sigma^\A [j \, s] = \tru,\\ \Leftrightarrow\;\; & \sigma^\mathbb B [i] = \tru \text{ if } \forall j’ \in [i'+lb\, s, i'+ ub\, s ,\, s],\; \sigma^\A [j'] = \tru,\\ \Leftrightarrow\;\; & \sigma^\mathbb A [i'] = \square_{[lb\, s,lb\, s]} (\sigma^\A[i'] \wedge \square_{[s,s]} \sigma^\A[i'] \wedge \square_{[2s,2s]}\sigma^\A[i'] \wedge \; \cdots \; \wedge \square_{[ub-lb,ub-lb]} \sigma^\A[i'] ), \end{align*} \]

On using the formula notation, we have that \((p(\phi) \mapsto \sigma^\A) \Leftrightarrow (\phi \mapsto \sigma^\B)\) where

\[ p(\phi) \;= \; \square_{[lb\, s,lb\, s, \A]} (\phi_1 \wedge \square_{[s,s,\A]} \phi_1 \wedge \square_{[2s,2s,\A]}\phi_1 \wedge \; \cdots\;\wedge \square_{[ub-lb,ub-lb,\A]} \phi_1 ). \]