模型檢測(cè)時(shí)態(tài)知識(shí)邏輯及其應(yīng)用.pdf

1、中山大學(xué)碩士學(xué)位論文模型檢測(cè)時(shí)態(tài)知識(shí)邏輯及其應(yīng)用姓名：何青申請(qǐng)學(xué)位級(jí)別：碩士專業(yè)：計(jì)算機(jī)軟件與理論指導(dǎo)教師：蘇開(kāi)樂(lè)20060606ModelCheckingTemporalLogicofKnowledgeandItsApplicationsMajor：ComputerSoftwareandTheoryName：HeQingSupervisor：Prof，KaileSuAbstractIntheareaofartificialintell

2、igenceandtheoreticalcomputerscience，researchershavepaidincrementalattentionstotheknowledgereasoningofmuhiagentsystemsduringtheneartenyearsTheyintendedtouselogicofknowledgetoformalizetheknowledgepropertiesofagents，andthen

3、verifyknowledgespecificationsofmulti—agentsystemswithformalmethodsModelcheckingasafullydevelopedtechnofogycaughtresearchers’eye，duetoitsexcellentperformanceofverifyinglargescalesystemsHowever，thistemporallogicbasedtechno

4、logywasnotconvenientlyappliedtotheverificationofknowledgelogicspecificationThus，someexpertscombinedthesetwologicsintothetemporallogicofknowledgemldthendevelopedvarionsmethodsandtoolsformodelcheckingitInthisthesis，we’vefi

5、rstintroducedsomeconceptionsofmodelcheckingandknowledgereasoningThenwe’vemainlyintroducedmytutor’SmethodofmodelcheckingtemporallogicofknowledgeLastlywe’veappliedthismethodtotwospecificareaswithonrtoolMCTK：oneproblemistov

6、erifythewinningstrategiesinthezerosumgames，whichistoautomaticallyfindoutwhetherthereexistsawayensuringthenecessarilywinofplayers；theotherproblemistoverifytheknowledgebasedsecurityprotocols，whosesecurepropertiesrelyonthek