Spatial Logics allow one to reason about the behaviour and structure of concurrent programs. SLMC is a spatiallogic model checker for pi-calculus processes. As a little exercise I used it for reasoning about Church numerals and processes that operate on them.

In his original work on the pi calculus, Robin Milner defined an encoding of Church numerals, where the number `n`

is encoded as n outputs on a successor channel, followed by an output on a zero channel, e.g.

defproc N0(x,z) = z!();

defproc N1(x,z) = x!().z!();

defproc N2(x,z) = x!().x!().z!();

defproc N3(x,z) = x!().x!().x!().z!();

defproc N1(x,z) = x!().z!();

defproc N2(x,z) = x!().x!().z!();

defproc N3(x,z) = x!().x!().x!().z!();

Milner also defines some handy processes for doing basic arithmetic:

defproc Succ(x,z,y,w) = y!().Copy(x,z,y,w)

and Copy(x,z,y,w) =

select {

x?().Succ(x,z,y,w);

z?().w!()

};

defproc Add(x1,z1,x2,z2,y,w) =

select {

x1?().y!().Add(x1,z1,x2,z2,y,w);

z1?().Copy(x2,z2,y,w)

};

and Copy(x,z,y,w) =

select {

x?().Succ(x,z,y,w);

z?().w!()

};

defproc Add(x1,z1,x2,z2,y,w) =

select {

x1?().y!().Add(x1,z1,x2,z2,y,w);

z1?().Copy(x2,z2,y,w)

};

Note that numbers are ephemeral – they are consumed when being processed. To do anything useful we therefore need a process to duplicate number processes:

defproc Double(x,z,y1,w1,y2,w2) =

select {

x?().new y1_,w1_,y2_,w2_ in (

Succ(y1_,w1_,y1,w1) |

Succ(y2_,w2_,y2,w2) |

Double(x,z,y1_,w1_,y2_,w2_));

z?().(w1!() | w2!())

};

select {

x?().new y1_,w1_,y2_,w2_ in (

Succ(y1_,w1_,y1,w1) |

Succ(y2_,w2_,y2,w2) |

Double(x,z,y1_,w1_,y2_,w2_));

z?().(w1!() | w2!())

};

Armed with the above we can define a process that calculates the Fibonacci function:

defproc Fib(x,z,y,w) =

select {

z?().w!();

x?().select {

z?().y!().w!();

x?().new x0,z0,x1,z1,x2,z2,y1,w1,y2,w2 in (

Double(x,z,x0,z0,x1,z1) |

Succ(x0,z0,x2,z2) |

Fib(x1,z1,y1,w1) |

Fib(x2,z2,y2,w2) |

Add(y1,w1,y2,w2,y,w))

}

};

select {

z?().w!();

x?().select {

z?().y!().w!();

x?().new x0,z0,x1,z1,x2,z2,y1,w1,y2,w2 in (

Double(x,z,x0,z0,x1,z1) |

Succ(x0,z0,x2,z2) |

Fib(x1,z1,y1,w1) |

Fib(x2,z2,y2,w2) |

Add(y1,w1,y2,w2,y,w))

}

};

This probably looks incomprehensible at first. It has been optimised to avoid unnecessary copying and roughly corresponds to the following pseudocode

fib(x) {

if (x-- == 0) return 0;

else if (x-- == 0) return 1;

else return fib(x) + fib(x+1);

}

if (x-- == 0) return 0;

else if (x-- == 0) return 1;

else return fib(x) + fib(x+1);

}

So far we have only defined some simple pi-calculus processes. Now let’s start reasoning about them. First would like to know whether a process represents a number. After a lot of trial-and-error, and consultation with my colleague Francis, I eventually arrived at the following SLMC predicate:

defprop number(x,z) =

minfix X.((<z!>true or <x!>true or <tau>true) and

[z!]allTau and [x!]X and [tau]X and

forall n.(n==z or n==x or [n]false));

defprop allTau =

minfix X.((void or <tau>true) and

[tau]X and forall n.[n]false);

minfix X.((<z!>true or <x!>true or <tau>true) and

[z!]allTau and [x!]X and [tau]X and

forall n.(n==z or n==x or [n]false));

defprop allTau =

minfix X.((void or <tau>true) and

[tau]X and forall n.[n]false);

Translated into English this says

A process represents a number if it communicates on two names, symbolically denoted as

`x`

and`z`

, s.t.

- it may do an output on
`z`

or`x`

, or perform an internal transition,- after performing an output on
`z`

it may only perform internal transitions and must eventually evolve to nothing,- after performing an output on
`x`

it must evolve to a process that represents a number,- it cannot perform an infinite sequence of internal transitions or outputs on
`x`

,- it may not perform any other actions.

Item 4 and 5 deserve some discussion. Item 4 basically excludes infinity as a number. Item 5 states that we want our processes to be *just* numbers and nothing else. For example, we would not want a process to behave like a number but also delete all files on our hard

drive. This point sparked some philosophical discussion with my colleague Paul. Specifically, axiomatisation in mathematics usually does not exclude additional behaviours. For example, file-deleting numbers satisfy all the Peano

axioms. Should there be an additional axiom along the lines of “Numbers must not satisfy any

axioms other than the ones stated here”?

Anyway, let’s put our `number`

predicate to some use:

check N0(x,z) |= number(x,z);

check N1(x,z) |= number(x,z);

check N2(x,z) |= number(x,z);

check N3(x,z) |= number(x,z);

check N1(x,z) |= number(x,z);

check N2(x,z) |= number(x,z);

check N3(x,z) |= number(x,z);

Feeding these to SLMC all result in success, so 0,1,2,3 really are numbers – hooray! Now for some counter examples of processes that are almost numbers, but not quite:

defproc Infinity(x,z) = x!().Infinity(x,z);

defproc ErraticNumber1(x,z) =

select {

x!().(e!() | ErraticNumber1(x,z));

z!()

};

defproc ErraticNumber2(x,z) = x!().(e!() | z!());

defproc ErraticNumber3(x,z) =

select {

x!().(e!() | z!());

z!()

};

defproc ErraticNumber4(x,z) =

select {

x!().(e!() | e?() | z!());

z!()

};

defproc ErraticNumber5(x,z) =

select {

x!().z!();

z!().(e!() | e?())

};

check Infinity(x,z) |= number(x,z);

check ErraticNumber1(x,z) |= number(x,z);

check ErraticNumber2(x,z) |= number(x,z);

check ErraticNumber3(x,z) |= number(x,z);

check ErraticNumber4(x,z) |= number(x,z);

check ErraticNumber5(x,z) |= number(x,z);

defproc ErraticNumber1(x,z) =

select {

x!().(e!() | ErraticNumber1(x,z));

z!()

};

defproc ErraticNumber2(x,z) = x!().(e!() | z!());

defproc ErraticNumber3(x,z) =

select {

x!().(e!() | z!());

z!()

};

defproc ErraticNumber4(x,z) =

select {

x!().(e!() | e?() | z!());

z!()

};

defproc ErraticNumber5(x,z) =

select {

x!().z!();

z!().(e!() | e?())

};

check Infinity(x,z) |= number(x,z);

check ErraticNumber1(x,z) |= number(x,z);

check ErraticNumber2(x,z) |= number(x,z);

check ErraticNumber3(x,z) |= number(x,z);

check ErraticNumber4(x,z) |= number(x,z);

check ErraticNumber5(x,z) |= number(x,z);

All the checks fail, as expected.

Finally, let’s check whether the Fibonacci process produces numbers for

certain inputs – or, more precisely, whether the Fibonnaci process,

when composed with certain number processes, evolves into a process

that represents a number:

defproc Fib0 = new x,z in (N0(x,z) | Fib(x,z,y,w));

defproc Fib1 = new x,z in (N1(x,z) | Fib(x,z,y,w));

defproc Fib2 = new x,z in (N2(x,z) | Fib(x,z,y,w));

defproc Fib3 = new x,z in (N3(x,z) | Fib(x,z,y,w));

check Fib0 |= number(y,w);

check Fib1 |= number(y,w);

check Fib2 |= number(y,w);

check Fib3 |= number(y,w);

defproc Fib1 = new x,z in (N1(x,z) | Fib(x,z,y,w));

defproc Fib2 = new x,z in (N2(x,z) | Fib(x,z,y,w));

defproc Fib3 = new x,z in (N3(x,z) | Fib(x,z,y,w));

check Fib0 |= number(y,w);

check Fib1 |= number(y,w);

check Fib2 |= number(y,w);

check Fib3 |= number(y,w);

These all succeed. However, the last check – whether `fib(3)`

is a number – takes several hours to complete. I know the complexity of the computations performed by SLMC can be quite bad, but I am still at a loss to explain why it would perform so much more badly on `fib(3)`

when the check for `fib(2)`

completes within a few milliseconds.

The reader may wonder why we selected particular examples to test the Fibonacci process, rather than checking whether it evolves to a number for any given input number. To express such a test we need the spatial logic’s guarantee operator, `|>`

, and then could write:

check Fib(x,z,y,w) |= number(x,z) |> number(y,w)

which says

Is Fibonacci a process that when composed with a process that is a

number, is a number?

Unfortunately, SLMC does not support the guarantee operator. There is a good reason for that. The expressiveness of the logic must be finely tuned in order for model checking of interesting properties to be decidable for interesting processes. Introducing the guarantee operator makes model checking undecidable for most interesting processes.

2000-14 LShift Ltd,
1st Floor, Hoxton Point, 6 Rufus Street, London,
N1 6PE,
UK+44 (0)20 7729 7060
Contact us

Matthew Sackman

on 08/04/06 at 12:48 pm

The examples given here seem, at first glance, to be expressible in HML. Given that the guarantee operator |> isn’t supported in the model checker, are there other parts of Spatial Logics that give more power than HML that are supported by SLMC?

Do spatial logics reduce to SHML or WHML and are respectful? Or is there a more complex relationship between the logics? Certainly the modal operators look right out of SHML – are there [[cond]] and <> equivalents of WHML too?

Amusing to see defproc again after all these years – last seen in BBC BASIC!

matthew

on 08/04/06 at 12:53 pm

Gah, silly HTML – I meant [[cond]] and <<cond>> in the above…

matthias

on 10/04/06 at 4:06 pm

The example doesn’t require the use of any of the spatial operators of the logic, so I supect they may well be expressible in HML.

Yep. All the spatial operators. See the SLMC papers/manual for details.

matthias

on 11/04/06 at 6:46 am

Greg Meredith pointed me towards Mads Dam‘s work on Proof Systems for pi-calculus Logics, which contains a number predicate in a more standard HML that looks very similar to mine. The differences are interesting:

Mads’ number processes are “located” at a single channel, whereas I use Milner’s original and simpler un-located encoding. The added complexity is reflected in Mad’s formula Nat0 on page 15. The rest is dealt with in Nat1, which corresponds very closely to my formula.

My formula fails to ensure that a number process must not simultaneously enable

`x`

and`z`

transitions. Consider a process that duplicates such a number, e.g. using`Double`

. The resulting number processes are not guaranteed to represent the same number, which is clearly undesirable. That is easy to fix by adding a condition`not (<z!>true and <x!>true)`

to the`number`

predicate.Mads’ formula fails to ensure that after the

`z`

transition a number process should not be able to do anything other than`tau`

transitions, and must eventually terminate. That is easy to fix.Mads’ formula disallows processes that can do a (finite) number of

`tau`

transitions during which`n`

and`z`

are disabled. I think that is wrong, but it is a matter of opinion and easy to change either way.