Concurrency via rewriting approaches to epistemology (create)

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 behavior. The intrinsic epistemic nature of these systems arises from social behavior. There are 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 systems 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 previous work some of members of our research team aVISPa put forward formalisms from different mathematical domains for analyzing some basic epistemic and spatial distributed systems. In particular, new models of concurrent epistemic computation [26] in concurrency theory were developed, new algebraic structure for axiomatizing belief and space [50] in order theory were provided, and a logical system for proving spatial properties [44,45] in proof theory was introduced. On the other hand, some of the authors have developed techniques for formally simulating and analyzing highly concurrent systems in rewrite-based formalisms [99]. These works represent significant advances towards achieving the above-mentioned main goal but much remains to be done for providing a single robust mathematical model for today's distributed systems. This project takes 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 post (e.g., a lie, a fact, an opinion) may lead to unwanted situations such as the public announcement of sensitive information or other intrusive behaviors. By building upon previous work, this project will coherently combine and develop new mathematical theories and techniques from concurrency theory and rewriting systems in a single model for epistemic and spatial distributed systems. In particular, the main goal is to predict the epistemic flow of information that may lead to unwanted behavior by means of the following two outcomes: (i) a mathematical model (namely, a process calculus), to specify the spatial topology of a system, and (ii) a rewriting logic semantics able to simulate and reproduce the mathematical model.