Section: New Results

Foundations of Concurrency

Distributed systems have changed substantially in the recent past with the advent of phenomena like social networks and cloud computing. In the previous incarnation of distributed computing the emphasis was on consistency, fault tolerance, resource management and related topics; these were all characterized by interaction between processes. Research proceeded along two lines: the algorithmic side which dominated the Principles Of Distributed Computing conferences and the more process algebraic approach epitomized by CONCUR where the emphasis was on developing compositional reasoning principles. What marks the new era of distributed systems is an emphasis on managing access to information to a much greater degree than before.

Belief, Knowledge, Lies and Other Utterances in an Algebra for Space and Extrusion

Spatial constraint systems are algebraic structures from concurrent constraint programming to specify spatial and epistemic behavior in multi-agent system. In [15], [11] we developed the theory of spatial constraint systems with operators to specify information and processes moving from a space to another. We investigated the properties of this new family of constraint systems and illustrated their applications. From a computational point of view the new operators provide for process/information extrusion, a central concept in formalisms for mobile communication. From an epistemic point of view extrusion corresponds to a notion we called utterance; a piece of information that an agent communicates to others but that may be inconsistent with the agent's beliefs. Utterances can then be used to express instances of epistemic notions such as hoaxes or intentional lies. Spatial constraint system can express the epistemic notion of belief by means of space functions that specify local information. We showed that spatial constraint can also express the epistemic notion of knowledge by means of a derived spatial operator that specifies global information. In [21] we reported on our progress using spatial constraint system as an abstract representation of modal and epistemic behaviour.

Deriving Inverse Operators for Modal Logic

In [20] we used spatial constraint systems to give an abstract characterization of the notion of normality in modal logic and to derive right inverse/reverse operators for modal languages. In particular, we identified the weakest condition for the existence of right inverses and showed that the abstract notion of normality corresponds to the preservation of finite suprema. We applied our results to existing modal languages such as the weakest normal modal logic, Hennessy-Milner logic, and linear-time temporal logic. We also discussed our results in the context of modal concepts such as bisimilarity and inconsistency invariance.

D-SPACES: Implementing Declarative Semantics for Spatially Structured Information

In [22] we introduced D-SPACES, an implementation of constraint systems with space and extrusion operators. D-SPACES is coded as a c++11 library providing implementations for constraint systems, space functions and extrusion functions. D-SPACES provides property-checking methods as well as an implementation of a specific type of constraint systems (boolean algebras). We illustrated the implementation with a small social network where users post their beliefs and utter their opinions.

Slicing Concurrent Constraint Programs

Concurrent Constraint Programming (CCP) is a declarative model for concurrency where agents interact by telling and asking constraints (pieces of information) in a shared store. Some previous works have developed (approximated) declarative debuggers for CCP languages. However, the task of debugging concurrent programs remains difficult. In [19] we defined a dynamic slicer for CCP and we showed it to be a useful companion tool for the existing debugging techniques. Our technique starts by considering a partial computation (a trace) that shows the presence of bugs. Often, the quantity of information in such a trace is overwhelming, and the user gets easily lost, since she cannot focus on the sources of the bugs. Our slicer allows for marking part of the state of the computation and assists the user to eliminate most of the redundant information in order to highlight the errors. We showed that this technique can be tailored to timed variants of CCP. We also developed a prototypical implementation freely available for making experiments.