Kripke結構

什麼是用於檢查Kripke結構上的不變量的（僞代碼）算法，以便在不變量被違反的情況下，算法返回的反例具有最小長度？Kripke結構

2013-01-23 Rinad Rama

您的kripke結構代表了什麼？這是一個明確的圖表嗎？ BDD？一套CNF公式？其中每一個都會有不同的答案。 – amit

http://en.wikipedia.org/wiki/Kripke_structure_(model_checking） –

我對Kripke結構很熟悉，但是雖然結構被抽象爲一個圖 - 但它很少在實踐中以這種方式實現。它通常以BDD的形式實現，甚至更常見的是一套CNF公式。 – amit

你沒有提供足夠的細節問題，但如果我不得不猜測，我會說你正在尋找breadth-first search。

2013-01-23 08:38:28

是的，但是如何通過廣度優先搜索獲得最小長度：/？ –

你甚至沒有告訴我們你如何測量長度，所以我們如何回答？ –

如果你在談論我認爲你在談論的事情（反例是某個圖中的路徑），那麼答案是：寬度優先搜索總是找到解決方案的路徑，長度最短，設計。 –

回答