基于知識(shí)的協(xié)議驗(yàn)證方法及工具.pdf

1、該文主要研究利用知識(shí)邏輯進(jìn)行協(xié)議驗(yàn)證的問題.一直以來,高效無二意的通信協(xié)議是人們進(jìn)行有效的遠(yuǎn)距離通信交流的基礎(chǔ),設(shè)計(jì)高效無二意的通信協(xié)議是一項(xiàng)極具挑戰(zhàn)性的工作.通信協(xié)議的效率可以通過設(shè)計(jì)高效的編碼方案或發(fā)明新型高速傳輸媒質(zhì)來提高;而無二意的通信協(xié)議必須滿足在一定的執(zhí)行環(huán)境中,所有可能發(fā)生的情況下,協(xié)議執(zhí)行的結(jié)果唯一確定.該文集中討論了如何驗(yàn)證一個(gè)設(shè)計(jì)好的通信協(xié)議是無二意的,即協(xié)議驗(yàn)證問題.這一問題也是一個(gè)極具挑戰(zhàn)性的問題,并且至今還沒有

2、一個(gè)完美的解決方案.傳統(tǒng)的協(xié)議驗(yàn)證方法多基于時(shí)態(tài)邏輯,主要考察系統(tǒng)在執(zhí)行協(xié)議時(shí)在時(shí)間序列上所具有的性質(zhì).引入多智能體系統(tǒng)后,協(xié)議的執(zhí)行不僅受時(shí)間的影響,還與智能體的知識(shí)狀態(tài)有關(guān).在多智能體系統(tǒng)中考察協(xié)議的執(zhí)行,不僅可以從時(shí)間序列上考慮,還可以從系統(tǒng)中的智能體執(zhí)行協(xié)議后,所具有的知識(shí)發(fā)生變化這個(gè)角度去考慮.這正是該文討論的切入點(diǎn),該文在傳統(tǒng)的基于時(shí)態(tài)邏輯的協(xié)議驗(yàn)證方法基礎(chǔ)上,引入知識(shí)邏輯,借助多智能體系統(tǒng)的知識(shí)模型,以新的視角研究協(xié)議,并