將模型表示爲LTL

基本上，模型檢查處理模型'm'（系統的行爲描述）和屬性'p'，系統應滿足該模型。對於這兩種工件，模型檢查器都會確定模型是否滿足屬性。將模型表示爲LTL

我的問題是，是否可以將模型'm'指定爲LTL公式，並檢查作爲LTL'm'的模型是否滿足屬性'p'。

理論上，我認爲這種方法應該可行，因爲我們可以生成兩個Büchi自動機，一個用於LTL公式'p'，另一個用於描述模型'm'的LTL屬性。如果兩個非確定性自動機的交集爲空，則作爲LTL的模型'm'滿足該屬性。

有人可以給我一個提示嗎？可能嗎？

來源

2014-10-29 igi

有趣的問題：簡短的答案可能不是。模型檢驗期間通常

，執行LTL到步琪自動機的轉換。這是可能的，因爲LTL比Buchi自動機不那麼富有表現力。但是，如果您有一些預先存在的設計，則不太可能在LTL中捕獲它。例如，當設計具有許多狀態時，這可能是LTL中的問題。

2015-02-05 00:09:12 adrianX

回答