Algebraic and coalgebraic semantics for knowledge acquisition: foundations, applications, and tool support

Lead Research Organisation: University of Oxford
Department Name: Computer Science

Abstract

I aim to develop high level structures for reasoning about knowledge of agents in a multi-agent system where agents communicate and as a result update their information. All of us take part in such situations when communicating through the internet, surfing the web, bidding in auctions, or buying on financial markets. Reasoning about knowledge acquisition in these situations becomes more challenging when some agents are not honest and they cheat and lie in their actions and as a result other agents acquire wrong information. The current models of these situations are low level: they require specifying untidy details and hide the high level structure of information flow between the agents. This makes modeling a hard task and proving properties of the model an involved and complicated problem. The complexity of reasoning in these situations raises the question: ``Which structures are required to reason about knowledge acquisition?'', in other words, ``What are the foundational structures of knowledge acquisition?''. High level methods provide us with a minimal unifying structure that benefits from partiality of information: we do not need to specify all the details of the situations we are modeling. They also bring out the conceptual structure of information and update, hide the untidy details, and tidy up the proofs. My plan is to (1) Study the foundational structures that govern knowledge acquisition as a result of information flow between the agents and then develop a unifying framework to formally express these structures in a logical syntax with a comprehensive semantics. I aim to use known mathematical structures, such as algebra, coalegbra and topology, for the semantics. The syntactic theory will be a rule-based proof-theoretic calculus that helps us prove properties about knowledge acquisition in a programmatic algorithmic manner. (2) Apply this framework to reason about security properties of multi-agent protocols. Examples of these protocols are communication protocols between a client and a bank for online banking. We want to make sure that such a protocol is secure, that is, the client's information remains secret throughout the transaction. Because of the potentially unlimited computational abilities of the intruder, these protocols become very complex and verifying their security becomes a challenging task. It is exactly here that our high level setting becomes a necessity, that is, in formal analysis of these protocols and in proving their security properties. The semantic structures that I aim to use have also been used to model the logic of Quantum Mechanics. So my model will be flexible enough to accommodate quantum situations. These situations are important for security protocols because they benefit from additional non-local capabilities of Quantum Mechanics, which guarantee better safety properties. I aim to apply the knowledge acquisition framework to Quantum protocols and prove their sharing and secrecy properties. On the same track, similar semantic structures have been used for information retrieval from the web. I aim to exploit these models and study their relationship to my framework. (3) Write a computer program to implement the axiomatic semantic structure and produce a software package. This software will help us automatically verify properties of multi-agent protocols, such as the security protocols mentioned above.

Publications

10 25 50

publication icon
Pardo P (2012) Planning in the Logics of Communication and Change in Proceedings of the 11th International Conference on Autonomous Agents and Multiagent Systems

publication icon
Pardo P (2013) Backward Planning in the Logics of Communication and Change in Proceedings of the International Conference on Agreement Technologies

publication icon
Richards S (2009) Aximo: Automated Axiomatic Reasoning for Information Update in Electronic Notes in Theoretical Computer Science

 
Description We found out that coalgebras can formalize the theory of multiagent information update and developed such a setting. As a result of this, it became apparent that the setting of subclassical logics can be applied to reason about these systems. Later, we developed two different intuitionistic logics for these systems and their sound and complete proof systems.
Exploitation Route They can be used by the multi-agent community to automatically reason about their protocol and prove properties theireof. The project New Foundational Structures for Engineering Verified multi-UAV's with EP/J012564/1, on which I was involved as a co-PI was an effort in this direction.
Sectors Aerospace, Defence and Marine,Digital/Communication/Information Technologies (including Software)

 
Description British-Dutch Scientific Collaboration Scheme
Amount £7,000 (GBP)
Organisation British Council 
Department British Council and Platform Beta Techniek
Sector Charity/Non Profit
Country United Kingdom
Start 10/2010 
End 10/2010
 
Description University of Oxford
Amount £529,968 (GBP)
Funding ID EP/J002607/1 
Organisation Engineering and Physical Sciences Research Council (EPSRC) 
Sector Academic/University
Country United Kingdom
Start  
 
Description University of Oxford
Amount £5,500 (GBP)
Funding ID PPS WS05 
Organisation University of Oxford 
Sector Academic/University
Country United Kingdom
Start  
 
Description Wolfson College Oxford
Amount £600 (GBP)
Funding ID Workshop Funds 
Organisation University of Oxford 
Department Wolfson College
Sector Academic/University
Country United Kingdom
Start 09/2009 
End 09/2009
 
Description Wolfson College Oxford
Amount £600 (GBP)
Funding ID Workshop Funds 
Organisation University of Oxford 
Department Wolfson College
Sector Academic/University
Country United Kingdom
Start  
 
Description Amsterdam 
Organisation University of Amsterdam
Department Institute for Logic Language Information and Computation (ILLC)
Country Netherlands 
Sector Academic/University 
PI Contribution A conference and a journal paper were published and a joint workshop was organized.
Collaborator Contribution A conference and a journal paper were published and a joint workshop was organized.
Impact A conference and a journal paper were published and a joint workshop was organized.
Start Year 2008
 
Description McGill 
Organisation McGill University
Department School of Computer Science
Country Canada 
Sector Academic/University 
PI Contribution A number of conference and workshop papers were published and an MSc thesis in McGill was sueprvised.
Collaborator Contribution A number of conference and workshop papers were published and an MSc thesis in McGill was sueprvised.
Impact A number of conference and workshop papers were published and an MSc thesis in McGill was sueprvised.
Start Year 2007
 
Description Montpellier 
Organisation University of Montpellier
Country France 
Sector Academic/University 
PI Contribution We worked on categorical models of natural language.
Collaborator Contribution We worked on categorical models of natural language.
Impact Papers, listed in the publication.
Start Year 2010
 
Description Pere 
Organisation Spanish National Research Council (CSIC)
Department Artificial Intelligence Research Institute (IIIA)
Country Spain 
Sector Public 
PI Contribution Working on planning using dynamic epistemic logic and supervising a phd student's thesis.
Collaborator Contribution Working on planning using dynamic epistemic logic
Impact Conference papers and a soon to be submitted journal version.
Start Year 2012
 
Title Aximo 
Description Automated software to check algebraic properties of pubich and private announcements in multi-agent systems 
Type Of Technology Webtool/Application 
Year Produced 2009 
Impact used during teaching in Oxford 
 
Description Invited talks 2 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Other academic audiences (collaborators, peers etc.)
Results and Impact sparked discussions and collaborations

na
Year(s) Of Engagement Activity 2008