你如何閱讀一組原子命題？

Question

我給出了原子命題{a，b，c}的上述系統。

然後，我打算說某些LTL公式是否成立（如♢☐c）。

我瞭解LTL公式的含義（最終永遠保持c），但我不知道如何閱讀該圖並將其與LTL關聯起來。

我假設它就像一個流程圖，我們從左上角開始，/{a}，可以通過不同的狀態。但是它們每個意思除以a？

Answer 1

看起來像FSM /轉換器而不是Kripke結構。輸入/輸出或更一般的先決條件/後置條件是FSM及其親屬的通用符號。先決條件/後置條件(a and b and ...)/(x and y and...)。所以a在q1的狀態。在接下來的狀態中，第四季度只有b或b and c或q3。可能當然是or而不是and在前提條件下，否則系統可能會停頓..