定義
設AP是一組原子命題，即對變數，常量和謂詞符號的布爾表達式。 Clarke等人[3]在AP上定義Kripke結構為4元組M =（S，I，R，L）由...組成
一組有限的狀態S.
一組初始狀態I⊆S.
過渡關係R⊆S×S使得R是左總的，即∀s∈S∃s'∈S使得（s，s'）∈R。
標籤（或解釋）功能L：S→2AP。
由於R是左總數，因此總是可以通過Kripke結構構建無限路徑。死鎖狀態可以通過單個傳出邊緣建模回自身。標記函式L為每個狀態s∈S定義在s中有效的所有原子命題的集合L（s）。
結構M的路徑是狀態序列ρ= s1，s2，s3 ......，使得對於每個i> 0，R（si，si + 1）成立。路徑ρ上的單詞是一系列原子命題的集合w = L（s1），L（s2），L（s3），...，它是字母表2AP上的ω-字。
根據這個定義，Kripke結構（例如，只有一個初始狀態i∈I）可以用具有單例輸入字母表的Moore機器識別，並且輸出函式是其標記函式。
例子
設原子命題集合AP = {p，q}。 p和q可以模擬Kripke結構正在建模的系統的任意布爾屬性。
右圖說明了Kripke結構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可以產生路徑ρ= s1，s2，s1，s2，s3，s3，s3，...和w = {p，q}，{q}，{p，q}，{q}，{p} ，{p}，{p}，...是路徑ρ上的執行字。 M可以產生屬於語言的執行詞（{p，q} {q}）*（{p}）ω∪（{p，q} {q}）ω。
與其他概念的關係
儘管這個術語在模型檢查社區中很普遍，但是一些關於模型檢查的教科書沒有以這種擴展的方式定義“Kripke結構”（或者根本沒有），而只是使用（標記的）過渡系統的概念， 有一套行動法，過渡關係被定義為S×Act×S的一個子集，它們還擴展到包括一組原子命題和狀態的標記函式（如上定義的L）。 在這種方法中，通過抽象出動作標籤獲得的二元關係稱為狀態圖。
Clarke等人。 將Kripke結構重新定義為一組過渡（而不僅僅是一個），當它們定義模態μ演算的語義時，它等同於上面標記的過渡。
