Alliance project
Simplicial and Cubical Sets and Knowledge Evolution in Distributed Systems.

Project teams:


British Team

  • Project leader : Timothy Porter, (Professor),
    Other team members: Core members: 

  • Ronald Brown (Emeritus Professor and Leverhulme Research Fellow, Bangor);

  • Chris D. Wensley, (Lecturer, Maths, Bangor);

  • Gareth Evans and Richard Lewis (Postgraduate Students, Maths, Bangor)
    Other members of staff and postgraduates associated with the project to a lesser extent:

  • Sian Hope, (Senior Lecturer in Computer Science, Bangor),

  • W.J.Teahan, (Lecturer in Computer Science, Bangor),

  • Leslie Pritchard, (Postgraduate Student, Computer Science, Bangor)

  • Anne Heyworth, (EPSRC, Research Assitant, Leicester).

French Team

Simplicial and Cubical Sets and Knowledge Evolution in Distributed Systems

The project searches for new mathematical models to handle the complex nature of distributed computation and other complex systems, modelled at least to start with as a Multiagent Systems (MAS).

Suppose there are n-agents in a distributed computational system.An agent will be a processor, sensor or finite state machine, interconnected by a communication network with other `agents'.Typically each agent has a local state that is a function of its initial state, the messages received from other agents, observations of the external environment and possible internal actions.

The network, even the number of agents, will usually evolve through time, for instance, in a Peer-to-Peer (P2P) information exchange network or where new agents may be `spawned' by some agent or group of agents in some Knowledge Grid systems, but we will assume a static net for the discussion here.. We refer loosely to different agents `knowing' various `facts' about the system or the environment. How does `knowledge' in this situation behave? How does it evolve? What sorts of mathematics might help in the study of the behaviour of such multiagent systems?

The Logics S5 and S5n.

In the study of `knowledge' in complex systems in Artificial Intelligence, various logics have played a central role. In Multi-Agent Systems, (MAS), one of the basic logics used for an n-agent system is S5n.This is an epistemic modal logic with operators interpreted as "agent i knows that p holds".

The basic semantics for S5n is given by Kripke equivalence frames.

Kripke equivalence frames

An equivalence frame (or simply (Kripke) frame)
F = (W, ~1, ... , ~n)
consists of a set W with, for each i in A = {1,2,..., n}, an equivalence relation ~i on W. Elements of W are called possible worlds and are denoted w, w', etc. We will write [w]i for the equivalence class of the element w of W for the ith equivalence relation, ~i.

A Kripke (equivalence) frame is very like a labelled transition system, but it has equivalence relations rather than partial orders as its basic relational structure. For dynamic networks (P2P or Knowledge Grid), equivalence frames will need mixing with transition system aspects

A more direct model of MASs is given by global states for interpreted systems. A set of globals states (SGS) for an interpreted system is a subset S of the product Le× L1× . . .× Ln. If S = Le× L1× . . .× Ln, then the SGS is called a hypercube. The idea behind allowing the possibility of considering a subset and not just the whole product is that some points in ?L = Le× ?Li may not be `feasible' because of explicit or implicit constraints present in the multiagent system (MAS).

Any SGS yields a Kripke frame. 

If we write L= (Le, L1, ... , Ln)and (S,Lfor an SGS based on L, then set F(SL) to be the frame with S as its set of possible worlds with ~i defined by:l~i l'iif and only ifli = l'i,  i.e. li andl'i correspond to the same local state for agent i. For
simplicity here we will assume that Le is a singleton set.

This construction underlies an equivalence of categories between Kripke equivalence frames and SGSs.

Aside on Categories for MASs.  (first installment)
 Fixed number of agents.
Category : Objects plus morphisms between them.

Categories for n-agent systems:

Objects: equivalence frames, F = (W, ~1, .  .  . , ~n).

Morphisms:   a choice:

 Basic or weak morphisms:  f from  F to F' = F = (W', ~'1, ... , ~'n) is a function f from  W to W' that preserves the equivalence relations in an obvious way.
These are not a good choice but they can be useful sometimes.
 

Bounded morphisms:  these use an extra condition to preserve the logic better.  This relates to functional bisimulation.
This condition is `geometric'.  It looks like a lifting condition / fibration from  algebraic topology or groupoid theory as well as behaving well for the logic!
 

Similar types of morphism can be defined for SGSs.
 

That reminds me of . . .

Global Actions and Groupoid Atlases.


Sets with families of equivalence relations on them occur in several areas of mathematics. In some there are well developed notions of morphism and of path in such a system and even a well behaved homotopy theory that allows for a geometric analysis of the system. Can we adapt ideas from those areas that are relevant to MASs? How do paths in these settings relate to runs in MAS theory? To what does homotopy correspond?

Homotopy?

The intuition behind homotopy is that of deforming paths within a space :

diagram illustrating a homotopy

Path a can be deformed (by a homotopy) to path a'.

... but what are these ‘global actions’?

A global action is a set with a family of group actions on it which need not be globally defined, but on the intersections of their various
‘domains’ they will satisfy some compatibility conditions. The set of the ‘domains’ (also referred to as ‘patches’) has a partial order
which controls the interactions between overlapping patches. Each patch is very like a Kripke frame, but the equivalence relation need
not be globally defined.
The prime example of a global action is a set X with a family of groups acting on it. In particular if G is a group (in the usual mathematical sense) then given a family of subgroups {Hi : i  in I} of G, we can consider the actions of each Hi on the set of elements of G by left multiplication.

Any group action gives rise to a small category in which all morphisms are invertible, i.e. to a groupoid. Any equivalence relation also gives rise to a groupoid.
In this way a generalisation both of a global action and of a Kripke frame is a groupoid atlas in which ‘group action’ or ‘equivalence
relation’ is replaced by ‘groupoid’.
More refined mathematical models for evolving MASs will need a combination of equivalence relations and order reflations so as to mirror the local transition systems of the agents as they ‘evolve’ through time.

Example 1. (From Kripke frames to Groupoid Atlases.)
Let X be a set and ~i, i = 1, 2, . . . , n, n equivalence relations on X.
Then F = (X, ~1, . . . , ~n) is a Kripke frame, but also, if we specify the local groupoids
Gi = Objects X, arrows from  x1to  x2 if and only if x1 ~i x2, and the poset of patches  to be discrete, i.e. “ less-than-or equals ” = “ = ”, we
have a simple groupoid atlas, A(F).