Concurrency, logic and algebra for social and spatial interactive computation (classic).

Giving mathematical foundations to today's concurrent systems (i.e., computational systems of multiple agents that interact with each other) is a serious challenge for theoretical computer science. Traditional mathematical models from concurrency theory do not single out two fundamental aspects of these systems: Namely, epistemic and spatial behaviour. The intrinsic epistemic nature of these systems arises from social behavior. We have millions of agents (users) posting and sharing partial information, beliefs, opinions and even intentional lies (hoaxes) on social networks. as for the spatial behavior, compelling examples are provided by processes (applications) and data moving across possibly nested spaces defined by friend circles, groups, and shared folders in social networks and cloud storage. It is therefore crucial to be able to describe, analyze and, in general, reason about concurrent system exhibiting epistemic and spatial behavior. This reasoning must be precise and reliable. Consequently, it ought to be founded upon mathematical principles in the same way as the reasoning about the behavior of sequential programs is founded upon logic, domain theory and other mathematical disciplines. 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 behaviour 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 behaviours. 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 system for proving spatial 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, and order theory in a single model for epistemic and spatial distributed systems. The expected outcome is a 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 behaviour. 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.