TLA+
他の時相演算子には、弱い公平性と強い公平性が含まれる。弱い公平を表すWFe(A)は、アクションAが連続して(つまり絶え間なく)有効になっている場合、それが最終的に実施される事を意味する。強い公平を表すSFe(A)アクションAは、(中断の有無にかかわらず、繰り返し)継続的に有効になっている場合は、それが最終的に実施される事を意味する。
ツールからのサポートはないが時相論的な存在記号と全称記号はTLAに含まれている。
ユーザー定義の演算子はマクロに似ている。演算子は、ドメインが集合である必要がないという点において関数とは異なる。たとえば、集合のメンバーシップ演算子は、そのドメインとして集合の圏を持つが、これはZFCでは有効な集合ではない(その存在はラッセルのパラドックスにつながるため)。再帰的で匿名のユーザー定義演算子がTLAに追加された。
TLAは、Leslie Lamportによって開発された形式仕様言語。並行システムと分散システムの設計、モデル化、文書化、および検証に使用される。 TLAは、網羅的にテスト可能な擬似コードとして説明されており、その使用はソフトウェアシステムの設計図を描くことに喩えられる。 TLAはTemporal Logic of Actionsの頭字語である。
設計と文書化に関して、TLA は非公式の技術仕様と同じ目的を果たす。ただし、TLAの仕様は論理学と数学の形式言語で記述されており、この言語で記述された仕様の精度は、システムの実装が始まる前に設計上の欠陥を明らかにすることを目的としている。
TLAのコードは形式言語で記述するため、有限モデル検査に適する。モデルチェッカーは、いくつかの実行ステップまでのすべての可能なシステム動作を見つけ、安全性や活性などの望ましい不変性プロパティの違反を調べる。 TLAのコードでは、基本的な集合論を使用して安全性(悪いことが起こらない事)を定義し、時相論理を使用して活性(良いことがいずれ起こる事)を定義する。