@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}
}

@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

Gokul Hariharan*, Brian Kempa, Tichakorn Wongpiromsarn, Phillip H. Jones, and Kristin Y. Rozier

This webpage contains further details and artifacts for reproducibility in “MLTL Multi-type: A logic to reason over signals of different types”

*gokul@iastate.edu

Implementation details

As you will see in the MLTLM semantics, a formula can correspond to infinitely many output signals for a given set of input signals generated by atomic propositions (see the paper and also the proof). An RV engine typically generates a single verdict per formula, so we use the following impositions so that given a set of input signals to a formula and projections, the formula generates a unique output signal.

The root node imposition

We consider MLTLM formulas that have the root node as a temporal operator, and impose that the output signal is direclty the signal generated from the root node with no further projections.

The closest ancestor type imposition

To match signal types in a binary propositional operator (\(\wedge,\vee\)), the signals are projected to the type on the closest ancestor of the operator in the AST representation.

The first imposition fixes the output signal type, and the second one fixes the placement of projections; once the projections between types are defined, the output signal is unique for a given formula.

Practical implications on the MLTLM RV engine

1. The first imposition implies that every formula must have a temporal operator at the root of its AST. In the MLTL monitor, a formula \(p\wedge q\) is sound, whereas in MLTLM \(p \wedge q\) represents a family of output signals. So, we require the user to instead use \(\square_{[0,0,\A]} (p\wedge q)\), where the temporal operator specifies the unique output signal type (\(\A\) in this case). Formulas without a temporal operator at the root is assigned the type \(\mathbb D\) by default in our implementation.

2. The MLTLM RV monitor gives you freedom to change the signal rate. Consider the formula \(\Diamond_{[0,364,\mathrm{day}]}\square_{[0,23,\mathrm{hour}]}p\). As we discuss in the paper the proposition \(p\) can generate a signal of any type (e.g., minutes, seconds, nanoseconds). If your sensor is generating a signal of a different rate, it will automatically be projected to an hourly rate before being further processed