行動の時間的論理

時相アクション論理( TLA ) は、 Leslie Lamportによって開発された、時相論理とアクション論理を組み合わせた論理です。並行システムおよび分散システムの動作を記述するために使用されます。仕様言語TLA+ の基礎となる論理です。

アクションの時相論理におけるステートメントは という形式です。ここで、Aはアクションであり、tにはAに現れる変数のサブセットが含まれます。アクションは、 のように、プライム付き変数とプライムなし変数を含む式です。プライムなし変数の意味は、この状態 における変数の値です。プライム付き変数の意味は、次の状態 における変数の値です。上記の式は、今日のxの値に、明日のxの値と今日のyの値を掛けたものを加えると、明日のyの値に等しいことを意味します。 ${\displaystyle [A]_{t}}$${\displaystyle x+x'*y=y'}$

の意味は、 A が現在有効であるか、またはtに現れる変数が変更されない ということです。これにより、プログラム変数の値がまったく変更されないスタッター ステップが可能になります。${\displaystyle [A]_{t}}$

Temporal Logic of Actions を実装する仕様言語は複数あります。各言語には独自の機能と使用例があります。

TLA+ は、TLA のデフォルトであり、最も広く使用されている仕様言語です。これは、並行システムと分散システムの動作を記述するために設計された数学言語です。仕様は関数型スタイルで記述されています。

----------------------------- モジュール HourClock -----------------------------
エクステンドナチュラル

変数 時間

初期値 == 時間 = 1

次へ == 時間' = 時間 = 12 の場合 1 それ以外の場合 時間 + 1

仕様 == 初期化 /\ [][次へ]_時間
================================================= ===========================

PlusCal は、TLA+ に変換される高水準アルゴリズム言語です。ユーザーは、使い慣れた疑似コードのような構文でアルゴリズムを記述でき、その後、自動的に TLA+ 仕様に変換されます。このため、PlusCal は、状態マシンではなくアルゴリズムの観点から考えることを好むユーザーに最適です。

----------------------------- モジュール HourClock ----------------------
エクステンドナチュラル

(*--アルゴリズム HourClock {
    変数 hour = 1;
    {
        (TRUE) の間 {
            時間 := (時間 % 12) + 1;
        }
    }
} --*)

Quint は、TLA+ に変換される別の仕様言語です。Quint は、Temporal Logic of Actions (TLA) の堅牢な理論的基礎と、最先端の型チェックおよび開発ツールを組み合わせています。PlusCal とは異なり、Quint の演算子とキーワードは TLA+ に 1 対 1 で変換されます。

FizzBee ^[1]は、分散システムに取り組む主流のソフトウェアエンジニアに形式手法をもたらすために設計された、Pythonのような構文を使用する高レベル仕様言語です。Temporal Logic of Actionsに基づいていますが、PlusCalやQuintとは異なり、内部でTLA+に変換したり使用したりすることはありません。

アクション 初期化:
  時間 =  1

アトミック アクション チェック: 
  # アクションの本体はStarlark（Python方言）です
  hour  =  ( hour  %  12 )  +  1

• 時間的論理
• プラスカル
• TLA+

• ランポート、レスリー (2002)。システムの仕様: ハードウェアおよびソフトウェア エンジニア向けの TLA+ 言語とツール。Addison- Wesley。ISBN 0-321-14306-X。
• レスリー・ランポート (1994 年 12 月 16 日)、TLA 入門(PDF) 、 2010 年 9 月 17 日取得
• 「分散システム、マイクロサービス、クラウドアプリケーションを開発する開発者にとって、これまでで最も簡単な形式手法言語」 。 2024年5月28日閲覧。

• 公式サイト
• 「TLA+ 証明システム」。INRIA。
• ランポート、レスリー (2014)。「プログラマのための思考」。BuildでのTLA+ の簡単な紹介
• 「FizzBee ウェブサイト」。
• 「Quint Git リポジトリ」。