<p>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:</p>

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

<p>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 <a href="https://ncatlab.org/nlab/show/Day+convolution" rel="nofollow noreferrer">Day tensor
product</a>
exists. Specializing the definitions gives us the following forcing clauses:</p>

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

<p>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$.</p>

<p>My questions are:</p>

<ol>
<li>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?</li>
<li>What is it used for? (I.e., what are some applications?)</li>
</ol>

CC BY-SA 3.0
2017-02-02T17:25:47.777Z
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.
Jan Johannsen
CC BY-SA 3.0
2017-02-02T17:32:00.703Z
@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. :)
Neel Krishnaswami
CC BY-SA 3.0
2017-02-02T17:39:31.993Z
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.
Jan Johannsen
CC BY-SA 3.0
2017-02-02T18:52:41.347Z
... And invariant under suffixes: e.g., we may extend the model from N to Z without changing the existing valuation of formulas.
Emil Jeřábek
CC BY-SA 3.0
2017-02-03T10:20:28.223Z
@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?
Neel Krishnaswami
<lo.logic><semantics><temporal-logic><linear-logic><model-theory>
Applications of the monoidal closed structure in LTL?
Neel Krishnaswami
# Applications of the monoidal closed structure in LTL?

(Asked by: username_0 on 2017-02-02)

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](https://ncatlab.org/nlab/show/Day+convolution)
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?)

**Tags:** lo.logic, semantics, temporal-logic, linear-logic, model-theory

> **Comments:**
> **username_1**: 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.  
> **username_0**: @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. :)  
> **username_1**: 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.  
> **username_2**: ... And invariant under suffixes: e.g., we may extend the model from N to Z without changing the existing valuation of formulas.  
> **username_0**: @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?  

---

## 0 answers

