EPIC: Epistemic Interactive Concurrency

In this project we take up the task of developing a mathematical model, conceptually different from existing models of concurrency, for the precise understanding of epistemic and spatial behavior in today’s concurrent systems. The model will be able to rigorously predict the behavior of a concurrent system in the presence of complex flow of epistemic information such as knowledge, facts, public announcements, lies and opinions. A compelling application of the model will be to predict if in a given social network, certain intentional lie may lead to unwanted situations such as the public announcement of sensitive information or other intrusive behaviors. In previous work we put forward formalisms from different mathematical domains for analysing some basic epistemic and spatial distributed systems. In particular, we developed a new model of concurrent epistemic computation [26] in concurrency theory, proposed a new algebraic structure for axiomatizing belief and space [50] in order theory, introduced a logical framework for proving epistemic, spatial and temporal properties [44,45] in proof theory. These works represent significant advances towards achieving our main goal but much remains to be done for providing a single robust mathematical model for today’s distributed systems. By building upon our previous work, this multidisciplinary project will coherently combine and develop new mathematical theories and techniques from concurrency theory, mathematical logic, information and order theory in a single model for epistemic and spatial distributed systems. The expected outcome is an executable mathematical model, a process calculus, to specify the spatial topology of a system and predict the epistemic flow of information that may lead to unwanted behavior. We will define a logic to reason about the system and endow it with a proof system. This will be used to produce automated tools to verify properties of our model.