模型檢測(cè)OBS觀察和SPR觀察下的知識(shí).pdf

1、該文主要研究有限狀態(tài)系統(tǒng)中的模型檢測(cè)知識(shí)的問(wèn)題.關(guān)于智能體知識(shí)的計(jì)算在不同的觀察下計(jì)算方法不同,該文研究了在OBS(Observational)觀察和SPR(Synchronous Perfect Recall)觀察下的模型檢測(cè)知識(shí)的問(wèn)題.在OBS觀察下,通過(guò)尋找與知識(shí)等價(jià)的局部命題來(lái)求解知識(shí),論文提出了利用描述有限狀態(tài)系統(tǒng)的程序語(yǔ)義來(lái)計(jì)算知識(shí)的方法.在CTL語(yǔ)言的基礎(chǔ)上定義了CTLK(Computation Tree Logic an

2、d Knowledge)語(yǔ)言的語(yǔ)法和語(yǔ)義,用它來(lái)描述KMAS(Knowledge based Multi-Agent System)的規(guī)格.并提出了符號(hào)化模型檢測(cè)這種規(guī)格的技術(shù).在SPR觀察下,通過(guò)形式化描述系統(tǒng)中的智能體怎樣利用它的記憶來(lái)判斷當(dāng)前的可能狀態(tài).在文章給出了利用符號(hào)化模型檢測(cè)技術(shù)計(jì)算SPR觀察下的智能體知識(shí)的算法.該文的實(shí)現(xiàn)部分MCLKT(Model Checking Limited Knowledge and Time)