From Join to UPPAAL and back

I'm currently teaching a course using UPPAAL for modelling and anlysis of communicating FAs (finite automatas). In this post, I will show some interesting connections between communicating FAs and coordination patters as found in the Join calculus (referred to as Join for brevity).

For concreteness, let's consider a (classic) coordination example: The 'bridge' problem. We have four soldiers on the left (unsafe) side of the bridge. They'd like to cross the bridge to get to the right (safe) side. The problem is it's at night and they need a torch to cross the bridge. The torch can carry a maximum of two soliders. We assume that the torch always carries two soliders from right to left and only solider goes back (left to right).

In Join, we can specify/model this problem as follows. We introduce synchronous methods 'take', 'release' and 'takeBack' to model the actions. We introduce asynchronous methods 'free', 'one', 'two', 'oneLeft', 'rightSide' and 'oneFrom' to represent the states of the torch and 'unsafe(i)', 'towards(i)', 'safe(i)' and 'back(i)' to represent the states of soldier i. Their meaning will become clear once see the join-patterns describing the interaction between torch and soldiers.

The behavior of the torch is specified via the following join-patterns (using Haskell-style syntax).

free = do take
          one

one = do take
         two

two = do release
         oneLeft

oneLeft = do release
             rightSide

rightSide = do takeBack
              oneFrom

oneFrom = do release
             free

Of course, we could have unfolded the above definitions into the following (and thus omitting the intermediate states)

free = do take
          take
          release
          release
          takeBack
          release
          free

This makes it even clearer that the torch waits for two soldiers to grab the torch. Then, the torch (with the soldiers) crosses the bridge (this is implicit). The torch releases both soliders and the torch will take back a soldier and release this soldier on the unsafe side again. The more verbose representation (using the intermediate states) will be useful later when discussing the connection to communicating FAs.

We yet need to model the behavior of solider(i). We finally make use of some multi-headed join-patterns.

unsafe(i) & take = towards(i)

towards(i) & release = safe(i)

safe(i) & takeBack = back(i)

back(i) & release = unsafe(i)

For example, the first join-pattern above says that if solider i is in the unsafe state and we can take the torch, then we unblock the caller of take (remember that take is synchronous) and we issue a new asynchronous method call towards(i). The semantics of join-pattern is actually fairly simply. In essence, multi-set rewriting where the methods are treated as resources. The multisetrewrite library introduced in a previous post, can easily encode join-patterns (and even more, eg guards etc).
I will release some runnable code at some later stage.

The point of this exercise is not to show what can be done with Join, rather, we want to establish some connections to communicating FAs. So, what's the connection? In Join, a join-pattern is triggered (aka executed) if we can match the pattern head with the specified method calls. In communicating FAs, two automatas 'communicate' if we find matching send (!) and receive (?) transitions.

   p --- a! --> q     r --- a? --> t

-----------------------------------------

  (p,r) --- a --> (q,t)

Each component of the tuple corresponds to the states of a communicating FA (CFA). If one CFA has a send edge (a!) which matches the receiving edge (a?) of another CFA, then we make a transition along those edges as shown in the above diagram. This smells similar to Join, right? Indeed, in Join we can represent

 p --- a! --> q

by

p = do a
       q

and

 p --- a? --> q

by

p & a = q

The states are turned into asynchronous method calls and the actions 'a' are turned into synchronous method calls.


In fact, the Join program shown above was derived from the following CFAs
using this translation scheme.

The torch CFA:

Torch

Get your own at Scribd or explore others:

The soldier CFA:
Soldier 3

Get your own at Scribd or explore others:

It's also possible to systematically translate Join programs to CFAs but it's getting more tedious to work out the details. Both languages are equally expressive. However, (I claim) Join allows us to specify more complex coordination patterns more easily than CFAs (therefore the transformation to CFAs gets quite involved). The advantages of having a Join representation of CFAs is that we know how to efficiently execute Join programs (eg see the multisetrewrite library which exploits join-style concurrency by executing non-overlapping join-patterns in parallel). On the other hand, a CFA representation of Join allows to make use of UPPAAL's expressive query language and its model checking facilities. For example, via the query

E<> safe(1) and safe(2) and safe(3) and safe(4)

we can check if (assuming we have four soldiers) it's possible for all four soldiers to reach the safe side. E says there exists a trace and <> says there exists a state.

We can also check if the system does not deadlock

A[] not deadlock

This property is not satisfied for the following reason. In case all four soldiers are on the safe side and one solider makes its way back to the unsafe side, the soldier gets to the unsafe side but won't be able to get back to the safe side. Remember that in our torch model, we require two soldiers per torch. For this example at least, the deadlock property doesn't say much. We only know that the program will terminate (possibly in some undesired state).

UPPAAL's query language is a subset of CTL btw. This implies that we canNOT verify (very compliated) queries such as "are the join-patterns confluent". Confluence requires to quantify over traces, then over states and then again over traces which is beyond CTL (for good reasons because it gets way too complex to check such properties).

Anyway, the connection between Join and CFAs is quite useful. This way I became a much better UPPAAL user. First write your program in Join and then convert to CFAs. I will write more about this connection at some later stage.