我目前正在寫我的碩士論文，面臨在時間邏輯中指定和驗證我的方法。我將很快解釋基本情況，但可以隨時索要詳細信息;-)基本上我想知道哪種時態邏輯最適合我的情況，並且真的很想反饋我的方法以及如何繼續。用於模型建模的LTL，CTL或TLA（內部有詳細說明）？
我的模型由參與者組成，它們將同時執行。對於每個參與者，都可以註冊規則。他們看起來像這樣： 條件 - >動作，例如收到（a，c）^收到（b，c） - >允許（c，d）這意味着c必須從b收到一條消息，並從c收到一條消息才能被允許向d發送消息。 在其中一個參與者發送或接收消息之前，我的原型會檢查參與者是否被允許執行該操作。到目前爲止，我想驗證算法是否執行以下操作： 1.如果不存在條件成立的規則：禁止該動作 2.如果存在條件成立並且禁止該動作的規則：禁止該動作 3如果存在規則，其條件成立，它允許動作並沒有其他的規則存在，其條件成立，禁止動作：讓行動
親切的問候給你所有的， 魯迪又名nanoquack
它看起來像你想知道你的規範的某些屬性是不變量。也就是說，如果在程序執行期間屬性總是爲真的。
不變量的概念可以表示在所有的時態邏輯形式。不過，我會使用TLA+，因爲有一個模型檢查器，一個可用的證明系統，一個活躍的社區和一些編寫規範的優秀書籍。
但是......要知道，時態邏輯不是小菜一碟，你需要花一些時間仔細閱讀和思考。
比較這三種邏輯存在一種誤解。 TLA +和LTL都是線性邏輯。 TLA +是一個基於Zermelo-Fraenkel set theory的公理理論，並且在語法上實施了口吃不變性（以確保改進是實用的）。 LTL是一種命題邏輯。
CTL是從LTL截然不同的，因爲CTL是分支時間邏輯，而LTL一個線性時間的邏輯。單個序列是線性時間公式的模型。相反，樹是分支時間公式的模型。一個序列表示一次執行，而一棵樹表示許多執行，以某種狀態開始。路徑量化在CTL中可用，而在LTL中不存在。 LTL和CTL有一個共同的子集，但它們是無法比擬的（=僅在LTL中可以表達某些屬性，而其他屬性僅在CTL中表示）。 CTL *是它們的共同超集。
對於您勾畫的應用程序，線性時間語義顯得更合適。我建議使用TLA +，因爲它爲描述系統提供了一個良好的規則，並且在時間上足夠的表達，以至於您可能不需要LTL（反之亦然：如果您無法在系統中指定具有口吃不變式的系統TLA +，那麼系統更有可能需要修訂，而不需要LTL的完整表達能力）。
TLA+ book是一個非常可讀的介紹所有級別的說明符。