TLA+
TLAには、一般的な演算子を含む一連の標準モジュールがある。それらは構文アナライザーで配布される。 TLCモデルチェッカーは、パフォーマンスを向上させるためにJava実装を使用する。
FiniteSets :有限集合を扱うためのモジュール。 IsFiniteSet(S)およびCardinality(S)演算子を提供する。
Sequences: Len(S)、Head(S)、Tail(S)、Append(S、E) 、連結、フィルターなどのタプルの演算子を定義する。
Bags: 多重集合を扱うためのモジュール。プリミティブな集合演算の類似物と重複カウントを提供する。
Naturals: 不等式および算術演算子とともに自然数を定義する。
Integers:整数を定義する。
Reals:実数と除算と無限大を定義する。
RealTime:リアルタイムのシステム仕様で役立つ定義を提供する。
TLC :ロギングやアサーションなど、モデルでチェックされた仕様のユーティリティ関数を提供する。
標準モジュールはEXTENDSまたはINSTANCEステートメントでインポートされる。
現代の時相論理は、1957年にアーサー・プライアーによって開発され、当時は時制論理と呼ばれていた。アミール・プヌーリが、コンピュータサイエンスへの時相論理の適用を真剣に研究した最初の人物だったが、アーサー・プライアーは1967年の10年前に既にその使用について予測していた。
プヌーリは、コンピュータープログラムの指定と推論における時相論理の使用を研究し、1977年に線形時相論理を導入した。 線形時相論理は、排他制御やデッドロックの解決などの特性を簡単に表現する、並行プログラムの分析のための重要なツールとなった。
プヌーリの線形時相論理に関する研究と同時に、学者はマルチプロセスプログラムの検証のためにホーア論理を一般化するために取り組んでいた。レスリー・ランポートは、ピアレビューで相互排除について提出した論文に誤りが見つかった後、この問題に関心を持つようになった。 Ed Ashcroftは、1975年の論文「Proving Assertions About Parallel Programs」で不変性を紹介した。これは、Lamportが1977年の論文「Proving Correctness of Multiprocess Programs」でFloydの方法を一般化するために使用した。ランポートの論文はまた、部分正当性と終了の一般化として、それぞれ安全性と活性を紹介した。 この方法は、EdsgerDijkstraによる1978年の論文で最初の同時ガベージコレクションアルゴリズムを検証するために使用された。