eal world”, represented abstractly using (time-varying) first-order logic predicates and terms. A representative composition result [11] here uses a translation into Petri nets. The “Roman” model for [4] focuses on an abstract notion of “activities” (without modeling how they impact the world), and in essence model web services as finite state automata with transitions labeled by these activities. A powerful composition result is obtained using a reduction to Propositional Dynamic Logic (PDL). The Conversation model [5] focuses on messages passed between web services, and again uses finite state automata to model the internal processing of a service, with transitions labeled by message sends and message reads. A key result here concerns determination of the “local” behavior of individual services, if they are required to conform to a given “global” behavior (as might be specified using choreography constraints, reminiscent of WS-Choreography [17]). The talk also discu...