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

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.