On the Soundness, Completeness and Applicability of the Logic of Knowledge and Communicative Commitments in Multi-Agent Systems

abstractBenthem?scorrespondencetheoryisoneofthemostimportanttoolsofthetheoryofmodallogicsdevelopedinthelastthreedecades.Correspondencetheory,asubfieldofthemodeltheory,reflectsasystematicstudyofrelationsbetweenclassesofframesandmodallanguage.Inthispaper,weusecorrespondencetheoryformodallogicstosolveaproblemnotaddressedyetintheliterature,namelythesoundnessandcomplete-nessofalogiccombiningtwodifferent,yetrelatedmodalities:agents?knowledgeandcommitments.ThepaperprovesthesoundnessandcompletenessofthislogiccalledCTLKC+.Thisworkishighlysignificantasitprovesthatcombiningthetwoagents?modalitiesresultedinaconsistentlogicthatcanbeusedtodesignreliablesystems.Themethodologyisasfollows:wedevelopasetofreasoningpostulates(axioms)thatre-flecttheinteractionbetweenagents?knowledgeandsocialcommitmentsinmulti-agentsystem(MAS)usingtheCTLKC+logicandcorrespondthemtocertainclassesofframes.Inparticular,wefirstgiveaname,for-malizationandmeaningforeachpostulate.Then,wecorrespondthepostulatestocertainclassesofframesandprovidetherequiredproofs.Thereafter,wepresentadiscussionthatillustratestheimportanceoftheproposedpostulatesinMASsusingaconcreteapplicationexamplecalledtheNetBillprotocoltakenfromthebusinessdomain.Finally,weshowhowthepostulateswereaddressedintheliterature.Theexistenceofsuchacorrespondenceallowsustoprovethatthelogicgeneratedbyanysubsetofthesepostulatesissoundandcompletewithrespecttomodelsthatarebasedonthecorrespondingframes.Theultimategoalofthispa-peristofurtherassessthelogicofknowledgeandcommitments(CTLKC+)fromanewperspective(i.e.,thesoundnessandcompleteness).Consequently,thisworkadvancestheliteratureoflogicsinMASsandclosesagapthathasnotbeenexploredbefore.