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.