概率時態(tài)知識邏輯的符號模型檢測研究.pdf

1、模型檢測作為一種自動驗證有限狀態(tài)系統(tǒng)是否滿足規(guī)范的形式化技術(shù)，在規(guī)劃和多智能體系統(tǒng)等人工智能領(lǐng)域得到了越來越多的應(yīng)用?，F(xiàn)在已經(jīng)開發(fā)出多個多智能體系統(tǒng)的模型檢測工具，如MCTK等。人工智能領(lǐng)域常遇到對具有概率特性的不確定信息進(jìn)行表示、推理和驗證的問題。智能體常常以一定概率相信某命題成立。雖然現(xiàn)今有較成熟的概率系統(tǒng)模型檢測工具，如PRISM等，但是它們不能表示智能體的知識，并不適合于多智能體系統(tǒng)。如今，在多智能體系統(tǒng)的研究中，缺乏對智能體在

2、不確定環(huán)境下對具有概率特性的信息的形式化描述和模型檢測方法。 本文重點研究具有概率特性的多智能體系統(tǒng)的規(guī)范表示及其模型檢測方法。提出概率認(rèn)知解釋系統(tǒng)，并在這一新的模型基礎(chǔ)上研究多智能體系統(tǒng)的概率時態(tài)知識邏輯的語義及符號模型檢測算法。提出的概率時態(tài)知識邏輯PECTLKn是在分支時態(tài)邏輯的存在片斷ECTL語言中加入表示智能體知識的S5n知識算子和表示智能體認(rèn)為事件發(fā)生概率的概率算子后得到的。該邏輯有豐富的概率、時態(tài)和認(rèn)知表達(dá)能力，用