A programming language for local computations in graphs! Computational completeness

We have developed a new programming language for implementing distributed algorithms encoded by means of local computations. This language, called Lidia, is based on a two-level transition system model: the first level is used to specify the behavior of each single component, whereas the second level captures their interactions. Transitions are basically expressed in a precondition-effect style. Lidia depends on a logic L_∞* that is used to express the preconditions of each transition. The main topic of This work is to present the L_∞* language and to bring out some of its basic properties. Moreover, we take advantage of these properties to define a class of distributed algorithms encoded by means of local computations that can be implemented in our programming language. The completeness of Lidia, related to the use of users defined functions, represents the main result of This work.