Oliver Scarlet

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…