RE: Yet Another Choreography Specification

> Thanks that is very helpful. I have a few follow-on questions:
>
> 1) do you have a guideline in mapping processes, events, and
> actions in BPML
>    to names in pi calculus; it seems to be quite arbitrary in your example

There are some very simple rules.

For example, each BPML one-way action is a pi-calculus action, but a two-way
operation is a pi-calculus process (send and choice for receive, or receive
and condition for send). A <sequence> is just a set of pi-calculus processes
that guard each other, an <all> is a |, a <choce> is a +, and every BPML
process is a !P.

Some rules are slightly more complicated. For example, a schedule is a
process where you send one message to set it and you receive a message when
the time event passes. You can model the time delay using the pi primitive
(easy), or simply by repeating a loop and counting CPU cycles (not so easy,
but correct).

Some rules are "trivial", just not trivial enough to cover in a one page
document. For example, every transaction completes by performing some
coordination that can be described using pi-calculus, but the definition
would take a page on its own. It's far easier to simplify it into
commit/rollback/heuristic messages (since 1PC and 2PC will always reduce to
that).

Essentially what you do is look for patterns that will always reduce the
same way, recast them into higher-level actions and do reduction using these
higher-level actions. Pi-calculus is instrumental in letting you do
reductions recursively, so if you look at a sequence that always gets
reduced to "I've received name X", you can just treat it as "I've received
name X".


> 2) a similar question regarding parameters and properties to names in a
> restriction
>    prefix

All properties defined in a context are new names in that process
(context->process). Parameters are both such properties, but also inputs for
the first action (preceded by !). Calling or spawning a process is no
different from sending it a message, except the channel is a new name in
some context that is only shared by some processes (i.e. your
implementation).

We make an arbitrary distinction between names that are known across systems
(WSDL services and operations) and names that are new inside a context that
is demarcated by a system or a process (call/spawn, compensate, raise) only
because it's easier to use these primitives to control access (same trust
domain) and deduct that a message exchange will always be possible. In
pi-calculus they would all be actions.


> 3) don't mean to be picky about your word usage, but since we are dealing
> with a
>    formal system, imprecise words may lead to confusion.  in
> particular,  in
> your
>    description about P1 reducing to P2 in pi calculus, didn't you need to
> first
>    perform an apply followed by a communication in order for P1
> to reduce to
> P2?

That's a good point. Indeed P1 would have to be activated in some way.
Whether you call it, spawn it or fire it from a schedule, you are still
activating it. So indeed P1 would actually start with !x(y). Let's think of
a process P0 that starts P1 by doing x!y. What starts P0? It's a recursive
problem.

Pi-calculus does allow you to define a process that is always reduced (no
guard), e.g.:

P = Q | R
Q = x!y
R = x(y)

Q will be reduced immediately (no guard), R will be reduced when (or after)
Q is reduced since there is a guard on R. I used that in the example, for
simplicity I elected P1 as the one that always gets reduced.


> 4) your comment that the relationship between BPML and
> pi-calculus parallels
> that
>    between Java and lamda-calculus is very puzzling... did you mean to say
> that
>    anything computable in Java is also computable in lamda-calculus, and
> vice versa,
>    or you really did mean that any one java method can be reduced
> to a pure
> lamda-calculus
>    expression, which is functional, no side effects.

A Java method that has side effects cannot be reduced to lambda-calculus
directly. But a Java method invocation can if you capture the input state
and output states in the input/output of the function, and all methods
invokes are constrained to access the state from the function variables.

Practical? Probably not. But if you want to look at a method in isolation,
e.g. to determine whether it's N or Log(N), you can do that, and that's
where a formal analysis becomes useful. In practice what we need is to
strike a blanace between reducing an enterprise wide process into
pi-calculus primitives and reducing just those portions of the process that
matter (e.g. how A,B and C interact).

For example, when we reduce processes to pi-calclulus we only look at
interactions between stateful services. All other information is not
interesting (it will always pi-calculus reduce). When we reduce a
transaction we only look at the outcome (commit/rollback/heuristic messages)
and ignore the voting phase of 2PC, since 2PC will always reduce to
commit/rollback/heuristic.


I usually tend to simplify the examples to make them more readable. But you
are right, if the example losses correctness it should be revised.

arkin

>
> Thanks,
> Joshua
>
> >From: "Assaf Arkin" <arkin@intalio.com>
> >To: <ed.peters@webMethods.com>, <abarros@dstc.edu.au>,
> <ChBussler@aol.com>,
> <bill.flood@sybase.com>, <public->>ws-chor@w3.org>
> >Cc: <W.M.P.v.d.Aalst@tm.tue.nl>, <m.dumas@qut.edu.au>,
> <l.aldred@qut.edu.au>, <a.terhofstede@qut.edu.au>
> >Date: Fri, 31 Jan 2003 10:18:34 -0800
> >Message-ID: <IGEJLEPAJBPHKACOOKHNEECLDCAA.arkin@intalio.com>
> >Subject: RE: Yet Another Choreography Specification
>
>
> >> -----Original Message-----
> >> From: public-ws-chor-request@w3.org
> >> [mailto:public-ws-chor-request@w3.org]On Behalf Of Ed Peters
> >> Sent: Friday, January 31, 2003 7:52 AM
> >> To: 'Assaf Arkin'; abarros@dstc.edu.au; ChBussler@aol.com;
> >> bill.flood@sybase.com; public-ws-chor@w3.org
> >> Cc: W.M.P.v.d.Aalst@tm.tue.nl; m.dumas@qut.edu.au; l.aldred@qut.edu.au;
> >> a.terhofstede@qut.edu.au
> >> Subject: RE: Yet Another Choreography Specification
> >>
> >>
> >>
> >> Assaf,
> >>
> >> Thanks very much for these pointers.  I wonder, are there any
> >> resources that
> >> might bridge the gap between theoretical treatments of pi-calculus and
> its
> >> manifestation in or influence on the BPML specification?  I've
> >> read numerous
> >> papers on pi-calculus, and I've pored through the BPML spec many
> >> times, and
> >> I'm afraid I'm missing the connection.
>
> >pi-calculus is a mathematical model. If you can reduce the process
> >definition into its pi-calculus form you can use pi-calculus to
> analyze it.
> >I'll illustrate by an example selected for its simplicity (taken from a
> >document I am writing about the design of BPML).
>
> >For the sake of this example I am using the 'pi' primitive
> (which refers to
> >some internal operation, say an assign) and equality test introduced in
> >later texts since they simplify the discussion. I am showing two systems
> >talking to each other:
>
> >P = P1 | P7
>
> >P1 = v(b,c,x,y,z) a!(w,b,c).P2 P2=P3+P4 P3=b(x).0 P4=c(y).P5 P5=pi.P6
> >P6=d!z.0
>
> >P7 = v(w,v,x,y,z) !P8 P8=!a(w).P9 P9=pi.P10 P10=?v=0.P11 - P12 P11=b!x.0
> >P12=c!y.P13 P13=d(z).0
>
> >property b,c
>
> >process P1
> >  parameter w
> >  property w,x,y,z
> >  action operation=a output=w,b,c
> >  choice P2
> >    event P3
> >      action operation=b input=x
> >      empty
> >    event P4
> >      action operation=c input=y
> >      . . . (determine z here)
> >      action operation=d output=z
> >             locate=d
>
> >property d
>
> >process P7
> >  property v,w,x,y,z
> >  event P8
> >  action P8 operation=a input=w
> >  ... determine v
> >  switch
> >    case P11
> >      condition v=0
> >      action operation=b output=x
> >             locate=b
> >    default P12
> >      action operation=c output=y
> >             locate=c
> >      action operation=d input=z,d
> >
> >In workflow terms you would say that activity P2 is enabled when
> process P1
> >starts, is executed after the action and is disabled after it is executed
> >(since it cannot be repeated in this context).
>
> >In pi-calculus you would reduce P1 to P2 by performing an action, then
> >reduce P2 after receiving one of the two inputs. If you run a
> trace of the
> >BPML process on the one hand and the pi-calculus process on the
> other hand,
> >you will see how processes get reduced in the same way.
>
> >The fact that both languages reduce in exactly the same way is what makes
> >pi-calculus so appealing as a formal model.
>
> ... [deleted]
>
> >You have to remember that the relationship between BPML and
> pi-calculus is
> >the same as the relationship between Java and lambda-calculus. Every Java
> >method can be reduced into a lambda-calculus form, and some of the
> >similarity is very obvious (you can easily see that a method is
> a function,
> >setting variables is the same). But where Java is a programming language
> and
> >uses higher level constructs, lambda-calculus is a concise mathematical
> >language, the translation is not always trivial, but mathematically
> >provable!
>
> ... [deleted]
>
> >arkin
>
>
> >>
> >> Regards,
> >> Ed
> >>

Received on Monday, 3 February 2003 14:40:25 UTC