[科普中國]-克里普克結(jié)構(gòu)

克里普克結(jié)構(gòu)（Kripke structure）是過渡系統(tǒng)的變體，最初由Saul Kripke提出，用于模型檢查來表示系統(tǒng)的行為。 它基本上是一個圖，其節(jié)點表示系統(tǒng)的可達狀態(tài)，其邊表示狀態(tài)轉(zhuǎn)換。 標記函數(shù)將每個節(jié)點映射到一組保持在相應狀態(tài)的屬性。 時間邏輯傳統(tǒng)上用Kripke結(jié)構(gòu)來解釋

定義設AP是一組原子命題，即對變量，常量和謂詞符號的布爾表達式。 Clarke等人[3]在AP上定義Kripke結(jié)構(gòu)為4元組M =（S，I，R，L）由...組成

一組有限的狀態(tài)S.

一組初始狀態(tài)I?S.

過渡關系R?S×S使得R是左總的，即?s∈S?s'∈S使得（s，s'）∈R。

標簽（或解釋）功能L：S→2AP。

由于R是左總數(shù)，因此總是可以通過Kripke結(jié)構(gòu)構(gòu)建無限路徑。死鎖狀態(tài)可以通過單個傳出邊緣建?；刈陨怼擞浐瘮?shù)L為每個狀態(tài)s∈S定義在s中有效的所有原子命題的集合L（s）。

結(jié)構(gòu)M的路徑是狀態(tài)序列ρ= s1，s2，s3 ......，使得對于每個i> 0，R（si，si + 1）成立。路徑ρ上的單詞是一系列原子命題的集合w = L（s1），L（s2），L（s3），...，它是字母表2AP上的ω-字。

根據(jù)這個定義，Kripke結(jié)構(gòu)（例如，只有一個初始狀態(tài)i∈I）可以用具有單例輸入字母表的Moore機器識別，并且輸出函數(shù)是其標記函數(shù)。

例子設原子命題集合AP = {p，q}。 p和q可以模擬Kripke結(jié)構(gòu)正在建模的系統(tǒng)的任意布爾屬性。

右圖說明了Kripke結(jié)構(gòu)M =（S，I，R，L），其中

S = {s1，s2，s3}。

I= {s1}。

R = {（s1，s2），（s2，s1）（s2，s3），（s3，s3）}。

L = {（s1，{p，q}），（s2，{q}），（s3，{p}）}。

M可以產(chǎn)生路徑ρ= s1，s2，s1，s2，s3，s3，s3，...和w = {p，q}，{q}，{p，q}，{q}，{p} ，{p}，{p}，...是路徑ρ上的執(zhí)行字。 M可以產(chǎn)生屬于語言的執(zhí)行詞（{p，q} {q}）*（{p}）ω∪（{p，q} {q}）ω。

與其他概念的關系盡管這個術語在模型檢查社區(qū)中很普遍，但是一些關于模型檢查的教科書沒有以這種擴展的方式定義“Kripke結(jié)構(gòu)”（或者根本沒有），而只是使用（標記的）過渡系統(tǒng)的概念， 有一套行動法，過渡關系被定義為S×Act×S的一個子集，它們還擴展到包括一組原子命題和狀態(tài)的標記函數(shù)（如上定義的L）。 在這種方法中，通過抽象出動作標簽獲得的二元關系稱為狀態(tài)圖。

Clarke等人。 將Kripke結(jié)構(gòu)重新定義為一組過渡（而不僅僅是一個），當它們定義模態(tài)μ演算的語義時，它等同于上面標記的過渡。

本詞條內(nèi)容貢獻者為:

李嘉騫 - 博士 - 同濟大學