Model-checking graph properties using Alloy

While developing an algorithm for fast distributed computation of a graph diameter and radius, some of my colleagues had a conjecture about graph topology that, if true, would enable an aggressive optimization of the algorithm.

In order to understand the conjecture we must first recall some (more or less) standard graph theory definitions:

  • The distance between two nodes is the length of the shortest path between them;
  • The eccentricity of a node is the greatest distance between that node and all others;
  • The diameter of a graph is the maximum eccentricity found in the graph;
  • A node is peripheral if its eccentricity is equal to the diameter;
  • The antipode of a node is the set of nodes at distance equal to its eccentricity.

Given a non-directed connected graph the initial conjecture was:

For every node, all nodes in its antipode are peripheral.

They quickly found a counter-example to this conjecture and relaxed it to the following:

For every node, some node in its antipode is peripheral.

For a long time they were not able to prove or refute this conjecture. At some point I was involved in the discussion and decided to model-check it using Alloy before attempting any proof.

Modeling a non-directed connected graph using Alloy is fairly trivial (assuming some basic knowledge of Alloy):

sig Node {
  adj : set Node -- adjacency relation
}

fact {
  adj = ~adj -- the adjacency relation is symmetrical
  no iden & adj -- no loops
  all n : Node | Node in n.*adj -- the graph is connected
}

To model distances I used a ternary relation between pairs of nodes and a natural number. Natural numbers are easily modeled with a total ordering, which is axiomatized in one of Alloy’s standard modules:

open util/ordering[Nat]

sig Nat {}

The distance relation can be declared in the node signature and axiomatized as follows:

sig Node {
  adj : set Node,
  dist : Node -> one Nat
}

fact {
  all n : Node | n.dist[n] = first
  all disj n,m : Node | n.dist[m] = min[n.adj.dist[m]].next
}

The two facts just state that, for every node:

  • The distance to itself is 0.
  • The distance to another node is 1 plus the minimum distance between its neighbors and that node.

We can now compute the eccentricity relation by direct transcription of the above definition, using a higher-order function without parameter (i.e. a constant):

fun ecc [] : Node -> one Nat {
  { n : Node, d : Nat | d = max[n.dist[Node]] }
}

Given this relation, the diameter, periphery and antipode relation can be trivially defined:

fun diam [] : one Nat {
  max[Node.ecc]
}

pred peripheral [n : Node] {
  n.ecc = diam
}

fun antipode [] : Node -> Node {
  { n, m : Node | n.dist[m] = n.ecc }
}

Following this approach, other graph concepts, such as radius or centrality, could also be trivially defined:

fun radius [] : one Nat {
  min[Node.ecc]
}

pred central [n : Node] {
  n.ecc = radius
}

The conjecture can now be directly transcribed into the following assertion:

check {
  all n : Node | some m : antipode[n] | peripheral[m]
}

Unfortunately, when the scope was increased to 7 we had several counter-examples. Here is one of them:

The diameter of this graph is 4. The antipode of node 6 is node 3, but this node is not peripheral, since it has eccentricity 3.

Bummer 😦 At least we can now easily model-check other similar properties before indulging in pointless discussions.

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s