# Programming with Linear Temporal Logic Operators

At Matrix AI our research into language constructs for formally describing distributed systems has led us to a concept called Linear Temporal Logic. It is a logic system that allows us to express logical statements about time. This article will provide a brief introduction to this logic system.

Linear Temporal Logic takes the basic ideas of Propositional and Predicate logic and introduces concepts about time.

Predicate logic is widely used for automatically checking and proving theorems, verifying software correctness and security, and is the foundation of the programming language ProLog.

In Linear Temporal Logic (LTL), we can express statements about things that are true. Our expression will have both
English word variants and also operator variants. The simplest statement is simply `A`

. This means that `A`

is true
right now. We can also write that `A`

will be true from now on and to the future, and that can be expressed
as `Forever A`

or □A. If `A`

will be true eventually, we can write `Eventually A`

or ◇A. Notice that `Not Forever Not A`

is the same as `Eventually A`

or ¬□¬A≡◇A. This is because if `A`

won't always be false then `A`

will eventually be true.
If we model time as discrete moments, we can say that `A`

will be true in the next moment, and write it as `Next A`

or
◯A.

There are more sophisticated operators too, such as `A Until B`

or A U B, which means `A`

is true until `B`

is true,
and `Eventually B`

. This can be written recursively as A U B ≡ B∨(A∧◇B∧◯(A U B)). There is also a weaker version
of `Until`

, denoted A W B, where `B`

need not occur. We can write A W B ≡ □A ∨ (A U B).

There is a strong parallel between Propositional Logic and Functional Programming. Let's use Haskell as an example. If
the formulas `A`

and `B`

are types then A∧B can be written the pair `(A,B)`

, A∨B can be written as `Either A B`

, and
if `A`

implies `B`

, we use the function type `A -> B`

. Now function application looks like Modus Ponens, the
distributivity laws look like alternative representations of the same types, and formal proofs look like Haskell
programs.

As for the modal operators of linear temporal logic, we have to look at Functional Reactive Programming. `Forever A`

is
an unending stream of values of type `A`

, `Eventually A`

is a container that will eventually yield a value of type `A`

,
and `A Until B`

is a stream of type `A`

terminated with a value of type `B`

. Using these types, IO operations can have
types like `Forever (Int, Int)`

for mouse position, `Eventually Bytestring`

for receiving network data,
and `Char `Until` Nothing`

for standard input.

Evan Czaplicki's Paper goes over the many attempts to implement Functional Reactive Programming. However, for distributed systems, a complete functional reactive language is unnecessary. Instead, we can learn from Arrowised FRP, and model processes as Signal Functions. This model may help us describe the distributed services that Matrix is orchestrating.