A simple model of temporal logic is via time-indexed truth functions. This lets us model the Boolean connectives, as well as the next-step operator and modal always operator:

$$ \begin{array}{lclll} n & \models & P & \iff & \mbox{condition}\\\hline n & \models & \top & \iff & \mbox{always} \\ n & \models & P \land Q & \iff & n \models P \mbox{ and } n \models Q \\ n & \models & \lnot P & \iff & n \not\models P \\ n & \models & X(P) & \iff & n+1 \models P \\ n & \models & G(P) & \iff & \forall k.\; n + k \models P \\ \end{array} $$

Thinking of this in terms of the Kripke-Joyal semantics for modal logic leads us to observe that the natural numbers, viewed as a discrete category, are monoidal with addition, and so the Day tensor product exists. Specializing the definitions gives us the following forcing clauses:

$$ \begin{array}{lclll} n & \models & P & \iff & \mbox{condition}\\\hline n & \models & P \otimes Q & \iff & \exists j, k.\; j + k = n \mbox{ and } j \models P \mbox{ and } k \models Q \\ n & \models & P \multimap Q & \iff & \forall k.\; k \models P \mbox{ implies } n + k \models Q \\ \end{array} $$

So we have an adjunction between $\otimes$ and $\multimap$. Namely, we can show that $P \otimes Q \vdash R$ if and only if $P \vdash Q \multimap R$.

My questions are:

  1. This structure is surely well-known to students of temporal logic. What is it called, and what is the standard temporal logic notation for it?
  2. What is it used for? (I.e., what are some applications?)
  • 1
    $\begingroup$ I don't think these connectives make much sense in the context of LTL. The naturals are only names for the points in time, so the semantics of a formula should be independent from their numeric value. $\endgroup$ – Jan Johannsen Feb 2 '17 at 17:25
  • $\begingroup$ @JanJohannsen: LTL orders times, and $x \leq y$ if and only if $\exists z.\; x + z = y$. As a result, some traditional LTL connectives are encodable using the monoidal structure. Eg, the globally operator $G(X) = \top \multimap X$, and the past-time connective is $F^{-1}(X) = \top \otimes X$. This doesn't mean it makes sense, but it doesn't obviously not make sense. :) $\endgroup$ – Neel Krishnaswami Feb 2 '17 at 17:32
  • 4
    $\begingroup$ Maybe, but usually LTL formulas are invariant under suffixes, i.e., if I forget about states 0 to 3, and rename all states $n\geq 4$ by $n-4$, then the same formulas are valid in these states. That does not hold for your proposed connectives. $\endgroup$ – Jan Johannsen Feb 2 '17 at 17:39
  • 2
    $\begingroup$ ... And invariant under suffixes: e.g., we may extend the model from N to Z without changing the existing valuation of formulas. $\endgroup$ – Emil Jeřábek Feb 2 '17 at 18:52
  • $\begingroup$ @JanJohannsen Thanks! That is a good reason. If you make an answer I will accept it. Are there any other similar kinds of properties people think LTL formulas should satisfy? $\endgroup$ – Neel Krishnaswami Feb 3 '17 at 10:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.